[ refactor ] ScopedSnocList: Preparing for the long jump (Phase 1)

Core idea is to split the process of transition from List-based Context on SnocList-based Context on 2 phases:

1. Apply a refactor which does not make any transition (even no observable changes for Idris users) actually but prepare the code for future update.
2. Roll out the transition with limited code changes invasion because it was partially done at the step before.

Co-authored-by: Viktor Yudov <[email protected]>

Author: GulinSS

idris2api.ipkg

@@ -73,6 +73,7 @@ modules =
     Core.LinearCheck,
     Core.Metadata,
     Core.Name,
+    Core.Name.CompatibleVars,
     Core.Name.Namespace,
     Core.Name.Scoped,
     Core.Normalise,
@@ -191,6 +192,7 @@ modules =
     Libraries.Data.NameMap.Traversable,
     Libraries.Data.Ordering.Extra,
     Libraries.Data.PosMap,
+    Libraries.Data.SnocList.Extra,
     Libraries.Data.SnocList.HasLength,
     Libraries.Data.SnocList.LengthMatch,
     Libraries.Data.SnocList.SizeOf,

libs/base/Data/SnocList.idr

@@ -471,3 +471,13 @@ tailRecAppendIsAppend : (sx, sy : SnocList a) -> tailRecAppend sx sy = sx ++ sy
 tailRecAppendIsAppend sx Lin = Refl
 tailRecAppendIsAppend sx (sy :< y) =
   trans (snocTailRecAppend y sx sy) (cong (:< y) $ tailRecAppendIsAppend sx sy)
+
+||| `reverseOnto` reverses the snoc list and prepends it to the "onto" argument
+export
+revOnto : (xs, vs : SnocList a) -> reverseOnto xs vs = xs ++ reverse vs
+revOnto _ [<] = Refl
+revOnto xs (vs :< v) =
+  do rewrite revOnto (xs :< v) vs
+     rewrite sym $ appendAssociative xs [<v] (reverse vs)
+     rewrite revOnto [<v] vs
+     Refl

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) ([<x] ++ sx)
-sucL Z     = S Z
-sucL (S n) = S (sucL n)
+sucR : HasLength n sx -> HasLength (S n) ([<x] ++ sx)
+sucR Z     = S Z
+sucR (S n) = S (sucR n)
 
 export
 hlAppend : HasLength m sx -> HasLength n sy -> HasLength (n + m) (sx ++ sy)

libs/base/Data/SnocList/Operations.idr

@@ -96,6 +96,17 @@ lengthHomomorphism sx (sy :< x) = Calc $
   ~~ 1 + (length sx + length sy) ...(cong (1+) $ lengthHomomorphism _ _)
   ~~ length sx + (1 + length sy) ...(plusSuccRightSucc _ _)
 
+export
+lengthDistributesOverFish : (sx : SnocList a) -> (ys : List a) ->
+                            length (sx <>< ys) === length sx + length ys
+lengthDistributesOverFish sx [] = sym $ plusZeroRightNeutral _
+lengthDistributesOverFish sx (y :: ys) = Calc $
+  |~ length ((sx :< y) <>< ys)
+  ~~ length (sx :< y) + length ys ...( lengthDistributesOverFish (sx :< y) ys)
+  ~~ S (length sx) + length ys    ...( Refl )
+  ~~ length sx + S (length ys)    ...( plusSuccRightSucc _ _ )
+  ~~ length sx + length (y :: ys) ...( Refl )
+
 -- cons-list operations on snoc-lists
 
 ||| Take `n` first elements from `sx`, returning the whole list if

src/Compiler/ANF.idr

@@ -8,8 +8,10 @@ import Core.Core
 import Core.TT
 
 import Data.List
+import Data.SnocList
 import Data.Vect
 import Libraries.Data.SortedSet
+import Libraries.Data.SnocList.Extra
 
 %default covering
 
@@ -136,10 +138,13 @@ Show ANFDef where
         show args ++ " -> " ++ show ret
   show (MkAError exp) = "Error: " ++ show exp
 
-data AVars : List Name -> Type where
-     Nil : AVars []
+data AVars : Scoped where
+     Nil : AVars ScopeEmpty
      (::) : Int -> AVars xs -> AVars (x :: xs)
 
+ScopeEmpty : AVars ScopeEmpty
+ScopeEmpty = []
+
 data Next : Type where
 
 nextVar : {auto v : Ref Next Int} ->
@@ -280,7 +285,7 @@ toANF (MkLCon t a ns) = pure $ MkACon t a ns
 toANF (MkLForeign ccs fargs t) = pure $ MkAForeign ccs fargs t
 toANF (MkLError err)
     = do v <- newRef Next (the Int 0)
-         pure $ MkAError !(anf [] err)
+         pure $ MkAError !(anf ScopeEmpty err)
 
 export
 freeVariables : ANF -> SortedSet AVar

src/Compiler/CaseOpts.idr

@@ -10,8 +10,13 @@ import Core.FC
 import Core.TT
 
 import Data.List
+import Data.SnocList
 import Data.Vect
 
+import Libraries.Data.List.SizeOf
+import Libraries.Data.SnocList.SizeOf
+import Libraries.Data.SnocList.Extra
+
 %default covering
 
 {-
@@ -37,7 +42,7 @@ shiftUnder : {args : _} ->
 shiftUnder First = weakenNVar (mkSizeOf args) (MkNVar First)
 shiftUnder (Later p) = insertNVar (mkSizeOf args) (MkNVar p)
 
-shiftVar : {outer, args : Scope} ->
+shiftVar : {outer : Scope} -> {args : List Name} ->
            NVar n (outer ++ (x :: args ++ vars)) ->
            NVar n (outer ++ (args ++ x :: vars))
 shiftVar nvar
@@ -108,7 +113,7 @@ liftOutLambda : {args : _} ->
                 (new : Name) ->
                 CExp (old :: args ++ vars) ->
                 CExp (args ++ new :: vars)
-liftOutLambda = shiftBinder {outer = []}
+liftOutLambda = shiftBinder {outer = ScopeEmpty}
 
 -- If all the alternatives start with a lambda, we can have a single lambda
 -- binding outside

src/Compiler/Common.idr

@@ -81,7 +81,7 @@ Ord UsePhase where
 public export
 record CompileData where
   constructor MkCompileData
-  mainExpr : CExp [] -- main expression to execute. This also appears in
+  mainExpr : ClosedCExp -- main expression to execute. This also appears in
                      -- the definitions below as MN "__mainExpression" 0
                      -- For incremental compilation and for compiling exported
                      -- names only, this can be set to 'erased'.
@@ -153,7 +153,7 @@ getMinimalDef (Coded ns bin)
          name <- fromBuf b
          let def
              = MkGlobalDef fc name (Erased fc Placeholder) [] [] [] [] mul
-                           [] (specified Public) (MkTotality Unchecked IsCovering) False
+                           ScopeEmpty (specified Public) (MkTotality Unchecked IsCovering) False
                            [] Nothing refsR False False True
                            None cdef Nothing [] Nothing
          pure (def, Just (ns, bin))
@@ -355,8 +355,8 @@ getCompileDataWith exports doLazyAnnots phase_in tm_in
                               traverse (lambdaLift doLazyAnnots) cseDefs
                          else pure []
 
-         let lifted = (mainname, MkLFun [] [] liftedtm) ::
-                      ldefs ++ concat lifted_in
+         let lifted = (mainname, MkLFun ScopeEmpty ScopeEmpty liftedtm) ::
+                      (ldefs ++ concat lifted_in)
 
          anf <- if phase >= ANF
                    then logTime 2 "Get ANF" $ traverse (\ (n, d) => pure (n, !(toANF d))) lifted
@@ -412,7 +412,7 @@ getCompileData = getCompileDataWith []
 
 export
 compileTerm : {auto c : Ref Ctxt Defs} ->
-              ClosedTerm -> Core (CExp [])
+              ClosedTerm -> Core ClosedCExp
 compileTerm tm_in
     = do tm <- toFullNames tm_in
          fixArityExp !(compileExp tm)

src/Compiler/CompileExpr.idr

@@ -13,9 +13,14 @@ import Core.TT
 import Core.Value
 
 import Data.List
+import Data.SnocList
 import Data.Maybe
 import Data.Vect
 
+import Libraries.Data.List.SizeOf
+import Libraries.Data.SnocList.SizeOf
+import Libraries.Data.SnocList.Extra
+
 %default covering
 
 data Args
@@ -40,7 +45,7 @@ numArgs defs (Ref _ _ n)
            _ => pure (Arity 0)
 numArgs _ tm = pure (Arity 0)
 
-mkSub : Nat -> (ns : List Name) -> List Nat -> (ns' ** Thin ns' ns)
+mkSub : Nat -> (ns : Scope) -> List Nat -> (ns' ** Thin ns' ns)
 mkSub i _ [] = (_ ** Refl)
 mkSub i [] ns = (_ ** Refl)
 mkSub i (x :: xs) es
@@ -319,7 +324,7 @@ mutual
     where
       mkSubst : Nat -> CExp vs ->
                 Nat -> (args : List Name) -> (SizeOf args, SubstCEnv args vs)
-      mkSubst _ _ _ [] = (zero, [])
+      mkSubst _ _ _ [] = (zero, ScopeEmpty)
       mkSubst i scr pos (a :: as)
           = let (s, env) = mkSubst (1 + i) scr pos as in
             if i == pos
@@ -386,8 +391,8 @@ mutual
 
 -- Need this for ensuring that argument list matches up to operator arity for
 -- builtins
-data ArgList : Nat -> List Name -> Type where
-     NoArgs : ArgList Z []
+data ArgList : Nat -> Scope -> Type where
+     NoArgs : ArgList Z ScopeEmpty
      ConsArg : (a : Name) -> ArgList k as -> ArgList (S k) (a :: as)
 
 mkArgList : Int -> (n : Nat) -> (ns ** ArgList n ns)
@@ -397,17 +402,17 @@ mkArgList i (S k)
           (_ ** ConsArg (MN "arg" i) rec)
 
 data NArgs : Type where
-     User : Name -> List (Closure []) -> NArgs
-     Struct : String -> List (String, Closure []) -> NArgs
+     User : Name -> List ClosedClosure -> NArgs
+     Struct : String -> List (String, ClosedClosure) -> NArgs
      NUnit : NArgs
      NPtr : NArgs
      NGCPtr : NArgs
      NBuffer : NArgs
      NForeignObj : NArgs
-     NIORes : Closure [] -> NArgs
+     NIORes : ClosedClosure -> NArgs
 
 getPArgs : {auto c : Ref Ctxt Defs} ->
-           Defs -> Closure [] -> Core (String, Closure [])
+           Defs -> ClosedClosure -> Core (String, ClosedClosure)
 getPArgs defs cl
     = do NDCon fc _ _ _ args <- evalClosure defs cl
              | nf => throw (GenericMsg (getLoc nf) "Badly formed struct type")
@@ -419,7 +424,7 @@ getPArgs defs cl
               _ => throw (GenericMsg fc "Badly formed struct type")
 
 getFieldArgs : {auto c : Ref Ctxt Defs} ->
-               Defs -> Closure [] -> Core (List (String, Closure []))
+               Defs -> ClosedClosure -> Core (List (String, ClosedClosure))
 getFieldArgs defs cl
     = do NDCon fc _ _ _ args <- evalClosure defs cl
              | nf => throw (GenericMsg (getLoc nf) "Badly formed struct type")
@@ -433,7 +438,7 @@ getFieldArgs defs cl
               _ => pure []
 
 getNArgs : {auto c : Ref Ctxt Defs} ->
-           Defs -> Name -> List (Closure []) -> Core NArgs
+           Defs -> Name -> List ClosedClosure -> Core NArgs
 getNArgs defs (NS _ (UN $ Basic "IORes")) [arg] = pure $ NIORes arg
 getNArgs defs (NS _ (UN $ Basic "Ptr")) [arg] = pure NPtr
 getNArgs defs (NS _ (UN $ Basic "AnyPtr")) [] = pure NPtr
@@ -449,7 +454,7 @@ getNArgs defs (NS _ (UN $ Basic "Struct")) [n, args]
 getNArgs defs n args = pure $ User n args
 
 nfToCFType : {auto c : Ref Ctxt Defs} ->
-             FC -> (inStruct : Bool) -> NF [] -> Core CFType
+             FC -> (inStruct : Bool) -> ClosedNF -> Core CFType
 nfToCFType _ _ (NPrimVal _ $ PrT IntType) = pure CFInt
 nfToCFType _ _ (NPrimVal _ $ PrT IntegerType) = pure CFInteger
 nfToCFType _ _ (NPrimVal _ $ PrT Bits8Type) = pure CFUnsigned8
@@ -469,15 +474,15 @@ nfToCFType _ _ (NPrimVal _ $ PrT WorldType) = pure CFWorld
 nfToCFType _ False (NBind fc _ (Pi _ _ _ ty) sc)
     = do defs <- get Ctxt
          sty <- nfToCFType fc False !(evalClosure defs ty)
-         sc' <- sc defs (toClosure defaultOpts [] (Erased fc Placeholder))
+         sc' <- sc defs (toClosure defaultOpts ScopeEmpty (Erased fc Placeholder))
          tty <- nfToCFType fc False sc'
          pure (CFFun sty tty)
 nfToCFType _ True (NBind fc _ _ _)
     = throw (GenericMsg fc "Function types not allowed in a foreign struct")
 nfToCFType _ s (NTCon fc n_in _ _ args)
     = do defs <- get Ctxt
          n <- toFullNames n_in
-         case !(getNArgs defs n $ map snd args) of
+         case !(getNArgs defs n $ toList (map snd args)) of
               User un uargs =>
                 do nargs <- traverse (evalClosure defs) uargs
                    cargs <- traverse (nfToCFType fc s) nargs
@@ -504,24 +509,24 @@ nfToCFType _ s (NErased _ _)
     = pure (CFUser (UN (Basic "__")) [])
 nfToCFType fc s t
     = do defs <- get Ctxt
-         ty <- quote defs [] t
+         ty <- quote defs ScopeEmpty t
          throw (GenericMsg (getLoc t)
                        ("Can't marshal type for foreign call " ++
                                       show !(toFullNames ty)))
 
 getCFTypes : {auto c : Ref Ctxt Defs} ->
-             List CFType -> NF [] ->
+             List CFType -> ClosedNF ->
              Core (List CFType, CFType)
 getCFTypes args (NBind fc _ (Pi _ _ _ ty) sc)
     = do defs <- get Ctxt
          aty <- nfToCFType fc False !(evalClosure defs ty)
-         sc' <- sc defs (toClosure defaultOpts [] (Erased fc Placeholder))
+         sc' <- sc defs (toClosure defaultOpts ScopeEmpty (Erased fc Placeholder))
          getCFTypes (aty :: args) sc'
 getCFTypes args t
     = pure (reverse args, !(nfToCFType (getLoc t) False t))
 
-lamRHSenv : Int -> FC -> (ns : List Name) -> (SizeOf ns, SubstCEnv ns [])
-lamRHSenv i fc [] = (zero, [])
+lamRHSenv : Int -> FC -> (ns : Scope) -> (SizeOf ns, SubstCEnv ns ScopeEmpty)
+lamRHSenv i fc [] = (zero, ScopeEmpty)
 lamRHSenv i fc (n :: ns)
     = let (s, env) = lamRHSenv (i + 1) fc ns in
       (suc s, CRef fc (MN "x" i) :: env)
@@ -531,7 +536,7 @@ mkBounds [] = None
 mkBounds (x :: xs) = Add x x (mkBounds xs)
 
 getNewArgs : {done : _} ->
-             SubstCEnv done args -> List Name
+             SubstCEnv done args -> Scope
 getNewArgs [] = []
 getNewArgs (CRef _ n :: xs) = n :: getNewArgs xs
 getNewArgs {done = x :: xs} (_ :: sub) = x :: getNewArgs sub
@@ -540,16 +545,16 @@ getNewArgs {done = x :: xs} (_ :: sub) = x :: getNewArgs sub
 -- we have to assume arity 0 for incremental compilation because
 -- we have no idea how it's defined, and when we made calls to the
 -- function, they had arity 0.
-lamRHS : (ns : List Name) -> CExp ns -> CExp []
+lamRHS : (ns : Scope) -> CExp ns -> ClosedCExp
 lamRHS ns 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
+          expLocs = mkLocals zero {vars = ScopeEmpty} bounds tmExp in
           lamBind (getFC tm) _ expLocs
   where
-    lamBind : FC -> (ns : List Name) -> CExp ns -> CExp []
+    lamBind : FC -> (ns : Scope) -> CExp ns -> ClosedCExp
     lamBind fc [] tm = tm
     lamBind fc (n :: ns) tm = lamBind fc ns (CLam fc n tm)
 
@@ -566,7 +571,7 @@ toCDef n ty erased (PMDef pi args _ tree _)
             else MkFun args' (shrinkCExp p comptree)
   where
     toLam : Bool -> CDef -> CDef
-    toLam True (MkFun args rhs) = MkFun [] (lamRHS args rhs)
+    toLam True (MkFun args rhs) = MkFun ScopeEmpty (lamRHS args rhs)
     toLam _ d = d
 toCDef n ty _ (ExternDef arity)
     = let (ns ** args) = mkArgList 0 arity in
@@ -580,7 +585,7 @@ toCDef n ty _ (ExternDef arity)
     getVars (ConsArg a rest) = MkVar First :: map weakenVar (getVars rest)
 toCDef n ty _ (ForeignDef arity cs)
     = do defs <- get Ctxt
-         (atys, retty) <- getCFTypes [] !(nf defs [] ty)
+         (atys, retty) <- getCFTypes [] !(nf defs ScopeEmpty ty)
          pure $ MkForeign cs atys retty
 toCDef n ty _ (Builtin {arity} op)
     = let (ns ** args) = mkArgList 0 arity in
@@ -595,7 +600,7 @@ toCDef n ty _ (Builtin {arity} op)
 toCDef n _ _ (DCon tag arity pos)
     = do let nt = snd <$> pos
          defs <- get Ctxt
-         args <- numArgs {vars = []} defs (Ref EmptyFC (DataCon tag arity) n)
+         args <- numArgs {vars = ScopeEmpty} defs (Ref EmptyFC (DataCon tag arity) n)
          let arity' = case args of
                  NewTypeBy ar _ => ar
                  EraseArgs ar erased => ar `minus` length erased
@@ -620,7 +625,7 @@ toCDef n ty _ def
 
 export
 compileExp : {auto c : Ref Ctxt Defs} ->
-             ClosedTerm -> Core (CExp [])
+             ClosedTerm -> Core ClosedCExp
 compileExp tm
     = do s <- newRef NextMN 0
          exp <- toCExp (UN $ Basic "main") tm