@@ -8,31 +8,62 @@ import Prelude.Maybe
8import Prelude.Monad
8import Prelude.Monad
9import Language.Reflection
9import Language.Reflection
11+||| Arguments, with plicity.
11data Arg : Type where
12data Arg : Type where
13+ ||| An explicit argument
12 Explicit : TTName -> Raw -> Arg
14 Explicit : TTName -> Raw -> Arg
16+ ||| An implicit argument, to be solved by unification
13 Implicit : TTName -> Raw -> Arg
17 Implicit : TTName -> Raw -> Arg
19+ ||| A type-class constraint argument, to be solved by type class
14 Constraint : TTName -> Raw -> Arg
21 Constraint : TTName -> Raw -> Arg
23+||| A type declaration
16data TyDecl : Type where
24data TyDecl : Type where
25+ ||| A type declaration.
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
31+ ||| @ fn the name to be declared, fully-qualified
32+ ||| @ args the arguments to the function
33+ ||| @ ret the final return type
17− Declare : TTName -> List Arg -> Raw -> TyDecl
34+ Declare : (fn : TTName) -> (args : List Arg) -> (ret : Raw) -> TyDecl
36+||| A single pattern-matching clause
19data FunClause : Type where
37data FunClause : Type where
20 MkFunClause : (lhs, rhs : Raw) -> FunClause
38 MkFunClause : (lhs, rhs : Raw) -> FunClause
21 MkImpossibleClause : (lhs : Raw) -> FunClause
39 MkImpossibleClause : (lhs : Raw) -> FunClause
41+||| A reflected function definition.
23data FunDefn : Type where
42data FunDefn : Type where
24 DefineFun : TTName -> List FunClause -> FunDefn
43 DefineFun : TTName -> List FunClause -> FunDefn
45+||| An argument to a type constructor.
26data TyConArg : Type where
46data TyConArg : Type where
47+ ||| Parameters are consistent across all constructors of the type
27 Parameter : TTName -> Raw -> TyConArg
48 Parameter : TTName -> Raw -> TyConArg
50+ ||| Indices are allowed to vary across constructors
28 Index : TTName -> Raw -> TyConArg
51 Index : TTName -> Raw -> TyConArg
53+||| A reflected datatype definition
30data Datatype : Type where
54data Datatype : Type where
55+ ||| A reflected datatype definition
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
31 MkDatatype : (familyName : TTName) ->
61 MkDatatype : (familyName : TTName) ->
32 (tyConArgs : List TyConArg) -> (tyConRes : Raw) ->
62 (tyConArgs : List TyConArg) -> (tyConRes : Raw) ->
33 (constrs : List (TTName, Raw)) ->
63 (constrs : List (TTName, Raw)) ->
66+||| A reflected elaboration script.
37data Elab : Type -> Type where
68data Elab : Type -> Type where
38 -- obligatory control stuff
69 -- obligatory control stuff
@@ -86,145 +117,210 @@ data Elab : Type -> Type where
86-- Public API
117-- Public API
87-------------
118-------------
88%access public
119%access public
121+ instance Functor Elab where
122+ map f t = prim__BindElab t (\x => prim__PureElab (f x))
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
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
137+ instance Monad Elab where
138+ x >>= f = prim__BindElab x f
140+ ||| Halt elaboration with an error
141+ fail : List ErrorReportPart -> Elab a
142+ fail err = prim__Fail err
144+ ||| Look up the lexical binding at the focused hole
145+ getEnv : Elab (List (TTName, Binder TT))
148+ ||| Get the name and type of the focused hole
149+ getGoal : Elab (TTName, TT)
150+ getGoal = prim__Goal
152+ ||| Get the hole queue, in order
153+ getHoles : Elab (List TTName)
154+ getHoles = prim__Holes
156+ ||| If the current hole contains a guess, return it
157+ getGuess : Elab (Maybe TT)
158+ getGuess = prim__Guess
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
164+ ||| Get the type of a fully-qualified name
165+ lookupTyExact : TTName -> Elab (TTName, NameType, TT)
166+ lookupTyExact n = case !(lookupTy n) of
168+ [] => fail [NamePart n, TextPart "is not defined."]
169+ xs => fail [NamePart n, TextPart "is ambiguous."]
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
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
181+ [] => fail [TextPart "No datatype named", NamePart n]
182+ xs => fail [TextPart "More than one datatype named", NamePart n]
184+ ||| Convert a type-annotated reflected term to its untyped
186+ forgetTypes : TT -> Elab Raw
187+ forgetTypes tt = prim__Forget tt
189+ ||| Generate a unique name based on some hint.
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
196+ ||| Substitute a guess into a hole.
200+ ||| Place a term into a hole, unifying its type
201+ fill : Raw -> Elab ()
202+ fill tm = prim__Fill tm
204+ ||| Fill with unification
205+ apply : Raw -> Elab ()
206+ apply tm = prim__Apply tm
208+ ||| Move the focus to the specified hole
210+ ||| @ hole the hole to focus on
211+ focus : (hole : TTName) -> Elab ()
212+ focus hole = prim__Focus hole
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
219+ ||| Convert a hole to make it suitable for bindings.
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.
226+ attack = prim__Attack
228+ ||| Introduce a new hole with a specified name and type.
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
235+ ||| Introduce a lambda binding around the current hole and focus on
236+ ||| the body. Requires that the hole be in binding form (use
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
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
249+ ||| Convert a hole into a pattern variable.
250+ patvar : TTName -> Elab ()
251+ patvar n = prim__PatVar n
253+ ||| Introduce a new pattern binding.
254+ patbind : TTName -> Elab ()
255+ patbind n = prim__PatBind n
257+ ||| Normalise the goal.
259+ compute = prim__Compute
261+ ||| Find the source context for the elaboration script
262+ getSourceLocation : Elab SourceLocation
263+ getSourceLocation = prim__SourceLocation
265+ ||| Attempt to solve the current goal with the source code location
266+ sourceLocation : Elab ()
267+ sourceLocation = do loc <- getSourceLocation
271+ ||| Attempt to rewrite the goal using an equality.
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
280+ ||| Add a type declaration to the global context.
281+ declareType : TyDecl -> Elab ()
282+ declareType decl = prim__DeclareType decl
284+ ||| Define a function in the global context. The function must have
285+ ||| already been declared, either in ordinary Idris code or using
287+ defineFunction : FunDefn -> Elab ()
288+ defineFunction defun = prim__DefineFunction defun
290+ ||| Register a new instance for type class resolution
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
297+ ||| Attempt to solve the current goal with a type class dictionary
299+ ||| @ fn the name of the definition being elaborated (to prevent Idris
301+ resolveTC : (fn : TTName) -> Elab ()
302+ resolveTC fn = prim__ResolveTC fn
304+ ||| Halt elaboration, dumping the internal state for inspection.
306+ ||| This is intended for elaboration script developers, not for
307+ ||| end-users. Use `fail` for final scripts.
309+ debug = prim__Debug Nothing
311+ ||| Halt elaboration, dumping the internal state and displaying a
314+ ||| This is intended for elaboration script developers, not for
315+ ||| end-users. Use `fail` for final scripts.
317+ ||| @ msg the message to display
318+ debugMessage : (msg : String) -> Elab a
319+ debugMessage msg = prim__Debug (Just msg)
321+ ||| Recursively invoke the reflected elaborator with some goal.
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
90−instance Functor Elab where
91− map f t = prim__BindElab t (\x => prim__PureElab (f x))
93−instance Applicative Elab where
94− pure x = prim__PureElab x
95− f <*> x = prim__BindElab f $ \g =>
96− prim__BindElab x $ \y =>
99−instance Alternative Elab where
100− empty = prim__Fail [TextPart "empty"]
101− x <|> y = prim__Try x y
103−instance Monad Elab where
104− x >>= f = prim__BindElab x f
106−fail : List ErrorReportPart -> Elab a
107−fail err = prim__Fail err
109−getEnv : Elab (List (TTName, Binder TT))
112−getGoal : Elab (TTName, TT)
115−getHoles : Elab (List TTName)
116−getHoles = prim__Holes
118−getGuess : Elab (Maybe TT)
119−getGuess = prim__Guess
121−lookupTy : TTName -> Elab (List (TTName, NameType, TT))
122−lookupTy n = prim__LookupTy n
124−lookupTyExact : TTName -> Elab (TTName, NameType, TT)
125−lookupTyExact n = case !(lookupTy n) of
127− [] => fail [NamePart n, TextPart "is not defined."]
128− xs => fail [NamePart n, TextPart "is ambiguous."]
130−lookupDatatype : TTName -> Elab (List Datatype)
131−lookupDatatype n = prim__LookupDatatype n
133−lookupDatatypeExact : TTName -> Elab Datatype
134−lookupDatatypeExact n = case !(lookupDatatype n) of
136− [] => fail [TextPart "No datatype named", NamePart n]
137− xs => fail [TextPart "More than one datatype named", NamePart n]
139−forgetTypes : TT -> Elab Raw
140−forgetTypes tt = prim__Forget tt
142−gensym : (hint : String) -> Elab TTName
143−gensym hint = prim__Gensym hint
148−fill : Raw -> Elab ()
149−fill tm = prim__Fill tm
151−||| Fill with unification
152−apply : Raw -> Elab ()
153−apply tm = prim__Apply tm
155−focus : (hole : TTName) -> Elab ()
156−focus hole = prim__Focus hole
158−unfocus : TTName -> Elab ()
159−unfocus hole = prim__Unfocus hole
162−attack = prim__Attack
164−claim : TTName -> Raw -> Elab ()
165−claim n ty = prim__Claim n ty
167−||| Introduce a lambda binding around the current hole and focus on
168−||| the body. Requires that the hole be in binding form (use
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
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
181−patvar : TTName -> Elab ()
182−patvar n = prim__PatVar n
184−patbind : TTName -> Elab ()
185−patbind n = prim__PatBind n
188−compute = prim__Compute
190−||| Find out the present source context for the tactic script
191−getSourceLocation : Elab SourceLocation
192−getSourceLocation = prim__SourceLocation
194−||| Attempt to solve the current goal with the source code location
195−sourceLocation : Elab ()
196−sourceLocation = do loc <- getSourceLocation
200−rewriteWith : Raw -> Elab ()
201−rewriteWith rule = prim__Rewrite rule
203−declareType : TyDecl -> Elab ()
204−declareType decl = prim__DeclareType decl
206−defineFunction : FunDefn -> Elab ()
207−defineFunction defun = prim__DefineFunction defun
209−||| Register a new instance for type class resolution
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
216−||| Attempt to solve the current goal with a type class dictionary
218−||| @ fn the name of the definition being elaborated (to prevent Idris
220−resolveTC : (fn : TTName) -> Elab ()
221−resolveTC fn = prim__ResolveTC fn
224−debug = prim__Debug Nothing
226−runElab : Raw -> Elab () -> Elab (TT, TT)
227−runElab goal script = prim__RecursiveElab goal script
229−debugMessage : String -> Elab a
230−debugMessage msg = prim__Debug (Just msg)