git.iko.soy/Idris-dev
on bf4e535 help sign in
Idris-dev/libs/prelude/Language/Reflection.idr
613 lines 19 kB history raw
1module Language.Reflection
3import Builtins
4import Prelude.Applicative
5import Prelude.Basics
6import Prelude.Foldable
7import Prelude.Functor
8import Prelude.List
9import Prelude.Nat
10import Prelude.Traversable
12%access public
14data TTName =
15 ||| A user-provided name
16 UN String |
17 ||| A name in some namespace.
18 |||
19 ||| The namespace is in reverse order, so `(NS (UN "foo") ["B", "A"])` represents the name `A.B.foo`
20 NS TTName (List String) |
21 ||| Machine-chosen names
22 MN Int String |
23 ||| Name of something which is never used in scope
24 NErased
25%name TTName n, n'
27implicit
28userSuppliedName : String -> TTName
29userSuppliedName = UN
31data TTUExp =
32 ||| Universe variable
33 UVar Int |
34 ||| Explicit universe level
35 UVal Int
36%name TTUExp uexp
38data NativeTy = IT8 | IT16 | IT32 | IT64
40data IntTy = ITFixed NativeTy | ITNative | ITBig | ITChar
42data ArithTy = ATInt Language.Reflection.IntTy | ATFloat
44||| Primitive constants
45data Const = I Int | BI Integer | Fl Float | Ch Char | Str String
46 | B8 Bits8 | B16 Bits16 | B32 Bits32 | B64 Bits64
47 | AType ArithTy | StrType
48 | VoidType | Forgot
49 | WorldType | TheWorld
50%name Const c, c'
52abstract class ReflConst (a : Type) where
53 toConst : a -> Const
55instance ReflConst Int where
56 toConst x = I x
58instance ReflConst Integer where
59 toConst = BI
61instance ReflConst Float where
62 toConst = Fl
64instance ReflConst Char where
65 toConst = Ch
67instance ReflConst String where
68 toConst = Str
70instance ReflConst Bits8 where
71 toConst = B8
73instance ReflConst Bits16 where
74 toConst = B16
76instance ReflConst Bits32 where
77 toConst = B32
79instance ReflConst Bits64 where
80 toConst = B64
82implicit
83reflectConstant: (ReflConst a) => a -> Const
84reflectConstant = toConst
87||| Types of named references
88data NameType =
89 ||| A reference which is just bound, e.g. by intro
90 Bound |
91 ||| A reference to a de Bruijn-indexed variable
92 Ref |
93 ||| Data constructor with tag and number
94 DCon Int Int |
95 ||| Type constructor with tag and number
96 TCon Int Int
98%name NameType nt, nt'
100||| Types annotations for bound variables in different
101||| binding contexts
102data Binder a = Lam a
103 | Pi a a
104 | Let a a
105 | NLet a a
106 | Hole a
107 | GHole a
108 | Guess a a
109 | PVar a
110 | PVTy a
111%name Binder b, b'
113instance Functor Binder where
114 map f (Lam x) = Lam (f x)
115 map f (Pi x k) = Pi (f x) (f k)
116 map f (Let x y) = Let (f x) (f y)
117 map f (NLet x y) = NLet (f x) (f y)
118 map f (Hole x) = Hole (f x)
119 map f (GHole x) = GHole (f x)
120 map f (Guess x y) = Guess (f x) (f y)
121 map f (PVar x) = PVar (f x)
122 map f (PVTy x) = PVTy (f x)
124instance Foldable Binder where
125 foldr f z (Lam x) = f x z
126 foldr f z (Pi x k) = f x (f k z)
127 foldr f z (Let x y) = f x (f y z)
128 foldr f z (NLet x y) = f x (f y z)
129 foldr f z (Hole x) = f x z
130 foldr f z (GHole x) = f x z
131 foldr f z (Guess x y) = f x (f y z)
132 foldr f z (PVar x) = f x z
133 foldr f z (PVTy x) = f x z
135instance Traversable Binder where
136 traverse f (Lam x) = [| Lam (f x) |]
137 traverse f (Pi x k) = [| Pi (f x) (f k) |]
138 traverse f (Let x y) = [| Let (f x) (f y) |]
139 traverse f (NLet x y) = [| NLet (f x) (f y) |]
140 traverse f (Hole x) = [| Hole (f x) |]
141 traverse f (GHole x) = [| GHole (f x) |]
142 traverse f (Guess x y) = [| Guess (f x) (f y) |]
143 traverse f (PVar x) = [| PVar (f x) |]
144 traverse f (PVTy x) = [| PVTy (f x) |]
146||| Universes
147data Universe = NullType | UniqueType | AllTypes
149||| Reflection of the well typed core language
150data TT =
151 ||| A reference to some name (P for Parameter)
152 P NameType TTName TT |
153 ||| de Bruijn variables
154 V Int |
155 ||| Bind a variable
156 Bind TTName (Binder TT) TT |
157 ||| Apply one term to another
158 App TT TT |
159 ||| Embed a constant
160 TConst Const |
161 ||| Argument projection; runtime only
162 Proj TT Int |
163 ||| Erased terms
164 Erased |
165 ||| Impossible terms
166 Impossible |
167 ||| The type of types along (with universe constraints)
168 TType TTUExp |
169 UType Universe
170%name TT tm, tm'
172||| Raw terms without types
173data Raw =
174 ||| Variables, global or local
175 Var TTName |
176 ||| Bind a variable
177 RBind TTName (Binder Raw) Raw |
178 ||| Application
179 RApp Raw Raw |
180 ||| The type of types
181 RType |
182 RUType Universe |
183 RForce Raw |
184 ||| Embed a constant
185 RConstant Const
186%name Raw tm, tm'
188data SourceLocation : Type where
189 FileLoc : (filename : String) -> (start : (Int, Int)) -> (end : (Int, Int)) -> SourceLocation
191%name SourceLocation loc
193||| Error reports are a list of report parts
194data ErrorReportPart =
195 ||| A human-readable string
196 TextPart String |
197 ||| An Idris name (to be semantically coloured)
198 NamePart TTName |
199 ||| An Idris term, to be pretty printed
200 TermPart TT |
201 ||| An indented sub-report, to provide more details
202 SubReport (List ErrorReportPart)
203%name ErrorReportPart part, p
205||| A representation of Idris's tactics that can be returned from custom
206||| tactic implementations. Generate these using `applyTactic`.
207data Tactic =
208 ||| Try the first tactic and resort to the second one on failure
209 Try Tactic Tactic |
210 ||| Only run if the goal has the right type
211 GoalType String Tactic |
212 ||| Resolve function name, find matching arguments in the
213 ||| context and compute the proof target
214 Refine TTName |
215 ||| Apply both tactics in sequence
216 Seq Tactic Tactic |
217 ||| Introduce a new hole with a particular type
218 Claim TTName TT |
219 ||| Move the current hole to the end
220 Unfocus |
221 ||| Intelligently construct the proof target from the context
222 Trivial |
223 ||| Build a proof by applying contructors up to a maximum depth
224 Search Int |
225 ||| Resolve a type class
226 Instance |
227 ||| Infer the proof target from the context
228 Solve |
229 ||| introduce all variables into the context
230 Intros |
231 ||| Introduce a named variable into the context, use the
232 ||| first one if the given name is not found
233 Intro TTName |
234 ||| Invoke the reflected rep. of another tactic
235 ApplyTactic TT |
236 ||| Turn a value into its reflected representation
237 Reflect TT |
238 ||| Use a `%reflection` function
239 ByReflection TT |
240 ||| Turn a raw value back into a term
241 Fill Raw |
242 ||| Use the given value to conclude the proof
243 Exact TT |
244 ||| Focus on a particular hole
245 Focus TTName |
246 ||| Rewrite with an equality
247 Rewrite TT |
248 ||| Perform induction on a particular expression
249 Induction TT |
250 ||| Perform case analysis on a particular expression
251 Case TT |
252 ||| Name a reflected term
253 LetTac TTName TT |
254 ||| Name a reflected term and type it
255 LetTacTy TTName TT TT |
256 ||| Normalise the goal
257 Compute |
258 ||| Do nothing
259 Skip |
260 ||| Fail with an error message
261 Fail (List ErrorReportPart) |
262 ||| Attempt to fill the hole with source code information
263 SourceFC
264%name Tactic tac, tac'
267||| Things with a canonical representation as a reflected term.
268|||
269||| This type class is intended to be used during proof automation and the
270||| construction of custom tactics.
271|||
272||| @ a the type to be quoted
273||| @ t the type to quote it to (typically `TT` or `Raw`)
274class Quotable a t where
275 ||| A representation of the type `a`.
276 |||
277 ||| This is to enable quoting polymorphic datatypes
278 quotedTy : t
280 ||| Quote a particular element of `a`.
281 |||
282 ||| Each equation should look something like ```quote (Foo x y) = `(Foo ~(quote x) ~(quote y))```
283 quote : a -> t
285instance Quotable Nat TT where
286 quotedTy = `(Nat)
288 quote Z = `(Z)
289 quote (S k) = `(S ~(quote k))
291instance Quotable Nat Raw where
292 quotedTy = `(Nat)
294 quote Z = `(Z)
295 quote (S k) = `(S ~(quote k))
297instance Quotable Int TT where
298 quotedTy = `(Int)
299 quote x = TConst (I x)
301instance Quotable Int Raw where
302 quotedTy = `(Int)
303 quote x = RConstant (I x)
305instance Quotable Float TT where
306 quotedTy = `(Float)
307 quote x = TConst (Fl x)
309instance Quotable Float Raw where
310 quotedTy = `(Float)
311 quote x = RConstant (Fl x)
313instance Quotable Char TT where
314 quotedTy = `(Char)
315 quote x = TConst (Ch x)
317instance Quotable Char Raw where
318 quotedTy = `(Char)
319 quote x = RConstant (Ch x)
321instance Quotable Bits8 TT where
322 quotedTy = `(Bits8)
323 quote x = TConst (B8 x)
325instance Quotable Bits8 Raw where
326 quotedTy = `(Bits8)
327 quote x = RConstant (B8 x)
329instance Quotable Bits16 TT where
330 quotedTy = `(Bits16)
331 quote x = TConst (B16 x)
333instance Quotable Bits16 Raw where
334 quotedTy = `(Bits16)
335 quote x = RConstant (B16 x)
337instance Quotable Bits32 TT where
338 quotedTy = `(Bits32)
339 quote x = TConst (B32 x)
341instance Quotable Bits32 Raw where
342 quotedTy = `(Bits32)
343 quote x = RConstant (B32 x)
345instance Quotable Bits64 TT where
346 quotedTy = `(Bits64)
347 quote x = TConst (B64 x)
349instance Quotable Bits64 Raw where
350 quotedTy = `(Bits64)
351 quote x = RConstant (B64 x)
353instance Quotable Integer TT where
354 quotedTy = `(Integer)
355 quote x = TConst (BI x)
357instance Quotable Integer Raw where
358 quotedTy = `(Integer)
359 quote x = RConstant (BI x)
361instance Quotable String TT where
362 quotedTy = `(String)
363 quote x = TConst (Str x)
365instance Quotable String Raw where
366 quotedTy = `(String)
367 quote x = RConstant (Str x)
369instance Quotable NameType TT where
370 quotedTy = `(NameType)
371 quote Bound = `(Bound)
372 quote Ref = `(Ref)
373 quote (DCon x y) = `(DCon ~(quote x) ~(quote y))
374 quote (TCon x y) = `(TCon ~(quote x) ~(quote y))
376instance Quotable NameType Raw where
377 quotedTy = `(NameType)
378 quote Bound = `(Bound)
379 quote Ref = `(Ref)
380 quote (DCon x y) = `(DCon ~(quote {t=Raw} x) ~(quote {t=Raw} y))
381 quote (TCon x y) = `(TCon ~(quote {t=Raw} x) ~(quote {t=Raw} y))
383instance Quotable a TT => Quotable (List a) TT where
384 quotedTy = `(List ~(quotedTy {a}))
385 quote [] = `(List.Nil {a=~(quotedTy {a})})
386 quote (x :: xs) = `(List.(::) {a=~(quotedTy {a})} ~(quote x) ~(quote xs))
388instance Quotable a Raw => Quotable (List a) Raw where
389 quotedTy = `(List ~(quotedTy {a}))
390 quote [] = `(List.Nil {a=~(quotedTy {a})})
391 quote (x :: xs) = `(List.(::) {a=~(quotedTy {a})} ~(quote x) ~(quote xs))
393instance Quotable TTName TT where
394 quotedTy = `(TTName)
395 quote (UN x) = `(UN ~(quote x))
396 quote (NS n xs) = `(NS ~(quote n) ~(quote xs))
397 quote (MN x y) = `(MN ~(quote x) ~(quote y))
398 quote NErased = `(NErased)
400instance Quotable TTName Raw where
401 quotedTy = `(TTName)
402 quote (UN x) = `(UN ~(quote {t=Raw} x))
403 quote (NS n xs) = `(NS ~(quote {t=Raw} n) ~(quote {t=Raw} xs))
404 quote (MN x y) = `(MN ~(quote {t=Raw} x) ~(quote {t=Raw} y))
405 quote NErased = `(NErased)
407instance Quotable NativeTy TT where
408 quotedTy = `(NativeTy)
409 quote IT8 = `(Reflection.IT8)
410 quote IT16 = `(Reflection.IT16)
411 quote IT32 = `(Reflection.IT32)
412 quote IT64 = `(Reflection.IT64)
414instance Quotable NativeTy Raw where
415 quotedTy = `(NativeTy)
416 quote IT8 = `(Reflection.IT8)
417 quote IT16 = `(Reflection.IT16)
418 quote IT32 = `(Reflection.IT32)
419 quote IT64 = `(Reflection.IT64)
421instance Quotable Reflection.IntTy TT where
422 quotedTy = `(Reflection.IntTy)
423 quote (ITFixed x) = `(ITFixed ~(quote x))
424 quote ITNative = `(Reflection.ITNative)
425 quote ITBig = `(ITBig)
426 quote ITChar = `(Reflection.ITChar)
428instance Quotable Reflection.IntTy Raw where
429 quotedTy = `(Reflection.IntTy)
430 quote (ITFixed x) = `(ITFixed ~(quote {t=Raw} x))
431 quote ITNative = `(Reflection.ITNative)
432 quote ITBig = `(ITBig)
433 quote ITChar = `(Reflection.ITChar)
435instance Quotable ArithTy TT where
436 quotedTy = `(ArithTy)
437 quote (ATInt x) = `(ATInt ~(quote x))
438 quote ATFloat = `(ATFloat)
440instance Quotable ArithTy Raw where
441 quotedTy = `(ArithTy)
442 quote (ATInt x) = `(ATInt ~(quote {t=Raw} x))
443 quote ATFloat = `(ATFloat)
445instance Quotable Const TT where
446 quotedTy = `(Const)
447 quote (I x) = `(I ~(quote x))
448 quote (BI x) = `(BI ~(quote x))
449 quote (Fl x) = `(Fl ~(quote x))
450 quote (Ch x) = `(Ch ~(quote x))
451 quote (Str x) = `(Str ~(quote x))
452 quote (B8 x) = `(B8 ~(quote x))
453 quote (B16 x) = `(B16 ~(quote x))
454 quote (B32 x) = `(B32 ~(quote x))
455 quote (B64 x) = `(B64 ~(quote x))
456 quote (AType x) = `(AType ~(quote x))
457 quote StrType = `(StrType)
458 quote VoidType = `(VoidType)
459 quote Forgot = `(Forgot)
460 quote WorldType = `(WorldType)
461 quote TheWorld = `(TheWorld)
463instance Quotable Const Raw where
464 quotedTy = `(Const)
465 quote (I x) = `(I ~(quote {t=Raw} x))
466 quote (BI x) = `(BI ~(quote {t=Raw} x))
467 quote (Fl x) = `(Fl ~(quote {t=Raw} x))
468 quote (Ch x) = `(Ch ~(quote {t=Raw} x))
469 quote (Str x) = `(Str ~(quote {t=Raw} x))
470 quote (B8 x) = `(B8 ~(quote {t=Raw} x))
471 quote (B16 x) = `(B16 ~(quote {t=Raw} x))
472 quote (B32 x) = `(B32 ~(quote {t=Raw} x))
473 quote (B64 x) = `(B64 ~(quote {t=Raw} x))
474 quote (AType x) = `(AType ~(quote {t=Raw} x))
475 quote StrType = `(StrType)
476 quote VoidType = `(VoidType)
477 quote Forgot = `(Forgot)
478 quote WorldType = `(WorldType)
479 quote TheWorld = `(TheWorld)
481instance Quotable TTUExp TT where
482 quotedTy = `(TTUExp)
483 quote (UVar x) = `(UVar ~(quote x))
484 quote (UVal x) = `(UVal ~(quote x))
486instance Quotable TTUExp Raw where
487 quotedTy = `(TTUExp)
488 quote (UVar x) = `(UVar ~(quote {t=Raw} x))
489 quote (UVal x) = `(UVal ~(quote {t=Raw} x))
491instance Quotable Universe TT where
492 quotedTy = `(Universe)
493 quote Reflection.NullType = `(NullType)
494 quote Reflection.UniqueType = `(UniqueType)
495 quote Reflection.AllTypes = `(AllTypes)
497instance Quotable Universe Raw where
498 quotedTy = `(Universe)
499 quote Reflection.NullType = `(NullType)
500 quote Reflection.UniqueType = `(UniqueType)
501 quote Reflection.AllTypes = `(AllTypes)
503mutual
504 instance Quotable TT TT where
505 quotedTy = `(TT)
506 quote (P nt n tm) = `(P ~(quote nt) ~(quote n) ~(quote tm))
507 quote (V x) = `(V ~(quote x))
508 quote (Bind n b tm) = `(Bind ~(quote n) ~(assert_total (quote b)) ~(quote tm))
509 quote (App f x) = `(App ~(quote f) ~(quote x))
510 quote (TConst c) = `(TConst ~(quote c))
511 quote (Proj tm x) = `(Proj ~(quote tm) ~(quote x))
512 quote Erased = `(Erased)
513 quote Impossible = `(Impossible)
514 quote (TType uexp) = `(TType ~(quote uexp))
515 quote (UType u) = `(UType ~(quote u))
517 instance Quotable (Binder TT) TT where
518 quotedTy = `(Binder TT)
519 quote (Lam x) = `(Lam {a=TT} ~(assert_total (quote x)))
520 quote (Pi x k) = `(Pi {a=TT} ~(assert_total (quote x))
521 ~(assert_total (quote k)))
522 quote (Let x y) = `(Let {a=TT} ~(assert_total (quote x))
523 ~(assert_total (quote y)))
524 quote (NLet x y) = `(NLet {a=TT} ~(assert_total (quote x))
525 ~(assert_total (quote y)))
526 quote (Hole x) = `(Hole {a=TT} ~(assert_total (quote x)))
527 quote (GHole x) = `(GHole {a=TT} ~(assert_total (quote x)))
528 quote (Guess x y) = `(Guess {a=TT} ~(assert_total (quote x))
529 ~(assert_total (quote y)))
530 quote (PVar x) = `(PVar {a=TT} ~(assert_total (quote x)))
531 quote (PVTy x) = `(PVTy {a=TT} ~(assert_total (quote x)))
534instance Quotable ErrorReportPart TT where
535 quotedTy = `(ErrorReportPart)
536 quote (TextPart x) = `(TextPart ~(quote x))
537 quote (NamePart n) = `(NamePart ~(quote n))
538 quote (TermPart tm) = `(TermPart ~(quote tm))
539 quote (SubReport xs) = `(SubReport ~(assert_total $ quote xs))
541mutual
542 quoteRaw : Raw -> TT
543 quoteRaw (Var n) = `(Var ~(quote n))
544 quoteRaw (RBind n b tm) = `(RBind ~(quote n) ~(assert_total $ quoteRawBinder b) ~(quoteRaw tm))
545 quoteRaw (RApp tm tm') = `(RApp ~(quoteRaw tm) ~(quoteRaw tm'))
546 quoteRaw RType = `(RType)
547 quoteRaw (RUType u) = `(RUType ~(quote u))
548 quoteRaw (RForce tm) = `(RForce ~(quoteRaw tm))
549 quoteRaw (RConstant c) = `(RConstant ~(quote c))
551 quoteRawBinder : Binder Raw -> TT
552 quoteRawBinder (Lam x) = `(Lam {a=Raw} ~(quoteRaw x))
553 quoteRawBinder (Pi x k) = `(Pi {a=Raw} ~(quoteRaw x) ~(quoteRaw k))
554 quoteRawBinder (Let x y) = `(Let {a=Raw} ~(quoteRaw x) ~(quoteRaw y))
555 quoteRawBinder (NLet x y) = `(NLet {a=Raw} ~(quoteRaw x) ~(quoteRaw y))
556 quoteRawBinder (Hole x) = `(Hole {a=Raw} ~(quoteRaw x))
557 quoteRawBinder (GHole x) = `(GHole {a=Raw} ~(quoteRaw x))
558 quoteRawBinder (Guess x y) = `(Guess {a=Raw} ~(quoteRaw x) ~(quoteRaw y))
559 quoteRawBinder (PVar x) = `(PVar {a=Raw} ~(quoteRaw x))
560 quoteRawBinder (PVTy x) = `(PVTy {a=Raw} ~(quoteRaw x))
562instance Quotable Raw TT where
563 quotedTy = `(Raw)
564 quote = quoteRaw
566instance Quotable (Binder Raw) TT where
567 quotedTy = `(Binder Raw)
568 quote = quoteRawBinder
570instance Quotable Tactic TT where
571 quotedTy = `(Tactic)
572 quote (Try tac tac') = `(Try ~(quote tac) ~(quote tac'))
573 quote (GoalType x tac) = `(GoalType ~(quote x) ~(quote tac))
574 quote (Refine n) = `(Refine ~(quote n))
575 quote (Claim n ty) = `(Claim ~(quote n) ~(quote ty))
576 quote Unfocus = `(Unfocus)
577 quote (Seq tac tac') = `(Seq ~(quote tac) ~(quote tac'))
578 quote Trivial = `(Trivial)
579 quote (Search x) = `(Search ~(quote x))
580 quote Instance = `(Instance)
581 quote Solve = `(Solve)
582 quote Intros = `(Intros)
583 quote (Intro n) = `(Intro ~(quote n))
584 quote (ApplyTactic tm) = `(ApplyTactic ~(quote tm))
585 quote (Reflect tm) = `(Reflect ~(quote tm))
586 quote (ByReflection tm) = `(ByReflection ~(quote tm))
587 quote (Fill tm) = `(Fill ~(quote tm))
588 quote (Exact tm) = `(Exact ~(quote tm))
589 quote (Focus n) = `(Focus ~(quote n))
590 quote (Rewrite tm) = `(Rewrite ~(quote tm))
591 quote (Induction tm) = `(Induction ~(quote tm))
592 quote (Case tm) = `(Case ~(quote tm))
593 quote (LetTac n tm) = `(LetTac ~(quote n) ~(quote tm))
594 quote (LetTacTy n tm tm') = `(LetTacTy ~(quote n) ~(quote tm) ~(quote tm'))
595 quote Compute = `(Compute)
596 quote Skip = `(Skip)
597 quote (Fail xs) = `(Fail ~(quote xs))
598 quote SourceFC = `(SourceFC)
601instance Quotable SourceLocation TT where
602 quotedTy = `(SourceLocation)
603 quote (FileLoc fn (sl, sc) (el, ec)) =
604 `(FileLoc ~(quote fn)
605 (~(quote sl), ~(quote sc))
606 (~(quote el), ~(quote ec)))
608instance Quotable SourceLocation Raw where
609 quotedTy = `(SourceLocation)
610 quote (FileLoc fn (sl, sc) (el, ec)) =
611 `(FileLoc ~(quote {t=Raw} fn)
612 (~(quote {t=Raw} sl), ~(quote {t=Raw} sc))
613 (~(quote {t=Raw} el), ~(quote {t=Raw} ec)))