git.iko.soy/Idris-dev
on c79fb21 help sign in
Idris-dev/libs/base/Language/Reflection.idr
476 lines 15 kB history raw
1module Language.Reflection
3%access public
5data 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
16%name TTName n, n'
18implicit
19userSuppliedName : String -> TTName
20userSuppliedName = UN
22data TTUExp =
23 ||| Universe variable
24 UVar Int |
25 ||| Explicit universe level
26 UVal Int
27%name TTUExp uexp
29data NativeTy = IT8 | IT16 | IT32 | IT64
31data IntTy = ITFixed NativeTy | ITNative | ITBig | ITChar
32 | ITVec NativeTy Int
34data ArithTy = ATInt Language.Reflection.IntTy | ATFloat
36||| Primitive constants
37data Const = I Int | BI Integer | Fl Float | Ch Char | Str String
38 | B8 Bits8 | B16 Bits16 | B32 Bits32 | B64 Bits64
39 | B8V Bits8x16 | B16V Bits16x8
40 | B32V Bits32x4 | B64V Bits64x2
41 | AType ArithTy | StrType
42 | PtrType | ManagedPtrType | BufferType | VoidType | Forgot
44%name Const c, c'
46abstract class ReflConst (a : Type) where
47 toConst : a -> Const
49instance ReflConst Int where
50 toConst x = I x
52instance ReflConst Integer where
53 toConst = BI
55instance ReflConst Float where
56 toConst = Fl
58instance ReflConst Char where
59 toConst = Ch
61instance ReflConst String where
62 toConst = Str
64instance ReflConst Bits8 where
65 toConst = B8
67instance ReflConst Bits16 where
68 toConst = B16
70instance ReflConst Bits32 where
71 toConst = B32
73instance ReflConst Bits64 where
74 toConst = B64
76implicit
77reflectConstant: (ReflConst a) => a -> Const
78reflectConstant = toConst
81||| Types of named references
82data NameType = Bound
83 -- ^ reference which is just bound, e.g. by intro
84 | Ref
85 -- ^ reference to a variable
86 | DCon Int Int
87 -- ^ constructor with tag and number
88 | TCon Int Int
89 -- ^ type constructor with tag and number
90%name NameType nt, nt'
92||| Types annotations for bound variables in different
93||| binding contexts
94data Binder a = Lam a
95 | Pi a
96 | Let a a
97 | NLet a a
98 | Hole a
99 | GHole a
100 | Guess a a
101 | PVar a
102 | PVTy a
103%name Binder b, b'
105instance Functor Binder where
106 map f (Lam x) = Lam (f x)
107 map f (Pi x) = Pi (f x)
108 map f (Let x y) = Let (f x) (f y)
109 map f (NLet x y) = NLet (f x) (f y)
110 map f (Hole x) = Hole (f x)
111 map f (GHole x) = GHole (f x)
112 map f (Guess x y) = Guess (f x) (f y)
113 map f (PVar x) = PVar (f x)
114 map f (PVTy x) = PVTy (f x)
116instance Foldable Binder where
117 foldr f z (Lam x) = f x z
118 foldr f z (Pi x) = f x z
119 foldr f z (Let x y) = f x (f y z)
120 foldr f z (NLet x y) = f x (f y z)
121 foldr f z (Hole x) = f x z
122 foldr f z (GHole x) = f x z
123 foldr f z (Guess x y) = f x (f y z)
124 foldr f z (PVar x) = f x z
125 foldr f z (PVTy x) = f x z
127instance Traversable Binder where
128 traverse f (Lam x) = [| Lam (f x) |]
129 traverse f (Pi x) = [| Pi (f x) |]
130 traverse f (Let x y) = [| Let (f x) (f y) |]
131 traverse f (NLet x y) = [| NLet (f x) (f y) |]
132 traverse f (Hole x) = [| Hole (f x) |]
133 traverse f (GHole x) = [| GHole (f x) |]
134 traverse f (Guess x y) = [| Guess (f x) (f y) |]
135 traverse f (PVar x) = [| PVar (f x) |]
136 traverse f (PVTy x) = [| PVTy (f x) |]
139||| Reflection of the well typed core language
140data 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
159%name TT tm, tm'
161||| Raw terms without types
162data 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
174%name Raw tm, tm'
176||| Error reports are a list of report parts
177data 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)
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`.
190data 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)
241%name Tactic tac, tac'
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
250class Quotable a where
251 ||| A representation of the type `a`.
252 |||
253 ||| This is to enable quoting polymorphic datatypes
254 quotedTy : TT
256 ||| Quote a particular element of `a`.
257 |||
258 ||| Each equation should look something like ```quote (Foo x y) = `(Foo ~(quote x) ~(quote y))```
259 quote : a -> TT
261instance Quotable Nat where
262 quotedTy = `(Nat)
264 quote Z = `(Z)
265 quote (S k) = `(S ~(quote k))
267instance Quotable Int where
268 quotedTy = `(Int)
269 quote x = TConst (I x)
271instance Quotable Float where
272 quotedTy = `(Float)
273 quote x = TConst (Fl x)
275instance Quotable Char where
276 quotedTy = `(Char)
277 quote x = TConst (Ch x)
279instance Quotable Bits8 where
280 quotedTy = `(Bits8)
281 quote x = TConst (B8 x)
283instance Quotable Bits16 where
284 quotedTy = `(Bits16)
285 quote x = TConst (B16 x)
287instance Quotable Bits32 where
288 quotedTy = `(Bits32)
289 quote x = TConst (B32 x)
291instance Quotable Bits64 where
292 quotedTy = `(Bits64)
293 quote x = TConst (B64 x)
295instance Quotable Integer where
296 quotedTy = `(Integer)
297 quote x = TConst (BI x)
299instance Quotable Bits8x16 where
300 quotedTy = `(Bits8x16)
301 quote x = TConst (B8V x)
303instance Quotable Bits16x8 where
304 quotedTy = `(Bits16x8)
305 quote x = TConst (B16V x)
307instance Quotable Bits32x4 where
308 quotedTy = `(Bits32x4)
309 quote x = TConst (B32V x)
311instance Quotable Bits64x2 where
312 quotedTy = `(Bits64x2)
313 quote x = TConst (B64V x)
315instance Quotable String where
316 quotedTy = `(String)
317 quote x = TConst (Str x)
319instance Quotable NameType where
320 quotedTy = `(NameType)
321 quote Bound = `(Bound)
322 quote Ref = `(Ref)
323 quote (DCon x y) = `(DCon ~(quote x) ~(quote y))
324 quote (TCon x y) = `(TCon ~(quote x) ~(quote y))
326instance Quotable a => Quotable (List a) where
327 quotedTy = `(List ~(quotedTy {a=a}))
328 quote [] = `(List.Nil {a=~quotedTy})
329 quote (x :: xs) = `(List.(::) {a=~quotedTy} ~(quote x) ~(quote xs))
331instance Quotable TTName where
332 quotedTy = `(TTName)
333 quote (UN x) = `(UN ~(quote x))
334 quote (NS n xs) = `(NS ~(quote n) ~(quote xs))
335 quote (MN x y) = `(MN ~(quote x) ~(quote y))
336 quote NErased = `(NErased)
338instance Quotable NativeTy where
339 quotedTy = `(NativeTy)
340 quote IT8 = `(Reflection.IT8)
341 quote IT16 = `(Reflection.IT16)
342 quote IT32 = `(Reflection.IT32)
343 quote IT64 = `(Reflection.IT64)
345instance Quotable Reflection.IntTy where
346 quotedTy = `(Reflection.IntTy)
347 quote (ITFixed x) = `(ITFixed ~(quote x))
348 quote ITNative = `(Reflection.ITNative)
349 quote ITBig = `(ITBig)
350 quote ITChar = `(Reflection.ITChar)
351 quote (ITVec x y) = `(ITVec ~(quote x) ~(quote y))
353instance Quotable ArithTy where
354 quotedTy = `(ArithTy)
355 quote (ATInt x) = `(ATInt ~(quote x))
356 quote ATFloat = `(ATFloat)
358instance Quotable Const where
359 quotedTy = `(Const)
360 quote (I x) = `(I ~(quote x))
361 quote (BI x) = `(BI ~(quote x))
362 quote (Fl x) = `(Fl ~(quote x))
363 quote (Ch x) = `(Ch ~(quote x))
364 quote (Str x) = `(Str ~(quote x))
365 quote (B8 x) = `(B8 ~(quote x))
366 quote (B16 x) = `(B16 ~(quote x))
367 quote (B32 x) = `(B32 ~(quote x))
368 quote (B64 x) = `(B64 ~(quote x))
369 quote (B8V xs) = `(B8V ~(quote xs))
370 quote (B16V xs) = `(B16V ~(quote xs))
371 quote (B32V xs) = `(B32V ~(quote xs))
372 quote (B64V xs) = `(B64V ~(quote xs))
373 quote (AType x) = `(AType ~(quote x))
374 quote StrType = `(StrType)
375 quote PtrType = `(PtrType)
376 quote ManagedPtrType = `(ManagedPtrType)
377 quote BufferType = `(BufferType)
378 quote VoidType = `(VoidType)
379 quote Forgot = `(Forgot)
382instance Quotable TTUExp where
383 quotedTy = `(TTUExp)
384 quote (UVar x) = `(UVar ~(quote x))
385 quote (UVal x) = `(UVal ~(quote x))
387mutual
388 instance Quotable TT where
389 quotedTy = `(TT)
390 quote (P nt n tm) = `(P ~(quote nt) ~(quote n) ~(quote tm))
391 quote (V x) = `(V ~(quote x))
392 quote (Bind n b tm) = `(Bind ~(quote n) ~(assert_total (quote b)) ~(quote tm))
393 quote (App f x) = `(App ~(quote f) ~(quote x))
394 quote (TConst c) = `(TConst ~(quote c))
395 quote (Proj tm x) = `(Proj ~(quote tm) ~(quote x))
396 quote Erased = `(Erased)
397 quote Impossible = `(Impossible)
398 quote (TType uexp) = `(TType ~(quote uexp))
400 instance Quotable (Binder TT) where
401 quotedTy = `(Binder TT)
402 quote (Lam x) = `(Lam {a=TT} ~(assert_total (quote x)))
403 quote (Pi x) = `(Pi {a=TT} ~(assert_total (quote x)))
404 quote (Let x y) = `(Let {a=TT} ~(assert_total (quote x))
405 ~(assert_total (quote y)))
406 quote (NLet x y) = `(NLet {a=TT} ~(assert_total (quote x))
407 ~(assert_total (quote y)))
408 quote (Hole x) = `(Hole {a=TT} ~(assert_total (quote x)))
409 quote (GHole x) = `(GHole {a=TT} ~(assert_total (quote x)))
410 quote (Guess x y) = `(Guess {a=TT} ~(assert_total (quote x))
411 ~(assert_total (quote y)))
412 quote (PVar x) = `(PVar {a=TT} ~(assert_total (quote x)))
413 quote (PVTy x) = `(PVTy {a=TT} ~(assert_total (quote x)))
416instance 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))
423mutual
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))
443instance Quotable Raw where
444 quotedTy = `(Raw)
445 quote = quoteRaw
447instance Quotable (Binder Raw) where
448 quotedTy = `(Binder Raw)
449 quote = quoteRawBinder
451instance 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))