tamarin-prover-theory- Term manipulation library for the tamarin prover.

MaintainerSimon Meier <iridcode@gmail.com>
Safe HaskellNone




Tokenizing infrastructure



symbol :: String -> Parser StringSource

Parse a symbol.

symbol_ :: String -> Parser ()Source

Parse a symbol without returning the parsed string.

dot :: Parser ()Source

A dot ..

comma :: Parser ()Source

A comma ,.

colon :: Parser ()Source

A colon :.

natural :: Parser IntegerSource

Parse an natural.

naturalSubscript :: Parser IntegerSource

Parse a Unicode-subscripted natural number.

Formal comments

formalComment :: Parser (String, String)Source

A formal comment; i.e., (header, body)

Identifiers and Variables

identifier :: Parser StringSource

Parse an identifier as a string

indexedIdentifier :: Parser (String, Integer)Source

Parse an identifier possibly indexed with a number.

freshName :: Parser StringSource

Parse a literal fresh name, e.g., ~n.

pubName :: Parser StringSource

Parse a literal public name, e.g., n.

sortedLVar :: [LSort] -> Parser LVarSource

Parse a logical variable with the given sorts allowed.

lvar :: Parser LVarSource

An arbitrary logical variable.

msgvar :: Parser LVarSource

Parse a non-node variable.

nodevar :: Parser NodeIdSource

Parse a graph node variable.


opExp :: Parser ()Source

The exponentiation operator ^.

opMult :: Parser ()Source

The multiplication operator *.

opEqual :: Parser ()Source

The equality operator =.

opLess :: Parser ()Source

The timepoint comparison operator <.

opAt :: Parser ()Source

The action-at-timepoint operator @.

opForall :: Parser ()Source

The logical-forall operator All or .

opExists :: Parser ()Source

The logical-exists operator Ex or .

opImplies :: Parser ()Source

The logical-implies operator ==>.

opLEquiv :: Parser ()Source

The logical-equivalence operator =.

opLAnd :: Parser ()Source

The logical-and operator & or .

opLOr :: Parser ()Source

The logical-or operator | or .

opLNot :: Parser ()Source

The logical not operator not or ¬.

opLFalse :: Parser ()Source

A logical false, F or .

opLTrue :: Parser ()Source

A logical false, T or .

opRequires :: Parser PremIdxSource

The requires-a-premise operator, ▶ subscript-idx.

opChain :: Parser ()Source

The chain operator ~~>.

Pseudo operators

equalSign :: Parser ()Source

The equal sign =.

opSharp :: Parser ()Source

The sharp operator #.

opBang :: Parser ()Source

The bang operator !.

opSlash :: Parser ()Source

The slash operator /.

opMinus :: Parser ()Source

The minus operator -.

opPlus :: Parser ()Source

The multiplication operator *.

opLeftarrow :: Parser ()Source

The leftarrow operator <--.

opRightarrow :: Parser ()Source

The rightarrow operator -->.

opLongleftarrow :: Parser ()Source

The longleftarrow operator <--.

opLongrightarrow :: Parser ()Source

The longrightarrow operator -->.


braced :: Parser a -> Parser aSource

Between braces.

parens :: Parser a -> Parser aSource

Between parentheses.

angled :: Parser a -> Parser aSource

Between angular brackets.

brackets :: Parser a -> Parser aSource

Between brackets.

singleQuoted :: Parser a -> Parser aSource

Between single quotes.

doubleQuoted :: Parser a -> Parser aSource

Between double quotes.

List parsing

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

A comma separated list of elements.

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

A comma separated non-empty list of elements.

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

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

Basic Parsing

type Parser a = Parsec String MaudeSig aSource

A parser for a stream of tokens.

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

Run a parser on the contents of a file.



:: FilePath 
-> Parser a 
-> String

Input string.

-> Either ParseError a 

Run a given parser on a given string.