git.iko.soy/Idris-dev
on master help sign in
Let Elab scripts run the type checker
commit0689f2bc7327024dd9814276e58e7e678e9d1ade authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateFri 22 May 2015, 17:29 (11 years ago) parent5a366ac
2 files changed+14
compare with master
unifiedsplit
libs/prelude/Language/Reflection/Elab.idr+6 src/Idris/Elab/Term.hs+8
libs/prelude/Language/Reflection/Elab.idr+6
@@ -85,6 +85,8 @@ data Elab : Type -> Type where
8585 prim__LookupTy : TTName -> Elab (List (TTName, NameType, TT))
8686 prim__LookupDatatype : TTName -> Elab (List Datatype)
8787
88+ prim__Check : Raw -> Elab (TT, TT)
89+
8890 prim__SourceLocation : Elab SourceLocation
8991
9092 prim__Forget : TT -> Elab Raw
@@ -186,6 +188,10 @@ namespace Tactics
186188 [] => fail [TextPart "No datatype named", NamePart n]
187189 xs => fail [TextPart "More than one datatype named", NamePart n]
188190
191+ ||| Attempt to type-check a term, getting back itself and its type
192+ check : (tm : Raw) -> Elab (TT, TT)
193+ check tm = prim__Check tm
194+
189195 ||| Convert a type-annotated reflected term to its untyped
190196 ||| equivalent
191197 forgetTypes : TT -> Elab Raw
src/Idris/Elab/Term.hs+8
@@ -1843,6 +1843,14 @@ runTactical ist fc env tm = do tm' <- eval tm
18431843 ty' <- reifyRaw ty
18441844 claim n' ty'
18451845 returnUnit
1846+ | n == tacN "prim__Check", [raw] <- args
1847+ = do raw' <- reifyRaw =<< eval raw
1848+ ctxt <- get_context
1849+ env <- get_env
1850+ (tm, ty) <- lift $ check ctxt env raw'
1851+ fmap fst . get_type_val $
1852+ rawPair (Var (reflm "TT"), Var (reflm "TT"))
1853+ (reflect tm, reflect ty)
18461854 | n == tacN "prim__Forget", [tt] <- args
18471855 = do tt' <- reifyTT tt
18481856 fmap fst . get_type_val . reflectRaw $ forget tt'