@@ -0,0 +1,247 @@
1+||| Implement an Agda-style reflection system as a DSL inside of
2+||| Idris's reflected elaboration. Requires handling type class
3+||| resolution and implicit arguments - some of the same features as
4+||| the Idris elaborator itself.
5+module AgdaStyleReflection
6+
7+
8+import Language.Reflection.Utils
9+import Pruviloj
10+
11+%default total
12+
13+
14+||| Function arguments as provided at the application site
15+record Arg a where
16+ constructor MkArg
17+ plicity : Plicity
18+ argValue : a
19+
20+instance Functor Arg where
21+ map f (MkArg plic x) = MkArg plic (f x)
22+
23+||| Reflected terms, in the tradition of Agda's reflection library
24+data Term
25+ = Var Nat (List (Arg Term))
26+ | Ctor TTName (List (Arg Term))
27+ | TyCtor TTName (List (Arg Term))
28+ | Def TTName (List (Arg Term))
29+ | Lam Term
30+ | Pi Term Term
31+ | Constant Const
32+ | Ty
33+
34+unApply : Raw -> (Raw, List Raw)
35+unApply tm = unApply' tm []
36+ where unApply' : Raw -> List Raw -> (Raw, List Raw)
37+ unApply' (RApp f x) xs = unApply' f (x::xs)
38+ unApply' notApp xs = (notApp, xs)
39+
40+||| Quote a reflected Idris term to a Term in some induced local context
41+covering
42+quoteTerm' : List TTName -> Raw -> Elab Term
43+quoteTerm' env (Var n) =
44+ case findIndex (==n) env of
45+ Just i => return (Var i [])
46+ Nothing =>
47+ case findIndex (\(n', _) => n == n') !getEnv of
48+ Just i => return (Var i [])
49+ Nothing => do [(n', nt, ty)] <- lookupTy n
50+ | [] => fail [TextPart "No such variable", NamePart n]
51+ | vs => fail ([TextPart "Can't disambiguate"] ++
52+ map (NamePart . fst) vs)
53+ case nt of
54+ Bound => fail [TextPart "Bound variable not found"]
55+ Ref => pure $ Def n' []
56+ DCon _ _ => pure $ Ctor n' []
57+ TCon _ _ => pure $ TyCtor n' []
58+quoteTerm' env (RBind n (Lam ty) tm) = Lam <$> quoteTerm' (n::env) tm
59+quoteTerm' env (RBind n (Pi ty kind) tm) = [| Pi (quoteTerm' env ty)
60+ (quoteTerm' (n::env) tm) |]
61+quoteTerm' env (RBind n (Let ty val) tm) = fail [TextPart "can't quote let"]
62+quoteTerm' env (RBind n (Hole ty) tm) = fail [TextPart "can't quote hole"]
63+quoteTerm' env (RBind n (GHole ty) tm) = fail [TextPart "can't quote deferred hole"]
64+quoteTerm' env (RBind n (Guess ty val) tm) = fail [TextPart "can't quote guess"]
65+quoteTerm' env (RBind n (PVar ty) tm) = fail [TextPart "can't quote patvar"]
66+quoteTerm' env (RBind n (PVTy ty) tm) = fail [TextPart "can't quote pattern type"]
67+quoteTerm' env (RApp tm tm') =
68+ do let (f, args) = unApply (RApp tm tm')
69+ rawArgs <- traverse (quoteTerm' env) args
70+ case f of
71+ Var n => doApp n rawArgs
72+ tm => fail [RawPart tm, TextPart "not normalized first"]
73+
74+ where
75+ mkArgs : List Term -> List FunArg -> List (Arg Term)
76+ mkArgs [] _ = []
77+ mkArgs tms [] = map (MkArg Explicit) tms
78+ mkArgs (tm::tms) (ar::ars) = MkArg (plicity ar) tm :: mkArgs tms ars
79+
80+ doApp : TTName -> List Term -> Elab Term
81+ doApp fn xs =
82+ do (fn', nt, ty) <- lookupTyExact fn
83+ (_, args, res) <- lookupArgsExact fn'
84+ let rest = mkArgs xs args
85+ case nt of
86+ Bound => fail [TextPart "Bound variable illegal here"]
87+ Ref => pure $ Def fn' rest
88+ DCon _ _ => pure $ Ctor fn' rest
89+ TCon _ _ => pure $ TyCtor fn' rest
90+
91+quoteTerm' env RType = pure Ty
92+quoteTerm' env (RUType x) = fail [TextPart "Uniqueness not supported here"]
93+quoteTerm' env (RConstant c) = pure (Constant c)
94+
95+||| Quote a reflected Idris term to a Term
96+covering
97+quoteTerm : Raw -> Elab Term
98+quoteTerm = quoteTerm' []
99+
100+||| Attempt to resolve a de Bruijn index in a context
101+resolveVar : Nat -> Elab TTName
102+resolveVar k =
103+ do env <- getEnv
104+ getVar k (map fst env)
105+
106+ where getVar : Nat -> List TTName -> Elab TTName
107+ getVar _ [] = fail [TextPart "Variable out of scope"]
108+ getVar Z (n :: _ ) = return n -- NB assumes unique names!
109+ getVar (S k) (_ :: env) = getVar k env
110+
111+||| Prepare to apply a global by matching its argument plicities to
112+||| its argument list.
113+prepareApply : List FunArg -> List (Arg Term) -> Elab (List (Arg (Maybe Term)))
114+prepareApply [] tms = pure $ map (map Just) tms -- overapplied OK - it may return a function!
115+prepareApply ars [] = pure [] -- underapplied is ok too
116+prepareApply (MkFunArg _ _ Constraint _ :: ars) (MkArg Constraint tm :: tms) =
117+ [| (pure (MkArg Constraint (Just tm))) :: prepareApply ars tms |]
118+prepareApply (MkFunArg _ _ Constraint _ :: ars) (MkArg plic tm :: tms) =
119+ [| (pure (MkArg Constraint Nothing)) :: prepareApply ars (MkArg plic tm :: tms) |]
120+prepareApply (MkFunArg _ _ Implicit _ :: ars) (MkArg Implicit tm :: tms) =
121+ [| (pure (MkArg Implicit (Just tm))) :: prepareApply ars tms |]
122+prepareApply (MkFunArg _ _ Implicit _ :: ars) (MkArg plic tm :: tms) =
123+ [| (pure (MkArg Implicit Nothing)) :: prepareApply ars (MkArg plic tm :: tms) |]
124+prepareApply (MkFunArg _ _ Explicit _ :: ars) (MkArg Explicit tm :: tms) =
125+ [| (pure (MkArg Explicit (Just tm))) :: prepareApply ars tms |]
126+prepareApply (MkFunArg _ _ Explicit _ :: ars) (MkArg plic tm :: tms) =
127+ fail [TextPart "Expected explicit argument, got something else!"]
128+
129+||| Should this argument be solved by unification?
130+toSolve : Arg (Maybe Term) -> Bool
131+toSolve (MkArg Explicit _) = False
132+toSolve (MkArg _ (Just _)) = False
133+toSolve _ = True
134+
135+mutual
136+ covering
137+ applyGlobal : List TTName -> TTName -> List (Arg Term) -> Elab ()
138+ applyGlobal locals fn args =
139+ do (fn', argSpec, _) <- lookupArgsExact fn
140+ todo <- prepareApply argSpec args
141+ hs <- apply (Var fn') (map toSolve todo)
142+ solve
143+ for_ {b=()} (zip todo hs) $ \(MkArg p tm, h) =>
144+ case p of
145+ Constraint => ignore $ inHole h (resolveTC `{applyGlobal})
146+ _ => case tm of
147+ Nothing => skip
148+ Just arg => ignore $ inHole h $ spliceTerm' locals arg
149+
150+ covering
151+ spliceTerm' : List TTName -> Term -> Elab ()
152+ spliceTerm' locals (Var k xs) =
153+ do n <- resolveVar k
154+ -- local bindings can't have non-explicit args, so just do a normal application
155+ hs <- apply (Var n) (map (const True) xs)
156+ solve
157+ for_ {b = ()} (zip hs xs) $ \(h, MkArg _ x) =>
158+ ignore $ inHole h (spliceTerm' locals x)
159+ spliceTerm' locals (Ctor n xs) = applyGlobal locals n xs
160+ spliceTerm' locals (TyCtor n xs) = applyGlobal locals n xs
161+ spliceTerm' locals (Def n xs) = applyGlobal locals n xs
162+ spliceTerm' locals (Lam body) =
163+ do x <- gensym "x"
164+ attack
165+ intro x
166+ spliceTerm' (x::locals) body
167+ solve
168+ spliceTerm' locals (Pi ty body) =
169+ do arg <- gensym "arg"
170+ claim arg `(Type)
171+ x <- gensym "x"
172+ attack
173+ forall x (Var arg)
174+ focus arg; spliceTerm' locals ty
175+ spliceTerm' (x::locals) body
176+ solve
177+ spliceTerm' locals (Constant c) =
178+ do fill (quote c); solve
179+ spliceTerm' locals Ty =
180+ do fill `(Type); solve
181+
182+covering
183+spliceTerm : Term -> Elab ()
184+spliceTerm = spliceTerm' []
185+
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))
194+
195+syntax "tactic" [expr] = %runElab (quoteGoalImpl expr)
196+
197+
198+
199+
200+
201+||| A simple proof search tactic with failure
202+|||
203+||| @ goal the type to fill out with search
204+covering
205+trivial' : (goal : Term) -> Maybe Term
206+trivial' (TyCtor `{Nat} []) = pure $ Ctor `{Z} []
207+trivial' (TyCtor `{Unit} []) = pure $ Ctor `{MkUnit} []
208+trivial' (TyCtor `{Pair} [MkArg Explicit a, MkArg Explicit b]) =
209+ pure $
210+ Ctor `{MkPair}
211+ [ MkArg Explicit !(trivial' a)
212+ , MkArg Explicit !(trivial' b)
213+ ]
214+trivial' (TyCtor `{Either} [MkArg Explicit a, MkArg Explicit b]) =
215+ (left <$> trivial' a) <|> (right <$> trivial' b)
216+ where left : Term -> Term
217+ left x = Ctor `{Left} [MkArg Explicit x]
218+ right : Term -> Term
219+ right x = Ctor `{Right} [MkArg Explicit x]
220+trivial' (Pi _ body) = Lam <$> trivial' body
221+trivial' _ = empty
222+
223+||| Attempt proof search, or fake an error message if it fails.
224+perhaps : Maybe Term -> Term
225+perhaps = maybe (Ctor (UN "PROOF SEARCH FAILURE") []) id
226+
227+||| A simple proof search tactic
228+|||
229+||| @ goal the type to fill out with search
230+covering
231+trivial : (goal : Term) -> Term
232+trivial = perhaps . trivial'
233+
234+foo : (Nat, (), Nat, Either (() -> ()) Void)
235+foo = quoteGoal x in trivial x
236+
237+bar : (Nat, (), Either Void Nat, Nat -> ())
238+bar = tactic trivial
239+
240+-- When checking right hand side of baz:
241+-- PROOF SEARCH FAILURE is not defined.
242+baz : (Nat, Void)
243+baz = tactic trivial
244+
245+-- Local Variables:
246+-- idris-load-packages: ("pruviloj")
247+-- End: