GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-09-19 09:57:53 +03:00
Code Issues Projects Releases Wiki Activity

Avoid printing constructor names "Nat" and "Inf" in error messages.

Browse Source
This commit is contained in:
Brian Huffman 2018-07-13 12:09:24 -07:00
parent 531be1145e
commit 3ed98578de
1 changed files with 6 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
src/Cryptol/TypeCheck/Solver/Numeric.hs
View File

@ -264,8 +264,8 @@ tryEqK ctxt ty lk =
-- NOTE: (Inf - Inf) shouldn't be possible
Nothing -> Unsolvable
$ TCErrorMessage
$ "Adding " ++ show rk ++ " will always exceed "
++ show lk
$ "Adding " ++ showNat' rk ++ " will always exceed "
++ showNat' lk
Just r -> SolvedIf [ b =#= tNat' r ]
<|>
@ -311,7 +311,7 @@ tryEqK ctxt ty lk =
Inf | rk > 1 -> SolvedIf [ b =#= tInf ]
Nat n | Just (a,True) <- genLog n rk -> SolvedIf [ b =#= tNum a]
_ -> Unsolvable $ TCErrorMessage
$ show rk ++ " ^^ anything /= " ++ show lk
$ show rk ++ " ^^ anything /= " ++ showNat' lk
-- XXX: Min, Max, etx
-- 2 = min (10,y) --> y = 2
@ -437,3 +437,6 @@ matchLinear = go (0, [])
showNat' :: Nat' -> String
showNat' Inf = "inf"
showNat' (Nat n) = show n