Skip to main content

oxilean_kernel/env/
types.rs

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