Function term_rewriting::parse

pub fn parse(
    sig: &mut Signature, 
    input: &str
) -> Result<(TRS, Vec<Term>), ParseError>

Parse a string as a TRS and a list of Terms.

TRS syntax

input is parsed as a <program>, defined as follows:

<program> ::= ( <comment>* <statement> ";" <comment>* )*

<comment> ::= "#" <any-char-but-newline> "\n"

<statement> ::= <rule> | <top-level-term>

<rule> ::= <top-level-term> "=" <top-level-term> ( "|" <top-level-term> )

<top-level-term) ::= ( <term> | ( "(" <top-level-term> ")" ) ) (" "  ( <term> | ( "(" <top-level-term> ")" ) ) )*

<term> ::= <variable> | <application>

<variable> ::= <identifier>"_"

<application> ::= <constant> | <binary-application> | <standard-application>

<constant> ::= <identifier>

<binary-application> ::= "(" <term> " " <term> ")"

<standard-application> ::= <identifier> "(" <term>* ")"

<identifier> ::= <alphanumeric>+