git.iko.soy/Idris-dev
on master help sign in
Add compute to Elab
commitd1e4752d06a819910d17c93ba9f91d40e6a94f39 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateThu 30 Apr 2015, 15:55 (11 years ago) parentf09605b
2 files changed+6
compare with master
unifiedsplit
libs/prelude/Language/Reflection/Elab.idr+4 src/Idris/Elab/Term.hs+2
libs/prelude/Language/Reflection/Elab.idr+4
@@ -70,6 +70,8 @@ data Elab : Type -> Type where
7070 prim__PatVar : TTName -> Elab ()
7171 prim__PatBind : TTName -> Elab ()
7272
73+ prim__Compute : Elab ()
74+
7375 prim__DeclareType : TyDecl -> Elab ()
7476 prim__DefineFunction : FunDefn -> Elab ()
7577
@@ -180,6 +182,8 @@ patvar n = prim__PatVar n
180182patbind : TTName -> Elab ()
181183patbind n = prim__PatBind n
182184
185+compute : Elab ()
186+compute = prim__Compute
183187
184188||| Find out the present source context for the tactic script
185189getSourceLocation : Elab SourceLocation
src/Idris/Elab/Term.hs+2
@@ -1803,6 +1803,8 @@ runTactical fc env tm = do tm' <- eval tm
18031803 = do n' <- reifyTTName n
18041804 patbind n'
18051805 returnUnit
1806+ | n == tacN "prim__Compute", [] <- args
1807+ = do compute ; returnUnit
18061808 | n == tacN "prim__DeclareType", [decl] <- args
18071809 = do (RDeclare n args res) <- reifyTyDecl decl
18081810 ctxt <- get_context