Copyright	(c) Artem Mavrin 2021
License	BSD3
Maintainer	artemvmavrin@gmail.com
Stability	experimental
Portability	POSIX
Safe Haskell	Safe
Language	Haskell2010

AutoProof.Internal.Parser

Contents

Safe parsing
Unsafe parsing

Description

Parser for propositional logic formulas

Synopsis

parseFormula :: String -> Maybe (Formula String)
parseJudgement :: String -> Maybe (Judgement String)
unsafeParseFormula :: String -> Formula String
unsafeParseJudgement :: String -> Judgement String

Safe parsing

parseFormula :: String -> Maybe (Formula String) Source #

(parseFormula s) parses a string s as a propositional formula, returning a Just a on success, where a is the parsed formula.

For a version of parseFormula that does not return a wrapped formula but also throws an error when it cannot parse, see unsafeParseFormula.

Conventions

Expand

Supported connective symbols:
- Negation: "~", "¬".
- Implication: "->", "=>", "→", "⇾", "⇒" "⊃".
- Disjunction: "|", "\/", "∨", "+"
- Conjunction: "&", "/\", "∧", "^", "*"
- Equivalence: "<->", "↔", "⇿", "⇔"
Implication is right-associative and has lower precedence than the other connectives.
Equivalence is left-associative and has higher precedence than implication but lower precedence than conjunction and disjunction.
Disjunction is left-associative and has higher precedence than equivalence but lower precedence than conjunction.
Conjunction is left-associative and has highest precedence out of the binary connectives.
Negation binds most tightly, and must immediately precede its argument (i.e., there should not be a space between a negation symbol and the proposition that follows).
Valid variable names begin with a letter (uppercase or lowercase) or an underscore, and may be followed by a letter, underscore, digit, or single quote (a "prime" symbol). The exceptions are the strings "false" and "true", which are parsed as the propositional literals \(\bot\) and \(\top\), respectively.

Examples

Expand

>>> parseFormula "a -> b -> c"
Just (Imp (Var "a") (Imp (Var "b") (Var "c")))

>>> parseFormula "~a | b -> c"
Just (Imp (Or (Not (Var "a")) (Var "b")) (Var "c"))

>>> parseFormula "(a -> b) & ~c"
Just (And (Imp (Var "a") (Var "b")) (Not (Var "c")))

parseJudgement :: String -> Maybe (Judgement String) Source #

(parseJudgement s) parses a string s as a propositional judgement.

A valid judgement is made up of an antecedent, a turnstile symbol, and a consequent (in that order). The antecedents are a (potentially empty) comma-separated list of formulas, the turnstile symbol is either "|-" or "⊢", and the consequent is another formula.

See parseFormula for the specification of valid formulas.

Examples

Expand

>>> parseJudgement "a, a -> b |- b"
Just ([Var "a",Imp (Var "a") (Var "b")] |- Var "b")

>>> parseJudgement "a |- a | b"
Just ([Var "a"] |- Or (Var "a") (Var "b"))

Unsafe parsing

unsafeParseFormula :: String -> Formula String Source #

(unsafeParseFormula s) parses a string s as a propositional formula, returning the parsed formula on success, and throwing an error on failure.

See parseFormula for grammar spcecifications.

Examples

Expand

>>> unsafeParseFormula "(a => b) => c"
Imp (Imp (Var "a") (Var "b")) (Var "c")

unsafeParseJudgement :: String -> Judgement String Source #

(unsafeParseJudgement s) parses a string s as a propositional judgement, returning the parsed judgement on success, and throwing an error on failure.

See parseJudgement for the specification of valid judgements.

Examples

Expand

>>> unsafeParseJudgement "a, b |- a -> b"
[Var "a",Var "b"] |- Imp (Var "a") (Var "b")

>>> unsafeParseJudgement "a & b |- a"
[And (Var "a") (Var "b")] |- Var "a"