@@ -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,49 +183,16 @@ 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
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] =
193+syntax "quoteGoal" {x} "in" [expr] = %runElab (quoteGoalImpl (\x => expr))
225− let z = %runElab quoteGoalImpl
194+
228−--syntax "tactic" [expr] = %runElab (quoteGoalImpl expr)
195+syntax "tactic" [expr] = %runElab (quoteGoalImpl expr)
@@ -264,19 +231,16 @@ covering
264trivial : (goal : Term) -> Term
231trivial : (goal : Term) -> Term
265trivial = perhaps . trivial'
232trivial = perhaps . trivial'
267−gargle : Nat -> Nat -> Term
268−gargle = quoteGoal x in \a, b => x
270foo : (Nat, (), Nat, Either (() -> ()) Void)
234foo : (Nat, (), Nat, Either (() -> ()) Void)
271−--foo = quoteGoal x in trivial x
235+foo = quoteGoal x in trivial x
273bar : (Nat, (), Either Void Nat, Nat -> ())
237bar : (Nat, (), Either Void Nat, Nat -> ())
274−--bar = tactic trivial
238+bar = tactic trivial
276-- When checking right hand side of baz:
240-- When checking right hand side of baz:
277-- PROOF SEARCH FAILURE is not defined.
241-- PROOF SEARCH FAILURE is not defined.
278−--baz : (Nat, Void)
242+baz : (Nat, Void)
279−--baz = tactic trivial
243+baz = tactic trivial
281-- Local Variables:
245-- Local Variables:
282-- idris-load-packages: ("pruviloj")
246-- idris-load-packages: ("pruviloj")