Skip to main content

oxilean_kernel/termination/
types.rs

1//! Auto-generated module
2//!
3//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)
4
5use super::functions::*;
6use crate::{Expr, Name};
7use std::collections::{HashMap, HashSet};
8
9/// A simple directed acyclic graph.
10#[allow(dead_code)]
11pub struct SimpleDag {
12    /// `edges[i]` is the list of direct successors of node `i`.
13    edges: Vec<Vec<usize>>,
14}
15#[allow(dead_code)]
16impl SimpleDag {
17    /// Creates a DAG with `n` nodes and no edges.
18    pub fn new(n: usize) -> Self {
19        Self {
20            edges: vec![Vec::new(); n],
21        }
22    }
23    /// Adds an edge from `from` to `to`.
24    pub fn add_edge(&mut self, from: usize, to: usize) {
25        if from < self.edges.len() {
26            self.edges[from].push(to);
27        }
28    }
29    /// Returns the successors of `node`.
30    pub fn successors(&self, node: usize) -> &[usize] {
31        self.edges.get(node).map(|v| v.as_slice()).unwrap_or(&[])
32    }
33    /// Returns `true` if `from` can reach `to` via DFS.
34    pub fn can_reach(&self, from: usize, to: usize) -> bool {
35        let mut visited = vec![false; self.edges.len()];
36        self.dfs(from, to, &mut visited)
37    }
38    fn dfs(&self, cur: usize, target: usize, visited: &mut Vec<bool>) -> bool {
39        if cur == target {
40            return true;
41        }
42        if cur >= visited.len() || visited[cur] {
43            return false;
44        }
45        visited[cur] = true;
46        for &next in self.successors(cur) {
47            if self.dfs(next, target, visited) {
48                return true;
49            }
50        }
51        false
52    }
53    /// Returns the topological order of nodes, or `None` if a cycle is detected.
54    pub fn topological_sort(&self) -> Option<Vec<usize>> {
55        let n = self.edges.len();
56        let mut in_degree = vec![0usize; n];
57        for succs in &self.edges {
58            for &s in succs {
59                if s < n {
60                    in_degree[s] += 1;
61                }
62            }
63        }
64        let mut queue: std::collections::VecDeque<usize> =
65            (0..n).filter(|&i| in_degree[i] == 0).collect();
66        let mut order = Vec::new();
67        while let Some(node) = queue.pop_front() {
68            order.push(node);
69            for &s in self.successors(node) {
70                if s < n {
71                    in_degree[s] -= 1;
72                    if in_degree[s] == 0 {
73                        queue.push_back(s);
74                    }
75                }
76            }
77        }
78        if order.len() == n {
79            Some(order)
80        } else {
81            None
82        }
83    }
84    /// Returns the number of nodes.
85    pub fn num_nodes(&self) -> usize {
86        self.edges.len()
87    }
88}
89/// A fixed-size sliding window that computes a running sum.
90#[allow(dead_code)]
91pub struct SlidingSum {
92    window: Vec<f64>,
93    capacity: usize,
94    pos: usize,
95    sum: f64,
96    count: usize,
97}
98#[allow(dead_code)]
99impl SlidingSum {
100    /// Creates a sliding sum with the given window size.
101    pub fn new(capacity: usize) -> Self {
102        Self {
103            window: vec![0.0; capacity],
104            capacity,
105            pos: 0,
106            sum: 0.0,
107            count: 0,
108        }
109    }
110    /// Adds a value to the window, removing the oldest if full.
111    pub fn push(&mut self, val: f64) {
112        let oldest = self.window[self.pos];
113        self.sum -= oldest;
114        self.sum += val;
115        self.window[self.pos] = val;
116        self.pos = (self.pos + 1) % self.capacity;
117        if self.count < self.capacity {
118            self.count += 1;
119        }
120    }
121    /// Returns the current window sum.
122    pub fn sum(&self) -> f64 {
123        self.sum
124    }
125    /// Returns the window mean, or `None` if empty.
126    pub fn mean(&self) -> Option<f64> {
127        if self.count == 0 {
128            None
129        } else {
130            Some(self.sum / self.count as f64)
131        }
132    }
133    /// Returns the current window size (number of valid elements).
134    pub fn count(&self) -> usize {
135        self.count
136    }
137}
138/// A min-heap implemented as a binary heap.
139#[allow(dead_code)]
140pub struct MinHeap<T: Ord> {
141    data: Vec<T>,
142}
143#[allow(dead_code)]
144impl<T: Ord> MinHeap<T> {
145    /// Creates a new empty min-heap.
146    pub fn new() -> Self {
147        Self { data: Vec::new() }
148    }
149    /// Inserts an element.
150    pub fn push(&mut self, val: T) {
151        self.data.push(val);
152        self.sift_up(self.data.len() - 1);
153    }
154    /// Removes and returns the minimum element.
155    pub fn pop(&mut self) -> Option<T> {
156        if self.data.is_empty() {
157            return None;
158        }
159        let n = self.data.len();
160        self.data.swap(0, n - 1);
161        let min = self.data.pop();
162        if !self.data.is_empty() {
163            self.sift_down(0);
164        }
165        min
166    }
167    /// Returns a reference to the minimum element.
168    pub fn peek(&self) -> Option<&T> {
169        self.data.first()
170    }
171    /// Returns the number of elements.
172    pub fn len(&self) -> usize {
173        self.data.len()
174    }
175    /// Returns `true` if empty.
176    pub fn is_empty(&self) -> bool {
177        self.data.is_empty()
178    }
179    fn sift_up(&mut self, mut i: usize) {
180        while i > 0 {
181            let parent = (i - 1) / 2;
182            if self.data[i] < self.data[parent] {
183                self.data.swap(i, parent);
184                i = parent;
185            } else {
186                break;
187            }
188        }
189    }
190    fn sift_down(&mut self, mut i: usize) {
191        let n = self.data.len();
192        loop {
193            let left = 2 * i + 1;
194            let right = 2 * i + 2;
195            let mut smallest = i;
196            if left < n && self.data[left] < self.data[smallest] {
197                smallest = left;
198            }
199            if right < n && self.data[right] < self.data[smallest] {
200                smallest = right;
201            }
202            if smallest == i {
203                break;
204            }
205            self.data.swap(i, smallest);
206            i = smallest;
207        }
208    }
209}
210/// A versioned record that stores a history of values.
211#[allow(dead_code)]
212pub struct VersionedRecord<T: Clone> {
213    history: Vec<T>,
214}
215#[allow(dead_code)]
216impl<T: Clone> VersionedRecord<T> {
217    /// Creates a new record with an initial value.
218    pub fn new(initial: T) -> Self {
219        Self {
220            history: vec![initial],
221        }
222    }
223    /// Updates the record with a new version.
224    pub fn update(&mut self, val: T) {
225        self.history.push(val);
226    }
227    /// Returns the current (latest) value.
228    pub fn current(&self) -> &T {
229        self.history
230            .last()
231            .expect("VersionedRecord history is always non-empty after construction")
232    }
233    /// Returns the value at version `n` (0-indexed), or `None`.
234    pub fn at_version(&self, n: usize) -> Option<&T> {
235        self.history.get(n)
236    }
237    /// Returns the version number of the current value.
238    pub fn version(&self) -> usize {
239        self.history.len() - 1
240    }
241    /// Returns `true` if more than one version exists.
242    pub fn has_history(&self) -> bool {
243        self.history.len() > 1
244    }
245}
246/// A dependency closure builder (transitive closure via BFS).
247#[allow(dead_code)]
248pub struct TransitiveClosure {
249    adj: Vec<Vec<usize>>,
250    n: usize,
251}
252#[allow(dead_code)]
253impl TransitiveClosure {
254    /// Creates a transitive closure builder for `n` nodes.
255    pub fn new(n: usize) -> Self {
256        Self {
257            adj: vec![Vec::new(); n],
258            n,
259        }
260    }
261    /// Adds a direct edge.
262    pub fn add_edge(&mut self, from: usize, to: usize) {
263        if from < self.n {
264            self.adj[from].push(to);
265        }
266    }
267    /// Computes all nodes reachable from `start` (including `start`).
268    pub fn reachable_from(&self, start: usize) -> Vec<usize> {
269        let mut visited = vec![false; self.n];
270        let mut queue = std::collections::VecDeque::new();
271        queue.push_back(start);
272        while let Some(node) = queue.pop_front() {
273            if node >= self.n || visited[node] {
274                continue;
275            }
276            visited[node] = true;
277            for &next in &self.adj[node] {
278                queue.push_back(next);
279            }
280        }
281        (0..self.n).filter(|&i| visited[i]).collect()
282    }
283    /// Returns `true` if `from` can transitively reach `to`.
284    pub fn can_reach(&self, from: usize, to: usize) -> bool {
285        self.reachable_from(from).contains(&to)
286    }
287}
288/// A simple decision tree node for rule dispatching.
289#[allow(dead_code)]
290#[allow(missing_docs)]
291pub enum DecisionNode {
292    /// A leaf with an action string.
293    Leaf(String),
294    /// An interior node: check `key` equals `val` → `yes_branch`, else `no_branch`.
295    Branch {
296        key: String,
297        val: String,
298        yes_branch: Box<DecisionNode>,
299        no_branch: Box<DecisionNode>,
300    },
301}
302#[allow(dead_code)]
303impl DecisionNode {
304    /// Evaluates the decision tree with the given context.
305    pub fn evaluate(&self, ctx: &std::collections::HashMap<String, String>) -> &str {
306        match self {
307            DecisionNode::Leaf(action) => action.as_str(),
308            DecisionNode::Branch {
309                key,
310                val,
311                yes_branch,
312                no_branch,
313            } => {
314                let actual = ctx.get(key).map(|s| s.as_str()).unwrap_or("");
315                if actual == val.as_str() {
316                    yes_branch.evaluate(ctx)
317                } else {
318                    no_branch.evaluate(ctx)
319                }
320            }
321        }
322    }
323    /// Returns the depth of the decision tree.
324    pub fn depth(&self) -> usize {
325        match self {
326            DecisionNode::Leaf(_) => 0,
327            DecisionNode::Branch {
328                yes_branch,
329                no_branch,
330                ..
331            } => 1 + yes_branch.depth().max(no_branch.depth()),
332        }
333    }
334}
335/// A sparse vector: stores only non-default elements.
336#[allow(dead_code)]
337pub struct SparseVec<T: Default + Clone + PartialEq> {
338    entries: std::collections::HashMap<usize, T>,
339    default_: T,
340    logical_len: usize,
341}
342#[allow(dead_code)]
343impl<T: Default + Clone + PartialEq> SparseVec<T> {
344    /// Creates a new sparse vector with logical length `len`.
345    pub fn new(len: usize) -> Self {
346        Self {
347            entries: std::collections::HashMap::new(),
348            default_: T::default(),
349            logical_len: len,
350        }
351    }
352    /// Sets element at `idx`.
353    pub fn set(&mut self, idx: usize, val: T) {
354        if val == self.default_ {
355            self.entries.remove(&idx);
356        } else {
357            self.entries.insert(idx, val);
358        }
359    }
360    /// Gets element at `idx`.
361    pub fn get(&self, idx: usize) -> &T {
362        self.entries.get(&idx).unwrap_or(&self.default_)
363    }
364    /// Returns the logical length.
365    pub fn len(&self) -> usize {
366        self.logical_len
367    }
368    /// Returns whether the collection is empty.
369    pub fn is_empty(&self) -> bool {
370        self.len() == 0
371    }
372    /// Returns the number of non-default elements.
373    pub fn nnz(&self) -> usize {
374        self.entries.len()
375    }
376}
377/// A hierarchical configuration tree.
378#[allow(dead_code)]
379pub struct ConfigNode {
380    key: String,
381    value: Option<String>,
382    children: Vec<ConfigNode>,
383}
384#[allow(dead_code)]
385impl ConfigNode {
386    /// Creates a leaf config node with a value.
387    pub fn leaf(key: impl Into<String>, value: impl Into<String>) -> Self {
388        Self {
389            key: key.into(),
390            value: Some(value.into()),
391            children: Vec::new(),
392        }
393    }
394    /// Creates a section node with children.
395    pub fn section(key: impl Into<String>) -> Self {
396        Self {
397            key: key.into(),
398            value: None,
399            children: Vec::new(),
400        }
401    }
402    /// Adds a child node.
403    pub fn add_child(&mut self, child: ConfigNode) {
404        self.children.push(child);
405    }
406    /// Returns the key.
407    pub fn key(&self) -> &str {
408        &self.key
409    }
410    /// Returns the value, or `None` for section nodes.
411    pub fn value(&self) -> Option<&str> {
412        self.value.as_deref()
413    }
414    /// Returns the number of children.
415    pub fn num_children(&self) -> usize {
416        self.children.len()
417    }
418    /// Looks up a dot-separated path.
419    pub fn lookup(&self, path: &str) -> Option<&str> {
420        let mut parts = path.splitn(2, '.');
421        let head = parts.next()?;
422        let tail = parts.next();
423        if head != self.key {
424            return None;
425        }
426        match tail {
427            None => self.value.as_deref(),
428            Some(rest) => self.children.iter().find_map(|c| c.lookup_relative(rest)),
429        }
430    }
431    fn lookup_relative(&self, path: &str) -> Option<&str> {
432        let mut parts = path.splitn(2, '.');
433        let head = parts.next()?;
434        let tail = parts.next();
435        if head != self.key {
436            return None;
437        }
438        match tail {
439            None => self.value.as_deref(),
440            Some(rest) => self.children.iter().find_map(|c| c.lookup_relative(rest)),
441        }
442    }
443}
444/// A simple key-value store backed by a sorted Vec for small maps.
445#[allow(dead_code)]
446pub struct SmallMap<K: Ord + Clone, V: Clone> {
447    entries: Vec<(K, V)>,
448}
449#[allow(dead_code)]
450impl<K: Ord + Clone, V: Clone> SmallMap<K, V> {
451    /// Creates a new empty small map.
452    pub fn new() -> Self {
453        Self {
454            entries: Vec::new(),
455        }
456    }
457    /// Inserts or replaces the value for `key`.
458    pub fn insert(&mut self, key: K, val: V) {
459        match self.entries.binary_search_by_key(&&key, |(k, _)| k) {
460            Ok(i) => self.entries[i].1 = val,
461            Err(i) => self.entries.insert(i, (key, val)),
462        }
463    }
464    /// Returns the value for `key`, or `None`.
465    pub fn get(&self, key: &K) -> Option<&V> {
466        self.entries
467            .binary_search_by_key(&key, |(k, _)| k)
468            .ok()
469            .map(|i| &self.entries[i].1)
470    }
471    /// Returns the number of entries.
472    pub fn len(&self) -> usize {
473        self.entries.len()
474    }
475    /// Returns `true` if empty.
476    pub fn is_empty(&self) -> bool {
477        self.entries.is_empty()
478    }
479    /// Returns all keys.
480    pub fn keys(&self) -> Vec<&K> {
481        self.entries.iter().map(|(k, _)| k).collect()
482    }
483    /// Returns all values.
484    pub fn values(&self) -> Vec<&V> {
485        self.entries.iter().map(|(_, v)| v).collect()
486    }
487}
488/// A reusable scratch buffer for path computations.
489#[allow(dead_code)]
490pub struct PathBuf {
491    components: Vec<String>,
492}
493#[allow(dead_code)]
494impl PathBuf {
495    /// Creates a new empty path buffer.
496    pub fn new() -> Self {
497        Self {
498            components: Vec::new(),
499        }
500    }
501    /// Pushes a component.
502    pub fn push(&mut self, comp: impl Into<String>) {
503        self.components.push(comp.into());
504    }
505    /// Pops the last component.
506    pub fn pop(&mut self) {
507        self.components.pop();
508    }
509    /// Returns the current path as a `/`-separated string.
510    pub fn as_str(&self) -> String {
511        self.components.join("/")
512    }
513    /// Returns the depth of the path.
514    pub fn depth(&self) -> usize {
515        self.components.len()
516    }
517    /// Clears the path.
518    pub fn clear(&mut self) {
519        self.components.clear();
520    }
521}
522/// Information about a function parameter for termination checking.
523#[derive(Debug, Clone)]
524pub struct ParamInfo {
525    /// Parameter name
526    pub name: Name,
527    /// Parameter position (0-indexed)
528    pub pos: usize,
529    /// The inductive type this param belongs to (if any)
530    pub inductive_type: Option<Name>,
531}
532/// A non-empty list (at least one element guaranteed).
533#[allow(dead_code)]
534pub struct NonEmptyVec<T> {
535    head: T,
536    tail: Vec<T>,
537}
538#[allow(dead_code)]
539impl<T> NonEmptyVec<T> {
540    /// Creates a non-empty vec with a single element.
541    pub fn singleton(val: T) -> Self {
542        Self {
543            head: val,
544            tail: Vec::new(),
545        }
546    }
547    /// Pushes an element.
548    pub fn push(&mut self, val: T) {
549        self.tail.push(val);
550    }
551    /// Returns a reference to the first element.
552    pub fn first(&self) -> &T {
553        &self.head
554    }
555    /// Returns a reference to the last element.
556    pub fn last(&self) -> &T {
557        self.tail.last().unwrap_or(&self.head)
558    }
559    /// Returns the number of elements.
560    pub fn len(&self) -> usize {
561        1 + self.tail.len()
562    }
563    /// Returns whether the collection is empty.
564    pub fn is_empty(&self) -> bool {
565        self.len() == 0
566    }
567    /// Returns all elements as a Vec.
568    pub fn to_vec(&self) -> Vec<&T> {
569        let mut v = vec![&self.head];
570        v.extend(self.tail.iter());
571        v
572    }
573}
574/// A write-once cell.
575#[allow(dead_code)]
576pub struct WriteOnce<T> {
577    value: std::cell::Cell<Option<T>>,
578}
579#[allow(dead_code)]
580impl<T: Copy> WriteOnce<T> {
581    /// Creates an empty write-once cell.
582    pub fn new() -> Self {
583        Self {
584            value: std::cell::Cell::new(None),
585        }
586    }
587    /// Writes a value.  Returns `false` if already written.
588    pub fn write(&self, val: T) -> bool {
589        if self.value.get().is_some() {
590            return false;
591        }
592        self.value.set(Some(val));
593        true
594    }
595    /// Returns the value if written.
596    pub fn read(&self) -> Option<T> {
597        self.value.get()
598    }
599    /// Returns `true` if the value has been written.
600    pub fn is_written(&self) -> bool {
601        self.value.get().is_some()
602    }
603}
604/// Well-founded relation kind for termination arguments.
605#[allow(dead_code)]
606#[derive(Debug, Clone, PartialEq, Eq)]
607pub enum WfRelationKind {
608    /// Structural recursion on an inductive type.
609    Structural {
610        /// The inductive type being recursed on.
611        inductive_type: Name,
612        /// Index of the parameter being checked.
613        param_index: usize,
614    },
615    /// Recursion on a numeric measure.
616    Measure {
617        /// The measure function.
618        measure_fn: Name,
619    },
620    /// Lexicographic combination of multiple relations.
621    Lexicographic {
622        /// The component relations.
623        components: Vec<WfRelationKind>,
624    },
625    /// Well-founded recursion on natural number subtraction.
626    NatSub,
627    /// Custom user-provided well-founded relation.
628    Custom {
629        /// The custom relation.
630        relation: Name,
631    },
632}
633impl WfRelationKind {
634    /// Check if this is a structural recursion.
635    #[allow(dead_code)]
636    pub fn is_structural(&self) -> bool {
637        matches!(self, WfRelationKind::Structural { .. })
638    }
639    /// Get the depth of a lexicographic argument.
640    #[allow(dead_code)]
641    pub fn lex_depth(&self) -> usize {
642        match self {
643            WfRelationKind::Lexicographic { components } => components.len(),
644            _ => 1,
645        }
646    }
647    /// Return a human-readable description.
648    #[allow(dead_code)]
649    pub fn description(&self) -> String {
650        match self {
651            WfRelationKind::Structural {
652                inductive_type,
653                param_index,
654            } => {
655                format!("structural on {} (param {})", inductive_type, param_index)
656            }
657            WfRelationKind::Measure { measure_fn } => {
658                format!("measure by {}", measure_fn)
659            }
660            WfRelationKind::Lexicographic { components } => {
661                format!("lexicographic ({} components)", components.len())
662            }
663            WfRelationKind::NatSub => "nat subtraction".to_string(),
664            WfRelationKind::Custom { relation } => {
665                format!("custom relation {}", relation)
666            }
667        }
668    }
669}
670/// Result of analyzing a function body for structural recursion.
671#[derive(Debug, Clone)]
672pub struct TerminationResult {
673    /// Which parameter is the decreasing one (if found)
674    pub decreasing_param: Option<usize>,
675    /// All recursive calls found
676    pub recursive_calls: Vec<RecCallInfo>,
677    /// Whether termination is verified
678    pub is_terminating: bool,
679}
680/// Simple trie for efficient string prefix lookup.
681#[allow(dead_code)]
682#[derive(Debug, Clone, Default)]
683pub struct StringTrie {
684    pub(super) children: std::collections::HashMap<char, StringTrie>,
685    is_end: bool,
686    pub(super) value: Option<String>,
687}
688impl StringTrie {
689    /// Create a new empty trie.
690    #[allow(dead_code)]
691    pub fn new() -> Self {
692        Self::default()
693    }
694    /// Insert a string into the trie.
695    #[allow(dead_code)]
696    pub fn insert(&mut self, s: &str) {
697        let mut node = self;
698        for c in s.chars() {
699            node = node.children.entry(c).or_default();
700        }
701        node.is_end = true;
702        node.value = Some(s.to_string());
703    }
704    /// Check if a string is in the trie.
705    #[allow(dead_code)]
706    pub fn contains(&self, s: &str) -> bool {
707        let mut node = self;
708        for c in s.chars() {
709            match node.children.get(&c) {
710                Some(next) => node = next,
711                None => return false,
712            }
713        }
714        node.is_end
715    }
716    /// Find all strings with a given prefix.
717    #[allow(dead_code)]
718    pub fn starts_with(&self, prefix: &str) -> Vec<String> {
719        let mut node = self;
720        for c in prefix.chars() {
721            match node.children.get(&c) {
722                Some(next) => node = next,
723                None => return vec![],
724            }
725        }
726        let mut results = Vec::new();
727        collect_strings(node, &mut results);
728        results
729    }
730    /// Get the number of strings in the trie.
731    #[allow(dead_code)]
732    pub fn len(&self) -> usize {
733        let mut count = if self.is_end { 1 } else { 0 };
734        for child in self.children.values() {
735            count += child.len();
736        }
737        count
738    }
739    /// Check if the trie is empty.
740    #[allow(dead_code)]
741    pub fn is_empty(&self) -> bool {
742        self.len() == 0
743    }
744}
745/// A label set for a graph node.
746#[allow(dead_code)]
747pub struct LabelSet {
748    labels: Vec<String>,
749}
750#[allow(dead_code)]
751impl LabelSet {
752    /// Creates a new empty label set.
753    pub fn new() -> Self {
754        Self { labels: Vec::new() }
755    }
756    /// Adds a label (deduplicates).
757    pub fn add(&mut self, label: impl Into<String>) {
758        let s = label.into();
759        if !self.labels.contains(&s) {
760            self.labels.push(s);
761        }
762    }
763    /// Returns `true` if `label` is present.
764    pub fn has(&self, label: &str) -> bool {
765        self.labels.iter().any(|l| l == label)
766    }
767    /// Returns the count of labels.
768    pub fn count(&self) -> usize {
769        self.labels.len()
770    }
771    /// Returns all labels.
772    pub fn all(&self) -> &[String] {
773        &self.labels
774    }
775}
776/// A counter that can measure elapsed time between snapshots.
777#[allow(dead_code)]
778pub struct Stopwatch {
779    start: std::time::Instant,
780    splits: Vec<f64>,
781}
782#[allow(dead_code)]
783impl Stopwatch {
784    /// Creates and starts a new stopwatch.
785    pub fn start() -> Self {
786        Self {
787            start: std::time::Instant::now(),
788            splits: Vec::new(),
789        }
790    }
791    /// Records a split time (elapsed since start).
792    pub fn split(&mut self) {
793        self.splits.push(self.elapsed_ms());
794    }
795    /// Returns total elapsed milliseconds since start.
796    pub fn elapsed_ms(&self) -> f64 {
797        self.start.elapsed().as_secs_f64() * 1000.0
798    }
799    /// Returns all recorded split times.
800    pub fn splits(&self) -> &[f64] {
801        &self.splits
802    }
803    /// Returns the number of splits.
804    pub fn num_splits(&self) -> usize {
805        self.splits.len()
806    }
807}
808/// Information about a recursive call.
809#[derive(Debug, Clone)]
810pub struct RecCallInfo {
811    /// The function being called
812    pub callee: Name,
813    /// The argument position being passed recursively
814    pub arg_pos: usize,
815    /// The argument expression
816    pub arg: Expr,
817    /// Whether the argument is structurally smaller
818    pub is_decreasing: bool,
819}
820/// Termination checker for recursive definitions.
821pub struct TerminationChecker {
822    /// Names of functions currently being checked (for cycle detection)
823    checking: HashSet<Name>,
824    /// Map from function name to its parameter info
825    param_info: HashMap<Name, Vec<ParamInfo>>,
826    /// Map from function name to its recursive calls
827    call_info: HashMap<Name, Vec<RecCallInfo>>,
828    /// Known structurally smaller expressions
829    /// Maps a variable to the set of expressions known to be smaller
830    smaller: HashMap<Expr, HashSet<Expr>>,
831}
832impl TerminationChecker {
833    /// Create a new termination checker.
834    pub fn new() -> Self {
835        Self {
836            checking: HashSet::new(),
837            param_info: HashMap::new(),
838            call_info: HashMap::new(),
839            smaller: HashMap::new(),
840        }
841    }
842    /// Register parameter info for a function.
843    pub fn register_params(&mut self, name: Name, params: Vec<ParamInfo>) {
844        self.param_info.insert(name, params);
845    }
846    /// Mark an expression as structurally smaller than another.
847    ///
848    /// This is used when we know that `small` is a subterm of `big`,
849    /// e.g., when pattern matching on an inductive type.
850    pub fn add_smaller(&mut self, big: Expr, small: Expr) {
851        self.smaller.entry(big).or_default().insert(small);
852    }
853    /// Check if `small` is known to be structurally smaller than `big`.
854    pub fn is_smaller(&self, big: &Expr, small: &Expr) -> bool {
855        if let Some(smalls) = self.smaller.get(big) {
856            if smalls.contains(small) {
857                return true;
858            }
859            for mid in smalls {
860                if self.is_smaller(mid, small) {
861                    return true;
862                }
863            }
864        }
865        false
866    }
867    /// Check if a recursive definition terminates.
868    ///
869    /// Returns Ok(()) if the definition is structurally decreasing,
870    /// or Err with a message explaining why it might not terminate.
871    pub fn check_terminates(&mut self, name: &Name, body: &Expr) -> Result<(), String> {
872        if self.checking.contains(name) {
873            return Err(format!("Cyclic dependency detected for {}", name));
874        }
875        self.checking.insert(name.clone());
876        let mut calls = Vec::new();
877        self.collect_recursive_calls(name, body, &mut calls, 0)?;
878        self.call_info.insert(name.clone(), calls.clone());
879        if calls.is_empty() {
880            self.checking.remove(name);
881            return Ok(());
882        }
883        let result = self.find_decreasing_param(name, &calls);
884        self.checking.remove(name);
885        if result.is_terminating {
886            Ok(())
887        } else {
888            Err(format!(
889                "Cannot verify termination of '{}': no structurally decreasing argument found",
890                name
891            ))
892        }
893    }
894    /// Check termination for mutual recursion.
895    pub fn check_mutual_terminates(
896        &mut self,
897        names: &[Name],
898        bodies: &[Expr],
899    ) -> Result<(), String> {
900        if names.len() != bodies.len() {
901            return Err("Mismatched names and bodies in mutual recursion".to_string());
902        }
903        for name in names {
904            self.checking.insert(name.clone());
905        }
906        for (name, body) in names.iter().zip(bodies.iter()) {
907            let mut calls = Vec::new();
908            self.collect_recursive_calls_mutual(names, body, &mut calls, 0)?;
909            self.call_info.insert(name.clone(), calls);
910        }
911        for name in names {
912            if let Some(calls) = self.call_info.get(name) {
913                if !calls.is_empty() {
914                    let result = self.find_decreasing_param(name, calls);
915                    if !result.is_terminating {
916                        for n in names {
917                            self.checking.remove(n);
918                        }
919                        return Err(format!(
920                            "Cannot verify termination of '{}' in mutual recursion block",
921                            name
922                        ));
923                    }
924                }
925            }
926        }
927        for name in names {
928            self.checking.remove(name);
929        }
930        Ok(())
931    }
932    /// Collect recursive calls in the body.
933    fn collect_recursive_calls(
934        &self,
935        fname: &Name,
936        expr: &Expr,
937        calls: &mut Vec<RecCallInfo>,
938        depth: usize,
939    ) -> Result<(), String> {
940        if depth > 200 {
941            return Err("Definition too deeply nested".to_string());
942        }
943        match expr {
944            Expr::App(f, a) => {
945                if let Some(call) = self.check_recursive_call(fname, expr) {
946                    calls.push(call);
947                }
948                self.collect_recursive_calls(fname, f, calls, depth + 1)?;
949                self.collect_recursive_calls(fname, a, calls, depth + 1)
950            }
951            Expr::Lam(_, _, ty, body) => {
952                self.collect_recursive_calls(fname, ty, calls, depth + 1)?;
953                self.collect_recursive_calls(fname, body, calls, depth + 1)
954            }
955            Expr::Pi(_, _, ty, body) => {
956                self.collect_recursive_calls(fname, ty, calls, depth + 1)?;
957                self.collect_recursive_calls(fname, body, calls, depth + 1)
958            }
959            Expr::Let(_, ty, val, body) => {
960                self.collect_recursive_calls(fname, ty, calls, depth + 1)?;
961                self.collect_recursive_calls(fname, val, calls, depth + 1)?;
962                self.collect_recursive_calls(fname, body, calls, depth + 1)
963            }
964            _ => Ok(()),
965        }
966    }
967    /// Collect recursive calls for mutual recursion.
968    fn collect_recursive_calls_mutual(
969        &self,
970        fnames: &[Name],
971        expr: &Expr,
972        calls: &mut Vec<RecCallInfo>,
973        depth: usize,
974    ) -> Result<(), String> {
975        if depth > 200 {
976            return Err("Definition too deeply nested".to_string());
977        }
978        match expr {
979            Expr::App(f, a) => {
980                for fname in fnames {
981                    if let Some(call) = self.check_recursive_call(fname, expr) {
982                        calls.push(call);
983                    }
984                }
985                self.collect_recursive_calls_mutual(fnames, f, calls, depth + 1)?;
986                self.collect_recursive_calls_mutual(fnames, a, calls, depth + 1)
987            }
988            Expr::Lam(_, _, ty, body) => {
989                self.collect_recursive_calls_mutual(fnames, ty, calls, depth + 1)?;
990                self.collect_recursive_calls_mutual(fnames, body, calls, depth + 1)
991            }
992            Expr::Pi(_, _, ty, body) => {
993                self.collect_recursive_calls_mutual(fnames, ty, calls, depth + 1)?;
994                self.collect_recursive_calls_mutual(fnames, body, calls, depth + 1)
995            }
996            Expr::Let(_, ty, val, body) => {
997                self.collect_recursive_calls_mutual(fnames, ty, calls, depth + 1)?;
998                self.collect_recursive_calls_mutual(fnames, val, calls, depth + 1)?;
999                self.collect_recursive_calls_mutual(fnames, body, calls, depth + 1)
1000            }
1001            _ => Ok(()),
1002        }
1003    }
1004    /// Check if an application is a recursive call.
1005    fn check_recursive_call(&self, fname: &Name, app: &Expr) -> Option<RecCallInfo> {
1006        let (head, args) = collect_app_args(app);
1007        if let Expr::Const(name, _) = head {
1008            if name == fname {
1009                for (i, arg) in args.iter().enumerate() {
1010                    let is_dec = self.is_structurally_smaller(arg);
1011                    if is_dec {
1012                        return Some(RecCallInfo {
1013                            callee: name.clone(),
1014                            arg_pos: i,
1015                            arg: (*arg).clone(),
1016                            is_decreasing: true,
1017                        });
1018                    }
1019                }
1020                if let Some(first_arg) = args.first() {
1021                    return Some(RecCallInfo {
1022                        callee: name.clone(),
1023                        arg_pos: 0,
1024                        arg: (*first_arg).clone(),
1025                        is_decreasing: false,
1026                    });
1027                }
1028            }
1029        }
1030        None
1031    }
1032    /// Check if an expression is structurally smaller than some parameter.
1033    fn is_structurally_smaller(&self, expr: &Expr) -> bool {
1034        for smalls in self.smaller.values() {
1035            if smalls.contains(expr) {
1036                return true;
1037            }
1038        }
1039        false
1040    }
1041    /// Find a parameter that is decreasing in all recursive calls.
1042    fn find_decreasing_param(&self, _name: &Name, calls: &[RecCallInfo]) -> TerminationResult {
1043        if calls.is_empty() {
1044            return TerminationResult {
1045                decreasing_param: None,
1046                recursive_calls: calls.to_vec(),
1047                is_terminating: true,
1048            };
1049        }
1050        let max_pos = calls.iter().map(|c| c.arg_pos).max().unwrap_or(0);
1051        for pos in 0..=max_pos {
1052            let all_decreasing = calls.iter().all(|c| {
1053                if c.arg_pos == pos {
1054                    c.is_decreasing
1055                } else {
1056                    true
1057                }
1058            });
1059            if all_decreasing && calls.iter().any(|c| c.arg_pos == pos && c.is_decreasing) {
1060                return TerminationResult {
1061                    decreasing_param: Some(pos),
1062                    recursive_calls: calls.to_vec(),
1063                    is_terminating: true,
1064                };
1065            }
1066        }
1067        let all_dec = calls.iter().all(|c| c.is_decreasing);
1068        TerminationResult {
1069            decreasing_param: None,
1070            recursive_calls: calls.to_vec(),
1071            is_terminating: all_dec,
1072        }
1073    }
1074    /// Get the recorded calls for a function.
1075    pub fn get_calls(&self, name: &Name) -> Option<&Vec<RecCallInfo>> {
1076        self.call_info.get(name)
1077    }
1078}
1079/// Represents a rewrite rule `lhs → rhs`.
1080#[allow(dead_code)]
1081#[allow(missing_docs)]
1082pub struct RewriteRule {
1083    /// The name of the rule.
1084    pub name: String,
1085    /// A string representation of the LHS pattern.
1086    pub lhs: String,
1087    /// A string representation of the RHS.
1088    pub rhs: String,
1089    /// Whether this is a conditional rule (has side conditions).
1090    pub conditional: bool,
1091}
1092#[allow(dead_code)]
1093impl RewriteRule {
1094    /// Creates an unconditional rewrite rule.
1095    pub fn unconditional(
1096        name: impl Into<String>,
1097        lhs: impl Into<String>,
1098        rhs: impl Into<String>,
1099    ) -> Self {
1100        Self {
1101            name: name.into(),
1102            lhs: lhs.into(),
1103            rhs: rhs.into(),
1104            conditional: false,
1105        }
1106    }
1107    /// Creates a conditional rewrite rule.
1108    pub fn conditional(
1109        name: impl Into<String>,
1110        lhs: impl Into<String>,
1111        rhs: impl Into<String>,
1112    ) -> Self {
1113        Self {
1114            name: name.into(),
1115            lhs: lhs.into(),
1116            rhs: rhs.into(),
1117            conditional: true,
1118        }
1119    }
1120    /// Returns a textual representation.
1121    pub fn display(&self) -> String {
1122        format!("{}: {} → {}", self.name, self.lhs, self.rhs)
1123    }
1124}
1125/// A type-erased function pointer with arity tracking.
1126#[allow(dead_code)]
1127pub struct RawFnPtr {
1128    /// The raw function pointer (stored as usize for type erasure).
1129    ptr: usize,
1130    arity: usize,
1131    name: String,
1132}
1133#[allow(dead_code)]
1134impl RawFnPtr {
1135    /// Creates a new raw function pointer descriptor.
1136    pub fn new(ptr: usize, arity: usize, name: impl Into<String>) -> Self {
1137        Self {
1138            ptr,
1139            arity,
1140            name: name.into(),
1141        }
1142    }
1143    /// Returns the arity.
1144    pub fn arity(&self) -> usize {
1145        self.arity
1146    }
1147    /// Returns the name.
1148    pub fn name(&self) -> &str {
1149        &self.name
1150    }
1151    /// Returns the raw pointer value.
1152    pub fn raw(&self) -> usize {
1153        self.ptr
1154    }
1155}
1156/// A pair of `StatSummary` values tracking before/after a transformation.
1157#[allow(dead_code)]
1158pub struct TransformStat {
1159    before: StatSummary,
1160    after: StatSummary,
1161}
1162#[allow(dead_code)]
1163impl TransformStat {
1164    /// Creates a new transform stat recorder.
1165    pub fn new() -> Self {
1166        Self {
1167            before: StatSummary::new(),
1168            after: StatSummary::new(),
1169        }
1170    }
1171    /// Records a before value.
1172    pub fn record_before(&mut self, v: f64) {
1173        self.before.record(v);
1174    }
1175    /// Records an after value.
1176    pub fn record_after(&mut self, v: f64) {
1177        self.after.record(v);
1178    }
1179    /// Returns the mean reduction ratio (after/before).
1180    pub fn mean_ratio(&self) -> Option<f64> {
1181        let b = self.before.mean()?;
1182        let a = self.after.mean()?;
1183        if b.abs() < f64::EPSILON {
1184            return None;
1185        }
1186        Some(a / b)
1187    }
1188}
1189/// A flat list of substitution pairs `(from, to)`.
1190#[allow(dead_code)]
1191pub struct FlatSubstitution {
1192    pairs: Vec<(String, String)>,
1193}
1194#[allow(dead_code)]
1195impl FlatSubstitution {
1196    /// Creates an empty substitution.
1197    pub fn new() -> Self {
1198        Self { pairs: Vec::new() }
1199    }
1200    /// Adds a pair.
1201    pub fn add(&mut self, from: impl Into<String>, to: impl Into<String>) {
1202        self.pairs.push((from.into(), to.into()));
1203    }
1204    /// Applies all substitutions to `s` (leftmost-first order).
1205    pub fn apply(&self, s: &str) -> String {
1206        let mut result = s.to_string();
1207        for (from, to) in &self.pairs {
1208            result = result.replace(from.as_str(), to.as_str());
1209        }
1210        result
1211    }
1212    /// Returns the number of pairs.
1213    pub fn len(&self) -> usize {
1214        self.pairs.len()
1215    }
1216    /// Returns `true` if empty.
1217    pub fn is_empty(&self) -> bool {
1218        self.pairs.is_empty()
1219    }
1220}
1221/// A pool of reusable string buffers.
1222#[allow(dead_code)]
1223pub struct StringPool {
1224    free: Vec<String>,
1225}
1226#[allow(dead_code)]
1227impl StringPool {
1228    /// Creates a new empty string pool.
1229    pub fn new() -> Self {
1230        Self { free: Vec::new() }
1231    }
1232    /// Takes a string from the pool (may be empty).
1233    pub fn take(&mut self) -> String {
1234        self.free.pop().unwrap_or_default()
1235    }
1236    /// Returns a string to the pool.
1237    pub fn give(&mut self, mut s: String) {
1238        s.clear();
1239        self.free.push(s);
1240    }
1241    /// Returns the number of free strings in the pool.
1242    pub fn free_count(&self) -> usize {
1243        self.free.len()
1244    }
1245}
1246/// A trie-based prefix counter.
1247#[allow(dead_code)]
1248pub struct PrefixCounter {
1249    children: std::collections::HashMap<char, PrefixCounter>,
1250    count: usize,
1251}
1252#[allow(dead_code)]
1253impl PrefixCounter {
1254    /// Creates an empty prefix counter.
1255    pub fn new() -> Self {
1256        Self {
1257            children: std::collections::HashMap::new(),
1258            count: 0,
1259        }
1260    }
1261    /// Records a string.
1262    pub fn record(&mut self, s: &str) {
1263        self.count += 1;
1264        let mut node = self;
1265        for c in s.chars() {
1266            node = node.children.entry(c).or_default();
1267            node.count += 1;
1268        }
1269    }
1270    /// Returns how many strings have been recorded that start with `prefix`.
1271    pub fn count_with_prefix(&self, prefix: &str) -> usize {
1272        let mut node = self;
1273        for c in prefix.chars() {
1274            match node.children.get(&c) {
1275                Some(n) => node = n,
1276                None => return 0,
1277            }
1278        }
1279        node.count
1280    }
1281}
1282/// A generic counter that tracks min/max/sum for statistical summaries.
1283#[allow(dead_code)]
1284pub struct StatSummary {
1285    count: u64,
1286    sum: f64,
1287    min: f64,
1288    max: f64,
1289}
1290#[allow(dead_code)]
1291impl StatSummary {
1292    /// Creates an empty summary.
1293    pub fn new() -> Self {
1294        Self {
1295            count: 0,
1296            sum: 0.0,
1297            min: f64::INFINITY,
1298            max: f64::NEG_INFINITY,
1299        }
1300    }
1301    /// Records a sample.
1302    pub fn record(&mut self, val: f64) {
1303        self.count += 1;
1304        self.sum += val;
1305        if val < self.min {
1306            self.min = val;
1307        }
1308        if val > self.max {
1309            self.max = val;
1310        }
1311    }
1312    /// Returns the mean, or `None` if no samples.
1313    pub fn mean(&self) -> Option<f64> {
1314        if self.count == 0 {
1315            None
1316        } else {
1317            Some(self.sum / self.count as f64)
1318        }
1319    }
1320    /// Returns the minimum, or `None` if no samples.
1321    pub fn min(&self) -> Option<f64> {
1322        if self.count == 0 {
1323            None
1324        } else {
1325            Some(self.min)
1326        }
1327    }
1328    /// Returns the maximum, or `None` if no samples.
1329    pub fn max(&self) -> Option<f64> {
1330        if self.count == 0 {
1331            None
1332        } else {
1333            Some(self.max)
1334        }
1335    }
1336    /// Returns the count of recorded samples.
1337    pub fn count(&self) -> u64 {
1338        self.count
1339    }
1340}
1341/// A window iterator that yields overlapping windows of size `n`.
1342#[allow(dead_code)]
1343pub struct WindowIterator<'a, T> {
1344    pub(super) data: &'a [T],
1345    pub(super) pos: usize,
1346    pub(super) window: usize,
1347}
1348#[allow(dead_code)]
1349impl<'a, T> WindowIterator<'a, T> {
1350    /// Creates a new window iterator.
1351    pub fn new(data: &'a [T], window: usize) -> Self {
1352        Self {
1353            data,
1354            pos: 0,
1355            window,
1356        }
1357    }
1358}
1359/// A token bucket rate limiter.
1360#[allow(dead_code)]
1361pub struct TokenBucket {
1362    capacity: u64,
1363    tokens: u64,
1364    refill_per_ms: u64,
1365    last_refill: std::time::Instant,
1366}
1367#[allow(dead_code)]
1368impl TokenBucket {
1369    /// Creates a new token bucket.
1370    pub fn new(capacity: u64, refill_per_ms: u64) -> Self {
1371        Self {
1372            capacity,
1373            tokens: capacity,
1374            refill_per_ms,
1375            last_refill: std::time::Instant::now(),
1376        }
1377    }
1378    /// Attempts to consume `n` tokens.  Returns `true` on success.
1379    pub fn try_consume(&mut self, n: u64) -> bool {
1380        self.refill();
1381        if self.tokens >= n {
1382            self.tokens -= n;
1383            true
1384        } else {
1385            false
1386        }
1387    }
1388    fn refill(&mut self) {
1389        let now = std::time::Instant::now();
1390        let elapsed_ms = now.duration_since(self.last_refill).as_millis() as u64;
1391        if elapsed_ms > 0 {
1392            let new_tokens = elapsed_ms * self.refill_per_ms;
1393            self.tokens = (self.tokens + new_tokens).min(self.capacity);
1394            self.last_refill = now;
1395        }
1396    }
1397    /// Returns the number of currently available tokens.
1398    pub fn available(&self) -> u64 {
1399        self.tokens
1400    }
1401    /// Returns the bucket capacity.
1402    pub fn capacity(&self) -> u64 {
1403        self.capacity
1404    }
1405}
1406/// Result of a termination check with detailed information.
1407#[allow(dead_code)]
1408#[derive(Debug, Clone)]
1409pub struct DetailedTerminationResult {
1410    /// Whether termination was verified.
1411    pub terminates: bool,
1412    /// The well-founded relation used (if termination was verified).
1413    pub wf_relation: Option<WfRelationKind>,
1414    /// The function name.
1415    pub function_name: Name,
1416    /// Explanation of why termination was/wasn't verified.
1417    pub explanation: String,
1418    /// All recursive calls found.
1419    pub recursive_calls: Vec<RecCallInfo>,
1420}
1421impl DetailedTerminationResult {
1422    /// Create a termination result for a non-recursive function.
1423    #[allow(dead_code)]
1424    pub fn non_recursive(name: Name) -> Self {
1425        Self {
1426            terminates: true,
1427            wf_relation: None,
1428            function_name: name,
1429            explanation: "No recursive calls; trivially terminating.".to_string(),
1430            recursive_calls: vec![],
1431        }
1432    }
1433    /// Create a successful termination result.
1434    #[allow(dead_code)]
1435    pub fn success(name: Name, wf: WfRelationKind, calls: Vec<RecCallInfo>) -> Self {
1436        let explanation = format!("Termination verified via {}.", wf.description());
1437        Self {
1438            terminates: true,
1439            wf_relation: Some(wf),
1440            function_name: name,
1441            explanation,
1442            recursive_calls: calls,
1443        }
1444    }
1445    /// Create a failure result.
1446    #[allow(dead_code)]
1447    pub fn failure(name: Name, calls: Vec<RecCallInfo>, reason: impl Into<String>) -> Self {
1448        Self {
1449            terminates: false,
1450            wf_relation: None,
1451            function_name: name,
1452            explanation: reason.into(),
1453            recursive_calls: calls,
1454        }
1455    }
1456}
1457/// A simple mutable key-value store for test fixtures.
1458#[allow(dead_code)]
1459pub struct Fixture {
1460    data: std::collections::HashMap<String, String>,
1461}
1462#[allow(dead_code)]
1463impl Fixture {
1464    /// Creates an empty fixture.
1465    pub fn new() -> Self {
1466        Self {
1467            data: std::collections::HashMap::new(),
1468        }
1469    }
1470    /// Sets a key.
1471    pub fn set(&mut self, key: impl Into<String>, val: impl Into<String>) {
1472        self.data.insert(key.into(), val.into());
1473    }
1474    /// Gets a value.
1475    pub fn get(&self, key: &str) -> Option<&str> {
1476        self.data.get(key).map(|s| s.as_str())
1477    }
1478    /// Returns the number of entries.
1479    pub fn len(&self) -> usize {
1480        self.data.len()
1481    }
1482    /// Returns whether the collection is empty.
1483    pub fn is_empty(&self) -> bool {
1484        self.len() == 0
1485    }
1486}
1487/// A simple stack-based calculator for arithmetic expressions.
1488#[allow(dead_code)]
1489pub struct StackCalc {
1490    stack: Vec<i64>,
1491}
1492#[allow(dead_code)]
1493impl StackCalc {
1494    /// Creates a new empty calculator.
1495    pub fn new() -> Self {
1496        Self { stack: Vec::new() }
1497    }
1498    /// Pushes an integer literal.
1499    pub fn push(&mut self, n: i64) {
1500        self.stack.push(n);
1501    }
1502    /// Adds the top two values.  Panics if fewer than two values.
1503    pub fn add(&mut self) {
1504        let b = self
1505            .stack
1506            .pop()
1507            .expect("stack must have at least two values for add");
1508        let a = self
1509            .stack
1510            .pop()
1511            .expect("stack must have at least two values for add");
1512        self.stack.push(a + b);
1513    }
1514    /// Subtracts top from second.
1515    pub fn sub(&mut self) {
1516        let b = self
1517            .stack
1518            .pop()
1519            .expect("stack must have at least two values for sub");
1520        let a = self
1521            .stack
1522            .pop()
1523            .expect("stack must have at least two values for sub");
1524        self.stack.push(a - b);
1525    }
1526    /// Multiplies the top two values.
1527    pub fn mul(&mut self) {
1528        let b = self
1529            .stack
1530            .pop()
1531            .expect("stack must have at least two values for mul");
1532        let a = self
1533            .stack
1534            .pop()
1535            .expect("stack must have at least two values for mul");
1536        self.stack.push(a * b);
1537    }
1538    /// Peeks the top value.
1539    pub fn peek(&self) -> Option<i64> {
1540        self.stack.last().copied()
1541    }
1542    /// Returns the stack depth.
1543    pub fn depth(&self) -> usize {
1544        self.stack.len()
1545    }
1546}
1547/// A tagged union for representing a simple two-case discriminated union.
1548#[allow(dead_code)]
1549pub enum Either2<A, B> {
1550    /// The first alternative.
1551    First(A),
1552    /// The second alternative.
1553    Second(B),
1554}
1555#[allow(dead_code)]
1556impl<A, B> Either2<A, B> {
1557    /// Returns `true` if this is the first alternative.
1558    pub fn is_first(&self) -> bool {
1559        matches!(self, Either2::First(_))
1560    }
1561    /// Returns `true` if this is the second alternative.
1562    pub fn is_second(&self) -> bool {
1563        matches!(self, Either2::Second(_))
1564    }
1565    /// Returns the first value if present.
1566    pub fn first(self) -> Option<A> {
1567        match self {
1568            Either2::First(a) => Some(a),
1569            _ => None,
1570        }
1571    }
1572    /// Returns the second value if present.
1573    pub fn second(self) -> Option<B> {
1574        match self {
1575            Either2::Second(b) => Some(b),
1576            _ => None,
1577        }
1578    }
1579    /// Maps over the first alternative.
1580    pub fn map_first<C, F: FnOnce(A) -> C>(self, f: F) -> Either2<C, B> {
1581        match self {
1582            Either2::First(a) => Either2::First(f(a)),
1583            Either2::Second(b) => Either2::Second(b),
1584        }
1585    }
1586}
1587/// A simple ordered index mapping names to integer IDs.
1588#[allow(dead_code)]
1589#[derive(Debug, Clone, Default)]
1590pub struct NameIndex {
1591    names: Vec<String>,
1592    index: std::collections::HashMap<String, usize>,
1593}
1594impl NameIndex {
1595    /// Create a new empty name index.
1596    #[allow(dead_code)]
1597    pub fn new() -> Self {
1598        Self::default()
1599    }
1600    /// Insert a name, returning its ID.
1601    /// If the name is already present, returns the existing ID.
1602    #[allow(dead_code)]
1603    pub fn insert(&mut self, name: impl Into<String>) -> usize {
1604        let name = name.into();
1605        if let Some(&id) = self.index.get(&name) {
1606            return id;
1607        }
1608        let id = self.names.len();
1609        self.index.insert(name.clone(), id);
1610        self.names.push(name);
1611        id
1612    }
1613    /// Get the ID for a name, if it exists.
1614    #[allow(dead_code)]
1615    pub fn get_id(&self, name: &str) -> Option<usize> {
1616        self.index.get(name).copied()
1617    }
1618    /// Get the name for an ID.
1619    #[allow(dead_code)]
1620    pub fn get_name(&self, id: usize) -> Option<&str> {
1621        self.names.get(id).map(|s| s.as_str())
1622    }
1623    /// Get the number of names in the index.
1624    #[allow(dead_code)]
1625    pub fn len(&self) -> usize {
1626        self.names.len()
1627    }
1628    /// Check if the index is empty.
1629    #[allow(dead_code)]
1630    pub fn is_empty(&self) -> bool {
1631        self.names.is_empty()
1632    }
1633    /// Get all names in insertion order.
1634    #[allow(dead_code)]
1635    pub fn all_names(&self) -> &[String] {
1636        &self.names
1637    }
1638}
1639/// A set of rewrite rules.
1640#[allow(dead_code)]
1641pub struct RewriteRuleSet {
1642    rules: Vec<RewriteRule>,
1643}
1644#[allow(dead_code)]
1645impl RewriteRuleSet {
1646    /// Creates an empty rule set.
1647    pub fn new() -> Self {
1648        Self { rules: Vec::new() }
1649    }
1650    /// Adds a rule.
1651    pub fn add(&mut self, rule: RewriteRule) {
1652        self.rules.push(rule);
1653    }
1654    /// Returns the number of rules.
1655    pub fn len(&self) -> usize {
1656        self.rules.len()
1657    }
1658    /// Returns `true` if the set is empty.
1659    pub fn is_empty(&self) -> bool {
1660        self.rules.is_empty()
1661    }
1662    /// Returns all conditional rules.
1663    pub fn conditional_rules(&self) -> Vec<&RewriteRule> {
1664        self.rules.iter().filter(|r| r.conditional).collect()
1665    }
1666    /// Returns all unconditional rules.
1667    pub fn unconditional_rules(&self) -> Vec<&RewriteRule> {
1668        self.rules.iter().filter(|r| !r.conditional).collect()
1669    }
1670    /// Looks up a rule by name.
1671    pub fn get(&self, name: &str) -> Option<&RewriteRule> {
1672        self.rules.iter().find(|r| r.name == name)
1673    }
1674}
1675/// A cache of termination results for batch checking.
1676#[allow(dead_code)]
1677#[derive(Debug, Clone, Default)]
1678pub struct TerminationCache {
1679    results: HashMap<Name, bool>,
1680}
1681impl TerminationCache {
1682    /// Create a new cache.
1683    #[allow(dead_code)]
1684    pub fn new() -> Self {
1685        Self::default()
1686    }
1687    /// Record that a function terminates.
1688    #[allow(dead_code)]
1689    pub fn mark_terminating(&mut self, name: Name) {
1690        self.results.insert(name, true);
1691    }
1692    /// Record that a function may not terminate.
1693    #[allow(dead_code)]
1694    pub fn mark_nonterminating(&mut self, name: Name) {
1695        self.results.insert(name, false);
1696    }
1697    /// Query if a function is known to terminate.
1698    #[allow(dead_code)]
1699    pub fn is_known_terminating(&self, name: &Name) -> Option<bool> {
1700        self.results.get(name).copied()
1701    }
1702    /// Get the number of cached results.
1703    #[allow(dead_code)]
1704    pub fn len(&self) -> usize {
1705        self.results.len()
1706    }
1707    /// Check if the cache is empty.
1708    #[allow(dead_code)]
1709    pub fn is_empty(&self) -> bool {
1710        self.results.is_empty()
1711    }
1712    /// Clear the cache.
1713    #[allow(dead_code)]
1714    pub fn clear(&mut self) {
1715        self.results.clear();
1716    }
1717}
1718/// A mutable reference stack for tracking the current "focus" in a tree traversal.
1719#[allow(dead_code)]
1720pub struct FocusStack<T> {
1721    items: Vec<T>,
1722}
1723#[allow(dead_code)]
1724impl<T> FocusStack<T> {
1725    /// Creates an empty focus stack.
1726    pub fn new() -> Self {
1727        Self { items: Vec::new() }
1728    }
1729    /// Focuses on `item`.
1730    pub fn focus(&mut self, item: T) {
1731        self.items.push(item);
1732    }
1733    /// Blurs (pops) the current focus.
1734    pub fn blur(&mut self) -> Option<T> {
1735        self.items.pop()
1736    }
1737    /// Returns the current focus, or `None`.
1738    pub fn current(&self) -> Option<&T> {
1739        self.items.last()
1740    }
1741    /// Returns the focus depth.
1742    pub fn depth(&self) -> usize {
1743        self.items.len()
1744    }
1745    /// Returns `true` if there is no current focus.
1746    pub fn is_empty(&self) -> bool {
1747        self.items.is_empty()
1748    }
1749}