merc_sabre 1.0.0

Implements a term rewrite engine based on a set automaton based rewriter.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125

use itertools::Itertools;

use crate::set_automaton::SetAutomaton;
use crate::set_automaton::State;
use core::fmt;

use super::MatchAnnouncement;
use super::MatchObligation;
use super::Transition;

impl<M> fmt::Debug for Transition<M> {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        write!(
            f,
            "Transition {{ {}, announce: [{:?}], dest: [{:?}] }}",
            self.symbol,
            self.announcements.iter().map(|(x, _)| { x }).format(", "),
            self.destinations.iter().format_with(", ", |element, f| {
                f(&format_args!("{} -> {}", element.0, element.1))
            })
        )
    }
}

impl fmt::Debug for MatchAnnouncement {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        write!(f, "({})@{}", self.rule, self.position)
    }
}

impl fmt::Debug for MatchObligation {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        write!(f, "{}@{}", self.pattern, self.position)
    }
}

impl fmt::Debug for State {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        writeln!(f, "Label: {}, ", self.label())?;
        writeln!(f, "Match goals: [")?;
        for m in self.match_goals() {
            writeln!(f, "\t {m:?}")?;
        }
        write!(f, "]")
    }
}

impl<M> fmt::Debug for SetAutomaton<M> {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        writeln!(f, "States: {{")?;

        for (state_index, s) in self.states().iter().enumerate() {
            writeln!(f, "State {state_index} {{\n{s:?}")?;

            writeln!(f, "Transitions: {{")?;
            for ((from, _), tr) in self.transitions() {
                if state_index == *from {
                    writeln!(f, "\t {tr:?}")?;
                }
            }
            writeln!(f, "}}")?;
        }

        writeln!(f, "}}")
    }
}

pub struct DotFormatter<'a, M> {
    pub(crate) automaton: &'a SetAutomaton<M>,
    pub(crate) show_backtransitions: bool,
    pub(crate) show_final: bool,
}

impl<M> fmt::Display for DotFormatter<'_, M> {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        // Write the header anf final states.
        writeln!(f, "digraph{{")?;

        if self.show_final {
            writeln!(f, "  final[label=\"💩\"];")?;
        }

        for (i, s) in self.automaton.states().iter().enumerate() {
            let match_goals = s.match_goals().iter().format_with("\\n", |goal, f| {
                f(&format_args!("{}", html_escape::encode_safe(&format!("{goal:?}"))))
            });

            writeln!(
                f,
                "  s{}[shape=record label=\"{{{{s{} | {}}} | {}}}\"]",
                i,
                i,
                s.label(),
                match_goals
            )?;
        }

        for ((i, _), tr) in self.automaton.transitions() {
            let announcements = tr.announcements.iter().format_with(", ", |(announcement, _), f| {
                f(&format_args!("{}@{}", announcement.rule.rhs, announcement.position))
            });

            if tr.destinations.is_empty() {
                if self.show_final {
                    writeln!(f, "  s{} -> final [label=\"{} \\[{}\\]\"]", i, tr.symbol, announcements)?;
                }
            } else {
                writeln!(f, "  \"s{}{}\" [shape=point]", i, tr.symbol,).unwrap();
                writeln!(
                    f,
                    "  s{} -> \"s{}{}\" [label=\"{} \\[{}\\]\"]",
                    i, i, tr.symbol, tr.symbol, announcements
                )?;

                for (pos, des) in &tr.destinations {
                    if self.show_backtransitions || *des != 0 {
                        // Hide backpointers to the initial state.
                        writeln!(f, "  \"s{}{}\" -> s{} [label = \"{}\"]", i, tr.symbol, des, pos)?;
                    }
                }
            }
        }
        writeln!(f, "}}")
    }
}