@@ -2,6 +2,10 @@
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.
5+|||
6+||| Since this test was put together, Agda has adopted an Idris-style
7+||| elaborator reflection mechanism. The module name is preserved for
8+||| historical interest.
59module AgdaStyleReflection
610
711
@@ -11,6 +15,7 @@ import Pruviloj
1115%default total
1216
1317
18+
1419||| Function arguments as provided at the application site
1520record Arg a where
1621 constructor MkArg
@@ -20,6 +25,10 @@ record Arg a where
2025implementation Functor Arg where
2126 map f (MkArg plic x) = MkArg plic (f x)
2227
28+implementation Show a => Show (Arg a) where
29+ showPrec d (MkArg plic x) = showCon d "MkArg" $ showArg plic ++ showArg x
30+
31+
2332||| Reflected terms, in the tradition of Agda's reflection library
2433data Term
2534 = Var Nat (List (Arg Term))
@@ -37,6 +46,41 @@ unApply tm = unApply' tm []
3746 unApply' (RApp f x) xs = unApply' f (x::xs)
3847 unApply' notApp xs = (notApp, xs)
3948
49+
50+implementation Quotable Plicity Raw where
51+ quotedTy = `(Plicity)
52+ quote Explicit = `(Explicit)
53+ quote Implicit = `(Implicit)
54+ quote Constraint = `(Constraint)
55+
56+implementation (Quotable a Raw) => Quotable (Arg a) Raw where
57+ quotedTy = `(Arg ~(quotedTy {a=a}))
58+ quote (MkArg plicity argValue) =
59+ `(MkArg {a=~(quotedTy {a=a})} ~(quote plicity) ~(quote argValue))
60+
61+
62+implementation Quotable Term Raw where
63+ quotedTy = `(Term)
64+ quote (Var k xs) = `(AgdaStyleReflection.Var ~(quote k) ~(assert_total $ quote xs))
65+ quote (Ctor n xs) = `(AgdaStyleReflection.Ctor ~(quote n) ~(assert_total $ quote xs))
66+ quote (TyCtor n xs) = `(AgdaStyleReflection.TyCtor ~(quote n) ~(assert_total $ quote xs))
67+ quote (Def n xs) = `(Def ~(quote n) ~(assert_total $ quote xs))
68+ quote (Lam x) = `(AgdaStyleReflection.Lam ~(quote x))
69+ quote (Pi x y) = `(AgdaStyleReflection.Pi ~(quote x) ~(quote y))
70+ quote (Constant c) = `(Constant ~(quote c))
71+ quote Ty = `(Ty)
72+
73+
74+implementation Show Term where
75+ showPrec d (Var k xs) = showCon d "Var" $ showArg k ++ showArg xs
76+ showPrec d (Ctor n xs) = showCon d "Ctor" $ showArg n ++ showArg xs
77+ showPrec d (TyCtor n xs) = showCon d "TyCtor" $ showArg n ++ showArg xs
78+ showPrec d (Def n xs) = showCon d "Def" $ showArg n ++ showArg xs
79+ showPrec d (Lam x) = showCon d "Lam" $ showArg x
80+ showPrec d (Pi x y) = showCon d "Pi" $ showArg x ++ showArg y
81+ showPrec d (Constant c) = showCon d "Constant" $ showArg c
82+ showPrec d Ty = "Ty"
83+
4084||| Quote a reflected Idris term to a Term in some induced local context
4185covering
4286quoteTerm' : List TTName -> Raw -> Elab Term
@@ -183,16 +227,39 @@ covering
183227spliceTerm : Term -> Elab ()
184228spliceTerm = spliceTerm' []
185229
186−||| Lift an Agda-style tactic into an Idris-style tactic
230+syntax "splice" [tm] = %runElab (spliceTerm tm)
231+
187232covering
188−quoteGoalImpl : (Term -> Term) -> Elab ()
189−quoteGoalImpl f = do compute
190− g <- goalType >>= quoteTerm
191− spliceTerm (f g)
233+quoteGoalImpl : TTName -> Elab ()
234+quoteGoalImpl f =
235+ do g <- goalType >>= quoteTerm
236+ fill (RApp (Var f) (quote g))
237+ solve
238+
239+syntax "quoteGoal" {g} "in" [e] =
240+ let f = \g : Term => e in %runElab (quoteGoalImpl `{f})
241+
242+
243+-- Note: this definition would seem to be the right thing, but it's not:
244+-- syntax "tactic" [tac] = quoteGoal g in splice tac g
245+-- This is because it would make
246+-- tactic foo
247+-- expand to
248+-- let f = \g : Term => %runElab (spliceTerm (tac g))
249+-- in %runElab (quoteGoalImpl `{f})
250+-- which confuses the meta-level at which the body of the lambda should be
251+-- run. It must be sequenced into the same monadic action as quoting the goal,
252+-- yielding the following implementation:
253+
254+covering
255+tacticImpl : (tac : Term -> Term) -> Elab ()
256+tacticImpl tac = do g <- goalType >>= quoteTerm
257+ AgdaStyleReflection.spliceTerm (tac g)
258+
259+syntax "tactic" [tacticCode] =
260+ %runElab (tacticImpl tacticCode)
192261
193−syntax "quoteGoal" {x} "in" [expr] = %runElab (quoteGoalImpl (\x => expr))
194262
195−syntax "tactic" [expr] = %runElab (quoteGoalImpl expr)
196263
197264
198265
@@ -231,12 +298,30 @@ covering
231298trivial : (goal : Term) -> Term
232299trivial = perhaps . trivial'
233300
234−foo : (Nat, (), Nat, Either (() -> ()) Void)
235−foo = quoteGoal x in trivial x
301+-- DOESN'T WORK because reflection operations are not pure - they have
302+-- side effects in the elaborator! Also due to metalevel confusion in
303+-- underlying syntax
304+--foo : (Nat, (), Either Void Nat, Nat -> ())
305+--foo = quoteGoal g in splice (trivial g)
236306
307+
308+-- WORKS because "tactic" takes care of the sequencing of operations
237309bar : (Nat, (), Either Void Nat, Nat -> ())
238310bar = tactic trivial
239311
312+someTerm : Term
313+someTerm = quoteGoal g in g
314+
315+ok : AgdaStyleReflection.someTerm = TyCtor (NS (UN "Term") ["AgdaStyleReflection"]) []
316+ok = Refl
317+
318+-- assert_total needed due to partial Show implementations
319+stringly : String -> String
320+stringly = quoteGoal g in \x => assert_total $ show g
321+
322+ok2 : stringly "fnord" = "Pi (Constant StrType) (Constant StrType)"
323+ok2 = Refl
324+
240325-- When checking right hand side of baz:
241326-- PROOF SEARCH FAILURE is not defined.
242327baz : (Nat, Void)