git.iko.soy/Idris-dev
on master help sign in
Merge pull request #2000 from david-christiansen/better-fin-error
ad2f186David Christiansen
libs/base/Data/Fin.idr+39−9
compare with master
unifiedsplit
@@ -1,6 +1,7 @@
1module Data.Fin
1module Data.Fin
2
2
3%default total
3%default total
4+%access public
4
5
5||| Numbers strictly less than some bound. The name comes from "finite sets".
6||| Numbers strictly less than some bound. The name comes from "finite sets".
6|||
7|||
@@ -144,18 +145,47 @@ fromInteger {n} x {prf} with (integerToFin x n)
144
145
145%language ErrorReflection
146%language ErrorReflection
146
147
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+ ]
147total
168total
148finFromIntegerErrors : Err -> Maybe (List ErrorReportPart)
169finFromIntegerErrors : 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+ ]
149finFromIntegerErrors (CantUnify x tm `(IsJust (integerToFin ~n ~m)) err xs y)
184finFromIntegerErrors (CantUnify x tm `(IsJust (integerToFin ~n ~m)) err xs y)
150− = Just [ TextPart "When using", TermPart n
185+ = mkFinIntegerErr n m
151− , TextPart "as a literal for a"
152− , TermPart `(Fin ~m)
153− , SubReport [ TextPart "Could not show that"
186+ [ TextPart "Could not show that" , TermPart n
154− , TermPart n
155− , TextPart "is less than"
187+ , TextPart "is less than" , TermPart (getNat m)
156− , TermPart m
157− ]
158− ]
188+ ]
159finFromIntegerErrors _ = Nothing
189finFromIntegerErrors _ = Nothing
160
190
161%error_handlers Data.Fin.fromInteger prf finFromIntegerErrors
191%error_handlers Data.Fin.fromInteger prf finFromIntegerErrors
test/error005/error005.idr+7
@@ -18,3 +18,10 @@ ok n = 1
18
18
19notOk : (n : Nat) -> Fin (plus 2 n)
19notOk : (n : Nat) -> Fin (plus 2 n)
20notOk n = 2
20notOk 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 @@
1error005.idr:13:1:When elaborating right hand side of two:
1error005.idr:13:1:When elaborating right hand side of two:
2When elaborating argument prf to function Data.Fin.fromInteger:
2When elaborating argument prf to function Data.Fin.fromInteger:
3 When using 2 as a literal for a Fin 2
3 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
5error005.idr:16:1:When elaborating right hand side of hahaha:
5error005.idr:16:1:When elaborating right hand side of hahaha:
6When elaborating argument prf to function Data.Fin.fromInteger:
6When elaborating argument prf to function Data.Fin.fromInteger:
7 When using 0 as a literal for a Fin n
7 When using 0 as a literal for a Fin n
8− Could not show that 0 is less than n
8+ 0 is not strictly less than n
9−error005.idr:21:1:When elaborating right hand side of notOk:
9+error005.idr:22:1:When elaborating right hand side of notOk:
10When elaborating argument prf to function Data.Fin.fromInteger:
10When elaborating argument prf to function Data.Fin.fromInteger:
11 When using 2 as a literal for a Fin (S (S n))
11 When using 2 as a literal for a Fin (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
12− Could not show that 2 is less than S (S n)
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