git.iko.soy/Idris-dev
on master help sign in
Merge pull request #3085 from david-christiansen/ttname-deceq
6076be4David Christiansen
CHANGELOG.md+5
compare with master
unifiedsplit
@@ -10,6 +10,11 @@
10* Remove deprecated options `--ideslave` and `--ideslave-socket`. These options
10* Remove deprecated options `--ideslave` and `--ideslave-socket`. These options
11 were replaced with `--ide-mode` and `--ide-mode-socket` in 0.9.17
11 were replaced with `--ide-mode` and `--ide-mode-socket` in 0.9.17
12
12
13+## Reflection changes
14+* The implicit coercion from String to TTName was removed.
15+
16+* Decidable equality for TTName is available.
17+
13# New in 0.11
18# New in 0.11
14
19
15## Updated export rules
20## Updated export rules
libs/prelude/Language/Reflection.idr+516−4
@@ -8,6 +8,8 @@ import Prelude.Functor
8import Prelude.List
8import Prelude.List
9import Prelude.Nat
9import Prelude.Nat
10import Prelude.Traversable
10import Prelude.Traversable
11+import Prelude.Uninhabited
12+import Decidable.Equality
11
13
12%access public export
14%access public export
13
15
@@ -24,7 +26,25 @@ record SourceLocation where
24 ||| The line and column of the end of the source span
26 ||| The line and column of the end of the source span
25 end : (Int, Int)
27 end : (Int, Int)
26
28
27−%name SourceLocation loc
29+%name SourceLocation loc, loc'
30+
31+private
32+fileLocInj : (FileLoc fn s e = FileLoc fn' s' e') -> (fn = fn', s = s', e = e')
33+fileLocInj Refl = (Refl, Refl, Refl)
34+
35+implementation DecEq SourceLocation where
36+ decEq (FileLoc f s e) (FileLoc f' s' e') with (decEq f f')
37+ decEq (FileLoc f s e) (FileLoc f s' e') | Yes Refl with (decEq s s')
38+ decEq (FileLoc f s e) (FileLoc f s e') | Yes Refl | Yes Refl with (decEq e e')
39+ decEq (FileLoc f s e) (FileLoc f s e) | Yes Refl | Yes Refl | Yes Refl =
40+ Yes Refl
41+ decEq (FileLoc f s e) (FileLoc f s e') | Yes Refl | Yes Refl | No contra =
42+ No $ contra . snd . snd . fileLocInj
43+ decEq (FileLoc f s e) (FileLoc f s' e') | Yes Refl | No contra =
44+ No $ contra . fst . snd . fileLocInj
45+ decEq (FileLoc f s e) (FileLoc f' s' e') | No contra =
46+ No $ contra . fst . fileLocInj
47+
28
48
29
49
30mutual
50mutual
@@ -52,12 +72,504 @@ mutual
52 | ElimN TTName
72 | ElimN TTName
53 | InstanceCtorN TTName
73 | InstanceCtorN TTName
54 | MetaN TTName TTName
74 | MetaN TTName TTName
75+ %name SpecialName sn, sn'
76+
77+-- Rather than implement one-off private functions, we make the
78+-- disjointness of the constructors available to all Idris programs,
79+-- at the cost of a bit of scrolling here.
80+
81+implementation Uninhabited (UN _ = NS _ _) where
82+ uninhabited Refl impossible
83+
84+implementation Uninhabited (UN _ = MN _ _) where
85+ uninhabited Refl impossible
86+
87+implementation Uninhabited (UN _ = SN _) where
88+ uninhabited Refl impossible
89+
90+implementation Uninhabited (NS _ _ = UN _) where
91+ uninhabited Refl impossible
92+
93+implementation Uninhabited (NS _ _ = MN _ _) where
94+ uninhabited Refl impossible
95+
96+implementation Uninhabited (NS _ _ = SN _) where
97+ uninhabited Refl impossible
98+
99+implementation Uninhabited (MN _ _ = UN _) where
100+ uninhabited Refl impossible
101+
102+implementation Uninhabited (MN _ _ = NS _ _) where
103+ uninhabited Refl impossible
104+
105+implementation Uninhabited (MN _ _ = SN _) where
106+ uninhabited Refl impossible
107+
108+implementation Uninhabited (SN _ = UN _) where
109+ uninhabited Refl impossible
110+
111+implementation Uninhabited (SN _ = MN _ _) where
112+ uninhabited Refl impossible
113+
114+implementation Uninhabited (SN _ = NS _ _) where
115+ uninhabited Refl impossible
116+
117+implementation Uninhabited ((WhereN x n n') = (WithN y z)) where
118+ uninhabited Refl impossible
119+
120+implementation Uninhabited ((WhereN x n n') = (InstanceN y xs)) where
121+ uninhabited Refl impossible
122+
123+implementation Uninhabited ((WhereN x n n') = (ParentN y z)) where
124+ uninhabited Refl impossible
125+
126+implementation Uninhabited ((WhereN x n n') = (MethodN y)) where
127+ uninhabited Refl impossible
128+
129+implementation Uninhabited ((WhereN x n n') = (CaseN loc y)) where
130+ uninhabited Refl impossible
131+
132+implementation Uninhabited ((WhereN x n n') = (ElimN y)) where
133+ uninhabited Refl impossible
134+
135+implementation Uninhabited ((WhereN x n n') = (InstanceCtorN y)) where
136+ uninhabited Refl impossible
137+
138+implementation Uninhabited ((WhereN x n n') = (MetaN y z)) where
139+ uninhabited Refl impossible
140+
141+implementation Uninhabited ((WithN x n) = (WhereN y n' z)) where
142+ uninhabited Refl impossible
143+
144+implementation Uninhabited ((WithN x n) = (InstanceN n' xs)) where
145+ uninhabited Refl impossible
146+
147+implementation Uninhabited ((WithN x n) = (ParentN n' y)) where
148+ uninhabited Refl impossible
149+
150+implementation Uninhabited ((WithN x n) = (MethodN n')) where
151+ uninhabited Refl impossible
152+
153+implementation Uninhabited ((WithN x n) = (CaseN loc n')) where
154+ uninhabited Refl impossible
155+
156+implementation Uninhabited ((WithN x n) = (ElimN n')) where
157+ uninhabited Refl impossible
158+
159+implementation Uninhabited ((WithN x n) = (InstanceCtorN n')) where
160+ uninhabited Refl impossible
161+
162+implementation Uninhabited ((WithN x n) = (MetaN n' y)) where
163+ uninhabited Refl impossible
164+
165+implementation Uninhabited ((InstanceN n xs) = (WhereN x n' y)) where
166+ uninhabited Refl impossible
167+
168+implementation Uninhabited ((InstanceN n xs) = (WithN x n')) where
169+ uninhabited Refl impossible
170+
171+implementation Uninhabited ((InstanceN n xs) = (ParentN n' x)) where
172+ uninhabited Refl impossible
173+
174+implementation Uninhabited ((InstanceN n xs) = (MethodN n')) where
175+ uninhabited Refl impossible
176+
177+implementation Uninhabited ((InstanceN n xs) = (CaseN loc n')) where
178+ uninhabited Refl impossible
179+
180+implementation Uninhabited ((InstanceN n xs) = (ElimN n')) where
181+ uninhabited Refl impossible
182+
183+implementation Uninhabited ((InstanceN n xs) = (InstanceCtorN n')) where
184+ uninhabited Refl impossible
185+
186+implementation Uninhabited ((InstanceN n xs) = (MetaN n' x)) where
187+ uninhabited Refl impossible
188+
189+implementation Uninhabited ((ParentN n x) = (WhereN y n' z)) where
190+ uninhabited Refl impossible
191+
192+implementation Uninhabited ((ParentN n x) = (WithN y n')) where
193+ uninhabited Refl impossible
194+
195+implementation Uninhabited ((ParentN n x) = (InstanceN n' xs)) where
196+ uninhabited Refl impossible
197+
198+implementation Uninhabited ((ParentN n x) = (MethodN n')) where
199+ uninhabited Refl impossible
55
200
201+implementation Uninhabited ((ParentN n x) = (CaseN loc n')) where
202+ uninhabited Refl impossible
56
203
204+implementation Uninhabited ((ParentN n x) = (ElimN n')) where
205+ uninhabited Refl impossible
57
206
58−implicit
207+implementation Uninhabited ((ParentN n x) = (InstanceCtorN n')) where
59−userSuppliedName : String -> TTName
208+ uninhabited Refl impossible
60−userSuppliedName = UN
209+
210+implementation Uninhabited ((ParentN n x) = (MetaN n' y)) where
211+ uninhabited Refl impossible
212+
213+implementation Uninhabited ((MethodN n) = (WhereN x n' y)) where
214+ uninhabited Refl impossible
215+
216+implementation Uninhabited ((MethodN n) = (WithN x n')) where
217+ uninhabited Refl impossible
218+
219+implementation Uninhabited ((MethodN n) = (InstanceN n' xs)) where
220+ uninhabited Refl impossible
221+
222+implementation Uninhabited ((MethodN n) = (ParentN n' x)) where
223+ uninhabited Refl impossible
224+
225+implementation Uninhabited ((MethodN n) = (CaseN loc n')) where
226+ uninhabited Refl impossible
227+
228+implementation Uninhabited ((MethodN n) = (ElimN n')) where
229+ uninhabited Refl impossible
230+
231+implementation Uninhabited ((MethodN n) = (InstanceCtorN n')) where
232+ uninhabited Refl impossible
233+
234+implementation Uninhabited ((MethodN n) = (MetaN n' x)) where
235+ uninhabited Refl impossible
236+
237+implementation Uninhabited ((CaseN loc n) = (WhereN x n' y)) where
238+ uninhabited Refl impossible
239+
240+implementation Uninhabited ((CaseN loc n) = (WithN x n')) where
241+ uninhabited Refl impossible
242+
243+implementation Uninhabited ((CaseN loc n) = (InstanceN n' xs)) where
244+ uninhabited Refl impossible
245+
246+implementation Uninhabited ((CaseN loc n) = (ParentN n' x)) where
247+ uninhabited Refl impossible
248+
249+implementation Uninhabited ((CaseN loc n) = (MethodN n')) where
250+ uninhabited Refl impossible
251+
252+implementation Uninhabited ((CaseN loc n) = (ElimN n')) where
253+ uninhabited Refl impossible
254+
255+implementation Uninhabited ((CaseN loc n) = (InstanceCtorN n')) where
256+ uninhabited Refl impossible
257+
258+implementation Uninhabited ((CaseN loc n) = (MetaN n' x)) where
259+ uninhabited Refl impossible
260+
261+implementation Uninhabited ((ElimN n) = (WhereN x n' y)) where
262+ uninhabited Refl impossible
263+
264+implementation Uninhabited ((ElimN n) = (WithN x n')) where
265+ uninhabited Refl impossible
266+
267+implementation Uninhabited ((ElimN n) = (InstanceN n' xs)) where
268+ uninhabited Refl impossible
269+
270+implementation Uninhabited ((ElimN n) = (ParentN n' x)) where
271+ uninhabited Refl impossible
272+
273+implementation Uninhabited ((ElimN n) = (MethodN n')) where
274+ uninhabited Refl impossible
275+
276+implementation Uninhabited ((ElimN n) = (CaseN loc n')) where
277+ uninhabited Refl impossible
278+
279+implementation Uninhabited ((ElimN n) = (InstanceCtorN n')) where
280+ uninhabited Refl impossible
281+
282+implementation Uninhabited ((ElimN n) = (MetaN n' x)) where
283+ uninhabited Refl impossible
284+
285+implementation Uninhabited ((InstanceCtorN n) = (WhereN x n' y)) where
286+ uninhabited Refl impossible
287+
288+implementation Uninhabited ((InstanceCtorN n) = (WithN x n')) where
289+ uninhabited Refl impossible
290+
291+implementation Uninhabited ((InstanceCtorN n) = (InstanceN n' xs)) where
292+ uninhabited Refl impossible
293+
294+implementation Uninhabited ((InstanceCtorN n) = (ParentN n' x)) where
295+ uninhabited Refl impossible
296+
297+implementation Uninhabited ((InstanceCtorN n) = (MethodN n')) where
298+ uninhabited Refl impossible
299+
300+implementation Uninhabited ((InstanceCtorN n) = (CaseN loc n')) where
301+ uninhabited Refl impossible
302+
303+implementation Uninhabited ((InstanceCtorN n) = (ElimN n')) where
304+ uninhabited Refl impossible
305+
306+implementation Uninhabited ((InstanceCtorN n) = (MetaN n' x)) where
307+ uninhabited Refl impossible
308+
309+implementation Uninhabited ((MetaN n n') = (WhereN x y z)) where
310+ uninhabited Refl impossible
311+
312+implementation Uninhabited ((MetaN n n') = (WithN x y)) where
313+ uninhabited Refl impossible
314+
315+implementation Uninhabited ((MetaN n n') = (InstanceN x xs)) where
316+ uninhabited Refl impossible
317+
318+implementation Uninhabited ((MetaN n n') = (ParentN x y)) where
319+ uninhabited Refl impossible
320+
321+implementation Uninhabited ((MetaN n n') = (MethodN x)) where
322+ uninhabited Refl impossible
323+
324+implementation Uninhabited ((MetaN n n') = (CaseN loc x)) where
325+ uninhabited Refl impossible
326+
327+implementation Uninhabited ((MetaN n n') = (ElimN x)) where
328+ uninhabited Refl impossible
329+
330+implementation Uninhabited ((MetaN n n') = (InstanceCtorN x)) where
331+ uninhabited Refl impossible
332+
333+mutual
334+ private
335+ unInj : (UN x = UN y) -> x = y
336+ unInj Refl = Refl
337+
338+ private
339+ nsInj : (NS n ns = NS n' ns') -> (n = n', ns = ns')
340+ nsInj Refl = (Refl, Refl)
341+
342+ private
343+ mnInj : (MN i s = MN i' s') -> (i = i', s = s')
344+ mnInj Refl = (Refl, Refl)
345+
346+ private
347+ snInj : SN sn = SN sn' -> sn = sn'
348+ snInj Refl = Refl
349+
350+ private
351+ decTTNameEq : (n1, n2 : TTName) -> Dec (n1 = n2)
352+ decTTNameEq (UN x) (UN y) with (decEq x y)
353+ decTTNameEq (UN x) (UN y) | Yes prf =
354+ Yes (cong prf)
355+ decTTNameEq (UN x) (UN y) | No contra =
356+ No $ contra . unInj
357+ decTTNameEq (UN x) (NS n xs) = No absurd
358+ decTTNameEq (UN x) (MN y z) = No absurd
359+ decTTNameEq (UN x) (SN y) = No absurd
360+ decTTNameEq (NS n xs) (UN x) = No absurd
361+ decTTNameEq (NS n ns) (NS n' ns') with (decTTNameEq n n')
362+ decTTNameEq (NS n ns) (NS n ns') | Yes Refl with (decEq ns ns')
363+ decTTNameEq (NS n ns) (NS n ns) | Yes Refl | Yes Refl =
364+ Yes Refl
365+ decTTNameEq (NS n ns) (NS n ns') | Yes Refl | No contra =
366+ No $ contra . snd . nsInj
367+ decTTNameEq (NS n ns) (NS n' ns') | No contra =
368+ No $ contra . fst . nsInj
369+ decTTNameEq (NS n xs) (MN x y) = No absurd
370+ decTTNameEq (NS n xs) (SN x) = No absurd
371+ decTTNameEq (MN x y) (UN z) = No absurd
372+ decTTNameEq (MN x y) (NS n xs) = No absurd
373+ decTTNameEq (MN x y) (MN z w) with (decEq x z)
374+ decTTNameEq (MN x y) (MN x w) | Yes Refl with (decEq y w)
375+ decTTNameEq (MN x y) (MN x y) | Yes Refl | Yes Refl =
376+ Yes Refl
377+ decTTNameEq (MN x y) (MN x w) | Yes Refl | No contra =
378+ No $ contra . snd . mnInj
379+ decTTNameEq (MN x y) (MN z w) | No contra =
380+ No $ contra . fst . mnInj
381+ decTTNameEq (MN x y) (SN z) = No absurd
382+ decTTNameEq (SN x) (UN y) = No absurd
383+ decTTNameEq (SN x) (NS n xs) = No absurd
384+ decTTNameEq (SN x) (MN y z) = No absurd
385+ decTTNameEq (SN x) (SN y) with (decSNEq x y)
386+ decTTNameEq (SN x) (SN x) | Yes Refl = Yes Refl
387+ decTTNameEq (SN x) (SN y) | (No contra) = No $ contra . snInj
388+
389+
390+ private
391+ whereNInj : (WhereN x n n' = WhereN y z w) -> (x = y, n = z, n' = w)
392+ whereNInj Refl = (Refl, Refl, Refl)
393+
394+ private
395+ withNInj : (WithN x n = WithN y n') -> (x = y, n = n')
396+ withNInj Refl = (Refl, Refl)
397+
398+ private
399+ instanceNInj : (InstanceN n xs = InstanceN n' ys) -> (n = n', xs = ys)
400+ instanceNInj Refl = (Refl, Refl)
401+
402+ private
403+ parentNInj : (ParentN n x = ParentN n' y) -> (n = n', x = y)
404+ parentNInj Refl = (Refl, Refl)
405+
406+ private
407+ methodNInj : (MethodN n = MethodN n') -> n = n'
408+ methodNInj Refl = Refl
409+
410+ private
411+ caseNInj : (CaseN loc n = CaseN loc' n') -> (loc = loc', n = n')
412+ caseNInj Refl = (Refl, Refl)
413+
414+ private
415+ elimNInj : (ElimN n = ElimN n') -> n = n'
416+ elimNInj Refl = Refl
417+
418+ private
419+ instanceCtorNInj : (InstanceCtorN n = InstanceCtorN n') -> n = n'
420+ instanceCtorNInj Refl = Refl
421+
422+ private
423+ metaNInj : (MetaN n m = MetaN n' m') -> (n = n', m = m')
424+ metaNInj Refl = (Refl, Refl)
425+
426+ private
427+ decSNEq : (n1, n2 : SpecialName) -> Dec (n1 = n2)
428+ decSNEq (WhereN x n n') (WhereN y z w) with (decEq x y)
429+ decSNEq (WhereN x n n') (WhereN x z w) | Yes Refl with (assert_total $ decTTNameEq n z)
430+ decSNEq (WhereN x n n') (WhereN x n w) | Yes Refl | Yes Refl with (assert_total $ decTTNameEq n' w)
431+ decSNEq (WhereN x n n') (WhereN x n n') | Yes Refl | Yes Refl | Yes Refl =
432+ Yes Refl
433+ decSNEq (WhereN x n n') (WhereN x n w) | Yes Refl | Yes Refl | No contra =
434+ No $ contra . snd . snd . whereNInj
435+ decSNEq (WhereN x n n') (WhereN x z w) | Yes Refl | No contra =
436+ No $ contra . fst . snd . whereNInj
437+ decSNEq (WhereN x n n') (WhereN y z w) | No contra =
438+ No $ contra . fst . whereNInj
439+ decSNEq (WhereN x n n') (WithN y z) = No absurd
440+ decSNEq (WhereN x n n') (InstanceN y xs) = No absurd
441+ decSNEq (WhereN x n n') (ParentN y z) = No absurd
442+ decSNEq (WhereN x n n') (MethodN y) = No absurd
443+ decSNEq (WhereN x n n') (CaseN loc y) = No absurd
444+ decSNEq (WhereN x n n') (ElimN y) = No absurd
445+ decSNEq (WhereN x n n') (InstanceCtorN y) = No absurd
446+ decSNEq (WhereN x n n') (MetaN y z) = No absurd
447+ decSNEq (WithN x n) (WhereN y n' z) = No absurd
448+ decSNEq (WithN x n) (WithN y n') with (decEq x y)
449+ decSNEq (WithN x n) (WithN x n') | Yes Refl with (assert_total $ decTTNameEq n n')
450+ decSNEq (WithN x n) (WithN x n) | Yes Refl | Yes Refl =
451+ Yes Refl
452+ decSNEq (WithN x n) (WithN x n') | Yes Refl | No contra =
453+ No $ contra . snd . withNInj
454+ decSNEq (WithN x n) (WithN y n') | No contra =
455+ No $ contra . fst . withNInj
456+ decSNEq (WithN x n) (InstanceN n' xs) = No absurd
457+ decSNEq (WithN x n) (ParentN n' y) = No absurd
458+ decSNEq (WithN x n) (MethodN n') = No absurd
459+ decSNEq (WithN x n) (CaseN loc n') = No absurd
460+ decSNEq (WithN x n) (ElimN n') = No absurd
461+ decSNEq (WithN x n) (InstanceCtorN n') = No absurd
462+ decSNEq (WithN x n) (MetaN n' y) = No absurd
463+ decSNEq (InstanceN n xs) (WhereN x n' y) = No absurd
464+ decSNEq (InstanceN n xs) (WithN x n') = No absurd
465+ decSNEq (InstanceN n xs) (InstanceN n' ys) with (assert_total $ decTTNameEq n n')
466+ decSNEq (InstanceN n xs) (InstanceN n ys) | Yes Refl with (decEq xs ys)
467+ decSNEq (InstanceN n xs) (InstanceN n xs) | Yes Refl | Yes Refl =
468+ Yes Refl
469+ decSNEq (InstanceN n xs) (InstanceN n ys) | Yes Refl | No contra =
470+ No $ contra . snd . instanceNInj
471+ decSNEq (InstanceN n xs) (InstanceN n' ys) | No contra =
472+ No $ contra . fst . instanceNInj
473+ decSNEq (InstanceN n xs) (ParentN n' x) = No absurd
474+ decSNEq (InstanceN n xs) (MethodN n') = No absurd
475+ decSNEq (InstanceN n xs) (CaseN loc n') = No absurd
476+ decSNEq (InstanceN n xs) (ElimN n') = No absurd
477+ decSNEq (InstanceN n xs) (InstanceCtorN n') = No absurd
478+ decSNEq (InstanceN n xs) (MetaN n' x) = No absurd
479+ decSNEq (ParentN n x) (WhereN y n' z) = No absurd
480+ decSNEq (ParentN n x) (WithN y n') = No absurd
481+ decSNEq (ParentN n x) (InstanceN n' xs) = No absurd
482+ decSNEq (ParentN n x) (ParentN n' y) with (assert_total $ decTTNameEq n n')
483+ decSNEq (ParentN n x) (ParentN n y) | Yes Refl with (decEq x y)
484+ decSNEq (ParentN n x) (ParentN n x) | Yes Refl | Yes Refl =
485+ Yes Refl
486+ decSNEq (ParentN n x) (ParentN n y) | Yes Refl | No contra =
487+ No $ contra . snd . parentNInj
488+ decSNEq (ParentN n x) (ParentN n' y) | No contra =
489+ No $ contra . fst . parentNInj
490+ decSNEq (ParentN n x) (MethodN n') = No absurd
491+ decSNEq (ParentN n x) (CaseN loc n') = No absurd
492+ decSNEq (ParentN n x) (ElimN n') = No absurd
493+ decSNEq (ParentN n x) (InstanceCtorN n') = No absurd
494+ decSNEq (ParentN n x) (MetaN n' y) = No absurd
495+ decSNEq (MethodN n) (WhereN x n' y) = No absurd
496+ decSNEq (MethodN n) (WithN x n') = No absurd
497+ decSNEq (MethodN n) (InstanceN n' xs) = No absurd
498+ decSNEq (MethodN n) (ParentN n' x) = No absurd
499+ decSNEq (MethodN n) (MethodN n') with (assert_total $ decTTNameEq n n')
500+ decSNEq (MethodN n) (MethodN n) | Yes Refl =
501+ Yes Refl
502+ decSNEq (MethodN n) (MethodN n') | No contra =
503+ No $ contra . methodNInj
504+ decSNEq (MethodN n) (CaseN loc n') = No absurd
505+ decSNEq (MethodN n) (ElimN n') = No absurd
506+ decSNEq (MethodN n) (InstanceCtorN n') = No absurd
507+ decSNEq (MethodN n) (MetaN n' x) = No absurd
508+ decSNEq (CaseN loc n) (WhereN x n' y) = No absurd
509+ decSNEq (CaseN loc n) (WithN x n') = No absurd
510+ decSNEq (CaseN loc n) (InstanceN n' xs) = No absurd
511+ decSNEq (CaseN loc n) (ParentN n' x) = No absurd
512+ decSNEq (CaseN loc n) (MethodN n') = No absurd
513+ decSNEq (CaseN loc n) (CaseN loc' n') with (decEq loc loc')
514+ decSNEq (CaseN loc n) (CaseN loc n') | Yes Refl with (assert_total $ decTTNameEq n n')
515+ decSNEq (CaseN loc n) (CaseN loc n) | Yes Refl | Yes Refl =
516+ Yes Refl
517+ decSNEq (CaseN loc n) (CaseN loc n') | Yes Refl | No contra =
518+ No $ contra . snd . caseNInj
519+ decSNEq (CaseN loc n) (CaseN loc' n') | No contra =
520+ No $ contra . fst . caseNInj
521+ decSNEq (CaseN loc n) (ElimN n') = No absurd
522+ decSNEq (CaseN loc n) (InstanceCtorN n') = No absurd
523+ decSNEq (CaseN loc n) (MetaN n' x) = No absurd
524+ decSNEq (ElimN n) (WhereN x n' y) = No absurd
525+ decSNEq (ElimN n) (WithN x n') = No absurd
526+ decSNEq (ElimN n) (InstanceN n' xs) = No absurd
527+ decSNEq (ElimN n) (ParentN n' x) = No absurd
528+ decSNEq (ElimN n) (MethodN n') = No absurd
529+ decSNEq (ElimN n) (CaseN loc n') = No absurd
530+ decSNEq (ElimN n) (ElimN n') with (assert_total $ decTTNameEq n n')
531+ decSNEq (ElimN n) (ElimN n) | Yes Refl =
532+ Yes Refl
533+ decSNEq (ElimN n) (ElimN n') | No contra =
534+ No $ contra . elimNInj
535+ decSNEq (ElimN n) (InstanceCtorN n') = No absurd
536+ decSNEq (ElimN n) (MetaN n' x) = No absurd
537+ decSNEq (InstanceCtorN n) (WhereN x n' y) = No absurd
538+ decSNEq (InstanceCtorN n) (WithN x n') = No absurd
539+ decSNEq (InstanceCtorN n) (InstanceN n' xs) = No absurd
540+ decSNEq (InstanceCtorN n) (ParentN n' x) = No absurd
541+ decSNEq (InstanceCtorN n) (MethodN n') = No absurd
542+ decSNEq (InstanceCtorN n) (CaseN loc n') = No absurd
543+ decSNEq (InstanceCtorN n) (ElimN n') = No absurd
544+ decSNEq (InstanceCtorN n) (InstanceCtorN n') with (assert_total $ decTTNameEq n n')
545+ decSNEq (InstanceCtorN n) (InstanceCtorN n) | Yes Refl =
546+ Yes Refl
547+ decSNEq (InstanceCtorN n) (InstanceCtorN n') | No contra =
548+ No $ contra . instanceCtorNInj
549+ decSNEq (InstanceCtorN n) (MetaN n' x) = No absurd
550+ decSNEq (MetaN n n') (WhereN x y z) = No absurd
551+ decSNEq (MetaN n n') (WithN x y) = No absurd
552+ decSNEq (MetaN n n') (InstanceN x xs) = No absurd
553+ decSNEq (MetaN n n') (ParentN x y) = No absurd
554+ decSNEq (MetaN n n') (MethodN x) = No absurd
555+ decSNEq (MetaN n n') (CaseN loc x) = No absurd
556+ decSNEq (MetaN n n') (ElimN x) = No absurd
557+ decSNEq (MetaN n n') (InstanceCtorN x) = No absurd
558+ decSNEq (MetaN n n') (MetaN x y) with (assert_total $ decTTNameEq n x)
559+ decSNEq (MetaN n n') (MetaN n y) | Yes Refl with (assert_total $ decTTNameEq n' y)
560+ decSNEq (MetaN n n') (MetaN n n') | Yes Refl | Yes Refl =
561+ Yes Refl
562+ decSNEq (MetaN n n') (MetaN n y) | Yes Refl | No contra =
563+ No $ contra . snd . metaNInj
564+ decSNEq (MetaN n n') (MetaN x y) | No contra =
565+ No $ contra . fst . metaNInj
566+
567+
568+implementation DecEq TTName where
569+ decEq = decTTNameEq
570+
571+implementation DecEq SpecialName where
572+ decEq = decSNEq
61
573
62data TTUExp =
574data TTUExp =
63 ||| Universe variable
575 ||| Universe variable
test/meta001/Finite.idr+2−2
@@ -56,8 +56,8 @@ mkOk1Clause fn size i (n, _, ty) =
56mkOk2Clause : TTName -> (size, i : Nat) -> (constr : (TTName, List CtorArg, Raw)) -> Elab (FunClause Raw)
56mkOk2Clause : TTName -> (size, i : Nat) -> (constr : (TTName, List CtorArg, Raw)) -> Elab (FunClause Raw)
57mkOk2Clause fn size i (n, [], Var ty) =
57mkOk2Clause fn size i (n, [], Var ty) =
58 return $ MkFunClause (RApp (Var fn) !(mkFin size i))
58 return $ MkFunClause (RApp (Var fn) !(mkFin size i))
59− [| (Var "Refl") `(Fin ~(quote size))
59+ [| (Var `{Refl}) `(Fin ~(quote size))
60− !(mkFin size i) |]
60+ !(mkFin size i) |]
61mkOk2Clause fn size i (n, _, ty) =
61mkOk2Clause fn size i (n, _, ty) =
62 fail [TextPart "unsupported constructor", NamePart n]
62 fail [TextPart "unsupported constructor", NamePart n]
63
63
test/tactics001/Tactics.idr+4−4
@@ -18,15 +18,15 @@ refl t x = RApp (RApp (Var (UN "Refl")) t) x
18plusZeroRightNeutralNew : (n : Nat) -> plus n 0 = n
18plusZeroRightNeutralNew : (n : Nat) -> plus n 0 = n
19plusZeroRightNeutralNew Z = Refl
19plusZeroRightNeutralNew Z = Refl
20plusZeroRightNeutralNew (S k) =
20plusZeroRightNeutralNew (S k) =
21− %runElab (do rewriteWith `(sym $ plusZeroRightNeutralNew ~(Var "k"))
21+ %runElab (do rewriteWith `(sym $ plusZeroRightNeutralNew ~(Var `{k}))
22− fill $ refl `(Nat : Type) `(S ~(Var (UN "k")))
22+ fill $ refl `(Nat : Type) `(S ~(Var `{k}))
23 solve)
23 solve)
24
24
25plusSuccRightSuccNew : (j, k : Nat) -> plus j (S k) = S (plus j k)
25plusSuccRightSuccNew : (j, k : Nat) -> plus j (S k) = S (plus j k)
26plusSuccRightSuccNew Z k = Refl
26plusSuccRightSuccNew Z k = Refl
27plusSuccRightSuccNew (S j) k =
27plusSuccRightSuccNew (S j) k =
28− %runElab (do rewriteWith `(sym $ plusSuccRightSuccNew ~(Var "j") ~(Var (UN "k")))
28+ %runElab (do rewriteWith `(sym $ plusSuccRightSuccNew ~(Var `{j}) ~(Var `{k}))
29− fill $ refl `(Nat : Type) `(S (S (plus ~(Var (UN "j")) ~(Var (UN "k")))))
29+ fill $ refl `(Nat : Type) `(S (S (plus ~(Var `{j}) ~(Var `{k}))))
30 solve)
30 solve)
31
31
32-- Test that side effects in new tactics work
32-- Test that side effects in new tactics work