git.iko.soy/Idris-dev
on 7afa310 help sign in
Idris-dev/libs/base/Language/Reflection.idr
479 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'
178||| Error reports are a list of report parts
179data ErrorReportPart =
180 ||| A human-readable string
181 TextPart String |
182 ||| An Idris name (to be semantically coloured)
183 NamePart TTName |
184 ||| An Idris term, to be pretty printed
185 TermPart TT |
186 ||| An indented sub-report, to provide more details
187 SubReport (List ErrorReportPart)
188%name ErrorReportPart part, p
190||| A representation of Idris's tactics that can be returned from custom
191||| tactic implementations. Generate these using `applyTactic`.
192data Tactic =
193 ||| Try the first tactic and resort to the second one on failure
194 Try Tactic Tactic |
195 ||| Only run if the goal has the right type
196 GoalType String Tactic |
197 ||| Resolve function name, find matching arguments in the
198 ||| context and compute the proof target
199 Refine TTName |
200 ||| Apply both tactics in sequence
201 Seq Tactic Tactic |
202 ||| Intelligently construct the proof target from the context
203 Trivial |
204 ||| Build a proof by applying contructors up to a maximum depth
205 Search Int |
206 ||| Resolve a type class
207 Instance |
208 ||| Infer the proof target from the context
209 Solve |
210 ||| introduce all variables into the context
211 Intros |
212 ||| Introduce a named variable into the context, use the
213 ||| first one if the given name is not found
214 Intro TTName |
215 ||| Invoke the reflected rep. of another tactic
216 ApplyTactic TT |
217 ||| Turn a value into its reflected representation
218 Reflect TT |
219 ||| Use a `%reflection` function
220 ByReflection TT |
221 ||| Turn a raw value back into a term
222 Fill Raw |
223 ||| Use the given value to conclude the proof
224 Exact TT |
225 ||| Focus on a particular hole
226 Focus TTName |
227 ||| Rewrite with an equality
228 Rewrite TT |
229 ||| Perform induction on a particular expression
230 Induction TT |
231 ||| Perform case analysis on a particular expression
232 Case TT |
233 ||| Name a reflected term
234 LetTac TTName TT |
235 ||| Name a reflected term and type it
236 LetTacTy TTName TT TT |
237 ||| Normalise the goal
238 Compute |
239 ||| Do nothing
240 Skip |
241 ||| Fail with an error message
242 Fail (List ErrorReportPart)
243%name Tactic tac, tac'
246||| Things with a canonical representation in the TT datatype.
247|||
248||| This type class is intended to be used during proof automation and the
249||| construction of custom tactics.
250|||
251||| @ a the type to be quoted
252class Quotable a where
253 ||| A representation of the type `a`.
254 |||
255 ||| This is to enable quoting polymorphic datatypes
256 quotedTy : TT
258 ||| Quote a particular element of `a`.
259 |||
260 ||| Each equation should look something like ```quote (Foo x y) = `(Foo ~(quote x) ~(quote y))```
261 quote : a -> TT
263instance Quotable Nat where
264 quotedTy = `(Nat)
266 quote Z = `(Z)
267 quote (S k) = `(S ~(quote k))
269instance Quotable Int where
270 quotedTy = `(Int)
271 quote x = TConst (I x)
273instance Quotable Float where
274 quotedTy = `(Float)
275 quote x = TConst (Fl x)
277instance Quotable Char where
278 quotedTy = `(Char)
279 quote x = TConst (Ch x)
281instance Quotable Bits8 where
282 quotedTy = `(Bits8)
283 quote x = TConst (B8 x)
285instance Quotable Bits16 where
286 quotedTy = `(Bits16)
287 quote x = TConst (B16 x)
289instance Quotable Bits32 where
290 quotedTy = `(Bits32)
291 quote x = TConst (B32 x)
293instance Quotable Bits64 where
294 quotedTy = `(Bits64)
295 quote x = TConst (B64 x)
297instance Quotable Integer where
298 quotedTy = `(Integer)
299 quote x = TConst (BI x)
301instance Quotable Bits8x16 where
302 quotedTy = `(Bits8x16)
303 quote x = TConst (B8V x)
305instance Quotable Bits16x8 where
306 quotedTy = `(Bits16x8)
307 quote x = TConst (B16V x)
309instance Quotable Bits32x4 where
310 quotedTy = `(Bits32x4)
311 quote x = TConst (B32V x)
313instance Quotable Bits64x2 where
314 quotedTy = `(Bits64x2)
315 quote x = TConst (B64V x)
317instance Quotable String where
318 quotedTy = `(String)
319 quote x = TConst (Str x)
321instance Quotable NameType where
322 quotedTy = `(NameType)
323 quote Bound = `(Bound)
324 quote Ref = `(Ref)
325 quote (DCon x y) = `(DCon ~(quote x) ~(quote y))
326 quote (TCon x y) = `(TCon ~(quote x) ~(quote y))
328instance Quotable a => Quotable (List a) where
329 quotedTy = `(List ~(quotedTy {a=a}))
330 quote [] = `(List.Nil {a=~quotedTy})
331 quote (x :: xs) = `(List.(::) {a=~quotedTy} ~(quote x) ~(quote xs))
333instance Quotable TTName where
334 quotedTy = `(TTName)
335 quote (UN x) = `(UN ~(quote x))
336 quote (NS n xs) = `(NS ~(quote n) ~(quote xs))
337 quote (MN x y) = `(MN ~(quote x) ~(quote y))
338 quote NErased = `(NErased)
340instance Quotable NativeTy where
341 quotedTy = `(NativeTy)
342 quote IT8 = `(Reflection.IT8)
343 quote IT16 = `(Reflection.IT16)
344 quote IT32 = `(Reflection.IT32)
345 quote IT64 = `(Reflection.IT64)
347instance Quotable Reflection.IntTy where
348 quotedTy = `(Reflection.IntTy)
349 quote (ITFixed x) = `(ITFixed ~(quote x))
350 quote ITNative = `(Reflection.ITNative)
351 quote ITBig = `(ITBig)
352 quote ITChar = `(Reflection.ITChar)
353 quote (ITVec x y) = `(ITVec ~(quote x) ~(quote y))
355instance Quotable ArithTy where
356 quotedTy = `(ArithTy)
357 quote (ATInt x) = `(ATInt ~(quote x))
358 quote ATFloat = `(ATFloat)
360instance Quotable Const where
361 quotedTy = `(Const)
362 quote (I x) = `(I ~(quote x))
363 quote (BI x) = `(BI ~(quote x))
364 quote (Fl x) = `(Fl ~(quote x))
365 quote (Ch x) = `(Ch ~(quote x))
366 quote (Str x) = `(Str ~(quote x))
367 quote (B8 x) = `(B8 ~(quote x))
368 quote (B16 x) = `(B16 ~(quote x))
369 quote (B32 x) = `(B32 ~(quote x))
370 quote (B64 x) = `(B64 ~(quote x))
371 quote (B8V xs) = `(B8V ~(quote xs))
372 quote (B16V xs) = `(B16V ~(quote xs))
373 quote (B32V xs) = `(B32V ~(quote xs))
374 quote (B64V xs) = `(B64V ~(quote xs))
375 quote (AType x) = `(AType ~(quote x))
376 quote StrType = `(StrType)
377 quote PtrType = `(PtrType)
378 quote ManagedPtrType = `(ManagedPtrType)
379 quote BufferType = `(BufferType)
380 quote VoidType = `(VoidType)
381 quote Forgot = `(Forgot)
384instance Quotable TTUExp where
385 quotedTy = `(TTUExp)
386 quote (UVar x) = `(UVar ~(quote x))
387 quote (UVal x) = `(UVal ~(quote x))
389mutual
390 instance Quotable TT where
391 quotedTy = `(TT)
392 quote (P nt n tm) = `(P ~(quote nt) ~(quote n) ~(quote tm))
393 quote (V x) = `(V ~(quote x))
394 quote (Bind n b tm) = `(Bind ~(quote n) ~(assert_total (quote b)) ~(quote tm))
395 quote (App f x) = `(App ~(quote f) ~(quote x))
396 quote (TConst c) = `(TConst ~(quote c))
397 quote (Proj tm x) = `(Proj ~(quote tm) ~(quote x))
398 quote Erased = `(Erased)
399 quote Impossible = `(Impossible)
400 quote (TType uexp) = `(TType ~(quote uexp))
402 instance Quotable (Binder TT) where
403 quotedTy = `(Binder TT)
404 quote (Lam x) = `(Lam {a=TT} ~(assert_total (quote x)))
405 quote (Pi x k) = `(Pi {a=TT} ~(assert_total (quote x))
406 ~(assert_total (quote k)))
407 quote (Let x y) = `(Let {a=TT} ~(assert_total (quote x))
408 ~(assert_total (quote y)))
409 quote (NLet x y) = `(NLet {a=TT} ~(assert_total (quote x))
410 ~(assert_total (quote y)))
411 quote (Hole x) = `(Hole {a=TT} ~(assert_total (quote x)))
412 quote (GHole x) = `(GHole {a=TT} ~(assert_total (quote x)))
413 quote (Guess x y) = `(Guess {a=TT} ~(assert_total (quote x))
414 ~(assert_total (quote y)))
415 quote (PVar x) = `(PVar {a=TT} ~(assert_total (quote x)))
416 quote (PVTy x) = `(PVTy {a=TT} ~(assert_total (quote x)))
419instance Quotable ErrorReportPart where
420 quotedTy = `(ErrorReportPart)
421 quote (TextPart x) = `(TextPart ~(quote x))
422 quote (NamePart n) = `(NamePart ~(quote n))
423 quote (TermPart tm) = `(TermPart ~(quote tm))
424 quote (SubReport xs) = `(SubReport ~(assert_total $ quote xs))
426mutual
427 quoteRaw : Raw -> TT
428 quoteRaw (Var n) = `(Var ~(quote n))
429 quoteRaw (RBind n b tm) = `(RBind ~(quote n) ~(assert_total $ quoteRawBinder b) ~(quoteRaw tm))
430 quoteRaw (RApp tm tm') = `(RApp ~(quoteRaw tm) ~(quoteRaw tm'))
431 quoteRaw RType = `(RType)
432 quoteRaw (RForce tm) = `(RForce ~(quoteRaw tm))
433 quoteRaw (RConstant c) = `(RConstant ~(quote c))
435 quoteRawBinder : Binder Raw -> TT
436 quoteRawBinder (Lam x) = `(Lam {a=Raw} ~(quoteRaw x))
437 quoteRawBinder (Pi x k) = `(Pi {a=Raw} ~(quoteRaw x) ~(quoteRaw k))
438 quoteRawBinder (Let x y) = `(Let {a=Raw} ~(quoteRaw x) ~(quoteRaw y))
439 quoteRawBinder (NLet x y) = `(NLet {a=Raw} ~(quoteRaw x) ~(quoteRaw y))
440 quoteRawBinder (Hole x) = `(Hole {a=Raw} ~(quoteRaw x))
441 quoteRawBinder (GHole x) = `(GHole {a=Raw} ~(quoteRaw x))
442 quoteRawBinder (Guess x y) = `(Guess {a=Raw} ~(quoteRaw x) ~(quoteRaw y))
443 quoteRawBinder (PVar x) = `(PVar {a=Raw} ~(quoteRaw x))
444 quoteRawBinder (PVTy x) = `(PVTy {a=Raw} ~(quoteRaw x))
446instance Quotable Raw where
447 quotedTy = `(Raw)
448 quote = quoteRaw
450instance Quotable (Binder Raw) where
451 quotedTy = `(Binder Raw)
452 quote = quoteRawBinder
454instance Quotable Tactic where
455 quotedTy = `(Tactic)
456 quote (Try tac tac') = `(Try ~(quote tac) ~(quote tac'))
457 quote (GoalType x tac) = `(GoalType ~(quote x) ~(quote tac))
458 quote (Refine n) = `(Refine ~(quote n))
459 quote (Seq tac tac') = `(Seq ~(quote tac) ~(quote tac'))
460 quote Trivial = `(Trivial)
461 quote (Search x) = `(Search ~(quote x))
462 quote Instance = `(Instance)
463 quote Solve = `(Solve)
464 quote Intros = `(Intros)
465 quote (Intro n) = `(Intro ~(quote n))
466 quote (ApplyTactic tm) = `(ApplyTactic ~(quote tm))
467 quote (Reflect tm) = `(Reflect ~(quote tm))
468 quote (ByReflection tm) = `(ByReflection ~(quote tm))
469 quote (Fill tm) = `(Fill ~(quote tm))
470 quote (Exact tm) = `(Exact ~(quote tm))
471 quote (Focus n) = `(Focus ~(quote n))
472 quote (Rewrite tm) = `(Rewrite ~(quote tm))
473 quote (Induction tm) = `(Induction ~(quote tm))
474 quote (Case tm) = `(Case ~(quote tm))
475 quote (LetTac n tm) = `(LetTac ~(quote n) ~(quote tm))
476 quote (LetTacTy n tm tm') = `(LetTacTy ~(quote n) ~(quote tm) ~(quote tm'))
477 quote Compute = `(Compute)
478 quote Skip = `(Skip)
479 quote (Fail xs) = `(Fail ~(quote xs))