@@ -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
@@ -382,3 +413,64 @@ mutual
382413 quote (PVTy x) = `(PVTy {a=TT} ~(assert_total (quote x)))
383414
384415
416+instance Quotable ErrorReportPart where
417+ quotedTy = `(ErrorReportPart)
418+ quote (TextPart x) = `(TextPart ~(quote x))
419+ quote (NamePart n) = `(NamePart ~(quote n))
420+ quote (TermPart tm) = `(TermPart ~(quote tm))
421+ quote (SubReport xs) = `(SubReport ~(assert_total $ quote xs))
422+
423+mutual
424+ quoteRaw : Raw -> TT
425+ quoteRaw (Var n) = `(Var ~(quote n))
426+ quoteRaw (RBind n b tm) = `(RBind ~(quote n) ~(assert_total $ quoteRawBinder b) ~(quoteRaw tm))
427+ quoteRaw (RApp tm tm') = `(RApp ~(quoteRaw tm) ~(quoteRaw tm'))
428+ quoteRaw RType = `(RType)
429+ quoteRaw (RForce tm) = `(RForce ~(quoteRaw tm))
430+ quoteRaw (RConstant c) = `(RConstant ~(quote c))
431+
432+ quoteRawBinder : Binder Raw -> TT
433+ quoteRawBinder (Lam x) = `(Lam {a=Raw} ~(quoteRaw x))
434+ quoteRawBinder (Pi x) = `(Pi {a=Raw} ~(quoteRaw x))
435+ quoteRawBinder (Let x y) = `(Let {a=Raw} ~(quoteRaw x) ~(quoteRaw y))
436+ quoteRawBinder (NLet x y) = `(NLet {a=Raw} ~(quoteRaw x) ~(quoteRaw y))
437+ quoteRawBinder (Hole x) = `(Hole {a=Raw} ~(quoteRaw x))
438+ quoteRawBinder (GHole x) = `(GHole {a=Raw} ~(quoteRaw x))
439+ quoteRawBinder (Guess x y) = `(Guess {a=Raw} ~(quoteRaw x) ~(quoteRaw y))
440+ quoteRawBinder (PVar x) = `(PVar {a=Raw} ~(quoteRaw x))
441+ quoteRawBinder (PVTy x) = `(PVTy {a=Raw} ~(quoteRaw x))
442+
443+instance Quotable Raw where
444+ quotedTy = `(Raw)
445+ quote = quoteRaw
446+
447+instance Quotable (Binder Raw) where
448+ quotedTy = `(Binder Raw)
449+ quote = quoteRawBinder
450+
451+instance Quotable Tactic where
452+ quotedTy = `(Tactic)
453+ quote (Try tac tac') = `(Try ~(quote tac) ~(quote tac'))
454+ quote (GoalType x tac) = `(GoalType ~(quote x) ~(quote tac))
455+ quote (Refine n) = `(Refine ~(quote n))
456+ quote (Seq tac tac') = `(Seq ~(quote tac) ~(quote tac'))
457+ quote Trivial = `(Trivial)
458+ quote (Search x) = `(Search ~(quote x))
459+ quote Instance = `(Instance)
460+ quote Solve = `(Solve)
461+ quote Intros = `(Intros)
462+ quote (Intro n) = `(Intro ~(quote n))
463+ quote (ApplyTactic tm) = `(ApplyTactic ~(quote tm))
464+ quote (Reflect tm) = `(Reflect ~(quote tm))
465+ quote (ByReflection tm) = `(ByReflection ~(quote tm))
466+ quote (Fill tm) = `(Fill ~(quote tm))
467+ quote (Exact tm) = `(Exact ~(quote tm))
468+ quote (Focus n) = `(Focus ~(quote n))
469+ quote (Rewrite tm) = `(Rewrite ~(quote tm))
470+ quote (Induction tm) = `(Induction ~(quote tm))
471+ quote (Case tm) = `(Case ~(quote tm))
472+ quote (LetTac n tm) = `(LetTac ~(quote n) ~(quote tm))
473+ quote (LetTacTy n tm tm') = `(LetTacTy ~(quote n) ~(quote tm) ~(quote tm'))
474+ quote Compute = `(Compute)
475+ quote Skip = `(Skip)
476+ quote (Fail xs) = `(Fail ~(quote xs))