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