@@ -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
@@ -382,3 +413,64 @@ mutual
382 quote (PVTy x) = `(PVTy {a=TT} ~(assert_total (quote x)))
413 quote (PVTy x) = `(PVTy {a=TT} ~(assert_total (quote x)))
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))
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))
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))
443+instance Quotable Raw where
447+instance Quotable (Binder Raw) where
448+ quotedTy = `(Binder Raw)
449+ quote = quoteRawBinder
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))