Safe Haskell	None
Language	Haskell2010

Camfort.Specification.Hoare.Parser.Types

Documentation

data HoareParseError Source #

Constructors

UnmatchedQuote
UnexpectedInput
MalformedExpression String
MalformedTypeSpec String
ParseError [Token]
LexError String

Instances

Instances details

Eq HoareParseError Source #
Instance details Defined in Camfort.Specification.Hoare.Parser.Types Methods (==) :: HoareParseError -> HoareParseError -> Bool # (/=) :: HoareParseError -> HoareParseError -> Bool #
Data HoareParseError Source #
Instance details Defined in Camfort.Specification.Hoare.Parser.Types Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> HoareParseError -> c HoareParseError # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c HoareParseError # toConstr :: HoareParseError -> Constr # dataTypeOf :: HoareParseError -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c HoareParseError) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c HoareParseError) # gmapT :: (forall b. Data b => b -> b) -> HoareParseError -> HoareParseError # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> HoareParseError -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> HoareParseError -> r # gmapQ :: (forall d. Data d => d -> u) -> HoareParseError -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> HoareParseError -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> HoareParseError -> m HoareParseError # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> HoareParseError -> m HoareParseError # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> HoareParseError -> m HoareParseError #
Ord HoareParseError Source #
Instance details Defined in Camfort.Specification.Hoare.Parser.Types Methods compare :: HoareParseError -> HoareParseError -> Ordering # (<) :: HoareParseError -> HoareParseError -> Bool # (<=) :: HoareParseError -> HoareParseError -> Bool # (>) :: HoareParseError -> HoareParseError -> Bool # (>=) :: HoareParseError -> HoareParseError -> Bool # max :: HoareParseError -> HoareParseError -> HoareParseError # min :: HoareParseError -> HoareParseError -> HoareParseError #
Show HoareParseError Source #
Instance details Defined in Camfort.Specification.Hoare.Parser.Types Methods showsPrec :: Int -> HoareParseError -> ShowS # show :: HoareParseError -> String # showList :: [HoareParseError] -> ShowS #
Exception HoareParseError Source #
Instance details Defined in Camfort.Specification.Hoare.Parser.Types Methods toException :: HoareParseError -> SomeException # fromException :: SomeException -> Maybe HoareParseError # displayException :: HoareParseError -> String #

prettyTokens :: [Token] -> String Source #

type HoareSpecParser = Either HoareParseError Source #

data Token Source #

Constructors

TQuoted String
TStaticAssert
TPre
TPost
TInvariant
TSeq
TRParen
TLParen
TAnd
TOr
TImpl
TEquiv
TNot
TTrue
TFalse
TDeclAux
TName String
TDColon

Instances

Instances details

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

parseExpression :: String -> HoareSpecParser (Expression ()) Source #

parseTypeSpec :: String -> HoareSpecParser (TypeSpec ()) Source #