@@ -1,3 +1,8 @@
1+||| Primitives and tactics for elaborator reflection.
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.
1module Language.Reflection.Elab
6module Language.Reflection.Elab
3import Builtins
8import Builtins
@@ -8,31 +13,62 @@ import Prelude.Maybe
8import Prelude.Monad
13import Prelude.Monad
9import Language.Reflection
14import Language.Reflection
16+||| Arguments, with plicity.
11data Arg : Type where
17data Arg : Type where
18+ ||| An explicit argument
12 Explicit : TTName -> Raw -> Arg
19 Explicit : TTName -> Raw -> Arg
21+ ||| An implicit argument, to be solved by unification
13 Implicit : TTName -> Raw -> Arg
22 Implicit : TTName -> Raw -> Arg
24+ ||| A type-class constraint argument, to be solved by type class
14 Constraint : TTName -> Raw -> Arg
26 Constraint : TTName -> Raw -> Arg
28+||| A type declaration
16data TyDecl : Type where
29data TyDecl : Type where
30+ ||| A type declaration.
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
36+ ||| @ fn the name to be declared, fully-qualified
37+ ||| @ args the arguments to the function
38+ ||| @ ret the final return type
17− Declare : TTName -> List Arg -> Raw -> TyDecl
39+ Declare : (fn : TTName) -> (args : List Arg) -> (ret : Raw) -> TyDecl
41+||| A single pattern-matching clause
19data FunClause : Type where
42data FunClause : Type where
20 MkFunClause : (lhs, rhs : Raw) -> FunClause
43 MkFunClause : (lhs, rhs : Raw) -> FunClause
21 MkImpossibleClause : (lhs : Raw) -> FunClause
44 MkImpossibleClause : (lhs : Raw) -> FunClause
46+||| A reflected function definition.
23data FunDefn : Type where
47data FunDefn : Type where
24 DefineFun : TTName -> List FunClause -> FunDefn
48 DefineFun : TTName -> List FunClause -> FunDefn
50+||| An argument to a type constructor.
26data TyConArg : Type where
51data TyConArg : Type where
52+ ||| Parameters are consistent across all constructors of the type
27 Parameter : TTName -> Raw -> TyConArg
53 Parameter : TTName -> Raw -> TyConArg
55+ ||| Indices are allowed to vary across constructors
28 Index : TTName -> Raw -> TyConArg
56 Index : TTName -> Raw -> TyConArg
58+||| A reflected datatype definition
30data Datatype : Type where
59data Datatype : Type where
60+ ||| A reflected datatype definition
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
31 MkDatatype : (familyName : TTName) ->
66 MkDatatype : (familyName : TTName) ->
32 (tyConArgs : List TyConArg) -> (tyConRes : Raw) ->
67 (tyConArgs : List TyConArg) -> (tyConRes : Raw) ->
33 (constrs : List (TTName, Raw)) ->
68 (constrs : List (TTName, Raw)) ->
71+||| A reflected elaboration script.
37data Elab : Type -> Type where
73data Elab : Type -> Type where
38 -- obligatory control stuff
74 -- obligatory control stuff
@@ -74,7 +110,9 @@ data Elab : Type -> Type where
75 prim__DeclareType : TyDecl -> Elab ()
111 prim__DeclareType : TyDecl -> Elab ()
76 prim__DefineFunction : FunDefn -> Elab ()
112 prim__DefineFunction : FunDefn -> Elab ()
113+ prim__AddInstance : TTName -> TTName -> Elab ()
115+ prim__ResolveTC : TTName -> Elab ()
78 prim__RecursiveElab : Raw -> Elab () -> Elab (TT, TT)
116 prim__RecursiveElab : Raw -> Elab () -> Elab (TT, TT)
80 prim__Debug : {a : Type} -> Maybe String -> Elab a
118 prim__Debug : {a : Type} -> Maybe String -> Elab a
@@ -84,131 +122,210 @@ data Elab : Type -> Type where
84-- Public API
122-- Public API
85-------------
123-------------
86%access public
124%access public
126+ instance Functor Elab where
127+ map f t = prim__BindElab t (\x => prim__PureElab (f x))
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
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
142+ instance Monad Elab where
143+ x >>= f = prim__BindElab x f
145+ ||| Halt elaboration with an error
146+ fail : List ErrorReportPart -> Elab a
147+ fail err = prim__Fail err
149+ ||| Look up the lexical binding at the focused hole
150+ getEnv : Elab (List (TTName, Binder TT))
153+ ||| Get the name and type of the focused hole
154+ getGoal : Elab (TTName, TT)
155+ getGoal = prim__Goal
157+ ||| Get the hole queue, in order
158+ getHoles : Elab (List TTName)
159+ getHoles = prim__Holes
161+ ||| If the current hole contains a guess, return it
162+ getGuess : Elab (Maybe TT)
163+ getGuess = prim__Guess
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
169+ ||| Get the type of a fully-qualified name
170+ lookupTyExact : TTName -> Elab (TTName, NameType, TT)
171+ lookupTyExact n = case !(lookupTy n) of
173+ [] => fail [NamePart n, TextPart "is not defined."]
174+ xs => fail [NamePart n, TextPart "is ambiguous."]
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
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
186+ [] => fail [TextPart "No datatype named", NamePart n]
187+ xs => fail [TextPart "More than one datatype named", NamePart n]
189+ ||| Convert a type-annotated reflected term to its untyped
191+ forgetTypes : TT -> Elab Raw
192+ forgetTypes tt = prim__Forget tt
194+ ||| Generate a unique name based on some hint.
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
201+ ||| Substitute a guess into a hole.
205+ ||| Place a term into a hole, unifying its type
206+ fill : Raw -> Elab ()
207+ fill tm = prim__Fill tm
209+ ||| Fill with unification
210+ apply : Raw -> Elab ()
211+ apply tm = prim__Apply tm
213+ ||| Move the focus to the specified hole
215+ ||| @ hole the hole to focus on
216+ focus : (hole : TTName) -> Elab ()
217+ focus hole = prim__Focus hole
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
224+ ||| Convert a hole to make it suitable for bindings.
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.
231+ attack = prim__Attack
233+ ||| Introduce a new hole with a specified name and type.
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
240+ ||| Introduce a lambda binding around the current hole and focus on
241+ ||| the body. Requires that the hole be in binding form (use
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
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
254+ ||| Convert a hole into a pattern variable.
255+ patvar : TTName -> Elab ()
256+ patvar n = prim__PatVar n
258+ ||| Introduce a new pattern binding.
259+ patbind : TTName -> Elab ()
260+ patbind n = prim__PatBind n
262+ ||| Normalise the goal.
264+ compute = prim__Compute
266+ ||| Find the source context for the elaboration script
267+ getSourceLocation : Elab SourceLocation
268+ getSourceLocation = prim__SourceLocation
270+ ||| Attempt to solve the current goal with the source code location
271+ sourceLocation : Elab ()
272+ sourceLocation = do loc <- getSourceLocation
276+ ||| Attempt to rewrite the goal using an equality.
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
285+ ||| Add a type declaration to the global context.
286+ declareType : TyDecl -> Elab ()
287+ declareType decl = prim__DeclareType decl
289+ ||| Define a function in the global context. The function must have
290+ ||| already been declared, either in ordinary Idris code or using
292+ defineFunction : FunDefn -> Elab ()
293+ defineFunction defun = prim__DefineFunction defun
295+ ||| Register a new instance for type class resolution
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
302+ ||| Attempt to solve the current goal with a type class dictionary
304+ ||| @ fn the name of the definition being elaborated (to prevent Idris
306+ resolveTC : (fn : TTName) -> Elab ()
307+ resolveTC fn = prim__ResolveTC fn
309+ ||| Halt elaboration, dumping the internal state for inspection.
311+ ||| This is intended for elaboration script developers, not for
312+ ||| end-users. Use `fail` for final scripts.
314+ debug = prim__Debug Nothing
316+ ||| Halt elaboration, dumping the internal state and displaying a
319+ ||| This is intended for elaboration script developers, not for
320+ ||| end-users. Use `fail` for final scripts.
322+ ||| @ msg the message to display
323+ debugMessage : (msg : String) -> Elab a
324+ debugMessage msg = prim__Debug (Just msg)
326+ ||| Recursively invoke the reflected elaborator with some goal.
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
88−instance Functor Elab where
89− map f t = prim__BindElab t (\x => prim__PureElab (f x))
91−instance Applicative Elab where
92− pure x = prim__PureElab x
93− f <*> x = prim__BindElab f $ \g =>
94− prim__BindElab x $ \y =>
97−instance Alternative Elab where
98− empty = prim__Fail [TextPart "empty"]
99− x <|> y = prim__Try x y
101−instance Monad Elab where
102− x >>= f = prim__BindElab x f
104−fail : List ErrorReportPart -> Elab a
105−fail err = prim__Fail err
107−getEnv : Elab (List (TTName, Binder TT))
110−getGoal : Elab (TTName, TT)
113−getHoles : Elab (List TTName)
114−getHoles = prim__Holes
116−getGuess : Elab (Maybe TT)
117−getGuess = prim__Guess
119−lookupTy : TTName -> Elab (List (TTName, NameType, TT))
120−lookupTy n = prim__LookupTy n
122−lookupTyExact : TTName -> Elab (TTName, NameType, TT)
123−lookupTyExact n = case !(lookupTy n) of
125− [] => fail [NamePart n, TextPart "is not defined."]
126− xs => fail [NamePart n, TextPart "is ambiguous."]
128−lookupDatatype : TTName -> Elab (List Datatype)
129−lookupDatatype n = prim__LookupDatatype n
131−lookupDatatypeExact : TTName -> Elab Datatype
132−lookupDatatypeExact n = case !(lookupDatatype n) of
134− [] => fail [TextPart "No datatype named", NamePart n]
135− xs => fail [TextPart "More than one datatype named", NamePart n]
137−forgetTypes : TT -> Elab Raw
138−forgetTypes tt = prim__Forget tt
140−gensym : (hint : String) -> Elab TTName
141−gensym hint = prim__Gensym hint
146−fill : Raw -> Elab ()
147−fill tm = prim__Fill tm
149−||| Fill with unification
150−apply : Raw -> Elab ()
151−apply tm = prim__Apply tm
153−focus : (hole : TTName) -> Elab ()
154−focus hole = prim__Focus hole
156−unfocus : TTName -> Elab ()
157−unfocus hole = prim__Unfocus hole
160−attack = prim__Attack
162−claim : TTName -> Raw -> Elab ()
163−claim n ty = prim__Claim n ty
165−||| Introduce a lambda binding around the current hole and focus on
166−||| the body. Requires that the hole be in binding form (use
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
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
179−patvar : TTName -> Elab ()
180−patvar n = prim__PatVar n
182−patbind : TTName -> Elab ()
183−patbind n = prim__PatBind n
186−compute = prim__Compute
188−||| Find out the present source context for the tactic script
189−getSourceLocation : Elab SourceLocation
190−getSourceLocation = prim__SourceLocation
192−||| Attempt to solve the current goal with the source code location
193−sourceLocation : Elab ()
194−sourceLocation = do loc <- getSourceLocation
198−rewriteWith : Raw -> Elab ()
199−rewriteWith rule = prim__Rewrite rule
201−declareType : TyDecl -> Elab ()
202−declareType decl = prim__DeclareType decl
204−defineFunction : FunDefn -> Elab ()
205−defineFunction defun = prim__DefineFunction defun
208−debug = prim__Debug Nothing
210−runElab : Raw -> Elab () -> Elab (TT, TT)
211−runElab goal script = prim__RecursiveElab goal script
213−debugMessage : String -> Elab a
214−debugMessage msg = prim__Debug (Just msg)