GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-11-30 23:45:23 +03:00
Code Issues Projects Releases Wiki Activity

Fix the solver code for Integral. It was previously failing too

Browse Source 
early if sequence element type is a variable.
This commit is contained in:
Rob Dockins 2020-05-14 09:18:30 -07:00
parent 9424752b45
commit 97d99072a0
1 changed files with 8 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

11
src/Cryptol/TypeCheck/Solver/Class.hs
View File

@ -148,15 +148,20 @@ solveIntegralInst ty = case tNoUser ty of
TCon (TC TCBit) [] ->
Unsolvable $ TCErrorMessage "Arithmetic cannot be done on individual bits."
-- fin n => Integral [n]
TCon (TC TCSeq) [n, TCon (TC TCBit) []] -> SolvedIf [ pFin n ]
-- Integral Integer
TCon (TC TCInteger) [] -> SolvedIf []
-- Integral (Z n)
TCon (TC TCIntMod) [n] -> SolvedIf [ pFin n, n >== tOne ]
-- fin n => Integral [n]
TCon (TC TCSeq) [n, elTy] ->
case tNoUser elTy of
TCon (TC TCBit) [] -> SolvedIf [ pFin n ]
TVar _ -> Unsolved
_ -> Unsolvable $ TCErrorMessage $ show
$ "Type" <+> quotes (pp ty) <+> "is not an intergral type."
TVar _ -> Unsolved
_ -> Unsolvable $ TCErrorMessage $ show