git.iko.soy/Idris-dev
on master help sign in
Improve rewriter for Fin.fromInteger
d364982David Raymond Christiansen
libs/base/Data/Fin.idr+27−10
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|||
@@ -143,19 +144,35 @@ fromInteger {n} x {prf} with (integerToFin x n)
143 fromInteger {n} x {prf = ItIsJust} | Just y = y
144 fromInteger {n} x {prf = ItIsJust} | Just y = y
144
145
145%language ErrorReflection
146%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+ ]
147total
155total
148finFromIntegerErrors : Err -> Maybe (List ErrorReportPart)
156finFromIntegerErrors : 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+ ]
149finFromIntegerErrors (CantUnify x tm `(IsJust (integerToFin ~n ~m)) err xs y)
171finFromIntegerErrors (CantUnify x tm `(IsJust (integerToFin ~n ~m)) err xs y)
150− = Just [ TextPart "When using", TermPart n
172+ = mkFinIntegerErr n m
151− , TextPart "as a literal for a"
152− , TermPart `(Fin ~m)
153− , SubReport [ TextPart "Could not show that"
173+ [ TextPart "Could not show that" , TermPart n
154− , TermPart n
155− , TextPart "is less than"
174+ , TextPart "is less than" , TermPart m
156− , TermPart m
157− ]
158− ]
175+ ]
159finFromIntegerErrors _ = Nothing
176finFromIntegerErrors _ = Nothing
160
177
161%error_handlers Data.Fin.fromInteger prf finFromIntegerErrors
178%error_handlers Data.Fin.fromInteger prf finFromIntegerErrors
test/error005/error005.idr+5
@@ -18,3 +18,8 @@ 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+
test/error005/expected+8−4
@@ -1,12 +1,16 @@
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