@@ -1,4 +1,4 @@
1− ||| Implement an Agda-style reflection system as a DSL inside of
1+||| Implement an Agda-style reflection system as a DSL inside of
22||| Idris's reflected elaboration. Requires handling type class
33||| resolution and implicit arguments - some of the same features as
44||| the Idris elaborator itself.
@@ -183,49 +183,16 @@ covering
183183spliceTerm : Term -> Elab ()
184184spliceTerm = spliceTerm' []
185185
186+||| Lift an Agda-style tactic into an Idris-style tactic
187+covering
188+quoteGoalImpl : (Term -> Term) -> Elab ()
189+quoteGoalImpl f = do compute
190+ g <- goalType >>= quoteTerm
191+ spliceTerm (f g)
186192
187−mutual
188− instance Quotable Plicity Raw where
189− quotedTy = `(Plicity)
190− quote Explicit = `(Explicit)
191− quote Implicit = `(Implicit)
192− quote Constraint = `(Constraint)
193−
194− instance Quotable a Raw => Quotable (Arg a) Raw where
195− quotedTy = `(Arg ~(quotedTy {a=a}))
196− quote (MkArg plicity argValue) = `(MkArg {a=~(quotedTy {a=a})} ~(quote plicity) ~(quote argValue) )
197−
198− instance Quotable Term Raw where
199− quotedTy = `(Term)
200−
201− quote (Var k xs) = `(Var ~(quote k) ~(assert_total $ quote xs))
202− quote (Ctor n xs) = `(Ctor ~(quote n) ~(assert_total $ quote xs))
203− quote (TyCtor n xs) = `(TyCtor ~(quote n) ~(assert_total $ quote xs))
204− quote (Def n xs) = `(Def ~(quote n) ~(assert_total $ quote xs))
205− quote (Lam x) = `(Lam ~(quote x) : Term)
206− quote (Pi x y) = `(Pi ~(quote x) ~(quote y) : Term)
207− quote (Constant c) = `(Constant ~(quote c) : Term)
208− quote Ty = `(Ty)
209−
210−-- ||| Lift an Agda-style tactic into an Idris-style tactic
211−-- covering
212−-- quoteGoalImpl : TTName -> Elab ()
213−-- quoteGoalImpl f = do compute
214−-- g <- goalType >>= quoteTerm
215−-- spliceTerm (f g)
216−
217−partial
218−quoteGoalImpl : Elab ()
219−quoteGoalImpl =
220− do g <- goalType >>= quoteTerm
221− fill (quote g)
222− solve
223−
224−syntax "quoteGoal" {x} "in" [expr] =
225− let z = %runElab quoteGoalImpl
226− in (\x => expr) z
227−
228−--syntax "tactic" [expr] = %runElab (quoteGoalImpl expr)
193+syntax "quoteGoal" {x} "in" [expr] = %runElab (quoteGoalImpl (\x => expr))
194+
195+syntax "tactic" [expr] = %runElab (quoteGoalImpl expr)
229196
230197
231198
@@ -264,19 +231,16 @@ covering
264231trivial : (goal : Term) -> Term
265232trivial = perhaps . trivial'
266233
267−gargle : Nat -> Nat -> Term
268−gargle = quoteGoal x in \a, b => x
269−
270234foo : (Nat, (), Nat, Either (() -> ()) Void)
271−--foo = quoteGoal x in trivial x
235+foo = quoteGoal x in trivial x
272236
273237bar : (Nat, (), Either Void Nat, Nat -> ())
274−--bar = tactic trivial
238+bar = tactic trivial
275239
276240-- When checking right hand side of baz:
277241-- PROOF SEARCH FAILURE is not defined.
278−--baz : (Nat, Void)
279−--baz = tactic trivial
242+baz : (Nat, Void)
243+baz = tactic trivial
280244
281245-- Local Variables:
282246-- idris-load-packages: ("pruviloj")