Skip to main content

oxilean_kernel/typeclasses/
functions.rs

1//! Auto-generated module
2//!
3//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)
4
5use crate::Node;
6use crate::{Expr, Name};
7use std::collections::HashMap;
8use std::rc::Rc;
9
10use super::types::{
11    ClassEdge, ConfigNode, DecisionNode, Either2, FlatSubstitution, FocusStack, Instance,
12    InstanceImpl, InstancePriority, InstanceSearchResult, LabelSet, LayeredTypeClassRegistry,
13    Method, MethodImpl, NonEmptyVec, NullResolver, PathBuf, RewriteRule, RewriteRuleSet, SimpleDag,
14    SlidingSum, SmallMap, SparseVec, StackCalc, StatSummary, Stopwatch, StringPool, TokenBucket,
15    TransformStat, TransitiveClosure, TypeClass, TypeClassRegistry, TypeClassStats,
16    VersionedRecord, WindowIterator, WriteOnce,
17};
18
19/// Check whether two type expressions are compatible for instance matching.
20///
21/// `needle` is the queried type; `haystack` is the registered instance type.
22/// Returns `true` if `needle` matches `haystack`, treating free/bound
23/// variables in `haystack` as wildcards (polymorphic instance parameters).
24pub fn instances_match(needle: &Expr, haystack: &Expr) -> bool {
25    match (needle, haystack) {
26        _ if needle == haystack => true,
27        (_, Expr::BVar(_)) | (_, Expr::FVar(_)) => true,
28        (Expr::Sort(_), Expr::Sort(_)) => true,
29        (Expr::Const(n1, _), Expr::Const(n2, _)) => n1 == n2,
30        (Expr::App(f1, a1), Expr::App(f2, a2)) => {
31            instances_match(f1, f2) && instances_match(a1, a2)
32        }
33        (Expr::Pi(_, _, d1, c1), Expr::Pi(_, _, d2, c2)) => {
34            instances_match(d1, d2) && instances_match(c1, c2)
35        }
36        (Expr::Lam(_, _, d1, b1), Expr::Lam(_, _, d2, b2)) => {
37            instances_match(d1, d2) && instances_match(b1, b2)
38        }
39        _ => false,
40    }
41}
42/// Check whether an expression is a type class constraint application.
43///
44/// Returns `true` if the head of the expression is a registered class name.
45pub fn is_class_constraint(expr: &Expr, registry: &TypeClassRegistry) -> bool {
46    class_name_of_constraint(expr)
47        .map(|n| registry.is_class(&n))
48        .unwrap_or(false)
49}
50/// Extract the class name from a constraint expression.
51///
52/// Given `Add Nat` returns `Some("Add")`; given a bare `Nat` returns `None`.
53pub fn class_name_of_constraint(expr: &Expr) -> Option<Name> {
54    match expr {
55        Expr::Const(name, _) => Some(name.clone()),
56        Expr::App(f, _) => class_name_of_constraint(f),
57        _ => None,
58    }
59}
60/// Build the projection term for the n-th method of a class.
61///
62/// The projection is an application of `ClassName.methodName`.
63pub fn build_method_projection(class: &Name, method: &Name, _index: usize) -> Expr {
64    let proj_name = class.clone().append_str(method.to_string());
65    Expr::Const(proj_name, vec![])
66}
67/// Register the built-in `Inhabited` class in the given registry.
68pub fn register_inhabited(registry: &mut TypeClassRegistry) {
69    use crate::Level;
70    let name = Name::str("Inhabited");
71    let ty = Expr::Sort(Level::succ(Level::zero()));
72    let mut cls = TypeClass::new(name.clone(), vec![Name::str("α")], ty);
73    cls.add_method(Method::new(Name::str("default"), Expr::BVar(0), 0));
74    registry.register_class(cls);
75}
76/// Register the built-in `Add` class in the given registry.
77pub fn register_add(registry: &mut TypeClassRegistry) {
78    use crate::Level;
79    let name = Name::str("Add");
80    let ty = Expr::Sort(Level::succ(Level::zero()));
81    let mut cls = TypeClass::new(name.clone(), vec![Name::str("α")], ty);
82    let add_ty = Expr::Pi(
83        crate::BinderInfo::Default,
84        Name::str("a"),
85        Node::new(Expr::BVar(0)),
86        Node::new(Expr::Pi(
87            crate::BinderInfo::Default,
88            Name::str("b"),
89            Node::new(Expr::BVar(1)),
90            Node::new(Expr::BVar(2)),
91        )),
92    );
93    cls.add_method(Method::new(Name::str("add"), add_ty, 0));
94    registry.register_class(cls);
95}
96/// Register the built-in `Mul` class in the given registry.
97pub fn register_mul(registry: &mut TypeClassRegistry) {
98    use crate::Level;
99    let name = Name::str("Mul");
100    let ty = Expr::Sort(Level::succ(Level::zero()));
101    let mut cls = TypeClass::new(name.clone(), vec![Name::str("α")], ty);
102    let mul_ty = Expr::Pi(
103        crate::BinderInfo::Default,
104        Name::str("a"),
105        Node::new(Expr::BVar(0)),
106        Node::new(Expr::Pi(
107            crate::BinderInfo::Default,
108            Name::str("b"),
109            Node::new(Expr::BVar(1)),
110            Node::new(Expr::BVar(2)),
111        )),
112    );
113    cls.add_method(Method::new(Name::str("mul"), mul_ty, 0));
114    registry.register_class(cls);
115}
116/// Register the `HEq` (heterogeneous equality) class placeholder.
117pub fn register_heq(registry: &mut TypeClassRegistry) {
118    use crate::Level;
119    let name = Name::str("HEq");
120    let ty = Expr::Sort(Level::zero());
121    let cls = TypeClass::new(name, vec![Name::str("α"), Name::str("β")], ty).mark_prop();
122    registry.register_class(cls);
123}
124/// Register a simple zero-method marker class (like `Nonempty`).
125pub fn register_marker(registry: &mut TypeClassRegistry, class_name: &str) {
126    use crate::Level;
127    let name = Name::str(class_name);
128    let ty = Expr::Sort(Level::succ(Level::zero()));
129    let cls = TypeClass::new(name, vec![Name::str("α")], ty);
130    registry.register_class(cls);
131}
132/// Build a default registry with common built-in classes.
133pub fn default_registry() -> TypeClassRegistry {
134    let mut reg = TypeClassRegistry::new();
135    register_inhabited(&mut reg);
136    register_add(&mut reg);
137    register_mul(&mut reg);
138    register_heq(&mut reg);
139    register_marker(&mut reg, "Nonempty");
140    register_marker(&mut reg, "Decidable");
141    register_marker(&mut reg, "DecidableEq");
142    register_marker(&mut reg, "Fintype");
143    reg
144}
145/// Check whether the given class name is a "pure Prop" class.
146pub fn is_prop_class(name: &Name, registry: &TypeClassRegistry) -> bool {
147    registry.get_class(name).map(|c| c.is_prop).unwrap_or(false)
148}
149/// Return all methods for a class, or an empty slice if the class is unknown.
150pub fn methods_of(class: &Name, registry: &TypeClassRegistry) -> Vec<Method> {
151    registry
152        .get_class(class)
153        .map(|c| c.methods.clone())
154        .unwrap_or_default()
155}
156/// Check if an instance covers (implements) all required methods.
157pub fn instance_is_complete(instance: &Instance, registry: &TypeClassRegistry) -> bool {
158    let class_name = &instance.class;
159    match registry.get_class(class_name) {
160        None => false,
161        Some(cls) => instance.implements_all(cls),
162    }
163}
164/// Get all super-class names required by a class, transitively.
165pub fn transitive_supers(class: &Name, registry: &TypeClassRegistry) -> Vec<Name> {
166    let mut result = Vec::new();
167    let mut work_list = vec![class.clone()];
168    while let Some(c) = work_list.pop() {
169        if let Some(cls) = registry.get_class(&c) {
170            for sup in &cls.super_classes {
171                if !result.contains(sup) {
172                    result.push(sup.clone());
173                    work_list.push(sup.clone());
174                }
175            }
176        }
177    }
178    result
179}
180/// Merge two registries together (second registry overrides on conflicts).
181pub fn merge_registries(base: TypeClassRegistry, overlay: TypeClassRegistry) -> TypeClassRegistry {
182    let mut result = base;
183    for (_, cls) in overlay.classes {
184        result.register_class(cls);
185    }
186    for inst in overlay.instances {
187        result.register_instance(inst);
188    }
189    result
190}
191/// Search for a method implementation across all matching instances.
192pub fn find_method_impl(
193    class: &Name,
194    ty: &Expr,
195    method: &str,
196    registry: &TypeClassRegistry,
197) -> Option<Expr> {
198    let instances = registry.find_instances(class, ty);
199    for inst in instances {
200        if let Some(impl_expr) = inst.get_method_impl(method) {
201            return Some(impl_expr.clone());
202        }
203    }
204    None
205}
206/// Count the total number of method implementations across all instances.
207pub fn total_method_impls(registry: &TypeClassRegistry) -> usize {
208    registry.instances.iter().map(|i| i.methods.len()).sum()
209}
210/// Print a human-readable summary of all classes and instances.
211pub fn describe_registry(registry: &TypeClassRegistry) -> String {
212    let mut lines = Vec::new();
213    lines.push("=== Type Class Registry ===".to_string());
214    let mut class_names: Vec<&String> = registry.classes.keys().collect();
215    class_names.sort();
216    for name in class_names {
217        let cls = &registry.classes[name];
218        lines.push(format!("class {} ({} method(s))", name, cls.method_count()));
219        for m in &cls.methods {
220            lines.push(format!("  method: {}", m.name));
221        }
222    }
223    lines.push(format!("--- {} instance(s) ---", registry.instance_count()));
224    for inst in &registry.instances {
225        let label = inst
226            .instance_name
227            .as_ref()
228            .map(|n| n.to_string())
229            .unwrap_or_else(|| "<anon>".to_string());
230        lines.push(format!(
231            "  instance {} : {} (priority {})",
232            label, inst.class, inst.priority
233        ));
234    }
235    lines.join("\n")
236}
237/// Check whether two class names are the same.
238pub fn classes_equal(a: &Name, b: &Name) -> bool {
239    a == b
240}
241/// Check whether an instance has priority strictly higher than another.
242pub fn has_higher_priority(a: &Instance, b: &Instance) -> bool {
243    a.priority < b.priority
244}
245#[cfg(test)]
246mod tests {
247    use super::*;
248    use crate::Level;
249    fn mk_sort() -> Expr {
250        Expr::Sort(Level::zero())
251    }
252    fn mk_const(s: &str) -> Expr {
253        Expr::Const(Name::str(s), vec![])
254    }
255    fn add_class() -> TypeClass {
256        let mut cls = TypeClass::new(Name::str("Add"), vec![Name::str("α")], mk_sort());
257        cls.add_method(Method::new(Name::str("add"), mk_sort(), 0));
258        cls
259    }
260    fn nat_instance() -> Instance {
261        Instance::new(Name::str("Add"), mk_const("Nat"))
262    }
263    #[test]
264    fn test_register_and_find_class() {
265        let mut reg = TypeClassRegistry::new();
266        reg.register_class(add_class());
267        assert!(reg.is_class(&Name::str("Add")));
268        assert!(!reg.is_class(&Name::str("Mul")));
269        assert_eq!(reg.class_count(), 1);
270    }
271    #[test]
272    fn test_class_method_lookup() {
273        let cls = add_class();
274        assert!(cls.find_method(&Name::str("add")).is_some());
275        assert!(cls.find_method(&Name::str("mul")).is_none());
276        assert_eq!(cls.method_count(), 1);
277    }
278    #[test]
279    fn test_instance_registration() {
280        let mut reg = TypeClassRegistry::new();
281        reg.register_class(add_class());
282        reg.register_instance(nat_instance());
283        assert_eq!(reg.instance_count(), 1);
284    }
285    #[test]
286    fn test_find_instances() {
287        let mut reg = TypeClassRegistry::new();
288        reg.register_class(add_class());
289        reg.register_instance(nat_instance());
290        let found = reg.find_instances(&Name::str("Add"), &mk_const("Nat"));
291        assert_eq!(found.len(), 1);
292        let none = reg.find_instances(&Name::str("Add"), &mk_const("Int"));
293        assert!(none.is_empty());
294    }
295    #[test]
296    fn test_find_best_instance_unique() {
297        let mut reg = TypeClassRegistry::new();
298        reg.register_class(add_class());
299        reg.register_instance(nat_instance());
300        let result = reg.find_best_instance(&Name::str("Add"), &mk_const("Nat"));
301        assert!(result.is_found());
302    }
303    #[test]
304    fn test_find_best_instance_not_found() {
305        let mut reg = TypeClassRegistry::new();
306        reg.register_class(add_class());
307        let result = reg.find_best_instance(&Name::str("Add"), &mk_const("Nat"));
308        assert!(matches!(result, InstanceSearchResult::NotFound));
309    }
310    #[test]
311    fn test_priority_ordering() {
312        let mut reg = TypeClassRegistry::new();
313        reg.register_class(add_class());
314        let low = Instance::new(Name::str("Add"), mk_const("Nat")).with_priority(200);
315        let high = Instance::new(Name::str("Add"), mk_const("Nat")).with_priority(50);
316        reg.register_instance(low);
317        reg.register_instance(high);
318        let result = reg.find_best_instance(&Name::str("Add"), &mk_const("Nat"));
319        if let InstanceSearchResult::Found(inst) = result {
320            assert_eq!(inst.priority, 50);
321        } else {
322            panic!("Expected Found");
323        }
324    }
325    #[test]
326    fn test_ambiguous_instances() {
327        let mut reg = TypeClassRegistry::new();
328        reg.register_class(add_class());
329        let a = Instance::new(Name::str("Add"), mk_const("Nat")).with_priority(100);
330        let b = Instance::new(Name::str("Add"), mk_const("Nat")).with_priority(100);
331        reg.register_instance(a);
332        reg.register_instance(b);
333        let result = reg.find_best_instance(&Name::str("Add"), &mk_const("Nat"));
334        assert!(result.is_ambiguous());
335    }
336    #[test]
337    fn test_local_instance_clear() {
338        let mut reg = TypeClassRegistry::new();
339        reg.register_class(add_class());
340        let local = nat_instance().as_local();
341        let global = Instance::named(Name::str("Add"), mk_const("Nat"), Name::str("natAdd"));
342        reg.register_instance(local);
343        reg.register_instance(global);
344        assert_eq!(reg.instance_count(), 2);
345        reg.clear_local_instances();
346        assert_eq!(reg.instance_count(), 1);
347    }
348    #[test]
349    fn test_class_name_of_constraint() {
350        let c = mk_const("Add");
351        assert_eq!(class_name_of_constraint(&c), Some(Name::str("Add")));
352        let app = Expr::App(Node::new(mk_const("Add")), Node::new(mk_const("Nat")));
353        assert_eq!(class_name_of_constraint(&app), Some(Name::str("Add")));
354        assert_eq!(class_name_of_constraint(&Expr::BVar(0)), None);
355    }
356    #[test]
357    fn test_default_registry() {
358        let reg = default_registry();
359        assert!(reg.is_class(&Name::str("Inhabited")));
360        assert!(reg.is_class(&Name::str("Add")));
361        assert!(reg.is_class(&Name::str("Mul")));
362        assert!(reg.is_class(&Name::str("Decidable")));
363    }
364    #[test]
365    fn test_transitive_supers() {
366        let mut reg = TypeClassRegistry::new();
367        let cls_a = TypeClass::new(Name::str("A"), vec![], mk_sort());
368        let mut cls_b = TypeClass::new(Name::str("B"), vec![], mk_sort());
369        cls_b.add_super(Name::str("A"));
370        let mut cls_c = TypeClass::new(Name::str("C"), vec![], mk_sort());
371        cls_c.add_super(Name::str("B"));
372        reg.register_class(cls_a);
373        reg.register_class(cls_b);
374        reg.register_class(cls_c);
375        let supers = transitive_supers(&Name::str("C"), &reg);
376        assert!(supers.contains(&Name::str("B")));
377        assert!(supers.contains(&Name::str("A")));
378    }
379    #[test]
380    fn test_method_projection() {
381        let mut reg = TypeClassRegistry::new();
382        reg.register_class(add_class());
383        let proj = reg.method_projection(&Name::str("Add"), &Name::str("add"));
384        assert!(proj.is_some());
385    }
386    #[test]
387    fn test_instance_method_impl() {
388        let mut inst = nat_instance();
389        inst.add_method_impl("add", mk_const("Nat.add"));
390        assert_eq!(inst.get_method_impl("add"), Some(&mk_const("Nat.add")));
391        assert_eq!(inst.implemented_count(), 1);
392    }
393    #[test]
394    fn test_merge_registries() {
395        let mut reg1 = TypeClassRegistry::new();
396        reg1.register_class(add_class());
397        let mut reg2 = TypeClassRegistry::new();
398        reg2.register_instance(nat_instance());
399        let merged = merge_registries(reg1, reg2);
400        assert_eq!(merged.class_count(), 1);
401        assert_eq!(merged.instance_count(), 1);
402    }
403    #[test]
404    fn test_instances_for_class() {
405        let mut reg = TypeClassRegistry::new();
406        reg.register_class(add_class());
407        reg.register_instance(nat_instance());
408        reg.register_instance(Instance::new(Name::str("Add"), mk_const("Int")));
409        let all = reg.instances_for_class(&Name::str("Add"));
410        assert_eq!(all.len(), 2);
411    }
412    #[test]
413    fn test_total_method_impls() {
414        let mut reg = TypeClassRegistry::new();
415        reg.register_class(add_class());
416        let mut inst = nat_instance();
417        inst.add_method_impl("add", mk_const("Nat.add"));
418        reg.register_instance(inst);
419        assert_eq!(total_method_impls(&reg), 1);
420    }
421}
422/// Build the full class hierarchy graph from a registry.
423///
424/// Returns a list of all parent–child edges discovered by inspecting
425/// every registered class's `super_classes` list.
426pub fn build_class_hierarchy(registry: &TypeClassRegistry) -> Vec<ClassEdge> {
427    let mut edges = Vec::new();
428    for cls in registry.classes.values() {
429        for sup in &cls.super_classes {
430            edges.push(ClassEdge::new(sup.clone(), cls.name.clone()));
431        }
432    }
433    edges
434}
435/// Check whether `ancestor` is an ancestor of `descendant` in the class hierarchy.
436pub fn is_ancestor(ancestor: &Name, descendant: &Name, registry: &TypeClassRegistry) -> bool {
437    let supers = transitive_supers(descendant, registry);
438    supers.contains(ancestor)
439}
440/// Find all instances that are complete (implement every method declared by the class).
441pub fn complete_instances(registry: &TypeClassRegistry) -> Vec<&Instance> {
442    registry
443        .instances
444        .iter()
445        .filter(|inst| instance_is_complete(inst, registry))
446        .collect()
447}
448/// Validate that all instances in the registry reference known classes.
449pub fn validate_registry(registry: &TypeClassRegistry) -> Vec<String> {
450    let mut errors = Vec::new();
451    for inst in &registry.instances {
452        if !registry.is_class(&inst.class) {
453            errors.push(format!("Instance references unknown class: {}", inst.class));
454        }
455    }
456    for cls in registry.classes.values() {
457        for sup in &cls.super_classes {
458            if !registry.is_class(sup) {
459                errors.push(format!(
460                    "Class {} references unknown super-class: {}",
461                    cls.name, sup
462                ));
463            }
464        }
465    }
466    errors
467}
468/// Check whether a class exists and has at least one registered instance.
469pub fn class_has_instance(class: &Name, registry: &TypeClassRegistry) -> bool {
470    registry.instances_for_class(class).iter().any(|_| true)
471}
472/// Count the number of classes with zero registered instances.
473pub fn classes_without_instances(registry: &TypeClassRegistry) -> usize {
474    registry
475        .classes
476        .keys()
477        .filter(|name| {
478            let n = Name::str(name.as_str());
479            registry.instances_for_class(&n).is_empty()
480        })
481        .count()
482}
483/// Return method names shared between two classes.
484pub fn shared_methods(a: &TypeClass, b: &TypeClass) -> Vec<Name> {
485    a.method_names()
486        .filter(|n| b.find_method(n).is_some())
487        .cloned()
488        .collect()
489}
490/// Return all (class_name, method_name) pairs in the registry.
491pub fn all_method_pairs(registry: &TypeClassRegistry) -> Vec<(Name, Name)> {
492    let mut pairs = Vec::new();
493    for cls in registry.classes.values() {
494        for m in &cls.methods {
495            pairs.push((cls.name.clone(), m.name.clone()));
496        }
497    }
498    pairs
499}
500/// A trait object for custom instance resolution strategies.
501///
502/// Implementors can supply alternative instance lookup logic.
503pub trait InstanceResolver: std::fmt::Debug {
504    /// Attempt to resolve an instance for `class` applied to `ty`.
505    fn resolve(&self, class: &Name, ty: &Expr) -> Option<Instance>;
506    /// Name of this resolver strategy.
507    fn name(&self) -> &'static str;
508}
509/// Check whether two instances are compatible (same class, overlapping params).
510#[allow(dead_code)]
511pub fn instances_compatible(a: &Instance, b: &Instance) -> bool {
512    a.class == b.class
513}
514/// Check whether an instance subsumes another (has a more general pattern).
515///
516/// For now this is a simple syntactic check.
517#[allow(dead_code)]
518pub fn instance_subsumes(general: &Instance, specific: &Instance) -> bool {
519    if general.class != specific.class {
520        return false;
521    }
522    general.ty == specific.ty || matches!(general.ty, Expr::Sort(_))
523}
524/// Return a human-readable summary of a `TypeClass`.
525#[allow(dead_code)]
526pub fn typeclass_summary(cls: &TypeClass) -> String {
527    let params: Vec<String> = cls.params.iter().map(|p| p.to_string()).collect();
528    let methods: Vec<String> = cls.methods.iter().map(|m| m.name.to_string()).collect();
529    format!(
530        "class {} ({}) {{ {} }}",
531        cls.name,
532        params.join(", "),
533        methods.join(", ")
534    )
535}
536/// Return a human-readable summary of an `Instance`.
537#[allow(dead_code)]
538pub fn instance_summary(inst: &Instance) -> String {
539    let n = inst
540        .instance_name
541        .as_ref()
542        .map(|n| n.to_string())
543        .unwrap_or_else(|| "_anon".to_string());
544    format!("instance {} : {}", n, inst.class)
545}
546#[cfg(test)]
547mod typeclass_extra_tests {
548    use super::*;
549    use crate::Level;
550    fn mk_sort() -> Expr {
551        Expr::Sort(Level::zero())
552    }
553    fn mk_name(s: &str) -> Name {
554        Name::str(s)
555    }
556    #[test]
557    fn test_typeclass_stats_hit_rate_empty() {
558        let s = TypeClassStats::new();
559        assert_eq!(s.hit_rate(), 1.0);
560    }
561    #[test]
562    fn test_typeclass_stats_hit_rate() {
563        let mut s = TypeClassStats {
564            total_lookups: 10,
565            cache_hits: 8,
566            ..Default::default()
567        };
568        assert!((s.hit_rate() - 0.8).abs() < 1e-10);
569        let s2 = TypeClassStats {
570            cache_hits: 2,
571            total_lookups: 2,
572            ..Default::default()
573        };
574        s.merge(&s2);
575        assert_eq!(s.cache_hits, 10);
576    }
577    #[test]
578    fn test_layered_registry_push_pop() {
579        let mut reg = LayeredTypeClassRegistry::new();
580        assert_eq!(reg.depth(), 0);
581        reg.push_layer();
582        assert_eq!(reg.depth(), 1);
583        reg.pop_layer();
584        assert_eq!(reg.depth(), 0);
585    }
586    #[test]
587    fn test_layered_registry_add_instance_top() {
588        let mut reg = LayeredTypeClassRegistry::new();
589        reg.push_layer();
590        let inst = Instance::named(mk_name("Add"), mk_sort(), mk_name("MyInst"));
591        reg.add_instance(inst.clone());
592        assert_eq!(reg.total_instances(), 1);
593        reg.pop_layer();
594        assert_eq!(reg.total_instances(), 0);
595    }
596    #[test]
597    fn test_layered_registry_find_global() {
598        let mut reg = LayeredTypeClassRegistry::new();
599        let inst = Instance::named(
600            mk_name("Add"),
601            Expr::Const(mk_name("Nat"), vec![]),
602            mk_name("NatAdd"),
603        );
604        reg.add_instance(inst);
605        let found = reg.find_instance(&mk_name("Add"), &Expr::Const(mk_name("Nat"), vec![]));
606        assert!(found.is_some());
607    }
608    #[test]
609    fn test_instance_priority_ordering() {
610        assert!(InstancePriority::Low < InstancePriority::Normal);
611        assert!(InstancePriority::Normal < InstancePriority::High);
612        assert!(InstancePriority::High < InstancePriority::Forced);
613    }
614    #[test]
615    fn test_instance_priority_from_u32() {
616        assert_eq!(InstancePriority::from_u32(0), InstancePriority::Low);
617        assert_eq!(InstancePriority::from_u32(100), InstancePriority::Normal);
618        assert_eq!(InstancePriority::from_u32(200), InstancePriority::High);
619        assert_eq!(InstancePriority::from_u32(999), InstancePriority::Forced);
620    }
621    #[test]
622    fn test_method_impl_custom() {
623        let m = MethodImpl::custom(mk_name("add"), mk_sort());
624        assert!(!m.is_default);
625    }
626    #[test]
627    fn test_method_impl_default() {
628        let m = MethodImpl::default_impl(mk_name("mul"), mk_sort());
629        assert!(m.is_default);
630    }
631    #[test]
632    fn test_instance_impl_add_get() {
633        let mut ii = InstanceImpl::new();
634        ii.add(MethodImpl::custom(mk_name("add"), mk_sort()));
635        ii.add(MethodImpl::default_impl(mk_name("mul"), mk_sort()));
636        assert_eq!(ii.len(), 2);
637        assert!(ii.get(&mk_name("add")).is_some());
638        assert!(ii.get(&mk_name("div")).is_none());
639        assert_eq!(ii.count_defaults(), 1);
640    }
641    #[test]
642    fn test_instances_compatible() {
643        let make_inst = |cls: &str| Instance::new(mk_name(cls), mk_sort());
644        let a = make_inst("Add");
645        let b = make_inst("Add");
646        let c = make_inst("Mul");
647        assert!(instances_compatible(&a, &b));
648        assert!(!instances_compatible(&a, &c));
649    }
650    #[test]
651    fn test_typeclass_summary() {
652        let cls = TypeClass {
653            name: mk_name("Add"),
654            params: vec![mk_name("α")],
655            ty: mk_sort(),
656            methods: vec![Method::new(mk_name("add"), mk_sort(), 0)],
657            super_classes: vec![],
658            is_prop: false,
659        };
660        let s = typeclass_summary(&cls);
661        assert!(s.contains("Add"));
662        assert!(s.contains("add"));
663    }
664    #[test]
665    fn test_null_resolver() {
666        let r = NullResolver;
667        assert_eq!(r.name(), "null");
668        assert!(r.resolve(&mk_name("Add"), &mk_sort()).is_none());
669    }
670    #[test]
671    fn test_instance_subsumes_empty_params() {
672        let general = Instance::new(mk_name("Eq"), Expr::Sort(crate::Level::zero()));
673        let specific = Instance::new(mk_name("Eq"), mk_sort());
674        assert!(instance_subsumes(&general, &specific));
675    }
676}
677#[cfg(test)]
678mod tests_padding_infra {
679    use super::*;
680    #[test]
681    fn test_stat_summary() {
682        let mut ss = StatSummary::new();
683        ss.record(10.0);
684        ss.record(20.0);
685        ss.record(30.0);
686        assert_eq!(ss.count(), 3);
687        assert!((ss.mean().expect("mean should succeed") - 20.0).abs() < 1e-9);
688        assert_eq!(ss.min().expect("min should succeed") as i64, 10);
689        assert_eq!(ss.max().expect("max should succeed") as i64, 30);
690    }
691    #[test]
692    fn test_transform_stat() {
693        let mut ts = TransformStat::new();
694        ts.record_before(100.0);
695        ts.record_after(80.0);
696        let ratio = ts.mean_ratio().expect("ratio should be present");
697        assert!((ratio - 0.8).abs() < 1e-9);
698    }
699    #[test]
700    fn test_small_map() {
701        let mut m: SmallMap<u32, &str> = SmallMap::new();
702        m.insert(3, "three");
703        m.insert(1, "one");
704        m.insert(2, "two");
705        assert_eq!(m.get(&2), Some(&"two"));
706        assert_eq!(m.len(), 3);
707        let keys = m.keys();
708        assert_eq!(*keys[0], 1);
709        assert_eq!(*keys[2], 3);
710    }
711    #[test]
712    fn test_label_set() {
713        let mut ls = LabelSet::new();
714        ls.add("foo");
715        ls.add("bar");
716        ls.add("foo");
717        assert_eq!(ls.count(), 2);
718        assert!(ls.has("bar"));
719        assert!(!ls.has("baz"));
720    }
721    #[test]
722    fn test_config_node() {
723        let mut root = ConfigNode::section("root");
724        let child = ConfigNode::leaf("key", "value");
725        root.add_child(child);
726        assert_eq!(root.num_children(), 1);
727    }
728    #[test]
729    fn test_versioned_record() {
730        let mut vr = VersionedRecord::new(0u32);
731        vr.update(1);
732        vr.update(2);
733        assert_eq!(*vr.current(), 2);
734        assert_eq!(vr.version(), 2);
735        assert!(vr.has_history());
736        assert_eq!(*vr.at_version(0).expect("value should be present"), 0);
737    }
738    #[test]
739    fn test_simple_dag() {
740        let mut dag = SimpleDag::new(4);
741        dag.add_edge(0, 1);
742        dag.add_edge(1, 2);
743        dag.add_edge(2, 3);
744        assert!(dag.can_reach(0, 3));
745        assert!(!dag.can_reach(3, 0));
746        let order = dag.topological_sort().expect("order should be present");
747        assert_eq!(order, vec![0, 1, 2, 3]);
748    }
749    #[test]
750    fn test_focus_stack() {
751        let mut fs: FocusStack<&str> = FocusStack::new();
752        fs.focus("a");
753        fs.focus("b");
754        assert_eq!(fs.current(), Some(&"b"));
755        assert_eq!(fs.depth(), 2);
756        fs.blur();
757        assert_eq!(fs.current(), Some(&"a"));
758    }
759}
760#[cfg(test)]
761mod tests_extra_iterators {
762    use super::*;
763    #[test]
764    fn test_window_iterator() {
765        let data = vec![1u32, 2, 3, 4, 5];
766        let windows: Vec<_> = WindowIterator::new(&data, 3).collect();
767        assert_eq!(windows.len(), 3);
768        assert_eq!(windows[0], &[1, 2, 3]);
769        assert_eq!(windows[2], &[3, 4, 5]);
770    }
771    #[test]
772    fn test_non_empty_vec() {
773        let mut nev = NonEmptyVec::singleton(10u32);
774        nev.push(20);
775        nev.push(30);
776        assert_eq!(nev.len(), 3);
777        assert_eq!(*nev.first(), 10);
778        assert_eq!(*nev.last(), 30);
779    }
780}
781#[cfg(test)]
782mod tests_padding2 {
783    use super::*;
784    #[test]
785    fn test_sliding_sum() {
786        let mut ss = SlidingSum::new(3);
787        ss.push(1.0);
788        ss.push(2.0);
789        ss.push(3.0);
790        assert!((ss.sum() - 6.0).abs() < 1e-9);
791        ss.push(4.0);
792        assert!((ss.sum() - 9.0).abs() < 1e-9);
793        assert_eq!(ss.count(), 3);
794    }
795    #[test]
796    fn test_path_buf() {
797        let mut pb = PathBuf::new();
798        pb.push("src");
799        pb.push("main");
800        assert_eq!(pb.as_str(), "src/main");
801        assert_eq!(pb.depth(), 2);
802        pb.pop();
803        assert_eq!(pb.as_str(), "src");
804    }
805    #[test]
806    fn test_string_pool() {
807        let mut pool = StringPool::new();
808        let s = pool.take();
809        assert!(s.is_empty());
810        pool.give("hello".to_string());
811        let s2 = pool.take();
812        assert!(s2.is_empty());
813        assert_eq!(pool.free_count(), 0);
814    }
815    #[test]
816    fn test_transitive_closure() {
817        let mut tc = TransitiveClosure::new(4);
818        tc.add_edge(0, 1);
819        tc.add_edge(1, 2);
820        tc.add_edge(2, 3);
821        assert!(tc.can_reach(0, 3));
822        assert!(!tc.can_reach(3, 0));
823        let r = tc.reachable_from(0);
824        assert_eq!(r.len(), 4);
825    }
826    #[test]
827    fn test_token_bucket() {
828        let mut tb = TokenBucket::new(100, 0);
829        assert_eq!(tb.available(), 100);
830        assert!(tb.try_consume(50));
831        assert_eq!(tb.available(), 50);
832        assert!(!tb.try_consume(60));
833        assert_eq!(tb.capacity(), 100);
834    }
835    #[test]
836    fn test_rewrite_rule_set() {
837        let mut rrs = RewriteRuleSet::new();
838        rrs.add(RewriteRule::unconditional(
839            "beta",
840            "App(Lam(x, b), v)",
841            "b[x:=v]",
842        ));
843        rrs.add(RewriteRule::conditional("comm", "a + b", "b + a"));
844        assert_eq!(rrs.len(), 2);
845        assert_eq!(rrs.unconditional_rules().len(), 1);
846        assert_eq!(rrs.conditional_rules().len(), 1);
847        assert!(rrs.get("beta").is_some());
848        let disp = rrs
849            .get("beta")
850            .expect("element at \'beta\' should exist")
851            .display();
852        assert!(disp.contains("→"));
853    }
854}
855#[cfg(test)]
856mod tests_padding3 {
857    use super::*;
858    #[test]
859    fn test_decision_node() {
860        let tree = DecisionNode::Branch {
861            key: "x".into(),
862            val: "1".into(),
863            yes_branch: Box::new(DecisionNode::Leaf("yes".into())),
864            no_branch: Box::new(DecisionNode::Leaf("no".into())),
865        };
866        let mut ctx = std::collections::HashMap::new();
867        ctx.insert("x".into(), "1".into());
868        assert_eq!(tree.evaluate(&ctx), "yes");
869        ctx.insert("x".into(), "2".into());
870        assert_eq!(tree.evaluate(&ctx), "no");
871        assert_eq!(tree.depth(), 1);
872    }
873    #[test]
874    fn test_flat_substitution() {
875        let mut sub = FlatSubstitution::new();
876        sub.add("foo", "bar");
877        sub.add("baz", "qux");
878        assert_eq!(sub.apply("foo and baz"), "bar and qux");
879        assert_eq!(sub.len(), 2);
880    }
881    #[test]
882    fn test_stopwatch() {
883        let mut sw = Stopwatch::start();
884        sw.split();
885        sw.split();
886        assert_eq!(sw.num_splits(), 2);
887        assert!(sw.elapsed_ms() >= 0.0);
888        for &s in sw.splits() {
889            assert!(s >= 0.0);
890        }
891    }
892    #[test]
893    fn test_either2() {
894        let e: Either2<i32, &str> = Either2::First(42);
895        assert!(e.is_first());
896        let mapped = e.map_first(|x| x * 2);
897        assert_eq!(mapped.first(), Some(84));
898        let e2: Either2<i32, &str> = Either2::Second("hello");
899        assert!(e2.is_second());
900        assert_eq!(e2.second(), Some("hello"));
901    }
902    #[test]
903    fn test_write_once() {
904        let wo: WriteOnce<u32> = WriteOnce::new();
905        assert!(!wo.is_written());
906        assert!(wo.write(42));
907        assert!(!wo.write(99));
908        assert_eq!(wo.read(), Some(42));
909    }
910    #[test]
911    fn test_sparse_vec() {
912        let mut sv: SparseVec<i32> = SparseVec::new(100);
913        sv.set(5, 10);
914        sv.set(50, 20);
915        assert_eq!(*sv.get(5), 10);
916        assert_eq!(*sv.get(50), 20);
917        assert_eq!(*sv.get(0), 0);
918        assert_eq!(sv.nnz(), 2);
919        sv.set(5, 0);
920        assert_eq!(sv.nnz(), 1);
921    }
922    #[test]
923    fn test_stack_calc() {
924        let mut calc = StackCalc::new();
925        calc.push(3);
926        calc.push(4);
927        assert_eq!(calc.add(), Some(7));
928        assert_eq!(calc.peek(), Some(7));
929        calc.push(2);
930        assert_eq!(calc.mul(), Some(14));
931        assert_eq!(calc.peek(), Some(14));
932    }
933}