git.iko.soy/Idris-dev
on master help sign in
Add compute to Elab
d1e4752David Raymond Christiansen
libs/prelude/Language/Reflection/Elab.idr+4
compare with master
unifiedsplit
@@ -70,6 +70,8 @@ data Elab : Type -> Type where
70 prim__PatVar : TTName -> Elab ()
70 prim__PatVar : TTName -> Elab ()
71 prim__PatBind : TTName -> Elab ()
71 prim__PatBind : TTName -> Elab ()
72
72
73+ prim__Compute : Elab ()
74+
73 prim__DeclareType : TyDecl -> Elab ()
75 prim__DeclareType : TyDecl -> Elab ()
74 prim__DefineFunction : FunDefn -> Elab ()
76 prim__DefineFunction : FunDefn -> Elab ()
75
77
@@ -180,6 +182,8 @@ patvar n = prim__PatVar n
180patbind : TTName -> Elab ()
182patbind : TTName -> Elab ()
181patbind n = prim__PatBind n
183patbind n = prim__PatBind n
182
184
185+compute : Elab ()
186+compute = prim__Compute
183
187
184||| Find out the present source context for the tactic script
188||| Find out the present source context for the tactic script
185getSourceLocation : Elab SourceLocation
189getSourceLocation : Elab SourceLocation
src/Idris/Elab/Term.hs+2
@@ -1803,6 +1803,8 @@ runTactical fc env tm = do tm' <- eval tm
1803 = do n' <- reifyTTName n
1803 = do n' <- reifyTTName n
1804 patbind n'
1804 patbind n'
1805 returnUnit
1805 returnUnit
1806+ | n == tacN "prim__Compute", [] <- args
1807+ = do compute ; returnUnit
1806 | n == tacN "prim__DeclareType", [decl] <- args
1808 | n == tacN "prim__DeclareType", [decl] <- args
1807 = do (RDeclare n args res) <- reifyTyDecl decl
1809 = do (RDeclare n args res) <- reifyTyDecl decl
1808 ctxt <- get_context
1810 ctxt <- get_context