{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE LambdaCase            #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NamedFieldPuns        #-}
{-# LANGUAGE PolyKinds             #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE TemplateHaskell       #-}
{-# LANGUAGE TypeFamilies          #-}

{-# OPTIONS_GHC -Wall #-}

-- TODO: Variables for user-defined data types

{-|

Defines a strongly-typed representation of Fortran variables.

-}
module Language.Fortran.Model.Vars
  (
    -- * Variables
    FortranVar(..)
    -- * Names
  , NamePair(..)
  , npSource
  , npUnique
  , SourceName(..)
  , UniqueName(..)
  ) where

import           Data.Typeable                      ((:~:) (..))

import           Control.Lens                       hiding (Index, op)

import           Data.SBV.Dynamic
import           Data.SBV                           (MonadSymbolic(..))

import           Control.Monad.Trans.Class          (lift)

import           Data.Vinyl                         (rtraverse)

import qualified Language.Fortran.AST               as F

import           Language.Expression.Pretty
import           Language.Verification

import           Language.Fortran.Model.Repr
import           Language.Fortran.Model.Repr.Prim
import           Language.Fortran.Model.Types
import           Language.Fortran.Model.Types.Match

--------------------------------------------------------------------------------
--  Names
--------------------------------------------------------------------------------

-- | Newtype wrapper for source-level variable names.
newtype SourceName = SourceName { SourceName -> Name
getSourceName :: F.Name }
  deriving (SourceName -> SourceName -> Bool
(SourceName -> SourceName -> Bool)
-> (SourceName -> SourceName -> Bool) -> Eq SourceName
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SourceName -> SourceName -> Bool
$c/= :: SourceName -> SourceName -> Bool
== :: SourceName -> SourceName -> Bool
$c== :: SourceName -> SourceName -> Bool
Eq, Eq SourceName
Eq SourceName
-> (SourceName -> SourceName -> Ordering)
-> (SourceName -> SourceName -> Bool)
-> (SourceName -> SourceName -> Bool)
-> (SourceName -> SourceName -> Bool)
-> (SourceName -> SourceName -> Bool)
-> (SourceName -> SourceName -> SourceName)
-> (SourceName -> SourceName -> SourceName)
-> Ord SourceName
SourceName -> SourceName -> Bool
SourceName -> SourceName -> Ordering
SourceName -> SourceName -> SourceName
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 :: SourceName -> SourceName -> SourceName
$cmin :: SourceName -> SourceName -> SourceName
max :: SourceName -> SourceName -> SourceName
$cmax :: SourceName -> SourceName -> SourceName
>= :: SourceName -> SourceName -> Bool
$c>= :: SourceName -> SourceName -> Bool
> :: SourceName -> SourceName -> Bool
$c> :: SourceName -> SourceName -> Bool
<= :: SourceName -> SourceName -> Bool
$c<= :: SourceName -> SourceName -> Bool
< :: SourceName -> SourceName -> Bool
$c< :: SourceName -> SourceName -> Bool
compare :: SourceName -> SourceName -> Ordering
$ccompare :: SourceName -> SourceName -> Ordering
$cp1Ord :: Eq SourceName
Ord)

instance Show SourceName where show :: SourceName -> Name
show = ShowS
forall a. Show a => a -> Name
show ShowS -> (SourceName -> Name) -> SourceName -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SourceName -> Name
getSourceName

-- | Newtype wrapper for unique variable names.
newtype UniqueName = UniqueName { UniqueName -> Name
getUniqueName :: F.Name }
  deriving (UniqueName -> UniqueName -> Bool
(UniqueName -> UniqueName -> Bool)
-> (UniqueName -> UniqueName -> Bool) -> Eq UniqueName
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: UniqueName -> UniqueName -> Bool
$c/= :: UniqueName -> UniqueName -> Bool
== :: UniqueName -> UniqueName -> Bool
$c== :: UniqueName -> UniqueName -> Bool
Eq, Eq UniqueName
Eq UniqueName
-> (UniqueName -> UniqueName -> Ordering)
-> (UniqueName -> UniqueName -> Bool)
-> (UniqueName -> UniqueName -> Bool)
-> (UniqueName -> UniqueName -> Bool)
-> (UniqueName -> UniqueName -> Bool)
-> (UniqueName -> UniqueName -> UniqueName)
-> (UniqueName -> UniqueName -> UniqueName)
-> Ord UniqueName
UniqueName -> UniqueName -> Bool
UniqueName -> UniqueName -> Ordering
UniqueName -> UniqueName -> UniqueName
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 :: UniqueName -> UniqueName -> UniqueName
$cmin :: UniqueName -> UniqueName -> UniqueName
max :: UniqueName -> UniqueName -> UniqueName
$cmax :: UniqueName -> UniqueName -> UniqueName
>= :: UniqueName -> UniqueName -> Bool
$c>= :: UniqueName -> UniqueName -> Bool
> :: UniqueName -> UniqueName -> Bool
$c> :: UniqueName -> UniqueName -> Bool
<= :: UniqueName -> UniqueName -> Bool
$c<= :: UniqueName -> UniqueName -> Bool
< :: UniqueName -> UniqueName -> Bool
$c< :: UniqueName -> UniqueName -> Bool
compare :: UniqueName -> UniqueName -> Ordering
$ccompare :: UniqueName -> UniqueName -> Ordering
$cp1Ord :: Eq UniqueName
Ord)

instance Show UniqueName where show :: UniqueName -> Name
show = ShowS
forall a. Show a => a -> Name
show ShowS -> (UniqueName -> Name) -> UniqueName -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UniqueName -> Name
getUniqueName

makeWrapped ''SourceName
makeWrapped ''UniqueName

-- | A 'NamePair' represents the name of some part of a Fortran program,
-- including the human-readable source name and the unique name.
data NamePair =
  NamePair
  { NamePair -> UniqueName
_npUnique :: UniqueName
  , NamePair -> SourceName
_npSource :: SourceName
  }
  deriving (NamePair -> NamePair -> Bool
(NamePair -> NamePair -> Bool)
-> (NamePair -> NamePair -> Bool) -> Eq NamePair
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: NamePair -> NamePair -> Bool
$c/= :: NamePair -> NamePair -> Bool
== :: NamePair -> NamePair -> Bool
$c== :: NamePair -> NamePair -> Bool
Eq, Eq NamePair
Eq NamePair
-> (NamePair -> NamePair -> Ordering)
-> (NamePair -> NamePair -> Bool)
-> (NamePair -> NamePair -> Bool)
-> (NamePair -> NamePair -> Bool)
-> (NamePair -> NamePair -> Bool)
-> (NamePair -> NamePair -> NamePair)
-> (NamePair -> NamePair -> NamePair)
-> Ord NamePair
NamePair -> NamePair -> Bool
NamePair -> NamePair -> Ordering
NamePair -> NamePair -> NamePair
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 :: NamePair -> NamePair -> NamePair
$cmin :: NamePair -> NamePair -> NamePair
max :: NamePair -> NamePair -> NamePair
$cmax :: NamePair -> NamePair -> NamePair
>= :: NamePair -> NamePair -> Bool
$c>= :: NamePair -> NamePair -> Bool
> :: NamePair -> NamePair -> Bool
$c> :: NamePair -> NamePair -> Bool
<= :: NamePair -> NamePair -> Bool
$c<= :: NamePair -> NamePair -> Bool
< :: NamePair -> NamePair -> Bool
$c< :: NamePair -> NamePair -> Bool
compare :: NamePair -> NamePair -> Ordering
$ccompare :: NamePair -> NamePair -> Ordering
$cp1Ord :: Eq NamePair
Ord, Int -> NamePair -> ShowS
[NamePair] -> ShowS
NamePair -> Name
(Int -> NamePair -> ShowS)
-> (NamePair -> Name) -> ([NamePair] -> ShowS) -> Show NamePair
forall a.
(Int -> a -> ShowS) -> (a -> Name) -> ([a] -> ShowS) -> Show a
showList :: [NamePair] -> ShowS
$cshowList :: [NamePair] -> ShowS
show :: NamePair -> Name
$cshow :: NamePair -> Name
showsPrec :: Int -> NamePair -> ShowS
$cshowsPrec :: Int -> NamePair -> ShowS
Show)

makeLenses ''NamePair

instance Pretty SourceName where
  pretty :: SourceName -> Name
pretty = Getting Name SourceName Name -> SourceName -> Name
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting Name SourceName Name
forall s t. Rewrapping s t => Iso s t (Unwrapped s) (Unwrapped t)
_Wrapped

-- | The pretty version of a 'NamePair' is its source name.
instance Pretty NamePair where
  pretty :: NamePair -> Name
pretty = SourceName -> Name
forall a. Pretty a => a -> Name
pretty (SourceName -> Name)
-> (NamePair -> SourceName) -> NamePair -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Getting SourceName NamePair SourceName -> NamePair -> SourceName
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting SourceName NamePair SourceName
Lens' NamePair SourceName
npSource

--------------------------------------------------------------------------------
--  Fortran Variables
--------------------------------------------------------------------------------

-- | A variable representing a value of type @a@. Contains a @'D' a@ as proof
-- that the type has a corresponding Fortran type, and the variable name.
data FortranVar a where
  FortranVar :: D a -> NamePair -> FortranVar a

instance VerifiableVar FortranVar where
  type VarKey FortranVar = UniqueName
  type VarSym FortranVar = CoreRepr
  type VarEnv FortranVar = PrimReprHandlers

  symForVar :: FortranVar a -> VarEnv FortranVar -> Symbolic (VarSym FortranVar a)
symForVar (FortranVar D a
d NamePair
np) VarEnv FortranVar
env =
    case D a
d of
      DPrim Prim p k a
prim -> D (PrimS a) -> SVal -> CoreRepr (PrimS a)
forall a. D (PrimS a) -> SVal -> CoreRepr (PrimS a)
CRPrim D a
D (PrimS a)
d (SVal -> CoreRepr (PrimS a))
-> SymbolicT IO SVal -> SymbolicT IO (CoreRepr (PrimS a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Prim p k a -> Name -> PrimReprHandlers -> SymbolicT IO SVal
forall r (m :: * -> *) (p :: Precision) (k :: BasicType) a.
(MonadReader r m, HasPrimReprHandlers r) =>
Prim p k a -> Name -> m (SymbolicT IO SVal)
primSymbolic Prim p k a
prim Name
uniqueName VarEnv FortranVar
PrimReprHandlers
env
      DArray Index i
i ArrValue a
val -> D (Array i a) -> ArrRepr i a -> CoreRepr (Array i a)
forall k (i :: k) a.
D (Array i a) -> ArrRepr i a -> CoreRepr (Array i a)
CRArray D a
D (Array i a)
d (ArrRepr i a -> CoreRepr (Array i a))
-> SymbolicT IO (ArrRepr i a)
-> SymbolicT IO (CoreRepr (Array i a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Index i
-> ArrValue a
-> Name
-> PrimReprHandlers
-> SymbolicT IO (ArrRepr i a)
forall r i a.
HasPrimReprHandlers r =>
Index i -> ArrValue a -> Name -> r -> Symbolic (ArrRepr i a)
arraySymbolic Index i
i ArrValue a
val Name
uniqueName VarEnv FortranVar
PrimReprHandlers
env
      DData SSymbol name
_ Rec (Field D) fs
_ -> Name -> SymbolicT IO (CoreRepr (Record name fs))
forall (m :: * -> *) a. MonadFail m => Name -> m a
fail Name
"User-defined data type variables are not supported yet"
    where
      uniqueName :: Name
uniqueName = NamePair
np NamePair -> Getting Name NamePair Name -> Name
forall s a. s -> Getting a s a -> a
^. (UniqueName -> Const Name UniqueName)
-> NamePair -> Const Name NamePair
Lens' NamePair UniqueName
npUnique ((UniqueName -> Const Name UniqueName)
 -> NamePair -> Const Name NamePair)
-> ((Name -> Const Name Name)
    -> UniqueName -> Const Name UniqueName)
-> Getting Name NamePair Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name -> Const Name Name) -> UniqueName -> Const Name UniqueName
forall s t. Rewrapping s t => Iso s t (Unwrapped s) (Unwrapped t)
_Wrapped

  varKey :: FortranVar a -> VarKey FortranVar
varKey (FortranVar D a
_ NamePair
np) = NamePair
np NamePair -> Getting UniqueName NamePair UniqueName -> UniqueName
forall s a. s -> Getting a s a -> a
^. Getting UniqueName NamePair UniqueName
Lens' NamePair UniqueName
npUnique

  eqVarTypes :: FortranVar a -> FortranVar b -> Maybe (a :~: b)
eqVarTypes (FortranVar D a
d1 NamePair
_) (FortranVar D b
d2 NamePair
_) = D a -> D b -> Maybe (a :~: b)
forall a b. D a -> D b -> Maybe (a :~: b)
eqD D a
d1 D b
d2

  castVarSym :: FortranVar a -> VarSym FortranVar b -> Maybe (VarSym FortranVar a)
castVarSym (FortranVar D a
d1 NamePair
_) VarSym FortranVar b
s = case VarSym FortranVar b
s of
    CRPrim d2 _  | Just a :~: PrimS a
Refl <- D a -> D (PrimS a) -> Maybe (a :~: PrimS a)
forall a b. D a -> D b -> Maybe (a :~: b)
eqD D a
d1 D (PrimS a)
d2 -> CoreRepr (PrimS a) -> Maybe (CoreRepr (PrimS a))
forall a. a -> Maybe a
Just VarSym FortranVar b
CoreRepr (PrimS a)
s
    CRArray d2 _ | Just a :~: Array i a
Refl <- D a -> D (Array i a) -> Maybe (a :~: Array i a)
forall a b. D a -> D b -> Maybe (a :~: b)
eqD D a
d1 D (Array i a)
d2 -> CoreRepr (Array i a) -> Maybe (CoreRepr (Array i a))
forall a. a -> Maybe a
Just VarSym FortranVar b
CoreRepr (Array i a)
s
    CRData d2 _  | Just a :~: Record name fs
Refl <- D a -> D (Record name fs) -> Maybe (a :~: Record name fs)
forall a b. D a -> D b -> Maybe (a :~: b)
eqD D a
d1 D (Record name fs)
d2 -> CoreRepr (Record name fs) -> Maybe (CoreRepr (Record name fs))
forall a. a -> Maybe a
Just VarSym FortranVar b
CoreRepr (Record name fs)
s

    -- Variables can't have the 'Bool' type so 'CRProp' can't be casted.
    VarSym FortranVar b
_            -> Maybe (VarSym FortranVar a)
forall a. Maybe a
Nothing

instance Pretty1 FortranVar where
  pretty1 :: FortranVar a -> Name
pretty1 (FortranVar D a
_ NamePair
np) = NamePair -> Name
forall a. Pretty a => a -> Name
pretty NamePair
np

--------------------------------------------------------------------------------
--  Internals
--------------------------------------------------------------------------------

arraySymbolic :: (HasPrimReprHandlers r) => Index i -> ArrValue a -> String -> r -> Symbolic (ArrRepr i a)
arraySymbolic :: Index i -> ArrValue a -> Name -> r -> Symbolic (ArrRepr i a)
arraySymbolic ixIndex :: Index i
ixIndex@(Index Prim p 'BTInt a
ixPrim) ArrValue a
valAV Name
nm r
env =
  case ArrValue a
valAV of
    ArrPrim Prim p k a
valPrim -> SArr -> ArrRepr i (PrimS a)
forall k (i :: k) a. SArr -> ArrRepr i (PrimS a)
ARPrim (SArr -> ArrRepr i (PrimS a))
-> SymbolicT IO SArr -> SymbolicT IO (ArrRepr i (PrimS a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Prim p 'BTInt a -> Prim p k a -> Name -> r -> SymbolicT IO SArr
forall r (p1 :: Precision) (k1 :: BasicType) i (p2 :: Precision)
       (k2 :: BasicType) a.
HasPrimReprHandlers r =>
Prim p1 k1 i -> Prim p2 k2 a -> Name -> r -> SymbolicT IO SArr
arraySymbolicPrim Prim p 'BTInt a
ixPrim Prim p k a
valPrim Name
nm r
env
    ArrData SSymbol name
_ Rec (Field ArrValue) fs
valData -> do
      Rec (Field (ArrRepr i)) fs
valReprs <- (forall (x :: (Symbol, *)).
 Field ArrValue x -> SymbolicT IO (Field (ArrRepr i) x))
-> Rec (Field ArrValue) fs
-> SymbolicT IO (Rec (Field (ArrRepr i)) fs)
forall u (h :: * -> *) (f :: u -> *) (g :: u -> *) (rs :: [u]).
Applicative h =>
(forall (x :: u). f x -> h (g x)) -> Rec f rs -> h (Rec g rs)
rtraverse ((forall a. ArrValue a -> SymbolicT IO (ArrRepr (PrimS a) a))
-> Field ArrValue x -> SymbolicT IO (Field (ArrRepr (PrimS a)) x)
forall k (t :: * -> *) (f :: k -> *) (g :: k -> *)
       (nv :: (Symbol, k)).
Functor t =>
(forall (a :: k). f a -> t (g a)) -> Field f nv -> t (Field g nv)
traverseField' (\ArrValue a
av -> Index i -> ArrValue a -> Name -> r -> Symbolic (ArrRepr i a)
forall r i a.
HasPrimReprHandlers r =>
Index i -> ArrValue a -> Name -> r -> Symbolic (ArrRepr i a)
arraySymbolic Index i
ixIndex ArrValue a
av Name
nm r
env)) Rec (Field ArrValue) fs
valData
      ArrRepr i (Record name fs)
-> SymbolicT IO (ArrRepr i (Record name fs))
forall (m :: * -> *) a. Monad m => a -> m a
return (ArrRepr i (Record name fs)
 -> SymbolicT IO (ArrRepr i (Record name fs)))
-> ArrRepr i (Record name fs)
-> SymbolicT IO (ArrRepr i (Record name fs))
forall a b. (a -> b) -> a -> b
$ Rec (Field (ArrRepr i)) fs -> ArrRepr i (Record name fs)
forall k (i :: k) (fs :: [(Symbol, *)]) (name :: Symbol).
Rec (Field (ArrRepr i)) fs -> ArrRepr i (Record name fs)
ARData Rec (Field (ArrRepr i)) fs
valReprs

arraySymbolicPrim :: (HasPrimReprHandlers r) => Prim p1 k1 i -> Prim p2 k2 a -> String -> r -> Symbolic SArr
arraySymbolicPrim :: Prim p1 k1 i -> Prim p2 k2 a -> Name -> r -> SymbolicT IO SArr
arraySymbolicPrim Prim p1 k1 i
ixPrim Prim p2 k2 a
valPrim Name
nm r
env = do
  Kind
k1 <- IO Kind -> SymbolicT IO Kind
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO Kind -> SymbolicT IO Kind)
-> (Kind -> IO Kind) -> Kind -> SymbolicT IO Kind
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kind -> IO Kind
forall (m :: * -> *) a. Monad m => a -> m a
return (Kind -> SymbolicT IO Kind) -> Kind -> SymbolicT IO Kind
forall a b. (a -> b) -> a -> b
$ Prim p1 k1 i -> r -> Kind
forall r (m :: * -> *) (p :: Precision) (k :: BasicType) a.
(MonadReader r m, HasPrimReprHandlers r) =>
Prim p k a -> m Kind
primSBVKind Prim p1 k1 i
ixPrim r
env
  Kind
k2 <- IO Kind -> SymbolicT IO Kind
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO Kind -> SymbolicT IO Kind)
-> (Kind -> IO Kind) -> Kind -> SymbolicT IO Kind
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kind -> IO Kind
forall (m :: * -> *) a. Monad m => a -> m a
return (Kind -> SymbolicT IO Kind) -> Kind -> SymbolicT IO Kind
forall a b. (a -> b) -> a -> b
$ Prim p2 k2 a -> r -> Kind
forall r (m :: * -> *) (p :: Precision) (k :: BasicType) a.
(MonadReader r m, HasPrimReprHandlers r) =>
Prim p k a -> m Kind
primSBVKind Prim p2 k2 a
valPrim r
env
  State
state <- SymbolicT IO State
forall (m :: * -> *). MonadSymbolic m => m State
symbolicEnv
  IO SArr -> SymbolicT IO SArr
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO SArr -> SymbolicT IO SArr) -> IO SArr -> SymbolicT IO SArr
forall a b. (a -> b) -> a -> b
$ State -> (Kind, Kind) -> (Int -> Name) -> Maybe SVal -> IO SArr
newSArr State
state (Kind
k1, Kind
k2) (\Int
i -> Name
nm Name -> ShowS
forall a. [a] -> [a] -> [a]
++ Name
"_" Name -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> Name
forall a. Show a => a -> Name
show Int
i) Maybe SVal
forall a. Maybe a
Nothing