Add support for reflecting ByReflection
commitd0edb70d4f95b72b9d94cf02ad5df7bc121bff07
authorDavid Raymond Christiansen <david@davidchristiansen.dk>
dateThu 6 Mar 2014, 21:42 (13 years ago)
parent202937d
libs/base/Language/Reflection.idr+2
@@ -180,6 +180,8 @@ data Tactic = Try Tactic Tactic
180180 -- ^ invoke the reflected rep. of another tactic
181181 | Reflect TT
182182 -- ^ turn a value into its reflected representation
183+ | ByReflection TT
184+ -- ^ use a %reflection function
183185 | Fill Raw
184186 -- ^ turn a raw value back into a term
185187 | Exact TT
src/Idris/ElabTerm.hs+2
@@ -1205,6 +1205,8 @@ reifyApp ist t [t']
12051205 | t == reflm "ApplyTactic" = liftM (ApplyTactic . delab ist) (reifyTT t')
12061206reifyApp ist t [t']
12071207 | t == reflm "Reflect" = liftM (Reflect . delab ist) (reifyTT t')
1208+reifyApp ist t [t']
1209+ | t == reflm "ByReflection" = liftM (ByReflection . delab ist) (reifyTT t')
12081210reifyApp _ t [t']
12091211 | t == reflm "Fill" = liftM (Fill . PQuote) (reifyRaw t')
12101212reifyApp ist t [t']