git.iko.soy/Idris-dev
on master help sign in
Add WHNF to Elab reflection
commit0fed832f4d952af42d010a646d198802eb1a09b7 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateSat 25 Jul 2015, 13:52 (11 years ago) parent3c5327f
2 files changed+9−7
compare with master
unifiedsplit
libs/prelude/Language/Reflection/Elab.idr+4−5 src/Idris/Elab/Term.hs+5−2
libs/prelude/Language/Reflection/Elab.idr+4−5
@@ -134,7 +134,7 @@ data Elab : Type -> Type where
134134
135135 prim__Compute : Elab ()
136136 prim__Normalise : (List (TTName, Binder TT)) -> TT -> Elab TT
137− prim__Whnf : (List (TTName, Binder TT)) -> TT -> Elab TT
137+ prim__Whnf : TT -> Elab TT
138138
139139 prim__DeclareType : TyDecl -> Elab ()
140140 prim__DefineFunction : FunDefn -> Elab ()
@@ -343,12 +343,11 @@ namespace Tactics
343343 normalise : (env : List (TTName, Binder TT)) -> (term : TT) -> Elab TT
344344 normalise env term = prim__Normalise env term
345345
346− ||| Reduce a term to weak-head normal form
346+ ||| Reduce a closed term to weak-head normal form
347347 |||
348− ||| @ env the environment in which to compute (get one of these from `getEnv`)
349348 ||| @ term the term to reduce
350− whnf : (env : List (TTName, Binder TT)) -> (term : TT) -> Elab TT
351− whnf env term = prim__Whnf env term
349+ whnf : (term : TT) -> Elab TT
350+ whnf term = prim__Whnf term
352351
353352 ||| Find the source context for the elaboration script
354353 getSourceLocation : Elab SourceLocation
src/Idris/Elab/Term.hs+5−2
@@ -17,6 +17,7 @@ import Idris.Core.Evaluate
1717import Idris.Core.Unify
1818import Idris.Core.ProofTerm (getProofTerm)
1919import Idris.Core.Typecheck (check, recheck, converts, isType)
20+import Idris.Core.WHNF (whnf)
2021import Idris.Coverage (buildSCG, checkDeclTotality, genClauses, recoverableCoverage, validCoverageCase)
2122import Idris.ErrReverse (errReverse)
2223import Idris.ElabQuasiquote (extractUnquotes)
@@ -2086,8 +2087,10 @@ runElabAction ist fc env tm ns = do tm' <- eval tm
20862087 ctxt <- get_context
20872088 let out = normaliseAll ctxt env' (finalise tm')
20882089 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
2090+ | n == tacN "prim__Whnf", [tm] <- args
2091+ = do tm' <- reifyTT tm
2092+ ctxt <- get_context
2093+ fmap fst . checkClosed . reflect $ whnf ctxt tm'
20912094 | n == tacN "prim__DeclareType", [decl] <- args
20922095 = do (RDeclare n args res) <- reifyTyDecl decl
20932096 ctxt <- get_context