git.iko.soy/Idris-dev
on master help sign in
Merge pull request #2000 from david-christiansen/better-fin-error

Better Fin error

commitad2f1864e480e9f8548005f58072cfaa711e6a47 authorDavid Christiansen <david@davidchristiansen.dk> dateSun 15 Mar 2015, 12:17 (12 years ago) parentfd0bbc2c666166
3 files changed+58−13
compare with master
unifiedsplit
libs/base/Data/Fin.idr+39−9 test/error005/error005.idr+7 test/error005/expected+12−4
libs/base/Data/Fin.idr+39−9
@@ -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|||
@@ -144,18 +145,47 @@ fromInteger {n} x {prf} with (integerToFin x n)
144145
145146%language ErrorReflection
146147
148+||| Attempt to convert a reflected (fromInteger n) to a Nat
149+total private
150+getNat' : TT -> Maybe TT
151+getNat' `(fromInteger ~(TConst (BI c)) : Nat) = Just $ quote (the Nat (fromInteger c))
152+getNat' _ = Nothing
153+
154+||| Attempt to convert a reflected (fromInteger n) to a Nat. Return
155+||| the original term on failure.
156+total private
157+getNat : TT -> TT
158+getNat tm = maybe tm id $ getNat' tm
159+
160+total private
161+mkFinIntegerErr : TT -> TT -> List ErrorReportPart -> Maybe (List ErrorReportPart)
162+mkFinIntegerErr lit finSize subErr
163+ = Just [ TextPart "When using", TermPart lit
164+ , TextPart "as a literal for a"
165+ , TermPart `(Fin ~(getNat finSize))
166+ , SubReport subErr
167+ ]
147168total
148169finFromIntegerErrors : Err -> Maybe (List ErrorReportPart)
170+finFromIntegerErrors (CantUnify x tm `(IsJust (integerToFin ~(TConst c) ~m)) err xs y)
171+ = mkFinIntegerErr (TConst c) m
172+ [ TermPart (TConst c)
173+ , TextPart "is not strictly less than"
174+ , TermPart (getNat m)
175+ ]
176+finFromIntegerErrors (CantUnify x tm `(IsJust (integerToFin ~(P Bound n t) ~m)) err xs y)
177+ = mkFinIntegerErr (P Bound n t) m
178+ [ TextPart "Could not show that", TermPart (P Bound n t)
179+ , TextPart "is less than", TermPart (getNat m)
180+ , TextPart "because", TermPart (P Bound n t)
181+ , TextPart "is a bound variable instead of a constant"
182+ , TermPart (TConst (AType (ATInt ITBig)))
183+ ]
149184finFromIntegerErrors (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− ]
185+ = mkFinIntegerErr n m
186+ [ TextPart "Could not show that" , TermPart n
187+ , TextPart "is less than" , TermPart (getNat m)
188+ ]
159189finFromIntegerErrors _ = Nothing
160190
161191%error_handlers Data.Fin.fromInteger prf finFromIntegerErrors
test/error005/error005.idr+7
@@ -18,3 +18,10 @@ 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+x : Fin 4
26+x = the (Fin 4) 5
27+
test/error005/expected+12−4
@@ -1,12 +1,20 @@
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
17+error005.idr:28:1:When elaborating right hand side of x:
18+When elaborating argument prf to function Data.Fin.fromInteger:
19+ When using 5 as a literal for a Fin 4
20+ 5 is not strictly less than 4