diff --git a/libs/base/Language/Reflection.idr b/libs/base/Language/Reflection.idr index 727aadef83..2dd00fd8b0 100644 --- a/libs/base/Language/Reflection.idr +++ b/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 diff --git a/src/TTImp/Elab/RunElab.idr b/src/TTImp/Elab/RunElab.idr index 9b709b73e6..979d7a0b6b 100644 --- a/src/TTImp/Elab/RunElab.idr +++ b/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 diff --git a/tests/idris2/reflection/reflection008/Interp.idr b/tests/idris2/reflection/reflection008/Interp.idr index 172e9d0eee..dcdfc09484 100644 --- a/tests/idris2/reflection/reflection008/Interp.idr +++ 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' diff --git a/tests/idris2/reflection/reflection008/expected b/tests/idris2/reflection/reflection008/expected index 35c1dc0c63..2909326996 100644 --- a/tests/idris2/reflection/reflection008/expected +++ b/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! diff --git a/tests/idris2/reflection/reflection008/input b/tests/idris2/reflection/reflection008/input index d2b2544434..b204da9cf6 100644 --- a/tests/idris2/reflection/reflection008/input +++ b/tests/idris2/reflection/reflection008/input @@ -1,4 +1,5 @@ :printdef evalAdd :printdef evalBlock +:printdef evalBlock' evalAdd 2 3 :q