[ refactor ] ScopedSnocList: WIP

.github/workflows/ci-idris2-and-libs.yml

@@ -120,6 +120,8 @@ jobs:
       - name: Build current version
         run: |
           make && make install
+      - name: Test
+        run: make ci-ubuntu-test INTERACTIVE=''
       - name: Artifact Idris2 from previous version
         uses: actions/upload-artifact@v4
         with:

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

libs/test/Test/Golden.idr

@@ -231,7 +231,7 @@ runTest opts testPath = do
   let cg = maybe "" (" --cg " ++) (codegen opts)
   let exe = "\"" ++ exeUnderTest opts ++ cg ++ "\""
   ignore $ system $ "cd " ++ escapeArg testPath ++ " && " ++
-    "sh ./run " ++ exe ++ " | tr -d '\\r' > output"
+    "timeout 1m sh ./run " ++ exe ++ " | tr -d '\\r' > output"
   end <- clockTime UTC
 
   Right out <- readFile $ testPath ++ "/output"

src/Compiler/ANF.idr

@@ -4,12 +4,15 @@ import Compiler.LambdaLift
 
 import Core.CompileExpr
 import Core.Context
+import Core.Context.Log
 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,9 +139,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 : SnocList Name -> Type where
+     Lin : AVars [<]
+     (:<) : AVars xs -> Int -> AVars (xs :< x)
 
 data Next : Type where
 
@@ -150,8 +153,8 @@ nextVar
          pure i
 
 lookup : {idx : _} -> (0 p : IsVar x idx vs) -> AVars vs -> Int
-lookup First (x :: xs) = x
-lookup (Later p) (x :: xs) = lookup p xs
+lookup First (xs :< x) = x
+lookup (Later p) (xs :< x) = lookup p xs
 
 bindArgs : {auto v : Ref Next Int} ->
            List ANF -> Core (List (AVar, Maybe ANF))
@@ -187,6 +190,15 @@ mlet fc val sc
     = do i <- nextVar
          pure $ ALet fc i val (sc (ALocal i))
 
+bindAsFresh :
+  {auto v : Ref Next Int} ->
+  (args : List Name) -> AVars vars' ->
+  Core (List Int, AVars (vars' <>< args))
+bindAsFresh [] vs = pure ([], vs)
+bindAsFresh (n :: ns) vs
+    = do i <- nextVar
+         mapFst (i ::) <$> bindAsFresh ns (vs :< i)
+
 mutual
   anfArgs : {vars : _} ->
             {auto v : Ref Next Int} ->
@@ -203,15 +215,16 @@ mutual
   anf vs (LAppName fc lazy n args)
       = anfArgs fc vs args (AAppName fc lazy n)
   anf vs (LUnderApp fc n m args)
-      = anfArgs fc vs args (AUnderApp fc n m)
+    --   = anfArgs fc vs (reverse args) (AUnderApp fc n m)
+    = anfArgs fc vs args (AUnderApp fc n m)
   anf vs (LApp fc lazy f a)
       = anfArgs fc vs [f, a] $
                 \case
                   [fvar, avar] => AApp fc lazy fvar avar
                   _ => ACrash fc "Can't happen (AApp)"
   anf vs (LLet fc x val sc)
       = do i <- nextVar
-           let vs' = i :: vs
+           let vs' = vs :< i
            pure $ ALet fc i !(anf vs val) !(anf vs' sc)
   anf vs (LCon fc n ci t args)
       = anfArgs fc vs args (ACon fc n ci t)
@@ -241,16 +254,8 @@ mutual
               {auto v : Ref Next Int} ->
               AVars vars -> LiftedConAlt vars -> Core AConAlt
   anfConAlt vs (MkLConAlt n ci t args sc)
-      = do (is, vs') <- bindArgs args vs
+      = do (is, vs') <- bindAsFresh 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
-          = do i <- nextVar
-               (is, vs') <- bindArgs ns vs
-               pure (i :: is, i :: vs')
 
   anfConstAlt : {vars : _} ->
                 {auto v : Ref Next Int} ->
@@ -259,28 +264,23 @@ mutual
       = pure $ MkAConstAlt c !(anf vs sc)
 
 export
-toANF : LiftedDef -> Core ANFDef
+toANF : {auto c : Ref Ctxt Defs} -> LiftedDef -> Core ANFDef
 toANF (MkLFun args scope sc)
     = do v <- newRef Next (the Int 0)
-         (iargs, vsNil) <- bindArgs args []
-         let vs : AVars args = rewrite sym (appendNilRightNeutral args) in
-                                      vsNil
-         (iargs', vs) <- bindArgs scope vs
-         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
-        = do i <- nextVar
-             (is, vs') <- bindArgs ns vs
-             pure (i :: is, i :: vs')
+         log "compile.execute" 40 $ "toANF args: \{show $ toList args}, scope: \{show $ asList scope}, lifted: \{show sc}"
+         (iargs, vsNil) <- bindAsFresh (cast args) [<]
+         let vs : AVars args
+           := rewrite sym $ appendLinLeftNeutral args in
+              rewrite snocAppendAsFish [<] args in vsNil
+         (iargs', vs) <- bindAsFresh (cast scope) vs
+         sc' <- anf (rewrite snocAppendAsFish args scope in vs) sc
+         log "compile.execute" 40 $ "toANF iargs: \{show iargs}, iargs': \{show iargs'}, lifted: \{show sc'}"
+         pure $ MkAFun (iargs ++ iargs') sc'
 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 [<] 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
 
 {-
@@ -32,38 +37,39 @@ case t of
 
 shiftUnder : {args : _} ->
              {idx : _} ->
-             (0 p : IsVar n idx (x :: args ++ vars)) ->
-             NVar n (args ++ x :: vars)
+             (0 p : IsVar n idx (vars ++ args :< x)) ->
+             NVar n (vars :< x ++ args)
 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))
+shiftVar :  {outer : Scope} -> {args : List Name} ->
+           NVar n ((vars <>< args :< x) ++ outer) ->
+           NVar n ((vars :< x <>< args) ++ outer)
 shiftVar nvar
   = let out = mkSizeOf outer in
+    -- TODO: G.Allois version has Left/Right swap
     case locateNVar out nvar of
       Left nvar => embed nvar
-      Right (MkNVar p) => weakenNs out (shiftUnder p)
+      Right (MkNVar p) => weakenNs out (shiftUndersN (mkSizeOf _) p)
 
 mutual
+  renameVar : IsVar x i ((vars :< old <>< args) ++ local) ->
+              IsVar x i ((vars :< new <>< args) ++ local)
+  renameVar = believe_me -- it's the same index, so just the identity at run time
+
   shiftBinder : {outer, args : _} ->
                 (new : Name) ->
-                CExp (outer ++ old :: (args ++ vars)) ->
-                CExp (outer ++ (args ++ new :: vars))
+                CExp (((vars <>< args) :< old) ++ outer) ->
+                CExp ((vars :< new <>< args) ++ outer)
   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 = 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 = outer :< n} 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 = outer :< n} 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)
@@ -85,36 +91,36 @@ mutual
   shiftBinder new (CErased fc) = CErased fc
   shiftBinder new (CCrash fc msg) = CCrash fc msg
 
-  shiftBinderConAlt : {outer, args : _} ->
+  shiftBinderConAlt : {outer : _} -> {args : _} ->
                 (new : Name) ->
-                CConAlt (outer ++ (x :: args ++ vars)) ->
-                CConAlt (outer ++ (args ++ new :: vars))
+                CConAlt (((vars <>< args) :< old) ++ outer) ->
+                CConAlt ((vars :< new <>< args) ++ outer)
   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 (((vars <>< args) :< old) ++ (outer <>< args'))
+                = rewrite sym $ snocAppendFishAssociative (vars <>< args :< old) outer args' in sc in
         MkConAlt n ci t args' $
-           rewrite (appendAssociative args' outer (args ++ new :: vars))
-             in shiftBinder new {outer = args' ++ outer} sc'
+           rewrite snocAppendFishAssociative (vars :< new <>< args) outer args'
+             in shiftBinder new {outer = outer <>< args'} sc'
 
   shiftBinderConstAlt : {outer, args : _} ->
                 (new : Name) ->
-                CConstAlt (outer ++ (x :: args ++ vars)) ->
-                CConstAlt (outer ++ (args ++ new :: vars))
+                CConstAlt (((vars <>< args) :< old) ++ outer) ->
+                CConstAlt ((vars :< new <>< args) ++ outer)
   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 (vars <>< args :< old) ->
+                CExp (vars :< new <>< args)
+liftOutLambda = shiftBinder {outer = [<]}
 
 -- 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 (vars :< new)))
 tryLiftOut new [] = Just []
 tryLiftOut new (MkConAlt n ci t args (CLam fc x sc) :: as)
     = do as' <- tryLiftOut new as
@@ -124,7 +130,7 @@ tryLiftOut _ _ = Nothing
 
 tryLiftOutConst : (new : Name) ->
                   List (CConstAlt vars) ->
-                  Maybe (List (CConstAlt (new :: vars)))
+                  Maybe (List (CConstAlt (vars :< new)))
 tryLiftOutConst new [] = Just []
 tryLiftOutConst new (MkConstAlt c (CLam fc x sc) :: as)
     = do as' <- tryLiftOutConst new as
@@ -134,7 +140,7 @@ tryLiftOutConst _ _ = Nothing
 
 tryLiftDef : (new : Name) ->
              Maybe (CExp vars) ->
-             Maybe (Maybe (CExp (new :: vars)))
+             Maybe (Maybe (CExp (vars :< new)))
 tryLiftDef new Nothing = Just Nothing
 tryLiftDef new (Just (CLam fc x sc))
    = let sc' = liftOutLambda {args = []} new sc in
@@ -313,8 +319,8 @@ doCaseOfCase fc x xalts xdef alts def
     updateAlt (MkConAlt n ci t args sc)
         = MkConAlt n ci t args $
               CConCase fc sc
-                       (map (weakenNs (mkSizeOf args)) alts)
-                       (map (weakenNs (mkSizeOf args)) def)
+                       (map (weakensN (mkSizeOf args)) alts)
+                       (map (weakensN (mkSizeOf args)) def)
 
     updateDef : CExp vars -> CExp vars
     updateDef sc = CConCase fc sc alts def