git.iko.soy/Idris-dev
on master help sign in
Evaluator access in Elab scripts

Now, Elab scripts can access the evaluator.

commitd54064fb21babd6480ed22bbbed2af221697a830 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateSat 25 Jul 2015, 12:46 (11 years ago) parenta3db741
3 files changed+28
compare with master
unifiedsplit
libs/prelude/Language/Reflection/Elab.idr+17 src/Idris/Elab/Term.hs+8 src/Idris/Reflection.hs+3
libs/prelude/Language/Reflection/Elab.idr+17
@@ -130,8 +130,11 @@ data Elab : Type -> Type where
130130 prim__Forall : TTName -> Raw -> Elab ()
131131 prim__PatVar : TTName -> Elab ()
132132 prim__PatBind : TTName -> Elab ()
133+ -- TODO: letbind
133134
134135 prim__Compute : Elab ()
136+ prim__Normalise : (List (TTName, Binder TT)) -> TT -> Elab TT
137+ prim__Whnf : (List (TTName, Binder TT)) -> TT -> Elab TT
135138
136139 prim__DeclareType : TyDecl -> Elab ()
137140 prim__DefineFunction : FunDefn -> Elab ()
@@ -333,6 +336,20 @@ namespace Tactics
333336 compute : Elab ()
334337 compute = prim__Compute
335338
339+ ||| Normalise a term in some lexical environment
340+ |||
341+ ||| @ env the environment in which to compute (get one of these from `getEnv`)
342+ ||| @ term the term to normalise
343+ normalise : (env : List (TTName, Binder TT)) -> (term : TT) -> Elab TT
344+ normalise env term = prim__Normalise env term
345+
346+ ||| Reduce a term to weak-head normal form
347+ |||
348+ ||| @ env the environment in which to compute (get one of these from `getEnv`)
349+ ||| @ term the term to reduce
350+ whnf : (env : List (TTName, Binder TT)) -> (term : TT) -> Elab TT
351+ whnf env term = prim__Whnf env term
352+
336353 ||| Find the source context for the elaboration script
337354 getSourceLocation : Elab SourceLocation
338355 getSourceLocation = prim__SourceLocation
src/Idris/Elab/Term.hs+8
@@ -2080,6 +2080,14 @@ runElabAction ist fc env tm ns = do tm' <- eval tm
20802080 returnUnit
20812081 | n == tacN "prim__Compute", [] <- args
20822082 = do compute ; returnUnit
2083+ | n == tacN "prim__Normalise", [env, tm] <- args
2084+ = do env' <- reifyEnv env
2085+ tm' <- reifyTT tm
2086+ ctxt <- get_context
2087+ let out = normaliseAll ctxt env' (finalise tm')
2088+ fmap fst . checkClosed $ reflect out
2089+ | n == tacN "prim__Whnf", [env, tm] <- args
2090+ = undefined -- TODO: merge Edwin's whnf from master, then call here
20832091 | n == tacN "prim__DeclareType", [decl] <- args
20842092 = do (RDeclare n args res) <- reifyTyDecl decl
20852093 ctxt <- get_context
src/Idris/Reflection.hs+3
@@ -801,6 +801,9 @@ reflectEnv = foldr consToEnvList emptyEnvList
801801 emptyEnvList = raw_apply (Var (sNS (sUN "Nil") ["List", "Prelude"]))
802802 [envTupleType]
803803
804+reifyEnv :: Term -> ElabD Env
805+reifyEnv = reifyList (reifyPair reifyTTName (reifyTTBinder reifyTT (reflm "TT")))
806+
804807-- | Reflect an error into the internal datatype of Idris -- TODO
805808rawBool :: Bool -> Raw
806809rawBool True = Var (sNS (sUN "True") ["Bool", "Prelude"])