git.iko.soy/Idris-dev
on master help sign in
Improve Fin error rewriter to remove "fromInteger"
c666166David Raymond Christiansen
libs/base/Data/Fin.idr+17−4
compare with master
unifiedsplit
@@ -144,12 +144,25 @@ fromInteger {n} x {prf} with (integerToFin x n)
144 fromInteger {n} x {prf = ItIsJust} | Just y = y
144 fromInteger {n} x {prf = ItIsJust} | Just y = y
145
145
146%language ErrorReflection
146%language ErrorReflection
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+
147total private
160total private
148mkFinIntegerErr : TT -> TT -> List ErrorReportPart -> Maybe (List ErrorReportPart)
161mkFinIntegerErr : TT -> TT -> List ErrorReportPart -> Maybe (List ErrorReportPart)
149mkFinIntegerErr lit finSize subErr
162mkFinIntegerErr lit finSize subErr
150 = Just [ TextPart "When using", TermPart lit
163 = Just [ TextPart "When using", TermPart lit
151 , TextPart "as a literal for a"
164 , TextPart "as a literal for a"
152− , TermPart `(Fin ~finSize)
165+ , TermPart `(Fin ~(getNat finSize))
153 , SubReport subErr
166 , SubReport subErr
154 ]
167 ]
155total
168total
@@ -158,12 +171,12 @@ finFromIntegerErrors (CantUnify x tm `(IsJust (integerToFin ~(TConst c) ~m)) err
158 = mkFinIntegerErr (TConst c) m
171 = mkFinIntegerErr (TConst c) m
159 [ TermPart (TConst c)
172 [ TermPart (TConst c)
160 , TextPart "is not strictly less than"
173 , TextPart "is not strictly less than"
161− , TermPart m
174+ , TermPart (getNat m)
162 ]
175 ]
163finFromIntegerErrors (CantUnify x tm `(IsJust (integerToFin ~(P Bound n t) ~m)) err xs y)
176finFromIntegerErrors (CantUnify x tm `(IsJust (integerToFin ~(P Bound n t) ~m)) err xs y)
164 = mkFinIntegerErr (P Bound n t) m
177 = mkFinIntegerErr (P Bound n t) m
165 [ TextPart "Could not show that", TermPart (P Bound n t)
178 [ TextPart "Could not show that", TermPart (P Bound n t)
166− , TextPart "is less than", TermPart m
179+ , TextPart "is less than", TermPart (getNat m)
167 , TextPart "because", TermPart (P Bound n t)
180 , TextPart "because", TermPart (P Bound n t)
168 , TextPart "is a bound variable instead of a constant"
181 , TextPart "is a bound variable instead of a constant"
169 , TermPart (TConst (AType (ATInt ITBig)))
182 , TermPart (TConst (AType (ATInt ITBig)))
@@ -171,7 +184,7 @@ finFromIntegerErrors (CantUnify x tm `(IsJust (integerToFin ~(P Bound n t) ~m))
171finFromIntegerErrors (CantUnify x tm `(IsJust (integerToFin ~n ~m)) err xs y)
184finFromIntegerErrors (CantUnify x tm `(IsJust (integerToFin ~n ~m)) err xs y)
172 = mkFinIntegerErr n m
185 = mkFinIntegerErr n m
173 [ TextPart "Could not show that" , TermPart n
186 [ TextPart "Could not show that" , TermPart n
174− , TextPart "is less than" , TermPart m
187+ , TextPart "is less than" , TermPart (getNat m)
175 ]
188 ]
176finFromIntegerErrors _ = Nothing
189finFromIntegerErrors _ = Nothing
177
190
test/error005/error005.idr+2
@@ -22,4 +22,6 @@ notOk n = 2
22b0rken : Integer -> Fin 3
22b0rken : Integer -> Fin 3
23b0rken n = fromInteger n
23b0rken n = fromInteger n
24
24
25+x : Fin 4
26+x = the (Fin 4) 5
25
27
test/error005/expected+4
@@ -14,3 +14,7 @@ error005.idr:23:24:When elaborating right hand side of b0rken:
14When elaborating argument prf to function Data.Fin.fromInteger:
14When elaborating argument prf to function Data.Fin.fromInteger:
15 When using n as a literal for a Fin 3
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
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