oxilean_kernel/inductive/
types.rs

1//! Auto-generated module
2//!
3//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)
4
5use super::functions::*;
6use crate::declaration::{
7    ConstantInfo, ConstantVal, ConstructorVal, InductiveVal, RecursorRule, RecursorVal,
8};
9use crate::{Expr, KernelError, Level, Name};
10use std::collections::HashMap;
11
12/// A generic counter that tracks min/max/sum for statistical summaries.
13#[allow(dead_code)]
14pub struct StatSummary {
15    count: u64,
16    sum: f64,
17    min: f64,
18    max: f64,
19}
20#[allow(dead_code)]
21impl StatSummary {
22    /// Creates an empty summary.
23    pub fn new() -> Self {
24        Self {
25            count: 0,
26            sum: 0.0,
27            min: f64::INFINITY,
28            max: f64::NEG_INFINITY,
29        }
30    }
31    /// Records a sample.
32    pub fn record(&mut self, val: f64) {
33        self.count += 1;
34        self.sum += val;
35        if val < self.min {
36            self.min = val;
37        }
38        if val > self.max {
39            self.max = val;
40        }
41    }
42    /// Returns the mean, or `None` if no samples.
43    pub fn mean(&self) -> Option<f64> {
44        if self.count == 0 {
45            None
46        } else {
47            Some(self.sum / self.count as f64)
48        }
49    }
50    /// Returns the minimum, or `None` if no samples.
51    pub fn min(&self) -> Option<f64> {
52        if self.count == 0 {
53            None
54        } else {
55            Some(self.min)
56        }
57    }
58    /// Returns the maximum, or `None` if no samples.
59    pub fn max(&self) -> Option<f64> {
60        if self.count == 0 {
61            None
62        } else {
63            Some(self.max)
64        }
65    }
66    /// Returns the count of recorded samples.
67    pub fn count(&self) -> u64 {
68        self.count
69    }
70}
71/// Errors that can occur when checking an inductive type definition.
72#[derive(Clone, Debug, PartialEq)]
73pub enum InductiveError {
74    /// The type name is already defined.
75    AlreadyDefined(Name),
76    /// A constructor references a type that is not in scope.
77    UndefinedType(Name),
78    /// A constructor has an invalid type (not a Pi ending in the inductive type).
79    InvalidConstructorType(Name),
80    /// The universe level is not large enough.
81    UniverseTooSmall(String),
82    /// A non-strictly positive occurrence of the type.
83    NonStrictlyPositive(Name),
84    /// General error.
85    Other(String),
86}
87/// An introduction rule (constructor) for an inductive type.
88#[derive(Clone, Debug, PartialEq)]
89pub struct IntroRule {
90    /// Constructor name
91    pub name: Name,
92    /// Constructor type (as a Pi-type)
93    pub ty: Expr,
94}
95/// A mutually inductive family of types.
96///
97/// Lean 4 supports mutual induction (e.g., `Even` and `Odd` defined together).
98/// This struct holds a group of inductive types that are checked together.
99#[derive(Clone, Debug)]
100pub struct InductiveFamily {
101    /// The inductive types in the family.
102    pub types: Vec<InductiveType>,
103    /// Shared universe parameters.
104    pub univ_params: Vec<Name>,
105}
106impl InductiveFamily {
107    /// Create a single-type family.
108    pub fn singleton(ty: InductiveType) -> Self {
109        let univ_params = ty.univ_params.clone();
110        Self {
111            types: vec![ty],
112            univ_params,
113        }
114    }
115    /// Create a mutually inductive family.
116    pub fn new(types: Vec<InductiveType>, univ_params: Vec<Name>) -> Self {
117        Self { types, univ_params }
118    }
119    /// Number of types in the family.
120    pub fn len(&self) -> usize {
121        self.types.len()
122    }
123    /// Whether the family contains a single type.
124    pub fn is_singleton(&self) -> bool {
125        self.types.len() == 1
126    }
127    /// Whether the family is empty.
128    pub fn is_empty(&self) -> bool {
129        self.types.is_empty()
130    }
131    /// All type names in the family.
132    pub fn type_names(&self) -> Vec<&Name> {
133        self.types.iter().map(|t| &t.name).collect()
134    }
135    /// All constructor names across all types.
136    pub fn all_constructor_names(&self) -> Vec<&Name> {
137        self.types
138            .iter()
139            .flat_map(|t| t.intro_rules.iter().map(|r| &r.name))
140            .collect()
141    }
142    /// Find a type by name.
143    pub fn find_type(&self, name: &Name) -> Option<&InductiveType> {
144        self.types.iter().find(|t| &t.name == name)
145    }
146    /// Total number of constructors across all types.
147    pub fn total_constructors(&self) -> usize {
148        self.types.iter().map(|t| t.intro_rules.len()).sum()
149    }
150}
151/// A simple key-value store backed by a sorted Vec for small maps.
152#[allow(dead_code)]
153pub struct SmallMap<K: Ord + Clone, V: Clone> {
154    entries: Vec<(K, V)>,
155}
156#[allow(dead_code)]
157impl<K: Ord + Clone, V: Clone> SmallMap<K, V> {
158    /// Creates a new empty small map.
159    pub fn new() -> Self {
160        Self {
161            entries: Vec::new(),
162        }
163    }
164    /// Inserts or replaces the value for `key`.
165    pub fn insert(&mut self, key: K, val: V) {
166        match self.entries.binary_search_by_key(&&key, |(k, _)| k) {
167            Ok(i) => self.entries[i].1 = val,
168            Err(i) => self.entries.insert(i, (key, val)),
169        }
170    }
171    /// Returns the value for `key`, or `None`.
172    pub fn get(&self, key: &K) -> Option<&V> {
173        self.entries
174            .binary_search_by_key(&key, |(k, _)| k)
175            .ok()
176            .map(|i| &self.entries[i].1)
177    }
178    /// Returns the number of entries.
179    pub fn len(&self) -> usize {
180        self.entries.len()
181    }
182    /// Returns `true` if empty.
183    pub fn is_empty(&self) -> bool {
184        self.entries.is_empty()
185    }
186    /// Returns all keys.
187    pub fn keys(&self) -> Vec<&K> {
188        self.entries.iter().map(|(k, _)| k).collect()
189    }
190    /// Returns all values.
191    pub fn values(&self) -> Vec<&V> {
192        self.entries.iter().map(|(_, v)| v).collect()
193    }
194}
195/// A hierarchical configuration tree.
196#[allow(dead_code)]
197pub struct ConfigNode {
198    key: String,
199    value: Option<String>,
200    children: Vec<ConfigNode>,
201}
202#[allow(dead_code)]
203impl ConfigNode {
204    /// Creates a leaf config node with a value.
205    pub fn leaf(key: impl Into<String>, value: impl Into<String>) -> Self {
206        Self {
207            key: key.into(),
208            value: Some(value.into()),
209            children: Vec::new(),
210        }
211    }
212    /// Creates a section node with children.
213    pub fn section(key: impl Into<String>) -> Self {
214        Self {
215            key: key.into(),
216            value: None,
217            children: Vec::new(),
218        }
219    }
220    /// Adds a child node.
221    pub fn add_child(&mut self, child: ConfigNode) {
222        self.children.push(child);
223    }
224    /// Returns the key.
225    pub fn key(&self) -> &str {
226        &self.key
227    }
228    /// Returns the value, or `None` for section nodes.
229    pub fn value(&self) -> Option<&str> {
230        self.value.as_deref()
231    }
232    /// Returns the number of children.
233    pub fn num_children(&self) -> usize {
234        self.children.len()
235    }
236    /// Looks up a dot-separated path.
237    pub fn lookup(&self, path: &str) -> Option<&str> {
238        let mut parts = path.splitn(2, '.');
239        let head = parts.next()?;
240        let tail = parts.next();
241        if head != self.key {
242            return None;
243        }
244        match tail {
245            None => self.value.as_deref(),
246            Some(rest) => self.children.iter().find_map(|c| c.lookup_relative(rest)),
247        }
248    }
249    fn lookup_relative(&self, path: &str) -> Option<&str> {
250        let mut parts = path.splitn(2, '.');
251        let head = parts.next()?;
252        let tail = parts.next();
253        if head != self.key {
254            return None;
255        }
256        match tail {
257            None => self.value.as_deref(),
258            Some(rest) => self.children.iter().find_map(|c| c.lookup_relative(rest)),
259        }
260    }
261}
262/// A simple directed acyclic graph.
263#[allow(dead_code)]
264pub struct SimpleDag {
265    /// `edges[i]` is the list of direct successors of node `i`.
266    edges: Vec<Vec<usize>>,
267}
268#[allow(dead_code)]
269impl SimpleDag {
270    /// Creates a DAG with `n` nodes and no edges.
271    pub fn new(n: usize) -> Self {
272        Self {
273            edges: vec![Vec::new(); n],
274        }
275    }
276    /// Adds an edge from `from` to `to`.
277    pub fn add_edge(&mut self, from: usize, to: usize) {
278        if from < self.edges.len() {
279            self.edges[from].push(to);
280        }
281    }
282    /// Returns the successors of `node`.
283    pub fn successors(&self, node: usize) -> &[usize] {
284        self.edges.get(node).map(|v| v.as_slice()).unwrap_or(&[])
285    }
286    /// Returns `true` if `from` can reach `to` via DFS.
287    pub fn can_reach(&self, from: usize, to: usize) -> bool {
288        let mut visited = vec![false; self.edges.len()];
289        self.dfs(from, to, &mut visited)
290    }
291    fn dfs(&self, cur: usize, target: usize, visited: &mut Vec<bool>) -> bool {
292        if cur == target {
293            return true;
294        }
295        if cur >= visited.len() || visited[cur] {
296            return false;
297        }
298        visited[cur] = true;
299        for &next in self.successors(cur) {
300            if self.dfs(next, target, visited) {
301                return true;
302            }
303        }
304        false
305    }
306    /// Returns the topological order of nodes, or `None` if a cycle is detected.
307    pub fn topological_sort(&self) -> Option<Vec<usize>> {
308        let n = self.edges.len();
309        let mut in_degree = vec![0usize; n];
310        for succs in &self.edges {
311            for &s in succs {
312                if s < n {
313                    in_degree[s] += 1;
314                }
315            }
316        }
317        let mut queue: std::collections::VecDeque<usize> =
318            (0..n).filter(|&i| in_degree[i] == 0).collect();
319        let mut order = Vec::new();
320        while let Some(node) = queue.pop_front() {
321            order.push(node);
322            for &s in self.successors(node) {
323                if s < n {
324                    in_degree[s] -= 1;
325                    if in_degree[s] == 0 {
326                        queue.push_back(s);
327                    }
328                }
329            }
330        }
331        if order.len() == n {
332            Some(order)
333        } else {
334            None
335        }
336    }
337    /// Returns the number of nodes.
338    pub fn num_nodes(&self) -> usize {
339        self.edges.len()
340    }
341}
342/// A window iterator that yields overlapping windows of size `n`.
343#[allow(dead_code)]
344pub struct WindowIterator<'a, T> {
345    pub(super) data: &'a [T],
346    pub(super) pos: usize,
347    pub(super) window: usize,
348}
349#[allow(dead_code)]
350impl<'a, T> WindowIterator<'a, T> {
351    /// Creates a new window iterator.
352    pub fn new(data: &'a [T], window: usize) -> Self {
353        Self {
354            data,
355            pos: 0,
356            window,
357        }
358    }
359}
360/// Environment extension for inductive types.
361pub struct InductiveEnv {
362    /// Map from type name to inductive declaration
363    inductives: HashMap<Name, InductiveType>,
364    /// Map from constructor name to parent type
365    constructors: HashMap<Name, Name>,
366    /// Map from recursor name to parent type
367    recursors: HashMap<Name, Name>,
368}
369impl InductiveEnv {
370    /// Create a new empty inductive environment.
371    pub fn new() -> Self {
372        Self {
373            inductives: HashMap::new(),
374            constructors: HashMap::new(),
375            recursors: HashMap::new(),
376        }
377    }
378    /// Add an inductive type to the environment.
379    #[allow(clippy::result_large_err)]
380    pub fn add(&mut self, ind: InductiveType) -> Result<(), KernelError> {
381        if self.inductives.contains_key(&ind.name) {
382            return Err(KernelError::Other(format!(
383                "inductive type already declared: {}",
384                ind.name
385            )));
386        }
387        for intro in &ind.intro_rules {
388            if self.constructors.contains_key(&intro.name) {
389                return Err(KernelError::Other(format!(
390                    "constructor already declared: {}",
391                    intro.name
392                )));
393            }
394            self.constructors
395                .insert(intro.name.clone(), ind.name.clone());
396        }
397        self.recursors
398            .insert(ind.recursor.clone(), ind.name.clone());
399        self.inductives.insert(ind.name.clone(), ind);
400        Ok(())
401    }
402    /// Get an inductive type by name.
403    pub fn get(&self, name: &Name) -> Option<&InductiveType> {
404        self.inductives.get(name)
405    }
406    /// Check if a name is a constructor.
407    pub fn is_constructor(&self, name: &Name) -> bool {
408        self.constructors.contains_key(name)
409    }
410    /// Get the parent type of a constructor.
411    pub fn get_constructor_parent(&self, name: &Name) -> Option<&Name> {
412        self.constructors.get(name)
413    }
414    /// Check if a name is a recursor.
415    pub fn is_recursor(&self, name: &Name) -> bool {
416        self.recursors.contains_key(name)
417    }
418    /// Get the parent type of a recursor.
419    pub fn get_recursor_parent(&self, name: &Name) -> Option<&Name> {
420        self.recursors.get(name)
421    }
422    /// Register an InductiveType into an Environment via ConstantInfo.
423    ///
424    /// This is the *checked* path: the declaration goes through
425    /// [`crate::inductive::derive::add_inductive_family`], which typechecks
426    /// the type and constructor telescopes, enforces the universe rule and
427    /// WHNF-hardened strict positivity, and derives the recursor itself.
428    #[allow(clippy::result_large_err)]
429    pub fn register_in_env(
430        &mut self,
431        ind: &InductiveType,
432        env: &mut crate::Environment,
433    ) -> Result<(), KernelError> {
434        crate::inductive::derive::add_inductive_family(
435            env,
436            ind.univ_params.clone(),
437            ind.num_params,
438            vec![ind.to_spec()],
439        )?;
440        self.add(ind.clone())?;
441        Ok(())
442    }
443}
444/// A non-empty list (at least one element guaranteed).
445#[allow(dead_code)]
446pub struct NonEmptyVec<T> {
447    head: T,
448    tail: Vec<T>,
449}
450#[allow(dead_code)]
451impl<T> NonEmptyVec<T> {
452    /// Creates a non-empty vec with a single element.
453    pub fn singleton(val: T) -> Self {
454        Self {
455            head: val,
456            tail: Vec::new(),
457        }
458    }
459    /// Pushes an element.
460    pub fn push(&mut self, val: T) {
461        self.tail.push(val);
462    }
463    /// Returns a reference to the first element.
464    pub fn first(&self) -> &T {
465        &self.head
466    }
467    /// Returns a reference to the last element.
468    pub fn last(&self) -> &T {
469        self.tail.last().unwrap_or(&self.head)
470    }
471    /// Returns the number of elements.
472    pub fn len(&self) -> usize {
473        1 + self.tail.len()
474    }
475    /// Returns whether the collection is empty.
476    pub fn is_empty(&self) -> bool {
477        self.len() == 0
478    }
479    /// Returns all elements as a Vec.
480    pub fn to_vec(&self) -> Vec<&T> {
481        let mut v = vec![&self.head];
482        v.extend(self.tail.iter());
483        v
484    }
485}
486/// A pair of `StatSummary` values tracking before/after a transformation.
487#[allow(dead_code)]
488pub struct TransformStat {
489    before: StatSummary,
490    after: StatSummary,
491}
492#[allow(dead_code)]
493impl TransformStat {
494    /// Creates a new transform stat recorder.
495    pub fn new() -> Self {
496        Self {
497            before: StatSummary::new(),
498            after: StatSummary::new(),
499        }
500    }
501    /// Records a before value.
502    pub fn record_before(&mut self, v: f64) {
503        self.before.record(v);
504    }
505    /// Records an after value.
506    pub fn record_after(&mut self, v: f64) {
507        self.after.record(v);
508    }
509    /// Returns the mean reduction ratio (after/before).
510    pub fn mean_ratio(&self) -> Option<f64> {
511        let b = self.before.mean()?;
512        let a = self.after.mean()?;
513        if b.abs() < f64::EPSILON {
514            return None;
515        }
516        Some(a / b)
517    }
518}
519/// A label set for a graph node.
520#[allow(dead_code)]
521pub struct LabelSet {
522    labels: Vec<String>,
523}
524#[allow(dead_code)]
525impl LabelSet {
526    /// Creates a new empty label set.
527    pub fn new() -> Self {
528        Self { labels: Vec::new() }
529    }
530    /// Adds a label (deduplicates).
531    pub fn add(&mut self, label: impl Into<String>) {
532        let s = label.into();
533        if !self.labels.contains(&s) {
534            self.labels.push(s);
535        }
536    }
537    /// Returns `true` if `label` is present.
538    pub fn has(&self, label: &str) -> bool {
539        self.labels.iter().any(|l| l == label)
540    }
541    /// Returns the count of labels.
542    pub fn count(&self) -> usize {
543        self.labels.len()
544    }
545    /// Returns all labels.
546    pub fn all(&self) -> &[String] {
547        &self.labels
548    }
549}
550/// A versioned record that stores a history of values.
551#[allow(dead_code)]
552pub struct VersionedRecord<T: Clone> {
553    /// Every earlier value, oldest first: version `n` is `earlier[n]`.
554    earlier: Vec<T>,
555    /// The latest value (version `earlier.len()`), declared last so it drops last.
556    current: T,
557}
558#[allow(dead_code)]
559impl<T: Clone> VersionedRecord<T> {
560    /// Creates a new record with an initial value.
561    pub fn new(initial: T) -> Self {
562        Self {
563            earlier: Vec::new(),
564            current: initial,
565        }
566    }
567    /// Updates the record with a new version.
568    pub fn update(&mut self, val: T) {
569        let previous = std::mem::replace(&mut self.current, val);
570        self.earlier.push(previous);
571    }
572    /// Returns the current (latest) value.
573    pub fn current(&self) -> &T {
574        &self.current
575    }
576    /// Returns the value at version `n` (0-indexed), or `None`.
577    pub fn at_version(&self, n: usize) -> Option<&T> {
578        match self.earlier.get(n) {
579            Some(value) => Some(value),
580            None if n == self.earlier.len() => Some(&self.current),
581            None => None,
582        }
583    }
584    /// Returns the version number of the current value.
585    pub fn version(&self) -> usize {
586        self.earlier.len()
587    }
588    /// Returns `true` if more than one version exists.
589    pub fn has_history(&self) -> bool {
590        !self.earlier.is_empty()
591    }
592}
593/// An inductive type declaration.
594#[derive(Clone, Debug, PartialEq)]
595pub struct InductiveType {
596    /// Type name
597    pub name: Name,
598    /// Universe parameters
599    pub univ_params: Vec<Name>,
600    /// Number of parameters (non-varying arguments)
601    pub num_params: u32,
602    /// Number of indices (varying arguments)
603    pub num_indices: u32,
604    /// Type of the inductive type (Pi type over params and indices)
605    pub ty: Expr,
606    /// Introduction rules (constructors)
607    pub intro_rules: Vec<IntroRule>,
608    /// Recursor name (generated automatically)
609    pub recursor: Name,
610    /// Whether this is a nested inductive type
611    pub is_nested: bool,
612    /// Whether this type is in Prop (proof-irrelevant)
613    pub is_prop: bool,
614}
615impl InductiveType {
616    /// Create a new inductive type.
617    pub fn new(
618        name: Name,
619        univ_params: Vec<Name>,
620        num_params: u32,
621        num_indices: u32,
622        ty: Expr,
623        intro_rules: Vec<IntroRule>,
624    ) -> Self {
625        let recursor = Name::mk_str(name.clone(), "rec".to_string());
626        Self {
627            name,
628            univ_params,
629            num_params,
630            num_indices,
631            ty,
632            intro_rules,
633            recursor,
634            is_nested: false,
635            is_prop: false,
636        }
637    }
638    /// Get the arity (total number of arguments).
639    pub fn arity(&self) -> u32 {
640        self.num_params + self.num_indices
641    }
642    /// Check if this inductive type is recursive.
643    pub fn is_recursive(&self) -> bool {
644        self.intro_rules
645            .iter()
646            .any(|rule| self.occurs_in_arguments(&self.name, &rule.ty))
647    }
648    /// Return a vector of references to constructor names.
649    pub fn constructor_names(&self) -> Vec<&Name> {
650        self.intro_rules.iter().map(|r| &r.name).collect()
651    }
652    /// Return the number of constructors.
653    pub fn num_constructors(&self) -> usize {
654        self.intro_rules.len()
655    }
656    fn occurs_in_arguments(&self, name: &Name, ty: &Expr) -> bool {
657        match ty {
658            Expr::Pi(_, _, dom, cod) => {
659                self.occurs_in_type(name, dom) || self.occurs_in_arguments(name, cod)
660            }
661            _ => false,
662        }
663    }
664    fn occurs_in_type(&self, name: &Name, ty: &Expr) -> bool {
665        match ty {
666            Expr::Const(n, _) => n == name,
667            Expr::App(f, a) => self.occurs_in_type(name, f) || self.occurs_in_type(name, a),
668            Expr::Pi(_, _, dom, cod) => {
669                self.occurs_in_type(name, dom) || self.occurs_in_type(name, cod)
670            }
671            Expr::Lam(_, _, ty_inner, body) => {
672                self.occurs_in_type(name, ty_inner) || self.occurs_in_type(name, body)
673            }
674            _ => false,
675        }
676    }
677    /// Convert this legacy declaration into an [`InductiveSpec`] for the
678    /// kernel derivation machinery in [`crate::inductive::derive`].
679    pub(crate) fn to_spec(&self) -> crate::inductive::derive::InductiveSpec {
680        crate::inductive::derive::InductiveSpec {
681            name: self.name.clone(),
682            ty: self.ty.clone(),
683            ctors: self
684                .intro_rules
685                .iter()
686                .map(|r| (r.name.clone(), r.ty.clone()))
687                .collect(),
688            rec_name: Some(self.recursor.clone()),
689        }
690    }
691    /// Generate ConstantInfo declarations for this inductive type.
692    ///
693    /// Returns: (InductiveVal, `Vec<ConstructorVal>`, RecursorVal).
694    ///
695    /// The recursor is derived by the kernel derivation machinery
696    /// ([`crate::inductive::derive`]) following Lean 4's `inductive.cpp`:
697    /// minor premises carry induction hypotheses, the elimination universe
698    /// and K flag are computed from the declared type (the caller-supplied
699    /// `is_prop` flag is ignored), and rule right-hand sides are closed
700    /// lambdas over `params ++ motives ++ minors ++ fields`.
701    ///
702    /// This environment-free path performs *no* positivity or universe
703    /// checking; use [`crate::inductive::derive::add_inductive_family`] for
704    /// the checked path.
705    #[allow(clippy::result_large_err)]
706    pub fn to_constant_infos(
707        &self,
708    ) -> Result<(ConstantInfo, Vec<ConstantInfo>, ConstantInfo), KernelError> {
709        let fam = crate::inductive::derive::derive_family_unchecked(
710            &self.univ_params,
711            self.num_params,
712            &[self.to_spec()],
713        )?;
714        let crate::inductive::derive::DerivedFamily {
715            mut inductives,
716            constructors,
717            mut recursors,
718        } = fam;
719        let ind = inductives.pop().ok_or_else(|| {
720            KernelError::Other("derivation produced no inductive declaration".to_string())
721        })?;
722        let rec = recursors.pop().ok_or_else(|| {
723            KernelError::Other("derivation produced no recursor declaration".to_string())
724        })?;
725        Ok((ind, constructors, rec))
726    }
727}
728/// Summary information about an inductive type (for display/LSP use).
729#[derive(Clone, Debug)]
730pub struct InductiveTypeInfo {
731    /// Type name.
732    pub name: Name,
733    /// Number of parameters.
734    pub num_params: u32,
735    /// Number of indices.
736    pub num_indices: u32,
737    /// Number of constructors.
738    pub num_constructors: usize,
739    /// Whether the type is in Prop.
740    pub is_prop: bool,
741    /// Whether the type is recursive (has recursive constructors).
742    pub is_recursive: bool,
743    /// Whether the type is mutually inductive.
744    pub is_mutual: bool,
745    /// Constructor names.
746    pub constructor_names: Vec<Name>,
747}
748impl InductiveTypeInfo {
749    /// Build info from an `InductiveType`.
750    pub fn from_type(ty: &InductiveType, is_mutual: bool) -> Self {
751        Self {
752            name: ty.name.clone(),
753            num_params: ty.num_params,
754            num_indices: ty.num_indices,
755            num_constructors: ty.intro_rules.len(),
756            is_prop: ty.is_prop,
757            is_recursive: ty.is_recursive(),
758            is_mutual,
759            constructor_names: ty.intro_rules.iter().map(|r| r.name.clone()).collect(),
760        }
761    }
762    /// Human-readable summary.
763    pub fn summary(&self) -> String {
764        format!(
765            "{}: {} params, {} indices, {} ctors, prop={}, recursive={}, mutual={}",
766            self.name,
767            self.num_params,
768            self.num_indices,
769            self.num_constructors,
770            self.is_prop,
771            self.is_recursive,
772            self.is_mutual
773        )
774    }
775}
776/// A mutable reference stack for tracking the current "focus" in a tree traversal.
777#[allow(dead_code)]
778pub struct FocusStack<T> {
779    items: Vec<T>,
780}
781#[allow(dead_code)]
782impl<T> FocusStack<T> {
783    /// Creates an empty focus stack.
784    pub fn new() -> Self {
785        Self { items: Vec::new() }
786    }
787    /// Focuses on `item`.
788    pub fn focus(&mut self, item: T) {
789        self.items.push(item);
790    }
791    /// Blurs (pops) the current focus.
792    pub fn blur(&mut self) -> Option<T> {
793        self.items.pop()
794    }
795    /// Returns the current focus, or `None`.
796    pub fn current(&self) -> Option<&T> {
797        self.items.last()
798    }
799    /// Returns the focus depth.
800    pub fn depth(&self) -> usize {
801        self.items.len()
802    }
803    /// Returns `true` if there is no current focus.
804    pub fn is_empty(&self) -> bool {
805        self.items.is_empty()
806    }
807}
808/// Builder for constructing `InductiveType` declarations incrementally.
809#[allow(dead_code)]
810pub struct InductiveTypeBuilder {
811    name: Option<Name>,
812    univ_params: Vec<Name>,
813    num_params: u32,
814    num_indices: u32,
815    ty: Option<Expr>,
816    intro_rules: Vec<IntroRule>,
817    is_prop: bool,
818    is_nested: bool,
819}
820#[allow(dead_code)]
821impl InductiveTypeBuilder {
822    /// Create an empty builder.
823    pub fn new() -> Self {
824        Self {
825            name: None,
826            univ_params: vec![],
827            num_params: 0,
828            num_indices: 0,
829            ty: None,
830            intro_rules: vec![],
831            is_prop: false,
832            is_nested: false,
833        }
834    }
835    /// Set the inductive type name.
836    pub fn name(mut self, name: Name) -> Self {
837        self.name = Some(name);
838        self
839    }
840    /// Set universe parameters.
841    pub fn univ_params(mut self, params: Vec<Name>) -> Self {
842        self.univ_params = params;
843        self
844    }
845    /// Set number of type parameters.
846    pub fn num_params(mut self, n: u32) -> Self {
847        self.num_params = n;
848        self
849    }
850    /// Set number of type indices.
851    pub fn num_indices(mut self, n: u32) -> Self {
852        self.num_indices = n;
853        self
854    }
855    /// Set the sort of the inductive type.
856    pub fn ty(mut self, ty: Expr) -> Self {
857        self.ty = Some(ty);
858        self
859    }
860    /// Add a constructor/introduction rule.
861    pub fn intro_rule(mut self, name: Name, ty: Expr) -> Self {
862        self.intro_rules.push(IntroRule { name, ty });
863        self
864    }
865    /// Mark as a Prop-valued inductive type (proof-irrelevant).
866    pub fn is_prop(mut self, v: bool) -> Self {
867        self.is_prop = v;
868        self
869    }
870    /// Mark as a nested inductive type.
871    pub fn is_nested(mut self, v: bool) -> Self {
872        self.is_nested = v;
873        self
874    }
875    /// Build the `InductiveType`. Returns `Err` if name or ty is missing.
876    pub fn build(self) -> Result<InductiveType, String> {
877        let name = self
878            .name
879            .ok_or_else(|| "InductiveTypeBuilder: name not set".to_string())?;
880        let ty = self
881            .ty
882            .ok_or_else(|| "InductiveTypeBuilder: ty not set".to_string())?;
883        let mut ind = InductiveType::new(
884            name,
885            self.univ_params,
886            self.num_params,
887            self.num_indices,
888            ty,
889            self.intro_rules,
890        );
891        ind.is_prop = self.is_prop;
892        ind.is_nested = self.is_nested;
893        Ok(ind)
894    }
895}
896/// A builder for constructing recursor definitions programmatically.
897///
898/// Recursors (eliminators) are the fundamental way to consume inductive types.
899/// This builder provides a fluent API for constructing them.
900#[derive(Clone, Debug)]
901pub struct RecursorBuilder {
902    /// Name of the recursor (typically `T.rec` or `T.recOn`).
903    pub name: Name,
904    /// Universe parameters.
905    pub univ_params: Vec<Name>,
906    /// Number of type parameters.
907    pub num_params: u32,
908    /// Number of indices.
909    pub num_indices: u32,
910    /// Number of motives (typically 1).
911    pub num_motives: u32,
912    /// Number of minor premises (one per constructor).
913    pub num_minor_premises: u32,
914    /// Recursor rules (one per constructor).
915    pub rules: Vec<RecursorRule>,
916    /// Whether the recursor targets `Prop`.
917    pub is_prop: bool,
918}
919impl RecursorBuilder {
920    /// Create a new builder.
921    pub fn new(name: Name) -> Self {
922        Self {
923            name,
924            univ_params: vec![],
925            num_params: 0,
926            num_indices: 0,
927            num_motives: 1,
928            num_minor_premises: 0,
929            rules: vec![],
930            is_prop: false,
931        }
932    }
933    /// Set universe parameters.
934    pub fn univ_params(mut self, params: Vec<Name>) -> Self {
935        self.univ_params = params;
936        self
937    }
938    /// Set the number of parameters.
939    pub fn num_params(mut self, n: u32) -> Self {
940        self.num_params = n;
941        self
942    }
943    /// Set the number of indices.
944    pub fn num_indices(mut self, n: u32) -> Self {
945        self.num_indices = n;
946        self
947    }
948    /// Set whether the recursor targets Prop.
949    pub fn is_prop(mut self, b: bool) -> Self {
950        self.is_prop = b;
951        self
952    }
953    /// Add a recursor rule.
954    pub fn add_rule(mut self, rule: RecursorRule) -> Self {
955        self.rules.push(rule);
956        self.num_minor_premises += 1;
957        self
958    }
959    /// Validate the builder state.
960    ///
961    /// Returns `Ok(())` if the builder is consistent.
962    pub fn validate(&self) -> Result<(), String> {
963        if self.name.is_anonymous() {
964            return Err("recursor name must not be anonymous".to_string());
965        }
966        if self.num_motives == 0 {
967            return Err("recursor must have at least one motive".to_string());
968        }
969        Ok(())
970    }
971    /// Return the name of the recursor.
972    pub fn build_name(&self) -> Name {
973        self.name.clone()
974    }
975    /// Build a complete [`RecursorVal`] from the builder state.
976    ///
977    /// `ty` is the type of the recursor (must be supplied by the caller since
978    /// this builder does not reconstruct the Pi telescope).
979    /// `all` is the list of inductive type names in the mutual family.
980    pub fn build(&self, ty: Expr, all: Vec<Name>) -> Result<RecursorVal, String> {
981        self.validate()?;
982        if self.rules.len() != self.num_minor_premises as usize {
983            return Err(format!(
984                "RecursorBuilder: num_minor_premises ({}) does not match rule count ({})",
985                self.num_minor_premises,
986                self.rules.len()
987            ));
988        }
989        Ok(RecursorVal {
990            common: ConstantVal {
991                name: self.name.clone(),
992                level_params: self.univ_params.clone(),
993                ty,
994            },
995            all,
996            num_params: self.num_params,
997            num_indices: self.num_indices,
998            num_motives: self.num_motives,
999            num_minors: self.num_minor_premises,
1000            rules: self.rules.clone(),
1001            k: false,
1002            is_unsafe: false,
1003        })
1004    }
1005}
oxilean_kernel/inductive/types.rs

oxilean_kernel/inductive/
types.rs
