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
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
#![forbid(unsafe_code)]
use log::info;
use merc_aterm::THREAD_TERM_POOL;
use merc_aterm::ThreadTermPool;
use merc_data::DataExpression;
use merc_data::DataExpressionRef;
use crate::RewriteSpecification;
use crate::matching::nonlinear::check_equivalence_classes;
use crate::set_automaton::MatchAnnouncement;
use crate::set_automaton::SetAutomaton;
use crate::utilities::AnnouncementSabre;
use crate::utilities::ConfigurationStack;
use crate::utilities::DataPositionIndexed;
use crate::utilities::SideInfo;
use crate::utilities::SideInfoType;
use merc_utilities::debug_trace;
/// A shared trait for all the rewriters
pub trait RewriteEngine {
/// Rewrites the given term into normal form.
fn rewrite(&mut self, term: &DataExpression) -> DataExpression;
}
#[derive(Default)]
pub struct RewritingStatistics {
/// Count the number of rewrite rules applied
pub rewrite_steps: usize,
/// Counts the number of times symbols are compared.
pub symbol_comparisons: usize,
/// The number of times rewrite is called recursively (to rewrite conditions etc)
pub recursions: usize,
}
/// A set automaton based rewrite engine described in Mark Bouwman, Rick Erkens:
/// Term Rewriting Based On Set Automaton Matching. CoRR abs/2202.08687 (2022)
pub struct SabreRewriter {
automaton: SetAutomaton<AnnouncementSabre>,
}
impl RewriteEngine for SabreRewriter {
fn rewrite(&mut self, term: &DataExpression) -> DataExpression {
self.stack_based_normalise(term)
}
}
impl SabreRewriter {
pub fn new(spec: &RewriteSpecification) -> Self {
let automaton = SetAutomaton::new(spec, AnnouncementSabre::new, false);
SabreRewriter { automaton }
}
/// Function to rewrite a term. See the module documentation.
pub fn stack_based_normalise(&mut self, t: &DataExpression) -> DataExpression {
let mut stats = RewritingStatistics::default();
let result = THREAD_TERM_POOL
.with_borrow(|tp| SabreRewriter::stack_based_normalise_aux(tp, &self.automaton, t, &mut stats));
info!(
"{} rewrites, {} single steps and {} symbol comparisons",
stats.recursions, stats.rewrite_steps, stats.symbol_comparisons
);
result
}
/// The _aux function splits the [TermPool] pool and the [SetAutomaton] to make borrow checker happy.
/// We can now mutate the term pool and read the state and transition information at the same time
fn stack_based_normalise_aux(
tp: &ThreadTermPool,
automaton: &SetAutomaton<AnnouncementSabre>,
t: &DataExpression,
stats: &mut RewritingStatistics,
) -> DataExpression {
stats.recursions += 1;
// We explore the configuration tree depth first using a ConfigurationStack
let mut cs = ConfigurationStack::new(0, t);
// Big loop until we know we have a normal form
'outer: loop {
// Inner loop so that we can easily break; to the next iteration
'skip_point: loop {
debug_trace!("{}", cs);
// Check if there is any configuration leaf left to explore, if not we have found a normal form
if let Some(leaf_index) = cs.get_unexplored_leaf() {
let leaf = &mut cs.stack[leaf_index];
let read_terms = cs.terms.read();
let leaf_term = &read_terms[leaf_index];
match ConfigurationStack::pop_side_branch_leaf(&mut cs.side_branch_stack, leaf_index) {
None => {
// Observe a symbol according to the state label of the set automaton.
let pos: DataExpressionRef =
leaf_term.get_data_position(automaton.states()[leaf.state].label());
let function_symbol = pos.data_function_symbol();
stats.symbol_comparisons += 1;
// Get the transition belonging to the observed symbol
if let Some(tr) = automaton
.transitions()
.get(&(leaf.state, function_symbol.operation_id()))
{
// Loop over the match announcements of the transition
for (announcement, annotation) in &tr.announcements {
if annotation.conditions.is_empty() && annotation.equivalence_classes.is_empty() {
if annotation.is_duplicating {
debug_trace!("Delaying duplicating rule {}", announcement.rule);
// We do not want to apply duplicating rules straight away
cs.side_branch_stack.push(SideInfo {
corresponding_configuration: leaf_index,
info: SideInfoType::DelayedRewriteRule(announcement, annotation),
});
} else {
// For a rewrite rule that is not duplicating or has a condition we just apply it straight away
drop(read_terms);
SabreRewriter::apply_rewrite_rule(
tp,
automaton,
announcement,
annotation,
leaf_index,
&mut cs,
stats,
);
break 'skip_point;
}
} else {
// We delay the condition checks
debug_trace!("Delaying condition check for rule {}", announcement.rule);
cs.side_branch_stack.push(SideInfo {
corresponding_configuration: leaf_index,
info: SideInfoType::EquivalenceAndConditionCheck(announcement, annotation),
});
}
}
drop(read_terms);
if tr.destinations.is_empty() {
// If there is no destination we are done matching and go back to the previous
// configuration on the stack with information on the side stack.
// Note, it could be that we stay at the same configuration and apply a rewrite
// rule that was just discovered whilst exploring this configuration.
let prev = cs.get_prev_with_side_info();
cs.current_node = prev;
if let Some(n) = prev {
cs.jump_back(n, tp);
}
} else {
// Grow the bud; if there is more than one destination a SideBranch object will be placed on the side stack
let tr_slice = tr.destinations.as_slice();
cs.grow(leaf_index, tr_slice);
}
} else {
let prev = cs.get_prev_with_side_info();
cs.current_node = prev;
if let Some(n) = prev {
drop(read_terms);
cs.jump_back(n, tp);
}
}
}
Some(sit) => {
match sit {
SideInfoType::SideBranch(sb) => {
// If there is a SideBranch pick the next child configuration
drop(read_terms);
cs.grow(leaf_index, sb);
}
SideInfoType::DelayedRewriteRule(announcement, annotation) => {
drop(read_terms);
// apply the delayed rewrite rule
SabreRewriter::apply_rewrite_rule(
tp,
automaton,
announcement,
annotation,
leaf_index,
&mut cs,
stats,
);
}
SideInfoType::EquivalenceAndConditionCheck(announcement, annotation) => {
// Apply the delayed rewrite rule if the conditions hold
if check_equivalence_classes(leaf_term, &annotation.equivalence_classes)
&& SabreRewriter::conditions_hold(
tp,
automaton,
announcement,
annotation,
leaf_term,
stats,
)
{
drop(read_terms);
SabreRewriter::apply_rewrite_rule(
tp,
automaton,
announcement,
annotation,
leaf_index,
&mut cs,
stats,
);
}
}
}
}
}
} else {
// No configuration left to explore, we have found a normal form
break 'outer;
}
}
}
cs.compute_final_term(tp)
}
/// Apply a rewrite rule and prune back
fn apply_rewrite_rule(
tp: &ThreadTermPool,
automaton: &SetAutomaton<AnnouncementSabre>,
announcement: &MatchAnnouncement,
annotation: &AnnouncementSabre,
leaf_index: usize,
cs: &mut ConfigurationStack<'_>,
stats: &mut RewritingStatistics,
) {
stats.rewrite_steps += 1;
let read_terms = cs.terms.read();
let leaf_subterm: &DataExpressionRef<'_> = &read_terms[leaf_index];
// Computes the new subterm of the configuration
let new_subterm = annotation
.rhs_term_stack
.evaluate(&leaf_subterm.get_data_position(&announcement.position));
debug_trace!(
"rewrote {} to {} using rule {}",
&leaf_subterm,
&new_subterm,
announcement.rule
);
// The match announcement tells us how far we need to prune back.
let prune_point = leaf_index - announcement.symbols_seen;
drop(read_terms);
cs.prune(tp, automaton, prune_point, new_subterm);
}
/// Checks conditions and subterm equality of non-linear patterns.
fn conditions_hold(
tp: &ThreadTermPool,
automaton: &SetAutomaton<AnnouncementSabre>,
announcement: &MatchAnnouncement,
annotation: &AnnouncementSabre,
subterm: &DataExpressionRef<'_>,
stats: &mut RewritingStatistics,
) -> bool {
for c in &annotation.conditions {
let subterm = subterm.get_data_position(&announcement.position);
let rhs: DataExpression = c.rhs_term_stack.evaluate(&subterm);
let lhs: DataExpression = c.lhs_term_stack.evaluate(&subterm);
// Equality => lhs == rhs.
if !c.equality || lhs != rhs {
let rhs_normal = SabreRewriter::stack_based_normalise_aux(tp, automaton, &rhs, stats);
let lhs_normal = SabreRewriter::stack_based_normalise_aux(tp, automaton, &lhs, stats);
// If lhs != rhs && !equality OR equality && lhs == rhs.
if (!c.equality && lhs_normal == rhs_normal) || (c.equality && lhs_normal != rhs_normal) {
return false;
}
}
}
true
}
}