@@ -2,6 +2,10 @@
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.
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.
5module AgdaStyleReflection
9module AgdaStyleReflection
@@ -11,6 +15,7 @@ import Pruviloj
11%default total
15%default total
14||| Function arguments as provided at the application site
19||| Function arguments as provided at the application site
15record Arg a where
20record Arg a where
16 constructor MkArg
21 constructor MkArg
@@ -20,6 +25,10 @@ record Arg a where
20implementation Functor Arg where
25implementation Functor Arg where
21 map f (MkArg plic x) = MkArg plic (f x)
26 map f (MkArg plic x) = MkArg plic (f x)
28+implementation Show a => Show (Arg a) where
29+ showPrec d (MkArg plic x) = showCon d "MkArg" $ showArg plic ++ showArg x
23||| Reflected terms, in the tradition of Agda's reflection library
32||| Reflected terms, in the tradition of Agda's reflection library
25 = Var Nat (List (Arg Term))
34 = Var Nat (List (Arg Term))
@@ -37,6 +46,41 @@ unApply tm = unApply' tm []
37 unApply' (RApp f x) xs = unApply' f (x::xs)
46 unApply' (RApp f x) xs = unApply' f (x::xs)
38 unApply' notApp xs = (notApp, xs)
47 unApply' notApp xs = (notApp, xs)
50+implementation Quotable Plicity Raw where
51+ quotedTy = `(Plicity)
52+ quote Explicit = `(Explicit)
53+ quote Implicit = `(Implicit)
54+ quote Constraint = `(Constraint)
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))
62+implementation Quotable Term Raw where
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))
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
40||| Quote a reflected Idris term to a Term in some induced local context
84||| Quote a reflected Idris term to a Term in some induced local context
42quoteTerm' : List TTName -> Raw -> Elab Term
86quoteTerm' : List TTName -> Raw -> Elab Term
@@ -183,16 +227,39 @@ covering
183spliceTerm : Term -> Elab ()
227spliceTerm : Term -> Elab ()
184spliceTerm = spliceTerm' []
228spliceTerm = spliceTerm' []
186−||| Lift an Agda-style tactic into an Idris-style tactic
230+syntax "splice" [tm] = %runElab (spliceTerm tm)
188−quoteGoalImpl : (Term -> Term) -> Elab ()
233+quoteGoalImpl : TTName -> Elab ()
189−quoteGoalImpl f = do compute
234+quoteGoalImpl f =
235+ do g <- goalType >>= quoteTerm
236+ fill (RApp (Var f) (quote g))
239+syntax "quoteGoal" {g} "in" [e] =
240+ let f = \g : Term => e in %runElab (quoteGoalImpl `{f})
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
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:
255+tacticImpl : (tac : Term -> Term) -> Elab ()
190− g <- goalType >>= quoteTerm
256+tacticImpl tac = do g <- goalType >>= quoteTerm
191− spliceTerm (f g)
257+ AgdaStyleReflection.spliceTerm (tac g)
259+syntax "tactic" [tacticCode] =
260+ %runElab (tacticImpl tacticCode)
193−syntax "quoteGoal" {x} "in" [expr] = %runElab (quoteGoalImpl (\x => expr))
195−syntax "tactic" [expr] = %runElab (quoteGoalImpl expr)
@@ -231,12 +298,30 @@ covering
231trivial : (goal : Term) -> Term
298trivial : (goal : Term) -> Term
232trivial = perhaps . trivial'
299trivial = perhaps . trivial'
301+-- DOESN'T WORK because reflection operations are not pure - they have
302+-- side effects in the elaborator! Also due to metalevel confusion in
234−foo : (Nat, (), Nat, Either (() -> ()) Void)
304+--foo : (Nat, (), Either Void Nat, Nat -> ())
235−foo = quoteGoal x in trivial x
305+--foo = quoteGoal g in splice (trivial g)
308+-- WORKS because "tactic" takes care of the sequencing of operations
237bar : (Nat, (), Either Void Nat, Nat -> ())
309bar : (Nat, (), Either Void Nat, Nat -> ())
238bar = tactic trivial
310bar = tactic trivial
313+someTerm = quoteGoal g in g
315+ok : AgdaStyleReflection.someTerm = TyCtor (NS (UN "Term") ["AgdaStyleReflection"]) []
318+-- assert_total needed due to partial Show implementations
319+stringly : String -> String
320+stringly = quoteGoal g in \x => assert_total $ show g
322+ok2 : stringly "fnord" = "Pi (Constant StrType) (Constant StrType)"
240-- When checking right hand side of baz:
325-- When checking right hand side of baz:
241-- PROOF SEARCH FAILURE is not defined.
326-- PROOF SEARCH FAILURE is not defined.
242baz : (Nat, Void)
327baz : (Nat, Void)