git.iko.soy/Idris-dev
on master help sign in
Improve rewriter for Fin.fromInteger

It now offers different errors when it couldn't prove the lemma due to having a variable for the Integer, or when it couldn't prove it due to having concrete values that are directly incorrect.

commitd3649824df8e50338b0f2951597329fff20953b9 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateSat 14 Mar 2015, 20:16 (12 years ago) parentd1d6a7e
3 files changed+40−14
compare with master
unifiedsplit
libs/base/Data/Fin.idr+27−10 test/error005/error005.idr+5 test/error005/expected+8−4
libs/base/Data/Fin.idr+27−10
@@ -1,6 +1,7 @@
11module Data.Fin
22
33%default total
4+%access public
45
56||| Numbers strictly less than some bound. The name comes from "finite sets".
67|||
@@ -143,19 +144,35 @@ fromInteger {n} x {prf} with (integerToFin x n)
143144 fromInteger {n} x {prf = ItIsJust} | Just y = y
144145
145146%language ErrorReflection
146−
147+total private
148+mkFinIntegerErr : TT -> TT -> List ErrorReportPart -> Maybe (List ErrorReportPart)
149+mkFinIntegerErr lit finSize subErr
150+ = Just [ TextPart "When using", TermPart lit
151+ , TextPart "as a literal for a"
152+ , TermPart `(Fin ~finSize)
153+ , SubReport subErr
154+ ]
147155total
148156finFromIntegerErrors : Err -> Maybe (List ErrorReportPart)
157+finFromIntegerErrors (CantUnify x tm `(IsJust (integerToFin ~(TConst c) ~m)) err xs y)
158+ = mkFinIntegerErr (TConst c) m
159+ [ TermPart (TConst c)
160+ , TextPart "is not strictly less than"
161+ , TermPart m
162+ ]
163+finFromIntegerErrors (CantUnify x tm `(IsJust (integerToFin ~(P Bound n t) ~m)) err xs y)
164+ = mkFinIntegerErr (P Bound n t) m
165+ [ TextPart "Could not show that", TermPart (P Bound n t)
166+ , TextPart "is less than", TermPart m
167+ , TextPart "because", TermPart (P Bound n t)
168+ , TextPart "is a bound variable instead of a constant"
169+ , TermPart (TConst (AType (ATInt ITBig)))
170+ ]
149171finFromIntegerErrors (CantUnify x tm `(IsJust (integerToFin ~n ~m)) err xs y)
150− = Just [ TextPart "When using", TermPart n
151− , TextPart "as a literal for a"
152− , TermPart `(Fin ~m)
153− , SubReport [ TextPart "Could not show that"
154− , TermPart n
155− , TextPart "is less than"
156− , TermPart m
157− ]
158− ]
172+ = mkFinIntegerErr n m
173+ [ TextPart "Could not show that" , TermPart n
174+ , TextPart "is less than" , TermPart m
175+ ]
159176finFromIntegerErrors _ = Nothing
160177
161178%error_handlers Data.Fin.fromInteger prf finFromIntegerErrors
test/error005/error005.idr+5
@@ -18,3 +18,8 @@ ok n = 1
1818
1919notOk : (n : Nat) -> Fin (plus 2 n)
2020notOk n = 2
21+
22+b0rken : Integer -> Fin 3
23+b0rken n = fromInteger n
24+
25+
test/error005/expected+8−4
@@ -1,12 +1,16 @@
11error005.idr:13:1:When elaborating right hand side of two:
22When elaborating argument prf to function Data.Fin.fromInteger:
33 When using 2 as a literal for a Fin 2
4− Could not show that 2 is less than 2
4+ 2 is not strictly less than 2
55error005.idr:16:1:When elaborating right hand side of hahaha:
66When elaborating argument prf to function Data.Fin.fromInteger:
77 When using 0 as a literal for a Fin n
8− Could not show that 0 is less than n
9−error005.idr:21:1:When elaborating right hand side of notOk:
8+ 0 is not strictly less than n
9+error005.idr:22:1:When elaborating right hand side of notOk:
1010When elaborating argument prf to function Data.Fin.fromInteger:
1111 When using 2 as a literal for a Fin (S (S n))
12− Could not show that 2 is less than S (S n)
12+ 2 is not strictly less than S (S n)
13+error005.idr:23:24:When elaborating right hand side of b0rken:
14+When elaborating argument prf to function Data.Fin.fromInteger:
15+ When using n as a literal for a Fin 3
16+ Could not show that n is less than 3 because n is a bound variable instead of a constant Integer