oxilean_kernel/check/
functions.rs

1//! Auto-generated module
2//!
3//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)
4
5use crate::declaration::{ConstantInfo, ConstructorVal, InductiveVal, QuotVal, RecursorVal};
6use crate::env::EnvError;
7use crate::{Declaration, Environment, KernelError, TypeChecker};
8#[cfg(test)]
9use crate::{Expr, Name};
10
11use super::types::{
12    BatchCheckResult, CheckConfig, CheckStats, ConfigNode, DecisionNode, DeclKind, DeclSummary,
13    Either2, EnvBuilder, FlatSubstitution, FocusStack, LabelSet, NonEmptyVec, PathBuf, RewriteRule,
14    RewriteRuleSet, SimpleDag, SlidingSum, SmallMap, SparseVec, StackCalc, StatSummary, Stopwatch,
15    StringPool, TempEnvScope, TokenBucket, TransformStat, TransitiveClosure, VersionedRecord,
16    WellFormedResult, WindowIterator, WriteOnce,
17};
18
19/// Check a declaration and add it to the environment.
20///
21/// Validates that the declaration is well-formed and type-correct, then
22/// inserts it into the environment. Returns an error if the declaration
23/// fails type checking or if the name is already declared.
24#[allow(clippy::result_large_err)]
25pub fn check_declaration(env: &mut Environment, decl: Declaration) -> Result<(), KernelError> {
26    let name = decl.name().clone();
27    match &decl {
28        Declaration::Axiom { ty, .. } => {
29            let mut tc = TypeChecker::new(env);
30            tc.ensure_sort(ty)?;
31        }
32        Declaration::Definition { ty, val, .. } => {
33            let mut tc = TypeChecker::new(env);
34            tc.ensure_sort(ty)?;
35            let val_ty = tc.infer_type(val)?;
36            tc.check_type(val, &val_ty, ty)?;
37        }
38        Declaration::Theorem { ty, val, .. } => {
39            let mut tc = TypeChecker::new(env);
40            tc.ensure_sort(ty)?;
41            let val_ty = tc.infer_type(val)?;
42            tc.check_type(val, &val_ty, ty)?;
43        }
44        Declaration::Opaque { ty, val, .. } => {
45            let mut tc = TypeChecker::new(env);
46            tc.ensure_sort(ty)?;
47            let val_ty = tc.infer_type(val)?;
48            tc.check_type(val, &val_ty, ty)?;
49        }
50    }
51    env.add(decl).map_err(|e| match e {
52        EnvError::DuplicateDeclaration(_) => {
53            KernelError::Other(format!("duplicate declaration: {}", name))
54        }
55        EnvError::NotFound(_) => KernelError::Other(format!("declaration not found: {}", name)),
56    })
57}
58/// Check multiple declarations in sequence.
59///
60/// Processes the declarations in the given order, stopping at the first
61/// error. Each successfully-checked declaration is added to the environment
62/// so that later declarations can refer to earlier ones.
63#[allow(clippy::result_large_err)]
64pub fn check_declarations(
65    env: &mut Environment,
66    decls: Vec<Declaration>,
67) -> Result<(), KernelError> {
68    for decl in decls {
69        check_declaration(env, decl)?;
70    }
71    Ok(())
72}
73/// Check a `ConstantInfo` (inductive, constructor, recursor, or quotient) and add
74/// it to the environment.
75///
76/// Unlike `check_declaration`, this function handles the richer LEAN 4-style
77/// constant info types that include inductive types, constructors, recursors, and
78/// quotient type components.
79#[allow(clippy::result_large_err)]
80pub fn check_constant_info(env: &mut Environment, ci: ConstantInfo) -> Result<(), KernelError> {
81    let name = ci.name().clone();
82    match &ci {
83        ConstantInfo::Axiom(av) => {
84            let mut tc = TypeChecker::new(env);
85            tc.ensure_sort(&av.common.ty)?;
86        }
87        ConstantInfo::Definition(dv) => {
88            let mut tc = TypeChecker::new(env);
89            tc.ensure_sort(&dv.common.ty)?;
90            let val_ty = tc.infer_type(&dv.value)?;
91            tc.check_type(&dv.value, &val_ty, &dv.common.ty)?;
92        }
93        ConstantInfo::Theorem(tv) => {
94            let mut tc = TypeChecker::new(env);
95            tc.ensure_sort(&tv.common.ty)?;
96            let val_ty = tc.infer_type(&tv.value)?;
97            tc.check_type(&tv.value, &val_ty, &tv.common.ty)?;
98        }
99        ConstantInfo::Opaque(ov) => {
100            let mut tc = TypeChecker::new(env);
101            tc.ensure_sort(&ov.common.ty)?;
102            let val_ty = tc.infer_type(&ov.value)?;
103            tc.check_type(&ov.value, &val_ty, &ov.common.ty)?;
104        }
105        ConstantInfo::Inductive(iv) => {
106            check_inductive_val(env, iv)?;
107        }
108        ConstantInfo::Constructor(cv) => {
109            check_constructor_val(env, cv)?;
110        }
111        ConstantInfo::Recursor(rv) => {
112            check_recursor_val(env, rv)?;
113        }
114        ConstantInfo::Quotient(qv) => {
115            check_quotient_val(env, qv)?;
116        }
117    }
118    env.add_constant(ci).map_err(|e| match e {
119        crate::env::EnvError::DuplicateDeclaration(_) => {
120            KernelError::Other(format!("duplicate declaration: {}", name))
121        }
122        crate::env::EnvError::NotFound(_) => {
123            KernelError::Other(format!("declaration not found: {}", name))
124        }
125    })
126}
127/// Check multiple `ConstantInfo` declarations, stopping on the first error.
128#[allow(clippy::result_large_err)]
129pub fn check_constant_infos(
130    env: &mut Environment,
131    cis: Vec<ConstantInfo>,
132) -> Result<(), KernelError> {
133    for ci in cis {
134        check_constant_info(env, ci)?;
135    }
136    Ok(())
137}
138/// Validate an `InductiveVal`: verify the type is a sort.
139///
140/// Constructor types are checked separately via `check_constructor_val` when
141/// each constructor `ConstantInfo` is added. Empty inductives (0 constructors,
142/// like `Empty`) are valid.
143#[allow(clippy::result_large_err)]
144pub(super) fn check_inductive_val(
145    env: &mut Environment,
146    iv: &InductiveVal,
147) -> Result<(), KernelError> {
148    let mut tc = TypeChecker::new(env);
149    tc.ensure_sort(&iv.common.ty)?;
150    Ok(())
151}
152/// Validate a `ConstructorVal`: verify the constructor's type is well-formed and
153/// that it returns the parent inductive type.
154#[allow(clippy::result_large_err)]
155pub(super) fn check_constructor_val(
156    env: &mut Environment,
157    cv: &ConstructorVal,
158) -> Result<(), KernelError> {
159    {
160        let mut tc = TypeChecker::new(env);
161        tc.ensure_sort(&cv.common.ty)?;
162    }
163    if !constructor_returns_inductive(&cv.common.ty, &cv.induct) {
164        return Err(KernelError::InvalidInductive(format!(
165            "constructor `{}` does not return inductive type `{}`",
166            cv.common.name, cv.induct
167        )));
168    }
169    Ok(())
170}
171/// Validate a `RecursorVal`: verify the recursor type is well-formed.
172#[allow(clippy::result_large_err)]
173pub(super) fn check_recursor_val(
174    env: &mut Environment,
175    rv: &RecursorVal,
176) -> Result<(), KernelError> {
177    let mut tc = TypeChecker::new(env);
178    tc.ensure_sort(&rv.common.ty)?;
179    Ok(())
180}
181/// Validate a `QuotVal`: verify the quotient component type is well-formed.
182#[allow(clippy::result_large_err)]
183pub(super) fn check_quotient_val(env: &mut Environment, qv: &QuotVal) -> Result<(), KernelError> {
184    let mut tc = TypeChecker::new(env);
185    tc.ensure_sort(&qv.common.ty)?;
186    Ok(())
187}
188/// Check whether a constructor type (Pi-type) ultimately returns the named
189/// inductive type (possibly applied to arguments).
190pub(super) fn constructor_returns_inductive(ty: &crate::Expr, ind_name: &crate::Name) -> bool {
191    use crate::Expr;
192    match ty {
193        Expr::Const(n, _) => n == ind_name,
194        Expr::App(f, _) => constructor_returns_inductive(f, ind_name),
195        Expr::Pi(_, _, _, cod) => constructor_returns_inductive(cod, ind_name),
196        _ => false,
197    }
198}
199/// Summarize a declaration without checking it.
200pub fn summarize_declaration(decl: &Declaration) -> DeclSummary {
201    match decl {
202        Declaration::Axiom {
203            name, univ_params, ..
204        } => DeclSummary {
205            name: format!("{}", name),
206            kind: DeclKind::Axiom,
207            has_body: false,
208            num_univ_params: univ_params.len(),
209        },
210        Declaration::Definition {
211            name, univ_params, ..
212        } => DeclSummary {
213            name: format!("{}", name),
214            kind: DeclKind::Definition,
215            has_body: true,
216            num_univ_params: univ_params.len(),
217        },
218        Declaration::Theorem {
219            name, univ_params, ..
220        } => DeclSummary {
221            name: format!("{}", name),
222            kind: DeclKind::Theorem,
223            has_body: true,
224            num_univ_params: univ_params.len(),
225        },
226        Declaration::Opaque {
227            name, univ_params, ..
228        } => DeclSummary {
229            name: format!("{}", name),
230            kind: DeclKind::Opaque,
231            has_body: true,
232            num_univ_params: univ_params.len(),
233        },
234    }
235}
236/// Check multiple declarations, collecting all errors rather than stopping at first.
237///
238/// Unlike `check_declarations`, this function continues even after encountering
239/// errors, and returns a summary of all results.
240pub fn check_declarations_collect_errors(
241    env: &mut Environment,
242    decls: Vec<Declaration>,
243) -> BatchCheckResult {
244    let mut num_ok = 0;
245    let mut num_failed = 0;
246    let mut errors = Vec::new();
247    for decl in decls {
248        let name = format!("{}", decl.name());
249        match check_declaration(env, decl) {
250            Ok(()) => num_ok += 1,
251            Err(e) => {
252                num_failed += 1;
253                errors.push((name, format!("{:?}", e)));
254            }
255        }
256    }
257    BatchCheckResult {
258        num_ok,
259        num_failed,
260        errors,
261    }
262}
263/// Check multiple declarations and collect statistics.
264///
265/// Returns `(stats, first_error)` where `first_error` is `Some(err)` if any
266/// declaration failed, and `None` if all succeeded.
267#[allow(clippy::result_large_err)]
268pub fn check_declarations_with_stats(
269    env: &mut Environment,
270    decls: Vec<Declaration>,
271) -> (CheckStats, Option<KernelError>) {
272    let mut stats = CheckStats::new();
273    for decl in decls {
274        let kind = summarize_declaration(&decl).kind;
275        match check_declaration(env, decl) {
276            Ok(()) => match kind {
277                DeclKind::Axiom => stats.num_axioms += 1,
278                DeclKind::Definition => stats.num_definitions += 1,
279                DeclKind::Theorem => stats.num_theorems += 1,
280                DeclKind::Opaque => stats.num_opaques += 1,
281            },
282            Err(e) => {
283                stats.num_failures += 1;
284                return (stats, Some(e));
285            }
286        }
287    }
288    (stats, None)
289}
290/// Check that a declaration name is valid (non-empty, no invalid characters).
291pub fn is_valid_decl_name(name: &str) -> bool {
292    !name.is_empty()
293        && name
294            .chars()
295            .all(|c| c.is_alphanumeric() || c == '_' || c == '.' || c == '\'')
296        && !name.starts_with('.')
297        && !name.ends_with('.')
298}
299/// Check that a declaration's universe parameter list has no duplicates.
300pub fn has_unique_univ_params(params: &[crate::Name]) -> bool {
301    let mut seen = std::collections::HashSet::new();
302    params.iter().all(|p| seen.insert(format!("{}", p)))
303}
304/// Check that two universe parameter lists are compatible (same length, same names).
305pub fn univ_params_compatible(p1: &[crate::Name], p2: &[crate::Name]) -> bool {
306    p1.len() == p2.len()
307        && p1
308            .iter()
309            .zip(p2.iter())
310            .all(|(a, b)| format!("{}", a) == format!("{}", b))
311}
312/// Format a declaration summary for display.
313pub fn format_decl_summary(summary: &DeclSummary) -> String {
314    let body_str = if summary.has_body { " := ..." } else { "" };
315    let params_str = if summary.num_univ_params > 0 {
316        format!(".{{u{}}}", summary.num_univ_params)
317    } else {
318        String::new()
319    };
320    format!(
321        "{} {}{}{} : ...",
322        summary.kind, summary.name, params_str, body_str
323    )
324}
325/// Format a batch check result for display.
326pub fn format_batch_result(result: &BatchCheckResult) -> String {
327    if result.all_ok() {
328        format!("All {} declarations OK", result.total())
329    } else {
330        let mut s = format!(
331            "{}/{} declarations OK. Failures:\n",
332            result.num_ok,
333            result.total()
334        );
335        for msg in result.error_messages() {
336            s.push_str("  - ");
337            s.push_str(&msg);
338            s.push('\n');
339        }
340        s
341    }
342}
343/// Check the integrity of an environment by re-type-checking all declarations.
344///
345/// This is an expensive operation intended for debugging and testing. It verifies
346/// that every declaration in the environment is still consistent.
347pub fn verify_environment_integrity(env: &Environment) -> Vec<String> {
348    let mut issues = Vec::new();
349    for name in env
350        .constant_names()
351        .cloned()
352        .collect::<Vec<_>>()
353        .into_iter()
354    {
355        if let Some(info) = env.get(&name) {
356            let ty = info.ty();
357            if !is_structurally_valid_expr(ty) {
358                issues.push(format!("{}: type is not structurally valid", name));
359            }
360        }
361    }
362    issues
363}
364/// Perform a basic structural validity check on an expression.
365///
366/// This checks that bound variable indices are in range, but does not
367/// perform full type checking.
368pub fn is_structurally_valid_expr(expr: &crate::Expr) -> bool {
369    check_expr_bvars(expr, 0)
370}
371pub(super) fn check_expr_bvars(expr: &crate::Expr, depth: u32) -> bool {
372    use crate::Expr;
373    match expr {
374        Expr::BVar(i) => *i < depth,
375        Expr::FVar(_) | Expr::Sort(_) | Expr::Const(_, _) | Expr::Lit(_) => true,
376        Expr::App(f, a) => check_expr_bvars(f, depth) && check_expr_bvars(a, depth),
377        Expr::Lam(_, _, ty, body) | Expr::Pi(_, _, ty, body) => {
378            check_expr_bvars(ty, depth) && check_expr_bvars(body, depth + 1)
379        }
380        Expr::Let(_, ty, val, body) => {
381            check_expr_bvars(ty, depth)
382                && check_expr_bvars(val, depth)
383                && check_expr_bvars(body, depth + 1)
384        }
385        Expr::Proj(_, _, e) => check_expr_bvars(e, depth),
386    }
387}
388/// Collect the names of all constants referenced in a declaration.
389///
390/// This includes references in both the type and the value (if present).
391pub fn declaration_dependencies(decl: &Declaration) -> Vec<crate::Name> {
392    use crate::collect_const_names;
393    let mut deps = collect_const_names(decl.ty());
394    if let Some(val) = decl.value() {
395        deps.extend(collect_const_names(val));
396    }
397    deps.sort_by(|a, b| format!("{}", a).cmp(&format!("{}", b)));
398    deps.dedup_by(|a, b| format!("{}", a) == format!("{}", b));
399    deps
400}
401/// Check that all dependencies of a declaration exist in the environment.
402///
403/// Returns the names of any missing dependencies.
404pub fn check_dependencies_exist(env: &Environment, decl: &Declaration) -> Vec<crate::Name> {
405    let deps = declaration_dependencies(decl);
406    deps.into_iter()
407        .filter(|name| env.get(name).is_none())
408        .collect()
409}
410#[cfg(test)]
411mod tests {
412    use super::*;
413    use crate::{Level, Literal, ReducibilityHint};
414    fn mk_type0() -> Expr {
415        Expr::Sort(Level::succ(Level::zero()))
416    }
417    fn mk_nat_axiom() -> Declaration {
418        Declaration::Axiom {
419            name: Name::str("Nat"),
420            univ_params: vec![],
421            ty: mk_type0(),
422        }
423    }
424    fn mk_nat_const() -> Expr {
425        Expr::Const(Name::str("Nat"), vec![])
426    }
427    #[test]
428    fn test_check_axiom() {
429        let mut env = Environment::new();
430        let nat_ty = Expr::Sort(Level::succ(Level::zero()));
431        let axiom = Declaration::Axiom {
432            name: Name::str("Nat"),
433            univ_params: vec![],
434            ty: nat_ty,
435        };
436        check_declaration(&mut env, axiom).expect("value should be present");
437        assert!(env.contains(&Name::str("Nat")));
438    }
439    #[test]
440    fn test_check_definition() {
441        let mut env = Environment::new();
442        env.add(mk_nat_axiom()).expect("value should be present");
443        let nat_ty = mk_nat_const();
444        let val = Expr::Lit(Literal::Nat(42));
445        let def = Declaration::Definition {
446            name: Name::str("answer"),
447            univ_params: vec![],
448            ty: nat_ty,
449            val,
450            hint: ReducibilityHint::Regular(1),
451        };
452        check_declaration(&mut env, def).expect("value should be present");
453        assert!(env.contains(&Name::str("answer")));
454    }
455    #[test]
456    fn test_type_mismatch() {
457        let mut env = Environment::new();
458        let type0 = mk_type0();
459        env.add(Declaration::Axiom {
460            name: Name::str("String"),
461            univ_params: vec![],
462            ty: type0.clone(),
463        })
464        .expect("value should be present");
465        env.add(Declaration::Axiom {
466            name: Name::str("Nat"),
467            univ_params: vec![],
468            ty: type0,
469        })
470        .expect("value should be present");
471        let string_ty = Expr::Const(Name::str("String"), vec![]);
472        let val = Expr::Lit(Literal::Nat(42));
473        let def = Declaration::Definition {
474            name: Name::str("bad"),
475            univ_params: vec![],
476            ty: string_ty,
477            val,
478            hint: ReducibilityHint::Regular(1),
479        };
480        let result = check_declaration(&mut env, def);
481        assert!(result.is_err());
482    }
483    #[test]
484    fn test_check_declarations_sequence() {
485        let mut env = Environment::new();
486        let decls = vec![
487            Declaration::Axiom {
488                name: Name::str("A"),
489                univ_params: vec![],
490                ty: mk_type0(),
491            },
492            Declaration::Axiom {
493                name: Name::str("B"),
494                univ_params: vec![],
495                ty: mk_type0(),
496            },
497        ];
498        check_declarations(&mut env, decls).expect("value should be present");
499        assert!(env.contains(&Name::str("A")));
500        assert!(env.contains(&Name::str("B")));
501    }
502    #[test]
503    fn test_decl_kind_display() {
504        assert_eq!(DeclKind::Axiom.as_str(), "axiom");
505        assert_eq!(DeclKind::Definition.as_str(), "def");
506        assert_eq!(DeclKind::Theorem.as_str(), "theorem");
507        assert_eq!(DeclKind::Opaque.as_str(), "opaque");
508        assert!(DeclKind::Theorem.is_proven());
509        assert!(DeclKind::Axiom.is_assumed());
510        assert!(DeclKind::Definition.is_definition());
511        assert!(!DeclKind::Axiom.is_definition());
512    }
513    #[test]
514    fn test_summarize_declaration() {
515        let decl = mk_nat_axiom();
516        let summary = summarize_declaration(&decl);
517        assert_eq!(summary.name, "Nat");
518        assert_eq!(summary.kind, DeclKind::Axiom);
519        assert!(!summary.has_body);
520        assert_eq!(summary.num_univ_params, 0);
521    }
522    #[test]
523    fn test_is_valid_decl_name() {
524        assert!(is_valid_decl_name("Nat"));
525        assert!(is_valid_decl_name("Nat.succ"));
526        assert!(is_valid_decl_name("foo_bar"));
527        assert!(!is_valid_decl_name(""));
528        assert!(!is_valid_decl_name(".leading_dot"));
529        assert!(!is_valid_decl_name("trailing_dot."));
530    }
531    #[test]
532    fn test_has_unique_univ_params() {
533        let u = Name::str("u");
534        let v = Name::str("v");
535        let params = vec![u.clone(), v.clone()];
536        assert!(has_unique_univ_params(&params));
537        let dup_params = vec![u.clone(), u.clone()];
538        assert!(!has_unique_univ_params(&dup_params));
539    }
540    #[test]
541    fn test_check_config_default() {
542        let cfg = CheckConfig::default();
543        assert!(cfg.check_type_is_sort);
544        assert!(cfg.check_value_type);
545        assert!(cfg.check_no_free_vars);
546    }
547    #[test]
548    fn test_check_config_lenient() {
549        let cfg = CheckConfig::lenient();
550        assert!(cfg.check_type_is_sort);
551        assert!(!cfg.check_value_type);
552    }
553    #[test]
554    fn test_check_config_strict() {
555        let cfg = CheckConfig::strict();
556        assert!(!cfg.allow_axioms);
557        assert!(cfg.max_depth > 0);
558    }
559    #[test]
560    fn test_batch_check_all_ok() {
561        let mut env = Environment::new();
562        let decls = vec![
563            Declaration::Axiom {
564                name: Name::str("X"),
565                univ_params: vec![],
566                ty: mk_type0(),
567            },
568            Declaration::Axiom {
569                name: Name::str("Y"),
570                univ_params: vec![],
571                ty: mk_type0(),
572            },
573        ];
574        let result = check_declarations_collect_errors(&mut env, decls);
575        assert!(result.all_ok());
576        assert_eq!(result.num_ok, 2);
577        assert_eq!(result.num_failed, 0);
578    }
579    #[test]
580    fn test_batch_check_with_error() {
581        let mut env = Environment::new();
582        let decls = vec![
583            Declaration::Axiom {
584                name: Name::str("M"),
585                univ_params: vec![],
586                ty: mk_type0(),
587            },
588            Declaration::Definition {
589                name: Name::str("bad_def"),
590                univ_params: vec![],
591                ty: Expr::Const(Name::str("UndefinedType"), vec![]),
592                val: Expr::Lit(Literal::Nat(0)),
593                hint: ReducibilityHint::Regular(1),
594            },
595        ];
596        let result = check_declarations_collect_errors(&mut env, decls);
597        assert!(!result.all_ok());
598        assert_eq!(result.num_ok, 1);
599        assert_eq!(result.num_failed, 1);
600    }
601    #[test]
602    fn test_env_builder_clean() {
603        let mut builder = EnvBuilder::new();
604        let added = builder.add(Declaration::Axiom {
605            name: Name::str("P"),
606            univ_params: vec![],
607            ty: mk_type0(),
608        });
609        assert!(added);
610        assert!(builder.is_clean());
611        assert_eq!(builder.stats().num_axioms, 1);
612    }
613    #[test]
614    fn test_env_builder_with_error() {
615        let mut builder = EnvBuilder::new();
616        let added = builder.add(Declaration::Definition {
617            name: Name::str("oops"),
618            univ_params: vec![],
619            ty: Expr::Const(Name::str("NoSuchType"), vec![]),
620            val: Expr::Lit(Literal::Nat(0)),
621            hint: ReducibilityHint::Regular(1),
622        });
623        assert!(!added);
624        assert!(!builder.is_clean());
625        assert_eq!(builder.errors().len(), 1);
626    }
627    #[test]
628    fn test_well_formed_result_display() {
629        let ok = WellFormedResult::Ok;
630        assert!(ok.is_ok());
631        assert_eq!(ok.description(), "well-formed");
632        let mismatch = WellFormedResult::TypeMismatch {
633            description: "Nat vs String".to_string(),
634        };
635        assert!(!mismatch.is_ok());
636        assert!(mismatch.description().contains("Nat vs String"));
637    }
638    #[test]
639    fn test_is_structurally_valid_expr() {
640        let bad = Expr::BVar(0);
641        assert!(!is_structurally_valid_expr(&bad));
642        let sort = Expr::Sort(Level::zero());
643        assert!(is_structurally_valid_expr(&sort));
644        let lam = Expr::Lam(
645            crate::BinderInfo::Default,
646            Name::str("x"),
647            Box::new(Expr::Sort(Level::zero())),
648            Box::new(Expr::BVar(0)),
649        );
650        assert!(is_structurally_valid_expr(&lam));
651    }
652    #[test]
653    fn test_format_decl_summary() {
654        let summary = DeclSummary {
655            name: "Nat.add".to_string(),
656            kind: DeclKind::Definition,
657            has_body: true,
658            num_univ_params: 0,
659        };
660        let s = format_decl_summary(&summary);
661        assert!(s.contains("Nat.add"));
662        assert!(s.contains("def"));
663    }
664    #[test]
665    fn test_check_stats_totals() {
666        let stats = CheckStats {
667            num_axioms: 2,
668            num_definitions: 3,
669            num_theorems: 1,
670            num_opaques: 0,
671            num_failures: 1,
672        };
673        assert_eq!(stats.total(), 6);
674        assert_eq!(stats.num_ok(), 6);
675    }
676    #[test]
677    fn test_format_batch_result_all_ok() {
678        let result = BatchCheckResult {
679            num_ok: 3,
680            num_failed: 0,
681            errors: vec![],
682        };
683        let s = format_batch_result(&result);
684        assert!(s.contains("3"));
685    }
686    #[test]
687    fn test_temp_env_scope() {
688        let mut env = Environment::new();
689        {
690            let mut scope = TempEnvScope::new(&mut env);
691            let ok = scope.add(Declaration::Axiom {
692                name: Name::str("TempDecl"),
693                univ_params: vec![],
694                ty: mk_type0(),
695            });
696            assert!(ok.is_ok());
697            assert_eq!(scope.num_added(), 1);
698        }
699        assert!(env.contains(&Name::str("TempDecl")));
700    }
701    #[allow(dead_code)]
702    fn mk_type1() -> Expr {
703        Expr::Sort(Level::succ(Level::succ(Level::zero())))
704    }
705    #[test]
706    fn test_check_constant_info_axiom() {
707        use crate::declaration::{AxiomVal, ConstantVal};
708        let mut env = Environment::new();
709        let ci = ConstantInfo::Axiom(AxiomVal {
710            common: ConstantVal {
711                name: Name::str("MyAxiom"),
712                level_params: vec![],
713                ty: mk_type0(),
714            },
715            is_unsafe: false,
716        });
717        check_constant_info(&mut env, ci).expect("value should be present");
718        assert!(env.contains(&Name::str("MyAxiom")));
719    }
720    #[test]
721    fn test_check_constant_info_inductive_simple() {
722        use crate::declaration::{ConstantVal, InductiveVal};
723        let mut env = Environment::new();
724        let iv = InductiveVal {
725            common: ConstantVal {
726                name: Name::str("Bool"),
727                level_params: vec![],
728                ty: mk_type0(),
729            },
730            num_params: 0,
731            num_indices: 0,
732            all: vec![Name::str("Bool")],
733            ctors: vec![Name::str("Bool.true"), Name::str("Bool.false")],
734            num_nested: 0,
735            is_rec: false,
736            is_unsafe: false,
737            is_reflexive: false,
738            is_prop: false,
739        };
740        let ci = ConstantInfo::Inductive(iv);
741        check_constant_info(&mut env, ci).expect("value should be present");
742        assert!(env.contains(&Name::str("Bool")));
743    }
744    #[test]
745    fn test_check_constant_info_inductive_empty() {
746        use crate::declaration::{ConstantVal, InductiveVal};
747        let mut env = Environment::new();
748        let iv = InductiveVal {
749            common: ConstantVal {
750                name: Name::str("Empty"),
751                level_params: vec![],
752                ty: mk_type0(),
753            },
754            num_params: 0,
755            num_indices: 0,
756            all: vec![Name::str("Empty")],
757            ctors: vec![],
758            num_nested: 0,
759            is_rec: false,
760            is_unsafe: false,
761            is_reflexive: false,
762            is_prop: false,
763        };
764        let ci = ConstantInfo::Inductive(iv);
765        check_constant_info(&mut env, ci).expect("value should be present");
766        assert!(env.contains(&Name::str("Empty")));
767    }
768    #[test]
769    fn test_check_constant_info_constructor_valid() {
770        use crate::declaration::{ConstantVal, ConstructorVal, InductiveVal};
771        let mut env = Environment::new();
772        let ind_ci = ConstantInfo::Inductive(InductiveVal {
773            common: ConstantVal {
774                name: Name::str("Bool"),
775                level_params: vec![],
776                ty: mk_type0(),
777            },
778            num_params: 0,
779            num_indices: 0,
780            all: vec![Name::str("Bool")],
781            ctors: vec![Name::str("Bool.true")],
782            num_nested: 0,
783            is_rec: false,
784            is_unsafe: false,
785            is_reflexive: false,
786            is_prop: false,
787        });
788        check_constant_info(&mut env, ind_ci).expect("value should be present");
789        let ctor_ci = ConstantInfo::Constructor(ConstructorVal {
790            common: ConstantVal {
791                name: Name::str("Bool.true"),
792                level_params: vec![],
793                ty: Expr::Const(Name::str("Bool"), vec![]),
794            },
795            induct: Name::str("Bool"),
796            cidx: 0,
797            num_params: 0,
798            num_fields: 0,
799            is_unsafe: false,
800        });
801        check_constant_info(&mut env, ctor_ci).expect("value should be present");
802        assert!(env.contains(&Name::str("Bool.true")));
803    }
804    #[test]
805    fn test_check_constant_info_constructor_wrong_return_type() {
806        use crate::declaration::{ConstantVal, ConstructorVal, InductiveVal};
807        let mut env = Environment::new();
808        env.add_constant(ConstantInfo::Inductive(InductiveVal {
809            common: ConstantVal {
810                name: Name::str("Bool"),
811                level_params: vec![],
812                ty: mk_type0(),
813            },
814            num_params: 0,
815            num_indices: 0,
816            all: vec![Name::str("Bool")],
817            ctors: vec![Name::str("Bool.bad")],
818            num_nested: 0,
819            is_rec: false,
820            is_unsafe: false,
821            is_reflexive: false,
822            is_prop: false,
823        }))
824        .expect("value should be present");
825        env.add_constant(ConstantInfo::Inductive(InductiveVal {
826            common: ConstantVal {
827                name: Name::str("Nat"),
828                level_params: vec![],
829                ty: mk_type0(),
830            },
831            num_params: 0,
832            num_indices: 0,
833            all: vec![Name::str("Nat")],
834            ctors: vec![],
835            num_nested: 0,
836            is_rec: false,
837            is_unsafe: false,
838            is_reflexive: false,
839            is_prop: false,
840        }))
841        .expect("value should be present");
842        let ctor_ci = ConstantInfo::Constructor(ConstructorVal {
843            common: ConstantVal {
844                name: Name::str("Bool.bad"),
845                level_params: vec![],
846                ty: Expr::Const(Name::str("Nat"), vec![]),
847            },
848            induct: Name::str("Bool"),
849            cidx: 0,
850            num_params: 0,
851            num_fields: 0,
852            is_unsafe: false,
853        });
854        let result = check_constant_info(&mut env, ctor_ci);
855        assert!(result.is_err(), "expected error for wrong return type");
856    }
857    #[test]
858    fn test_check_constant_info_recursor() {
859        use crate::declaration::{ConstantVal, InductiveVal, RecursorVal};
860        let mut env = Environment::new();
861        env.add_constant(ConstantInfo::Inductive(InductiveVal {
862            common: ConstantVal {
863                name: Name::str("Bool"),
864                level_params: vec![],
865                ty: mk_type0(),
866            },
867            num_params: 0,
868            num_indices: 0,
869            all: vec![Name::str("Bool")],
870            ctors: vec![],
871            num_nested: 0,
872            is_rec: false,
873            is_unsafe: false,
874            is_reflexive: false,
875            is_prop: false,
876        }))
877        .expect("value should be present");
878        let rec_ty = mk_type0();
879        let rec_ci = ConstantInfo::Recursor(RecursorVal {
880            common: ConstantVal {
881                name: Name::str("Bool.rec"),
882                level_params: vec![],
883                ty: rec_ty,
884            },
885            all: vec![Name::str("Bool")],
886            num_params: 0,
887            num_indices: 0,
888            num_motives: 1,
889            num_minors: 2,
890            rules: vec![],
891            k: false,
892            is_unsafe: false,
893        });
894        check_constant_info(&mut env, rec_ci).expect("value should be present");
895        assert!(env.contains(&Name::str("Bool.rec")));
896    }
897    #[test]
898    fn test_check_constant_info_quotient() {
899        use crate::declaration::{ConstantVal, QuotKind, QuotVal};
900        let mut env = Environment::new();
901        let quot_ci = ConstantInfo::Quotient(QuotVal {
902            common: ConstantVal {
903                name: Name::str("Quot"),
904                level_params: vec![],
905                ty: mk_type0(),
906            },
907            kind: QuotKind::Type,
908        });
909        check_constant_info(&mut env, quot_ci).expect("value should be present");
910        assert!(env.contains(&Name::str("Quot")));
911    }
912    #[test]
913    fn test_check_constant_infos_sequence() {
914        use crate::declaration::{AxiomVal, ConstantVal};
915        let mut env = Environment::new();
916        let cis = vec![
917            ConstantInfo::Axiom(AxiomVal {
918                common: ConstantVal {
919                    name: Name::str("P"),
920                    level_params: vec![],
921                    ty: mk_type0(),
922                },
923                is_unsafe: false,
924            }),
925            ConstantInfo::Axiom(AxiomVal {
926                common: ConstantVal {
927                    name: Name::str("Q"),
928                    level_params: vec![],
929                    ty: mk_type0(),
930                },
931                is_unsafe: false,
932            }),
933        ];
934        check_constant_infos(&mut env, cis).expect("value should be present");
935        assert!(env.contains(&Name::str("P")));
936        assert!(env.contains(&Name::str("Q")));
937    }
938    #[test]
939    fn test_check_constant_info_duplicate() {
940        use crate::declaration::{AxiomVal, ConstantVal};
941        let mut env = Environment::new();
942        let make_ci = || {
943            ConstantInfo::Axiom(AxiomVal {
944                common: ConstantVal {
945                    name: Name::str("Dup"),
946                    level_params: vec![],
947                    ty: mk_type0(),
948                },
949                is_unsafe: false,
950            })
951        };
952        check_constant_info(&mut env, make_ci()).expect("value should be present");
953        let result = check_constant_info(&mut env, make_ci());
954        assert!(result.is_err(), "duplicate should fail");
955    }
956}
957#[cfg(test)]
958mod tests_padding_infra {
959    use super::*;
960    #[test]
961    fn test_stat_summary() {
962        let mut ss = StatSummary::new();
963        ss.record(10.0);
964        ss.record(20.0);
965        ss.record(30.0);
966        assert_eq!(ss.count(), 3);
967        assert!((ss.mean().expect("mean should succeed") - 20.0).abs() < 1e-9);
968        assert_eq!(ss.min().expect("min should succeed") as i64, 10);
969        assert_eq!(ss.max().expect("max should succeed") as i64, 30);
970    }
971    #[test]
972    fn test_transform_stat() {
973        let mut ts = TransformStat::new();
974        ts.record_before(100.0);
975        ts.record_after(80.0);
976        let ratio = ts.mean_ratio().expect("ratio should be present");
977        assert!((ratio - 0.8).abs() < 1e-9);
978    }
979    #[test]
980    fn test_small_map() {
981        let mut m: SmallMap<u32, &str> = SmallMap::new();
982        m.insert(3, "three");
983        m.insert(1, "one");
984        m.insert(2, "two");
985        assert_eq!(m.get(&2), Some(&"two"));
986        assert_eq!(m.len(), 3);
987        let keys = m.keys();
988        assert_eq!(*keys[0], 1);
989        assert_eq!(*keys[2], 3);
990    }
991    #[test]
992    fn test_label_set() {
993        let mut ls = LabelSet::new();
994        ls.add("foo");
995        ls.add("bar");
996        ls.add("foo");
997        assert_eq!(ls.count(), 2);
998        assert!(ls.has("bar"));
999        assert!(!ls.has("baz"));
1000    }
1001    #[test]
1002    fn test_config_node() {
1003        let mut root = ConfigNode::section("root");
1004        let child = ConfigNode::leaf("key", "value");
1005        root.add_child(child);
1006        assert_eq!(root.num_children(), 1);
1007    }
1008    #[test]
1009    fn test_versioned_record() {
1010        let mut vr = VersionedRecord::new(0u32);
1011        vr.update(1);
1012        vr.update(2);
1013        assert_eq!(*vr.current(), 2);
1014        assert_eq!(vr.version(), 2);
1015        assert!(vr.has_history());
1016        assert_eq!(*vr.at_version(0).expect("value should be present"), 0);
1017    }
1018    #[test]
1019    fn test_simple_dag() {
1020        let mut dag = SimpleDag::new(4);
1021        dag.add_edge(0, 1);
1022        dag.add_edge(1, 2);
1023        dag.add_edge(2, 3);
1024        assert!(dag.can_reach(0, 3));
1025        assert!(!dag.can_reach(3, 0));
1026        let order = dag.topological_sort().expect("order should be present");
1027        assert_eq!(order, vec![0, 1, 2, 3]);
1028    }
1029    #[test]
1030    fn test_focus_stack() {
1031        let mut fs: FocusStack<&str> = FocusStack::new();
1032        fs.focus("a");
1033        fs.focus("b");
1034        assert_eq!(fs.current(), Some(&"b"));
1035        assert_eq!(fs.depth(), 2);
1036        fs.blur();
1037        assert_eq!(fs.current(), Some(&"a"));
1038    }
1039}
1040#[cfg(test)]
1041mod tests_extra_iterators {
1042    use super::*;
1043    #[test]
1044    fn test_window_iterator() {
1045        let data = vec![1u32, 2, 3, 4, 5];
1046        let windows: Vec<_> = WindowIterator::new(&data, 3).collect();
1047        assert_eq!(windows.len(), 3);
1048        assert_eq!(windows[0], &[1, 2, 3]);
1049        assert_eq!(windows[2], &[3, 4, 5]);
1050    }
1051    #[test]
1052    fn test_non_empty_vec() {
1053        let mut nev = NonEmptyVec::singleton(10u32);
1054        nev.push(20);
1055        nev.push(30);
1056        assert_eq!(nev.len(), 3);
1057        assert_eq!(*nev.first(), 10);
1058        assert_eq!(*nev.last(), 30);
1059    }
1060}
1061#[cfg(test)]
1062mod tests_padding2 {
1063    use super::*;
1064    #[test]
1065    fn test_sliding_sum() {
1066        let mut ss = SlidingSum::new(3);
1067        ss.push(1.0);
1068        ss.push(2.0);
1069        ss.push(3.0);
1070        assert!((ss.sum() - 6.0).abs() < 1e-9);
1071        ss.push(4.0);
1072        assert!((ss.sum() - 9.0).abs() < 1e-9);
1073        assert_eq!(ss.count(), 3);
1074    }
1075    #[test]
1076    fn test_path_buf() {
1077        let mut pb = PathBuf::new();
1078        pb.push("src");
1079        pb.push("main");
1080        assert_eq!(pb.as_str(), "src/main");
1081        assert_eq!(pb.depth(), 2);
1082        pb.pop();
1083        assert_eq!(pb.as_str(), "src");
1084    }
1085    #[test]
1086    fn test_string_pool() {
1087        let mut pool = StringPool::new();
1088        let s = pool.take();
1089        assert!(s.is_empty());
1090        pool.give("hello".to_string());
1091        let s2 = pool.take();
1092        assert!(s2.is_empty());
1093        assert_eq!(pool.free_count(), 0);
1094    }
1095    #[test]
1096    fn test_transitive_closure() {
1097        let mut tc = TransitiveClosure::new(4);
1098        tc.add_edge(0, 1);
1099        tc.add_edge(1, 2);
1100        tc.add_edge(2, 3);
1101        assert!(tc.can_reach(0, 3));
1102        assert!(!tc.can_reach(3, 0));
1103        let r = tc.reachable_from(0);
1104        assert_eq!(r.len(), 4);
1105    }
1106    #[test]
1107    fn test_token_bucket() {
1108        let mut tb = TokenBucket::new(100, 10);
1109        assert_eq!(tb.available(), 100);
1110        assert!(tb.try_consume(50));
1111        assert_eq!(tb.available(), 50);
1112        assert!(!tb.try_consume(60));
1113        assert_eq!(tb.capacity(), 100);
1114    }
1115    #[test]
1116    fn test_rewrite_rule_set() {
1117        let mut rrs = RewriteRuleSet::new();
1118        rrs.add(RewriteRule::unconditional(
1119            "beta",
1120            "App(Lam(x, b), v)",
1121            "b[x:=v]",
1122        ));
1123        rrs.add(RewriteRule::conditional("comm", "a + b", "b + a"));
1124        assert_eq!(rrs.len(), 2);
1125        assert_eq!(rrs.unconditional_rules().len(), 1);
1126        assert_eq!(rrs.conditional_rules().len(), 1);
1127        assert!(rrs.get("beta").is_some());
1128        let disp = rrs
1129            .get("beta")
1130            .expect("element at \'beta\' should exist")
1131            .display();
1132        assert!(disp.contains("→"));
1133    }
1134}
1135#[cfg(test)]
1136mod tests_padding3 {
1137    use super::*;
1138    #[test]
1139    fn test_decision_node() {
1140        let tree = DecisionNode::Branch {
1141            key: "x".into(),
1142            val: "1".into(),
1143            yes_branch: Box::new(DecisionNode::Leaf("yes".into())),
1144            no_branch: Box::new(DecisionNode::Leaf("no".into())),
1145        };
1146        let mut ctx = std::collections::HashMap::new();
1147        ctx.insert("x".into(), "1".into());
1148        assert_eq!(tree.evaluate(&ctx), "yes");
1149        ctx.insert("x".into(), "2".into());
1150        assert_eq!(tree.evaluate(&ctx), "no");
1151        assert_eq!(tree.depth(), 1);
1152    }
1153    #[test]
1154    fn test_flat_substitution() {
1155        let mut sub = FlatSubstitution::new();
1156        sub.add("foo", "bar");
1157        sub.add("baz", "qux");
1158        assert_eq!(sub.apply("foo and baz"), "bar and qux");
1159        assert_eq!(sub.len(), 2);
1160    }
1161    #[test]
1162    fn test_stopwatch() {
1163        let mut sw = Stopwatch::start();
1164        sw.split();
1165        sw.split();
1166        assert_eq!(sw.num_splits(), 2);
1167        assert!(sw.elapsed_ms() >= 0.0);
1168        for &s in sw.splits() {
1169            assert!(s >= 0.0);
1170        }
1171    }
1172    #[test]
1173    fn test_either2() {
1174        let e: Either2<i32, &str> = Either2::First(42);
1175        assert!(e.is_first());
1176        let mapped = e.map_first(|x| x * 2);
1177        assert_eq!(mapped.first(), Some(84));
1178        let e2: Either2<i32, &str> = Either2::Second("hello");
1179        assert!(e2.is_second());
1180        assert_eq!(e2.second(), Some("hello"));
1181    }
1182    #[test]
1183    fn test_write_once() {
1184        let wo: WriteOnce<u32> = WriteOnce::new();
1185        assert!(!wo.is_written());
1186        assert!(wo.write(42));
1187        assert!(!wo.write(99));
1188        assert_eq!(wo.read(), Some(42));
1189    }
1190    #[test]
1191    fn test_sparse_vec() {
1192        let mut sv: SparseVec<i32> = SparseVec::new(100);
1193        sv.set(5, 10);
1194        sv.set(50, 20);
1195        assert_eq!(*sv.get(5), 10);
1196        assert_eq!(*sv.get(50), 20);
1197        assert_eq!(*sv.get(0), 0);
1198        assert_eq!(sv.nnz(), 2);
1199        sv.set(5, 0);
1200        assert_eq!(sv.nnz(), 1);
1201    }
1202    #[test]
1203    fn test_stack_calc() {
1204        let mut calc = StackCalc::new();
1205        calc.push(3);
1206        calc.push(4);
1207        calc.add();
1208        assert_eq!(calc.peek(), Some(7));
1209        calc.push(2);
1210        calc.mul();
1211        assert_eq!(calc.peek(), Some(14));
1212    }
1213}
oxilean_kernel/check/functions.rs

oxilean_kernel/check/
functions.rs
