diff --git a/libs/base/Data/SnocList/HasLength.idr b/libs/base/Data/SnocList/HasLength.idr index dbb771aa2c..9f14d5912f 100644 --- a/libs/base/Data/SnocList/HasLength.idr +++ b/libs/base/Data/SnocList/HasLength.idr @@ -29,9 +29,9 @@ map f Z = Z map f (S hl) = S (map f hl) export -sucL : HasLength n sx -> HasLength (S n) ([ HasLength (S n) ([ HasLength n sy -> HasLength (n + m) (sx ++ sy) diff --git a/src/Core/Case/CaseTree.idr b/src/Core/Case/CaseTree.idr index 8b3e9f7ae0..76cf9f70c6 100644 --- a/src/Core/Case/CaseTree.idr +++ b/src/Core/Case/CaseTree.idr @@ -10,6 +10,7 @@ import Idris.Pretty.Annotations import Libraries.Data.NameMap import Libraries.Text.PrettyPrint.Prettyprinter import Libraries.Data.String.Extra -- needed for boostrapping +import Libraries.Data.SnocList.SizeOf %default covering @@ -197,7 +198,7 @@ mutual insertCaseNames : SizeOf outer -> SizeOf ns -> CaseTree (inner ++ outer) -> - CaseTree ((inner ++ ns) ++ outer) + CaseTree (inner ++ ns ++ outer) insertCaseNames outer ns (Case idx prf scTy alts) = let MkNVar prf' = insertNVarNames outer ns (MkNVar prf) in Case _ prf' (insertNames outer ns scTy) @@ -209,13 +210,23 @@ mutual insertCaseAltNames : SizeOf outer -> SizeOf ns -> CaseAlt (inner ++ outer) -> - CaseAlt ((inner ++ ns) ++ outer) + CaseAlt (inner ++ ns ++ outer) insertCaseAltNames p q (ConCase x tag args ct) - = ConCase x tag args - (rewrite appendAssociative args outer (inner ++ ns) in - insertCaseNames (mkSizeOf args + p) q {inner} - (rewrite sym (appendAssociative args outer inner) in - ct)) + = ConCase x tag args locals' + where + ct' : CaseTree (inner ++ (outer ++ args)) + ct' = rewrite (appendAssociative inner outer args) in ct + + locals : CaseTree (inner ++ (ns ++ (outer ++ args))) + locals = insertCaseNames (p + mkSizeOf args) q ct' + + locals' : CaseTree ((inner ++ (ns ++ outer)) ++ args) + locals' = do + rewrite (appendAssociative inner ns outer) + rewrite sym (appendAssociative (inner ++ ns) outer args) + rewrite sym (appendAssociative inner ns (outer ++ args)) + locals + insertCaseAltNames outer ns (DelayCase tyn valn ct) = DelayCase tyn valn (insertCaseNames (suc (suc outer)) ns ct) diff --git a/src/Core/CompileExpr.idr b/src/Core/CompileExpr.idr index 444b837902..1c8abb6919 100644 --- a/src/Core/CompileExpr.idr +++ b/src/Core/CompileExpr.idr @@ -273,12 +273,12 @@ mutual export data Names : SnocList Name -> Type where - Nil : Names [<] - (::) : Name -> Names xs -> Names (xs :< x) + Lin : Names [<] + (:<) : Names xs -> Name -> Names (xs :< x) elem : Name -> Names xs -> Bool -elem n [] = False -elem n (x :: xs) = n == x || elem n xs +elem n [<] = False +elem n (xs :< x) = n == x || elem n xs tryNext : Name -> Name tryNext (UN n) = MN (displayUserName n) 0 @@ -293,19 +293,19 @@ uniqueName s ns = export getLocName : (idx : Nat) -> Names vars -> (0 p : IsVar name idx vars) -> Name -getLocName Z (x :: xs) First = x -getLocName (S k) (x :: xs) (Later p) = getLocName k xs p +getLocName Z (xs :< x) First = x +getLocName (S k) (xs :< x) (Later p) = getLocName k xs p export addLocs : (args : SnocList Name) -> Names vars -> Names (vars ++ args) addLocs [<] ns = ns addLocs (xs :< x) ns = let rec = addLocs xs ns in - uniqueName x rec :: rec + rec :< uniqueName x rec -conArgs : (args : SnocList Name) -> Names (vars ++ args) -> List Name -conArgs [<] ns = [] -conArgs (as :< a) (n :: ns) = n :: conArgs as ns +conArgs : (args : SnocList Name) -> Names (vars ++ args) -> SnocList Name +conArgs [<] ns = [<] +conArgs (as :< a) (ns :< n) = conArgs as ns :< n mutual forgetExp : Names vars -> CExp vars -> NamedCExp @@ -344,7 +344,7 @@ mutual forgetConAlt : Names vars -> CConAlt vars -> NamedConAlt forgetConAlt locs (MkConAlt n ci t args exp) = let args' = addLocs args locs in - MkNConAlt n ci t (conArgs args args') (forgetExp args' exp) + MkNConAlt n ci t (cast $ conArgs args args') (forgetExp args' exp) forgetConstAlt : Names vars -> CConstAlt vars -> NamedConstAlt forgetConstAlt locs (MkConstAlt c exp) @@ -353,15 +353,15 @@ mutual export forget : {vars : _} -> CExp vars -> NamedCExp forget {vars} exp - = forgetExp (addLocs vars []) - (rewrite appendNilRightNeutral vars in exp) + = forgetExp (addLocs vars [<]) + (rewrite appendLinLeftNeutral vars in exp) export forgetDef : CDef -> NamedDef forgetDef (MkFun args def) - = let ns = addLocs args [] + = let ns = addLocs args [<] args' = conArgs {vars = [<]} args ns in - MkNmFun args' (forget def) + MkNmFun (cast args') (forget def) forgetDef (MkCon t a nt) = MkNmCon t a nt forgetDef (MkForeign ccs fargs ty) = MkNmForeign ccs fargs ty forgetDef (MkError err) = MkNmError (forget err) @@ -427,7 +427,7 @@ mutual insertNames : SizeOf outer -> SizeOf ns -> CExp (inner ++ outer) -> - CExp ((inner ++ ns) ++ outer) + CExp (inner ++ ns ++ outer) insertNames outer ns (CLocal fc prf) = let MkNVar var' = insertNVarNames outer ns (MkNVar prf) in CLocal fc var' @@ -461,18 +461,27 @@ mutual insertNamesConAlt : SizeOf outer -> SizeOf ns -> CConAlt (inner ++ outer) -> - CConAlt ((inner ++ ns) ++ outer) + CConAlt (inner ++ (ns ++ outer)) insertNamesConAlt {outer} {ns} p q (MkConAlt x ci tag args sc) - = let sc' : CExp (outer ++ (inner <>< args)) - = rewrite sym (appendAssociative args outer inner) in sc in - MkConAlt x ci tag args - (rewrite appendAssociative args outer (inner ++ ns) in - insertNames (mkSizeOf args + p) q sc') + = MkConAlt x ci tag args locals' + where + sc' : CExp (inner ++ (outer ++ args)) + sc' = rewrite (appendAssociative inner outer args) in sc + + locals : CExp (inner ++ (ns ++ (outer ++ args))) + locals = insertNames (p + mkSizeOf args) q sc' + + locals' : CExp ((inner ++ (ns ++ outer)) ++ args) + locals' = do + rewrite (appendAssociative inner ns outer) + rewrite sym (appendAssociative (inner ++ ns) outer args) + rewrite sym (appendAssociative inner ns (outer ++ args)) + locals insertNamesConstAlt : SizeOf outer -> SizeOf ns -> CConstAlt (inner ++ outer) -> - CConstAlt ((inner ++ ns) ++ outer) + CConstAlt (inner ++ (ns ++ outer)) insertNamesConstAlt outer ns (MkConstAlt x sc) = MkConstAlt x (insertNames outer ns sc) export @@ -571,10 +580,12 @@ mutual substConAlt : Substitutable CExp CConAlt substConAlt {vars} {outer} {dropped} p q env (MkConAlt x ci tag args sc) = MkConAlt x ci tag args - (rewrite appendAssociative args outer vars in - substEnv (mkSizeOf args + p) q env - (rewrite sym (appendAssociative args outer (vars ++ dropped)) in - sc)) + (rewrite (sym $ appendAssociative vars outer args) + in substEnv (p + mkSizeOf args) q env sc' + ) + where + sc' : CExp ((vars ++ dropped) ++ (outer ++ args)) + sc' = rewrite (appendAssociative (vars ++ dropped) outer args) in sc substConstAlt : Substitutable CExp CConstAlt substConstAlt outer dropped env (MkConstAlt x sc) = MkConstAlt x (substEnv outer dropped env sc) @@ -590,7 +601,7 @@ mutual mkLocals : SizeOf outer -> Bounds bound -> CExp (vars ++ outer) -> - CExp ((vars ++ bound) ++ outer) + CExp (vars ++ (bound ++ outer)) mkLocals later bs (CLocal {idx} {x} fc p) = let MkNVar p' = addVars later bs (MkNVar p) in CLocal {x} fc p' mkLocals later bs (CRef fc var) @@ -630,18 +641,27 @@ mutual mkLocalsConAlt : SizeOf outer -> Bounds bound -> CConAlt (vars ++ outer) -> - CConAlt ((vars ++ bound) ++ outer) + CConAlt (vars ++ (bound ++ outer)) mkLocalsConAlt {bound} {outer} {vars} p bs (MkConAlt x ci tag args sc) - = let sc' : CExp (outer ++ (vars <>< args)) - = rewrite sym (appendAssociative args outer vars) in sc in - MkConAlt x ci tag args - (rewrite appendAssociative args outer (vars ++ bound) in - mkLocals (mkSizeOf args + p) bs sc') + = MkConAlt x ci tag args locals' + where + sc' : CExp (vars ++ (outer ++ args)) + sc' = rewrite (appendAssociative vars outer args) in sc + + locals : CExp (vars ++ (bound ++ (outer ++ args))) + locals = mkLocals (p + mkSizeOf args) bs sc' + + locals' : CExp ((vars ++ (bound ++ outer)) ++ args) + locals' = do + rewrite (appendAssociative vars bound outer) + rewrite sym (appendAssociative (vars ++ bound) outer args) + rewrite sym (appendAssociative vars bound (outer ++ args)) + locals mkLocalsConstAlt : SizeOf outer -> Bounds bound -> CConstAlt (vars ++ outer) -> - CConstAlt ((vars ++ bound) ++ outer) + CConstAlt (vars ++ (bound ++ outer)) mkLocalsConstAlt later bs (MkConstAlt x sc) = MkConstAlt x (mkLocals later bs sc) export diff --git a/src/Core/Env.idr b/src/Core/Env.idr index 20104670e5..e4442a528f 100644 --- a/src/Core/Env.idr +++ b/src/Core/Env.idr @@ -1,50 +1,54 @@ module Core.Env import Core.TT +import Core.Name.CompatibleVars import Data.List import Data.SnocList +import Libraries.Data.SnocList.SizeOf +import Libraries.Data.SnocList.HasLength + %default total -- Environment containing types and values of local variables public export data Env : (tm : SnocList Name -> Type) -> SnocList Name -> Type where - Nil : Env tm [<] - (::) : Binder (tm vars) -> Env tm vars -> Env tm (vars :< x) + Lin : Env tm [<] + (:<) : Env tm vars -> Binder (tm vars) -> Env tm (vars :< x) %name Env rho export -extend : (x : Name) -> Binder (tm vars) -> Env tm vars -> Env tm (vars :< x) -extend x = (::) {x} +extend : (x : Name) -> Env tm vars -> Binder (tm vars) -> Env tm (vars :< x) +extend x = (:<) {x} export (++) : {ns : _} -> Env Term ns -> Env Term vars -> Env Term (vars ++ ns) -(++) (b :: bs) e = extend _ (map embed b) (bs ++ e) -(++) [] e = e +(++) (bs :< b) e = extend _ (bs ++ e) (map embed b) +(++) [<] e = e export length : Env tm xs -> Nat -length [] = 0 -length (_ :: xs) = S (length xs) +length [<] = 0 +length (xs :< _) = S (length xs) export lengthNoLet : Env tm xs -> Nat -lengthNoLet [] = 0 -lengthNoLet (Let _ _ _ _ :: xs) = lengthNoLet xs -lengthNoLet (_ :: xs) = S (lengthNoLet xs) +lengthNoLet [<] = 0 +lengthNoLet (xs :< Let _ _ _ _) = lengthNoLet xs +lengthNoLet (xs :< _) = S (lengthNoLet xs) export lengthExplicitPi : Env tm xs -> Nat -lengthExplicitPi [] = 0 -lengthExplicitPi (Pi _ _ Explicit _ :: rho) = S (lengthExplicitPi rho) -lengthExplicitPi (_ :: rho) = lengthExplicitPi rho +lengthExplicitPi [<] = 0 +lengthExplicitPi (rho :< Pi _ _ Explicit _) = S (lengthExplicitPi rho) +lengthExplicitPi (rho :< _) = lengthExplicitPi rho export namesNoLet : {xs : _} -> Env tm xs -> SnocList Name -namesNoLet [] = [<] -namesNoLet (Let _ _ _ _ :: xs) = namesNoLet xs -namesNoLet {xs = _ :< x} (_ :: env) = namesNoLet env :< x +namesNoLet [<] = [<] +namesNoLet (xs :< Let _ _ _ _) = namesNoLet xs +namesNoLet {xs = _ :< x} (env :< _) = namesNoLet env :< x public export data IsDefined : Name -> SnocList Name -> Type where @@ -55,8 +59,8 @@ export defined : {vars : _} -> (n : Name) -> Env Term vars -> Maybe (IsDefined n vars) -defined n [] = Nothing -defined {vars = xs :< x} n (b :: env) +defined n [<] = Nothing +defined {vars = xs :< x} n (env :< b) = case nameEq n x of Nothing => do MkIsDefined rig prf <- defined n env pure (MkIsDefined rig (Later prf)) @@ -66,28 +70,29 @@ defined {vars = xs :< x} n (b :: env) -- outer environment export bindEnv : {vars : _} -> FC -> Env Term vars -> (tm : Term vars) -> ClosedTerm -bindEnv loc [] tm = tm -bindEnv loc (b :: env) tm +bindEnv loc [<] tm = tm +bindEnv loc (env :< b) tm = bindEnv loc env (Bind loc _ (PVar (binderLoc b) (multiplicity b) Explicit (binderType b)) tm) +public export revOnto : (xs, vs : SnocList a) -> reverseOnto xs vs = xs ++ reverse vs revOnto xs [<] = Refl revOnto xs (vs :< v) = rewrite revOnto (xs :< v) vs in - rewrite appendAssociative (reverse vs) [ reverse vs ++ reverse ns = reverse (ns ++ vs) -revNs [<] ns = rewrite appendNilRightNeutral (reverse ns) in Refl +revNs [<] ns = rewrite appendLinLeftNeutral (reverse ns) in Refl revNs (vs :< v) ns = rewrite revOnto [ (ns : SnocList Name) -> (0 p : IsVar x idx vars) -> Env tm vars -> Binder (tm (reverseOnto vars ns)) -getBinderUnder {idx = Z} {vars = vs :< v} ns First (b :: env) - = rewrite revOnto vs (ns :< v) in map (weakenNs (reverse (mkSizeOf ((ns :< v))))) b -getBinderUnder {idx = S k} {vars = vs :< v} ns (Later lp) (b :: env) +getBinderUnder {idx = Z} {vars = vs :< v} ns First (env :< b) + = rewrite revOnto (vs :< x) ns in + rewrite sym $ appendAssociative vs [ {vars : _} -> {idx : Nat} -> @@ -113,8 +121,8 @@ getBinder el env = getBinderUnder [<] el env -- needlessly weaken stuff; export getBinderLoc : {vars : _} -> {idx : Nat} -> (0 p : IsVar x idx vars) -> Env tm vars -> FC -getBinderLoc {idx = Z} First (b :: _) = binderLoc b -getBinderLoc {idx = S k} (Later p) (_ :: env) = getBinderLoc p env +getBinderLoc {idx = Z} First (_ :< b) = binderLoc b +getBinderLoc {idx = S k} (Later p) (env :< _) = getBinderLoc p env -- Make a type which abstracts over an environment -- Don't include 'let' bindings, since they have a concrete value and @@ -122,12 +130,12 @@ getBinderLoc {idx = S k} (Later p) (_ :: env) = getBinderLoc p env export abstractEnvType : {vars : _} -> FC -> Env Term vars -> (tm : Term vars) -> ClosedTerm -abstractEnvType fc [] tm = tm -abstractEnvType fc (Let fc' c val ty :: env) tm +abstractEnvType fc [<] tm = tm +abstractEnvType fc (env :< Let fc' c val ty) tm = abstractEnvType fc env (Bind fc _ (Let fc' c val ty) tm) -abstractEnvType fc (Pi fc' c e ty :: env) tm +abstractEnvType fc (env :< Pi fc' c e ty) tm = abstractEnvType fc env (Bind fc _ (Pi fc' c e ty) tm) -abstractEnvType fc (b :: env) tm +abstractEnvType fc (env :< b) tm = let bnd = Pi (binderLoc b) (multiplicity b) Explicit (binderType b) in abstractEnvType fc env (Bind fc _ bnd tm) @@ -135,10 +143,10 @@ abstractEnvType fc (b :: env) tm export abstractEnv : {vars : _} -> FC -> Env Term vars -> (tm : Term vars) -> ClosedTerm -abstractEnv fc [] tm = tm -abstractEnv fc (Let fc' c val ty :: env) tm +abstractEnv fc [<] tm = tm +abstractEnv fc (env :< Let fc' c val ty) tm = abstractEnv fc env (Bind fc _ (Let fc' c val ty) tm) -abstractEnv fc (b :: env) tm +abstractEnv fc (env :< b) tm = let bnd = Lam (binderLoc b) (multiplicity b) Explicit (binderType b) in abstractEnv fc env (Bind fc _ bnd tm) @@ -146,18 +154,18 @@ abstractEnv fc (b :: env) tm export abstractFullEnvType : {vars : _} -> FC -> Env Term vars -> (tm : Term vars) -> ClosedTerm -abstractFullEnvType fc [] tm = tm -abstractFullEnvType fc (Pi fc' c e ty :: env) tm +abstractFullEnvType fc [<] tm = tm +abstractFullEnvType fc (env :< Pi fc' c e ty) tm = abstractFullEnvType fc env (Bind fc _ (Pi fc' c e ty) tm) -abstractFullEnvType fc (b :: env) tm +abstractFullEnvType fc (env :< b) tm = let bnd = Pi fc (multiplicity b) Explicit (binderType b) in abstractFullEnvType fc env (Bind fc _ bnd tm) export letToLam : Env Term vars -> Env Term vars -letToLam [] = [] -letToLam (Let fc c val ty :: env) = Lam fc c Explicit ty :: letToLam env -letToLam (b :: env) = b :: letToLam env +letToLam [<] = [<] +letToLam (env :< Let fc c val ty) = letToLam env :< Lam fc c Explicit ty +letToLam (env :< b) = letToLam env :< b mutual -- Quicker, if less safe, to store variables as a Nat, for quick comparison @@ -180,7 +188,7 @@ mutual = findUsedArgs env (findUsed env u a) as findUsed env used (Bind fc x b tm) = assert_total $ - dropS (findUsed (b :: env) + dropS (findUsed (env :< b) (map S (findUsedInBinder env used b)) tm) where @@ -256,26 +264,25 @@ findSubEnv env tm = mkShrink (findUsedLocs env tm) export shrinkEnv : Env Term vars -> Thin newvars vars -> Maybe (Env Term newvars) shrinkEnv env Refl = Just env -shrinkEnv (b :: env) (Drop p) = shrinkEnv env p -shrinkEnv (b :: env) (Keep p) +shrinkEnv (env :< b) (Drop p) = shrinkEnv env p +shrinkEnv (env :< b) (Keep p) = do env' <- shrinkEnv env p b' <- assert_total (shrinkBinder b p) - pure (b' :: env') + pure (env' :< b') export mkEnvOnto : FC -> (xs : SnocList Name) -> Env Term ys -> Env Term (ys ++ xs) mkEnvOnto fc [<] vs = vs mkEnvOnto fc (ns :< n) vs - = PVar fc top Explicit (Erased fc Placeholder) - :: mkEnvOnto fc ns vs + = mkEnvOnto fc ns vs :< PVar fc top Explicit (Erased fc Placeholder) -- Make a dummy environment, if we genuinely don't care about the values -- and types of the contents. -- We use this when building and comparing case trees. export mkEnv : FC -> (vs : SnocList Name) -> Env Term vs -mkEnv fc [<] = [] -mkEnv fc (ns :< n) = PVar fc top Explicit (Erased fc Placeholder) :: mkEnv fc ns +mkEnv fc [<] = [<] +mkEnv fc (ns :< n) = mkEnv fc ns :< PVar fc top Explicit (Erased fc Placeholder) -- Update an environment so that all names are guaranteed unique. In the -- case of a clash, the most recently bound is left unchanged. @@ -305,38 +312,37 @@ uniqifyEnv env = uenv [<] env uenv : {vars : _} -> SnocList Name -> Env Term vars -> (vars' ** (Env Term vars', CompatibleVars vars vars')) - uenv used [] = ([<] ** ([], Pre)) - uenv used {vars = vs :< v} (b :: bs) + uenv used [<] = ([<] ** ([<], Pre)) + uenv used {vars = vs :< v} (bs :< b) = if v `elem` used then let v' = uniqueLocal used v (vs' ** (env', compat)) = uenv (used :< v') bs b' = map (compatNs compat) b in - (vs' :< v' ** (b' :: env', Ext compat)) + (vs' :< v' ** (env' :< b', Ext compat)) else let (vs' ** (env', compat)) = uenv (used :< v) bs b' = map (compatNs compat) b in - (vs' :< v ** (b' :: env', Ext compat)) + (vs' :< v ** (env' :< b', Ext compat)) export allVars : {vars : _} -> Env Term vars -> List (Var vars) -allVars [] = [] -allVars (v :: vs) = MkVar First :: map weaken (allVars vs) +allVars [<] = [] +allVars (vs :< v) = MkVar First :: map weaken (allVars vs) export allVarsNoLet : {vars : _} -> Env Term vars -> List (Var vars) -allVarsNoLet [] = [] -allVarsNoLet (Let _ _ _ _ :: vs) = map weaken (allVars vs) -allVarsNoLet (v :: vs) = MkVar First :: map weaken (allVars vs) +allVarsNoLet [<] = [] +allVarsNoLet (vs :< Let _ _ _ _) = map weaken (allVars vs) +allVarsNoLet (vs :< v) = MkVar First :: map weaken (allVars vs) export close : FC -> String -> Env Term vars -> Term vars -> ClosedTerm close fc nm env tm = let (s, env) = mkSubstEnv 0 env in - substs s env (rewrite appendNilRightNeutral vars in tm) + substs s env (rewrite appendLinLeftNeutral vars in tm) where - mkSubstEnv : Int -> Env Term vs -> (SizeOf vs, SubstEnv vs [<]) - mkSubstEnv i [] = (zero, []) - mkSubstEnv i (v :: vs) + mkSubstEnv i [<] = (zero, [<]) + mkSubstEnv i (vs :< v) = let (s, env) = mkSubstEnv (i + 1) vs in - (suc s, Ref fc Bound (MN nm i) :: env) + (suc s, env :< Ref fc Bound (MN nm i)) diff --git a/src/Core/Name/Scoped.idr b/src/Core/Name/Scoped.idr index d6edd3507b..0604077743 100644 --- a/src/Core/Name/Scoped.idr +++ b/src/Core/Name/Scoped.idr @@ -113,7 +113,7 @@ Strengthenable tm = {0 vars, ns : Scope} -> public export 0 GenWeakenable : Scoped -> Type GenWeakenable tm = {0 local, ns, outer : Scope} -> - SizeOf outer -> SizeOf ns -> tm (local ++ outer) -> tm ((local ++ ns) ++ outer) + SizeOf outer -> SizeOf ns -> tm (local ++ outer) -> tm (local ++ ns ++ outer) public export 0 Thinnable : Scoped -> Type @@ -147,7 +147,7 @@ interface GenWeaken (0 tm : Scoped) where export genWeaken : GenWeaken tm => - SizeOf outer -> tm (local ++ outer) -> tm (local :< n ++ outer) + SizeOf outer -> tm (local ++ outer) -> tm (local ++ ([ Type where - None : Bounds [] - Add : (x : Name) -> Name -> Bounds xs -> Bounds (x :: xs) + data Bounds : SnocList Name -> Type where + None : Bounds [<] + Add : (x : Name) -> Name -> Bounds xs -> Bounds (xs :< x) export - sizeOf : Bounds xs -> Libraries.Data.List.SizeOf.SizeOf xs + sizeOf : Bounds xs -> Libraries.Data.SnocList.SizeOf.SizeOf xs sizeOf None = zero sizeOf (Add _ _ b) = suc (sizeOf b) export addVars : SizeOf outer -> Bounds bound -> NVar name (vars ++ outer) -> - NVar name ((vars ++ bound) ++ outer) + NVar name (vars ++ bound ++ outer) addVars p = insertNVarNames p . sizeOf export resolveRef : SizeOf outer -> SizeOf done -> Bounds bound -> FC -> Name -> - Maybe (Var ((done <>> (vars ++ bound)) ++ outer)) + Maybe (Var (vars ++ (bound ++ done) ++ outer)) resolveRef _ _ None _ _ = Nothing -resolveRef {outer} {vars} {done} p q (Add {xs} new old bs) fc n +resolveRef {outer} {done} p q (Add {xs} new old bs) fc n = if n == old - then Just (weakenNs p (mkVarChiply q)) - else resolveRef p (q :< new) bs fc n + then do + rewrite appendAssociative vars ((xs :< new) ++ done) outer + rewrite appendAssociative vars (xs :< new) done + Just $ weakenNs {tm = Var} p (mkVar q) + else do + rewrite sym $ appendAssociative xs [ Bounds bound -> - Term (vars ++ outer) -> Term ((vars ++ bound) ++ outer) + Term (vars ++ outer) -> Term (vars ++ (bound ++ outer)) mkLocals outer bs (Local fc r idx p) = let MkNVar p' = addVars outer bs (MkNVar p) in Local fc r _ p' mkLocals outer bs (Ref fc Bound name) diff --git a/src/Core/TT/Term/Subst.idr b/src/Core/TT/Term/Subst.idr index 9e7c880e21..8d15ea9bdf 100644 --- a/src/Core/TT/Term/Subst.idr +++ b/src/Core/TT/Term/Subst.idr @@ -56,4 +56,4 @@ substs dropped env tm = substTerm zero dropped env tm export subst : Term vars -> Term (vars :< x) -> Term vars -subst val tm = substs (suc zero) [val] tm +subst val tm = substs (suc zero) [ embedNVar v - Right v => - rewrite sym $ appendAssociative local ns outer in - weakenNVar (q + p) v + Left v => rewrite appendAssociative local ns outer in embedNVar v + Right v => weakenNVar (q + p) v ||| The (partial) inverse to insertNVar export diff --git a/src/Libraries/Data/SnocList/HasLength.idr b/src/Libraries/Data/SnocList/HasLength.idr index eda9f7a5e0..a0c55a5252 100644 --- a/src/Libraries/Data/SnocList/HasLength.idr +++ b/src/Libraries/Data/SnocList/HasLength.idr @@ -23,9 +23,9 @@ hasLength Z = Refl hasLength (S p) = cong S (hasLength p) export -sucL : HasLength n sx -> HasLength (S n) ([ HasLength (S n) ([ HasLength n sy -> HasLength (n + m) (sx ++ sy) diff --git a/src/Libraries/Data/SnocList/SizeOf.idr b/src/Libraries/Data/SnocList/SizeOf.idr index b860858cca..3b23027bfd 100644 --- a/src/Libraries/Data/SnocList/SizeOf.idr +++ b/src/Libraries/Data/SnocList/SizeOf.idr @@ -44,10 +44,10 @@ public export suc : SizeOf as -> SizeOf (as :< a) suc (MkSizeOf n p) = MkSizeOf (S n) (S p) --- ||| suc but from the left +-- ||| suc but from the right export -sucL : SizeOf as -> SizeOf ([ SizeOf ([<) : SizeOf {a} sx -> LSizeOf {a} ys -> SizeOf (sx <>< ys)