Record erasable args in definitions

This could allow us to actually erase (rather than compile with nil)
although experiments show that has no impact on performance. It is
useful to see, though, and other back ends may benefit.

idris2.ipkg

@@ -98,6 +98,7 @@ modules =
     TTImp.Elab.Record,
     TTImp.Elab.Rewrite,
     TTImp.Elab.Term,
+    TTImp.Elab.Utils,
     TTImp.Interactive.CaseSplit,
     TTImp.Interactive.ExprSearch,
     TTImp.Interactive.GenerateDef,

src/Compiler/CompileExpr.idr

@@ -159,7 +159,7 @@ mutual
   toCExpTm tags n (Bind fc x (Lam _ _ _) sc)
       = pure $ CLam fc x !(toCExp tags n sc)
   toCExpTm tags n (Bind fc x (Let Rig0 val _) sc)
-      = pure $ CLet fc x (CErased fc) !(toCExp tags n sc)
+      = pure $ shrinkCExp (DropCons SubRefl) !(toCExp tags n sc)
   toCExpTm tags n (Bind fc x (Let _ val _) sc)
       = pure $ CLet fc x !(toCExp tags n val) !(toCExp tags n sc)
   toCExpTm tags n (Bind fc x (Pi c e ty) sc)

src/Core/Binary.idr

@@ -27,7 +27,7 @@ import Data.Buffer
 -- TTC files can only be compatible if the version number is the same
 export
 ttcVersion : Int
-ttcVersion = 7
+ttcVersion = 8
 
 export
 checkTTCVersion : Int -> Int -> Core ()

src/Core/CompileExpr.idr

@@ -30,9 +30,9 @@ mutual
        COp : FC -> PrimFn arity -> Vect arity (CExp vars) -> CExp vars
        -- Externally defined primitive operations
        CExtPrim : FC -> (p : Name) -> List (CExp vars) -> CExp vars
-       -- A forced (evaluated) value (TODO: is this right?)
+       -- A forced (evaluated) value
        CForce : FC -> CExp vars -> CExp vars
-       -- A delayed value (lazy? TODO: check)
+       -- A delayed value
        CDelay : FC -> CExp vars -> CExp vars
        -- A case match statement
        CConCase : FC -> (sc : CExp vars) -> List (CConAlt vars) -> Maybe (CExp vars) -> CExp vars
@@ -212,6 +212,51 @@ mutual
   embedConstAlt : CConstAlt args -> CConstAlt (args ++ vars)
   embedConstAlt (MkConstAlt c sc) = MkConstAlt c (embed sc)
 
+mutual
+  -- Shrink the scope of a compiled expression, replacing any variables not
+  -- in the remaining set with Erased
+  export
+  shrinkCExp : SubVars newvars vars -> CExp vars -> CExp newvars
+  shrinkCExp sub (CLocal fc prf) 
+      = case subElem prf sub of
+             Nothing => CErased fc
+             Just (MkVar prf') => CLocal fc prf'
+  shrinkCExp _ (CRef fc x) = CRef fc x
+  shrinkCExp sub (CLam fc x sc) 
+      = let sc' = shrinkCExp (KeepCons sub) sc in
+            CLam fc x sc'
+  shrinkCExp sub (CLet fc x val sc) 
+      = let sc' = shrinkCExp (KeepCons sub) sc in
+            CLet fc x (shrinkCExp sub val) sc'
+  shrinkCExp sub (CApp fc x xs)
+      = CApp fc (shrinkCExp sub x) (assert_total (map (shrinkCExp sub) xs))
+  shrinkCExp sub (CCon fc x tag xs)
+      = CCon fc x tag (assert_total (map (shrinkCExp sub) xs))
+  shrinkCExp sub (COp fc x xs)
+      = COp fc x (assert_total (map (shrinkCExp sub) xs))
+  shrinkCExp sub (CExtPrim fc p xs)
+      = CExtPrim fc p (assert_total (map (shrinkCExp sub) xs))
+  shrinkCExp sub (CForce fc x) = CForce fc (shrinkCExp sub x)
+  shrinkCExp sub (CDelay fc x) = CDelay fc (shrinkCExp sub x)
+  shrinkCExp sub (CConCase fc sc xs def)
+      = CConCase fc (shrinkCExp sub sc) 
+                 (assert_total (map (shrinkConAlt sub) xs))
+                 (assert_total (map (shrinkCExp sub) def))
+  shrinkCExp sub (CConstCase fc sc xs def)
+      = CConstCase fc (shrinkCExp sub sc) 
+                   (assert_total (map (shrinkConstAlt sub) xs))
+                   (assert_total (map (shrinkCExp sub) def))
+  shrinkCExp _ (CPrimVal fc x) = CPrimVal fc x
+  shrinkCExp _ (CErased fc) = CErased fc
+  shrinkCExp _ (CCrash fc x) = CCrash fc x
+
+  shrinkConAlt : SubVars newvars vars -> CConAlt vars -> CConAlt newvars
+  shrinkConAlt sub (MkConAlt x tag args sc)
+        = MkConAlt x tag args (shrinkCExp (subExtend args sub) sc)
+
+  shrinkConstAlt : SubVars newvars vars -> CConstAlt vars -> CConstAlt newvars
+  shrinkConstAlt sub (MkConstAlt x sc) = MkConstAlt x (shrinkCExp sub sc)
+
 mutual
   export
   Weaken CExp where

src/Core/Context.idr

@@ -162,6 +162,7 @@ record GlobalDef where
   location : FC
   fullname : Name -- original unresolved name
   type : ClosedTerm
+  eraseArgs : List Nat -- which argument positions to erase at runtime
   multiplicity : RigCount
   vars : List Name -- environment name is defined in
   visibility : Visibility
@@ -422,7 +423,7 @@ export
 newDef : FC -> Name -> RigCount -> List Name -> 
          ClosedTerm -> Visibility -> Def -> GlobalDef
 newDef fc n rig vars ty vis def 
-    = MkGlobalDef fc n ty rig vars vis unchecked [] empty False False False def
+    = MkGlobalDef fc n ty [] rig vars vis unchecked [] empty False False False def
                   Nothing []
 
 public export
@@ -817,7 +818,7 @@ addBuiltin : {auto x : Ref Ctxt Defs} ->
              Name -> ClosedTerm -> Totality ->
              PrimFn arity -> Core ()
 addBuiltin n ty tot op 
-    = do addDef n (MkGlobalDef emptyFC n ty RigW [] Public tot 
+    = do addDef n (MkGlobalDef emptyFC n ty [] RigW [] Public tot 
                                [Inline] empty False False True (Builtin op)
                                Nothing []) 
          pure ()

src/Core/TT.idr

@@ -795,6 +795,12 @@ subExtend : (ns : List Name) -> SubVars xs ys -> SubVars (ns ++ xs) (ns ++ ys)
 subExtend [] sub = sub
 subExtend (x :: xs) sub = KeepCons (subExtend xs sub)
 
+export
+subInclude : (ns : List Name) -> SubVars xs ys -> SubVars (xs ++ ns) (ys ++ ns)
+subInclude ns SubRefl = SubRefl
+subInclude ns (DropCons p) = DropCons (subInclude ns p)
+subInclude ns (KeepCons p) = KeepCons (subInclude ns p)
+
 mutual
   export
   shrinkBinder : Binder (Term vars) -> SubVars newvars vars -> 

src/Core/TTC.idr

@@ -846,6 +846,7 @@ TTC GlobalDef where
            when (isUserName (fullname gdef)) $
               do toBuf b (location gdef)
                  toBuf b (type gdef)
+                 toBuf b (eraseArgs gdef)
                  toBuf b (multiplicity gdef)
                  toBuf b (vars gdef)
                  toBuf b (visibility gdef)
@@ -863,17 +864,17 @@ TTC GlobalDef where
            let refs = map fromList refsList
            if isUserName name
               then do loc <- fromBuf b; 
-                      ty <- fromBuf b; mul <- fromBuf b
+                      ty <- fromBuf b; eargs <- fromBuf b; 
-                      vars <- fromBuf b
+                      mul <- fromBuf b; vars <- fromBuf b
                       vis <- fromBuf b; tot <- fromBuf b
                       fl <- fromBuf b
                       inv <- fromBuf b
                       c <- fromBuf b
                       sc <- fromBuf b
-                      pure (MkGlobalDef loc name ty mul vars vis 
+                      pure (MkGlobalDef loc name ty eargs mul vars vis 
                                         tot fl refs inv c True def cdef sc)
               else do let fc = emptyFC
-                      pure (MkGlobalDef fc name (Erased fc)
+                      pure (MkGlobalDef fc name (Erased fc) []
                                         RigW [] Public unchecked [] refs
                                         False False True def cdef [])
 

src/Idris/REPL.idr

@@ -52,6 +52,7 @@ showInfo (n, idx, d)
     = do coreLift $ putStrLn (show (fullname d) ++ " ==> " ++ 
                               show !(toFullNames (definition d)))
          coreLift $ putStrLn (show (multiplicity d))
+         coreLift $ putStrLn ("Erasable args: " ++ show (eraseArgs d))
          case compexpr d of
               Nothing => pure ()
               Just expr => coreLift $ putStrLn ("Compiled: " ++ show expr)

src/TTImp/ProcessData.idr

@@ -11,6 +11,7 @@ import Core.Value
 
 import TTImp.BindImplicits
 import TTImp.Elab.Check
+import TTImp.Elab.Utils
 import TTImp.Elab
 import TTImp.TTImp
 
@@ -201,8 +202,9 @@ processData {vars} eopts nest env fc vis (MkImpData dfc n_in ty_raw opts cons_ra
          addToSave n
          log 10 $ "Saving from " ++ show n ++ ": " ++ show (keys (getMetas ty))
 
+         let connames = map conName cons
          when (not (NoHints `elem` opts)) $
-              traverse_ (\x => addHintFor fc (Resolved tidx) x True False) (map conName cons)
+              traverse_ (\x => addHintFor fc (Resolved tidx) x True False) connames
 
-         pure ()
+         traverse_ updateErasable (Resolved tidx :: connames)
 

src/TTImp/ProcessType.idr

@@ -12,6 +12,7 @@ import Core.Value
 
 import TTImp.BindImplicits
 import TTImp.Elab.Check
+import TTImp.Elab.Utils
 import TTImp.Elab
 import TTImp.TTImp
 
@@ -101,7 +102,12 @@ processType {vars} eopts nest env fc rig vis opts (MkImpTy tfc n_in ty_raw)
          -- TODO: Check name visibility
 
          def <- initDef n env ty opts
-         addDef (Resolved idx) (newDef fc n rig vars (abstractEnvType tfc env ty) vis def)
+         let fullty = abstractEnvType tfc env ty
+         erased <- findErased fullty
+
+         addDef (Resolved idx) 
+                (record { eraseArgs = erased }
+                        (newDef fc n rig vars fullty vis def))
          -- Flag it as checked, because we're going to check the clauses 
          -- from the top level.
          -- But, if it's a case block, it'll be checked as part of the top