Scyther.Theory.Parser

Lexing

type Token = (SourcePos, Keyword)

The tokens delivered by our Alex based scanner

data Keyword

Lexable Keywords

Constructors

IDENT String

SQUOTE

DQUOTE

RIGHTARROW

LEFTARROW

LONGRIGHTARROW

LONGLEFTARROW

COMMA

DOT

COLON

QUESTIONMARK

AND

MID

DOLLAR

SHARP

LPAREN

RPAREN

LBRACKET

RBRACKET

LBRACE

RBRACE

TILDE

HAT

STAR

UNDERSCORE

MINUS

PLUS

EQUAL

LESS

GREATER

EOF

FORALL

EXISTS

LAND

LOR

LNOT

APPROX

DUMMY_KEYWORD

Instances

Eq Keyword

Show Keyword

scanString :: FilePath -> String -> [Token]

Scan a string using the given filename in the error messages.

NOTE: Lexical errors are thrown using error.

scanFile :: FilePath -> IO [Token]

Scan a file

Parsing

type Parser s a = Parsec [Token] s a

A parser with an arbitrary user state for a stream of tokens.

parseFile :: Parser s a -> s -> FilePath -> IO a

Parser s a theory file.

Additional combinators

liftMaybe :: MonadPlus m => Maybe a -> m a

Lift a maybe to a monad plus action.

liftMaybe' :: Monad m => String -> Maybe a -> m a

Lift a maybe to a monad action with the given failure message.

token :: (Keyword -> Maybe a) -> Parser s a

Parse a token based on the acceptance condition

Keyword combinations

kw :: Keyword -> Parser s ()

Parse a term.

betweenKWs :: Keyword -> Keyword -> Parser s a -> Parser s a

Parse content between keywords.

commaSep :: Parser s a -> Parser s [a]

A comma separated list of elements.

commaSep1 :: Parser s a -> Parser s [a]

A comma separated non-empty list of elements.

list :: Parser s a -> Parser s [a]

Parse a list of items '[' item ',' ... ',' item ']'

braced :: Parser s a -> Parser s a

Between braces.

parens :: Parser s a -> Parser s a

Between parentheses.

brackets :: Parser s a -> Parser s a

Between parentheses.

singleQuoted :: Parser s a -> Parser s a

Between single quotes.

doubleQuoted :: Parser s a -> Parser s a

Between double quotes.

identifier :: Parser s String

Parse an identifier as a string

string :: String -> Parser s ()

Parse a fixed string which could be an identifier.

strings :: [String] -> Parser s ()

Parse a sequence of fixed strings.

integer :: Parser s Int

Parse an integer.

genFunOpen :: Parser s a -> Parser s b -> Parser s a

Left-hand-side of a function application written with the given delimiter.

genFunApp :: Parser s a -> Parser s b -> Parser s d -> Parser s c -> Parser s c

Left-hand-side of a function application.

funOpen :: String -> Parser s ()

Left-hand-side of a function application.

funApp :: String -> Parser s a -> Parser s a

A function application.

Security protocol theorys for the free-algebra

protocol :: Parser s Protocol

Parse a protocol.

claims :: (String -> Maybe Protocol) -> Parser s [ThyItem]

Parse a claim.

theory :: Parser s Theory

Parse a theory.

parseTheory :: FilePath -> IO Theory

Parse a security protocol theory given as a string using the given filename for the error messages

Extended patterns

mkLTSPat :: Pattern -> Pattern

mkMultIdentityPat :: Pattern

mkExpPat :: Pattern -> Pattern -> Pattern

mkMultPat :: Pattern -> Pattern -> Pattern

destLTSPat :: Pattern -> Maybe Pattern

destMultIdentityPat :: Pattern -> Maybe ()

destExpPat :: Pattern -> Maybe (Pattern, Pattern)

destMultPat :: Pattern -> Maybe (Pattern, Pattern)