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