git.iko.soy/Idris-dev
on f1e161d help sign in
Idris-dev/libs/base/Language/Reflection.idr
487 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 =
83 ||| A reference which is just bound, e.g. by intro
84 Bound |
85 ||| A reference to a de Bruijn-indexed variable
86 Ref |
87 ||| Data constructor with tag and number
88 DCon Int Int |
89 ||| Type constructor with tag and number
90 TCon Int Int
92%name NameType nt, nt'
94||| Types annotations for bound variables in different
95||| binding contexts
96data Binder a = Lam a
97 | Pi a a
98 | Let a a
99 | NLet a a
100 | Hole a
101 | GHole a
102 | Guess a a
103 | PVar a
104 | PVTy a
105%name Binder b, b'
107instance Functor Binder where
108 map f (Lam x) = Lam (f x)
109 map f (Pi x k) = Pi (f x) (f k)
110 map f (Let x y) = Let (f x) (f y)
111 map f (NLet x y) = NLet (f x) (f y)
112 map f (Hole x) = Hole (f x)
113 map f (GHole x) = GHole (f x)
114 map f (Guess x y) = Guess (f x) (f y)
115 map f (PVar x) = PVar (f x)
116 map f (PVTy x) = PVTy (f x)
118instance Foldable Binder where
119 foldr f z (Lam x) = f x z
120 foldr f z (Pi x k) = f x (f k z)
121 foldr f z (Let x y) = f x (f y z)
122 foldr f z (NLet x y) = f x (f y z)
123 foldr f z (Hole x) = f x z
124 foldr f z (GHole x) = f x z
125 foldr f z (Guess x y) = f x (f y z)
126 foldr f z (PVar x) = f x z
127 foldr f z (PVTy x) = f x z
129instance Traversable Binder where
130 traverse f (Lam x) = [| Lam (f x) |]
131 traverse f (Pi x k) = [| Pi (f x) (f k) |]
132 traverse f (Let x y) = [| Let (f x) (f y) |]
133 traverse f (NLet x y) = [| NLet (f x) (f y) |]
134 traverse f (Hole x) = [| Hole (f x) |]
135 traverse f (GHole x) = [| GHole (f x) |]
136 traverse f (Guess x y) = [| Guess (f x) (f y) |]
137 traverse f (PVar x) = [| PVar (f x) |]
138 traverse f (PVTy x) = [| PVTy (f x) |]
141||| Reflection of the well typed core language
142data TT =
143 ||| A reference to some name (P for Parameter)
144 P NameType TTName TT |
145 ||| de Bruijn variables
146 V Int |
147 ||| Bind a variable
148 Bind TTName (Binder TT) TT |
149 ||| Apply one term to another
150 App TT TT |
151 ||| Embed a constant
152 TConst Const |
153 ||| Argument projection; runtime only
154 Proj TT Int |
155 ||| Erased terms
156 Erased |
157 ||| Impossible terms
158 Impossible |
159 ||| The type of types along (with universe constraints)
160 TType TTUExp
161%name TT tm, tm'
163||| Raw terms without types
164data Raw =
165 ||| Variables, global or local
166 Var TTName |
167 ||| Bind a variable
168 RBind TTName (Binder Raw) Raw |
169 ||| Application
170 RApp Raw Raw |
171 ||| The type of types
172 RType |
173 RForce Raw |
174 ||| Embed a constant
175 RConstant Const
176%name Raw tm, tm'
178data SourceLocation : Type where
179 FileLoc : (filename : String) -> (start : (Int, Int)) -> (end : (Int, Int)) -> SourceLocation
181%name SourceLocation loc
183||| Error reports are a list of report parts
184data ErrorReportPart =
185 ||| A human-readable string
186 TextPart String |
187 ||| An Idris name (to be semantically coloured)
188 NamePart TTName |
189 ||| An Idris term, to be pretty printed
190 TermPart TT |
191 ||| An indented sub-report, to provide more details
192 SubReport (List ErrorReportPart)
193%name ErrorReportPart part, p
195||| A representation of Idris's tactics that can be returned from custom
196||| tactic implementations. Generate these using `applyTactic`.
197data Tactic =
198 ||| Try the first tactic and resort to the second one on failure
199 Try Tactic Tactic |
200 ||| Only run if the goal has the right type
201 GoalType String Tactic |
202 ||| Resolve function name, find matching arguments in the
203 ||| context and compute the proof target
204 Refine TTName |
205 ||| Apply both tactics in sequence
206 Seq Tactic Tactic |
207 ||| Intelligently construct the proof target from the context
208 Trivial |
209 ||| Build a proof by applying contructors up to a maximum depth
210 Search Int |
211 ||| Resolve a type class
212 Instance |
213 ||| Infer the proof target from the context
214 Solve |
215 ||| introduce all variables into the context
216 Intros |
217 ||| Introduce a named variable into the context, use the
218 ||| first one if the given name is not found
219 Intro TTName |
220 ||| Invoke the reflected rep. of another tactic
221 ApplyTactic TT |
222 ||| Turn a value into its reflected representation
223 Reflect TT |
224 ||| Use a `%reflection` function
225 ByReflection TT |
226 ||| Turn a raw value back into a term
227 Fill Raw |
228 ||| Use the given value to conclude the proof
229 Exact TT |
230 ||| Focus on a particular hole
231 Focus TTName |
232 ||| Rewrite with an equality
233 Rewrite TT |
234 ||| Perform induction on a particular expression
235 Induction TT |
236 ||| Perform case analysis on a particular expression
237 Case TT |
238 ||| Name a reflected term
239 LetTac TTName TT |
240 ||| Name a reflected term and type it
241 LetTacTy TTName TT TT |
242 ||| Normalise the goal
243 Compute |
244 ||| Do nothing
245 Skip |
246 ||| Fail with an error message
247 Fail (List ErrorReportPart) |
248 ||| Attempt to fill the hole with source code information
249 SourceFC
250%name Tactic tac, tac'
253||| Things with a canonical representation in the TT datatype.
254|||
255||| This type class is intended to be used during proof automation and the
256||| construction of custom tactics.
257|||
258||| @ a the type to be quoted
259class Quotable a where
260 ||| A representation of the type `a`.
261 |||
262 ||| This is to enable quoting polymorphic datatypes
263 quotedTy : TT
265 ||| Quote a particular element of `a`.
266 |||
267 ||| Each equation should look something like ```quote (Foo x y) = `(Foo ~(quote x) ~(quote y))```
268 quote : a -> TT
270instance Quotable Nat where
271 quotedTy = `(Nat)
273 quote Z = `(Z)
274 quote (S k) = `(S ~(quote k))
276instance Quotable Int where
277 quotedTy = `(Int)
278 quote x = TConst (I x)
280instance Quotable Float where
281 quotedTy = `(Float)
282 quote x = TConst (Fl x)
284instance Quotable Char where
285 quotedTy = `(Char)
286 quote x = TConst (Ch x)
288instance Quotable Bits8 where
289 quotedTy = `(Bits8)
290 quote x = TConst (B8 x)
292instance Quotable Bits16 where
293 quotedTy = `(Bits16)
294 quote x = TConst (B16 x)
296instance Quotable Bits32 where
297 quotedTy = `(Bits32)
298 quote x = TConst (B32 x)
300instance Quotable Bits64 where
301 quotedTy = `(Bits64)
302 quote x = TConst (B64 x)
304instance Quotable Integer where
305 quotedTy = `(Integer)
306 quote x = TConst (BI x)
308instance Quotable Bits8x16 where
309 quotedTy = `(Bits8x16)
310 quote x = TConst (B8V x)
312instance Quotable Bits16x8 where
313 quotedTy = `(Bits16x8)
314 quote x = TConst (B16V x)
316instance Quotable Bits32x4 where
317 quotedTy = `(Bits32x4)
318 quote x = TConst (B32V x)
320instance Quotable Bits64x2 where
321 quotedTy = `(Bits64x2)
322 quote x = TConst (B64V x)
324instance Quotable String where
325 quotedTy = `(String)
326 quote x = TConst (Str x)
328instance Quotable NameType where
329 quotedTy = `(NameType)
330 quote Bound = `(Bound)
331 quote Ref = `(Ref)
332 quote (DCon x y) = `(DCon ~(quote x) ~(quote y))
333 quote (TCon x y) = `(TCon ~(quote x) ~(quote y))
335instance Quotable a => Quotable (List a) where
336 quotedTy = `(List ~(quotedTy {a=a}))
337 quote [] = `(List.Nil {a=~quotedTy})
338 quote (x :: xs) = `(List.(::) {a=~quotedTy} ~(quote x) ~(quote xs))
340instance Quotable TTName where
341 quotedTy = `(TTName)
342 quote (UN x) = `(UN ~(quote x))
343 quote (NS n xs) = `(NS ~(quote n) ~(quote xs))
344 quote (MN x y) = `(MN ~(quote x) ~(quote y))
345 quote NErased = `(NErased)
347instance Quotable NativeTy where
348 quotedTy = `(NativeTy)
349 quote IT8 = `(Reflection.IT8)
350 quote IT16 = `(Reflection.IT16)
351 quote IT32 = `(Reflection.IT32)
352 quote IT64 = `(Reflection.IT64)
354instance Quotable Reflection.IntTy where
355 quotedTy = `(Reflection.IntTy)
356 quote (ITFixed x) = `(ITFixed ~(quote x))
357 quote ITNative = `(Reflection.ITNative)
358 quote ITBig = `(ITBig)
359 quote ITChar = `(Reflection.ITChar)
360 quote (ITVec x y) = `(ITVec ~(quote x) ~(quote y))
362instance Quotable ArithTy where
363 quotedTy = `(ArithTy)
364 quote (ATInt x) = `(ATInt ~(quote x))
365 quote ATFloat = `(ATFloat)
367instance Quotable Const where
368 quotedTy = `(Const)
369 quote (I x) = `(I ~(quote x))
370 quote (BI x) = `(BI ~(quote x))
371 quote (Fl x) = `(Fl ~(quote x))
372 quote (Ch x) = `(Ch ~(quote x))
373 quote (Str x) = `(Str ~(quote x))
374 quote (B8 x) = `(B8 ~(quote x))
375 quote (B16 x) = `(B16 ~(quote x))
376 quote (B32 x) = `(B32 ~(quote x))
377 quote (B64 x) = `(B64 ~(quote x))
378 quote (B8V xs) = `(B8V ~(quote xs))
379 quote (B16V xs) = `(B16V ~(quote xs))
380 quote (B32V xs) = `(B32V ~(quote xs))
381 quote (B64V xs) = `(B64V ~(quote xs))
382 quote (AType x) = `(AType ~(quote x))
383 quote StrType = `(StrType)
384 quote PtrType = `(PtrType)
385 quote ManagedPtrType = `(ManagedPtrType)
386 quote BufferType = `(BufferType)
387 quote VoidType = `(VoidType)
388 quote Forgot = `(Forgot)
391instance Quotable TTUExp where
392 quotedTy = `(TTUExp)
393 quote (UVar x) = `(UVar ~(quote x))
394 quote (UVal x) = `(UVal ~(quote x))
396mutual
397 instance Quotable TT where
398 quotedTy = `(TT)
399 quote (P nt n tm) = `(P ~(quote nt) ~(quote n) ~(quote tm))
400 quote (V x) = `(V ~(quote x))
401 quote (Bind n b tm) = `(Bind ~(quote n) ~(assert_total (quote b)) ~(quote tm))
402 quote (App f x) = `(App ~(quote f) ~(quote x))
403 quote (TConst c) = `(TConst ~(quote c))
404 quote (Proj tm x) = `(Proj ~(quote tm) ~(quote x))
405 quote Erased = `(Erased)
406 quote Impossible = `(Impossible)
407 quote (TType uexp) = `(TType ~(quote uexp))
409 instance Quotable (Binder TT) where
410 quotedTy = `(Binder TT)
411 quote (Lam x) = `(Lam {a=TT} ~(assert_total (quote x)))
412 quote (Pi x k) = `(Pi {a=TT} ~(assert_total (quote x))
413 ~(assert_total (quote k)))
414 quote (Let x y) = `(Let {a=TT} ~(assert_total (quote x))
415 ~(assert_total (quote y)))
416 quote (NLet x y) = `(NLet {a=TT} ~(assert_total (quote x))
417 ~(assert_total (quote y)))
418 quote (Hole x) = `(Hole {a=TT} ~(assert_total (quote x)))
419 quote (GHole x) = `(GHole {a=TT} ~(assert_total (quote x)))
420 quote (Guess x y) = `(Guess {a=TT} ~(assert_total (quote x))
421 ~(assert_total (quote y)))
422 quote (PVar x) = `(PVar {a=TT} ~(assert_total (quote x)))
423 quote (PVTy x) = `(PVTy {a=TT} ~(assert_total (quote x)))
426instance Quotable ErrorReportPart where
427 quotedTy = `(ErrorReportPart)
428 quote (TextPart x) = `(TextPart ~(quote x))
429 quote (NamePart n) = `(NamePart ~(quote n))
430 quote (TermPart tm) = `(TermPart ~(quote tm))
431 quote (SubReport xs) = `(SubReport ~(assert_total $ quote xs))
433mutual
434 quoteRaw : Raw -> TT
435 quoteRaw (Var n) = `(Var ~(quote n))
436 quoteRaw (RBind n b tm) = `(RBind ~(quote n) ~(assert_total $ quoteRawBinder b) ~(quoteRaw tm))
437 quoteRaw (RApp tm tm') = `(RApp ~(quoteRaw tm) ~(quoteRaw tm'))
438 quoteRaw RType = `(RType)
439 quoteRaw (RForce tm) = `(RForce ~(quoteRaw tm))
440 quoteRaw (RConstant c) = `(RConstant ~(quote c))
442 quoteRawBinder : Binder Raw -> TT
443 quoteRawBinder (Lam x) = `(Lam {a=Raw} ~(quoteRaw x))
444 quoteRawBinder (Pi x k) = `(Pi {a=Raw} ~(quoteRaw x) ~(quoteRaw k))
445 quoteRawBinder (Let x y) = `(Let {a=Raw} ~(quoteRaw x) ~(quoteRaw y))
446 quoteRawBinder (NLet x y) = `(NLet {a=Raw} ~(quoteRaw x) ~(quoteRaw y))
447 quoteRawBinder (Hole x) = `(Hole {a=Raw} ~(quoteRaw x))
448 quoteRawBinder (GHole x) = `(GHole {a=Raw} ~(quoteRaw x))
449 quoteRawBinder (Guess x y) = `(Guess {a=Raw} ~(quoteRaw x) ~(quoteRaw y))
450 quoteRawBinder (PVar x) = `(PVar {a=Raw} ~(quoteRaw x))
451 quoteRawBinder (PVTy x) = `(PVTy {a=Raw} ~(quoteRaw x))
453instance Quotable Raw where
454 quotedTy = `(Raw)
455 quote = quoteRaw
457instance Quotable (Binder Raw) where
458 quotedTy = `(Binder Raw)
459 quote = quoteRawBinder
461instance Quotable Tactic where
462 quotedTy = `(Tactic)
463 quote (Try tac tac') = `(Try ~(quote tac) ~(quote tac'))
464 quote (GoalType x tac) = `(GoalType ~(quote x) ~(quote tac))
465 quote (Refine n) = `(Refine ~(quote n))
466 quote (Seq tac tac') = `(Seq ~(quote tac) ~(quote tac'))
467 quote Trivial = `(Trivial)
468 quote (Search x) = `(Search ~(quote x))
469 quote Instance = `(Instance)
470 quote Solve = `(Solve)
471 quote Intros = `(Intros)
472 quote (Intro n) = `(Intro ~(quote n))
473 quote (ApplyTactic tm) = `(ApplyTactic ~(quote tm))
474 quote (Reflect tm) = `(Reflect ~(quote tm))
475 quote (ByReflection tm) = `(ByReflection ~(quote tm))
476 quote (Fill tm) = `(Fill ~(quote tm))
477 quote (Exact tm) = `(Exact ~(quote tm))
478 quote (Focus n) = `(Focus ~(quote n))
479 quote (Rewrite tm) = `(Rewrite ~(quote tm))
480 quote (Induction tm) = `(Induction ~(quote tm))
481 quote (Case tm) = `(Case ~(quote tm))
482 quote (LetTac n tm) = `(LetTac ~(quote n) ~(quote tm))
483 quote (LetTacTy n tm tm') = `(LetTacTy ~(quote n) ~(quote tm) ~(quote tm'))
484 quote Compute = `(Compute)
485 quote Skip = `(Skip)
486 quote (Fail xs) = `(Fail ~(quote xs))
487 quote SourceFC = `(SourceFC)