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