Crate merc_sabre 

Overview

The Set Automaton Based Rewrite Engine (abbreviated Sabre) is a library that implements rewriting on top of the (sorted) data expressions defined in the merc_data crate. For the purpose of rewriting, these sorts are irrelevant, but it is important that we can have function symbols with the same name and arity but different sorts.

Usage

Typically one parses the rewrite rules from a file writting the mCRL2 language, or the Rewrite Engine Competition (REC) format, but it can also be constructed programmatically for demonstration purposes, or for testing.

use merc_aterm::ATerm;

use merc_sabre::test_utility::create_rewrite_rule;
use merc_sabre::RewriteSpecification;
use merc_sabre::SabreRewriter;
use merc_sabre::RewriteEngine;

use merc_data::to_untyped_data_expression;

// Peano arithmetic rewrite rules
let rule_zero = create_rewrite_rule("plus(x, 0)", "x", &["x"]).unwrap();
let rule_succ = create_rewrite_rule("plus(x, S(y))", "S(plus(x, y))", &["x", "y"]).unwrap();

let spec = RewriteSpecification::new(vec![rule_zero, rule_succ]);

let mut rewriter = SabreRewriter::new(&spec);
let term = to_untyped_data_expression(ATerm::from_string("plus(S(S(0)), S(0))").unwrap(), None);

let rewritten_term = rewriter.rewrite(&term);
assert_eq!(rewritten_term.to_string(), "S(S(S(0)))");

This crate implements a NaiveRewriter for reference testing, an InnermostRewriter that is strictly innermost and uses Adaptive Pattern Matching, and the full SabreRewriter that uses the Set Automaton construction for matching.

Safety

This crate does not use unsafe code.

Related work

The Set Automaton Based Rewrite Engine (abbreviated Sabre) was first described in the following article:

“Term Rewriting Based On Set Automaton Matching”. Mark Bouwman, Rick Erkens. DOI.

The Set automaton construction that is used for matching is based on the following article:

“Erkens, R., Groote, J.F. (2021). A Set Automaton to Locate All Pattern Matches in a Term”. In: Cerone, A., Ölveczky, P.C. (eds) Theoretical Aspects of Computing – ICTAC 2021. ICTAC 2021. Lecture Notes in Computer Science, vol 12819. Springer, Cham. DOI

Authors

The original sabre crate was implemented by Mark Bouwman, with theoretical contributions by Rick Erkens and Jan Friso Groote. This version has been adapted to use the merc_aterm crate for the term representation, by Maurice Laveaux.

Minimum Supported Rust Version

We do not maintain an official minimum supported rust version (MSRV), and it may be upgraded at any time when necessary.

License

All MERC crates are licensed under the BSL-1.0 license. See the LICENSE file in the repository root for more information.

Modules

test_utility

utilities

Structs

AnnouncementInnermost

Condition

A condition of a conditional rewrite rule.

Derivative

DotFormatter

InnermostRewriter

Innermost Adaptive Pattern Matching Automaton (APMA) rewrite engine.

MatchAnnouncement

A match announcement contains the rule that can be announced as a match at the given position.

MatchObligation

Represents a match obligation in the SetAutomaton.

NaiveRewriter

Naive Adaptive Pattern Matching Automaton (APMA) rewrite engine implementation for testing purposes.

RewriteSpecification

A rewrite specification is a set of rewrite rules, given by Rule.

RewritingStatistics

Rule

A rewrite rule.

SabreRewriter

A set automaton based rewrite engine described in Mark Bouwman, Rick Erkens: Term Rewriting Based On Set Automaton Matching. CoRR abs/2202.08687 (2022)

SetAutomaton

The Set Automaton used to find all matching patterns in a term.

State

Transition

Represents a transition in the SetAutomaton.

Traits

RewriteEngine

A shared trait for all the rewriters

Functions

is_supported_rule

Checks whether the set automaton can use this rule, no higher order rules or binders.