[ refactor ] Port Yaffle's Value

.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

@@ -52,7 +52,6 @@ modules =
     Core.Binary.Prims,
     Core.Case.CaseBuilder,
     Core.Case.CaseTree,
-    Core.Case.CaseTree.Pretty,
     Core.Case.Util,
     Core.CompileExpr,
     Core.CompileExpr.Pretty,
@@ -62,12 +61,18 @@ modules =
     Core.Context.Log,
     Core.Context.Pretty,
     Core.Context.TTC,
+    Core.Evaluate,
+    Core.Evaluate.Convert,
+    Core.Evaluate.Expand,
+    Core.Evaluate.Normalise,
+    Core.Evaluate.Value,
+    Core.Evaluate.Quote,
     Core.Core,
     Core.Coverage,
     Core.Directory,
     Core.Env,
+    Core.Erase,
     Core.FC,
-    Core.GetType,
     Core.Hash,
     Core.InitPrimitives,
     Core.LinearCheck,
@@ -76,16 +81,11 @@ modules =
     Core.Name.CompatibleVars,
     Core.Name.Namespace,
     Core.Name.Scoped,
-    Core.Normalise,
-    Core.Normalise.Convert,
-    Core.Normalise.Eval,
-    Core.Normalise.Quote,
     Core.Options,
     Core.Options.Log,
     Core.Ord,
     Core.Primitives,
     Core.Reflect,
-    Core.SchemeEval,
     Core.Termination.CallGraph,
     Core.Termination.SizeChange,
     Core.Termination.Positivity,
@@ -104,15 +104,8 @@ modules =
     Core.TTC,
     Core.Unify,
     Core.UnifyState,
-    Core.Value,
     Core.WithData,
 
-    Core.SchemeEval.Builtins,
-    Core.SchemeEval.Compile,
-    Core.SchemeEval.Evaluate,
-    Core.SchemeEval.Quote,
-    Core.SchemeEval.ToScheme,
-
     IdrisPaths,
 
     Idris.CommandLine,
@@ -198,6 +191,7 @@ modules =
     Libraries.Data.SnocList.HasLength,
     Libraries.Data.SnocList.LengthMatch,
     Libraries.Data.SnocList.SizeOf,
+    Libraries.Data.SnocList.Quantifiers.Extra,
     Libraries.Data.Span,
     Libraries.Data.SparseMatrix,
     Libraries.Data.String,
@@ -273,7 +267,6 @@ modules =
     TTImp.Elab,
     TTImp.Impossible,
     TTImp.Parser,
-    TTImp.PartialEval,
     TTImp.ProcessBuiltin,
     TTImp.ProcessData,
     TTImp.ProcessDecls,

libs/contrib/Data/List/TailRec.idr

@@ -196,17 +196,15 @@ partitionOnto_ext : (lfts, rgts : List a) -> (p : a -> Bool) -> (xs : List a) ->
 partitionOnto_ext  lfts rgts p [] = Refl
 partitionOnto_ext  lfts rgts p (x::xs) with (@@(p x), @@(List.partition p xs))
  partitionOnto_ext lfts rgts p (x::xs) | ((True **px_tru), ((dl_l, dl_r)**dl_pf))
-   = rewrite px_tru in
-     rewrite dl_pf  in
+   = rewrite dl_pf  in
      rewrite px_tru in
      let u = partitionOnto_ext (x :: lfts) rgts p xs in
      coe (\u => (reverseOnto (x :: fst u) lfts
                 ,reverseOnto (     snd u) rgts)
                 = partitionOnto (x :: lfts) rgts p xs) dl_pf u
 
  partitionOnto_ext lfts rgts p (x::xs) | ((False**px_fls), ((dl_l, dl_r)**dl_pf))
-   = rewrite px_fls in
-     rewrite dl_pf  in
+   = rewrite dl_pf  in
      rewrite px_fls in
      let u = partitionOnto_ext lfts (x :: rgts) p xs in
      coe (\u => (reverseOnto (     fst u) lfts

libs/test/Test/Golden.idr

@@ -230,8 +230,10 @@ runTest opts testPath = do
   start <- clockTime UTC
   let cg = maybe "" (" --cg " ++) (codegen opts)
   let exe = "\"" ++ exeUnderTest opts ++ cg ++ "\""
+  putStrLn $ "Running " ++ testPath
+  fflush stdout
   ignore $ system $ "cd " ++ escapeArg testPath ++ " && " ++
-    "sh ./run " ++ exe ++ " | tr -d '\\r' > output"
+    "timeout 120s sh ./run " ++ exe ++ " | tr -d '\\r' > output"
   end <- clockTime UTC
 
   Right out <- readFile $ testPath ++ "/output"

src/Algebra/Semiring.idr

@@ -56,3 +56,7 @@ branchOne yes no rig = if isLinear rig then yes else no
 export
 branchVal : (Semiring a, Eq a) => Lazy b -> Lazy b -> a -> b
 branchVal yes no rig = if isRigOther rig then yes else no
+
+export
+presence : Semiring a => Eq a => a -> a
+presence = elimSemi erased linear (const linear)

src/Compiler/ANF.idr

@@ -4,10 +4,15 @@ import Compiler.LambdaLift
 
 import Core.CompileExpr
 import Core.Context
+import Core.Context.Log
 
+import Data.SnocList.Quantifiers
+import Data.String
 import Data.SortedSet
 import Data.Vect
 
+import Libraries.Data.SnocList.Extra
+
 %default covering
 
 -- Convert the lambda lifted form to ANF, with variable names made explicit.
@@ -82,26 +87,26 @@ mutual
   Show ANF where
     show (AV _ v) = show v
     show (AAppName fc lazy n args)
-        = show n ++ showLazy lazy ++ "(" ++ showSep ", " (map show args) ++ ")"
+        = show n ++ showLazy lazy ++ "(" ++ joinBy ", " (map show args) ++ ")"
     show (AUnderApp fc n m args)
         = "<" ++ show n ++ " underapp " ++ show m ++ ">(" ++
-          showSep ", " (map show args) ++ ")"
+          joinBy ", " (map show args) ++ ")"
     show (AApp fc lazy c arg)
         = show c ++ showLazy lazy ++ " @ (" ++ show arg ++ ")"
     show (ALet fc x val sc)
         = "%let v" ++ show x ++ " = (" ++ show val ++ ") in (" ++ show sc ++ ")"
     show (ACon fc n _ t args)
-        = "%con " ++ show n ++ "(" ++ showSep ", " (map show args) ++ ")"
+        = "%con " ++ show n ++ "(" ++ joinBy ", " (map show args) ++ ")"
     show (AOp fc lazy op args)
-        = "%op " ++ show op ++ showLazy lazy ++ "(" ++ showSep ", " (toList (map show args)) ++ ")"
+        = "%op " ++ show op ++ showLazy lazy ++ "(" ++ joinBy ", " (toList (map show args)) ++ ")"
     show (AExtPrim fc lazy p args)
-        = "%extprim " ++ show p ++ showLazy lazy ++ "(" ++ showSep ", " (map show args) ++ ")"
+        = "%extprim " ++ show p ++ showLazy lazy ++ "(" ++ joinBy ", " (map show args) ++ ")"
     show (AConCase fc sc alts def)
         = "%case " ++ show sc ++ " of { "
-             ++ showSep "| " (map show alts) ++ " " ++ show def ++ " }"
+             ++ joinBy "| " (map show alts) ++ " " ++ show def ++ " }"
     show (AConstCase fc sc alts def)
         = "%case " ++ show sc ++ " of { "
-             ++ showSep "| " (map show alts) ++ " " ++ show def ++ " }"
+             ++ joinBy "| " (map show alts) ++ " " ++ show def ++ " }"
     show (APrimVal _ x) = show x
     show (AErased _) = "___"
     show (ACrash _ x) = "%CRASH(" ++ show x ++ ")"
@@ -111,7 +116,7 @@ mutual
   Show AConAlt where
     show (MkAConAlt n _ t args sc)
         = "%conalt " ++ show n ++
-             "(" ++ showSep ", " (map showArg args) ++ ") => " ++ show sc
+             "(" ++ joinBy ", " (map showArg args) ++ ") => " ++ show sc
       where
         showArg : Int -> String
         showArg i = "v" ++ show i
@@ -136,6 +141,12 @@ Show ANFDef where
 AVars : Scope -> Type
 AVars = All (\_ => Int)
 
+namespace AVars
+  public export
+  empty : AVars Scope.empty
+  empty = [<]
+
+
 data Next : Type where
 
 nextVar : {auto v : Ref Next Int} ->
@@ -145,10 +156,6 @@ nextVar
          put Next (i + 1)
          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
-
 bindArgs : {auto v : Ref Next Int} ->
            List ANF -> Core (List (AVar, Maybe ANF))
 bindArgs [] = pure []
@@ -183,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 (Scope.ext vars' args))
+bindAsFresh [] vs = pure ([], vs)
+bindAsFresh (n :: ns) vs
+    = do i <- nextVar
+         mapFst (i ::) <$> bindAsFresh ns (vs :< i)
+
 mutual
   anfArgs : {auto v : Ref Next Int} ->
             FC -> AVars vars ->
@@ -193,7 +209,7 @@ mutual
 
   anf : {auto v : Ref Next Int} ->
         AVars vars -> Lifted vars -> Core ANF
-  anf vs (LLocal fc p) = pure $ AV fc (ALocal (lookup p vs))
+  anf vs (LLocal fc p) = pure $ AV fc (ALocal (lookup vs p))
   anf vs (LAppName fc lazy n args)
       = anfArgs fc vs args (AAppName fc lazy n)
   anf vs (LUnderApp fc n m args)
@@ -205,7 +221,7 @@ mutual
                   _ => 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)
@@ -231,48 +247,44 @@ mutual
   anf vs (LErased fc) = pure $ AErased fc
   anf vs (LCrash fc err) = pure $ ACrash fc err
 
+  anfConScope : {auto v : Ref Next Int} ->
+                AVars vars -> LiftedCaseScope vars ->
+                Core (List Int, ANF)
+  anfConScope vs (LRHS sc) = pure ([], !(anf vs sc))
+  anfConScope vs (LArg x sc)
+      = do i <- nextVar
+           (args, sc') <- anfConScope (vs :< i) sc
+           pure (i :: args, sc')
+
   anfConAlt : {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
-           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')
+  anfConAlt vs (MkLConAlt n ci t sc)
+      = do (args, sc') <- anfConScope vs sc
+           pure $ MkAConAlt n ci t args sc'
 
   anfConstAlt : {auto v : Ref Next Int} ->
                 AVars vars -> LiftedConstAlt vars -> Core AConstAlt
   anfConstAlt vs (MkLConstAlt c sc)
       = 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 args AVars.empty
+         (iargs', vs) <- bindAsFresh (toList scope) vsNil
+         sc' <- anf vs $
+            do rewrite fishAsSnocAppend (cast args) (toList scope)
+               rewrite castToList scope
+               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 AVars.empty err)
 
 export
 freeVariables : ANF -> SortedSet AVar