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

The input is parsed as a program, defined as follows in augmented Backus-Naur form:

program = *wsp *( *comment statement ";" *comment ) *wsp

statement = rule / top-level-term

rule = top-level-term *wsp "=" *wsp top-level-term
rule /= rule *wsp "|" *wsp top-level-term

top-level-term = term / "(" top-level-term ")"
top-level-term /= top-level-term 1*wsp top-level-term

term = variable / application

variable = identifier"_"

application = identifier "(" [ term *( 1*wsp term ) ] ")"
application /= identifier
application /= binary-application

; binary application is the '.' operator with arity 2.
binary-application = "(" *wsp term *wsp term *wsp ")"

identifier = 1*( ALPHA / DIGIT )

comment = "#" *any-char-but-newline "\n"

wsp = SP / TAB / CR / LF

Examples

let inp = "
#-- rules:
    S x_ y_ z_ = x_ z_ (y_ z_);
    K x_ y_ = x_;
    PLUS(SUCC(x_) y_) = PLUS(x_ SUCC(y_));
    PLUS(ZERO y_) = y_;

#-- terms:
    S K S K;
    PLUS(SUCC(SUCC(SUCC(ZERO))) SUCC(ZERO));
";
let (trs, terms) = parse(&mut Signature::default(), inp).unwrap();