GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-12-17 13:01:31 +03:00
Code Issues Projects Releases Wiki Activity

Add a rule for simplifying x +y = inf

Browse Source
This commit is contained in:
Trevor Elliott 2017-03-24 18:02:29 -07:00
parent 90f7d0c330
commit 8a4eadfdac
1 changed files with 24 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -29,6 +29,7 @@ cryIsEqual ctxt t1 t2 =
<|> tryEqMin t1 t2 <|> tryEqMin t1 t2
<|> tryEqMin t2 t1 <|> tryEqMin t2 t1
<|> tryEqMulConst t1 t2 <|> tryEqMulConst t1 t2
<|> tryEqAddInf ctxt t1 t2
@ -234,3 +235,26 @@ tryEqMulConst l r =
in if d == 1 in if d == 1
then Unsolved then Unsolved
else (SolvedIf [ tMul (tNum lk') l' =#= tMul (tNum rk') r' ]) else (SolvedIf [ tMul (tNum lk') l' =#= tMul (tNum rk') r' ])
tryEqAddInf :: Ctxt -> Type -> Type -> Match Solved
tryEqAddInf ctxt l r = check l r <|> check r l
where
-- check for x = a + b /\ x = inf
check x y =
do (x1,x2) <- anAdd x
aInf y
let x1Fin = iIsFin (typeInterval ctxt x1)
let x2Fin = iIsFin (typeInterval ctxt x2)
return $!
if | x1Fin ->
SolvedIf [ x2 =#= y ]
| x2Fin ->
SolvedIf [ x1 =#= y ]
| otherwise ->
Unsolved