ScopedSnocList: WIP

src/Compiler/ANF.idr

@@ -6,6 +6,7 @@ import Core.CompileExpr
 import Core.Context
 import Core.Core
 import Core.TT
+import Core.Name.ScopedList
 
 import Data.List
 import Data.Vect
@@ -136,9 +137,9 @@ Show ANFDef where
         show args ++ " -> " ++ show ret
   show (MkAError exp) = "Error: " ++ show exp
 
-data AVars : List Name -> Type where
-     Nil : AVars []
-     (::) : Int -> AVars xs -> AVars (x :: xs)
+data AVars : ScopedList Name -> Type where
+     Nil : AVars SLNil
+     (::) : Int -> AVars xs -> AVars (x :%: xs)
 
 data Next : Type where
 
@@ -194,7 +195,7 @@ mutual
             List (Lifted vars) -> (List AVar -> ANF) -> Core ANF
   anfArgs fc vs args f
       = do args' <- traverse (anf vs) args
-           letBind fc args' f
+           letBind fc (toList args') f
 
   anf : {vars : _} ->
         {auto v : Ref Next Int} ->
@@ -244,10 +245,10 @@ mutual
       = do (is, vs') <- bindArgs args vs
            pure $ MkAConAlt n ci t is !(anf vs' sc)
     where
-      bindArgs : (args : List Name) -> AVars vars' ->
-                 Core (List Int, AVars (args ++ vars'))
-      bindArgs [] vs = pure ([], vs)
-      bindArgs (n :: ns) vs
+      bindArgs : (args : ScopedList Name) -> AVars vars' ->
+                 Core (List Int, AVars (args +%+ vars'))
+      bindArgs SLNil vs = pure ([], vs)
+      bindArgs (n :%: ns) vs
           = do i <- nextVar
                (is, vs') <- bindArgs ns vs
                pure (i :: is, i :: vs')
@@ -269,10 +270,10 @@ toANF (MkLFun args scope sc)
          pure $ MkAFun (iargs ++ reverse iargs') !(anf vs sc)
   where
     bindArgs : {auto v : Ref Next Int} ->
-               (args : List Name) -> AVars vars' ->
-               Core (List Int, AVars (args ++ vars'))
-    bindArgs [] vs = pure ([], vs)
-    bindArgs (n :: ns) vs
+               (args : ScopedList Name) -> AVars vars' ->
+               Core (List Int, AVars (args +%+ vars'))
+    bindArgs SLNil vs = pure ([], vs)
+    bindArgs (n :%: ns) vs
         = do i <- nextVar
              (is, vs') <- bindArgs ns vs
              pure (i :: is, i :: vs')

src/Compiler/CaseOpts.idr

@@ -32,14 +32,14 @@ case t of
 
 shiftUnder : {args : _} ->
              {idx : _} ->
-             (0 p : IsVar n idx (x :: args ++ vars)) ->
-             NVar n (args ++ x :: vars)
+             (0 p : IsVar n idx (x :%: args +%+ vars)) ->
+             NVar n (args +%+ x :%: vars)
 shiftUnder First = weakenNVar (mkSizeOf args) (MkNVar First)
 shiftUnder (Later p) = insertNVar (mkSizeOf args) (MkNVar p)
 
 shiftVar : {outer, args : Scope} ->
-           NVar n (outer ++ (x :: args ++ vars)) ->
-           NVar n (outer ++ (args ++ x :: vars))
+           NVar n (outer +%+ (x :%: args +%+ vars)) ->
+           NVar n (outer +%+ (args +%+ x :%: vars))
 shiftVar nvar
   = let out = mkSizeOf outer in
     case locateNVar out nvar of
@@ -49,21 +49,21 @@ shiftVar nvar
 mutual
   shiftBinder : {outer, args : _} ->
                 (new : Name) ->
-                CExp (outer ++ old :: (args ++ vars)) ->
-                CExp (outer ++ (args ++ new :: vars))
+                CExp (outer +%+ old :%: (args +%+ vars)) ->
+                CExp (outer +%+ (args +%+ new :%: vars))
   shiftBinder new (CLocal fc p)
       = case shiftVar (MkNVar p) of
              MkNVar p' => CLocal fc (renameVar p')
     where
-      renameVar : IsVar x i (outer ++ (args ++ (old :: rest))) ->
-                  IsVar x i (outer ++ (args ++ (new :: rest)))
+      renameVar : IsVar x i (outer +%+ (args +%+ (old :%: rest))) ->
+                  IsVar x i (outer +%+ (args +%+ (new :%: rest)))
       renameVar = believe_me -- it's the same index, so just the identity at run time
   shiftBinder new (CRef fc n) = CRef fc n
   shiftBinder {outer} new (CLam fc n sc)
-      = CLam fc n $ shiftBinder {outer = n :: outer} new sc
+      = CLam fc n $ shiftBinder {outer = n :%: outer} new sc
   shiftBinder new (CLet fc n inlineOK val sc)
       = CLet fc n inlineOK (shiftBinder new val)
-                           $ shiftBinder {outer = n :: outer} new sc
+                           $ shiftBinder {outer = n :%: outer} new sc
   shiftBinder new (CApp fc f args)
       = CApp fc (shiftBinder new f) $ map (shiftBinder new) args
   shiftBinder new (CCon fc ci c tag args)
@@ -87,34 +87,34 @@ mutual
 
   shiftBinderConAlt : {outer, args : _} ->
                 (new : Name) ->
-                CConAlt (outer ++ (x :: args ++ vars)) ->
-                CConAlt (outer ++ (args ++ new :: vars))
+                CConAlt (outer +%+ (x :%: args +%+ vars)) ->
+                CConAlt (outer +%+ (args +%+ new :%: vars))
   shiftBinderConAlt new (MkConAlt n ci t args' sc)
-      = let sc' : CExp ((args' ++ outer) ++ (x :: args ++ vars))
-                = rewrite sym (appendAssociative args' outer (x :: args ++ vars)) in sc in
+      = let sc' : CExp ((args' +%+ outer) +%+ (x :%: args +%+ vars))
+                = rewrite sym (appendAssociative args' outer (x :%: args +%+ vars)) in sc in
         MkConAlt n ci t args' $
-           rewrite (appendAssociative args' outer (args ++ new :: vars))
-             in shiftBinder new {outer = args' ++ outer} sc'
+           rewrite (appendAssociative args' outer (args +%+ new :%: vars))
+             in shiftBinder new {outer = args' +%+ outer} sc'
 
   shiftBinderConstAlt : {outer, args : _} ->
                 (new : Name) ->
-                CConstAlt (outer ++ (x :: args ++ vars)) ->
-                CConstAlt (outer ++ (args ++ new :: vars))
+                CConstAlt (outer +%+ (x :%: args +%+ vars)) ->
+                CConstAlt (outer +%+ (args +%+ new :%: vars))
   shiftBinderConstAlt new (MkConstAlt c sc) = MkConstAlt c $ shiftBinder new sc
 
 -- If there's a lambda inside a case, move the variable so that it's bound
 -- outside the case block so that we can bind it just once outside the block
 liftOutLambda : {args : _} ->
                 (new : Name) ->
-                CExp (old :: args ++ vars) ->
-                CExp (args ++ new :: vars)
-liftOutLambda = shiftBinder {outer = []}
+                CExp (old :%: args +%+ vars) ->
+                CExp (args +%+ new :%: vars)
+liftOutLambda = shiftBinder {outer = SLNil}
 
 -- If all the alternatives start with a lambda, we can have a single lambda
 -- binding outside
 tryLiftOut : (new : Name) ->
              List (CConAlt vars) ->
-             Maybe (List (CConAlt (new :: vars)))
+             Maybe (List (CConAlt (new :%: vars)))
 tryLiftOut new [] = Just []
 tryLiftOut new (MkConAlt n ci t args (CLam fc x sc) :: as)
     = do as' <- tryLiftOut new as
@@ -124,20 +124,20 @@ tryLiftOut _ _ = Nothing
 
 tryLiftOutConst : (new : Name) ->
                   List (CConstAlt vars) ->
-                  Maybe (List (CConstAlt (new :: vars)))
+                  Maybe (List (CConstAlt (new :%: vars)))
 tryLiftOutConst new [] = Just []
 tryLiftOutConst new (MkConstAlt c (CLam fc x sc) :: as)
     = do as' <- tryLiftOutConst new as
-         let sc' = liftOutLambda {args = []} new sc
+         let sc' = liftOutLambda {args = SLNil} new sc
          pure (MkConstAlt c sc' :: as')
 tryLiftOutConst _ _ = Nothing
 
 tryLiftDef : (new : Name) ->
              Maybe (CExp vars) ->
-             Maybe (Maybe (CExp (new :: vars)))
+             Maybe (Maybe (CExp (new :%: vars)))
 tryLiftDef new Nothing = Just Nothing
 tryLiftDef new (Just (CLam fc x sc))
-   = let sc' = liftOutLambda {args = []} new sc in
+   = let sc' = liftOutLambda {args = SLNil} new sc in
          pure (Just sc')
 tryLiftDef _ _ = Nothing
 

src/Compiler/Common.idr

@@ -80,7 +80,7 @@ Ord UsePhase where
 public export
 record CompileData where
   constructor MkCompileData
-  mainExpr : CExp [] -- main expression to execute. This also appears in
+  mainExpr : CExp SLNil -- 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'.
@@ -152,7 +152,7 @@ getMinimalDef (Coded ns bin)
          name <- fromBuf b
          let def
              = MkGlobalDef fc name (Erased fc Placeholder) [] [] [] [] mul
-                           [] (specified Public) (MkTotality Unchecked IsCovering) False
+                           SLNil (specified Public) (MkTotality Unchecked IsCovering) False
                            [] Nothing refsR False False True
                            None cdef Nothing [] Nothing
          pure (def, Just (ns, bin))
@@ -351,8 +351,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 SLNil SLNil liftedtm) ::
+                      (ldefs ++ concat lifted_in)
 
          anf <- if phase >= ANF
                    then logTime 2 "Get ANF" $ traverse (\ (n, d) => pure (n, !(toANF d))) lifted
@@ -408,7 +408,7 @@ getCompileData = getCompileDataWith []
 
 export
 compileTerm : {auto c : Ref Ctxt Defs} ->
-              ClosedTerm -> Core (CExp [])
+              ClosedTerm -> Core (CExp SLNil)
 compileTerm tm_in
     = do tm <- toFullNames tm_in
          fixArityExp !(compileExp tm)