git.iko.soy/Idris-dev
on master help sign in
Let Elab scripts run the type checker
0689f2bDavid Raymond Christiansen
libs/prelude/Language/Reflection/Elab.idr+6
compare with master
unifiedsplit
@@ -85,6 +85,8 @@ data Elab : Type -> Type where
85 prim__LookupTy : TTName -> Elab (List (TTName, NameType, TT))
85 prim__LookupTy : TTName -> Elab (List (TTName, NameType, TT))
86 prim__LookupDatatype : TTName -> Elab (List Datatype)
86 prim__LookupDatatype : TTName -> Elab (List Datatype)
87
87
88+ prim__Check : Raw -> Elab (TT, TT)
89+
88 prim__SourceLocation : Elab SourceLocation
90 prim__SourceLocation : Elab SourceLocation
89
91
90 prim__Forget : TT -> Elab Raw
92 prim__Forget : TT -> Elab Raw
@@ -186,6 +188,10 @@ namespace Tactics
186 [] => fail [TextPart "No datatype named", NamePart n]
188 [] => fail [TextPart "No datatype named", NamePart n]
187 xs => fail [TextPart "More than one datatype named", NamePart n]
189 xs => fail [TextPart "More than one datatype named", NamePart n]
188
190
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+
189 ||| Convert a type-annotated reflected term to its untyped
195 ||| Convert a type-annotated reflected term to its untyped
190 ||| equivalent
196 ||| equivalent
191 forgetTypes : TT -> Elab Raw
197 forgetTypes : TT -> Elab Raw
src/Idris/Elab/Term.hs+8
@@ -1843,6 +1843,14 @@ runTactical ist fc env tm = do tm' <- eval tm
1843 ty' <- reifyRaw ty
1843 ty' <- reifyRaw ty
1844 claim n' ty'
1844 claim n' ty'
1845 returnUnit
1845 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)
1846 | n == tacN "prim__Forget", [tt] <- args
1854 | n == tacN "prim__Forget", [tt] <- args
1847 = do tt' <- reifyTT tt
1855 = do tt' <- reifyTT tt
1848 fmap fst . get_type_val . reflectRaw $ forget tt'
1856 fmap fst . get_type_val . reflectRaw $ forget tt'