Lines
62.22 %
Functions
25 %
Branches
33.33 %
use core::fmt;
use ahash::AHashSet;
use merc_aterm::ATerm;
use merc_data::to_untyped_data_expression;
use merc_sabre::Condition;
use merc_sabre::RewriteSpecification;
use merc_sabre::Rule;
/// A rewrite specification contains all the bare info we need for rewriting (in particular no type information) as a syntax tree.
/// Parsing a REC file results in a RewriteSpecificationSyntax.
#[derive(Clone, Default, Debug)]
pub struct RewriteSpecificationSyntax {
pub rewrite_rules: Vec<RewriteRuleSyntax>,
/// Constructor symbols with their arities, as declared in the `CONS` section.
/// Retained because they are part of the specification, but the untyped
/// rewriter does not need them, so [Self::to_rewrite_spec] currently ignores them.
pub constructors: Vec<(String, usize)>,
pub variables: Vec<String>,
}
impl RewriteSpecificationSyntax {
/// Converts the syntax tree into a rewrite specification
pub fn to_rewrite_spec(&self) -> RewriteSpecification {
// The names for all variables
let variables = AHashSet::from_iter(self.variables.clone());
// Store the rewrite rules in the maximally shared term storage
let mut rewrite_rules = Vec::new();
for rule in &self.rewrite_rules {
// Convert the conditions.
let mut conditions = vec![];
for c in &rule.conditions {
let condition = Condition {
lhs: to_untyped_data_expression(c.lhs.clone(), Some(&variables)),
rhs: to_untyped_data_expression(c.rhs.clone(), Some(&variables)),
equality: c.equality,
};
conditions.push(condition);
rewrite_rules.push(Rule {
lhs: to_untyped_data_expression(rule.lhs.clone(), Some(&variables)),
rhs: to_untyped_data_expression(rule.rhs.clone(), Some(&variables)),
conditions,
});
RewriteSpecification::new(rewrite_rules)
/// Merges the current specification with another one.
pub fn merge(&mut self, include_spec: &RewriteSpecificationSyntax) {
self.rewrite_rules.extend_from_slice(&include_spec.rewrite_rules);
self.constructors.extend_from_slice(&include_spec.constructors);
for s in &include_spec.variables {
if !self.variables.contains(s) {
self.variables.push(s.clone());
impl fmt::Display for RewriteSpecificationSyntax {
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
writeln!(f, "Variables: ")?;
for variable in &self.variables {
writeln!(f, "{variable}")?;
writeln!(f, "Rewrite rules: ")?;
writeln!(f, "{rule}")?;
writeln!(f)
/// Syntax tree for rewrite rules
#[derive(Debug, Clone, Eq, PartialEq)]
pub struct RewriteRuleSyntax {
pub lhs: ATerm,
pub rhs: ATerm,
pub conditions: Vec<ConditionSyntax>,
impl fmt::Display for RewriteRuleSyntax {
write!(f, "{} -> {}", self.lhs, self.rhs)?;
for (i, condition) in self.conditions.iter().enumerate() {
let keyword = if i == 0 { "if" } else { "and-if" };
let comparison = if condition.equality { "=" } else { "<>" };
write!(f, " {keyword} {} {comparison} {}", condition.lhs, condition.rhs)?;
Ok(())
/// Syntax tree for conditional part of a rewrite rule
#[derive(Debug, Clone, Eq, PartialEq, Ord, PartialOrd)]
pub struct ConditionSyntax {
pub equality: bool, // The condition either specifies that lhs and rhs are equal or different