@@ -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
2||| Idris's reflected elaboration. Requires handling type class
2||| Idris's reflected elaboration. Requires handling type class
3||| resolution and implicit arguments - some of the same features as
3||| resolution and implicit arguments - some of the same features as
4||| the Idris elaborator itself.
4||| the Idris elaborator itself.
@@ -183,16 +183,49 @@ covering
183spliceTerm : Term -> Elab ()
183spliceTerm : Term -> Elab ()
184spliceTerm = spliceTerm' []
184spliceTerm = spliceTerm' []
186−||| Lift an Agda-style tactic into an Idris-style tactic
188−quoteGoalImpl : (Term -> Term) -> Elab ()
189−quoteGoalImpl f = do compute
190− g <- goalType >>= quoteTerm
193−syntax "quoteGoal" {x} "in" [expr] = %runElab (quoteGoalImpl (\x => expr))
188+ instance Quotable Plicity Raw where
189+ quotedTy = `(Plicity)
190+ quote Explicit = `(Explicit)
191+ quote Implicit = `(Implicit)
192+ quote Constraint = `(Constraint)
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) )
198+ instance Quotable Term Raw where
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)
210+-- ||| Lift an Agda-style tactic into an Idris-style tactic
212+-- quoteGoalImpl : TTName -> Elab ()
213+-- quoteGoalImpl f = do compute
214+-- g <- goalType >>= quoteTerm
218+quoteGoalImpl : Elab ()
220+ do g <- goalType >>= quoteTerm
224+syntax "quoteGoal" {x} "in" [expr] =
225+ let z = %runElab quoteGoalImpl
195−syntax "tactic" [expr] = %runElab (quoteGoalImpl expr)
228+--syntax "tactic" [expr] = %runElab (quoteGoalImpl expr)
@@ -231,16 +264,19 @@ covering
231trivial : (goal : Term) -> Term
264trivial : (goal : Term) -> Term
232trivial = perhaps . trivial'
265trivial = perhaps . trivial'
267+gargle : Nat -> Nat -> Term
268+gargle = quoteGoal x in \a, b => x
234foo : (Nat, (), Nat, Either (() -> ()) Void)
270foo : (Nat, (), Nat, Either (() -> ()) Void)
235−foo = quoteGoal x in trivial x
271+--foo = quoteGoal x in trivial x
237bar : (Nat, (), Either Void Nat, Nat -> ())
273bar : (Nat, (), Either Void Nat, Nat -> ())
238−bar = tactic trivial
274+--bar = tactic trivial
240-- When checking right hand side of baz:
276-- When checking right hand side of baz:
241-- PROOF SEARCH FAILURE is not defined.
277-- PROOF SEARCH FAILURE is not defined.
242−baz : (Nat, Void)
278+--baz : (Nat, Void)
243−baz = tactic trivial
279+--baz = tactic trivial
245-- Local Variables:
281-- Local Variables:
246-- idris-load-packages: ("pruviloj")
282-- idris-load-packages: ("pruviloj")