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

Make fin decisions first.

Browse Source
This commit is contained in:
Iavor S. Diatchki 2015-06-24 11:19:52 -07:00
parent c4c587d14b
commit 91ebb1ca2b
1 changed files with 10 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

11
src/Cryptol/TypeCheck/Solver/Numeric/Simplify1.hs
View File

@ -141,14 +141,23 @@ mkIf a t e
| t == e = t
| otherwise = case a of
AFin x -> If a (pKnownFin x t) (pKnownInf x e)
_ | If b@(AFin y) _ _ <- t -> If b (mkFinIf y) (mkInfIf y)
| If b@(AFin y) _ _ <- e -> If b (mkFinIf y) (mkInfIf y)
AEq x' y'
| x == y -> t
| x == y -> t
| otherwise -> If (AEq x y) t e
where (x,y) = balanceEq x' y'
_ -> If a t e
where
mkFinIf y = mkIf a (pKnownFin y t) (pKnownFin y e)
mkInfIf y = case apSubstAtom (Map.singleton y (K Inf)) a of
Nothing -> mkIf a (pKnownInf y t) (pKnownInf y t)
Just a' -> pIf a' (pKnownInf y t) (pKnownInf y t)
-- | If-then-else with non-atom at decision.
pIf :: (Eq a, HasVars a) => I Bool -> I a -> I a -> I a