1use crate::{FxHashMap, Symbol};
4use packed_term_arena::tree::{MutAlgebra, Tree, TreeArena};
5use smallvec::SmallVec;
6use thiserror::Error;
7
8#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash, PartialOrd, Ord)]
15pub enum HomLabel {
16 Symbol(Symbol),
18 Var(usize),
20}
21
22pub type HomTerm = Tree;
28
29#[derive(Clone, Debug, Error, PartialEq, Eq)]
31pub enum HomomorphismError {
32 #[error("source symbol {symbol:?} was registered with arity {first}, then {second}")]
34 ArityMismatch {
35 symbol: Symbol,
37 first: usize,
39 second: usize,
41 },
42 #[error("source symbol {symbol:?} was registered with a different image term")]
44 ConflictingSourceTerm {
45 symbol: Symbol,
47 },
48 #[error("source symbol {symbol:?} image is missing variable ?{variable}")]
50 MissingVariable {
51 symbol: Symbol,
53 variable: usize,
55 },
56 #[error("source symbol {symbol:?} image uses variable ?{variable} more than once")]
58 DuplicateVariable {
59 symbol: Symbol,
61 variable: usize,
63 },
64 #[error("source symbol {symbol:?} image uses variable ?{variable}, but arity is {arity}")]
66 OutOfRangeVariable {
67 symbol: Symbol,
69 variable: usize,
71 arity: usize,
73 },
74 #[error("source symbol {symbol:?} has no homomorphic image")]
76 UnmappedSymbol {
77 symbol: Symbol,
79 },
80 #[error("image variable ?{variable} cannot be substituted for source arity {arity}")]
82 ApplyVariableOutOfRange {
83 variable: usize,
85 arity: usize,
87 },
88}
89
90#[derive(Clone, Debug, PartialEq, Eq, Hash)]
91enum TermKey {
92 Var(usize),
93 Symbol(Symbol, Vec<TermKey>),
94}
95
96#[derive(Debug)]
107pub struct Homomorphism {
108 arena: TreeArena<HomLabel>,
109 terms: Vec<HomTerm>,
110 labels: Vec<SmallVec<[Symbol; 2]>>,
111 symbol_to_term: FxHashMap<Symbol, usize>,
112 arities: FxHashMap<Symbol, usize>,
113 term_dedup: FxHashMap<TermKey, usize>,
114 root_index: FxHashMap<Symbol, Vec<usize>>,
115}
116
117impl Default for Homomorphism {
118 fn default() -> Self {
119 Self::new()
120 }
121}
122
123impl Homomorphism {
124 pub fn new() -> Self {
126 Self {
127 arena: TreeArena::new(),
128 terms: Vec::new(),
129 labels: Vec::new(),
130 symbol_to_term: FxHashMap::default(),
131 arities: FxHashMap::default(),
132 term_dedup: FxHashMap::default(),
133 root_index: FxHashMap::default(),
134 }
135 }
136
137 pub fn with_arena(arena: TreeArena<HomLabel>) -> Self {
141 Self {
142 arena,
143 terms: Vec::new(),
144 labels: Vec::new(),
145 symbol_to_term: FxHashMap::default(),
146 arities: FxHashMap::default(),
147 term_dedup: FxHashMap::default(),
148 root_index: FxHashMap::default(),
149 }
150 }
151
152 pub fn arena(&self) -> &TreeArena<HomLabel> {
154 &self.arena
155 }
156
157 pub fn add_var(&mut self, variable: usize) -> HomTerm {
159 self.arena.add_node(HomLabel::Var(variable), Vec::new())
160 }
161
162 pub fn add_symbol(&mut self, symbol: Symbol, children: Vec<HomTerm>) -> HomTerm {
164 self.arena.add_node(HomLabel::Symbol(symbol), children)
165 }
166
167 pub fn add(
174 &mut self,
175 src: Symbol,
176 src_arity: usize,
177 rhs: HomTerm,
178 ) -> Result<(), HomomorphismError> {
179 if let Some(&old) = self.arities.get(&src)
180 && old != src_arity
181 {
182 return Err(HomomorphismError::ArityMismatch {
183 symbol: src,
184 first: old,
185 second: src_arity,
186 });
187 }
188
189 self.validate_nondeleting(src, src_arity, rhs)?;
190 let key = self.term_key(rhs);
191
192 if let Some(&old_term_id) = self.symbol_to_term.get(&src) {
193 let old_key = self.term_key(self.terms[old_term_id]);
194 if old_key != key {
195 return Err(HomomorphismError::ConflictingSourceTerm { symbol: src });
196 }
197 return Ok(());
198 }
199
200 let term_id = if let Some(&tid) = self.term_dedup.get(&key) {
201 tid
202 } else {
203 let tid = self.terms.len();
204 if let HomLabel::Symbol(symbol) = *self.arena.get_label(rhs) {
205 self.root_index.entry(symbol).or_default().push(tid);
206 }
207 self.term_dedup.insert(key, tid);
208 self.terms.push(rhs);
209 self.labels.push(SmallVec::new());
210 tid
211 };
212
213 self.arities.insert(src, src_arity);
214 self.symbol_to_term.insert(src, term_id);
215 self.labels[term_id].push(src);
216 Ok(())
217 }
218
219 pub fn get(&self, src: Symbol) -> Option<HomTerm> {
221 let &tid = self.symbol_to_term.get(&src)?;
222 Some(self.terms[tid])
223 }
224
225 pub fn term_id(&self, src: Symbol) -> Option<usize> {
227 self.symbol_to_term.get(&src).copied()
228 }
229
230 pub fn label_set(&self, term_id: usize) -> &[Symbol] {
232 &self.labels[term_id]
233 }
234
235 pub fn source_arity(&self, src: Symbol) -> Option<usize> {
237 self.arities.get(&src).copied()
238 }
239
240 pub fn term_sets(&self) -> impl Iterator<Item = (usize, &[Symbol], HomTerm)> + '_ {
242 self.terms
243 .iter()
244 .copied()
245 .enumerate()
246 .map(|(tid, term)| (tid, self.labels[tid].as_slice(), term))
247 }
248
249 pub fn num_terms(&self) -> usize {
251 self.terms.len()
252 }
253
254 pub fn term_by_id(&self, term_id: usize) -> HomTerm {
256 self.terms[term_id]
257 }
258
259 pub fn terms_with_root(&self, sym: Symbol) -> &[usize] {
261 self.root_index
262 .get(&sym)
263 .map(Vec::as_slice)
264 .unwrap_or_default()
265 }
266
267 pub fn apply(
274 &self,
275 input_arena: &TreeArena<Symbol>,
276 input_root: Tree,
277 output_arena: &mut TreeArena<Symbol>,
278 ) -> Result<Tree, HomomorphismError> {
279 let mut alg = ApplyAlg {
280 hom: self,
281 output_arena,
282 };
283 input_arena.map(input_root, |symbol| *symbol, &mut alg)
284 }
285
286 fn validate_nondeleting(
287 &self,
288 src: Symbol,
289 src_arity: usize,
290 rhs: HomTerm,
291 ) -> Result<(), HomomorphismError> {
292 let mut seen = vec![false; src_arity];
293 let mut vars = Vec::new();
294 self.collect_vars(rhs, &mut vars);
295 for variable in vars {
296 if variable >= src_arity {
297 return Err(HomomorphismError::OutOfRangeVariable {
298 symbol: src,
299 variable,
300 arity: src_arity,
301 });
302 }
303 if seen[variable] {
304 return Err(HomomorphismError::DuplicateVariable {
305 symbol: src,
306 variable,
307 });
308 }
309 seen[variable] = true;
310 }
311 for (variable, was_seen) in seen.into_iter().enumerate() {
312 if !was_seen {
313 return Err(HomomorphismError::MissingVariable {
314 symbol: src,
315 variable,
316 });
317 }
318 }
319 Ok(())
320 }
321
322 fn collect_vars(&self, term: HomTerm, out: &mut Vec<usize>) {
323 match *self.arena.get_label(term) {
324 HomLabel::Var(variable) => out.push(variable),
325 HomLabel::Symbol(_) => {
326 for &child in self.arena.get_children(term) {
327 self.collect_vars(child, out);
328 }
329 }
330 }
331 }
332
333 fn term_key(&self, term: HomTerm) -> TermKey {
334 match *self.arena.get_label(term) {
335 HomLabel::Var(variable) => TermKey::Var(variable),
336 HomLabel::Symbol(symbol) => TermKey::Symbol(
337 symbol,
338 self.arena
339 .get_children(term)
340 .iter()
341 .map(|&child| self.term_key(child))
342 .collect(),
343 ),
344 }
345 }
346
347 fn instantiate(
348 &self,
349 rhs: HomTerm,
350 mapped_children: &[Tree],
351 output_arena: &mut TreeArena<Symbol>,
352 ) -> Result<Tree, HomomorphismError> {
353 match *self.arena.get_label(rhs) {
354 HomLabel::Var(variable) => mapped_children.get(variable).copied().ok_or(
355 HomomorphismError::ApplyVariableOutOfRange {
356 variable,
357 arity: mapped_children.len(),
358 },
359 ),
360 HomLabel::Symbol(symbol) => {
361 let children = self
362 .arena
363 .get_children(rhs)
364 .iter()
365 .map(|&child| self.instantiate(child, mapped_children, output_arena))
366 .collect::<Result<Vec<_>, _>>()?;
367 Ok(output_arena.add_node(symbol, children))
368 }
369 }
370 }
371}
372
373struct ApplyAlg<'h, 'out> {
374 hom: &'h Homomorphism,
375 output_arena: &'out mut TreeArena<Symbol>,
376}
377
378impl MutAlgebra<Symbol, Result<Tree, HomomorphismError>> for ApplyAlg<'_, '_> {
379 fn apply(
380 &mut self,
381 src: Symbol,
382 children: Vec<Result<Tree, HomomorphismError>>,
383 ) -> Result<Tree, HomomorphismError> {
384 let mapped_children = children.into_iter().collect::<Result<Vec<_>, _>>()?;
385 let rhs = self
386 .hom
387 .get(src)
388 .ok_or(HomomorphismError::UnmappedSymbol { symbol: src })?;
389 self.hom
390 .instantiate(rhs, &mapped_children, self.output_arena)
391 }
392}
393
394#[cfg(test)]
395mod tests {
396 use super::*;
397
398 fn sym(i: u32) -> Symbol {
399 Symbol(i)
400 }
401
402 fn var(arena: &mut TreeArena<HomLabel>, i: usize) -> Tree {
403 arena.add_node(HomLabel::Var(i), vec![])
404 }
405
406 fn node(arena: &mut TreeArena<HomLabel>, symbol: Symbol, children: Vec<Tree>) -> Tree {
407 arena.add_node(HomLabel::Symbol(symbol), children)
408 }
409
410 #[test]
411 fn deduplicates_identical_terms() {
412 let mut arena = TreeArena::new();
413 let v0 = var(&mut arena, 0);
414 let v1 = var(&mut arena, 1);
415 let term = node(&mut arena, sym(10), vec![v0, v1]);
416 let same_v0 = var(&mut arena, 0);
417 let same_v1 = var(&mut arena, 1);
418 let same = node(&mut arena, sym(10), vec![same_v0, same_v1]);
419
420 let mut h = Homomorphism::with_arena(arena);
421 h.add(sym(0), 2, term).unwrap();
422 h.add(sym(1), 2, same).unwrap();
423
424 assert_eq!(h.term_id(sym(0)), h.term_id(sym(1)));
425 let labels = h.label_set(h.term_id(sym(0)).unwrap());
426 assert!(labels.contains(&sym(0)));
427 assert!(labels.contains(&sym(1)));
428 assert_eq!(h.num_terms(), 1);
429 }
430
431 #[test]
432 fn rejects_invalid_nondeleting_terms() {
433 let mut arena = TreeArena::new();
434 let missing_v0 = var(&mut arena, 0);
435 let missing = node(&mut arena, sym(10), vec![missing_v0]);
436 let duplicate_v0a = var(&mut arena, 0);
437 let duplicate_v0b = var(&mut arena, 0);
438 let duplicate = node(&mut arena, sym(10), vec![duplicate_v0a, duplicate_v0b]);
439 let out_of_range_v0 = var(&mut arena, 0);
440 let out_of_range_v2 = var(&mut arena, 2);
441 let out_of_range = node(&mut arena, sym(10), vec![out_of_range_v0, out_of_range_v2]);
442
443 let mut h = Homomorphism::with_arena(arena);
444 assert!(matches!(
445 h.add(sym(0), 2, missing),
446 Err(HomomorphismError::MissingVariable { variable: 1, .. })
447 ));
448 assert!(matches!(
449 h.add(sym(1), 2, duplicate),
450 Err(HomomorphismError::DuplicateVariable { variable: 0, .. })
451 ));
452 assert!(matches!(
453 h.add(sym(2), 2, out_of_range),
454 Err(HomomorphismError::OutOfRangeVariable { variable: 2, .. })
455 ));
456 }
457
458 #[test]
459 fn rejects_conflicting_reregistration() {
460 let mut arena = TreeArena::new();
461 let first_v0 = var(&mut arena, 0);
462 let first = node(&mut arena, sym(10), vec![first_v0]);
463 let second_v0 = var(&mut arena, 0);
464 let second = node(&mut arena, sym(11), vec![second_v0]);
465
466 let mut h = Homomorphism::with_arena(arena);
467 h.add(sym(0), 1, first).unwrap();
468 assert!(matches!(
469 h.add(sym(0), 2, first),
470 Err(HomomorphismError::ArityMismatch { .. })
471 ));
472 assert!(matches!(
473 h.add(sym(0), 1, second),
474 Err(HomomorphismError::ConflictingSourceTerm { .. })
475 ));
476 }
477
478 #[test]
479 fn apply_maps_nullary_and_nested_terms() {
480 let mut hom_arena = TreeArena::new();
481 let leaf_rhs = node(&mut hom_arena, sym(20), vec![]);
482 let concat_v0 = var(&mut hom_arena, 0);
483 let concat_v1 = var(&mut hom_arena, 1);
484 let concat_rhs = node(&mut hom_arena, sym(21), vec![concat_v0, concat_v1]);
485 let wrap_rhs = node(&mut hom_arena, sym(22), vec![concat_rhs]);
486
487 let mut hom = Homomorphism::with_arena(hom_arena);
488 hom.add(sym(0), 0, leaf_rhs).unwrap();
489 hom.add(sym(1), 2, wrap_rhs).unwrap();
490
491 let mut input = TreeArena::new();
492 let l = input.add_node(sym(0), vec![]);
493 let r = input.add_node(sym(0), vec![]);
494 let root = input.add_node(sym(1), vec![l, r]);
495
496 let mut output = TreeArena::new();
497 let out_root = hom.apply(&input, root, &mut output).unwrap();
498 assert_eq!(*output.get_label(out_root), sym(22));
499 let concat = output.get_children(out_root)[0];
500 assert_eq!(*output.get_label(concat), sym(21));
501 let leaves = output.get_children(concat);
502 assert_eq!(*output.get_label(leaves[0]), sym(20));
503 assert_eq!(*output.get_label(leaves[1]), sym(20));
504 }
505
506 #[test]
507 fn apply_reports_unmapped_symbols() {
508 let hom_arena = TreeArena::new();
509 let hom = Homomorphism::with_arena(hom_arena);
510 let mut input = TreeArena::new();
511 let root = input.add_node(sym(99), vec![]);
512 let mut output = TreeArena::new();
513 assert_eq!(
514 hom.apply(&input, root, &mut output),
515 Err(HomomorphismError::UnmappedSymbol { symbol: sym(99) })
516 );
517 }
518}