@@ -2,24 +2,28 @@ module Language.Reflection
3%access public
3%access public
5−data TTName = UN String
5+data TTName =
6− -- ^ User-provided name
6+ ||| A user-provided name
8+ ||| A name in some namespace.
10+ ||| The namespace is in reverse order, so `(NS (UN "foo") ["B", "A"])` represents the name `A.B.foo`
7− | NS TTName (List String)
11+ NS TTName (List String) |
10− -- ^ Machine chosen names
12+ ||| Machine-chosen names
11− | NErased
13+ MN Int String |
12− -- ^ Name of somethng which is never used in scope
14+ ||| Name of something which is never used in scope
13%name TTName n, n'
16%name TTName n, n'
16userSuppliedName : String -> TTName
19userSuppliedName : String -> TTName
17userSuppliedName = UN
20userSuppliedName = UN
19−data TTUExp = UVar Int
22+data TTUExp =
20− -- ^ universe variable
23+ ||| Universe variable
25+ ||| Explicit universe level
21− | UVal Int
26+ UVal Int
22− -- ^ explicit universe variable
23%name TTUExp uexp
27%name TTUExp uexp
25data NativeTy = IT8 | IT16 | IT32 | IT64
29data NativeTy = IT8 | IT16 | IT32 | IT64
@@ -133,98 +137,125 @@ instance Traversable Binder where
135||| Reflection of the well typed core language
139||| Reflection of the well typed core language
141+ ||| A reference to some name (P for Parameter)
136−data TT = P NameType TTName TT
142+ P NameType TTName TT |
139− -- ^ variables
143+ ||| de Bruijn variables
140− | Bind TTName (Binder TT) TT
146+ Bind TTName (Binder TT) TT |
141− -- ^ type annotated named bindings
147+ ||| Apply one term to another
142− | App TT TT
148+ App TT TT |
143− -- ^ (named) application of a function to a value
149+ ||| Embed a constant
144− | TConst Const
150+ TConst Const |
147− -- ^ argument projection; runtime only
151+ ||| Argument projection; runtime only
148− | Erased
153+ ||| Erased terms
149− -- ^ erased terms
154+ Erased |
150− | Impossible
155+ ||| Impossible terms
151− -- ^ impossible terms
156+ Impossible |
157+ ||| The type of types along (with universe constraints)
152− | TType TTUExp
158+ TType TTUExp
155%name TT tm, tm'
159%name TT tm, tm'
157||| Raw terms without types
161||| Raw terms without types
163+ ||| Variables, global or local
158−data Raw = Var TTName
164+ Var TTName |
159− | RBind TTName (Binder Raw) Raw
166+ RBind TTName (Binder Raw) Raw |
160− | RApp Raw Raw
168+ RApp Raw Raw |
169+ ||| The type of types
162− | RForce Raw
171+ RForce Raw |
172+ ||| Embed a constant
163− | RConstant Const
173+ RConstant Const
165%name Raw tm, tm'
174%name Raw tm, tm'
167||| Error reports are a list of report parts
176||| Error reports are a list of report parts
168−data ErrorReportPart = TextPart String
177+data ErrorReportPart =
178+ ||| A human-readable string
180+ ||| An Idris name (to be semantically coloured)
169− | NamePart TTName
181+ NamePart TTName |
182+ ||| An Idris term, to be pretty printed
170− | TermPart TT
183+ TermPart TT |
184+ ||| An indented sub-report, to provide more details
171− | SubReport (List ErrorReportPart)
185+ SubReport (List ErrorReportPart)
172%name ErrorReportPart part, p
186%name ErrorReportPart part, p
188+||| A representation of Idris's tactics that can be returned from custom
189+||| tactic implementations. Generate these using `applyTactic`.
174−data Tactic = Try Tactic Tactic
190+data Tactic =
175− -- ^ try the first tactic and resort to the second one on failure
191+ ||| Try the first tactic and resort to the second one on failure
176− | GoalType String Tactic
192+ Try Tactic Tactic |
177− -- ^ only run if the goal has the right type
193+ ||| Only run if the goal has the right type
178− | Refine TTName
194+ GoalType String Tactic |
179− -- ^ resolve function name, find matching arguments in the
195+ ||| Resolve function name, find matching arguments in the
180− -- context and compute the proof target
196+ ||| context and compute the proof target
181− | Seq Tactic Tactic
197+ Refine TTName |
182− -- ^ apply both tactics in sequence
198+ ||| Apply both tactics in sequence
200+ ||| Intelligently construct the proof target from the context
183− | Trivial
201+ Trivial |
184− -- ^ intelligently construct the proof target from the context
186− -- ^ build a proof by applying contructors up to a maximum depth
202+ ||| Build a proof by applying contructors up to a maximum depth
187− | Instance
203+ Search Int |
188− -- ^ resolve a type class
204+ ||| Resolve a type class
206+ ||| Infer the proof target from the context
190− -- ^ infer the proof target from the context
192− -- ^ introduce all variables into the context
208+ ||| introduce all variables into the context
193− | Intro TTName
209+ Intros |
194− -- ^ introduce a named variable into the context, use the
210+ ||| Introduce a named variable into the context, use the
195− -- first one if the given name is not found
211+ ||| first one if the given name is not found
213+ ||| Invoke the reflected rep. of another tactic
196− | ApplyTactic TT
214+ ApplyTactic TT |
197− -- ^ invoke the reflected rep. of another tactic
215+ ||| Turn a value into its reflected representation
198− | Reflect TT
216+ Reflect TT |
199− -- ^ turn a value into its reflected representation
201− -- ^ use a %reflection function
217+ ||| Use a `%reflection` function
202− | Fill Raw
218+ ByReflection TT |
203− -- ^ turn a raw value back into a term
219+ ||| Turn a raw value back into a term
204− | Exact TT
220+ Fill Raw |
205− -- ^ use the given value to conclude the proof
221+ ||| Use the given value to conclude the proof
206− | Focus TTName
222+ Exact TT |
207− -- ^ focus a named hole
223+ ||| Focus on a particular hole
208− | Rewrite TT
224+ Focus TTName |
209− -- ^ rewrite using the reflected rep. of a equality proof
225+ ||| Rewrite with an equality
210− | Induction TT
226+ Rewrite TT |
211− -- ^ do induction on the particular expression
227+ ||| Perform induction on a particular expression
212− | Case TT
228+ Induction TT |
213− -- ^ do case analysis on particular expression
229+ ||| Perform case analysis on a particular expression
231+ ||| Name a reflected term
214− | LetTac TTName TT
232+ LetTac TTName TT |
215− -- ^ name a reflected term
233+ ||| Name a reflected term and type it
216− | LetTacTy TTName TT TT
234+ LetTacTy TTName TT TT |
217− -- ^ name a reflected term and type it
235+ ||| Normalise the goal
218− | Compute
236+ Compute |
219− -- ^ normalise the context
237+ ||| Do nothing
221− -- ^ do nothing
239+ ||| Fail with an error message
222− | Fail (List ErrorReportPart)
240+ Fail (List ErrorReportPart)
223%name Tactic tac, tac'
241%name Tactic tac, tac'
244+||| Things with a canonical representation in the TT datatype.
246+||| This type class is intended to be used during proof automation and the
247+||| construction of custom tactics.
249+||| @ a the type to be quoted
226class Quotable a where
250class Quotable a where
251+ ||| A representation of the type `a`.
253+ ||| This is to enable quoting polymorphic datatypes
227 quotedTy : TT
254 quotedTy : TT
256+ ||| Quote a particular element of `a`.
258+ ||| Each equation should look something like ```quote (Foo x y) = `(Foo ~(quote x) ~(quote y))```
228 quote : a -> TT
259 quote : a -> TT
230instance Quotable Nat where
261instance Quotable Nat where