Module razor_fol::parser

Implements a parser for first-order formulae and theories in Razor's syntax.

The module provides a parser for first-order formulae by implementing FromStr for Formula and Theory. The parser is often used implicitly through str::parse method.

Example: The following example parses a string into a Formula:

use razor_fol::syntax::Formula;

// parse a string into `Formula`:
let formula: Formula = "exists x. P(x) & Q(x)".parse().unwrap();

assert_eq!("∃ x. (P(x) ∧ Q(x))", formula.to_string());

Similarly, a Theory can be parsed from a string:

use razor_fol::syntax::Theory;

// parse a string into `Theory` (formulae are separated by `;`)
let theory: Theory = r#"
   // mathematical notation:
   ∀ x. Eq(x, x);
   // verbose notation:
   forall x, y. (Eq(x, y) implies Eq(y, x));
   // compact notation:
   ? x, y, z. (Eq(x, y) & Eq(y, z) -> Eq(x, z));
"#.parse().unwrap();

assert_eq!("∀ x. Eq(x, x)\n\
∀ x, y. (Eq(x, y) → Eq(y, x))\n\
∃ x, y, z. ((Eq(x, y) ∧ Eq(y, z)) → Eq(x, z))", theory.to_string());

Functions

p_block_comment
p_line_comment
spaces
theory