git.iko.soy/Idris-dev
on master help sign in
Improve Fin error rewriter to remove "fromInteger"

"fromInteger" now never shows up in the errors, at least not applied to an Integer constant.

commitc6661660adc6d47a50c526b9a13ee51df7746db3 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateSat 14 Mar 2015, 22:27 (12 years ago) parentd364982
3 files changed+23−4
compare with master
unifiedsplit
libs/base/Data/Fin.idr+17−4 test/error005/error005.idr+2 test/error005/expected+4
libs/base/Data/Fin.idr+17−4
@@ -144,12 +144,25 @@ fromInteger {n} x {prf} with (integerToFin x n)
144144 fromInteger {n} x {prf = ItIsJust} | Just y = y
145145
146146%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+
147160total private
148161mkFinIntegerErr : TT -> TT -> List ErrorReportPart -> Maybe (List ErrorReportPart)
149162mkFinIntegerErr lit finSize subErr
150163 = Just [ TextPart "When using", TermPart lit
151164 , TextPart "as a literal for a"
152− , TermPart `(Fin ~finSize)
165+ , TermPart `(Fin ~(getNat finSize))
153166 , SubReport subErr
154167 ]
155168total
@@ -158,12 +171,12 @@ finFromIntegerErrors (CantUnify x tm `(IsJust (integerToFin ~(TConst c) ~m)) err
158171 = mkFinIntegerErr (TConst c) m
159172 [ TermPart (TConst c)
160173 , TextPart "is not strictly less than"
161− , TermPart m
174+ , TermPart (getNat m)
162175 ]
163176finFromIntegerErrors (CantUnify x tm `(IsJust (integerToFin ~(P Bound n t) ~m)) err xs y)
164177 = mkFinIntegerErr (P Bound n t) m
165178 [ 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)
167180 , TextPart "because", TermPart (P Bound n t)
168181 , TextPart "is a bound variable instead of a constant"
169182 , TermPart (TConst (AType (ATInt ITBig)))
@@ -171,7 +184,7 @@ finFromIntegerErrors (CantUnify x tm `(IsJust (integerToFin ~(P Bound n t) ~m))
171184finFromIntegerErrors (CantUnify x tm `(IsJust (integerToFin ~n ~m)) err xs y)
172185 = mkFinIntegerErr n m
173186 [ TextPart "Could not show that" , TermPart n
174− , TextPart "is less than" , TermPart m
187+ , TextPart "is less than" , TermPart (getNat m)
175188 ]
176189finFromIntegerErrors _ = Nothing
177190
test/error005/error005.idr+2
@@ -22,4 +22,6 @@ notOk n = 2
2222b0rken : Integer -> Fin 3
2323b0rken n = fromInteger n
2424
25+x : Fin 4
26+x = the (Fin 4) 5
2527
test/error005/expected+4
@@ -14,3 +14,7 @@ error005.idr:23:24:When elaborating right hand side of b0rken:
1414When elaborating argument prf to function Data.Fin.fromInteger:
1515 When using n as a literal for a Fin 3
1616 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