camfort-1.0.1: CamFort - Cambridge Fortran infrastructure
Safe HaskellNone
LanguageHaskell2010

Language.Fortran.Model.Repr

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

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 ArrReprs 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

LiftD (PrimS Float) AlgReal Source # 
Instance details

Defined in Language.Fortran.Model.Repr

LiftD (PrimS Int8) Integer Source # 
Instance details

Defined in Language.Fortran.Model.Repr

LiftD (PrimS Int16) Integer Source # 
Instance details

Defined in Language.Fortran.Model.Repr

LiftD (PrimS Int32) Integer Source # 
Instance details

Defined in Language.Fortran.Model.Repr

LiftD (PrimS Int64) Integer Source # 
Instance details

Defined in Language.Fortran.Model.Repr

LiftD (PrimS Char8) Word8 Source # 
Instance details

Defined in Language.Fortran.Model.Repr

LiftD (PrimS Bool64) Bool Source # 
Instance details

Defined in Language.Fortran.Model.Repr

LiftD (PrimS Bool32) Bool Source # 
Instance details

Defined in Language.Fortran.Model.Repr

LiftD (PrimS Bool16) Bool Source # 
Instance details

Defined in Language.Fortran.Model.Repr

LiftD (PrimS Bool8) Bool Source # 
Instance details

Defined in Language.Fortran.Model.Repr

Combinators

coreReprD :: CoreRepr a -> D a Source #

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