Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
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
exists; i.e. anything with a corresponding Fortran type. D
aHighRepr
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
- data ArrRepr i a where
- data HighRepr a where
- 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.
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) CoreOp Source # | |
MonadEvalFortran r m => HFoldableAt (Compose m CoreRepr :: Type -> Type) MetaOp Source # | |
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.
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).
Instances
HFoldableAt HighRepr LogicOp Source # | |
MonadEvalFortran r m => HFoldableAt (Compose m HighRepr :: Type -> Type) CoreOp Source # | |
(MonadReader r m, HasPrimReprHandlers r) => HFoldableAt (Compose m HighRepr :: Type -> Type) HighOp Source # | |
(MonadReader r m, HasPrimReprHandlers r) => HFoldableAt (Compose m HighRepr :: Type -> Type) LiftDOp Source # | |
MonadEvalFortran r m => HFoldableAt (Compose m HighRepr :: Type -> Type) MetaOp Source # | |
Monad m => HFoldableAt (Compose m HighRepr :: Type -> Type) LogicOp Source # | |
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.
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
LiftD (PrimS Int16) Integer Source # | |
LiftD (PrimS Int32) Integer Source # | |
LiftD (PrimS Int64) Integer Source # | |
LiftD (PrimS Int8) Integer Source # | |
LiftD (PrimS Bool16) Bool Source # | |
LiftD (PrimS Bool32) Bool Source # | |
LiftD (PrimS Bool64) Bool Source # | |
LiftD (PrimS Bool8) Bool Source # | |
LiftD (PrimS Char8) Word8 Source # | |
LiftD (PrimS Double) AlgReal Source # | |
LiftD (PrimS Float) AlgReal Source # | |