@@ -1,3 +1,8 @@
1+||| Primitives and tactics for elaborator reflection.
2+|||
3+||| Elaborator reflection allows Idris code to control Idris's
4+||| built-in elaborator, and re-use features like the unifier, the
5+||| type checker, and the hole mechanism.
16module Language.Reflection.Elab
27
38import Builtins
@@ -8,31 +13,62 @@ import Prelude.Maybe
813import Prelude.Monad
914import Language.Reflection
1015
16+||| Arguments, with plicity.
1117data Arg : Type where
18+ ||| An explicit argument
1219 Explicit : TTName -> Raw -> Arg
20+
21+ ||| An implicit argument, to be solved by unification
1322 Implicit : TTName -> Raw -> Arg
23+
24+ ||| A type-class constraint argument, to be solved by type class
25+ ||| resolution
1426 Constraint : TTName -> Raw -> Arg
1527
28+||| A type declaration
1629data TyDecl : Type where
17− Declare : TTName -> List Arg -> Raw -> TyDecl
18−
30+ ||| A type declaration.
31+ |||
32+ ||| Each argument is in the scope of the names of previous
33+ ||| arguments, and the return type is in the scope of all the
34+ ||| argument names.
35+ |||
36+ ||| @ fn the name to be declared, fully-qualified
37+ ||| @ args the arguments to the function
38+ ||| @ ret the final return type
39+ Declare : (fn : TTName) -> (args : List Arg) -> (ret : Raw) -> TyDecl
40+
41+||| A single pattern-matching clause
1942data FunClause : Type where
2043 MkFunClause : (lhs, rhs : Raw) -> FunClause
2144 MkImpossibleClause : (lhs : Raw) -> FunClause
2245
46+||| A reflected function definition.
2347data FunDefn : Type where
2448 DefineFun : TTName -> List FunClause -> FunDefn
2549
50+||| An argument to a type constructor.
2651data TyConArg : Type where
52+ ||| Parameters are consistent across all constructors of the type
2753 Parameter : TTName -> Raw -> TyConArg
54+
55+ ||| Indices are allowed to vary across constructors
2856 Index : TTName -> Raw -> TyConArg
2957
58+||| A reflected datatype definition
3059data Datatype : Type where
60+ ||| A reflected datatype definition
61+ |||
62+ ||| @ familyName the name of the type constructor
63+ ||| @ tyConArgs the arguments to the type constructor
64+ ||| @ tyConRes the result of the type constructor
65+ ||| @ constrs the constructors, with their types
3166 MkDatatype : (familyName : TTName) ->
3267 (tyConArgs : List TyConArg) -> (tyConRes : Raw) ->
3368 (constrs : List (TTName, Raw)) ->
3469 Datatype
3570
71+||| A reflected elaboration script.
3672abstract
3773data Elab : Type -> Type where
3874 -- obligatory control stuff
@@ -74,7 +110,9 @@ data Elab : Type -> Type where
74110
75111 prim__DeclareType : TyDecl -> Elab ()
76112 prim__DefineFunction : FunDefn -> Elab ()
113+ prim__AddInstance : TTName -> TTName -> Elab ()
77114
115+ prim__ResolveTC : TTName -> Elab ()
78116 prim__RecursiveElab : Raw -> Elab () -> Elab (TT, TT)
79117
80118 prim__Debug : {a : Type} -> Maybe String -> Elab a
@@ -84,131 +122,210 @@ data Elab : Type -> Type where
84122-- Public API
85123-------------
86124%access public
125+namespace Tactics
126+ instance Functor Elab where
127+ map f t = prim__BindElab t (\x => prim__PureElab (f x))
128+
129+ instance Applicative Elab where
130+ pure x = prim__PureElab x
131+ f <*> x = prim__BindElab f $ \g =>
132+ prim__BindElab x $ \y =>
133+ prim__PureElab $ g y
134+
135+ ||| The Alternative instance on Elab represents left-biased error
136+ ||| handling. In other words, `t <|> t'` will run `t`, and if it
137+ ||| fails, roll back the elaboration state and run `t'`.
138+ instance Alternative Elab where
139+ empty = prim__Fail [TextPart "empty"]
140+ x <|> y = prim__Try x y
141+
142+ instance Monad Elab where
143+ x >>= f = prim__BindElab x f
144+
145+ ||| Halt elaboration with an error
146+ fail : List ErrorReportPart -> Elab a
147+ fail err = prim__Fail err
148+
149+ ||| Look up the lexical binding at the focused hole
150+ getEnv : Elab (List (TTName, Binder TT))
151+ getEnv = prim__Env
152+
153+ ||| Get the name and type of the focused hole
154+ getGoal : Elab (TTName, TT)
155+ getGoal = prim__Goal
156+
157+ ||| Get the hole queue, in order
158+ getHoles : Elab (List TTName)
159+ getHoles = prim__Holes
160+
161+ ||| If the current hole contains a guess, return it
162+ getGuess : Elab (Maybe TT)
163+ getGuess = prim__Guess
164+
165+ ||| Look up the types of every overloading of a name
166+ lookupTy : TTName -> Elab (List (TTName, NameType, TT))
167+ lookupTy n = prim__LookupTy n
168+
169+ ||| Get the type of a fully-qualified name
170+ lookupTyExact : TTName -> Elab (TTName, NameType, TT)
171+ lookupTyExact n = case !(lookupTy n) of
172+ [res] => return res
173+ [] => fail [NamePart n, TextPart "is not defined."]
174+ xs => fail [NamePart n, TextPart "is ambiguous."]
175+
176+ ||| Find the reflected representation of all datatypes whose names
177+ ||| are overloadings of some name
178+ lookupDatatype : TTName -> Elab (List Datatype)
179+ lookupDatatype n = prim__LookupDatatype n
180+
181+ ||| Find the reflected representation of a datatype, given its
182+ ||| fully-qualified name.
183+ lookupDatatypeExact : TTName -> Elab Datatype
184+ lookupDatatypeExact n = case !(lookupDatatype n) of
185+ [res] => return res
186+ [] => fail [TextPart "No datatype named", NamePart n]
187+ xs => fail [TextPart "More than one datatype named", NamePart n]
188+
189+ ||| Convert a type-annotated reflected term to its untyped
190+ ||| equivalent
191+ forgetTypes : TT -> Elab Raw
192+ forgetTypes tt = prim__Forget tt
193+
194+ ||| Generate a unique name based on some hint.
195+ |||
196+ ||| **NB**: the generated name is unique _for this run of the
197+ ||| elaborator_. Do not assume that they are globally unique.
198+ gensym : (hint : String) -> Elab TTName
199+ gensym hint = prim__Gensym hint
200+
201+ ||| Substitute a guess into a hole.
202+ solve : Elab ()
203+ solve = prim__Solve
204+
205+ ||| Place a term into a hole, unifying its type
206+ fill : Raw -> Elab ()
207+ fill tm = prim__Fill tm
208+
209+ ||| Fill with unification
210+ apply : Raw -> Elab ()
211+ apply tm = prim__Apply tm
212+
213+ ||| Move the focus to the specified hole
214+ |||
215+ ||| @ hole the hole to focus on
216+ focus : (hole : TTName) -> Elab ()
217+ focus hole = prim__Focus hole
218+
219+ ||| Send the currently-focused hole to the end of the hole queue and
220+ ||| focus on the next hole.
221+ unfocus : TTName -> Elab ()
222+ unfocus hole = prim__Unfocus hole
223+
224+ ||| Convert a hole to make it suitable for bindings.
225+ |||
226+ ||| The binding tactics require that a hole be directly under its
227+ ||| binding, or else the scopes of the generated terms won't make
228+ ||| sense. This tactic creates a new hole of the proper form, and
229+ ||| points the old hole at it.
230+ attack : Elab ()
231+ attack = prim__Attack
232+
233+ ||| Introduce a new hole with a specified name and type.
234+ |||
235+ ||| The new hole will be focused, and the previously-focused hole
236+ ||| will be immediately after it in the hole queue.
237+ claim : TTName -> Raw -> Elab ()
238+ claim n ty = prim__Claim n ty
239+
240+ ||| Introduce a lambda binding around the current hole and focus on
241+ ||| the body. Requires that the hole be in binding form (use
242+ ||| `attack`).
243+ |||
244+ ||| @ n the name to use for the argument, or `Nothing` to use the name
245+ ||| in the corresponding hole type (a dependent function)
246+ intro : (n : Maybe TTName) -> Elab ()
247+ intro n = prim__Intro n
248+
249+ ||| Introduce a dependent function type binding into the current hole,
250+ ||| and focus on the body.
251+ forall : TTName -> Raw -> Elab ()
252+ forall n ty = prim__Forall n ty
253+
254+ ||| Convert a hole into a pattern variable.
255+ patvar : TTName -> Elab ()
256+ patvar n = prim__PatVar n
257+
258+ ||| Introduce a new pattern binding.
259+ patbind : TTName -> Elab ()
260+ patbind n = prim__PatBind n
261+
262+ ||| Normalise the goal.
263+ compute : Elab ()
264+ compute = prim__Compute
265+
266+ ||| Find the source context for the elaboration script
267+ getSourceLocation : Elab SourceLocation
268+ getSourceLocation = prim__SourceLocation
269+
270+ ||| Attempt to solve the current goal with the source code location
271+ sourceLocation : Elab ()
272+ sourceLocation = do loc <- getSourceLocation
273+ fill (quote loc)
274+ solve
275+
276+ ||| Attempt to rewrite the goal using an equality.
277+ |||
278+ ||| The tactic searches the goal for applicable subterms, and
279+ ||| constructs a context for `replace` using them. In some cases,
280+ ||| this is not possible, and `replace` must be called manually with
281+ ||| an appropriate context.
282+ rewriteWith : Raw -> Elab ()
283+ rewriteWith rule = prim__Rewrite rule
284+
285+ ||| Add a type declaration to the global context.
286+ declareType : TyDecl -> Elab ()
287+ declareType decl = prim__DeclareType decl
288+
289+ ||| Define a function in the global context. The function must have
290+ ||| already been declared, either in ordinary Idris code or using
291+ ||| `declareType`.
292+ defineFunction : FunDefn -> Elab ()
293+ defineFunction defun = prim__DefineFunction defun
294+
295+ ||| Register a new instance for type class resolution
296+ |||
297+ ||| @ className the name of the class for which an instance is being registered
298+ ||| @ instName the name of the definition to use in instance search
299+ addInstance : (className, instName : TTName) -> Elab ()
300+ addInstance className instName = prim__AddInstance className instName
301+
302+ ||| Attempt to solve the current goal with a type class dictionary
303+ |||
304+ ||| @ fn the name of the definition being elaborated (to prevent Idris
305+ ||| from looping)
306+ resolveTC : (fn : TTName) -> Elab ()
307+ resolveTC fn = prim__ResolveTC fn
308+
309+ ||| Halt elaboration, dumping the internal state for inspection.
310+ |||
311+ ||| This is intended for elaboration script developers, not for
312+ ||| end-users. Use `fail` for final scripts.
313+ debug : Elab a
314+ debug = prim__Debug Nothing
315+
316+ ||| Halt elaboration, dumping the internal state and displaying a
317+ ||| message.
318+ |||
319+ ||| This is intended for elaboration script developers, not for
320+ ||| end-users. Use `fail` for final scripts.
321+ |||
322+ ||| @ msg the message to display
323+ debugMessage : (msg : String) -> Elab a
324+ debugMessage msg = prim__Debug (Just msg)
325+
326+ ||| Recursively invoke the reflected elaborator with some goal.
327+ |||
328+ ||| The result is the final term and its type.
329+ runElab : Raw -> Elab () -> Elab (TT, TT)
330+ runElab goal script = prim__RecursiveElab goal script
87331
88−instance Functor Elab where
89− map f t = prim__BindElab t (\x => prim__PureElab (f x))
90−
91−instance Applicative Elab where
92− pure x = prim__PureElab x
93− f <*> x = prim__BindElab f $ \g =>
94− prim__BindElab x $ \y =>
95− prim__PureElab $ g y
96−
97−instance Alternative Elab where
98− empty = prim__Fail [TextPart "empty"]
99− x <|> y = prim__Try x y
100−
101−instance Monad Elab where
102− x >>= f = prim__BindElab x f
103−
104−fail : List ErrorReportPart -> Elab a
105−fail err = prim__Fail err
106−
107−getEnv : Elab (List (TTName, Binder TT))
108−getEnv = prim__Env
109−
110−getGoal : Elab (TTName, TT)
111−getGoal = prim__Goal
112−
113−getHoles : Elab (List TTName)
114−getHoles = prim__Holes
115−
116−getGuess : Elab (Maybe TT)
117−getGuess = prim__Guess
118−
119−lookupTy : TTName -> Elab (List (TTName, NameType, TT))
120−lookupTy n = prim__LookupTy n
121−
122−lookupTyExact : TTName -> Elab (TTName, NameType, TT)
123−lookupTyExact n = case !(lookupTy n) of
124− [res] => return res
125− [] => fail [NamePart n, TextPart "is not defined."]
126− xs => fail [NamePart n, TextPart "is ambiguous."]
127−
128−lookupDatatype : TTName -> Elab (List Datatype)
129−lookupDatatype n = prim__LookupDatatype n
130−
131−lookupDatatypeExact : TTName -> Elab Datatype
132−lookupDatatypeExact n = case !(lookupDatatype n) of
133− [res] => return res
134− [] => fail [TextPart "No datatype named", NamePart n]
135− xs => fail [TextPart "More than one datatype named", NamePart n]
136−
137−forgetTypes : TT -> Elab Raw
138−forgetTypes tt = prim__Forget tt
139−
140−gensym : (hint : String) -> Elab TTName
141−gensym hint = prim__Gensym hint
142−
143−solve : Elab ()
144−solve = prim__Solve
145−
146−fill : Raw -> Elab ()
147−fill tm = prim__Fill tm
148−
149−||| Fill with unification
150−apply : Raw -> Elab ()
151−apply tm = prim__Apply tm
152−
153−focus : (hole : TTName) -> Elab ()
154−focus hole = prim__Focus hole
155−
156−unfocus : TTName -> Elab ()
157−unfocus hole = prim__Unfocus hole
158−
159−attack : Elab ()
160−attack = prim__Attack
161−
162−claim : TTName -> Raw -> Elab ()
163−claim n ty = prim__Claim n ty
164−
165−||| Introduce a lambda binding around the current hole and focus on
166−||| the body. Requires that the hole be in binding form (use
167−||| `attack`).
168−|||
169−||| @ n the name to use for the argument, or `Nothing` to use the name
170−||| in the corresponding hole type (a dependent function)
171−intro : (n : Maybe TTName) -> Elab ()
172−intro n = prim__Intro n
173−
174−||| Introduce a dependent function type binding into the current hole,
175−||| and focus on the body.
176−forall : TTName -> Raw -> Elab ()
177−forall n ty = prim__Forall n ty
178−
179−patvar : TTName -> Elab ()
180−patvar n = prim__PatVar n
181−
182−patbind : TTName -> Elab ()
183−patbind n = prim__PatBind n
184−
185−compute : Elab ()
186−compute = prim__Compute
187−
188−||| Find out the present source context for the tactic script
189−getSourceLocation : Elab SourceLocation
190−getSourceLocation = prim__SourceLocation
191−
192−||| Attempt to solve the current goal with the source code location
193−sourceLocation : Elab ()
194−sourceLocation = do loc <- getSourceLocation
195− fill (quote loc)
196− solve
197−
198−rewriteWith : Raw -> Elab ()
199−rewriteWith rule = prim__Rewrite rule
200−
201−declareType : TyDecl -> Elab ()
202−declareType decl = prim__DeclareType decl
203−
204−defineFunction : FunDefn -> Elab ()
205−defineFunction defun = prim__DefineFunction defun
206−
207−debug : Elab a
208−debug = prim__Debug Nothing
209−
210−runElab : Raw -> Elab () -> Elab (TT, TT)
211−runElab goal script = prim__RecursiveElab goal script
212−
213−debugMessage : String -> Elab a
214−debugMessage msg = prim__Debug (Just msg)