Merge pull request #3194 from buzden/elab-treat-spec-map-ap

[ fix ] Exponentially reduce memory consumption for elab scripts running

libs/base/Language/Reflection.idr

@@ -34,6 +34,8 @@ data LookupDir =
 export
 data Elab : Type -> Type where
      Pure : a -> Elab a
+     Map  : (a -> b) -> Elab a -> Elab b
+     Ap   : Elab (a -> b) -> Elab a -> Elab b
      Bind : Elab a -> (a -> Elab b) -> Elab b
      Fail : FC -> String -> Elab a
      Warn : FC -> String -> Elab ()
@@ -103,12 +105,12 @@ data Elab : Type -> Type where
 
 export
 Functor Elab where
-  map f e = Bind e $ Pure . f
+  map = Map
 
 export
 Applicative Elab where
   pure = Pure
-  f <*> a = Bind f (<$> a)
+  (<*>) = Ap
 
 export
 Alternative Elab where

src/TTImp/Elab/RunElab.idr

@@ -159,6 +159,20 @@ elabScript rig fc nest env script@(NDCon nfc nm t ar args) exp
     elabCon defs "Pure" [_,val]
         = do empty <- clearDefs defs
              evalClosure empty val
+    elabCon defs "Map" [_,_,fm,act]
+        -- fm : A -> B
+        -- elab : A
+        = do act <- elabScript rig fc nest env !(evalClosure defs act) exp
+             act <- quote defs env act
+             fm <- evalClosure defs fm
+             applyToStack defs withHoles env fm [(getLoc act, toClosure withAll env act)]
+    elabCon defs "Ap" [_,_,actF,actX]
+        -- actF : Elab (A -> B)
+        -- actX : Elab A
+        = do actF <- elabScript rig fc nest env !(evalClosure defs actF) exp
+             actX <- elabScript rig fc nest env !(evalClosure defs actX) exp
+             actX <- quote defs env actX
+             applyToStack defs withHoles env actF [(getLoc actX, toClosure withAll env actX)]
     elabCon defs "Bind" [_,_,act,k]
         -- act : Elab A
         -- k : A -> Elab B

tests/idris2/reflection/reflection008/Interp.idr

@@ -61,3 +61,14 @@ testBlock = Op {a=Base Nat} {b=Base Nat} plus (Val 3) (Val 4)
 
 evalBlock : Nat
 evalBlock = eval [] testBlock
+
+namespace Hidden
+  export
+  unreducible : Nat -> Nat -> Nat
+  unreducible x y = y `minus` x
+
+testBlock' : Lang gam (Base Nat)
+testBlock' = Op {a=Base Nat} {b=Base Nat} unreducible (Val 3) (Val 4)
+
+evalBlock' : Nat
+evalBlock' = eval [] testBlock'

tests/idris2/reflection/reflection008/expected

@@ -3,5 +3,7 @@ Main> Main.evalAdd : Nat -> Nat -> Nat
 evalAdd x y = let add = \val, val => plus val val in add x y
 Main> Main.evalBlock : Nat
 evalBlock = plus 3 4
+Main> Main.evalBlock' : Nat
+evalBlock' = unreducible 3 4
 Main> 5
 Main> Bye for now!

tests/idris2/reflection/reflection008/input

@@ -1,4 +1,5 @@
 :printdef evalAdd
 :printdef evalBlock
+:printdef evalBlock'
 evalAdd 2 3
 :q