From 20f4f9a10819ea2aa0a981d9edc4d2f7082db777 Mon Sep 17 00:00:00 2001 From: Trevor Elliott Date: Tue, 28 Mar 2017 13:20:35 -0700 Subject: [PATCH] Simplify addition of constants in equality and geq constraints Simplifying constraints of the form `k1 + a == k2 + b`. If `k1 > k2`, then the constraint can be rewritten to `(k1 - k2) + a == b`, or `a == (k2 - k1) + b` otherwise. This allows the constraint solver to make progress in cases where `a` or `b` include unification variables. --- src/Cryptol/TypeCheck/Solver/Numeric.hs | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) diff --git a/src/Cryptol/TypeCheck/Solver/Numeric.hs b/src/Cryptol/TypeCheck/Solver/Numeric.hs index ede69344..330b16e8 100644 --- a/src/Cryptol/TypeCheck/Solver/Numeric.hs +++ b/src/Cryptol/TypeCheck/Solver/Numeric.hs @@ -30,6 +30,7 @@ cryIsEqual ctxt t1 t2 = <|> tryEqMin t2 t1 <|> tryEqMulConst t1 t2 <|> tryEqAddInf ctxt t1 t2 + <|> tryAddConst (=#=) t1 t2 @@ -46,6 +47,9 @@ cryIsGeq i t1 t2 = <|> tryGeqThanSub i t1 t2 <|> (geqByInterval i t1 t2) <|> (guard (t1 == t2) >> return (SolvedIf [])) + <|> tryAddConst (>==) t1 t2 + -- XXX: k >= width e + -- XXX: width e >= k -- XXX: max a 10 >= 2 --> True @@ -258,3 +262,21 @@ tryEqAddInf ctxt l r = check l r <|> check r l | otherwise -> Unsolved + + + +-- | Check for addition of constants to both sides of a relation. +-- +-- This relies on the fact that constants are floated left during +-- simplification. +tryAddConst :: (Type -> Type -> Prop) -> Type -> Type -> Match Solved +tryAddConst rel l r = + do (x1,x2) <- anAdd l + (y1,y2) <- anAdd r + + k1 <- aNat x1 + k2 <- aNat y1 + + if k1 > k2 + then return (SolvedIf [ tAdd (tNum (k1 - k2)) x2 `rel` y2 ]) + else return (SolvedIf [ x2 `rel` tAdd (tNum (k2 - k1)) y2 ])