Logic.Judge.Formula.Parser

Attoparsec-based parser for various logical (sub)structures.

Parser typeclass

class Parseable a where

A Parseable is something with an associated Attoparsec Parser.

Minimal complete definition

parser

Methods

parser :: Parser a

A parser for type a.

parserEmbedded :: Parser a

In some cases, the parser for a type must be embellished with some other symbols when it occurs as part of a parser of a different type, but not when it occurs on its own. This parser allows us to specify this alternative.

Instances

Parseable Justification

Methods

parser :: Parser Justification

parserEmbedded :: Parser Justification

Parseable Modality

Methods

parser :: Parser Modality

parserEmbedded :: Parser Modality

Parseable Quantifier

Methods

parser :: Parser Quantifier

parserEmbedded :: Parser Quantifier

Parseable Classical

Methods

parser :: Parser Classical

parserEmbedded :: Parser Classical

Parseable f => Parseable [f]

Methods

parser :: Parser [f]

parserEmbedded :: Parser [f]

Parseable e => Parseable (Ambiguous (Term e))

Methods

parser :: Parser (Ambiguous (Term e))

parserEmbedded :: Parser (Ambiguous (Term e))

Parseable f => Parseable (Marked f)

Methods

parser :: Parser (Marked f)

parserEmbedded :: Parser (Marked f)

Parseable e => Parseable (Formula e)

Methods

parser :: Parser (Formula e)

parserEmbedded :: Parser (Formula e)

parse :: (Monad m, Parseable a) => Text -> m a

Read a text into a parseable structure.

Formula parsers

formula :: Parser ext -> Parser (Formula ext)

Builds a parser for formulas of classical propositional logic extended with some type e.

modality :: Parser Modality

Parser for modal operators of modal logic.

justification :: Parser Justification

Parser for justification terms of justification logic.

quantifier :: Parser Quantifier

Parser for quantifiers of first-order predicate logic.

Auxiliary parsers

named :: Parser x -> Parser (String, x)

Make a parser for something that is named by prepending it with an identifier and a = sign.

marked :: Parser formula -> Parser (Marked formula)

Parser for a marked formula.

identifier :: Parser String

Parser that accepts and returns any string that starts with a letter.

boolean :: Parser Bool

Parser that accepts a boolean (as binary number or unicode ⊥, ⊤).

comments :: Parser ()

Parser for comments.

Generic parser building

data Operator a

Operators wrap a parser for a function in additional information. Note that the function they wrap must take arguments of the same type.

expression :: [[Operator a]] -> Parser a -> Parser a

Build a parser for a recursive expression with prefix-, infix- and postfix operators. Note: To avoid ambiguous left/right associative operators, don't put multiple operators of different associative direction into one precedence bucket.

ambiguity :: [Parser a] -> Parser [a]

Given a number of parsers that introduce an ambiguity (e.g. parsers that may succeed on precisely the same text), collects the results of all successful parses, provided that at least one succceeds.