diff --git a/src/Compiler/Inline.idr b/src/Compiler/Inline.idr index 90d8d506b9..38a511f417 100644 --- a/src/Compiler/Inline.idr +++ b/src/Compiler/Inline.idr @@ -22,17 +22,21 @@ import Libraries.Data.List.LengthMatch import Libraries.Data.NameMap import Libraries.Data.WithDefault +import Libraries.Data.SnocList.LengthMatch +import Libraries.Data.SnocList.SizeOf +import Libraries.Data.SnocList.HasLength + %default covering data EEnv : SnocList Name -> SnocList Name -> Type where - Nil : EEnv free [<] - (::) : CExp free -> EEnv free vars -> EEnv free (vars :< x) + Lin : EEnv free [<] + (:<) : EEnv free vars -> CExp free -> EEnv free (vars :< x) extend : EEnv free vars -> (args : SnocList (CExp free)) -> (args' : SnocList Name) -> LengthMatch args args' -> EEnv free (vars ++ args') -extend env [<] [<] NilMatch = env -extend env (xs :< a) (ns :< n) (ConsMatch w) - = a :: extend env xs ns w +extend env [<] [<] LinMatch = env +extend env (xs :< a) (ns :< n) (SnocMatch w) + = extend env xs ns w :< a Stack : SnocList Name -> Type Stack vars = List (CExp vars) @@ -54,7 +58,7 @@ takeFromStack : EEnv free vars -> Stack free -> (args : SnocList Name) -> Maybe (EEnv free (vars ++ args), Stack free) takeFromStack env (e :: es) (as :< a) = do (env', stk') <- takeFromStack env es as - pure (e :: env', stk') + pure (env' :< e, stk') takeFromStack env stk [<] = pure (env, stk) takeFromStack env [] args = Nothing @@ -123,11 +127,11 @@ mutual Core (CExp free) evalLocal {vars = [<]} fc rec stk env p = pure $ unload stk (CLocal fc p) - evalLocal {vars = xs :< x} fc rec stk (v :: env) First + evalLocal {vars = xs :< x} fc rec stk (env :< v) First = case stk of [] => pure v _ => eval rec env stk (weakenNs (mkSizeOf xs) v) - evalLocal {vars = xs :< x} fc rec stk (_ :: env) (Later p) + evalLocal {vars = xs :< x} fc rec stk (env :< _) (Later p) = evalLocal fc rec stk env p tryApply : {vars, free : _} -> @@ -139,7 +143,7 @@ mutual = do let Just (env', stk') = takeFromStack env stk args | Nothing => pure Nothing res <- eval rec env' stk' - (rewrite sym (appendAssociative args vars free) in + (rewrite appendAssociative free vars args in embed {outer = free ++ vars} exp) pure (Just res) tryApply rec stk env _ = pure Nothing @@ -162,7 +166,7 @@ mutual case (n == NS primIONS (UN $ Basic "io_bind"), stk) of (True, act :: cont :: world :: stk) => do xn <- genName "act" - sc <- eval rec [] [] (CApp fc cont [CRef fc xn, world]) + sc <- eval rec [<] [] (CApp fc cont [CRef fc xn, world]) pure $ unload stk $ CLet fc xn NotInline (CApp fc act [world]) @@ -171,7 +175,7 @@ mutual do wn <- genName "world" xn <- genName "act" let world : forall vars. CExp vars := CRef fc wn - sc <- eval rec [] [] (CApp fc cont [CRef fc xn, world]) + sc <- eval rec [<] [] (CApp fc cont [CRef fc xn, world]) pure $ CLam fc wn $ refToLocal wn wn $ CLet fc xn NotInline (CApp fc act [world]) @@ -193,12 +197,12 @@ mutual else pure $ unloadApp arity stk (CRef fc n) eval {vars} {free} rec env [] (CLam fc x sc) = do xn <- genName "lamv" - sc' <- eval rec (CRef fc xn :: env) [] sc + sc' <- eval rec (env :< CRef fc xn) [] sc pure $ CLam fc x (refToLocal xn x sc') - eval rec env (e :: stk) (CLam fc x sc) = eval rec (e :: env) stk sc + eval rec env (e :: stk) (CLam fc x sc) = eval rec (env :< e) stk sc eval {vars} {free} rec env stk (CLet fc x NotInline val sc) = do xn <- genName "letv" - sc' <- eval rec (CRef fc xn :: env) [] sc + sc' <- eval rec (env :< CRef fc xn) [] sc val' <- eval rec env [] val pure (unload stk $ CLet fc x NotInline val' (refToLocal xn x sc')) eval {vars} {free} rec env stk (CLet fc x YesInline val sc) @@ -207,9 +211,9 @@ mutual -- are guaranteed not to duplicate work. (We don't know -- that yet). then do val' <- eval rec env [] val - eval rec (val' :: env) stk sc + eval rec (env :< val') stk sc else do xn <- genName "letv" - sc' <- eval rec (CRef fc xn :: env) stk sc + sc' <- eval rec (env :< CRef fc xn) stk sc val' <- eval rec env [] val pure (CLet fc x YesInline val' (refToLocal xn x sc')) eval rec env stk (CApp fc f@(CRef nfc n) args) @@ -231,7 +235,7 @@ mutual = pure $ unload stk $ CExtPrim fc p !(traverse (eval rec env []) args) eval rec env stk (CForce fc lr e) = case !(eval rec env [] e) of - CDelay _ _ e' => eval rec [] stk e' + CDelay _ _ e' => eval rec [<] stk e' res => pure $ unload stk (CForce fc lr res) -- change this to preserve laziness semantics eval rec env stk (CDelay fc lr e) = pure $ unload stk (CDelay fc lr !(eval rec env [] e)) @@ -248,8 +252,8 @@ mutual (0 p : IsVar x idx (free ++ vs)) -> EEnv free vs -> CExp free -> EEnv free vs updateLoc {vs = [<]} p env val = env - updateLoc {vs = (xs :< x)} First (e :: env) val = val :: env - updateLoc {vs = (xs :< y)} (Later p) (e :: env) val = e :: updateLoc p env val + updateLoc {vs = (xs :< x)} First (env :< e) val = env :< val + updateLoc {vs = (xs :< y)} (Later p) (env :< e) val = updateLoc p env val :< e update : {vs : _} -> CExp (free ++ vs) -> EEnv free vs -> CExp free -> EEnv free vs @@ -274,7 +278,7 @@ mutual extendLoc fc env (ns :< n) = do xn <- genName "cv" (bs', env') <- extendLoc fc env ns - pure (Add n xn bs', CRef fc xn :: env') + pure (Add n xn bs', env' :< CRef fc xn) evalAlt : {vars, free : _} -> {auto c : Ref Ctxt Defs} -> @@ -284,7 +288,7 @@ mutual evalAlt {free} {vars} fc rec env stk (MkConAlt n ci t args sc) = do (bs, env') <- extendLoc fc env args scEval <- eval rec env' stk - (rewrite sym (appendAssociative args vars free) in sc) + (rewrite appendAssociative free vars args in sc) pure $ MkConAlt n ci t args (refsToLocals bs scEval) evalConstAlt : {vars, free : _} -> @@ -306,7 +310,7 @@ mutual = traverseOpt (eval rec env stk) def pickAlt {vars} {free} rec env stk con@(CCon fc n ci t args) (MkConAlt n' _ t' args' sc :: alts) def = - let args'' = fromList args + let args'' = cast args in if matches n t n' t' then case checkLengthMatch args'' args' of Nothing => pure Nothing @@ -314,7 +318,7 @@ mutual do let env' : EEnv free (vars ++ args') = extend env args'' args' m pure $ Just !(eval rec env' stk - (rewrite sym (appendAssociative args' vars free) in + (rewrite appendAssociative free vars args' in sc)) else pickAlt rec env stk con alts def where @@ -421,18 +425,18 @@ getLams : {done : _} -> SizeOf done -> Int -> SubstCEnv done args -> CExp (args ++ done) -> (args' ** (SizeOf args', SubstCEnv args' args, CExp (args ++ args'))) getLams {done} d i env (CLam fc x sc) - = getLams {done = done :< x} (suc d) (i + 1) (CRef fc (MN "ext" i) :: env) sc + = getLams {done = done :< x} (suc d) (i + 1) (env :< CRef fc (MN "ext" i)) sc getLams {done} d i env sc = (done ** (d, env, sc)) -mkBounds : (xs : _) -> Core.Name.SnocList.Bounds xs +mkBounds : (xs : _) -> Bounds xs mkBounds [<] = None mkBounds (xs :< x) = Add x x (mkBounds xs) getNewArgs : {done : _} -> SubstCEnv done args -> SnocList Name -getNewArgs [] = [<] -getNewArgs (CRef _ n :: xs) = getNewArgs xs :< n -getNewArgs {done = xs :< x} (_ :: sub) = getNewArgs sub :< x +getNewArgs [<] = [<] +getNewArgs (xs :< CRef _ n) = getNewArgs xs :< n +getNewArgs {done = xs :< x} (sub :< _) = getNewArgs sub :< x -- Move any lambdas in the body of the definition into the lhs list of vars. -- Annoyingly, the indices will need fixing up because the order in the top @@ -440,11 +444,11 @@ getNewArgs {done = xs :< x} (_ :: sub) = getNewArgs sub :< x -- not the highest, as you'd expect if they were all lambdas). mergeLambdas : (args : SnocList Name) -> CExp args -> (args' ** CExp args') mergeLambdas args (CLam fc x sc) - = let (args' ** (s, env, exp')) = getLams zero 0 [] (CLam fc x sc) + = let (args' ** (s, env, exp')) = getLams zero 0 [<] (CLam fc x sc) expNs = substs s env exp' newArgs = reverse $ getNewArgs env expLocs = mkLocals (mkSizeOf args) {vars = [<]} (mkBounds newArgs) - (rewrite appendNilRightNeutral args in expNs) in + (rewrite appendLinLeftNeutral args in expNs) in (_ ** expLocs) mergeLambdas args exp = (args ** exp) @@ -457,7 +461,7 @@ doEval : {args : _} -> doEval n exp = do l <- newRef LVar (the Int 0) log "compiler.inline.eval" 10 (show n ++ ": " ++ show exp) - exp' <- eval [] [] [] exp + exp' <- eval [] [<] [] exp log "compiler.inline.eval" 10 ("Inlined: " ++ show exp') pure exp' diff --git a/src/Core/Name.idr b/src/Core/Name.idr index ee466b056d..c4829364ef 100644 --- a/src/Core/Name.idr +++ b/src/Core/Name.idr @@ -449,9 +449,9 @@ nameEq (Resolved x) (Resolved y) with (decEq x y) nameEq _ _ = Nothing export -namesEq : (xs, ys : List Name) -> Maybe (xs = ys) -namesEq [] [] = Just Refl -namesEq (x :: xs) (y :: ys) +namesEq : (xs : SnocList Name) -> (ys : SnocList Name) -> Maybe (xs = ys) +namesEq [<] [<] = Just Refl +namesEq (xs :< x) (ys :< y) = do p <- nameEq x y ps <- namesEq xs ys rewrite p diff --git a/src/Core/TTC.idr b/src/Core/TTC.idr index 715b17bfae..9a16c23a27 100644 --- a/src/Core/TTC.idr +++ b/src/Core/TTC.idr @@ -483,16 +483,16 @@ mutual export {vars : _} -> TTC (Env Term vars) where - toBuf b [] = pure () - toBuf b ((::) bnd env) + toBuf b [<] = pure () + toBuf b (env :< bnd) = do toBuf b bnd; toBuf b env -- Length has to correspond to length of 'vars' - fromBuf {vars = [<]} b = pure Nil + fromBuf {vars = [<]} b = pure Lin fromBuf {vars = xs :< x} b = do bnd <- fromBuf b env <- fromBuf b - pure (bnd :: env) + pure (env :< bnd) export TTC Visibility where diff --git a/src/Core/UnifyState.idr b/src/Core/UnifyState.idr index de4f6128e9..8938cdedb5 100644 --- a/src/Core/UnifyState.idr +++ b/src/Core/UnifyState.idr @@ -317,71 +317,78 @@ addPolyConstraint fc env arg x@(NApp _ (NMeta _ _ _) _) y addPolyConstraint fc env arg x y = pure () -mkLocal : {wkns : SnocList Name} -> FC -> Binder (Term vars) -> Term (wkns <>> (done ++ vars) :< x) -mkLocal fc b = Local fc (Just (isLet b)) _ (mkIsVarChiply (mkHasLength wkns)) +mkLocal : {wkns : SnocList Name} -> FC -> Binder (Term vars) -> Term (((done ++ vars) :< x ++ wkns)) +mkLocal fc b = Local fc (Just (isLet b)) _ (mkIsVar (mkHasLength wkns)) mkConstantAppArgs : {vars : _} -> Bool -> FC -> Env Term vars -> (wkns : SnocList Name) -> - List (Term (wkns <>> (done ++ vars))) -mkConstantAppArgs lets fc [] wkns = [] -mkConstantAppArgs {done} {vars = xs :< x} lets fc (b :: env) wkns - = let rec = mkConstantAppArgs {done} lets fc env (wkns :< x) in + List (Term ((done ++ vars) ++ wkns)) +mkConstantAppArgs lets fc [<] wkns = [] +mkConstantAppArgs {done} {vars = xs :< x} lets fc (env :< b) wkns + = let rec = mkConstantAppArgs {done} lets fc env (cons x wkns) in if lets || not (isLet b) - then mkLocal fc b :: rec - else rec + then mkLocal fc b :: + rewrite sym $ appendAssociative (done ++ xs) [ Bool -> FC -> Env Term vars -> Thin smaller vars -> (wkns : SnocList Name) -> - List (Term (wkns <>> (done ++ vars))) -mkConstantAppArgsSub lets fc [] p wkns = [] + List (Term ((done ++ vars) ++ wkns)) +mkConstantAppArgsSub lets fc [<] p wkns = [] mkConstantAppArgsSub {done} {vars = xs :< x} - lets fc (b :: env) Refl wkns - = mkConstantAppArgs lets fc env (wkns :< x) + lets fc (env :< b) Refl wkns + = rewrite sym $ appendAssociative (done ++ xs) [ Bool -> FC -> Env Term vars -> Thin smaller vars -> (wkns : SnocList Name) -> - List (Term (wkns <>> (done ++ vars))) -mkConstantAppArgsOthers lets fc [] p wkns = [] + List (Term ((done ++ vars) ++ wkns)) +mkConstantAppArgsOthers lets fc [<] p wkns = [] mkConstantAppArgsOthers {done} {vars = xs :< x} - lets fc (b :: env) Refl wkns - = mkConstantAppArgsOthers lets fc env Refl (wkns :< x) + lets fc (env :< b) Refl wkns + = rewrite sym $ appendAssociative (done ++ xs) [ FC -> Term vars -> Env Term vars -> Term vars applyTo fc tm env = let args = reverse (mkConstantAppArgs {done = [<]} False fc env [<]) in - apply fc tm (rewrite sym (appendNilRightNeutral vars) in args) + apply fc tm (rewrite sym (appendLinLeftNeutral vars) in args) export applyToFull : {vars : _} -> FC -> Term vars -> Env Term vars -> Term vars applyToFull fc tm env = let args = reverse (mkConstantAppArgs {done = [<]} True fc env [<]) in - apply fc tm (rewrite sym (appendNilRightNeutral vars) in args) + apply fc tm (rewrite sym (appendLinLeftNeutral vars) in args) export applyToSub : {vars : _} -> @@ -389,7 +396,7 @@ applyToSub : {vars : _} -> Thin smaller vars -> Term vars applyToSub fc tm env sub = let args = reverse (mkConstantAppArgsSub {done = [<]} True fc env sub [<]) in - apply fc tm (rewrite sym (appendNilRightNeutral vars) in args) + apply fc tm (rewrite sym (appendLinLeftNeutral vars) in args) export applyToOthers : {vars : _} -> @@ -397,7 +404,7 @@ applyToOthers : {vars : _} -> Thin smaller vars -> Term vars applyToOthers fc tm env sub = let args = reverse (mkConstantAppArgsOthers {done = [<]} True fc env sub [<]) in - apply fc tm (rewrite sym (appendNilRightNeutral vars) in args) + apply fc tm (rewrite sym (appendLinLeftNeutral vars) in args) -- Create a new metavariable with the given name and return type, -- and return a term which is the metavariable applied to the environment @@ -425,7 +432,7 @@ newMetaLets {vars} fc rig env n ty def nocyc lets where envArgs : List (Term vars) envArgs = let args = reverse (mkConstantAppArgs {done = [<]} lets fc env [<]) in - rewrite sym (appendNilRightNeutral vars) in args + (rewrite sym (appendLinLeftNeutral vars) in args) export newMeta : {vars : _} -> @@ -439,10 +446,10 @@ newMeta fc r env n ty def cyc = newMetaLets fc r env n ty def cyc False mkConstant : {vars : _} -> FC -> Env Term vars -> Term vars -> ClosedTerm -mkConstant fc [] tm = tm +mkConstant fc [<] tm = tm -- mkConstant {vars = x :: _} fc (Let c val ty :: env) tm -- = mkConstant fc env (Bind fc x (Let c val ty) tm) -mkConstant {vars = _ :< x} fc (b :: env) tm +mkConstant {vars = _ :< x} fc (env :< b) tm = let ty = binderType b in mkConstant fc env (Bind fc x (Lam fc (multiplicity b) Explicit ty) tm) @@ -471,7 +478,7 @@ newConstant {vars} fc rig env tm ty constrs where envArgs : List (Term vars) envArgs = let args = reverse (mkConstantAppArgs {done = [<]} True fc env [<]) in - rewrite sym (appendNilRightNeutral vars) in args + rewrite sym $ appendLinLeftNeutral vars in args -- Create a new search with the given name and return type, -- and return a term which is the name applied to the environment @@ -486,14 +493,14 @@ newSearch {vars} fc rig depth def env n ty = do let hty = abstractEnvType fc env ty let hole = newDef fc n rig [<] hty (specified Public) (BySearch rig depth def) log "unify.search" 10 $ "Adding new search " ++ show fc ++ " " ++ show n - logTermNF "unify.search" 10 "New search type" [] hty + logTermNF "unify.search" 10 "New search type" [<] hty idx <- addDef n hole addGuessName fc n idx pure (idx, Meta fc n idx envArgs) where envArgs : List (Term vars) envArgs = let args = reverse (mkConstantAppArgs {done = [<]} False fc env [<]) in - rewrite sym (appendNilRightNeutral vars) in args + rewrite sym $ appendLinLeftNeutral vars in args -- Add a hole which stands for a delayed elaborator export @@ -513,7 +520,7 @@ newDelayed {vars} fc rig env n ty where envArgs : List (Term vars) envArgs = let args = reverse (mkConstantAppArgs {done = [<]} False fc env [<]) in - rewrite sym (appendNilRightNeutral vars) in args + rewrite sym $ appendLinLeftNeutral vars in args export tryErrorUnify : {auto c : Ref Ctxt Defs} -> @@ -586,7 +593,7 @@ checkValidHole base (idx, (fc, n)) do defs <- get Ctxt Just ty <- lookupTyExact n (gamma defs) | Nothing => pure () - throw (CantSolveGoal fc (gamma defs) [] ty Nothing) + throw (CantSolveGoal fc (gamma defs) [<] ty Nothing) Guess tm envb (con :: _) => do ust <- get UST let Just c = lookup con (constraints ust) @@ -619,13 +626,13 @@ checkUserHolesAfter : {auto u : Ref UST UState} -> Int -> Bool -> Core () checkUserHolesAfter base now = do gs_map <- getGuesses - let gs = toScopedList gs_map + let gs = toList gs_map log "unify.unsolved" 10 $ "Unsolved guesses " ++ show gs - Core.Core.SnocList.traverse_ (checkValidHole base) gs + Core.Core.traverse_ (checkValidHole base) gs hs_map <- getCurrentHoles - let hs = toScopedList hs_map + let hs = toList hs_map let hs' = if any isUserName (map (snd . snd) hs) - then Core.Name.SnocList.Lin else hs + then [] else hs when (now && not (isNil hs')) $ throw (UnsolvedHoles (map snd (nubBy nameEq $ toList hs))) -- Note the hole names, to ensure they are resolved @@ -662,34 +669,34 @@ dumpHole str n hole (Guess tm envb constraints, ty) => do logString str n $ "!" ++ show !(getFullName (Resolved hole)) ++ " : " - ++ show !(toFullNames !(normaliseHoles defs [] ty)) + ++ show !(toFullNames !(normaliseHoles defs [<] ty)) ++ "\n\t = " - ++ show !(normaliseHoles defs [] tm) + ++ show !(normaliseHoles defs [<] tm) ++ "\n\twhen" traverse_ dumpConstraint constraints (Hole _ p, ty) => logString str n $ "?" ++ show (fullname gdef) ++ " : " - ++ show !(normaliseHoles defs [] ty) + ++ show !(normaliseHoles defs [<] ty) ++ if implbind p then " (ImplBind)" else "" ++ if invertible gdef then " (Invertible)" else "" (BySearch _ _ _, ty) => logString str n $ "Search " ++ show hole ++ " : " ++ - show !(toFullNames !(normaliseHoles defs [] ty)) + show !(toFullNames !(normaliseHoles defs [<] ty)) (PMDef _ args t _ _, ty) => log str 4 $ "Solved: " ++ show hole ++ " : " ++ - show !(normalise defs [] ty) ++ - " = " ++ show !(normalise defs [] (Ref emptyFC Func (Resolved hole))) + show !(normalise defs [<] ty) ++ + " = " ++ show !(normalise defs [<] (Ref emptyFC Func (Resolved hole))) (ImpBind, ty) => log str 4 $ "Bound: " ++ show hole ++ " : " ++ - show !(normalise defs [] ty) + show !(normalise defs [<] ty) (Delayed, ty) => log str 4 $ "Delayed elaborator : " ++ - show !(normalise defs [] ty) + show !(normalise defs [<] ty) _ => pure () where dumpConstraint : Int -> Core ()