From 55140b0685f6c116f8b1d9535878c253136f7105 Mon Sep 17 00:00:00 2001 From: "Iavor S. Diatchki" Date: Fri, 27 Feb 2015 14:37:51 -0800 Subject: [PATCH] Simplify simplification rules for addition --- .../TypeCheck/Solver/Numeric/Simplify.hs | 34 +++++++------------ 1 file changed, 13 insertions(+), 21 deletions(-) diff --git a/src/Cryptol/TypeCheck/Solver/Numeric/Simplify.hs b/src/Cryptol/TypeCheck/Solver/Numeric/Simplify.hs index 9eb2cbd5..332887ee 100644 --- a/src/Cryptol/TypeCheck/Solver/Numeric/Simplify.hs +++ b/src/Cryptol/TypeCheck/Solver/Numeric/Simplify.hs @@ -552,29 +552,17 @@ crySimpExprStep expr = x :+ y -> case (x,y) of - (K (Nat 0), _) -> Just y - (K Inf, _) -> Just inf - (K a, K b) -> Just (K (IN.nAdd a b)) - (_, K b) -> Just (K b :+ x) - - -- Adding constants + (K (Nat 0), _) -> Just y + (K Inf, _) -> Just inf + (K a, K b) -> Just (K (IN.nAdd a b)) (K a, K b :+ c) -> Just (K (IN.nAdd a b) :+ c) - (K a, K b :- c) -> Just (K (IN.nAdd a b) :- c) - (K a, c :- K b) -> case IN.nSub a b of - Just (Nat 0) -> Just c - Just r -> Just (K r :+ c) - Nothing -> do r <- IN.nSub b a - return (c :- K r) - (K a :+ c1, K b :+ c2) -> Just (K (IN.nAdd a b) :+ (c1 :+ c2)) - (K a :+ c1, K b :- c) -> Just (K (IN.nAdd a b) :+ (c1 :- c)) - (K a :+ c1, c :- K b) -> case IN.nSub a b of - Just (Nat 0) -> Just (c1 :+ c) - Just r -> Just (K r :+ (c1 :+ c)) - Nothing -> do r <- IN.nSub b a - return (c1 :+ (c :- K r)) + -- Normalize a bit + (_, K b) -> Just (K b :+ x) + (_, b :- c) -> Just ((x :+ b) :- c) + (a :+ b, _) -> Just (a :+ (b :+ y)) - _ -> Nothing + _ -> Nothing x :- y -> case (x,y) of @@ -601,7 +589,6 @@ crySimpExprStep expr = _ -> Nothing - -- XXX: More rules like + x :* y -> case (x,y) of (K (Nat 0), _) -> Just zero @@ -611,6 +598,11 @@ crySimpExprStep expr = (K a, K b :* z) -> Just (K (IN.nMul a b) :* z) + -- Normalize, somewhat + (a :* b, _) -> Just (a :* (b :* y)) + (Var a, Var b) + | b > a -> Just (y :* x) + _ -> Nothing Div x y ->