module Cryptol.TypeCheck.Solver.Numeric.Simplify
(
crySimplify, crySimplifyMaybe
, crySimpPropExpr, crySimpPropExprMaybe
) where
import Cryptol.TypeCheck.Solver.Numeric.AST
import Cryptol.TypeCheck.Solver.Numeric.SimplifyExpr
import Cryptol.TypeCheck.Solver.InfNat(genLog,genRoot,rootExact)
import Cryptol.Utils.Misc ( anyJust )
import Control.Monad ( mplus )
import Data.List ( sortBy )
import Data.Maybe ( fromMaybe )
import qualified Data.Set as Set
crySimplify :: Prop -> Prop
crySimplify p = fromMaybe p (crySimplifyMaybe p)
crySimplifyMaybe :: Prop -> Maybe Prop
crySimplifyMaybe p =
let mbSimpExprs = simpSubs p
exprsSimped = fromMaybe p mbSimpExprs
mbRearrange = tryRearrange exprsSimped
rearranged = fromMaybe exprsSimped mbRearrange
in crySimplify `fmap` (crySimpStep rearranged `mplus` mbRearrange
`mplus` mbSimpExprs)
where
tryRearrange q = case q of
_ :&& _ -> cryRearrangeAnd q
_ :|| _ -> cryRearrangeOr q
_ -> Nothing
simpSubs q = case q of
Not a -> Not `fmap` crySimplifyMaybe a
a :&& b -> do [a',b'] <- anyJust crySimplifyMaybe [a,b]
return (a' :&& b')
a :|| b -> do [a',b'] <- anyJust crySimplifyMaybe [a,b]
return (a' :|| b')
_ -> crySimpPropExprMaybe q
crySimpStep :: Prop -> Maybe Prop
crySimpStep prop =
case prop of
Fin x -> cryIsFin x
x :== y -> Just (cryIsEq x y)
x :> y -> Just (cryIsGt x y)
x :>= y ->
case (x,y) of
(K (Nat 0), _) -> Just (y :== zero)
(K (Nat a), Width b) -> Just (K (Nat (2 ^ a)) :>= b)
(_, K (Nat 0)) -> Just PTrue
(Width e, K (Nat b)) -> Just (e :>= K (Nat (2^(b1))))
(K Inf, _) -> Just PTrue
(_, K Inf) -> Just (x :== inf)
_ -> Just (x :== inf :|| one :+ x :> y)
x :==: y ->
case (x,y) of
(K a, K b) -> Just (if a == b then PTrue else PFalse)
(K (Nat n), _) | Just p <- cryIsNat True n y -> Just p
(_, K (Nat n)) | Just p <- cryIsNat True n x -> Just p
_ | x == y -> Just PTrue
| otherwise -> case (x,y) of
(Var _, _) -> Nothing
(_, Var _) -> Just (y :==: x)
_ -> Nothing
x :>: y ->
case (x,y) of
(K (Nat n),_) | Just p <- cryNatGt True n y -> Just p
(_, K (Nat n)) | Just p <- cryGtNat True n x -> Just p
_ | x == y -> Just PFalse
| otherwise -> Nothing
p :&& q -> cryAnd p q
p :|| q -> cryOr p q
Not p -> cryNot p
PFalse -> Nothing
PTrue -> Nothing
cryRearrangeAnd :: Prop -> Maybe Prop
cryRearrangeAnd prop =
case rebalance prop of
Just p -> Just p
Nothing -> cryAnds `fmap` cryRearrange cmpAnd (split prop)
where
rebalance (a :&& b) =
case a of
PFalse -> Just PFalse
PTrue -> Just b
a1 :&& a2 -> Just (a1 :&& (a2 :&& b))
_ -> fmap (a :&&) (rebalance b)
rebalance _ = Nothing
split (a :&& b) = a : split b
split a = [a]
cryRearrangeOr :: Prop -> Maybe Prop
cryRearrangeOr prop =
case rebalance prop of
Just p -> Just p
Nothing -> cryOrs `fmap` cryRearrange cmpOr (split prop)
where
rebalance (a :|| b) =
case a of
PFalse -> Just b
PTrue -> Just PTrue
a1 :|| a2 -> Just (a1 :|| (a2 :|| b))
_ -> fmap (a :||) (rebalance b)
rebalance _ = Nothing
split (a :|| b) = a : split b
split a = [a]
cryIsDefn :: Prop -> Maybe (Name, Expr)
cryIsDefn (Var x :==: e) = if (x `Set.member` cryExprFVS e)
then Nothing
else Just (x,e)
cryIsDefn _ = Nothing
type PropOrdering = (Int,Prop) -> (Int,Prop) -> Ordering
cryRearrange :: PropOrdering -> [Prop] -> Maybe [Prop]
cryRearrange cmp ps = if ascending keys then Nothing else Just sortedProps
where
(keys, sortedProps) = unzip (sortBy cmp (zip [ 0 :: Int .. ] ps))
ascending (x : y : zs) = x < y && ascending (y : zs)
ascending _ = True
cmpAnd :: PropOrdering
cmpAnd (k1,prop1) (k2,prop2) =
case (prop1, prop2) of
(PFalse, PFalse) -> compare k1 k2
(PFalse, _) -> LT
(_,PFalse) -> GT
(PTrue, PTrue) -> compare k1 k2
(PTrue, _) -> LT
(_,PTrue) -> GT
(Not (Fin (Var x)), Not (Fin (Var y))) -> cmpVars x y
(Not (Fin (Var _)), _) -> LT
(_, Not (Fin (Var _))) -> GT
_ | Just (x,_) <- mbL
, Just (y,_) <- mbR -> cmpVars x y
| Just _ <- mbL -> LT
| Just _ <- mbR -> GT
where
mbL = cryIsDefn prop1
mbR = cryIsDefn prop2
(Fin (Var x), Fin (Var y)) -> cmpVars x y
(Fin (Var _), _) -> LT
(_, Fin (Var _)) -> GT
_ -> compare k1 k2
where
cmpVars x y
| x < y = LT
| x > y = GT
| otherwise = compare k1 k2
cmpOr :: PropOrdering
cmpOr (k1,prop1) (k2,prop2) =
case (prop1, prop2) of
(PTrue, PTrue) -> compare k1 k2
(PTrue, _) -> LT
(_,PTrue) -> GT
(PFalse, PFalse) -> compare k1 k2
(PFalse, _) -> LT
(_,PFalse) -> GT
(Fin (Var x), Fin (Var y)) -> cmpVars x y
(Fin (Var _), _) -> LT
(_, Fin (Var _)) -> GT
(Not (Fin (Var x)), Not (Fin (Var y))) -> cmpVars x y
(Not (Fin (Var _)), _) -> LT
(_, Not (Fin (Var _))) -> GT
_ -> compare k1 k2
where
cmpVars x y
| x < y = LT
| x > y = GT
| otherwise = compare k1 k2
cryAnd :: Prop -> Prop -> Maybe Prop
cryAnd p q =
case p of
PTrue -> Just q
PFalse -> Just PFalse
Not (Fin (Var x))
| Just q' <- cryKnownFin x False q -> Just (p :&& q')
Fin (Var x)
| Just q' <- cryKnownFin x True q -> Just (p :&& q')
_ | Just (x,e) <- cryIsDefn p
, Just q' <- cryLet x e q
-> Just (p :&& q')
_ -> Nothing
cryOr :: Prop -> Prop -> Maybe Prop
cryOr p q =
case p of
PTrue -> Just PTrue
PFalse -> Just q
Fin (Var x)
| Just q' <- cryKnownFin x False q -> Just (p :|| q')
Not (Fin (Var x))
| Just q' <- cryKnownFin x True q -> Just (p :|| q')
_ -> Nothing
cryKnownFin :: Name -> Bool -> Prop -> Maybe Prop
cryKnownFin a isFin prop =
case prop of
Fin (Var a') | a == a' -> Just (if isFin then PTrue else PFalse)
p :&& q -> do [p',q'] <- anyJust (cryKnownFin a isFin) [p,q]
return (p' :&& q')
p :|| q -> do [p',q'] <- anyJust (cryKnownFin a isFin) [p,q]
return (p' :|| q')
Not p -> Not `fmap` cryKnownFin a isFin p
x :==: y
| not isFin, Just [x',y'] <- anyJust (cryLet a inf) [x,y]
-> Just (cryNatOp (:==:) x' y')
x :>: y
| not isFin, Just [x',y'] <- anyJust (cryLet a inf) [x,y]
-> Just (cryNatOp (:>:) x' y')
_ -> Nothing
cryNot :: Prop -> Maybe Prop
cryNot prop =
case prop of
Fin _ -> Nothing
x :== y -> Just (x :> y :|| y :> x)
x :>= y -> Just (y :> x)
x :> y -> Just (y :>= x)
x :==: y -> Just (x :>: y :|| y :>: x)
_ :>: _ -> Nothing
p :&& q -> Just (Not p :|| Not q)
p :|| q -> Just (Not p :&& Not q)
Not p -> Just p
PFalse -> Just PTrue
PTrue -> Just PFalse
cryIsEq :: Expr -> Expr -> Prop
cryIsEq l r =
case (l,r) of
(K m, K n) -> if m == n then PTrue else PFalse
(K Inf, _) -> Not (Fin r)
(_, K Inf) -> Not (Fin l)
(Div x y, z) -> x :>= z :* y :&& (one :+ z) :* y :> x
(K (Nat n),_) | Just p <- cryIsNat False n r -> p
(_,K (Nat n)) | Just p <- cryIsNat False n l -> p
_ -> Not (Fin l) :&& Not (Fin r)
:|| Fin l :&& Fin r :&& cryNatOp (:==:) l r
cryIsGt :: Expr -> Expr -> Prop
cryIsGt (K m) (K n) = if m > n then PTrue else PFalse
cryIsGt (K (Nat n)) e | Just p <- cryNatGt False n e = p
cryIsGt e (K (Nat n)) | Just p <- cryGtNat False n e = p
cryIsGt x y = Fin y :&& (x :== inf :||
Fin x :&& cryNatOp (:>:) x y)
cryIsFin :: Expr -> Maybe Prop
cryIsFin expr =
case expr of
K Inf -> Just PFalse
K (Nat _) -> Just PTrue
Var _ -> Nothing
t1 :+ t2 -> Just (Fin t1 :&& Fin t2)
t1 :- _ -> Just (Fin t1)
t1 :* t2 -> Just ( Fin t1 :&& Fin t2
:|| t1 :== zero :&& t2 :== inf
:|| t2 :== zero :&& t1 :== inf
)
Div t1 _ -> Just (Fin t1)
Mod _ _ -> Just PTrue
t1 :^^ t2 ->
Just ( Fin t1 :&& Fin t2
:|| t1 :== inf :&& t2 :== zero
:|| t2 :== inf :&& (t1 :== zero :|| t1 :== one)
)
Min t1 t2 -> Just (Fin t1 :|| Fin t2)
Max t1 t2 -> Just (Fin t1 :&& Fin t2)
Width t1 -> Just (Fin t1)
LenFromThen _ _ _ -> Just PTrue
LenFromThenTo _ _ _ -> Just PTrue
cryIsNat :: Bool -> Integer -> Expr -> Maybe Prop
cryIsNat useFinite n expr =
case expr of
K Inf -> Just PFalse
K (Nat m) -> Just (if m == n then PTrue else PFalse)
Var _ | useFinite -> Nothing
| otherwise -> Just (Fin expr :&& expr :==: K (Nat n))
K (Nat m) :+ e2 -> Just $ if m > n then PFalse
else eq e2 $ K $ Nat $ n m
x :+ y
| n == 0 -> Just (eq x zero :&& eq y zero)
| n == 1 -> Just (eq x zero :&& eq y one :||
eq x one :&& eq y zero)
| otherwise -> Nothing
e1 :- e2 -> Just $ eq (K (Nat n) :+ e2) e1
K (Nat m) :* e2 ->
Just $ if m == 0
then if n == 0 then PTrue else PFalse
else case divMod n m of
(q,r) -> if r == 0 then eq e2 (K (Nat q))
else PFalse
e1 :* e2
| n == 0 -> Just (eq e1 zero :|| eq e2 zero)
| n == 1 -> Just (eq e1 one :&& eq e2 one)
| otherwise -> Nothing
Div x y -> Just (gt (one :+ x) (K (Nat n) :* y) :&&
gt (K (Nat (n + 1)) :* y) x)
Mod _ _ | useFinite -> Nothing
| otherwise -> Just (cryNatOp (:==:) expr (K (Nat n)))
K (Nat m) :^^ y -> Just $ case genLog n m of
Just (a, exact)
| exact -> eq y (K (Nat a))
_ -> PFalse
x :^^ K (Nat m) -> Just $ case rootExact n m of
Just a -> eq x (K (Nat a))
Nothing -> PFalse
x :^^ y
| n == 0 -> Just (eq x zero :&& gt y zero)
| n == 1 -> Just (eq x one :|| eq y zero)
| otherwise -> Nothing
Min x y
| n == 0 -> Just (eq x zero :|| eq y zero)
| otherwise -> Just ( eq x (K (Nat n)) :&& gt y (K (Nat (n 1)))
:|| eq y (K (Nat n)) :&& gt x (K (Nat (n 1)))
)
Max x y -> Just ( eq x (K (Nat n)) :&& gt (K (Nat (n + 1))) y
:|| eq y (K (Nat n)) :&& gt (K (Nat (n + 1))) y
)
Width x
| n == 0 -> Just (eq x zero)
| otherwise -> Just (gt x (K (Nat (2^(n1) 1))) :&&
gt (K (Nat (2 ^ n))) x)
LenFromThen x y w
| n == 0 -> Just PFalse
| n == 1 -> Just (gt y x :&& gt (y :+ one) (two :^^ w))
| otherwise -> Nothing
LenFromThenTo x y z
| n == 0 -> Just ( gt x y :&& gt z x
:|| gt y x :&& gt x z
)
| n == 1 -> Just (gt z y :&& gt (x :+ one) z :||
gt y z :&& gt (z :+ one) x)
| otherwise -> Nothing
where
eq x y = if useFinite then x :==: y else x :== y
gt x y = if useFinite then x :>: y else x :> y
cryNatGt :: Bool -> Integer -> Expr -> Maybe Prop
cryNatGt useFinite n expr
| n == 0 = Just PFalse
| n == 1 = Just (eq expr zero)
| otherwise =
case expr of
K x -> Just $ if Nat n > x then PTrue else PFalse
Var _ -> Nothing
K (Nat m) :+ y -> Just $ if n >= m then gt (k (n m)) y else PFalse
_ :+ _ -> Nothing
x :- y -> Just $ gt (k n :+ y) x
K (Nat m) :* y
| m == 0 -> Just PTrue
| otherwise -> Just $ case divMod n m of
(q,0) -> gt (k q) y
(0,_) -> eq y zero
(q,_) -> gt (k (q + 1)) y
_ :* _ -> Nothing
Div x y -> Just $ gt (k n :* y) x
Mod _ (K (Nat m))
| m <= n -> Just PTrue
Mod (K (Nat m)) _
| m < n -> Just PTrue
Mod _ _ -> Nothing
K (Nat m) :^^ y
| m == 0 -> Just PTrue
| m == 1 -> Just PTrue
| otherwise -> do (a,exact) <- genLog n m
return $ if exact
then gt (k a) y
else gt (k (a + 1)) y
x :^^ K (Nat m)
| m == 0 -> Just PTrue
| m == 1 -> Just (gt (k n) x)
| otherwise -> do (a,exact) <- genRoot n m
return $ if exact
then gt (k a) x
else gt (k (a + 1)) x
_ :^^ _ -> Nothing
Min x y -> Just $ gt (k n) x :|| gt (k n) y
Max x y -> Just $ gt (k n) x :&& gt (k n) y
Width x -> Just $ gt (k (2 ^ n)) x
LenFromThen _ _ _ -> Nothing
LenFromThenTo _ _ _ -> Nothing
where
k x = K (Nat x)
eq x y = if useFinite then x :==: y else x :== y
gt x y = if useFinite then x :>: y else x :> y
cryGtNat :: Bool -> Integer -> Expr -> Maybe Prop
cryGtNat useFinite n expr =
case expr of
K x -> Just $ if x > Nat n then PTrue else PFalse
Var _ -> Nothing
K (Nat m) :+ y
| m > n -> Just PTrue
| otherwise -> Just (gt y (K (Nat (n m))))
x :+ y
| n == 0 -> Just (gt x zero :|| gt y zero)
| otherwise -> Nothing
x :- y -> Just $ gt x (K (Nat n) :+ y)
K (Nat m) :* y
| m > 0 -> Just $ case divMod n m of
(a,_) -> gt y $ K $ Nat a
x :* y
| n == 0 -> Just (gt x zero :&& gt y zero)
| otherwise -> Nothing
Div x y -> Just $ gt (one :+ x) (K (Nat (n+1)) :* y)
Mod _ (K (Nat m))
| m <= n -> Just PFalse
Mod (K (Nat m)) _
| m < n -> Just PFalse
Mod _ _ -> Nothing
K (Nat m) :^^ y
| m == 0 -> Just $ if n == 0 then eq y zero else PFalse
| m == 1 -> Just $ if n == 0 then PTrue else PFalse
| otherwise -> do (a,_exact) <- genLog n m
Just (gt y (K (Nat a)))
x :^^ K (Nat m)
| m == 0 -> Just $ if n == 0 then PTrue else PFalse
| m == 1 -> Just $ gt x (K (Nat n))
| otherwise -> do (a,exact) <- genRoot n m
Just $ if exact
then gt x (K (Nat a))
else gt (one :+ x) (K (Nat (a+1)))
x :^^ y
| n == 0 -> Just (gt x zero :|| eq y zero)
| otherwise -> Nothing
Min x y -> Just $ gt x (K (Nat n)) :&& gt y (K (Nat n))
Max x y -> Just $ gt x (K (Nat n)) :|| gt y (K (Nat n))
Width x -> Just $ gt (one :+ x) (K (Nat (2 ^ n)))
LenFromThen _ _ _
| n == 0 -> Just PTrue
| otherwise -> Nothing
LenFromThenTo x y z
| n == 0 -> Just (gt x y :&& gt z x :|| gt y x :&& gt x z)
| otherwise -> Nothing
where
eq x y = if useFinite then x :==: y else x :== y
gt x y = if useFinite then x :>: y else x :> y
crySimpPropExpr :: Prop -> Prop
crySimpPropExpr p = fromMaybe p (crySimpPropExprMaybe p)
crySimpPropExprMaybe :: Prop -> Maybe Prop
crySimpPropExprMaybe prop =
case prop of
Fin e -> Fin `fmap` crySimpExprMaybe e
a :== b -> binop crySimpExprMaybe (:== ) a b
a :>= b -> binop crySimpExprMaybe (:>= ) a b
a :> b -> binop crySimpExprMaybe (:> ) a b
a :==: b -> binop crySimpExprMaybe (:==:) a b
a :>: b -> binop crySimpExprMaybe (:>: ) a b
a :&& b -> binop crySimpPropExprMaybe (:&&) a b
a :|| b -> binop crySimpPropExprMaybe (:||) a b
Not p -> Not `fmap` crySimpPropExprMaybe p
PFalse -> Nothing
PTrue -> Nothing
where
binop simp f l r =
case (simp l, simp r) of
(Nothing,Nothing) -> Nothing
(l',r') -> Just (f (fromMaybe l l') (fromMaybe r r'))
cryNoInf :: Expr -> IfExpr Expr
cryNoInf expr =
case expr of
x :* y ->
do x' <- cryNoInf x
y' <- cryNoInf y
case (x', y') of
(K Inf, K Inf) -> return inf
(K Inf, _) -> mkIf (y' :==: zero) (return zero) (return inf)
(_, K Inf) -> mkIf (x' :==: zero) (return zero) (return inf)
_ -> return (x' :* y')
x :^^ y ->
do x' <- cryNoInf x
y' <- cryNoInf y
case (x', y') of
(K Inf, K Inf) -> return inf
(K Inf, _) -> mkIf (y' :==: zero) (return one) (return inf)
(_, K Inf) -> mkIf (x' :==: zero) (return zero)
$ mkIf (x' :==: one) (return one)
$ return inf
_ -> return (x' :^^ y')
K _ -> return expr
Var _ -> return expr
x :+ y ->
do x' <- cryNoInf x
y' <- cryNoInf y
case (x', y') of
(K Inf, _) -> return inf
(_, K Inf) -> return inf
_ -> return (x' :+ y')
x :- y ->
do x' <- cryNoInf x
y' <- cryNoInf y
case (x', y') of
(_, K Inf) -> Impossible
(K Inf, _) -> return inf
_ -> mkIf (x' :==: y)
(return zero)
(mkIf (x' :>: y) (return (x' :- y'))
Impossible)
Div x y ->
do x' <- cryNoInf x
y' <- cryNoInf y
case (x', y') of
(K Inf, _) -> Impossible
(_, K Inf) -> return zero
_ -> mkIf (y' :>: zero) (return (Div x' y')) Impossible
Mod x y ->
do x' <- cryNoInf x
mkIf (Fin y)
(do y' <- cryNoInf y
case (x',y') of
(K Inf, _) -> Impossible
(_, K Inf) -> Impossible
_ -> mkIf (y' :>: zero) (return (Mod x' y')) Impossible
)
(return x')
Min x y ->
do x' <- cryNoInf x
y' <- cryNoInf y
case (x',y') of
(K Inf, _) -> return y'
(_, K Inf) -> return x'
_ -> return (Min x' y')
Max x y ->
do x' <- cryNoInf x
y' <- cryNoInf y
case (x', y') of
(K Inf, _) -> return inf
(_, K Inf) -> return inf
_ -> return (Max x' y')
Width x ->
do x' <- cryNoInf x
case x' of
K Inf -> return inf
_ -> return (Width x')
LenFromThen x y w -> fun3 LenFromThen x y w
LenFromThenTo x y z -> fun3 LenFromThenTo x y z
where
fun3 f x y z =
do x' <- cryNoInf x
y' <- cryNoInf y
z' <- cryNoInf z
case (x',y',z') of
(K Inf, _, _) -> Impossible
(_, K Inf, _) -> Impossible
(_, _, K Inf) -> Impossible
_ -> mkIf (x' :==: y') Impossible
(return (f x' y' z'))
mkIf p t e = case crySimplify p of
PTrue -> t
PFalse -> e
p' -> If p' t e
cryNatOp :: (Expr -> Expr -> Prop) -> Expr -> Expr -> Prop
cryNatOp op x y =
toProp $
do x' <- noInf x
y' <- noInf y
return (op x' y')
where
noInf a = do a' <- cryNoInf a
case a' of
K Inf -> Impossible
_ -> return a'
toProp ite =
case ite of
Impossible -> PFalse
Return p -> p
If p t e -> p :&& toProp t :|| Not p :&& toProp e