Safe Haskell	None
Language	Haskell2010

Camfort.Specification.Hoare.Syntax

Contents

Syntax Types
Lenses

Description

Defines the syntax of invariant annotations. See Camfort.Specification.Hoare for a high-level overview.

In this module, the word 'primitive' is used to refer to untyped expression syntax (as opposed to the typed expression syntax defined in Language.Fortran.Model.Op).

Synopsis

data PrimLogic a
- = PLAnd a a
- | PLOr a a
- | PLImpl a a
- | PLEquiv a a
- | PLNot a
- | PLLit Bool
data PrimFormula ann
- = PFExpr (Expression ann)
- | PFLogical (PrimLogic (PrimFormula ann))
data SpecKind
- = SpecPre
- | SpecPost
- | SpecSeq
- | SpecInvariant
data Specification a = Specification {
- _specType :: SpecKind
- _specFormula :: a
}
data AuxDecl ann = AuxDecl {
- _adName :: Name
- _adTy :: TypeSpec ann
}
type PrimSpec ann = Specification (PrimFormula ann)
data SpecOrDecl ann
- = SodSpec (PrimSpec ann)
- | SodDecl (AuxDecl ann)
specType :: forall a. Lens' (Specification a) SpecKind
specFormula :: forall a a. Lens (Specification a) (Specification a) a a
adTy :: forall ann ann. Lens (AuxDecl ann) (AuxDecl ann) (TypeSpec ann) (TypeSpec ann)
adName :: forall ann. Lens' (AuxDecl ann) Name
_Specification :: forall a a. Iso (Specification a) (Specification a) (SpecKind, a) (SpecKind, a)
_SodDecl :: forall ann. Prism' (SpecOrDecl ann) (AuxDecl ann)
_SodSpec :: forall ann. Prism' (SpecOrDecl ann) (PrimSpec ann)
refining :: Eq r => r -> APrism s t (a, r) (a, r) -> Prism s t a a
_SpecPre :: Prism' (Specification a) a
_SpecPost :: Prism' (Specification a) a
_SpecSeq :: Prism' (Specification a) a
_SpecInvariant :: Prism' (Specification a) a

Syntax Types

data PrimLogic a Source #

A type of primitive logical operators.

Constructors

PLAnd a a
PLOr a a
PLImpl a a
PLEquiv a a
PLNot a
PLLit Bool

Instances

Instances details

Functor PrimLogic Source #
Instance details Defined in Camfort.Specification.Hoare.Syntax Methods fmap :: (a -> b) -> PrimLogic a -> PrimLogic b # (<$) :: a -> PrimLogic b -> PrimLogic a #
Foldable PrimLogic Source #
Instance details Defined in Camfort.Specification.Hoare.Syntax Methods fold :: Monoid m => PrimLogic m -> m # foldMap :: Monoid m => (a -> m) -> PrimLogic a -> m # foldMap' :: Monoid m => (a -> m) -> PrimLogic a -> m # foldr :: (a -> b -> b) -> b -> PrimLogic a -> b # foldr' :: (a -> b -> b) -> b -> PrimLogic a -> b # foldl :: (b -> a -> b) -> b -> PrimLogic a -> b # foldl' :: (b -> a -> b) -> b -> PrimLogic a -> b # foldr1 :: (a -> a -> a) -> PrimLogic a -> a # foldl1 :: (a -> a -> a) -> PrimLogic a -> a # toList :: PrimLogic a -> [a] # null :: PrimLogic a -> Bool # length :: PrimLogic a -> Int # elem :: Eq a => a -> PrimLogic a -> Bool # maximum :: Ord a => PrimLogic a -> a # minimum :: Ord a => PrimLogic a -> a # sum :: Num a => PrimLogic a -> a # product :: Num a => PrimLogic a -> a #
Traversable PrimLogic Source #
Instance details Defined in Camfort.Specification.Hoare.Syntax Methods traverse :: Applicative f => (a -> f b) -> PrimLogic a -> f (PrimLogic b) # sequenceA :: Applicative f => PrimLogic (f a) -> f (PrimLogic a) # mapM :: Monad m => (a -> m b) -> PrimLogic a -> m (PrimLogic b) # sequence :: Monad m => PrimLogic (m a) -> m (PrimLogic a) #
Eq a => Eq (PrimLogic a) Source #
Instance details Defined in Camfort.Specification.Hoare.Syntax Methods (==) :: PrimLogic a -> PrimLogic a -> Bool # (/=) :: PrimLogic a -> PrimLogic a -> Bool #
Data a => Data (PrimLogic a) Source #
Instance details Defined in Camfort.Specification.Hoare.Syntax Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> PrimLogic a -> c (PrimLogic a) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (PrimLogic a) # toConstr :: PrimLogic a -> Constr # dataTypeOf :: PrimLogic a -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (PrimLogic a)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (PrimLogic a)) # gmapT :: (forall b. Data b => b -> b) -> PrimLogic a -> PrimLogic a # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PrimLogic a -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PrimLogic a -> r # gmapQ :: (forall d. Data d => d -> u) -> PrimLogic a -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> PrimLogic a -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> PrimLogic a -> m (PrimLogic a) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> PrimLogic a -> m (PrimLogic a) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> PrimLogic a -> m (PrimLogic a) #
Show a => Show (PrimLogic a) Source #
Instance details Defined in Camfort.Specification.Hoare.Syntax Methods showsPrec :: Int -> PrimLogic a -> ShowS # show :: PrimLogic a -> String # showList :: [PrimLogic a] -> ShowS #

data PrimFormula ann Source #

Logical expressions over Fortran expressions.

Constructors

PFExpr (Expression ann)
PFLogical (PrimLogic (PrimFormula ann))

Instances

Instances details

Functor PrimFormula Source #
Instance details Defined in Camfort.Specification.Hoare.Syntax Methods fmap :: (a -> b) -> PrimFormula a -> PrimFormula b # (<$) :: a -> PrimFormula b -> PrimFormula a #
Eq ann => Eq (PrimFormula ann) Source #
Instance details Defined in Camfort.Specification.Hoare.Syntax Methods (==) :: PrimFormula ann -> PrimFormula ann -> Bool # (/=) :: PrimFormula ann -> PrimFormula ann -> Bool #
Data ann => Data (PrimFormula ann) Source #
Instance details Defined in Camfort.Specification.Hoare.Syntax Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> PrimFormula ann -> c (PrimFormula ann) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (PrimFormula ann) # toConstr :: PrimFormula ann -> Constr # dataTypeOf :: PrimFormula ann -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (PrimFormula ann)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (PrimFormula ann)) # gmapT :: (forall b. Data b => b -> b) -> PrimFormula ann -> PrimFormula ann # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PrimFormula ann -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PrimFormula ann -> r # gmapQ :: (forall d. Data d => d -> u) -> PrimFormula ann -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> PrimFormula ann -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> PrimFormula ann -> m (PrimFormula ann) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> PrimFormula ann -> m (PrimFormula ann) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> PrimFormula ann -> m (PrimFormula ann) #
Show ann => Show (PrimFormula ann) Source #
Instance details Defined in Camfort.Specification.Hoare.Syntax Methods showsPrec :: Int -> PrimFormula ann -> ShowS # show :: PrimFormula ann -> String # showList :: [PrimFormula ann] -> ShowS #
Show a => Pretty (PrimFormula a) Source #
Instance details Defined in Camfort.Specification.Hoare.Syntax Methods pretty :: PrimFormula a -> String prettysPrec :: Int -> PrimFormula a -> ShowS

data SpecKind Source #

Labels for the keyword used in static_assert annotations.

Constructors

SpecPre	static_assert pre(...)
SpecPost	static_assert post(...)
SpecSeq	static_assert seq(...)
SpecInvariant	static_assert invariant(...)

Instances

Instances details

Eq SpecKind Source #
Instance details Defined in Camfort.Specification.Hoare.Syntax Methods (==) :: SpecKind -> SpecKind -> Bool # (/=) :: SpecKind -> SpecKind -> Bool #
Data SpecKind Source #
Instance details Defined in Camfort.Specification.Hoare.Syntax Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SpecKind -> c SpecKind # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SpecKind # toConstr :: SpecKind -> Constr # dataTypeOf :: SpecKind -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SpecKind) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SpecKind) # gmapT :: (forall b. Data b => b -> b) -> SpecKind -> SpecKind # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SpecKind -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SpecKind -> r # gmapQ :: (forall d. Data d => d -> u) -> SpecKind -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> SpecKind -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> SpecKind -> m SpecKind # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SpecKind -> m SpecKind # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SpecKind -> m SpecKind #
Show SpecKind Source #
Instance details Defined in Camfort.Specification.Hoare.Syntax Methods showsPrec :: Int -> SpecKind -> ShowS # show :: SpecKind -> String # showList :: [SpecKind] -> ShowS #

data Specification a Source #

A static_assert annotation.

Constructors

Specification
Fields _specType :: SpecKind _specFormula :: a

Instances

Instances details

Functor Specification Source #
Instance details Defined in Camfort.Specification.Hoare.Syntax Methods fmap :: (a -> b) -> Specification a -> Specification b # (<$) :: a -> Specification b -> Specification a #
Eq a => Eq (Specification a) Source #
Instance details Defined in Camfort.Specification.Hoare.Syntax Methods (==) :: Specification a -> Specification a -> Bool # (/=) :: Specification a -> Specification a -> Bool #
Data a => Data (Specification a) Source #
Instance details Defined in Camfort.Specification.Hoare.Syntax Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Specification a -> c (Specification a) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Specification a) # toConstr :: Specification a -> Constr # dataTypeOf :: Specification a -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Specification a)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Specification a)) # gmapT :: (forall b. Data b => b -> b) -> Specification a -> Specification a # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Specification a -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Specification a -> r # gmapQ :: (forall d. Data d => d -> u) -> Specification a -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Specification a -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Specification a -> m (Specification a) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Specification a -> m (Specification a) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Specification a -> m (Specification a) #
Pretty a => Show (Specification a) Source #
Instance details Defined in Camfort.Specification.Hoare.Syntax Methods showsPrec :: Int -> Specification a -> ShowS # show :: Specification a -> String # showList :: [Specification a] -> ShowS #

data AuxDecl ann Source #

A decl_aux annotation.

Constructors

AuxDecl
Fields _adName :: Name _adTy :: TypeSpec ann

Instances

Instances details

Functor AuxDecl Source #
Instance details Defined in Camfort.Specification.Hoare.Syntax Methods fmap :: (a -> b) -> AuxDecl a -> AuxDecl b # (<$) :: a -> AuxDecl b -> AuxDecl a #
Eq ann => Eq (AuxDecl ann) Source #
Instance details Defined in Camfort.Specification.Hoare.Syntax Methods (==) :: AuxDecl ann -> AuxDecl ann -> Bool # (/=) :: AuxDecl ann -> AuxDecl ann -> Bool #
Data ann => Data (AuxDecl ann) Source #
Instance details Defined in Camfort.Specification.Hoare.Syntax Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> AuxDecl ann -> c (AuxDecl ann) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (AuxDecl ann) # toConstr :: AuxDecl ann -> Constr # dataTypeOf :: AuxDecl ann -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (AuxDecl ann)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (AuxDecl ann)) # gmapT :: (forall b. Data b => b -> b) -> AuxDecl ann -> AuxDecl ann # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> AuxDecl ann -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> AuxDecl ann -> r # gmapQ :: (forall d. Data d => d -> u) -> AuxDecl ann -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> AuxDecl ann -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> AuxDecl ann -> m (AuxDecl ann) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> AuxDecl ann -> m (AuxDecl ann) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> AuxDecl ann -> m (AuxDecl ann) #
Show ann => Show (AuxDecl ann) Source #
Instance details Defined in Camfort.Specification.Hoare.Syntax Methods showsPrec :: Int -> AuxDecl ann -> ShowS # show :: AuxDecl ann -> String # showList :: [AuxDecl ann] -> ShowS #

type PrimSpec ann = Specification (PrimFormula ann) Source #

A specification over untyped logical expressions.

data SpecOrDecl ann Source #

A static_assert or decl_aux annotation.

Constructors

SodSpec (PrimSpec ann)
SodDecl (AuxDecl ann)

Instances

Instances details

Functor SpecOrDecl Source #
Instance details Defined in Camfort.Specification.Hoare.Syntax Methods fmap :: (a -> b) -> SpecOrDecl a -> SpecOrDecl b # (<$) :: a -> SpecOrDecl b -> SpecOrDecl a #
ASTEmbeddable HA (SpecOrDecl InnerHA) Source #
Instance details Defined in Camfort.Specification.Hoare.Annotation Methods annotateWithAST :: HA -> SpecOrDecl InnerHA -> HA Source #
Eq ann => Eq (SpecOrDecl ann) Source #
Instance details Defined in Camfort.Specification.Hoare.Syntax Methods (==) :: SpecOrDecl ann -> SpecOrDecl ann -> Bool # (/=) :: SpecOrDecl ann -> SpecOrDecl ann -> Bool #
Data ann => Data (SpecOrDecl ann) Source #
Instance details Defined in Camfort.Specification.Hoare.Syntax Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SpecOrDecl ann -> c (SpecOrDecl ann) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (SpecOrDecl ann) # toConstr :: SpecOrDecl ann -> Constr # dataTypeOf :: SpecOrDecl ann -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (SpecOrDecl ann)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (SpecOrDecl ann)) # gmapT :: (forall b. Data b => b -> b) -> SpecOrDecl ann -> SpecOrDecl ann # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SpecOrDecl ann -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SpecOrDecl ann -> r # gmapQ :: (forall d. Data d => d -> u) -> SpecOrDecl ann -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> SpecOrDecl ann -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> SpecOrDecl ann -> m (SpecOrDecl ann) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SpecOrDecl ann -> m (SpecOrDecl ann) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SpecOrDecl ann -> m (SpecOrDecl ann) #
Show ann => Show (SpecOrDecl ann) Source #
Instance details Defined in Camfort.Specification.Hoare.Syntax Methods showsPrec :: Int -> SpecOrDecl ann -> ShowS # show :: SpecOrDecl ann -> String # showList :: [SpecOrDecl ann] -> ShowS #

Lenses

specType :: forall a. Lens' (Specification a) SpecKind Source #

specFormula :: forall a a. Lens (Specification a) (Specification a) a a Source #

adTy :: forall ann ann. Lens (AuxDecl ann) (AuxDecl ann) (TypeSpec ann) (TypeSpec ann) Source #

adName :: forall ann. Lens' (AuxDecl ann) Name Source #

_Specification :: forall a a. Iso (Specification a) (Specification a) (SpecKind, a) (SpecKind, a) Source #

_SodDecl :: forall ann. Prism' (SpecOrDecl ann) (AuxDecl ann) Source #

_SodSpec :: forall ann. Prism' (SpecOrDecl ann) (PrimSpec ann) Source #

refining :: Eq r => r -> APrism s t (a, r) (a, r) -> Prism s t a a Source #

Given a prism p projecting a pair, refining x p projects values from the front left of the pair such that the right of the pair matches x.

>>> [1, 2, 3] ^? refining [] _Cons
Nothing

>>> [1] ^? refining [] _Cons
Just 1

_SpecPre :: Prism' (Specification a) a Source #

Match a static_assert pre(...) annotation.

_SpecPost :: Prism' (Specification a) a Source #

Match a static_assert post(...) annotation.

_SpecSeq :: Prism' (Specification a) a Source #

Match a static_assert seq(...) annotation.

_SpecInvariant :: Prism' (Specification a) a Source #

Match a static_assert invariant(...) annotation.