[ refactor ] split Core.TT (#3151)

idris2api.ipkg

@@ -73,6 +73,7 @@ modules =
     Core.Metadata,
     Core.Name,
     Core.Name.Namespace,
+    Core.Name.Scoped,
     Core.Normalise,
     Core.Normalise.Convert,
     Core.Normalise.Eval,
@@ -90,8 +91,14 @@ modules =
     Core.Termination,
     Core.Transform,
     Core.TT,
-    Core.TT.Views,
+    Core.TT.Binder,
+    Core.TT.Primitive,
+    Core.TT.Subst,
+    Core.TT.Term,
+    Core.TT.Term.Subst,
     Core.TT.Traversals,
+    Core.TT.Var,
+    Core.TT.Views,
     Core.TTC,
     Core.Unify,
     Core.UnifyState,
@@ -164,21 +171,28 @@ modules =
 
     Libraries.Data.ANameMap,
     Libraries.Data.DList,
+    Libraries.Data.Erased,
     Libraries.Data.Fin,
     Libraries.Data.Graph,
     Libraries.Data.IMaybe,
     Libraries.Data.IntMap,
     Libraries.Data.IOArray,
     Libraries.Data.IOMatrix,
-    Libraries.Data.LengthMatch,
     Libraries.Data.List.Extra,
-    Libraries.Data.List.Quantifiers.Extra,
+    Libraries.Data.List.HasLength,
     Libraries.Data.List.Lazy,
+    Libraries.Data.List.LengthMatch,
+    Libraries.Data.List.Quantifiers.Extra,
+    Libraries.Data.List.SizeOf,
     Libraries.Data.List1,
     Libraries.Data.NameMap,
     Libraries.Data.NameMap.Traversable,
+    Libraries.Data.Ordering.Extra,
     Libraries.Data.PosMap,
     Libraries.Data.Primitives,
+    Libraries.Data.SnocList.HasLength,
+    Libraries.Data.SnocList.LengthMatch,
+    Libraries.Data.SnocList.SizeOf,
     Libraries.Data.Span,
     Libraries.Data.SortedMap,
     Libraries.Data.SortedSet,

libs/base/System/Concurrency.idr

@@ -215,4 +215,3 @@ channelGet chan = primIO (prim__channelGet chan)
 export
 channelPut : HasIO io => (chan : Channel a) -> (val : a) -> io ()
 channelPut chan val = primIO (prim__channelPut chan val)
-

src/Compiler/CaseOpts.idr

@@ -37,23 +37,22 @@ shiftUnder : {args : _} ->
 shiftUnder First = weakenNVar (mkSizeOf args) (MkNVar First)
 shiftUnder (Later p) = insertNVar (mkSizeOf args) (MkNVar p)
 
-shiftVar : {outer, args : _} ->
-           {idx : _} ->
-           (0 p : IsVar n idx (outer ++ (x :: args ++ vars))) ->
+shiftVar : {outer, args : Scope} ->
+           NVar n (outer ++ (x :: args ++ vars)) ->
            NVar n (outer ++ (args ++ x :: vars))
-shiftVar {outer = []} p = shiftUnder p
-shiftVar {outer = (n::xs)} First = MkNVar First
-shiftVar {outer = (y::xs)} (Later p)
-    = case shiftVar p of
-           MkNVar p' => MkNVar (Later p')
+shiftVar nvar
+  = let out = mkSizeOf outer in
+    case locateNVar out nvar of
+      Left nvar => embed nvar
+      Right (MkNVar p) => weakenNs out (shiftUnder p)
 
 mutual
   shiftBinder : {outer, args : _} ->
                 (new : Name) ->
                 CExp (outer ++ old :: (args ++ vars)) ->
                 CExp (outer ++ (args ++ new :: vars))
   shiftBinder new (CLocal fc p)
-      = case shiftVar p of
+      = case shiftVar (MkNVar p) of
              MkNVar p' => CLocal fc (renameVar p')
     where
       renameVar : IsVar x i (outer ++ (args ++ (old :: rest))) ->

src/Compiler/CompileExpr.idr

@@ -39,14 +39,14 @@ numArgs defs (Ref _ _ n)
            _ => pure (Arity 0)
 numArgs _ tm = pure (Arity 0)
 
-mkSub : Nat -> (ns : List Name) -> List Nat -> (ns' ** SubVars ns' ns)
-mkSub i _ [] = (_ ** SubRefl)
-mkSub i [] ns = (_ ** SubRefl)
+mkSub : Nat -> (ns : List Name) -> List Nat -> (ns' ** Thin ns' ns)
+mkSub i _ [] = (_ ** Refl)
+mkSub i [] ns = (_ ** Refl)
 mkSub i (x :: xs) es
     = let (ns' ** p) = mkSub (S i) xs es in
           if i `elem` es
-             then (ns' ** DropCons p)
-             else (x :: ns' ** KeepCons p)
+             then (ns' ** Drop p)
+             else (x :: ns' ** Keep p)
 
 weakenVar : Var ns -> Var (a :: ns)
 weakenVar (MkVar p) = (MkVar (Later p))
@@ -134,13 +134,13 @@ eraseConArgs arity epos fn args
 mkDropSubst : Nat -> List Nat ->
               (rest : List Name) ->
               (vars : List Name) ->
-              (vars' ** SubVars (vars' ++ rest) (vars ++ rest))
-mkDropSubst i es rest [] = ([] ** SubRefl)
+              (vars' ** Thin (vars' ++ rest) (vars ++ rest))
+mkDropSubst i es rest [] = ([] ** Refl)
 mkDropSubst i es rest (x :: xs)
     = let (vs ** sub) = mkDropSubst (1 + i) es rest xs in
           if i `elem` es
-             then (vs ** DropCons sub)
-             else (x :: vs ** KeepCons sub)
+             then (vs ** Drop sub)
+             else (x :: vs ** Keep sub)
 
 -- Rewrite applications of Nat-like constructors and functions to more optimal
 -- versions using Integer
@@ -338,7 +338,7 @@ toCExpTm n (Bind fc x (Lam _ _ _ _) sc)
     = pure $ CLam fc x !(toCExp n sc)
 toCExpTm n (Bind fc x (Let _ rig val _) sc)
     = do sc' <- toCExp n sc
-         pure $ branchZero (shrinkCExp (DropCons SubRefl) sc')
+         pure $ branchZero (shrinkCExp (Drop Refl) sc')
                         (CLet fc x YesInline !(toCExp n val) sc')
                         rig
 toCExpTm n (Bind fc x (Pi _ c e ty) sc)
@@ -454,31 +454,32 @@ mutual
                      if noworld -- just substitute the scrutinee into
                                 -- the RHS
                         then
-                             let env : SubstCEnv args vars
+                             let (s, env) : (SizeOf args, SubstCEnv args vars)
                                      = mkSubst 0 scr pos args in
                               do log "compiler.newtype.world" 50 "Inlining case on \{show n} (no world)"
-                                 pure $ Just (substs env !(toCExpTree n sc))
+                                 pure $ Just (substs s env !(toCExpTree n sc))
                         else -- let bind the scrutinee, and substitute the
                              -- name into the RHS
-                             let env : SubstCEnv args (MN "eff" 0 :: vars)
+                             let (s, env) : (_, SubstCEnv args (MN "eff" 0 :: vars))
                                      = mkSubst 0 (CLocal fc First) pos args in
                              do sc' <- toCExpTree n sc
                                 let scope = insertNames {outer=args}
                                                         {inner=vars}
                                                         {ns = [MN "eff" 0]}
                                                         (mkSizeOf _) (mkSizeOf _) sc'
-                                let tm = CLet fc (MN "eff" 0) NotInline scr (substs env scope)
+                                let tm = CLet fc (MN "eff" 0) NotInline scr (substs s env scope)
                                 log "compiler.newtype.world" 50 "Kept the scrutinee \{show tm}"
                                 pure (Just tm)
                 _ => pure Nothing -- there's a normal match to do
     where
       mkSubst : Nat -> CExp vs ->
-                Nat -> (args : List Name) -> SubstCEnv args vs
-      mkSubst _ _ _ [] = Nil
+                Nat -> (args : List Name) -> (SizeOf args, SubstCEnv args vs)
+      mkSubst _ _ _ [] = (zero, [])
       mkSubst i scr pos (a :: as)
-          = if i == pos
-               then scr :: mkSubst (1 + i) scr pos as
-               else CErased fc :: mkSubst (1 + i) scr pos as
+          = let (s, env) = mkSubst (1 + i) scr pos as in
+            if i == pos
+               then (suc s, scr :: env)
+               else (suc s, CErased fc :: env)
   getNewType fc scr n (_ :: ns) = getNewType fc scr n ns
 
   getDef : {vars : _} ->
@@ -678,10 +679,11 @@ getCFTypes args (NBind fc _ (Pi _ _ _ ty) sc)
 getCFTypes args t
     = pure (reverse args, !(nfToCFType (getLoc t) False t))
 
-lamRHSenv : Int -> FC -> (ns : List Name) -> SubstCEnv ns []
-lamRHSenv i fc [] = []
+lamRHSenv : Int -> FC -> (ns : List Name) -> (SizeOf ns, SubstCEnv ns [])
+lamRHSenv i fc [] = (zero, [])
 lamRHSenv i fc (n :: ns)
-    = CRef fc (MN "x" i) :: lamRHSenv (i + 1) fc ns
+    = let (s, env) = lamRHSenv (i + 1) fc ns in
+      (suc s, CRef fc (MN "x" i) :: env)
 
 mkBounds : (xs : _) -> Bounds xs
 mkBounds [] = None
@@ -699,8 +701,8 @@ getNewArgs {done = x :: xs} (_ :: sub) = x :: getNewArgs sub
 -- function, they had arity 0.
 lamRHS : (ns : List Name) -> CExp ns -> CExp []
 lamRHS ns tm
-    = let env = lamRHSenv 0 (getFC tm) ns
-          tmExp = substs env (rewrite appendNilRightNeutral ns in tm)
+    = let (s, env) = lamRHSenv 0 (getFC tm) ns
+          tmExp = substs s env (rewrite appendNilRightNeutral ns in tm)
           newArgs = reverse $ getNewArgs env
           bounds = mkBounds newArgs
           expLocs = mkLocals zero {vars = []} bounds tmExp in

src/Compiler/Inline.idr

@@ -17,7 +17,7 @@ import Core.TT
 import Data.Maybe
 import Data.List
 import Data.Vect
-import Libraries.Data.LengthMatch
+import Libraries.Data.List.LengthMatch
 import Libraries.Data.NameMap
 import Libraries.Data.WithDefault
 
@@ -139,7 +139,7 @@ mutual
                | Nothing => pure Nothing
            res <- eval rec env' stk'
                      (rewrite sym (appendAssociative args vars free) in
-                              embed {vars = vars ++ free} exp)
+                              embed {outer = vars ++ free} exp)
            pure (Just res)
   tryApply rec stk env _ = pure Nothing
 
@@ -414,12 +414,12 @@ fixArity (MkError exp) = pure $ MkError !(fixArityTm exp [])
 fixArity d = pure d
 
 -- TODO: get rid of this `done` by making the return `args'` runtime irrelevant?
-getLams : {done : _} ->
+getLams : {done : _} -> SizeOf done ->
           Int -> SubstCEnv done args -> CExp (done ++ args) ->
-          (args' ** (SubstCEnv args' args, CExp (args' ++ args)))
-getLams {done} i env (CLam fc x sc)
-    = getLams {done = x :: done} (i + 1) (CRef fc (MN "ext" i) :: env) sc
-getLams {done} i env sc = (done ** (env, sc))
+          (args' ** (SizeOf args', SubstCEnv args' args, CExp (args' ++ args)))
+getLams {done} d i env (CLam fc x sc)
+    = getLams {done = x :: done} (suc d) (i + 1) (CRef fc (MN "ext" i) :: env) sc
+getLams {done} d i env sc = (done ** (d, env, sc))
 
 mkBounds : (xs : _) -> Bounds xs
 mkBounds [] = None
@@ -437,8 +437,8 @@ getNewArgs {done = x :: xs} (_ :: sub) = x :: getNewArgs sub
 -- not the highest, as you'd expect if they were all lambdas).
 mergeLambdas : (args : List Name) -> CExp args -> (args' ** CExp args')
 mergeLambdas args (CLam fc x sc)
-    = let (args' ** (env, exp')) = getLams 0 [] (CLam fc x sc)
-          expNs = substs env exp'
+    = 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

src/Compiler/LambdaLift.idr

@@ -31,7 +31,7 @@ mutual
   ||| @ vars is the list of names accessible within the current scope of the
   |||   lambda-lifted code.
   public export
-  data Lifted : (vars : List Name) -> Type where
+  data Lifted : Scoped where
 
        ||| A local variable in the lambda-lifted syntax tree.
        |||
@@ -424,6 +424,7 @@ mutual
            update Lifts { defs $= ((n, MkLFun (dropped vars unused) bound scl') ::) }
            pure $ LUnderApp fc n (length bound) (allVars fc vars unused)
     where
+
         allPrfs : (vs : List Name) -> (unused : Vect (length vs) Bool) -> List (Var vs)
         allPrfs [] _ = []
         allPrfs (v :: vs) (False::uvs) = MkVar First :: map weaken (allPrfs vs uvs)

src/Compiler/Opts/ConstantFold.idr

@@ -50,7 +50,8 @@ record WkCExp (vars : List Name) where
   expr : CExp supp
 
 Weaken WkCExp where
-  weaken (MkWkCExp s Refl e) = MkWkCExp (suc s) Refl e
+  weakenNs s' (MkWkCExp {outer, supp} s Refl e)
+    = MkWkCExp (s' + s) (appendAssociative ns outer supp)  e
 
 lookup : FC -> Var ds -> Subst ds vars -> CExp vars
 lookup fc (MkVar p) rho = case go p rho of

src/Compiler/Opts/Identity.idr

@@ -17,8 +17,8 @@ parameters (fn1 : Name) (idIdx : Nat)
   mutual
     -- special case for matching on 'Nat'-shaped things
     isUnsucc : Var vars -> CExp vars -> Maybe (Constant, Var (x :: vars))
-    isUnsucc (MkVar {i} _) (COp _ (Sub _) [CLocal {idx} _ _, CPrimVal _ c]) =
-        if i == idx
+    isUnsucc var (COp _ (Sub _) [CLocal _ p, CPrimVal _ c]) =
+        if var == MkVar p
             then Just (c, MkVar First)
             else Nothing
     isUnsucc _ _ = Nothing
@@ -29,7 +29,7 @@ parameters (fn1 : Name) (idIdx : Nat)
 
     -- does the CExp evaluate to the var, the constructor or the constant?
     cexpIdentity : Var vars -> Maybe (Name, List (Var vars)) -> Maybe Constant -> CExp vars -> Bool
-    cexpIdentity (MkVar {i} _) _ _ (CLocal {idx} fc p) = idx == i
+    cexpIdentity var _ _ (CLocal fc p) = var == MkVar p
     cexpIdentity var _ _ (CRef _ _) = False
     cexpIdentity var _ _ (CLam _ _ _) = False
     cexpIdentity var con const (CLet _ _ NotInline val sc) = False

src/Core/AutoSearch.idr

@@ -186,7 +186,7 @@ getUsableEnv fc rigc p [] = []
 getUsableEnv {vars = v :: vs} {done} fc rigc p (b :: env)
    = let rest = getUsableEnv fc rigc (sucR p) env in
          if (multiplicity b == top || isErased rigc)
-            then let MkVar var = weakenVar p (MkVar First) in
+            then let 0 var = mkIsVar (hasLength p) in
                      (Local (binderLoc b) Nothing _ var,
                        rewrite appendAssociative done [v] vs in
                           weakenNs (sucR p) (binderType b)) ::

src/Core/Case/CaseBuilder.idr

@@ -16,7 +16,7 @@ import Idris.Pretty.Annotations
 import Data.List
 import Data.String
 import Data.Vect
-import Libraries.Data.LengthMatch
+import Libraries.Data.List.LengthMatch
 import Libraries.Data.SortedSet
 
 import Decidable.Equality
@@ -176,7 +176,7 @@ getPat (Later p) (x :: xs) = getPat p xs
 
 dropPat : {idx : Nat} ->
           (0 el : IsVar nm idx ps) ->
-          NamedPats ns ps -> NamedPats ns (dropVar ps el)
+          NamedPats ns ps -> NamedPats ns (dropIsVar ps el)
 dropPat First (x :: xs) = xs
 dropPat (Later p) (x :: xs) = x :: dropPat p xs
 
@@ -218,7 +218,7 @@ Weaken ArgType where
   weakenNs s Unknown = Unknown
 
 Weaken (PatInfo p) where
-  weaken (MkInfo p el fty) = MkInfo p (Later el) (weaken fty)
+  weakenNs s (MkInfo p el fty) = MkInfo p (weakenIsVar s el) (weakenNs s fty)
 
 -- FIXME: perhaps 'vars' should be second argument so we can use Weaken interface
 weaken : {x, vars : _} ->
@@ -941,11 +941,11 @@ pickNextViable {ps = q :: qs} fc phase fn npss
                             pure (_ ** MkNVar (Later var))
 
 moveFirst : {idx : Nat} -> (0 el : IsVar nm idx ps) -> NamedPats ns ps ->
-            NamedPats ns (nm :: dropVar ps el)
+            NamedPats ns (nm :: dropIsVar ps el)
 moveFirst el nps = getPat el nps :: dropPat el nps
 
 shuffleVars : {idx : Nat} -> (0 el : IsVar nm idx todo) -> PatClause vars todo ->
-              PatClause vars (nm :: dropVar todo el)
+              PatClause vars (nm :: dropIsVar todo el)
 shuffleVars First orig@(MkPatClause pvars lhs pid rhs) = orig -- no-op
 shuffleVars el (MkPatClause pvars lhs pid rhs)
     = MkPatClause pvars (moveFirst el lhs) pid rhs
@@ -1165,11 +1165,11 @@ mkPatClause fc fn args ty pid (ps, rhs)
                      Nothing => pure (Nothing, CaseBuilder.Unknown)
                      Just (NBind pfc _ (Pi _ c _ farg) fsc) =>
                         pure (Just !(fsc defs (toClosure defaultOpts [] (Ref pfc Bound arg))),
-                                Known c (embed {more = arg :: args}
+                                Known c (embed {outer = arg :: args}
                                           !(quote empty [] farg)))
                      Just t =>
                         pure (Nothing,
-                                Stuck (embed {more = arg :: args}
+                                Stuck (embed {outer = arg :: args}
                                         !(quote empty [] t)))
              pure (MkInfo p First (Builtin.snd fa_tys)
                       :: weaken !(mkNames args ps eq (Builtin.fst fa_tys)))
@@ -1197,7 +1197,7 @@ patCompile fc fn phase ty (p :: ps) def
          i <- newRef PName (the Int 0)
          cases <- match fc fn phase pats
                         (rewrite sym (appendNilRightNeutral ns) in
-                                 map (TT.weakenNs n) def)
+                                 map (weakenNs n) def)
          pure (_ ** cases)
   where
     mkPatClausesFrom : Int -> (args : List Name) ->
@@ -1375,17 +1375,6 @@ getPMDef fc phase fn ty clauses
     labelPat i [] = []
     labelPat i (x :: xs) = ("pat" ++ show i ++ ":", x) :: labelPat (i + 1) xs
 
-    mkSubstEnv : Int -> String -> Env Term vars -> SubstEnv vars []
-    mkSubstEnv i pname [] = Nil
-    mkSubstEnv i pname (v :: vs)
-       = Ref fc Bound (MN pname i) :: mkSubstEnv (i + 1) pname vs
-
-    close : {vars : _} ->
-            Env Term vars -> String -> Term vars -> ClosedTerm
-    close {vars} env pname tm
-        = substs (mkSubstEnv 0 pname env)
-              (rewrite appendNilRightNeutral vars in tm)
-
     toClosed : Defs -> (String, Clause) -> (ClosedTerm, ClosedTerm)
     toClosed defs (pname, MkClause env lhs rhs)
-          = (close env pname lhs, close env pname rhs)
+          = (close fc pname env lhs, close fc pname env rhs)