Language.Fortran.Model.Repr

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.

Core Fortran Representations

data CoreRepr a where

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

MonadEvalFortran r m => HFoldableAt (Compose m CoreRepr :: Type -> Type) MetaOp

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

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

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 ArrReprs over the record's fields.

High-level data representations

data HighRepr a where

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

HFoldableAt HighRepr LogicOp

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

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

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

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

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

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

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

Methods

liftD :: b -> a

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

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

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

Instances

LiftD (PrimS Double) AlgReal

Defined in Language.Fortran.Model.Repr

Methods

liftD :: PrimS Double -> AlgReal

liftDRepr :: PrimReprHandlers -> HighRepr (PrimS Double) -> HighRepr AlgReal

LiftD (PrimS Float) AlgReal

Defined in Language.Fortran.Model.Repr

Methods

liftD :: PrimS Float -> AlgReal

liftDRepr :: PrimReprHandlers -> HighRepr (PrimS Float) -> HighRepr AlgReal

LiftD (PrimS Int8) Integer

Defined in Language.Fortran.Model.Repr

Methods

liftD :: PrimS Int8 -> Integer

liftDRepr :: PrimReprHandlers -> HighRepr (PrimS Int8) -> HighRepr Integer

LiftD (PrimS Int16) Integer

Defined in Language.Fortran.Model.Repr

Methods

liftD :: PrimS Int16 -> Integer

liftDRepr :: PrimReprHandlers -> HighRepr (PrimS Int16) -> HighRepr Integer

LiftD (PrimS Int32) Integer

Defined in Language.Fortran.Model.Repr

Methods

liftD :: PrimS Int32 -> Integer

liftDRepr :: PrimReprHandlers -> HighRepr (PrimS Int32) -> HighRepr Integer

LiftD (PrimS Int64) Integer

Defined in Language.Fortran.Model.Repr

Methods

liftD :: PrimS Int64 -> Integer

liftDRepr :: PrimReprHandlers -> HighRepr (PrimS Int64) -> HighRepr Integer

LiftD (PrimS Char8) Word8

Defined in Language.Fortran.Model.Repr

Methods

liftD :: PrimS Char8 -> Word8

liftDRepr :: PrimReprHandlers -> HighRepr (PrimS Char8) -> HighRepr Word8

LiftD (PrimS Bool64) Bool

Defined in Language.Fortran.Model.Repr

Methods

liftD :: PrimS Bool64 -> Bool

liftDRepr :: PrimReprHandlers -> HighRepr (PrimS Bool64) -> HighRepr Bool

LiftD (PrimS Bool32) Bool

Defined in Language.Fortran.Model.Repr

Methods

liftD :: PrimS Bool32 -> Bool

liftDRepr :: PrimReprHandlers -> HighRepr (PrimS Bool32) -> HighRepr Bool

LiftD (PrimS Bool16) Bool

Defined in Language.Fortran.Model.Repr

Methods

liftD :: PrimS Bool16 -> Bool

liftDRepr :: PrimReprHandlers -> HighRepr (PrimS Bool16) -> HighRepr Bool

LiftD (PrimS Bool8) Bool

Defined in Language.Fortran.Model.Repr

Methods

liftD :: PrimS Bool8 -> Bool

liftDRepr :: PrimReprHandlers -> HighRepr (PrimS Bool8) -> HighRepr Bool

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

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

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

Combinators

coreReprD :: CoreRepr a -> D a

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