Safe Haskell	None
Language	Haskell2010

Language.Fortran.Model.Repr

Contents

Core Fortran Representations
High-level data representations
Lifting Fortran types to high-level representations
Combinators

Description

Symbolic representations of Fortran values, for symbolic reasoning.

There is a distinction between core representations (CoreRepr) and high-level representations (HighRepr). CoreRepr represents any a such that D a exists; i.e. anything with a corresponding Fortran type. HighRepr is a superset of CoreRepr. It represents Fortran types, and also higher-level types that facilitate reasoning. There is more information about this distinction in Language.Fortran.Model.Op.

Synopsis

data CoreRepr a where
- CRPrim :: D (PrimS a) -> SVal -> CoreRepr (PrimS a)
- CRArray :: D (Array i a) -> ArrRepr i a -> CoreRepr (Array i a)
- CRData :: D (Record name fs) -> Rec (Field CoreRepr) fs -> CoreRepr (Record name fs)
data ArrRepr i a where
- ARPrim :: SArr -> ArrRepr i (PrimS a)
- ARData :: Rec (Field (ArrRepr i)) fs -> ArrRepr i (Record name fs)
data HighRepr a where
- HRCore :: CoreRepr a -> HighRepr a
- HRHigh :: SBV a -> HighRepr a
class SymVal a => LiftD b a | b -> a where
- liftD :: b -> a
- liftDRepr :: PrimReprHandlers -> HighRepr b -> HighRepr a
liftDInt :: PrimReprHandlers -> HighRepr (PrimS a) -> HighRepr Integer
liftDReal :: PrimReprHandlers -> HighRepr (PrimS a) -> HighRepr AlgReal
liftDBool :: PrimReprHandlers -> HighRepr (PrimS a) -> HighRepr Bool
coreReprD :: CoreRepr a -> D a

Core Fortran Representations

data CoreRepr a where Source #

Symbolic representations of Fortran values, using Data.SBV.Dynamic.

Constructors

CRPrim :: D (PrimS a) -> SVal -> CoreRepr (PrimS a)
CRArray :: D (Array i a) -> ArrRepr i a -> CoreRepr (Array i a)
CRData :: D (Record name fs) -> Rec (Field CoreRepr) fs -> CoreRepr (Record name fs)

Instances

Instances details

MonadEvalFortran r m => HFoldableAt (Compose m CoreRepr :: Type -> Type) MetaOp
Instance details Defined in Language.Fortran.Model.Op.Meta Methods hfoldMap :: forall t (a :: k). (forall (b :: k). t b -> Compose m CoreRepr b) -> MetaOp t a -> Compose m CoreRepr a
MonadEvalFortran r m => HFoldableAt (Compose m CoreRepr :: Type -> Type) CoreOp
Instance details Defined in Language.Fortran.Model.Op.Core Methods hfoldMap :: forall t (a :: k). (forall (b :: k). t b -> Compose m CoreRepr b) -> CoreOp t a -> Compose m CoreRepr a

data ArrRepr i a where Source #

Symbolic respresentations of Fortran arrays. SBV arrays can only contain basic values, so in order to represent arrays of derived data types, we use multiple flat arrays, one for each basic field. Nested derived data types are recursively expanded.

Arrays of arrays are not yet supported.

Constructors

ARPrim :: SArr -> ArrRepr i (PrimS a)	A primitive type is represented by a flat `SArr`.
ARData :: Rec (Field (ArrRepr i)) fs -> ArrRepr i (Record name fs)	A derived data type is represented by a record of `ArrRepr`s over the record's fields.

High-level data representations

data HighRepr a where Source #

Symbolic representations of Fortran values plus types in the higher-level meta-language (see Language.Fortran.Op for more information).

Constructors

HRCore :: CoreRepr a -> HighRepr a
HRHigh :: SBV a -> HighRepr a

Instances

Instances details

HFoldableAt HighRepr LogicOp Source #
Instance details Defined in Language.Fortran.Model.Repr Methods hfoldMap :: forall t (a :: k). (forall (b :: k). t b -> HighRepr b) -> LogicOp t a -> HighRepr a
Monad m => HFoldableAt (Compose m HighRepr :: Type -> Type) LogicOp Source #
Instance details Defined in Language.Fortran.Model.Repr Methods hfoldMap :: forall t (a :: k). (forall (b :: k). t b -> Compose m HighRepr b) -> LogicOp t a -> Compose m HighRepr a
(MonadReader r m, HasPrimReprHandlers r) => HFoldableAt (Compose m HighRepr :: Type -> Type) LiftDOp
Instance details Defined in Language.Fortran.Model.Op.High Methods hfoldMap :: forall t (a :: k). (forall (b :: k). t b -> Compose m HighRepr b) -> LiftDOp t a -> Compose m HighRepr a
(MonadReader r m, HasPrimReprHandlers r) => HFoldableAt (Compose m HighRepr :: Type -> Type) HighOp
Instance details Defined in Language.Fortran.Model.Op.High Methods hfoldMap :: forall t (a :: k). (forall (b :: k). t b -> Compose m HighRepr b) -> HighOp t a -> Compose m HighRepr a
MonadEvalFortran r m => HFoldableAt (Compose m HighRepr :: Type -> Type) MetaOp
Instance details Defined in Language.Fortran.Model.Op.Meta Methods hfoldMap :: forall t (a :: k). (forall (b :: k). t b -> Compose m HighRepr b) -> MetaOp t a -> Compose m HighRepr a
MonadEvalFortran r m => HFoldableAt (Compose m HighRepr :: Type -> Type) CoreOp
Instance details Defined in Language.Fortran.Model.Op.Core Methods hfoldMap :: forall t (a :: k). (forall (b :: k). t b -> Compose m HighRepr b) -> CoreOp t a -> Compose m HighRepr a

Lifting Fortran types to high-level representations

class SymVal a => LiftD b a | b -> a where Source #

Provides conversions between symbolic representations of core Fortran values and their corresponding high-level types.

Methods

liftD :: b -> a Source #

Go from a core value to the corresponding high-level value.

liftDRepr :: PrimReprHandlers -> HighRepr b -> HighRepr a Source #

Go from a symbolic core value to the corresponding symbolic high-level value.

Instances

Instances details

LiftD (PrimS Double) AlgReal Source #
Instance details Defined in Language.Fortran.Model.Repr Methods liftD :: PrimS Double -> AlgReal Source # liftDRepr :: PrimReprHandlers -> HighRepr (PrimS Double) -> HighRepr AlgReal Source #
LiftD (PrimS Float) AlgReal Source #
Instance details Defined in Language.Fortran.Model.Repr Methods liftD :: PrimS Float -> AlgReal Source # liftDRepr :: PrimReprHandlers -> HighRepr (PrimS Float) -> HighRepr AlgReal Source #
LiftD (PrimS Int8) Integer Source #
Instance details Defined in Language.Fortran.Model.Repr Methods liftD :: PrimS Int8 -> Integer Source # liftDRepr :: PrimReprHandlers -> HighRepr (PrimS Int8) -> HighRepr Integer Source #
LiftD (PrimS Int16) Integer Source #
Instance details Defined in Language.Fortran.Model.Repr Methods liftD :: PrimS Int16 -> Integer Source # liftDRepr :: PrimReprHandlers -> HighRepr (PrimS Int16) -> HighRepr Integer Source #
LiftD (PrimS Int32) Integer Source #
Instance details Defined in Language.Fortran.Model.Repr Methods liftD :: PrimS Int32 -> Integer Source # liftDRepr :: PrimReprHandlers -> HighRepr (PrimS Int32) -> HighRepr Integer Source #
LiftD (PrimS Int64) Integer Source #
Instance details Defined in Language.Fortran.Model.Repr Methods liftD :: PrimS Int64 -> Integer Source # liftDRepr :: PrimReprHandlers -> HighRepr (PrimS Int64) -> HighRepr Integer Source #
LiftD (PrimS Char8) Word8 Source #
Instance details Defined in Language.Fortran.Model.Repr Methods liftD :: PrimS Char8 -> Word8 Source # liftDRepr :: PrimReprHandlers -> HighRepr (PrimS Char8) -> HighRepr Word8 Source #
LiftD (PrimS Bool64) Bool Source #
Instance details Defined in Language.Fortran.Model.Repr Methods liftD :: PrimS Bool64 -> Bool Source # liftDRepr :: PrimReprHandlers -> HighRepr (PrimS Bool64) -> HighRepr Bool Source #
LiftD (PrimS Bool32) Bool Source #
Instance details Defined in Language.Fortran.Model.Repr Methods liftD :: PrimS Bool32 -> Bool Source # liftDRepr :: PrimReprHandlers -> HighRepr (PrimS Bool32) -> HighRepr Bool Source #
LiftD (PrimS Bool16) Bool Source #
Instance details Defined in Language.Fortran.Model.Repr Methods liftD :: PrimS Bool16 -> Bool Source # liftDRepr :: PrimReprHandlers -> HighRepr (PrimS Bool16) -> HighRepr Bool Source #
LiftD (PrimS Bool8) Bool Source #
Instance details Defined in Language.Fortran.Model.Repr Methods liftD :: PrimS Bool8 -> Bool Source # liftDRepr :: PrimReprHandlers -> HighRepr (PrimS Bool8) -> HighRepr Bool Source #

liftDInt :: PrimReprHandlers -> HighRepr (PrimS a) -> HighRepr Integer Source #

liftDReal :: PrimReprHandlers -> HighRepr (PrimS a) -> HighRepr AlgReal Source #

liftDBool :: PrimReprHandlers -> HighRepr (PrimS a) -> HighRepr Bool Source #

Combinators

coreReprD :: CoreRepr a -> D a Source #

Any type that has a core representation has a corresponding Fortran type.