git.iko.soy/Idris-dev
on master help sign in
Add support for reflecting ByReflection
d0edb70David Raymond Christiansen
libs/base/Language/Reflection.idr+2
compare with master
unifiedsplit
@@ -180,6 +180,8 @@ data Tactic = Try Tactic Tactic
180 -- ^ invoke the reflected rep. of another tactic
180 -- ^ invoke the reflected rep. of another tactic
181 | Reflect TT
181 | Reflect TT
182 -- ^ turn a value into its reflected representation
182 -- ^ turn a value into its reflected representation
183+ | ByReflection TT
184+ -- ^ use a %reflection function
183 | Fill Raw
185 | Fill Raw
184 -- ^ turn a raw value back into a term
186 -- ^ turn a raw value back into a term
185 | Exact TT
187 | Exact TT
src/Idris/ElabTerm.hs+2
@@ -1205,6 +1205,8 @@ reifyApp ist t [t']
1205 | t == reflm "ApplyTactic" = liftM (ApplyTactic . delab ist) (reifyTT t')
1205 | t == reflm "ApplyTactic" = liftM (ApplyTactic . delab ist) (reifyTT t')
1206reifyApp ist t [t']
1206reifyApp ist t [t']
1207 | t == reflm "Reflect" = liftM (Reflect . delab ist) (reifyTT t')
1207 | t == reflm "Reflect" = liftM (Reflect . delab ist) (reifyTT t')
1208+reifyApp ist t [t']
1209+ | t == reflm "ByReflection" = liftM (ByReflection . delab ist) (reifyTT t')
1208reifyApp _ t [t']
1210reifyApp _ t [t']
1209 | t == reflm "Fill" = liftM (Fill . PQuote) (reifyRaw t')
1211 | t == reflm "Fill" = liftM (Fill . PQuote) (reifyRaw t')
1210reifyApp ist t [t']
1212reifyApp ist t [t']