ScopedSnocList: WIP: trivial constructor substitutions

src/Core/Case/CaseBuilder.idr

@@ -19,6 +19,7 @@ import Data.String
 import Data.Vect
 import Libraries.Data.List.LengthMatch
 import Libraries.Data.SortedSet
+import Libraries.Data.SnocList.SizeOf
 
 import Decidable.Equality
 

src/Core/Coverage.idr

@@ -15,6 +15,7 @@ import Data.String
 
 import Libraries.Data.NameMap
 import Libraries.Data.String.Extra
+import Libraries.Data.SnocList.SizeOf
 import Libraries.Text.PrettyPrint.Prettyprinter
 
 %default covering
@@ -77,7 +78,7 @@ conflict defs env nfty n
               | Nothing => pure False
          case (definition gdef, type gdef) of
               (DCon t arity _, dty)
-                  => do Nothing <- conflictNF 0 nfty !(nf defs [] dty)
+                  => do Nothing <- conflictNF 0 nfty !(nf defs [<] dty)
                             | Just ms => pure $ conflictMatch ms
                         pure True
               _ => pure False
@@ -110,7 +111,7 @@ conflict defs env nfty n
           -- put posslbe
           = let x' = MN (show x) i in
                 conflictNF (i + 1) t
-                       !(sc defs (toClosure defaultOpts [] (Ref fc Bound x')))
+                       !(sc defs (toClosure defaultOpts [<] (Ref fc Bound x')))
       conflictNF i nf (NApp _ (NRef Bound n) [<])
           = do empty <- clearDefs defs
                pure (Just [(n, !(quote empty env nf))])
@@ -455,7 +456,7 @@ checkMatched cs ulhs
   where
     tryClauses : List Clause -> ClosedTerm -> Core (Maybe ClosedTerm)
     tryClauses [] ulhs
-        = do logTermNF "coverage" 10 "Nothing matches" [] ulhs
+        = do logTermNF "coverage" 10 "Nothing matches" [<] ulhs
              pure $ Just ulhs
     tryClauses (MkClause env lhs _ :: cs) ulhs
         = if !(clauseMatches env lhs ulhs)

src/Core/GetType.idr

@@ -33,7 +33,7 @@ mutual
            chkMeta fc env !(nf defs env (embed mty)) args
   chk env (Bind fc nm b sc)
       = do bt <- chkBinder env b
-           sct <- chk {vars = _ :< nm} (b :: env) sc
+           sct <- chk {vars = _ :< nm} (env :< b) sc
            pure $ gnf env (discharge fc nm b !(getTerm bt) !(getTerm sct))
   chk env (App fc f a)
       = do fty <- chk env f

src/Core/LinearCheck.idr

@@ -12,6 +12,7 @@ import Core.Value
 import Core.TT
 
 import Data.List
+import Data.SnocList
 
 import Libraries.Data.SnocList.SizeOf
 
@@ -20,29 +21,29 @@ import Libraries.Data.SnocList.SizeOf
 -- List of variable usages - we'll count the contents of specific variables
 -- when discharging binders, to ensure that linear names are only used once
 data Usage : SnocList Name -> Type where
-     Nil : Usage vars
-     (::) : Var vars -> Usage vars -> Usage vars
+     Lin : Usage vars
+     (:<) : Usage vars -> Var vars -> Usage vars
 
 Show (Usage vars) where
   show xs = "[" ++ showAll xs ++ "]"
     where
       showAll : Usage vs -> String
-      showAll [] = ""
-      showAll [el] = show el
-      showAll (x :: xs) = show x ++ ", " ++ show xs
+      showAll [<] = ""
+      showAll [<el] = show el
+      showAll (xs :< x) = show x ++ ", " ++ show xs
 
 doneScope : Usage (vars :< n) -> Usage vars
-doneScope [] = []
-doneScope (MkVar First :: xs) = doneScope xs
-doneScope (MkVar (Later p) :: xs) = MkVar p :: doneScope xs
+doneScope [<] = [<]
+doneScope (xs :< MkVar First) = doneScope xs
+doneScope (xs :< MkVar (Later p)) = doneScope xs :< MkVar p
 
 (++) : Usage ns -> Usage ns -> Usage ns
-(++) [] ys = ys
-(++) (x :: xs) ys = x :: xs ++ ys
+(++) sx Lin = sx
+(++) sx (sy :< y) = (sx ++ sy) :< y
 
 count : Nat -> Usage ns -> Nat
-count p [] = 0
-count p (v :: xs)
+count p [<] = 0
+count p (xs :< v)
     = if p == varIdx v then 1 + count p xs else count p xs
 
 mutual
@@ -196,12 +197,12 @@ mutual
       -- count the usage if we're in a linear context. If not, the usage doesn't
       -- matter
       used : RigCount -> Usage vars
-      used r = if isLinear r then [MkVar prf] else []
+      used r = if isLinear r then [<MkVar prf] else [<]
 
   lcheck rig erase env (Ref fc nt fn)
       = do logC "quantity" 15 $ do pure "lcheck Ref \{show (nt)} \{show !(toFullNames fn)}"
            ty <- lcheckDef fc rig erase env fn
-           pure (Ref fc nt fn, gnf env (embed ty), [])
+           pure (Ref fc nt fn, gnf env (embed ty), [<])
 
   -- If the meta has a definition, and we're not in Rig0, expand it first
   -- and check the result.
@@ -261,7 +262,7 @@ mutual
                               (Lam _ _ _ _) => eraseLinear env
                               _ => env
                          else env
-           (sc', sct, usedsc) <- lcheck rig erase (b' :: env') sc
+           (sc', sct, usedsc) <- lcheck rig erase (env' :< b') sc
 
            let used_in = count 0 usedsc
            holeFound <- if not erase && isLinear (multiplicity b)
@@ -295,18 +296,18 @@ mutual
                          else linear
 
       getZeroes : {vs : _} -> Env Term vs -> List (Var vs)
-      getZeroes [] = []
-      getZeroes (b :: bs)
+      getZeroes [<] = []
+      getZeroes (bs :< b)
           = if isErased (multiplicity b)
                then MkVar First :: map weaken (getZeroes bs)
                else map weaken (getZeroes bs)
 
       eraseLinear : Env Term vs -> Env Term vs
-      eraseLinear [] = []
-      eraseLinear (b :: bs)
+      eraseLinear [<] = [<]
+      eraseLinear (bs :< b)
           = if isLinear (multiplicity b)
-               then setMultiplicity b erased :: eraseLinear bs
-               else b :: eraseLinear bs
+               then eraseLinear bs :< setMultiplicity b erased
+               else eraseLinear bs :< b
 
       checkUsageOK : Nat -> RigCount -> Core ()
       checkUsageOK used r = when (isLinear r && used /= 1)
@@ -351,7 +352,7 @@ mutual
                   do when (not erase) $ needFunctionType f' gfty
                      -- we don't do any linearity checking when `erase` is set
                      -- so returning an empty usage is fine
-                     pure (App fc f a, gErased fc, [])
+                     pure (App fc f a, gErased fc, [<])
                 _ =>
                   needFunctionType f' gfty
     where
@@ -386,14 +387,14 @@ mutual
                 _ => throw (GenericMsg fc "Not a delayed type")
   lcheck rig erase env (PrimVal fc c)
       = do log "quantity" 15 "lcheck PrimVal"
-           pure (PrimVal fc c, gErased fc, [])
+           pure (PrimVal fc c, gErased fc, [<])
   lcheck rig erase env (Erased fc i)
       = do log "quantity" 15 "lcheck Erased"
-           pure (Erased fc i, gErased fc, [])
+           pure (Erased fc i, gErased fc, [<])
   lcheck rig erase env (TType fc u)
       -- Not universe checking here, just use the top of the hierarchy
       = do log "quantity" 15 "lcheck TType"
-           pure (TType fc u, gType fc (MN "top" 0), [])
+           pure (TType fc u, gType fc (MN "top" 0), [<])
 
   lcheckBinder : {vars : _} ->
                  {auto c : Ref Ctxt Defs} ->
@@ -403,24 +404,24 @@ mutual
                  Core (Binder (Term vars), Glued vars, Usage vars)
   lcheckBinder rig erase env (Lam fc c x ty)
       = do (tyv, tyt, _) <- lcheck erased erase env ty
-           pure (Lam fc c x tyv, tyt, [])
+           pure (Lam fc c x tyv, tyt, [<])
   lcheckBinder rig erase env (Let fc rigc val ty)
       = do (tyv, tyt, _) <- lcheck erased erase env ty
            (valv, valt, vs) <- lcheck (rig |*| rigc) erase env val
            pure (Let fc rigc valv tyv, tyt, vs)
   lcheckBinder rig erase env (Pi fc c x ty)
       = do (tyv, tyt, _) <- lcheck (rig |*| c) erase env ty
-           pure (Pi fc c x tyv, tyt, [])
+           pure (Pi fc c x tyv, tyt, [<])
   lcheckBinder rig erase env (PVar fc c p ty)
       = do (tyv, tyt, _) <- lcheck erased erase env ty
-           pure (PVar fc c p tyv, tyt, [])
+           pure (PVar fc c p tyv, tyt, [<])
   lcheckBinder rig erase env (PLet fc rigc val ty)
       = do (tyv, tyt, _) <- lcheck erased erase env ty
            (valv, valt, vs) <- lcheck (rig |*| rigc) erase env val
            pure (PLet fc rigc valv tyv, tyt, vs)
   lcheckBinder rig erase env (PVTy fc c ty)
       = do (tyv, tyt, _) <- lcheck erased erase env ty
-           pure (PVTy fc c tyv, tyt, [])
+           pure (PVTy fc c tyv, tyt, [<])
 
   discharge : {vars : _} ->
               Defs -> Env Term vars ->
@@ -525,12 +526,12 @@ mutual
       checkEnvUsage : {vars : _} ->
                       SizeOf done ->
                       RigCount ->
-                      Env Term vars -> Usage (done <>> vars) ->
-                      List (Term (done <>> vars)) ->
-                      Term (done <>> vars) -> Core ()
-      checkEnvUsage s rig [] usage args tm = pure ()
-      checkEnvUsage s rig {done} {vars = xs :< nm} (b :: env) usage args tm
-          = do let pos = mkVarChiply s
+                      Env Term vars -> Usage (vars ++ done) ->
+                      List (Term (vars ++ done)) ->
+                      Term (vars ++ done) -> Core ()
+      checkEnvUsage s rig [<] usage args tm = pure ()
+      checkEnvUsage s rig {done} {vars = xs :< nm} (env :< b) usage args tm
+          = do let pos = mkVar s
                let used_in = count (varIdx pos) usage
 
                holeFound <- if isLinear (multiplicity b)
@@ -543,7 +544,10 @@ mutual
                checkUsageOK (getLoc (binderType b))
                             used nm (isLocArg pos args)
                                     ((multiplicity b) |*| rig)
-               checkEnvUsage (s :< nm) rig env usage args tm
+               checkEnvUsage ([<nm] + s) rig env
+                    (rewrite appendAssociative xs [<nm] done in usage)
+                    (rewrite appendAssociative xs [<nm] done in args)
+                    (rewrite appendAssociative xs [<nm] done in tm)
 
       getPUsage : ClosedTerm -> (vs ** (Env Term vs, Term vs, Term vs)) ->
                   Core (List (Name, ArgUsage))
@@ -646,15 +650,15 @@ mutual
                Name -> Int -> Def -> List (Term vars) ->
                Core (Term vars, Glued vars, Usage vars)
   expandMeta rig erase env n idx (PMDef _ [<] (STerm _ fn) _ _) args
-      = do tm <- substMeta (embed fn) args zero []
+      = do tm <- substMeta (embed fn) args zero [<]
            lcheck rig erase env tm
     where
       substMeta : {drop, vs : _} ->
                   Term (vs ++ drop) -> List (Term vs) ->
                   SizeOf drop -> SubstEnv drop vs ->
                   Core (Term vs)
       substMeta (Bind bfc n (Lam _ c e ty) sc) (a :: as) drop env
-          = substMeta sc as (suc drop) (a :: env)
+          = substMeta sc as (suc drop) (env :< a)
       substMeta (Bind bfc n (Let _ c val ty) sc) as drop env
           = substMeta (subst val sc) as drop env
       substMeta rhs [] drop env = pure (substs drop env rhs)
@@ -691,19 +695,19 @@ mutual
                       ++ " not a function type)"))
   lcheckMeta rig erase env fc n idx [] chk nty
       = do defs <- get Ctxt
-           pure (Meta fc n idx (reverse chk), glueBack defs env nty, [])
+           pure (Meta fc n idx (reverse chk), glueBack defs env nty, [<])
 
 
 checkEnvUsage : {vars : _} ->
                 {auto c : Ref Ctxt Defs} ->
                 {auto u : Ref UST UState} ->
                 FC -> SizeOf done -> RigCount ->
-                Env Term vars -> Usage (done <>> vars) ->
-                Term (done <>> vars) ->
+                Env Term vars -> Usage (vars ++ done) ->
+                Term (vars ++ done) ->
                 Core ()
-checkEnvUsage fc s rig [] usage tm = pure ()
-checkEnvUsage fc s rig {vars = xs :< nm} (b :: env) usage tm
-    = do let pos = mkVarChiply s
+checkEnvUsage fc s rig [<] usage tm = pure ()
+checkEnvUsage fc s rig {vars = xs :< nm} (env :< b) usage tm
+    = do let pos = mkVar s
          let used_in = count (varIdx pos) usage
 
          holeFound <- if isLinear (multiplicity b)
@@ -714,7 +718,10 @@ checkEnvUsage fc s rig {vars = xs :< nm} (b :: env) usage tm
                        then 1
                        else used_in
          checkUsageOK used ((multiplicity b) |*| rig)
-         checkEnvUsage fc (s :< nm) rig env usage tm
+         checkEnvUsage fc ([<nm] + s) rig env
+            (rewrite appendAssociative xs [<nm] done in usage)
+            (rewrite appendAssociative xs [<nm] done in tm)
+
   where
     checkUsageOK : Nat -> RigCount -> Core ()
     checkUsageOK used r = when (isLinear r && used /= 1)

src/Core/Metadata.idr

@@ -205,9 +205,9 @@ addLHS loc outerenvlen env tm
 
   where
     toPat : Env Term vs -> Env Term vs
-    toPat (Lam fc c p ty :: bs) = PVar fc c p ty :: toPat bs
-    toPat (b :: bs) = b :: toPat bs
-    toPat [] = []
+    toPat (bs :< Lam fc c p ty) = toPat bs :< PVar fc c p ty
+    toPat (bs :< b) = toPat bs :< b
+    toPat [<] = [<]
 
 -- For giving local variable names types, just substitute the name
 -- rather than storing the whole environment, otherwise we'll repeatedly
@@ -219,8 +219,8 @@ addLHS loc outerenvlen env tm
 -- types directly!
 substEnv : {vars : _} ->
            FC -> Env Term vars -> (tm : Term vars) -> ClosedTerm
-substEnv loc [] tm = tm
-substEnv {vars = _ :< x} loc (b :: env) tm
+substEnv loc [<] tm = tm
+substEnv {vars = _ :< x} loc (env :< b) tm
     = substEnv loc env (subst (Ref loc Bound x) tm)
 
 export
@@ -357,7 +357,7 @@ normaliseTypes
     nfType : Defs -> (NonEmptyFC, (Name, Nat, ClosedTerm)) ->
              Core (NonEmptyFC, (Name, Nat, ClosedTerm))
     nfType defs (loc, (n, len, ty))
-       = pure (loc, (n, len, !(normaliseArgHoles defs [] ty)))
+       = pure (loc, (n, len, !(normaliseArgHoles defs [<] ty)))
 
 record TTMFile where
   constructor MkTTMFile

src/Core/Termination/CallGraph.idr

@@ -5,6 +5,7 @@ import Core.Context.Log
 import Core.Env
 import Core.Normalise
 import Core.Value
+import Core.Name.CompatibleVars
 
 import Libraries.Data.SparseMatrix
 
@@ -76,7 +77,7 @@ mutual
   findSC {vars} defs env g pats (Bind fc n b sc)
        = pure $
             !(findSCbinder b) ++
-            !(findSC defs (b :: env) g (map weaken pats) sc)
+            !(findSC defs (env :< b) g (map weaken pats) sc)
     where
       findSCbinder : Binder (Term vars) -> Core (List SCCall)
       findSCbinder (Let _ c val ty) = findSC defs env g pats val