mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-12-15 18:52:13 +03:00
Simplify simplification rules for addition
This commit is contained in:
parent
e0b1b3b502
commit
55140b0685
@ -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 ->
|
||||
|
Loading…
Reference in New Issue
Block a user