oxilean_kernel/inductive/
functions.rs

1//! Auto-generated module
2//!
3//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)
4
5use crate::{Expr, KernelError, Level, Name};
6
7use super::types::{
8    ConfigNode, FocusStack, InductiveEnv, InductiveError, InductiveFamily, InductiveType,
9    InductiveTypeBuilder, InductiveTypeInfo, IntroRule, LabelSet, NonEmptyVec, RecursorBuilder,
10    SimpleDag, SmallMap, StatSummary, TransformStat, VersionedRecord, WindowIterator,
11};
12
13/// Count the number of Pi arguments in a type.
14pub(super) fn count_pi_args(ty: &Expr) -> u32 {
15    match ty {
16        Expr::Pi(_, _, _, body) => 1 + count_pi_args(body),
17        _ => 0,
18    }
19}
20/// Peel all Pi binders from a type, returning a list of domain types and the final body.
21pub(super) fn peel_pi_binders(ty: &Expr) -> (Vec<Expr>, &Expr) {
22    let mut domains = Vec::new();
23    let mut current = ty;
24    while let Expr::Pi(_, _, dom, body) = current {
25        domains.push(dom.as_ref().clone());
26        current = body;
27    }
28    (domains, current)
29}
30/// Lift all free BVars in an expression by `amount` (used to adjust de Bruijn indices
31/// when inserting new binders outside the expression).
32pub(super) fn lift_expr_bvars(expr: &Expr, amount: u32) -> Expr {
33    lift_expr_bvars_at(expr, amount, 0)
34}
35fn lift_expr_bvars_at(expr: &Expr, amount: u32, cutoff: u32) -> Expr {
36    match expr {
37        Expr::BVar(i) => {
38            if *i >= cutoff {
39                Expr::BVar(i + amount)
40            } else {
41                expr.clone()
42            }
43        }
44        Expr::Sort(_) | Expr::FVar(_) | Expr::Const(_, _) | Expr::Lit(_) => expr.clone(),
45        Expr::App(f, a) => Expr::App(
46            Box::new(lift_expr_bvars_at(f, amount, cutoff)),
47            Box::new(lift_expr_bvars_at(a, amount, cutoff)),
48        ),
49        Expr::Pi(bi, n, ty, body) => Expr::Pi(
50            *bi,
51            n.clone(),
52            Box::new(lift_expr_bvars_at(ty, amount, cutoff)),
53            Box::new(lift_expr_bvars_at(body, amount, cutoff + 1)),
54        ),
55        Expr::Lam(bi, n, ty, body) => Expr::Lam(
56            *bi,
57            n.clone(),
58            Box::new(lift_expr_bvars_at(ty, amount, cutoff)),
59            Box::new(lift_expr_bvars_at(body, amount, cutoff + 1)),
60        ),
61        Expr::Let(n, ty, val, body) => Expr::Let(
62            n.clone(),
63            Box::new(lift_expr_bvars_at(ty, amount, cutoff)),
64            Box::new(lift_expr_bvars_at(val, amount, cutoff)),
65            Box::new(lift_expr_bvars_at(body, amount, cutoff + 1)),
66        ),
67        Expr::Proj(n, idx, e) => Expr::Proj(
68            n.clone(),
69            *idx,
70            Box::new(lift_expr_bvars_at(e, amount, cutoff)),
71        ),
72    }
73}
74/// Check an inductive type declaration for validity.
75#[allow(clippy::result_large_err)]
76pub fn check_inductive(ind: &InductiveType) -> Result<(), KernelError> {
77    for intro in &ind.intro_rules {
78        if !returns_type(&intro.ty, &ind.name) {
79            return Err(KernelError::InvalidInductive(format!(
80                "constructor {} does not return type {}",
81                intro.name, ind.name
82            )));
83        }
84    }
85    for intro in &ind.intro_rules {
86        check_positivity(&ind.name, &intro.ty)?;
87    }
88    Ok(())
89}
90fn returns_type(ty: &Expr, name: &Name) -> bool {
91    match ty {
92        Expr::Const(n, _) => n == name,
93        Expr::App(f, _) => returns_type(f, name),
94        Expr::Pi(_, _, _, cod) => returns_type(cod, name),
95        _ => false,
96    }
97}
98#[allow(clippy::result_large_err)]
99fn check_positivity(ind_name: &Name, ty: &Expr) -> Result<(), KernelError> {
100    check_positivity_rec(ind_name, ty, true)
101}
102#[allow(clippy::result_large_err)]
103fn check_positivity_rec(ind_name: &Name, ty: &Expr, positive: bool) -> Result<(), KernelError> {
104    match ty {
105        Expr::Const(n, _) => {
106            if n == ind_name && !positive {
107                return Err(KernelError::InvalidInductive(format!(
108                    "negative occurrence of {} in constructor type",
109                    ind_name
110                )));
111            }
112            Ok(())
113        }
114        Expr::App(f, a) => {
115            check_positivity_rec(ind_name, f, positive)?;
116            check_positivity_rec(ind_name, a, positive)
117        }
118        Expr::Pi(_, _, dom, cod) => {
119            check_positivity_rec_domain(ind_name, dom)?;
120            check_positivity_rec(ind_name, cod, positive)
121        }
122        Expr::Lam(_, _, ty_inner, body) => {
123            check_positivity_rec(ind_name, ty_inner, positive)?;
124            check_positivity_rec(ind_name, body, positive)
125        }
126        _ => Ok(()),
127    }
128}
129/// Check the domain of a Pi binder for strict positivity.
130/// Direct references to `ind_name` are allowed; references inside
131/// nested function types (which would be truly negative) are rejected.
132#[allow(clippy::result_large_err)]
133fn check_positivity_rec_domain(ind_name: &Name, dom: &Expr) -> Result<(), KernelError> {
134    match dom {
135        Expr::Const(_, _) => Ok(()),
136        Expr::App(f, a) => {
137            check_positivity_rec_domain(ind_name, f)?;
138            check_positivity_rec_domain(ind_name, a)
139        }
140        Expr::Pi(_, _, inner_dom, inner_cod) => {
141            check_positivity_rec(ind_name, inner_dom, false)?;
142            check_positivity_rec_domain(ind_name, inner_cod)
143        }
144        _ => Ok(()),
145    }
146}
147/// Reduce a recursor application (iota-reduction).
148///
149/// This is the legacy API. The new implementation is in `reduce.rs`.
150pub fn reduce_recursor(_rec_name: &Name, _args: &[Expr]) -> Option<Expr> {
151    None
152}
153#[cfg(test)]
154mod tests {
155    use super::*;
156    use crate::BinderInfo;
157    #[test]
158    fn test_inductive_creation() {
159        let bool_ty = Expr::Sort(Level::zero());
160        let true_intro = IntroRule {
161            name: Name::str("true"),
162            ty: Expr::Const(Name::str("Bool"), vec![]),
163        };
164        let false_intro = IntroRule {
165            name: Name::str("false"),
166            ty: Expr::Const(Name::str("Bool"), vec![]),
167        };
168        let bool_ind = InductiveType::new(
169            Name::str("Bool"),
170            vec![],
171            0,
172            0,
173            bool_ty,
174            vec![true_intro, false_intro],
175        );
176        assert_eq!(bool_ind.name, Name::str("Bool"));
177        assert_eq!(bool_ind.intro_rules.len(), 2);
178        assert!(!bool_ind.is_recursive());
179    }
180    #[test]
181    fn test_inductive_env() {
182        let mut env = InductiveEnv::new();
183        let bool_ty = Expr::Sort(Level::zero());
184        let bool_ind = InductiveType::new(
185            Name::str("Bool"),
186            vec![],
187            0,
188            0,
189            bool_ty,
190            vec![IntroRule {
191                name: Name::str("true"),
192                ty: Expr::Const(Name::str("Bool"), vec![]),
193            }],
194        );
195        env.add(bool_ind).expect("value should be present");
196        assert!(env.get(&Name::str("Bool")).is_some());
197        assert!(env.is_constructor(&Name::str("true")));
198    }
199    #[test]
200    fn test_positivity_check() {
201        let pos_ty = Expr::Pi(
202            BinderInfo::Default,
203            Name::str("x"),
204            Box::new(Expr::Const(Name::str("Bool"), vec![])),
205            Box::new(Expr::Const(Name::str("Nat"), vec![])),
206        );
207        assert!(check_positivity(&Name::str("Nat"), &pos_ty).is_ok());
208        let neg_ty = Expr::Pi(
209            BinderInfo::Default,
210            Name::str("f"),
211            Box::new(Expr::Pi(
212                BinderInfo::Default,
213                Name::str("n"),
214                Box::new(Expr::Const(Name::str("Nat"), vec![])),
215                Box::new(Expr::Const(Name::str("Bool"), vec![])),
216            )),
217            Box::new(Expr::Const(Name::str("Bool"), vec![])),
218        );
219        assert!(check_positivity(&Name::str("Nat"), &neg_ty).is_err());
220    }
221    #[test]
222    fn test_recursive_detection() {
223        let nat_ty = Expr::Sort(Level::zero());
224        let nat_ind = InductiveType::new(
225            Name::str("Nat"),
226            vec![],
227            0,
228            0,
229            nat_ty,
230            vec![
231                IntroRule {
232                    name: Name::str("zero"),
233                    ty: Expr::Const(Name::str("Nat"), vec![]),
234                },
235                IntroRule {
236                    name: Name::str("succ"),
237                    ty: Expr::Pi(
238                        BinderInfo::Default,
239                        Name::str("n"),
240                        Box::new(Expr::Const(Name::str("Nat"), vec![])),
241                        Box::new(Expr::Const(Name::str("Nat"), vec![])),
242                    ),
243                },
244            ],
245        );
246        assert!(nat_ind.is_recursive());
247    }
248    #[test]
249    fn test_to_constant_infos() {
250        let nat_ind = InductiveType::new(
251            Name::str("Nat"),
252            vec![],
253            0,
254            0,
255            Expr::Sort(Level::succ(Level::zero())),
256            vec![
257                IntroRule {
258                    name: Name::str("Nat.zero"),
259                    ty: Expr::Const(Name::str("Nat"), vec![]),
260                },
261                IntroRule {
262                    name: Name::str("Nat.succ"),
263                    ty: Expr::Pi(
264                        BinderInfo::Default,
265                        Name::str("n"),
266                        Box::new(Expr::Const(Name::str("Nat"), vec![])),
267                        Box::new(Expr::Const(Name::str("Nat"), vec![])),
268                    ),
269                },
270            ],
271        );
272        let (ind_ci, ctor_cis, rec_ci) = nat_ind.to_constant_infos();
273        assert!(ind_ci.is_inductive());
274        let iv = ind_ci.to_inductive_val().expect("iv should be present");
275        assert_eq!(iv.ctors.len(), 2);
276        assert!(iv.is_rec);
277        assert_eq!(ctor_cis.len(), 2);
278        assert!(ctor_cis[0].is_constructor());
279        let cv0 = ctor_cis[0]
280            .to_constructor_val()
281            .expect("cv0 should be present");
282        assert_eq!(cv0.num_fields, 0);
283        let cv1 = ctor_cis[1]
284            .to_constructor_val()
285            .expect("cv1 should be present");
286        assert_eq!(cv1.num_fields, 1);
287        assert!(rec_ci.is_recursor());
288        let rv = rec_ci.to_recursor_val().expect("rv should be present");
289        assert_eq!(rv.num_minors, 2);
290        assert_eq!(rv.get_major_idx(), 3);
291    }
292    #[test]
293    fn test_register_in_env() {
294        let mut env = crate::Environment::new();
295        let mut ind_env = InductiveEnv::new();
296        let bool_ind = InductiveType::new(
297            Name::str("Bool"),
298            vec![],
299            0,
300            0,
301            Expr::Sort(Level::succ(Level::zero())),
302            vec![
303                IntroRule {
304                    name: Name::str("Bool.true"),
305                    ty: Expr::Const(Name::str("Bool"), vec![]),
306                },
307                IntroRule {
308                    name: Name::str("Bool.false"),
309                    ty: Expr::Const(Name::str("Bool"), vec![]),
310                },
311            ],
312        );
313        ind_env
314            .register_in_env(&bool_ind, &mut env)
315            .expect("value should be present");
316        assert!(env.is_inductive(&Name::str("Bool")));
317        assert!(env.is_constructor(&Name::str("Bool.true")));
318        assert!(env.is_constructor(&Name::str("Bool.false")));
319        assert!(env.is_recursor(&Name::str("Bool").append_str("rec")));
320    }
321}
322/// Build the `Bool` inductive type (no parameters, two constructors).
323#[allow(dead_code)]
324pub fn mk_bool_inductive() -> InductiveType {
325    InductiveTypeBuilder::new()
326        .name(Name::str("Bool"))
327        .ty(Expr::Sort(Level::succ(Level::zero())))
328        .intro_rule(
329            Name::str("Bool.true"),
330            Expr::Const(Name::str("Bool"), vec![]),
331        )
332        .intro_rule(
333            Name::str("Bool.false"),
334            Expr::Const(Name::str("Bool"), vec![]),
335        )
336        .build()
337        .expect("Bool inductive type build failed")
338}
339/// Build the `Nat` inductive type.
340#[allow(dead_code)]
341pub fn mk_nat_inductive() -> InductiveType {
342    InductiveTypeBuilder::new()
343        .name(Name::str("Nat"))
344        .ty(Expr::Sort(Level::succ(Level::zero())))
345        .intro_rule(Name::str("Nat.zero"), Expr::Const(Name::str("Nat"), vec![]))
346        .intro_rule(
347            Name::str("Nat.succ"),
348            Expr::Pi(
349                crate::BinderInfo::Default,
350                Name::str("n"),
351                Box::new(Expr::Const(Name::str("Nat"), vec![])),
352                Box::new(Expr::Const(Name::str("Nat"), vec![])),
353            ),
354        )
355        .build()
356        .expect("Nat inductive type build failed")
357}
358/// Build the `Unit` inductive type (single constructor, no fields).
359#[allow(dead_code)]
360pub fn mk_unit_inductive() -> InductiveType {
361    InductiveTypeBuilder::new()
362        .name(Name::str("Unit"))
363        .ty(Expr::Sort(Level::succ(Level::zero())))
364        .intro_rule(
365            Name::str("Unit.unit"),
366            Expr::Const(Name::str("Unit"), vec![]),
367        )
368        .build()
369        .expect("Unit inductive type build failed")
370}
371/// Build the `Empty` inductive type (no constructors — ex falso).
372#[allow(dead_code)]
373pub fn mk_empty_inductive() -> InductiveType {
374    InductiveTypeBuilder::new()
375        .name(Name::str("Empty"))
376        .ty(Expr::Sort(Level::succ(Level::zero())))
377        .build()
378        .unwrap_or_else(|_| {
379            InductiveType::new(
380                Name::str("Empty"),
381                vec![],
382                0,
383                0,
384                Expr::Sort(Level::succ(Level::zero())),
385                vec![],
386            )
387        })
388}
389/// Given an `InductiveType`, return the number of fields in each constructor.
390#[allow(dead_code)]
391pub fn constructor_field_counts(ind: &InductiveType) -> Vec<(Name, u32)> {
392    ind.intro_rules
393        .iter()
394        .map(|r| {
395            let total = count_pi_args(&r.ty);
396            let fields = total.saturating_sub(ind.num_params);
397            (r.name.clone(), fields)
398        })
399        .collect()
400}
401/// Check whether an inductive type is a singleton (one constructor, no recursive fields).
402#[allow(dead_code)]
403pub fn is_singleton_inductive(ind: &InductiveType) -> bool {
404    if ind.intro_rules.len() != 1 {
405        return false;
406    }
407    !ind.is_recursive()
408}
409/// Check whether an inductive type is an enum (all constructors have no fields).
410#[allow(dead_code)]
411pub fn is_enum_inductive(ind: &InductiveType) -> bool {
412    ind.intro_rules.iter().all(|r| {
413        let fields = count_pi_args(&r.ty).saturating_sub(ind.num_params);
414        fields == 0
415    })
416}
417/// Return the recursor name for a given inductive type name.
418#[allow(dead_code)]
419pub fn recursor_name(ind_name: &Name) -> Name {
420    Name::Str(Box::new(ind_name.clone()), "rec".to_string())
421}
422#[cfg(test)]
423mod extra_tests {
424    use super::*;
425    use crate::BinderInfo;
426    #[test]
427    fn test_builder_basic() {
428        let ind = InductiveTypeBuilder::new()
429            .name(Name::str("MyType"))
430            .ty(Expr::Sort(Level::succ(Level::zero())))
431            .intro_rule(
432                Name::str("MyType.mk"),
433                Expr::Const(Name::str("MyType"), vec![]),
434            )
435            .build()
436            .expect("value should be present");
437        assert_eq!(ind.name, Name::str("MyType"));
438        assert_eq!(ind.intro_rules.len(), 1);
439    }
440    #[test]
441    fn test_builder_missing_name_fails() {
442        let result = InductiveTypeBuilder::new()
443            .ty(Expr::Sort(Level::zero()))
444            .build();
445        assert!(result.is_err());
446    }
447    #[test]
448    fn test_builder_missing_ty_fails() {
449        let result = InductiveTypeBuilder::new().name(Name::str("X")).build();
450        assert!(result.is_err());
451    }
452    #[test]
453    fn test_mk_bool_inductive() {
454        let b = mk_bool_inductive();
455        assert_eq!(b.name, Name::str("Bool"));
456        assert_eq!(b.intro_rules.len(), 2);
457        assert!(is_enum_inductive(&b));
458    }
459    #[test]
460    fn test_mk_nat_inductive() {
461        let n = mk_nat_inductive();
462        assert_eq!(n.name, Name::str("Nat"));
463        assert!(n.is_recursive());
464        assert!(!is_enum_inductive(&n));
465    }
466    #[test]
467    fn test_mk_unit_inductive() {
468        let u = mk_unit_inductive();
469        assert!(is_singleton_inductive(&u));
470    }
471    #[test]
472    fn test_mk_empty_inductive() {
473        let e = mk_empty_inductive();
474        assert_eq!(e.name, Name::str("Empty"));
475        assert_eq!(e.intro_rules.len(), 0);
476        assert!(!is_singleton_inductive(&e));
477    }
478    #[test]
479    fn test_constructor_field_counts_bool() {
480        let b = mk_bool_inductive();
481        let counts = constructor_field_counts(&b);
482        assert_eq!(counts.len(), 2);
483        assert_eq!(counts[0].1, 0);
484        assert_eq!(counts[1].1, 0);
485    }
486    #[test]
487    fn test_constructor_field_counts_nat() {
488        let n = mk_nat_inductive();
489        let counts = constructor_field_counts(&n);
490        assert_eq!(counts[0].1, 0);
491        assert_eq!(counts[1].1, 1);
492    }
493    #[test]
494    fn test_recursor_name() {
495        let n = Name::str("Nat");
496        let r = recursor_name(&n);
497        assert_eq!(r, Name::Str(Box::new(Name::str("Nat")), "rec".to_string()));
498    }
499    #[test]
500    fn test_is_prop_flag() {
501        let mut ind = mk_bool_inductive();
502        assert!(!ind.is_prop);
503        ind.is_prop = true;
504        assert!(ind.is_prop);
505    }
506    #[test]
507    fn test_arity() {
508        let ind = InductiveTypeBuilder::new()
509            .name(Name::str("Vec"))
510            .ty(Expr::Sort(Level::succ(Level::zero())))
511            .num_params(1)
512            .num_indices(1)
513            .intro_rule(Name::str("Vec.nil"), Expr::Const(Name::str("Vec"), vec![]))
514            .build()
515            .expect("value should be present");
516        assert_eq!(ind.arity(), 2);
517    }
518    #[test]
519    fn test_builder_univ_params() {
520        let ind = InductiveTypeBuilder::new()
521            .name(Name::str("List"))
522            .ty(Expr::Sort(Level::succ(Level::zero())))
523            .univ_params(vec![Name::str("u")])
524            .intro_rule(
525                Name::str("List.nil"),
526                Expr::Const(Name::str("List"), vec![Level::param(Name::str("u"))]),
527            )
528            .build()
529            .expect("value should be present");
530        assert_eq!(ind.univ_params.len(), 1);
531    }
532    #[test]
533    fn test_is_nested_flag() {
534        let ind = InductiveTypeBuilder::new()
535            .name(Name::str("NTree"))
536            .ty(Expr::Sort(Level::succ(Level::zero())))
537            .is_nested(true)
538            .intro_rule(
539                Name::str("NTree.leaf"),
540                Expr::Const(Name::str("NTree"), vec![]),
541            )
542            .build()
543            .expect("value should be present");
544        assert!(ind.is_nested);
545    }
546    #[test]
547    fn test_positivity_passes_for_nat_succ() {
548        let succ_ty = Expr::Pi(
549            BinderInfo::Default,
550            Name::str("n"),
551            Box::new(Expr::Const(Name::str("Nat"), vec![])),
552            Box::new(Expr::Const(Name::str("Nat"), vec![])),
553        );
554        assert!(check_positivity(&Name::str("Nat"), &succ_ty).is_ok());
555    }
556}
557#[cfg(test)]
558mod inductive_extra_tests {
559    use super::*;
560    fn mk_nat_type() -> InductiveType {
561        InductiveType::new(
562            Name::str("Nat"),
563            vec![],
564            0,
565            0,
566            Expr::Sort(Level::succ(Level::zero())),
567            vec![
568                IntroRule {
569                    name: Name::str("Nat.zero"),
570                    ty: Expr::Const(Name::str("Nat"), vec![]),
571                },
572                IntroRule {
573                    name: Name::str("Nat.succ"),
574                    ty: Expr::Pi(
575                        crate::BinderInfo::Default,
576                        Name::str("n"),
577                        Box::new(Expr::Const(Name::str("Nat"), vec![])),
578                        Box::new(Expr::Const(Name::str("Nat"), vec![])),
579                    ),
580                },
581            ],
582        )
583    }
584    #[test]
585    fn test_recursor_builder_validate() {
586        let builder = RecursorBuilder::new(Name::str("Nat.rec"));
587        assert!(builder.validate().is_ok());
588    }
589    #[test]
590    fn test_recursor_builder_build_name() {
591        let builder = RecursorBuilder::new(Name::str("List.rec"));
592        assert_eq!(builder.build_name(), Name::str("List.rec"));
593    }
594    #[test]
595    fn test_recursor_builder_chain() {
596        let builder = RecursorBuilder::new(Name::str("Nat.rec"))
597            .num_params(0)
598            .num_indices(0)
599            .is_prop(false);
600        assert!(!builder.is_prop);
601        assert_eq!(builder.num_params, 0);
602    }
603    #[test]
604    fn test_inductive_family_singleton() {
605        let nat = mk_nat_type();
606        let fam = InductiveFamily::singleton(nat.clone());
607        assert!(fam.is_singleton());
608        assert_eq!(fam.len(), 1);
609        assert_eq!(fam.total_constructors(), 2);
610    }
611    #[test]
612    fn test_inductive_family_type_names() {
613        let nat = mk_nat_type();
614        let fam = InductiveFamily::singleton(nat);
615        let names = fam.type_names();
616        assert_eq!(names.len(), 1);
617        assert_eq!(*names[0], Name::str("Nat"));
618    }
619    #[test]
620    fn test_inductive_family_all_constructor_names() {
621        let nat = mk_nat_type();
622        let fam = InductiveFamily::singleton(nat);
623        let ctors = fam.all_constructor_names();
624        assert_eq!(ctors.len(), 2);
625    }
626    #[test]
627    fn test_inductive_family_find_type() {
628        let nat = mk_nat_type();
629        let fam = InductiveFamily::singleton(nat);
630        assert!(fam.find_type(&Name::str("Nat")).is_some());
631        assert!(fam.find_type(&Name::str("List")).is_none());
632    }
633    #[test]
634    fn test_inductive_type_info_from_type() {
635        let nat = mk_nat_type();
636        let info = InductiveTypeInfo::from_type(&nat, false);
637        assert_eq!(info.name, Name::str("Nat"));
638        assert_eq!(info.num_constructors, 2);
639        assert!(!info.is_prop);
640        assert!(!info.is_mutual);
641    }
642    #[test]
643    fn test_inductive_type_info_summary() {
644        let nat = mk_nat_type();
645        let info = InductiveTypeInfo::from_type(&nat, false);
646        let s = info.summary();
647        assert!(s.contains("Nat"));
648        assert!(s.contains("ctors"));
649    }
650    #[test]
651    fn test_inductive_error_display() {
652        let e = InductiveError::AlreadyDefined(Name::str("Nat"));
653        assert!(e.to_string().contains("already defined"));
654        let e2 = InductiveError::NonStrictlyPositive(Name::str("T"));
655        assert!(e2.to_string().contains("non-strictly-positive"));
656    }
657    #[test]
658    fn test_inductive_error_other() {
659        let e = InductiveError::Other("some problem".to_string());
660        assert!(e.to_string().contains("some problem"));
661    }
662    #[test]
663    fn test_inductive_family_empty() {
664        let fam = InductiveFamily::new(vec![], vec![]);
665        assert!(fam.is_empty());
666        assert_eq!(fam.total_constructors(), 0);
667    }
668    #[test]
669    fn test_inductive_type_is_recursive() {
670        let nat = mk_nat_type();
671        assert!(nat.is_recursive());
672    }
673    #[test]
674    fn test_inductive_type_num_constructors() {
675        let nat = mk_nat_type();
676        assert_eq!(nat.num_constructors(), 2);
677    }
678    fn mk_bool_type() -> InductiveType {
679        InductiveType::new(
680            Name::str("Bool"),
681            vec![],
682            0,
683            0,
684            Expr::Sort(Level::succ(Level::zero())),
685            vec![
686                IntroRule {
687                    name: Name::str("Bool.false"),
688                    ty: Expr::Const(Name::str("Bool"), vec![]),
689                },
690                IntroRule {
691                    name: Name::str("Bool.true"),
692                    ty: Expr::Const(Name::str("Bool"), vec![]),
693                },
694            ],
695        )
696    }
697    #[test]
698    fn test_recursor_rhs_bool_false() {
699        let bool_ind = mk_bool_type();
700        let (_, _, rec_ci) = bool_ind.to_constant_infos();
701        let rec_val = rec_ci.to_recursor_val().expect("rec_val should be present");
702        let rule_false = rec_val
703            .get_rule(&Name::str("Bool.false"))
704            .expect("rule_false should be present");
705        assert_eq!(rule_false.nfields, 0);
706        assert_eq!(rule_false.rhs, Expr::BVar(1));
707    }
708    #[test]
709    fn test_recursor_rhs_bool_true() {
710        let bool_ind = mk_bool_type();
711        let (_, _, rec_ci) = bool_ind.to_constant_infos();
712        let rec_val = rec_ci.to_recursor_val().expect("rec_val should be present");
713        let rule_true = rec_val
714            .get_rule(&Name::str("Bool.true"))
715            .expect("rule_true should be present");
716        assert_eq!(rule_true.nfields, 0);
717        assert_eq!(rule_true.rhs, Expr::BVar(0));
718    }
719    #[test]
720    fn test_recursor_rhs_nat_zero() {
721        let nat_ind = mk_nat_type();
722        let (_, _, rec_ci) = nat_ind.to_constant_infos();
723        let rec_val = rec_ci.to_recursor_val().expect("rec_val should be present");
724        let rule_zero = rec_val
725            .get_rule(&Name::str("Nat.zero"))
726            .expect("rule_zero should be present");
727        assert_eq!(rule_zero.nfields, 0);
728        assert_eq!(rule_zero.rhs, Expr::BVar(1));
729    }
730    #[test]
731    fn test_recursor_rhs_nat_succ() {
732        let nat_ind = mk_nat_type();
733        let (_, _, rec_ci) = nat_ind.to_constant_infos();
734        let rec_val = rec_ci.to_recursor_val().expect("rec_val should be present");
735        let rule_succ = rec_val
736            .get_rule(&Name::str("Nat.succ"))
737            .expect("rule_succ should be present");
738        assert_eq!(rule_succ.nfields, 1);
739        let nat_rec = Expr::Const(Name::str("Nat").append_str("rec"), vec![]);
740        let ih = Expr::App(
741            Box::new(Expr::App(
742                Box::new(Expr::App(
743                    Box::new(Expr::App(Box::new(nat_rec), Box::new(Expr::BVar(3)))),
744                    Box::new(Expr::BVar(2)),
745                )),
746                Box::new(Expr::BVar(1)),
747            )),
748            Box::new(Expr::BVar(0)),
749        );
750        let expected = Expr::App(
751            Box::new(Expr::App(Box::new(Expr::BVar(1)), Box::new(Expr::BVar(0)))),
752            Box::new(ih),
753        );
754        assert_eq!(rule_succ.rhs, expected);
755    }
756    #[test]
757    fn test_recursor_iota_bool() {
758        use crate::reduce::Reducer;
759        use crate::{BinderInfo, Environment};
760        let mut env = Environment::new();
761        let mut ind_env = crate::InductiveEnv::new();
762        let bool_ind = mk_bool_type();
763        ind_env
764            .register_in_env(&bool_ind, &mut env)
765            .expect("value should be present");
766        let bool_const = Expr::Const(Name::str("Bool"), vec![]);
767        let false_const = Expr::Const(Name::str("Bool.false"), vec![]);
768        let true_const = Expr::Const(Name::str("Bool.true"), vec![]);
769        let motive = Expr::Lam(
770            BinderInfo::Default,
771            Name::str("_"),
772            Box::new(bool_const.clone()),
773            Box::new(bool_const.clone()),
774        );
775        let rec_app = Expr::App(
776            Box::new(Expr::App(
777                Box::new(Expr::App(
778                    Box::new(Expr::App(
779                        Box::new(Expr::Const(Name::str("Bool").append_str("rec"), vec![])),
780                        Box::new(motive),
781                    )),
782                    Box::new(false_const.clone()),
783                )),
784                Box::new(true_const.clone()),
785            )),
786            Box::new(false_const.clone()),
787        );
788        let mut reducer = Reducer::new();
789        let result = reducer.whnf_env(&rec_app, &env);
790        assert_eq!(
791            result, false_const,
792            "Bool.rec motive false true Bool.false should reduce to Bool.false"
793        );
794    }
795    #[test]
796    fn test_recursor_iota_nat_zero() {
797        use crate::reduce::Reducer;
798        use crate::{BinderInfo, Environment};
799        let mut env = Environment::new();
800        let mut ind_env = crate::InductiveEnv::new();
801        let nat_ind = mk_nat_type();
802        ind_env
803            .register_in_env(&nat_ind, &mut env)
804            .expect("value should be present");
805        let nat_const = Expr::Const(Name::str("Nat"), vec![]);
806        let zero_const = Expr::Const(Name::str("Nat.zero"), vec![]);
807        let motive = Expr::Lam(
808            BinderInfo::Default,
809            Name::str("_"),
810            Box::new(nat_const.clone()),
811            Box::new(nat_const.clone()),
812        );
813        let zero_val = zero_const.clone();
814        let succ_fn = Expr::Lam(
815            BinderInfo::Default,
816            Name::str("n"),
817            Box::new(nat_const.clone()),
818            Box::new(Expr::Lam(
819                BinderInfo::Default,
820                Name::str("ih"),
821                Box::new(nat_const.clone()),
822                Box::new(Expr::App(
823                    Box::new(Expr::Const(Name::str("Nat.succ"), vec![])),
824                    Box::new(Expr::BVar(1)),
825                )),
826            )),
827        );
828        let rec_app = Expr::App(
829            Box::new(Expr::App(
830                Box::new(Expr::App(
831                    Box::new(Expr::App(
832                        Box::new(Expr::Const(Name::str("Nat").append_str("rec"), vec![])),
833                        Box::new(motive),
834                    )),
835                    Box::new(zero_val.clone()),
836                )),
837                Box::new(succ_fn),
838            )),
839            Box::new(zero_const.clone()),
840        );
841        let mut reducer = Reducer::new();
842        let result = reducer.whnf_env(&rec_app, &env);
843        assert_eq!(
844            result, zero_val,
845            "Nat.rec motive zero_val succ_fn Nat.zero should reduce to zero_val"
846        );
847    }
848}
849#[cfg(test)]
850mod tests_padding_infra {
851    use super::*;
852    #[test]
853    fn test_stat_summary() {
854        let mut ss = StatSummary::new();
855        ss.record(10.0);
856        ss.record(20.0);
857        ss.record(30.0);
858        assert_eq!(ss.count(), 3);
859        assert!((ss.mean().expect("mean should succeed") - 20.0).abs() < 1e-9);
860        assert_eq!(ss.min().expect("min should succeed") as i64, 10);
861        assert_eq!(ss.max().expect("max should succeed") as i64, 30);
862    }
863    #[test]
864    fn test_transform_stat() {
865        let mut ts = TransformStat::new();
866        ts.record_before(100.0);
867        ts.record_after(80.0);
868        let ratio = ts.mean_ratio().expect("ratio should be present");
869        assert!((ratio - 0.8).abs() < 1e-9);
870    }
871    #[test]
872    fn test_small_map() {
873        let mut m: SmallMap<u32, &str> = SmallMap::new();
874        m.insert(3, "three");
875        m.insert(1, "one");
876        m.insert(2, "two");
877        assert_eq!(m.get(&2), Some(&"two"));
878        assert_eq!(m.len(), 3);
879        let keys = m.keys();
880        assert_eq!(*keys[0], 1);
881        assert_eq!(*keys[2], 3);
882    }
883    #[test]
884    fn test_label_set() {
885        let mut ls = LabelSet::new();
886        ls.add("foo");
887        ls.add("bar");
888        ls.add("foo");
889        assert_eq!(ls.count(), 2);
890        assert!(ls.has("bar"));
891        assert!(!ls.has("baz"));
892    }
893    #[test]
894    fn test_config_node() {
895        let mut root = ConfigNode::section("root");
896        let child = ConfigNode::leaf("key", "value");
897        root.add_child(child);
898        assert_eq!(root.num_children(), 1);
899    }
900    #[test]
901    fn test_versioned_record() {
902        let mut vr = VersionedRecord::new(0u32);
903        vr.update(1);
904        vr.update(2);
905        assert_eq!(*vr.current(), 2);
906        assert_eq!(vr.version(), 2);
907        assert!(vr.has_history());
908        assert_eq!(*vr.at_version(0).expect("value should be present"), 0);
909    }
910    #[test]
911    fn test_simple_dag() {
912        let mut dag = SimpleDag::new(4);
913        dag.add_edge(0, 1);
914        dag.add_edge(1, 2);
915        dag.add_edge(2, 3);
916        assert!(dag.can_reach(0, 3));
917        assert!(!dag.can_reach(3, 0));
918        let order = dag.topological_sort().expect("order should be present");
919        assert_eq!(order, vec![0, 1, 2, 3]);
920    }
921    #[test]
922    fn test_focus_stack() {
923        let mut fs: FocusStack<&str> = FocusStack::new();
924        fs.focus("a");
925        fs.focus("b");
926        assert_eq!(fs.current(), Some(&"b"));
927        assert_eq!(fs.depth(), 2);
928        fs.blur();
929        assert_eq!(fs.current(), Some(&"a"));
930    }
931}
932#[cfg(test)]
933mod tests_extra_iterators {
934    use super::*;
935    #[test]
936    fn test_window_iterator() {
937        let data = vec![1u32, 2, 3, 4, 5];
938        let windows: Vec<_> = WindowIterator::new(&data, 3).collect();
939        assert_eq!(windows.len(), 3);
940        assert_eq!(windows[0], &[1, 2, 3]);
941        assert_eq!(windows[2], &[3, 4, 5]);
942    }
943    #[test]
944    fn test_non_empty_vec() {
945        let mut nev = NonEmptyVec::singleton(10u32);
946        nev.push(20);
947        nev.push(30);
948        assert_eq!(nev.len(), 3);
949        assert_eq!(*nev.first(), 10);
950        assert_eq!(*nev.last(), 30);
951    }
952}
oxilean_kernel/inductive/functions.rs

oxilean_kernel/inductive/
functions.rs
