oxilean_kernel/inductive/
functions.rs

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

oxilean_kernel/inductive/
functions.rs
