Theory.Text.Parser.Token

Tokenizing infrastructure

Symbols

symbol :: String -> Parser String

Parse a symbol.

symbol_ :: String -> Parser ()

Parse a symbol without returning the parsed string.

dot :: Parser ()

A dot ..

comma :: Parser ()

A comma ,.

colon :: Parser ()

A colon :.

natural :: Parser Integer

Parse an natural.

naturalSubscript :: Parser Integer

Parse a Unicode-subscripted natural number.

Formal comments

formalComment :: Parser (String, String)

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

Identifiers and Variables

identifier :: Parser String

Parse an identifier as a string

indexedIdentifier :: Parser (String, Integer)

Parse an identifier possibly indexed with a number.

freshName :: Parser String

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

pubName :: Parser String

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

sortedLVar :: [LSort] -> Parser LVar

Parse a logical variable with the given sorts allowed.

lvar :: Parser LVar

An arbitrary logical variable.

msgvar :: Parser LVar

Parse a non-node variable.

nodevar :: Parser NodeId

Parse a graph node variable.

Operators

opExp :: Parser ()

The exponentiation operator ^.

opMult :: Parser ()

The multiplication operator *.

opEqual :: Parser ()

The equality operator =.

opLess :: Parser ()

The timepoint comparison operator <.

opAt :: Parser ()

The action-at-timepoint operator @.

opForall :: Parser ()

The logical-forall operator All or ∀.

opExists :: Parser ()

The logical-exists operator Ex or ∃.

opImplies :: Parser ()

The logical-implies operator ==>.

opLEquiv :: Parser ()

The logical-equivalence operator =.

opLAnd :: Parser ()

The logical-and operator & or ∧.

opLOr :: Parser ()

The logical-or operator | or ∨.

opLNot :: Parser ()

The logical not operator not or ¬.

opLFalse :: Parser ()

A logical false, F or ⊥.

opLTrue :: Parser ()

A logical false, T or ⊥.

opRequires :: Parser PremIdx

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

opChain :: Parser ()

The chain operator ~~>.

Pseudo operators

equalSign :: Parser ()

The equal sign =.

opSharp :: Parser ()

The sharp operator #.

opBang :: Parser ()

The bang operator !.

opSlash :: Parser ()

The slash operator /.

opMinus :: Parser ()

The minus operator -.

opPlus :: Parser ()

The multiplication operator *.

opLeftarrow :: Parser ()

The leftarrow operator <--.

opRightarrow :: Parser ()

The rightarrow operator -->.

opLongleftarrow :: Parser ()

The longleftarrow operator <--.

opLongrightarrow :: Parser ()

The longrightarrow operator -->.

Parentheses/quoting

braced :: Parser a -> Parser a

Between braces.

parens :: Parser a -> Parser a

Between parentheses.

angled :: Parser a -> Parser a

Between angular brackets.

brackets :: Parser a -> Parser a

Between brackets.

singleQuoted :: Parser a -> Parser a

Between single quotes.

doubleQuoted :: Parser a -> Parser a

Between double quotes.

List parsing

commaSep :: Parser a -> Parser [a]

A comma separated list of elements.

commaSep1 :: Parser a -> Parser [a]

A comma separated non-empty list of elements.

list :: Parser a -> Parser [a]

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

Basic Parsing

type Parser a = Parsec String MaudeSig a

A parser for a stream of tokens.

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

Run a parser on the contents of a file.

parseString

Arguments

:: FilePath

-> Parser a

-> String

Input string.

-> Either ParseError a

Run a given parser on a given string.