| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Camfort.Specification.Hoare.Translate
Description
Translation from annotation syntax defined in Camfort.Specification.Hoare.Syntax to strongly-typed meta-expressions defined in Language.Fortran.Model.Op.Meta.
Synopsis
- type MetaExpr = HFree' AllOps
- type MetaFormula = Prop (MetaExpr FortranVar)
- type AllOps = '[HighOp, MetaOp, CoreOp]
- translateBoolExpression :: (Monad m, MonadFail m) => Expression (Analysis ann) -> TranslateT m (MetaExpr FortranVar Bool)
- translateFormula :: (Monad m, MonadFail m) => PrimFormula (Analysis ann) -> TranslateT m (MetaFormula Bool)
- intoMetaExpr :: (ChooseOp op AllOps, HTraversable op) => HFree op v a -> MetaExpr v a
Meta Expression Types
type MetaFormula = Prop (MetaExpr FortranVar) Source #
Translation
translateBoolExpression :: (Monad m, MonadFail m) => Expression (Analysis ann) -> TranslateT m (MetaExpr FortranVar Bool) Source #
Translate a boolean-valued untyped Fortran expression into a strongly typed MetaExpr.
translateFormula :: (Monad m, MonadFail m) => PrimFormula (Analysis ann) -> TranslateT m (MetaFormula Bool) Source #
Translate an untyped logical formula into a strongly typed MetaFormula.