git.iko.soy/Idris-dev
on master help sign in
Add letbind to Elab reflection
29e29c2David Raymond Christiansen
libs/prelude/Language/Reflection/Elab.idr+9−1
compare with master
unifiedsplit
@@ -134,7 +134,7 @@ data Elab : Type -> Type where
134 prim__Forall : TTName -> Raw -> Elab ()
134 prim__Forall : TTName -> Raw -> Elab ()
135 prim__PatVar : TTName -> Elab ()
135 prim__PatVar : TTName -> Elab ()
136 prim__PatBind : TTName -> Elab ()
136 prim__PatBind : TTName -> Elab ()
137− -- TODO: letbind
137+ prim__LetBind : TTName -> Raw -> Raw -> Elab ()
138
138
139 prim__Compute : Elab ()
139 prim__Compute : Elab ()
140 prim__Normalise : (List (TTName, Binder TT)) -> TT -> Elab TT
140 prim__Normalise : (List (TTName, Binder TT)) -> TT -> Elab TT
@@ -348,6 +348,14 @@ namespace Tactics
348 patbind : TTName -> Elab ()
348 patbind : TTName -> Elab ()
349 patbind n = prim__PatBind n
349 patbind n = prim__PatBind n
350
350
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+
351 ||| Normalise the goal.
359 ||| Normalise the goal.
352 compute : Elab ()
360 compute : Elab ()
353 compute = prim__Compute
361 compute = prim__Compute
src/Idris/Elab/Term.hs+6
@@ -1908,6 +1908,12 @@ runElabAction ist fc env tm ns = do tm' <- eval tm
1908 = do n' <- reifyTTName n
1908 = do n' <- reifyTTName n
1909 patbind n'
1909 patbind n'
1910 returnUnit
1910 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
1911 | n == tacN "prim__Compute", [] <- args
1917 | n == tacN "prim__Compute", [] <- args
1912 = do compute ; returnUnit
1918 = do compute ; returnUnit
1913 | n == tacN "prim__Normalise", [env, tm] <- args
1919 | n == tacN "prim__Normalise", [env, tm] <- args