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