@@ -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,16 +183,49 @@ 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)
192−
193−syntax "quoteGoal" {x} "in" [expr] = %runElab (quoteGoalImpl (\x => expr))
194186
195−syntax "tactic" [expr] = %runElab (quoteGoalImpl expr)
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)
196229
197230
198231
@@ -231,16 +264,19 @@ covering
231264trivial : (goal : Term) -> Term
232265trivial = perhaps . trivial'
233266
267+gargle : Nat -> Nat -> Term
268+gargle = quoteGoal x in \a, b => x
269+
234270foo : (Nat, (), Nat, Either (() -> ()) Void)
235−foo = quoteGoal x in trivial x
271+--foo = quoteGoal x in trivial x
236272
237273bar : (Nat, (), Either Void Nat, Nat -> ())
238−bar = tactic trivial
274+--bar = tactic trivial
239275
240276-- When checking right hand side of baz:
241277-- PROOF SEARCH FAILURE is not defined.
242−baz : (Nat, Void)
243−baz = tactic trivial
278+--baz : (Nat, Void)
279+--baz = tactic trivial
244280
245281-- Local Variables:
246282-- idris-load-packages: ("pruviloj")