--------------------------------------------------------------------------------
-- | This module contains common functions used in the implementations of
--     Simplifiable Expr in both Interpreter.hs and PLE.hs.
--------------------------------------------------------------------------------

{-# LANGUAGE PartialTypeSignatures     #-}
{-# LANGUAGE FlexibleInstances         #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE ViewPatterns              #-}

{-# OPTIONS_GHC -Wno-name-shadowing    #-}

module Language.Fixpoint.Solver.Simplify (applyBooleanFolding, applyConstantFolding, applySetFolding, isSetPred) where

import           Language.Fixpoint.Types hiding (simplify)
import           Language.Fixpoint.Smt.Theories
import           Data.Hashable
import qualified Data.HashSet         as S
import qualified Data.Maybe           as Mb


applyBooleanFolding :: Brel -> Expr -> Expr -> Expr
applyBooleanFolding :: Brel -> Expr -> Expr -> Expr
applyBooleanFolding Brel
brel Expr
e1 Expr
e2 =
  case (Expr
e1, Expr
e2) of
    (ECon (R Double
left), ECon (R Double
right)) ->
      forall a. a -> Maybe a -> a
Mb.fromMaybe Expr
e (Brel -> Double -> Double -> Maybe Expr
bfR Brel
brel Double
left Double
right)
    (ECon (R Double
left), ECon (I Integer
right)) ->
      forall a. a -> Maybe a -> a
Mb.fromMaybe Expr
e (Brel -> Double -> Double -> Maybe Expr
bfR Brel
brel Double
left (forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
right))
    (ECon (I Integer
left), ECon (R Double
right)) ->
      forall a. a -> Maybe a -> a
Mb.fromMaybe Expr
e (Brel -> Double -> Double -> Maybe Expr
bfR Brel
brel (forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
left) Double
right)
    (ECon (I Integer
left), ECon (I Integer
right)) ->
      forall a. a -> Maybe a -> a
Mb.fromMaybe Expr
e (Brel -> Integer -> Integer -> Maybe Expr
bfI Brel
brel Integer
left Integer
right)
    (Expr, Expr)
_ -> if Expr -> Bool
isTautoPred Expr
e then Expr
PTrue else
           if Expr -> Bool
isContraPred Expr
e then Expr
PFalse else Expr
e
  where
    e :: Expr
e = Brel -> Expr -> Expr -> Expr
PAtom Brel
brel Expr
e1 Expr
e2

    getOp :: Ord a => Brel -> (a -> a -> Bool)
    getOp :: forall a. Ord a => Brel -> a -> a -> Bool
getOp Brel
Gt   =  forall a. Ord a => a -> a -> Bool
(>)
    getOp Brel
Ge   =  forall a. Ord a => a -> a -> Bool
(>=)
    getOp Brel
Lt   =  forall a. Ord a => a -> a -> Bool
(<)
    getOp Brel
Le   =  forall a. Ord a => a -> a -> Bool
(<=)
    getOp Brel
Eq   =  forall a. Eq a => a -> a -> Bool
(==)
    getOp Brel
Ne   =  forall a. Eq a => a -> a -> Bool
(/=)
    getOp Brel
Ueq  =  forall a. Eq a => a -> a -> Bool
(==)
    getOp Brel
Une  =  forall a. Eq a => a -> a -> Bool
(/=)

    bfR :: Brel -> Double -> Double -> Maybe Expr
    bfR :: Brel -> Double -> Double -> Maybe Expr
bfR Brel
brel Double
left Double
right = if forall a. Ord a => Brel -> a -> a -> Bool
getOp Brel
brel Double
left Double
right then forall a. a -> Maybe a
Just Expr
PTrue else forall a. a -> Maybe a
Just Expr
PFalse

    bfI :: Brel -> Integer -> Integer -> Maybe Expr
    bfI :: Brel -> Integer -> Integer -> Maybe Expr
bfI Brel
brel Integer
left Integer
right = if forall a. Ord a => Brel -> a -> a -> Bool
getOp Brel
brel Integer
left Integer
right then forall a. a -> Maybe a
Just Expr
PTrue else forall a. a -> Maybe a
Just Expr
PFalse


-- | Replace constant integer and floating point expressions by constant values
-- where possible.
applyConstantFolding :: Bop -> Expr -> Expr -> Expr
applyConstantFolding :: Bop -> Expr -> Expr -> Expr
applyConstantFolding Bop
bop Expr
e1 Expr
e2 =
  case (Expr -> Expr
dropECst Expr
e1, Expr -> Expr
dropECst Expr
e2) of
    (ECon (R Double
left), ECon (R Double
right)) ->
      forall a. a -> Maybe a -> a
Mb.fromMaybe Expr
e (Bop -> Double -> Double -> Maybe Expr
cfR Bop
bop Double
left Double
right)
    (ECon (R Double
left), ECon (I Integer
right)) ->
      forall a. a -> Maybe a -> a
Mb.fromMaybe Expr
e (Bop -> Double -> Double -> Maybe Expr
cfR Bop
bop Double
left (forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
right))
    (ECon (I Integer
left), ECon (R Double
right)) ->
      forall a. a -> Maybe a -> a
Mb.fromMaybe Expr
e (Bop -> Double -> Double -> Maybe Expr
cfR Bop
bop (forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
left) Double
right)
    (ECon (I Integer
left), ECon (I Integer
right)) ->
      forall a. a -> Maybe a -> a
Mb.fromMaybe Expr
e (Bop -> Integer -> Integer -> Maybe Expr
cfI Bop
bop Integer
left Integer
right)
    (EBin Bop
Mod  Expr
_   Expr
_              , Expr
_)  -> Expr
e
    (EBin Bop
bop1 Expr
e11 (Expr -> Expr
dropECst -> ECon (R Double
left)), ECon (R Double
right))
      | Bop
bop forall a. Eq a => a -> a -> Bool
== Bop
bop1 -> forall b a. b -> (a -> b) -> Maybe a -> b
maybe Expr
e (Bop -> Expr -> Expr -> Expr
EBin Bop
bop Expr
e11) (Bop -> Double -> Double -> Maybe Expr
cfR (Bop -> Bop
rop Bop
bop) Double
left Double
right)
      | Bool
otherwise   -> Expr
e
    (EBin Bop
bop1 Expr
e11 (Expr -> Expr
dropECst -> ECon (R Double
left)), ECon (I Integer
right))
      | Bop
bop forall a. Eq a => a -> a -> Bool
== Bop
bop1 -> forall b a. b -> (a -> b) -> Maybe a -> b
maybe Expr
e (Bop -> Expr -> Expr -> Expr
EBin Bop
bop Expr
e11) (Bop -> Double -> Double -> Maybe Expr
cfR (Bop -> Bop
rop Bop
bop) Double
left (forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
right))
      | Bool
otherwise   -> Expr
e
    (EBin Bop
bop1 Expr
e11 (Expr -> Expr
dropECst -> ECon (I Integer
left)), ECon (R Double
right))
      | Bop
bop forall a. Eq a => a -> a -> Bool
== Bop
bop1 -> forall b a. b -> (a -> b) -> Maybe a -> b
maybe Expr
e (Bop -> Expr -> Expr -> Expr
EBin Bop
bop Expr
e11) (Bop -> Double -> Double -> Maybe Expr
cfR (Bop -> Bop
rop Bop
bop) (forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
left) Double
right)
      | Bool
otherwise   -> Expr
e
    (EBin Bop
bop1 Expr
e11 (Expr -> Expr
dropECst -> ECon (I Integer
left)), ECon (I Integer
right))
      | Bop
bop forall a. Eq a => a -> a -> Bool
== Bop
bop1 -> forall b a. b -> (a -> b) -> Maybe a -> b
maybe Expr
e (Bop -> Expr -> Expr -> Expr
EBin Bop
bop Expr
e11) (Bop -> Integer -> Integer -> Maybe Expr
cfI (Bop -> Bop
rop Bop
bop) Integer
left Integer
right)
      | Bool
otherwise   -> Expr
e
    (Expr, Expr)
_ -> Expr
e
  where

    rop :: Bop -> Bop
    rop :: Bop -> Bop
rop Bop
Plus   = Bop
Plus
    rop Bop
Minus  = Bop
Plus
    rop Bop
Times  = Bop
Times
    rop Bop
Div    = Bop
Times
    rop Bop
RTimes = Bop
RTimes
    rop Bop
RDiv   = Bop
RTimes
    rop Bop
Mod    = Bop
Mod

    e :: Expr
e = Bop -> Expr -> Expr -> Expr
EBin Bop
bop Expr
e1 Expr
e2

    getOp :: Num a => Bop -> Maybe (a -> a -> a)
    getOp :: forall a. Num a => Bop -> Maybe (a -> a -> a)
getOp Bop
Minus    = forall a. a -> Maybe a
Just (-)
    getOp Bop
Plus     = forall a. a -> Maybe a
Just forall a. Num a => a -> a -> a
(+)
    getOp Bop
Times    = forall a. a -> Maybe a
Just forall a. Num a => a -> a -> a
(*)
    getOp Bop
RTimes   = forall a. a -> Maybe a
Just forall a. Num a => a -> a -> a
(*)
    getOp Bop
_        = forall a. Maybe a
Nothing

    cfR :: Bop -> Double -> Double -> Maybe Expr
    cfR :: Bop -> Double -> Double -> Maybe Expr
cfR Bop
bop Double
left Double
right = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Double -> Double -> Double) -> Expr
go (forall {a}. Fractional a => Bop -> Maybe (a -> a -> a)
getOp' Bop
bop)
      where
        go :: (Double -> Double -> Double) -> Expr
go Double -> Double -> Double
f = Constant -> Expr
ECon forall a b. (a -> b) -> a -> b
$ Double -> Constant
R forall a b. (a -> b) -> a -> b
$ Double -> Double -> Double
f Double
left Double
right

        getOp' :: Bop -> Maybe (a -> a -> a)
getOp' Bop
Div      = forall a. a -> Maybe a
Just forall a. Fractional a => a -> a -> a
(/)
        getOp' Bop
RDiv     = forall a. a -> Maybe a
Just forall a. Fractional a => a -> a -> a
(/)
        getOp' Bop
op       = forall a. Num a => Bop -> Maybe (a -> a -> a)
getOp Bop
op

    cfI :: Bop -> Integer -> Integer -> Maybe Expr
    cfI :: Bop -> Integer -> Integer -> Maybe Expr
cfI Bop
bop Integer
left Integer
right = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Integer -> Integer -> Integer) -> Expr
go (forall {a}. Integral a => Bop -> Maybe (a -> a -> a)
getOp' Bop
bop)
      where
        go :: (Integer -> Integer -> Integer) -> Expr
go Integer -> Integer -> Integer
f = Constant -> Expr
ECon forall a b. (a -> b) -> a -> b
$ Integer -> Constant
I forall a b. (a -> b) -> a -> b
$ Integer -> Integer -> Integer
f Integer
left Integer
right

        getOp' :: Bop -> Maybe (a -> a -> a)
getOp' Bop
Mod = forall a. a -> Maybe a
Just forall a. Integral a => a -> a -> a
mod
        getOp' Bop
op  = forall a. Num a => Bop -> Maybe (a -> a -> a)
getOp Bop
op

isSetPred :: Expr -> Bool
isSetPred :: Expr -> Bool
isSetPred (EVar Symbol
s) | Symbol
s forall a. Eq a => a -> a -> Bool
== Symbol
setEmp          = Bool
True
isSetPred (EApp Expr
e1 Expr
_) = case Expr
e1 of
  (EVar Symbol
s) | Symbol
s forall a. Eq a => a -> a -> Bool
== Symbol
setMem Bool -> Bool -> Bool
|| Symbol
s forall a. Eq a => a -> a -> Bool
== Symbol
setSub  -> Bool
True
  Expr
_                                      -> Bool
False
isSetPred Expr
_                               = Bool
False

-- Note: this is currently limited to sets of integer constants
applySetFolding :: Expr -> Expr -> Expr
applySetFolding :: Expr -> Expr -> Expr
applySetFolding Expr
e1 Expr
e2   = case Expr
e1 of
    (EVar Symbol
s) | Symbol
s forall a. Eq a => a -> a -> Bool
== Symbol
setEmp
      -> forall b a. b -> (a -> b) -> Maybe a -> b
maybe Expr
e (Bool -> Expr
fromBool forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. HashSet a -> Bool
S.null) (Expr -> Maybe (HashSet Integer)
evalSetI Expr
e2)
    (EApp (EVar Symbol
s) Expr
e1') | Symbol
s forall a. Eq a => a -> a -> Bool
== Symbol
setMem
      -> forall b a. b -> (a -> b) -> Maybe a -> b
maybe Expr
e Bool -> Expr
fromBool (forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
S.member forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> Maybe Integer
getInt Expr
e1' forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr -> Maybe (HashSet Integer)
evalSetI Expr
e2)
                        | Symbol
s forall a. Eq a => a -> a -> Bool
== Symbol
setEmp
      -> forall b a. b -> (a -> b) -> Maybe a -> b
maybe Expr
e (Bool -> Expr
fromBool forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. HashSet a -> Bool
S.null) (forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
S.difference forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> Maybe (HashSet Integer)
evalSetI Expr
e1' forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr -> Maybe (HashSet Integer)
evalSetI Expr
e2)
                        | Bool
otherwise
      -> Expr
e
    Expr
_                   -> Expr
e
  where
    e :: Expr
e = Expr -> Expr -> Expr
EApp Expr
e1 Expr
e2

    fromBool :: Bool -> Expr
fromBool Bool
True  = Expr
PTrue
    fromBool Bool
False = Expr
PFalse

    getInt :: Expr -> Maybe Integer
    getInt :: Expr -> Maybe Integer
getInt (ECon (I Integer
n)) = forall a. a -> Maybe a
Just Integer
n
    getInt Expr
_            = forall a. Maybe a
Nothing

    getOp :: (Eq a, Hashable a) => Symbol -> Maybe (S.HashSet a -> S.HashSet a -> S.HashSet a)
    getOp :: forall a.
(Eq a, Hashable a) =>
Symbol -> Maybe (HashSet a -> HashSet a -> HashSet a)
getOp Symbol
s | Symbol
s forall a. Eq a => a -> a -> Bool
== Symbol
setCup = forall a. a -> Maybe a
Just forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
S.union
            | Symbol
s forall a. Eq a => a -> a -> Bool
== Symbol
setCap = forall a. a -> Maybe a
Just forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
S.intersection
            | Symbol
s forall a. Eq a => a -> a -> Bool
== Symbol
setDif = forall a. a -> Maybe a
Just forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
S.difference
            | Bool
otherwise   = forall a. Maybe a
Nothing

    evalSetI :: Expr -> Maybe (S.HashSet Integer)
    evalSetI :: Expr -> Maybe (HashSet Integer)
evalSetI (EApp Expr
e1 Expr
e2) = case Expr
e1 of
      (EVar Symbol
s) | Symbol
s forall a. Eq a => a -> a -> Bool
== Symbol
setEmpty -> forall a. a -> Maybe a
Just forall a. HashSet a
S.empty
               | Symbol
s forall a. Eq a => a -> a -> Bool
== Symbol
setSng   -> case Expr
e2 of
        (ECon (I Integer
n))             -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. Hashable a => a -> HashSet a
S.singleton Integer
n
        Expr
_                        -> forall a. Maybe a
Nothing
      (EApp (EVar Symbol
f) Expr
e1')  -> forall a.
(Eq a, Hashable a) =>
Symbol -> Maybe (HashSet a -> HashSet a -> HashSet a)
getOp Symbol
f forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr -> Maybe (HashSet Integer)
evalSetI Expr
e1' forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr -> Maybe (HashSet Integer)
evalSetI Expr
e2
      Expr
_                    -> forall a. Maybe a
Nothing
    evalSetI Expr
_            = forall a. Maybe a
Nothing