content: --------------------------------------------------------------------------------
  -- | 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              #-}
  
  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' e1 e2 =
    case (e1, e2) of
      (ECon (R left), ECon (R right)) ->
        Mb.fromMaybe e (bfR brel' left right)
      (ECon (R left), ECon (I right)) ->
        Mb.fromMaybe e (bfR brel' left (fromIntegral right))
      (ECon (I left), ECon (R right)) ->
        Mb.fromMaybe e (bfR brel' (fromIntegral left) right)
      (ECon (I left), ECon (I right)) ->
        Mb.fromMaybe e (bfI brel' left right)
      _ -> if isTautoPred e then PTrue else
             if isContraPred e then PFalse else e
    where
      e = PAtom brel' e1 e2
  
      getOp :: Ord a => Brel -> (a -> a -> Bool)
      getOp Gt   =  (>)
      getOp Ge   =  (>=)
      getOp Lt   =  (<)
      getOp Le   =  (<=)
      getOp Eq   =  (==)
      getOp Ne   =  (/=)
      getOp Ueq  =  (==)
      getOp Une  =  (/=)
  
      bfR :: Brel -> Double -> Double -> Maybe Expr
      bfR brel left right = if getOp brel left right then Just PTrue else Just PFalse
  
      bfI :: Brel -> Integer -> Integer -> Maybe Expr
      bfI brel left right = if getOp brel left right then Just PTrue else Just PFalse
  
  
  -- | Replace constant integer and floating point expressions by constant values
  -- where possible.
  applyConstantFolding :: Bop -> Expr -> Expr -> Expr
  applyConstantFolding bop' e1 e2 =
    case (dropECst e1, dropECst e2) of
      (ECon (R left), ECon (R right)) ->
        Mb.fromMaybe e (cfR bop' left right)
      (ECon (R left), ECon (I right)) ->
        Mb.fromMaybe e (cfR bop' left (fromIntegral right))
      (ECon (I left), ECon (R right)) ->
        Mb.fromMaybe e (cfR bop' (fromIntegral left) right)
      (ECon (I left), ECon (I right)) ->
        Mb.fromMaybe e (cfI bop' left right)
      (EBin Mod  _   _              , _)  -> e
      (EBin bop1 e11 (dropECst -> ECon (R left)), ECon (R right))
        | bop' == bop1 -> maybe e (EBin bop' e11) (cfR (rop bop') left right)
        | otherwise   -> e
      (EBin bop1 e11 (dropECst -> ECon (R left)), ECon (I right))
        | bop' == bop1 -> maybe e (EBin bop' e11) (cfR (rop bop') left (fromIntegral right))
        | otherwise   -> e
      (EBin bop1 e11 (dropECst -> ECon (I left)), ECon (R right))
        | bop' == bop1 -> maybe e (EBin bop' e11) (cfR (rop bop') (fromIntegral left) right)
        | otherwise   -> e
      (EBin bop1 e11 (dropECst -> ECon (I left)), ECon (I right))
        | bop' == bop1 -> maybe e (EBin bop' e11) (cfI (rop bop') left right)
        | otherwise   -> e
      _ -> e
    where
  
      rop :: Bop -> Bop
      rop Plus   = Plus
      rop Minus  = Plus
      rop Times  = Times
      rop Div    = Times
      rop RTimes = RTimes
      rop RDiv   = RTimes
      rop Mod    = Mod
  
      e = EBin bop' e1 e2
  
      getOp :: Num a => Bop -> Maybe (a -> a -> a)
      getOp Minus    = Just (-)
      getOp Plus     = Just (+)
      getOp Times    = Just (*)
      getOp RTimes   = Just (*)
      getOp _        = Nothing
  
      cfR :: Bop -> Double -> Double -> Maybe Expr
      cfR bop left right = go (getOp' bop)
        where
          go (Just f) =
            let x = f left right
             in if isNaN x || isInfinite x then Just $ ECon (R x)
                else Nothing
          go Nothing = Nothing
  
          getOp' Div  | right /= 0 = Just (/)
          getOp' RDiv | right /= 0 = Just (/)
          getOp' op = getOp op
  
      cfI :: Bop -> Integer -> Integer -> Maybe Expr
      cfI bop left right = fmap go (getOp' bop)
        where
          go f = ECon $ I $ f left right
  
          getOp' Mod | right /= 0 = Just mod
          getOp' op  = getOp op
  
  isSetPred :: Expr -> Bool
  isSetPred (EVar s) | s == setEmp          = True
  isSetPred (EApp e1 _) = case e1 of
    (EVar s) | s == setMem || s == setSub  -> True
    _                                      -> False
  isSetPred _                               = False
  
  -- Note: this is currently limited to sets of integer constants
  applySetFolding :: Expr -> Expr -> Expr
  applySetFolding expr1 expr2   = case expr1 of
      (EVar s) | s == setEmp
        -> maybe e (fromBool . S.null) (evalSetI expr2)
      (EApp (EVar s) e1') | s == setMem
        -> maybe e fromBool (S.member <$> getInt e1' <*> evalSetI expr2)
                          | s == setEmp
        -> maybe e (fromBool . S.null) (S.difference <$> evalSetI e1' <*> evalSetI expr2)
                          | otherwise
        -> e
      _                   -> e
    where
      e = EApp expr1 expr2
  
      fromBool True  = PTrue
      fromBool False = PFalse
  
      getInt :: Expr -> Maybe Integer
      getInt (ECon (I n)) = Just n
      getInt _            = Nothing
  
      getOp :: (Eq a, Hashable a) => Symbol -> Maybe (S.HashSet a -> S.HashSet a -> S.HashSet a)
      getOp s | s == setCup = Just S.union
              | s == setCap = Just S.intersection
              | s == setDif = Just S.difference
              | otherwise   = Nothing
  
      evalSetI :: Expr -> Maybe (S.HashSet Integer)
      evalSetI (EApp e1 e2) = case e1 of
        (EVar s) | s == setEmpty -> Just S.empty
                 | s == setSng   -> case e2 of
          (ECon (I n))             -> Just $ S.singleton n
          _                        -> Nothing
        (EApp (EVar f) e1')  -> getOp f <*> evalSetI e1' <*> evalSetI e2
        _                    -> Nothing
      evalSetI _            = Nothing
  
  