{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Language.Fortran.Vars.CPValue
  ( CPValue(..)
  , meet
  , unaryOper
  , binaryOper
  , isTop
  , isBot
  , isConstInt
  )
where

import           Language.Fortran.Vars.Types
                                                ( ExpVal(..) )
import           Language.Fortran.Vars.Operation
                                                ( unaryOp
                                                , binaryOp
                                                )

import           Language.Fortran.AST           ( UnaryOp(..)
                                                , BinaryOp(..)
                                                )

import           Data.Data                      ( Data )
import           Data.Typeable                  ( Typeable )
import           GHC.Generics                   ( Generic )
import           Control.DeepSeq                ( NFData )

-- | CPValue (Constant Propagation Value) represnts the value of an expression
-- determined by constant propagation analysis.
-- The value can be uninitialized, a constant, or unknown due to conflict.
-- The data type is represented with 'ExpVal' together with two special values:
-- Top represents uninitialized value and is the least upper bound
-- Bot represents unknown and is the greatest lower bound
-- Top, Const, and Bot forms a lattice strucutre with meet operation defined below
data CPValue
  = Top           -- ^ represents uninitialized value
  | Const ExpVal  -- ^ represents a constant value
  | Bot           -- ^ short for bottom, represents unknown value
  deriving (CPValue -> CPValue -> Bool
(CPValue -> CPValue -> Bool)
-> (CPValue -> CPValue -> Bool) -> Eq CPValue
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: CPValue -> CPValue -> Bool
$c/= :: CPValue -> CPValue -> Bool
== :: CPValue -> CPValue -> Bool
$c== :: CPValue -> CPValue -> Bool
Eq, Eq CPValue
Eq CPValue
-> (CPValue -> CPValue -> Ordering)
-> (CPValue -> CPValue -> Bool)
-> (CPValue -> CPValue -> Bool)
-> (CPValue -> CPValue -> Bool)
-> (CPValue -> CPValue -> Bool)
-> (CPValue -> CPValue -> CPValue)
-> (CPValue -> CPValue -> CPValue)
-> Ord CPValue
CPValue -> CPValue -> Bool
CPValue -> CPValue -> Ordering
CPValue -> CPValue -> CPValue
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: CPValue -> CPValue -> CPValue
$cmin :: CPValue -> CPValue -> CPValue
max :: CPValue -> CPValue -> CPValue
$cmax :: CPValue -> CPValue -> CPValue
>= :: CPValue -> CPValue -> Bool
$c>= :: CPValue -> CPValue -> Bool
> :: CPValue -> CPValue -> Bool
$c> :: CPValue -> CPValue -> Bool
<= :: CPValue -> CPValue -> Bool
$c<= :: CPValue -> CPValue -> Bool
< :: CPValue -> CPValue -> Bool
$c< :: CPValue -> CPValue -> Bool
compare :: CPValue -> CPValue -> Ordering
$ccompare :: CPValue -> CPValue -> Ordering
Ord, Int -> CPValue -> ShowS
[CPValue] -> ShowS
CPValue -> String
(Int -> CPValue -> ShowS)
-> (CPValue -> String) -> ([CPValue] -> ShowS) -> Show CPValue
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [CPValue] -> ShowS
$cshowList :: [CPValue] -> ShowS
show :: CPValue -> String
$cshow :: CPValue -> String
showsPrec :: Int -> CPValue -> ShowS
$cshowsPrec :: Int -> CPValue -> ShowS
Show, Typeable CPValue
Typeable CPValue
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> CPValue -> c CPValue)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c CPValue)
-> (CPValue -> Constr)
-> (CPValue -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c CPValue))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CPValue))
-> ((forall b. Data b => b -> b) -> CPValue -> CPValue)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> CPValue -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> CPValue -> r)
-> (forall u. (forall d. Data d => d -> u) -> CPValue -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> CPValue -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> CPValue -> m CPValue)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> CPValue -> m CPValue)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> CPValue -> m CPValue)
-> Data CPValue
CPValue -> DataType
CPValue -> Constr
(forall b. Data b => b -> b) -> CPValue -> CPValue
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> CPValue -> u
forall u. (forall d. Data d => d -> u) -> CPValue -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> CPValue -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> CPValue -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> CPValue -> m CPValue
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> CPValue -> m CPValue
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c CPValue
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> CPValue -> c CPValue
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c CPValue)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CPValue)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> CPValue -> m CPValue
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> CPValue -> m CPValue
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> CPValue -> m CPValue
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> CPValue -> m CPValue
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> CPValue -> m CPValue
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> CPValue -> m CPValue
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> CPValue -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> CPValue -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> CPValue -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> CPValue -> [u]
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> CPValue -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> CPValue -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> CPValue -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> CPValue -> r
gmapT :: (forall b. Data b => b -> b) -> CPValue -> CPValue
$cgmapT :: (forall b. Data b => b -> b) -> CPValue -> CPValue
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CPValue)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CPValue)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c CPValue)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c CPValue)
dataTypeOf :: CPValue -> DataType
$cdataTypeOf :: CPValue -> DataType
toConstr :: CPValue -> Constr
$ctoConstr :: CPValue -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c CPValue
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c CPValue
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> CPValue -> c CPValue
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> CPValue -> c CPValue
Data, Typeable, (forall x. CPValue -> Rep CPValue x)
-> (forall x. Rep CPValue x -> CPValue) -> Generic CPValue
forall x. Rep CPValue x -> CPValue
forall x. CPValue -> Rep CPValue x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep CPValue x -> CPValue
$cfrom :: forall x. CPValue -> Rep CPValue x
Generic, CPValue -> ()
(CPValue -> ()) -> NFData CPValue
forall a. (a -> ()) -> NFData a
rnf :: CPValue -> ()
$crnf :: CPValue -> ()
NFData)


-- | meet operation for CPValue lattice with user defined function to handle
-- two Const values
meetWith :: (ExpVal -> ExpVal -> CPValue) -> CPValue -> CPValue -> CPValue
meetWith :: (ExpVal -> ExpVal -> CPValue) -> CPValue -> CPValue -> CPValue
meetWith ExpVal -> ExpVal -> CPValue
f CPValue
v1 CPValue
v2 = case (CPValue
v1, CPValue
v2) of
  (CPValue
Bot     , CPValue
_       ) -> CPValue
Bot
  (CPValue
_       , CPValue
Bot     ) -> CPValue
Bot
  (CPValue
Top     , CPValue
v       ) -> CPValue
v
  (CPValue
v       , CPValue
Top     ) -> CPValue
v
  (Const ExpVal
c1, Const ExpVal
c2) -> ExpVal -> ExpVal -> CPValue
f ExpVal
c1 ExpVal
c2

-- | meet operation for CPValue lattice.
-- meet of two different constant value indicates conflict, therefore yields Bot.
meet :: CPValue -> CPValue -> CPValue
meet :: CPValue -> CPValue -> CPValue
meet = (ExpVal -> ExpVal -> CPValue) -> CPValue -> CPValue -> CPValue
meetWith (\ExpVal
c1 ExpVal
c2 -> if ExpVal
c1 ExpVal -> ExpVal -> Bool
forall a. Eq a => a -> a -> Bool
== ExpVal
c2 then ExpVal -> CPValue
Const ExpVal
c1 else CPValue
Bot)


unaryOper :: UnaryOp -> CPValue -> CPValue
unaryOper :: UnaryOp -> CPValue -> CPValue
unaryOper UnaryOp
op CPValue
v = case CPValue
v of
  CPValue
Top          -> CPValue
Top
  CPValue
Bot          -> CPValue
Bot
  Const ExpVal
expVal -> ExpVal -> CPValue
Const (UnaryOp -> ExpVal -> ExpVal
unaryOp UnaryOp
op ExpVal
expVal)

binaryOper :: BinaryOp -> CPValue -> CPValue -> CPValue
binaryOper :: BinaryOp -> CPValue -> CPValue -> CPValue
binaryOper BinaryOp
op CPValue
v1 CPValue
v2 = case (BinaryOp
op, CPValue
v1, CPValue
v2) of
  (BinaryOp
Multiplication, Const (Int Int
0), CPValue
_) -> ExpVal -> CPValue
Const (Int -> ExpVal
Int Int
0)
  (BinaryOp
Multiplication, CPValue
_, Const (Int Int
0)) -> ExpVal -> CPValue
Const (Int -> ExpVal
Int Int
0)
  (BinaryOp
Multiplication, Const (Real Double
0.0), CPValue
_) -> ExpVal -> CPValue
Const (Double -> ExpVal
Real Double
0.0)
  (BinaryOp
Multiplication, CPValue
_, Const (Real Double
0.0)) -> ExpVal -> CPValue
Const (Double -> ExpVal
Real Double
0.0)
  (BinaryOp
Exponentiation, Const (Real Double
1.0), CPValue
_) -> ExpVal -> CPValue
Const (Double -> ExpVal
Real Double
1.0)
  (BinaryOp
Exponentiation, Const (Int Int
1), CPValue
_) -> ExpVal -> CPValue
Const (Double -> ExpVal
Real Double
1.0)
  (BinaryOp
Exponentiation, CPValue
_, Const (Real Double
0.0)) -> ExpVal -> CPValue
Const (Double -> ExpVal
Real Double
1.0)
  (BinaryOp
Exponentiation, CPValue
_, Const (Int Int
0)) -> ExpVal -> CPValue
Const (Double -> ExpVal
Real Double
1.0)
  (BinaryOp
And, Const (Logical Bool
False), CPValue
_) -> ExpVal -> CPValue
Const (Bool -> ExpVal
Logical Bool
False)
  (BinaryOp
And, CPValue
_, Const (Logical Bool
False)) -> ExpVal -> CPValue
Const (Bool -> ExpVal
Logical Bool
False)
  (BinaryOp
Or, Const (Logical Bool
True), CPValue
_) -> ExpVal -> CPValue
Const (Bool -> ExpVal
Logical Bool
True)
  (BinaryOp
Or, CPValue
_, Const (Logical Bool
True)) -> ExpVal -> CPValue
Const (Bool -> ExpVal
Logical Bool
True)
  (BinaryOp
_, CPValue
Bot, CPValue
_) -> CPValue
Bot
  (BinaryOp
_, CPValue
_, CPValue
Bot) -> CPValue
Bot
  (BinaryOp
_, CPValue
Top, CPValue
_) -> CPValue
Top
  (BinaryOp
_, CPValue
_, CPValue
Top) -> CPValue
Top
  (BinaryOp
_, Const ExpVal
x, Const ExpVal
y) -> ExpVal -> CPValue
Const (BinaryOp -> ExpVal -> ExpVal -> ExpVal
binaryOp BinaryOp
op ExpVal
x ExpVal
y)


isTop :: CPValue -> Bool
isTop :: CPValue -> Bool
isTop CPValue
Top = Bool
True
isTop CPValue
_   = Bool
False

isBot :: CPValue -> Bool
isBot :: CPValue -> Bool
isBot CPValue
Bot = Bool
True
isBot CPValue
_   = Bool
False

isConstInt :: CPValue -> Bool
isConstInt :: CPValue -> Bool
isConstInt (Const Int{}) = Bool
True
isConstInt CPValue
_             = Bool
False