git.iko.soy/Idris-dev
on master help sign in
Add letbind to Elab reflection
commit29e29c20bf23ac055665e6fb233683cceaaea1bb authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateTue 25 Aug 2015, 12:40 (11 years ago) parentce764bf
2 files changed+15−1
compare with master
unifiedsplit
libs/prelude/Language/Reflection/Elab.idr+9−1 src/Idris/Elab/Term.hs+6
libs/prelude/Language/Reflection/Elab.idr+9−1
@@ -134,7 +134,7 @@ data Elab : Type -> Type where
134134 prim__Forall : TTName -> Raw -> Elab ()
135135 prim__PatVar : TTName -> Elab ()
136136 prim__PatBind : TTName -> Elab ()
137− -- TODO: letbind
137+ prim__LetBind : TTName -> Raw -> Raw -> Elab ()
138138
139139 prim__Compute : Elab ()
140140 prim__Normalise : (List (TTName, Binder TT)) -> TT -> Elab TT
@@ -348,6 +348,14 @@ namespace Tactics
348348 patbind : TTName -> Elab ()
349349 patbind n = prim__PatBind n
350350
351+ ||| Introduce a new let binding
352+ |||
353+ ||| @ n the name to let bind
354+ ||| @ ty the type of the term to be let-bound
355+ ||| @ tm the term to be bound
356+ letbind : (n : TTName) -> (ty, tm : Raw) -> Elab ()
357+ letbind n ty tm = prim__LetBind n ty tm
358+
351359 ||| Normalise the goal.
352360 compute : Elab ()
353361 compute = prim__Compute
src/Idris/Elab/Term.hs+6
@@ -1908,6 +1908,12 @@ runElabAction ist fc env tm ns = do tm' <- eval tm
19081908 = do n' <- reifyTTName n
19091909 patbind n'
19101910 returnUnit
1911+ | n == tacN "prim__LetBind", [n, ty, tm] <- args
1912+ = do n' <- reifyTTName n
1913+ ty' <- reifyRaw ty
1914+ tm' <- reifyRaw tm
1915+ letbind n' ty' tm'
1916+ returnUnit
19111917 | n == tacN "prim__Compute", [] <- args
19121918 = do compute ; returnUnit
19131919 | n == tacN "prim__Normalise", [env, tm] <- args