{-# 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 #-}
module Language.Fortran.Model.Vars
(
FortranVar(..)
, 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
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
$c== :: SourceName -> SourceName -> Bool
== :: SourceName -> SourceName -> Bool
$c/= :: SourceName -> SourceName -> Bool
/= :: 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
$ccompare :: SourceName -> SourceName -> Ordering
compare :: SourceName -> SourceName -> Ordering
$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
>= :: SourceName -> SourceName -> Bool
$cmax :: SourceName -> SourceName -> SourceName
max :: SourceName -> SourceName -> SourceName
$cmin :: SourceName -> SourceName -> SourceName
min :: SourceName -> SourceName -> SourceName
Ord)
instance Show SourceName where show :: SourceName -> Name
show = Name -> Name
forall a. Show a => a -> Name
show (Name -> Name) -> (SourceName -> Name) -> SourceName -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SourceName -> Name
getSourceName
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
$c== :: UniqueName -> UniqueName -> Bool
== :: UniqueName -> UniqueName -> Bool
$c/= :: UniqueName -> UniqueName -> Bool
/= :: 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
$ccompare :: UniqueName -> UniqueName -> Ordering
compare :: UniqueName -> UniqueName -> Ordering
$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
>= :: UniqueName -> UniqueName -> Bool
$cmax :: UniqueName -> UniqueName -> UniqueName
max :: UniqueName -> UniqueName -> UniqueName
$cmin :: UniqueName -> UniqueName -> UniqueName
min :: UniqueName -> UniqueName -> UniqueName
Ord)
instance Show UniqueName where show :: UniqueName -> Name
show = Name -> Name
forall a. Show a => a -> Name
show (Name -> Name) -> (UniqueName -> Name) -> UniqueName -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UniqueName -> Name
getUniqueName
makeWrapped ''SourceName
makeWrapped ''UniqueName
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
$c== :: NamePair -> NamePair -> Bool
== :: NamePair -> NamePair -> Bool
$c/= :: NamePair -> NamePair -> Bool
/= :: 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
$ccompare :: NamePair -> NamePair -> Ordering
compare :: NamePair -> NamePair -> Ordering
$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
>= :: NamePair -> NamePair -> Bool
$cmax :: NamePair -> NamePair -> NamePair
max :: NamePair -> NamePair -> NamePair
$cmin :: NamePair -> NamePair -> NamePair
min :: NamePair -> NamePair -> NamePair
Ord, Int -> NamePair -> Name -> Name
[NamePair] -> Name -> Name
NamePair -> Name
(Int -> NamePair -> Name -> Name)
-> (NamePair -> Name)
-> ([NamePair] -> Name -> Name)
-> Show NamePair
forall a.
(Int -> a -> Name -> Name)
-> (a -> Name) -> ([a] -> Name -> Name) -> Show a
$cshowsPrec :: Int -> NamePair -> Name -> Name
showsPrec :: Int -> NamePair -> Name -> Name
$cshow :: NamePair -> Name
show :: NamePair -> Name
$cshowList :: [NamePair] -> Name -> Name
showList :: [NamePair] -> Name -> Name
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
(Unwrapped SourceName -> Const Name (Unwrapped SourceName))
-> SourceName -> Const Name SourceName
forall s t. Rewrapping s t => Iso s t (Unwrapped s) (Unwrapped t)
Iso' SourceName (Unwrapped SourceName)
_Wrapped
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
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 :: forall a.
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 a1
prim -> D (PrimS a1) -> SVal -> CoreRepr (PrimS a1)
forall a1. D (PrimS a1) -> SVal -> CoreRepr (PrimS a1)
CRPrim D a
D (PrimS a1)
d (SVal -> CoreRepr (PrimS a1))
-> SymbolicT IO SVal -> SymbolicT IO (CoreRepr (PrimS a1))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Prim p k a1 -> 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 a1
prim Name
Unwrapped UniqueName
uniqueName VarEnv FortranVar
PrimReprHandlers
env
DArray Index i
i ArrValue a1
val -> D (Array i a1) -> ArrRepr i a1 -> CoreRepr (Array i a1)
forall {k} (i :: k) a1.
D (Array i a1) -> ArrRepr i a1 -> CoreRepr (Array i a1)
CRArray D a
D (Array i a1)
d (ArrRepr i a1 -> CoreRepr (Array i a1))
-> SymbolicT IO (ArrRepr i a1)
-> SymbolicT IO (CoreRepr (Array i a1))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Index i
-> ArrValue a1
-> Name
-> PrimReprHandlers
-> SymbolicT IO (ArrRepr i a1)
forall r i a.
HasPrimReprHandlers r =>
Index i -> ArrValue a -> Name -> r -> Symbolic (ArrRepr i a)
arraySymbolic Index i
i ArrValue a1
val Name
Unwrapped UniqueName
uniqueName VarEnv FortranVar
PrimReprHandlers
env
DData SSymbol name
_ Rec (Field D) fs
_ -> Name -> SymbolicT IO (CoreRepr (Record name fs))
forall a. Name -> SymbolicT IO a
forall (m :: * -> *) a. MonadFail m => Name -> m a
fail Name
"User-defined data type variables are not supported yet"
where
uniqueName :: Unwrapped UniqueName
uniqueName = NamePair
np NamePair
-> Getting (Unwrapped UniqueName) NamePair (Unwrapped UniqueName)
-> Unwrapped UniqueName
forall s a. s -> Getting a s a -> a
^. (UniqueName -> Const (Unwrapped UniqueName) UniqueName)
-> NamePair -> Const (Unwrapped UniqueName) NamePair
Lens' NamePair UniqueName
npUnique ((UniqueName -> Const (Unwrapped UniqueName) UniqueName)
-> NamePair -> Const (Unwrapped UniqueName) NamePair)
-> ((Unwrapped UniqueName
-> Const (Unwrapped UniqueName) (Unwrapped UniqueName))
-> UniqueName -> Const (Unwrapped UniqueName) UniqueName)
-> Getting (Unwrapped UniqueName) NamePair (Unwrapped UniqueName)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Unwrapped UniqueName
-> Const (Unwrapped UniqueName) (Unwrapped UniqueName))
-> UniqueName -> Const (Unwrapped UniqueName) UniqueName
forall s t. Rewrapping s t => Iso s t (Unwrapped s) (Unwrapped t)
Iso' UniqueName (Unwrapped UniqueName)
_Wrapped
varKey :: forall a. 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 :: forall a b. 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 :: forall a b.
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 D (PrimS a1)
d2 SVal
_ | Just a :~: PrimS a1
Refl <- D a -> D (PrimS a1) -> Maybe (a :~: PrimS a1)
forall a b. D a -> D b -> Maybe (a :~: b)
eqD D a
d1 D (PrimS a1)
d2 -> CoreRepr (PrimS a1) -> Maybe (CoreRepr (PrimS a1))
forall a. a -> Maybe a
Just VarSym FortranVar b
CoreRepr (PrimS a1)
s
CRArray D (Array i a1)
d2 ArrRepr i a1
_ | Just a :~: Array i a1
Refl <- D a -> D (Array i a1) -> Maybe (a :~: Array i a1)
forall a b. D a -> D b -> Maybe (a :~: b)
eqD D a
d1 D (Array i a1)
d2 -> CoreRepr (Array i a1) -> Maybe (CoreRepr (Array i a1))
forall a. a -> Maybe a
Just VarSym FortranVar b
CoreRepr (Array i a1)
s
CRData D (Record name fs)
d2 Rec (Field CoreRepr) fs
_ | 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
VarSym FortranVar b
_ -> Maybe (VarSym FortranVar a)
Maybe (CoreRepr a)
forall a. Maybe a
Nothing
instance Pretty1 FortranVar where
pretty1 :: forall a. FortranVar a -> Name
pretty1 (FortranVar D a
_ NamePair
np) = NamePair -> Name
forall a. Pretty a => a -> Name
pretty NamePair
np
arraySymbolic :: (HasPrimReprHandlers r) => Index i -> ArrValue a -> String -> r -> Symbolic (ArrRepr i a)
arraySymbolic :: forall r i a.
HasPrimReprHandlers r =>
Index i -> ArrValue a -> Name -> r -> Symbolic (ArrRepr i a)
arraySymbolic ixIndex :: Index i
ixIndex@(Index Prim p 'BTInt a1
ixPrim) ArrValue a
valAV Name
nm r
env =
case ArrValue a
valAV of
ArrPrim Prim p k a1
valPrim -> SArr -> ArrRepr i a
SArr -> ArrRepr i (PrimS a1)
forall {k} (i :: k) a1. SArr -> ArrRepr i (PrimS a1)
ARPrim (SArr -> ArrRepr i a)
-> SymbolicT IO SArr -> Symbolic (ArrRepr i a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Prim p 'BTInt a1 -> Prim p k a1 -> 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 a1
ixPrim Prim p k a1
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 a1) a))
-> Field ArrValue x -> SymbolicT IO (Field (ArrRepr (PrimS a1)) 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 a -> Symbolic (ArrRepr i a)
forall a. a -> SymbolicT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (ArrRepr i a -> Symbolic (ArrRepr i a))
-> ArrRepr i a -> Symbolic (ArrRepr i a)
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 :: 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 p1 k1 i
ixPrim Prim p2 k2 a
valPrim Name
nm r
env = do
Kind
k1 <- IO Kind -> SymbolicT IO Kind
forall (m :: * -> *) a. Monad m => m a -> SymbolicT m a
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 a. a -> IO a
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 (m :: * -> *) a. Monad m => m a -> SymbolicT m a
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 a. a -> IO a
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 (m :: * -> *) a. Monad m => m a -> SymbolicT m a
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 -> Name -> Name
forall a. [a] -> [a] -> [a]
++ Name
"_" Name -> Name -> Name
forall a. [a] -> [a] -> [a]
++ Int -> Name
forall a. Show a => a -> Name
show Int
i) Maybe SVal
forall a. Maybe a
Nothing