git.iko.soy/Idris-dev
on master help sign in
Evaluator access in Elab scripts
d54064fDavid Raymond Christiansen
libs/prelude/Language/Reflection/Elab.idr+17
compare with master
unifiedsplit
@@ -130,8 +130,11 @@ data Elab : Type -> Type where
130 prim__Forall : TTName -> Raw -> Elab ()
130 prim__Forall : TTName -> Raw -> Elab ()
131 prim__PatVar : TTName -> Elab ()
131 prim__PatVar : TTName -> Elab ()
132 prim__PatBind : TTName -> Elab ()
132 prim__PatBind : TTName -> Elab ()
133+ -- TODO: letbind
133
134
134 prim__Compute : Elab ()
135 prim__Compute : Elab ()
136+ prim__Normalise : (List (TTName, Binder TT)) -> TT -> Elab TT
137+ prim__Whnf : (List (TTName, Binder TT)) -> TT -> Elab TT
135
138
136 prim__DeclareType : TyDecl -> Elab ()
139 prim__DeclareType : TyDecl -> Elab ()
137 prim__DefineFunction : FunDefn -> Elab ()
140 prim__DefineFunction : FunDefn -> Elab ()
@@ -333,6 +336,20 @@ namespace Tactics
333 compute : Elab ()
336 compute : Elab ()
334 compute = prim__Compute
337 compute = prim__Compute
335
338
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+
336 ||| Find the source context for the elaboration script
353 ||| Find the source context for the elaboration script
337 getSourceLocation : Elab SourceLocation
354 getSourceLocation : Elab SourceLocation
338 getSourceLocation = prim__SourceLocation
355 getSourceLocation = prim__SourceLocation
src/Idris/Elab/Term.hs+8
@@ -2080,6 +2080,14 @@ runElabAction ist fc env tm ns = do tm' <- eval tm
2080 returnUnit
2080 returnUnit
2081 | n == tacN "prim__Compute", [] <- args
2081 | n == tacN "prim__Compute", [] <- args
2082 = do compute ; returnUnit
2082 = 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
2083 | n == tacN "prim__DeclareType", [decl] <- args
2091 | n == tacN "prim__DeclareType", [decl] <- args
2084 = do (RDeclare n args res) <- reifyTyDecl decl
2092 = do (RDeclare n args res) <- reifyTyDecl decl
2085 ctxt <- get_context
2093 ctxt <- get_context
src/Idris/Reflection.hs+3
@@ -801,6 +801,9 @@ reflectEnv = foldr consToEnvList emptyEnvList
801 emptyEnvList = raw_apply (Var (sNS (sUN "Nil") ["List", "Prelude"]))
801 emptyEnvList = raw_apply (Var (sNS (sUN "Nil") ["List", "Prelude"]))
802 [envTupleType]
802 [envTupleType]
803
803
804+reifyEnv :: Term -> ElabD Env
805+reifyEnv = reifyList (reifyPair reifyTTName (reifyTTBinder reifyTT (reflm "TT")))
806+
804-- | Reflect an error into the internal datatype of Idris -- TODO
807-- | Reflect an error into the internal datatype of Idris -- TODO
805rawBool :: Bool -> Raw
808rawBool :: Bool -> Raw
806rawBool True = Var (sNS (sUN "True") ["Bool", "Prelude"])
809rawBool True = Var (sNS (sUN "True") ["Bool", "Prelude"])