git.iko.soy/Idris-dev
on master help sign in
Add WHNF to Elab reflection
0fed832David Raymond Christiansen
libs/prelude/Language/Reflection/Elab.idr+4−5
compare with master
unifiedsplit
@@ -134,7 +134,7 @@ data Elab : Type -> Type where
134
134
135 prim__Compute : Elab ()
135 prim__Compute : Elab ()
136 prim__Normalise : (List (TTName, Binder TT)) -> TT -> Elab TT
136 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
138
138
139 prim__DeclareType : TyDecl -> Elab ()
139 prim__DeclareType : TyDecl -> Elab ()
140 prim__DefineFunction : FunDefn -> Elab ()
140 prim__DefineFunction : FunDefn -> Elab ()
@@ -343,12 +343,11 @@ namespace Tactics
343 normalise : (env : List (TTName, Binder TT)) -> (term : TT) -> Elab TT
343 normalise : (env : List (TTName, Binder TT)) -> (term : TT) -> Elab TT
344 normalise env term = prim__Normalise env term
344 normalise env term = prim__Normalise env term
345
345
346− ||| Reduce a term to weak-head normal form
346+ ||| Reduce a closed term to weak-head normal form
347 |||
347 |||
348− ||| @ env the environment in which to compute (get one of these from `getEnv`)
349 ||| @ term the term to reduce
348 ||| @ term the term to reduce
350− whnf : (env : List (TTName, Binder TT)) -> (term : TT) -> Elab TT
349+ whnf : (term : TT) -> Elab TT
351− whnf env term = prim__Whnf env term
350+ whnf term = prim__Whnf term
352
351
353 ||| Find the source context for the elaboration script
352 ||| Find the source context for the elaboration script
354 getSourceLocation : Elab SourceLocation
353 getSourceLocation : Elab SourceLocation
src/Idris/Elab/Term.hs+5−2
@@ -17,6 +17,7 @@ import Idris.Core.Evaluate
17import Idris.Core.Unify
17import Idris.Core.Unify
18import Idris.Core.ProofTerm (getProofTerm)
18import Idris.Core.ProofTerm (getProofTerm)
19import Idris.Core.Typecheck (check, recheck, converts, isType)
19import Idris.Core.Typecheck (check, recheck, converts, isType)
20+import Idris.Core.WHNF (whnf)
20import Idris.Coverage (buildSCG, checkDeclTotality, genClauses, recoverableCoverage, validCoverageCase)
21import Idris.Coverage (buildSCG, checkDeclTotality, genClauses, recoverableCoverage, validCoverageCase)
21import Idris.ErrReverse (errReverse)
22import Idris.ErrReverse (errReverse)
22import Idris.ElabQuasiquote (extractUnquotes)
23import Idris.ElabQuasiquote (extractUnquotes)
@@ -2086,8 +2087,10 @@ runElabAction ist fc env tm ns = do tm' <- eval tm
2086 ctxt <- get_context
2087 ctxt <- get_context
2087 let out = normaliseAll ctxt env' (finalise tm')
2088 let out = normaliseAll ctxt env' (finalise tm')
2088 fmap fst . checkClosed $ reflect out
2089 fmap fst . checkClosed $ reflect out
2089− | n == tacN "prim__Whnf", [env, tm] <- args
2090+ | n == tacN "prim__Whnf", [tm] <- args
2090− = undefined -- TODO: merge Edwin's whnf from master, then call here
2091+ = do tm' <- reifyTT tm
2092+ ctxt <- get_context
2093+ fmap fst . checkClosed . reflect $ whnf ctxt tm'
2091 | n == tacN "prim__DeclareType", [decl] <- args
2094 | n == tacN "prim__DeclareType", [decl] <- args
2092 = do (RDeclare n args res) <- reifyTyDecl decl
2095 = do (RDeclare n args res) <- reifyTyDecl decl
2093 ctxt <- get_context
2096 ctxt <- get_context