oxilean_elab/pattern_match/
types.rs

1//! Auto-generated module
2//!
3//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)
4
5use super::functions::*;
6use crate::context::ElabContext;
7use oxilean_kernel::{Environment, Expr, FVarId, Level, Name};
8use oxilean_parse::{Located, MatchArm, Pattern, SurfaceExpr};
9use std::collections::HashMap;
10
11/// Decision tree for compiled pattern matching.
12#[derive(Debug, Clone)]
13#[allow(dead_code)]
14pub struct DecisionTree {
15    /// Root node of the decision tree.
16    root: DecisionNode,
17}
18impl DecisionTree {
19    /// Create a new decision tree from match arms.
20    pub fn new(arms: &[(Located<Pattern>, Located<SurfaceExpr>)]) -> Result<Self, String> {
21        if arms.is_empty() {
22            return Ok(Self {
23                root: DecisionNode::Leaf(Expr::BVar(0)),
24            });
25        }
26        let mut node = DecisionNode::Fail;
27        for (pat, rhs_surf) in arms.iter().rev() {
28            let rhs = surface_to_placeholder(&rhs_surf.value);
29            node = build_node_from_pattern(&pat.value, rhs, node);
30        }
31        Ok(Self { root: node })
32    }
33    /// Create a decision tree from elaborated match equations.
34    #[allow(dead_code)]
35    pub fn from_equations(equations: &[MatchEquation]) -> Result<Self, String> {
36        if equations.is_empty() {
37            return Ok(Self {
38                root: DecisionNode::Fail,
39            });
40        }
41        let mut node = DecisionNode::Fail;
42        for eq in equations.iter().rev() {
43            if eq.patterns.is_empty() {
44                node = DecisionNode::Leaf(eq.rhs.clone());
45            } else {
46                node = build_node_from_elab_pattern(&eq.patterns[0], eq.rhs.clone(), node);
47            }
48        }
49        Ok(Self { root: node })
50    }
51    /// Compile the decision tree to a kernel expression.
52    pub fn compile(&self) -> Expr {
53        compile_node(&self.root)
54    }
55}
56/// High-level elaboration of a `match` expression.
57#[allow(dead_code)]
58pub struct MatchElaborator {
59    /// Fresh variable counter.
60    next_var: u64,
61    /// Whether to perform exhaustiveness checking.
62    pub check_exhaustive: bool,
63    /// Whether to perform redundancy checking.
64    pub check_redundant: bool,
65}
66#[allow(dead_code)]
67impl MatchElaborator {
68    /// Create a new match elaborator.
69    pub fn new() -> Self {
70        Self {
71            next_var: 10000,
72            check_exhaustive: true,
73            check_redundant: true,
74        }
75    }
76    /// Generate a fresh free variable ID.
77    pub fn fresh_fvar(&mut self) -> FVarId {
78        let id = FVarId(self.next_var);
79        self.next_var += 1;
80        id
81    }
82    /// Elaborate a pattern and return the `ElabPattern` plus variable bindings.
83    #[allow(clippy::type_complexity)]
84    pub fn elab_pattern(
85        &mut self,
86        pat: &Pattern,
87        ty: &Expr,
88    ) -> Result<(ElabPattern, Vec<(FVarId, Name, Expr)>), String> {
89        elab_pattern_with_counter(pat, ty, &mut self.next_var)
90    }
91    /// Run exhaustiveness checking on a set of surface patterns.
92    pub fn check_exhaust(&self, patterns: &[Located<Pattern>]) -> ExhaustivenessResult {
93        check_exhaustive_full(patterns)
94    }
95    /// Run redundancy checking on a set of surface patterns.
96    pub fn check_redundant_arms(&self, patterns: &[Located<Pattern>]) -> Vec<usize> {
97        check_redundant_full(patterns)
98    }
99}
100/// Substitutes free variables within an elaborated pattern.
101#[allow(dead_code)]
102#[derive(Debug, Default)]
103pub struct PatternSubstitution {
104    /// Mapping from `FVarId` to replacement expression.
105    subst: HashMap<FVarId, Expr>,
106}
107#[allow(dead_code)]
108impl PatternSubstitution {
109    /// Create an empty substitution.
110    pub fn new() -> Self {
111        Self::default()
112    }
113    /// Bind a free variable to an expression.
114    pub fn bind(&mut self, fvar: FVarId, expr: Expr) {
115        self.subst.insert(fvar, expr);
116    }
117    /// Look up the replacement for a free variable.
118    pub fn get(&self, fvar: &FVarId) -> Option<&Expr> {
119        self.subst.get(fvar)
120    }
121    /// Return the number of bindings.
122    pub fn len(&self) -> usize {
123        self.subst.len()
124    }
125    /// Return true if there are no bindings.
126    pub fn is_empty(&self) -> bool {
127        self.subst.is_empty()
128    }
129    /// Apply the substitution to an expression (identity placeholder).
130    pub fn apply_to_expr(&self, expr: &Expr) -> Expr {
131        expr.clone()
132    }
133    /// Merge another substitution into this one (later bindings override).
134    pub fn merge(&mut self, other: &PatternSubstitution) {
135        for (k, v) in &other.subst {
136            self.subst.insert(*k, v.clone());
137        }
138    }
139}
140/// Heuristics for selecting the best column to split in a pattern matrix.
141#[allow(dead_code)]
142#[derive(Debug, Clone, Copy, PartialEq, Eq)]
143pub enum ColumnHeuristic {
144    /// Always choose the leftmost column.
145    LeftMost,
146    /// Choose the column with the most constructor patterns.
147    MostConstructors,
148    /// Choose the column with the smallest number of distinct patterns.
149    SmallestBranching,
150}
151#[allow(dead_code)]
152impl ColumnHeuristic {
153    /// Apply this heuristic to select a column from the matrix.
154    pub fn select_column(&self, matrix: &PatternMatrix) -> usize {
155        match self {
156            ColumnHeuristic::LeftMost => 0,
157            ColumnHeuristic::MostConstructors => matrix.best_column(),
158            ColumnHeuristic::SmallestBranching => matrix.best_column(),
159        }
160    }
161}
162/// An elaborated pattern with full type information.
163#[derive(Clone, Debug, PartialEq)]
164pub enum ElabPattern {
165    /// Wildcard: matches anything.
166    Wild,
167    /// Variable binding: captures the matched value.
168    Var(FVarId, Name, Expr),
169    /// Constructor application: matches a specific constructor.
170    Ctor(Name, Vec<ElabPattern>, Expr),
171    /// Literal pattern.
172    Lit(oxilean_kernel::Literal),
173    /// Or pattern: matches if either sub-pattern matches.
174    Or(Box<ElabPattern>, Box<ElabPattern>),
175    /// As-pattern: binds a variable while matching a sub-pattern.
176    As(FVarId, Name, Box<ElabPattern>),
177    /// Inaccessible pattern: not used for matching, only for type-checking.
178    Inaccessible(Expr),
179}
180/// Statistics about a collection of patterns.
181#[allow(dead_code)]
182#[derive(Debug, Clone, Default)]
183pub struct PatternStats {
184    /// Total number of patterns.
185    pub total: usize,
186    /// Number of wildcard patterns.
187    pub wilds: usize,
188    /// Number of variable bindings.
189    pub variables: usize,
190    /// Number of constructor patterns.
191    pub constructors: usize,
192    /// Number of literal patterns.
193    pub literals: usize,
194    /// Number of or-patterns.
195    pub ors: usize,
196    /// Number of as-patterns.
197    pub as_pats: usize,
198    /// Number of inaccessible patterns.
199    pub inaccessibles: usize,
200    /// Maximum nesting depth.
201    pub max_depth: usize,
202}
203#[allow(dead_code)]
204impl PatternStats {
205    /// Compute statistics from a slice of elaborated patterns.
206    pub fn from_patterns(patterns: &[ElabPattern]) -> Self {
207        let mut stats = Self {
208            total: patterns.len(),
209            ..Self::default()
210        };
211        for pat in patterns {
212            stats.count_pattern(pat);
213            let depth = pattern_depth(pat);
214            if depth > stats.max_depth {
215                stats.max_depth = depth;
216            }
217        }
218        stats
219    }
220    fn count_pattern(&mut self, pat: &ElabPattern) {
221        match pat {
222            ElabPattern::Wild => self.wilds += 1,
223            ElabPattern::Var(_, _, _) => self.variables += 1,
224            ElabPattern::Ctor(_, sub, _) => {
225                self.constructors += 1;
226                for s in sub {
227                    self.count_pattern(s);
228                }
229            }
230            ElabPattern::Lit(_) => self.literals += 1,
231            ElabPattern::Or(a, b) => {
232                self.ors += 1;
233                self.count_pattern(a);
234                self.count_pattern(b);
235            }
236            ElabPattern::As(_, _, inner) => {
237                self.as_pats += 1;
238                self.count_pattern(inner);
239            }
240            ElabPattern::Inaccessible(_) => self.inaccessibles += 1,
241        }
242    }
243}
244/// Elaboration result for pattern matching.
245#[derive(Debug, Clone)]
246pub struct MatchResult {
247    /// The compiled match expression.
248    pub expr: Expr,
249    /// Generated auxiliary definitions.
250    pub defs: Vec<(Name, Expr)>,
251    /// The expanded equations.
252    pub equations: Vec<MatchEquation>,
253    /// Missing patterns (for incomplete matches).
254    pub missing_patterns: Vec<MissingPattern>,
255    /// Indices of redundant arms.
256    pub redundant_arms: Vec<usize>,
257}
258/// A match equation: a row in the pattern matrix.
259#[derive(Clone, Debug)]
260pub struct MatchEquation {
261    /// The patterns for this row (one per scrutinee in multi-match).
262    pub patterns: Vec<ElabPattern>,
263    /// The right-hand side expression.
264    pub rhs: Expr,
265    /// Index of the original arm this equation came from.
266    pub arm_idx: usize,
267}
268/// A pattern matrix used during compilation.
269#[derive(Clone, Debug)]
270#[allow(dead_code)]
271pub struct PatternMatrix {
272    /// Rows of the matrix: each row has patterns and a rhs index.
273    pub(super) rows: Vec<MatrixRow>,
274    /// Number of columns.
275    pub(super) num_cols: usize,
276}
277#[allow(dead_code)]
278impl PatternMatrix {
279    /// Create a new pattern matrix from equations.
280    pub(crate) fn from_equations(equations: &[MatchEquation]) -> Self {
281        let num_cols = equations.first().map(|e| e.patterns.len()).unwrap_or(0);
282        let rows = equations
283            .iter()
284            .map(|eq| MatrixRow {
285                patterns: eq.patterns.clone(),
286                rhs_idx: eq.arm_idx,
287            })
288            .collect();
289        Self { rows, num_cols }
290    }
291    /// Check if the matrix is empty.
292    pub(crate) fn is_empty(&self) -> bool {
293        self.rows.is_empty()
294    }
295    /// Pick the best column to split on (heuristic: most constructors).
296    pub(crate) fn best_column(&self) -> usize {
297        if self.num_cols == 0 {
298            return 0;
299        }
300        let mut best_col = 0;
301        let mut best_score = 0;
302        for col in 0..self.num_cols {
303            let mut ctors = Vec::new();
304            for row in &self.rows {
305                if col < row.patterns.len() {
306                    if let ElabPattern::Ctor(name, _, _) = &row.patterns[col] {
307                        if !ctors.contains(name) {
308                            ctors.push(name.clone());
309                        }
310                    }
311                }
312            }
313            if ctors.len() > best_score {
314                best_score = ctors.len();
315                best_col = col;
316            }
317        }
318        best_col
319    }
320    /// Specialize the matrix for a given constructor.
321    ///
322    /// Keeps only rows where column `col` matches `ctor_name`, and expands
323    /// the constructor's sub-patterns into new columns.
324    pub(super) fn specialize(
325        &self,
326        col: usize,
327        ctor_name: &Name,
328        ctor_arity: usize,
329    ) -> PatternMatrix {
330        let mut new_rows = Vec::new();
331        for row in &self.rows {
332            if col >= row.patterns.len() {
333                continue;
334            }
335            match &row.patterns[col] {
336                ElabPattern::Ctor(name, sub_pats, _) if name == ctor_name => {
337                    let mut new_pats = Vec::new();
338                    for sp in sub_pats {
339                        new_pats.push(sp.clone());
340                    }
341                    while new_pats.len() < ctor_arity {
342                        new_pats.push(ElabPattern::Wild);
343                    }
344                    for (j, p) in row.patterns.iter().enumerate() {
345                        if j != col {
346                            new_pats.push(p.clone());
347                        }
348                    }
349                    new_rows.push(MatrixRow {
350                        patterns: new_pats,
351                        rhs_idx: row.rhs_idx,
352                    });
353                }
354                ElabPattern::Wild | ElabPattern::Var(_, _, _) => {
355                    let mut new_pats = Vec::new();
356                    for _ in 0..ctor_arity {
357                        new_pats.push(ElabPattern::Wild);
358                    }
359                    for (j, p) in row.patterns.iter().enumerate() {
360                        if j != col {
361                            new_pats.push(p.clone());
362                        }
363                    }
364                    new_rows.push(MatrixRow {
365                        patterns: new_pats,
366                        rhs_idx: row.rhs_idx,
367                    });
368                }
369                _ => {}
370            }
371        }
372        let num_cols = if self.num_cols > 0 {
373            self.num_cols - 1 + ctor_arity
374        } else {
375            ctor_arity
376        };
377        PatternMatrix {
378            rows: new_rows,
379            num_cols,
380        }
381    }
382    /// Default matrix: rows where column `col` is a wildcard/variable.
383    pub(super) fn default_matrix(&self, col: usize) -> PatternMatrix {
384        let mut new_rows = Vec::new();
385        for row in &self.rows {
386            if col >= row.patterns.len() {
387                continue;
388            }
389            match &row.patterns[col] {
390                ElabPattern::Wild | ElabPattern::Var(_, _, _) => {
391                    let new_pats: Vec<ElabPattern> = row
392                        .patterns
393                        .iter()
394                        .enumerate()
395                        .filter(|(j, _)| *j != col)
396                        .map(|(_, p)| p.clone())
397                        .collect();
398                    new_rows.push(MatrixRow {
399                        patterns: new_pats,
400                        rhs_idx: row.rhs_idx,
401                    });
402                }
403                _ => {}
404            }
405        }
406        let num_cols = if self.num_cols > 0 {
407            self.num_cols - 1
408        } else {
409            0
410        };
411        PatternMatrix {
412            rows: new_rows,
413            num_cols,
414        }
415    }
416}
417/// Normalizes patterns by removing redundant wrappers.
418#[allow(dead_code)]
419pub struct PatternNormalizer;
420#[allow(dead_code)]
421impl PatternNormalizer {
422    /// Create a new normalizer.
423    pub fn new() -> Self {
424        Self
425    }
426    /// Normalize an elaborated pattern.
427    pub fn normalize(&self, pat: &ElabPattern) -> ElabPattern {
428        match pat {
429            ElabPattern::As(_, _, inner) if is_irrefutable(inner) => self.normalize(inner),
430            ElabPattern::Or(a, b) if a == b => self.normalize(a),
431            ElabPattern::Ctor(name, sub, ty) => {
432                let normalized_sub: Vec<ElabPattern> =
433                    sub.iter().map(|s| self.normalize(s)).collect();
434                ElabPattern::Ctor(name.clone(), normalized_sub, ty.clone())
435            }
436            ElabPattern::Or(a, b) => {
437                ElabPattern::Or(Box::new(self.normalize(a)), Box::new(self.normalize(b)))
438            }
439            ElabPattern::As(fv, n, inner) => {
440                ElabPattern::As(*fv, n.clone(), Box::new(self.normalize(inner)))
441            }
442            other => other.clone(),
443        }
444    }
445    /// Normalize a list of patterns in place.
446    pub fn normalize_all(&self, patterns: &[ElabPattern]) -> Vec<ElabPattern> {
447        patterns.iter().map(|p| self.normalize(p)).collect()
448    }
449}
450/// Analyzes the structure of a compiled decision tree.
451#[allow(dead_code)]
452pub struct DecisionTreeAnalyzer;
453#[allow(dead_code)]
454impl DecisionTreeAnalyzer {
455    /// Estimate the depth of the decision tree.
456    pub fn estimate_depth(tree: &DecisionTree) -> usize {
457        Self::node_depth(&tree.root)
458    }
459    /// Estimate the total number of nodes in the tree.
460    pub fn estimate_nodes(tree: &DecisionTree) -> usize {
461        Self::count_nodes(&tree.root)
462    }
463    /// Return true if the tree has a default (wildcard) arm.
464    pub fn has_default_arm(tree: &DecisionTree) -> bool {
465        Self::node_has_default(&tree.root)
466    }
467    /// Return the number of arms (leaf nodes) in the tree.
468    pub fn num_arms(tree: &DecisionTree) -> usize {
469        Self::count_leaves(&tree.root)
470    }
471    fn node_depth(node: &DecisionNode) -> usize {
472        match node {
473            DecisionNode::Leaf(_) | DecisionNode::Fail => 1,
474            DecisionNode::Switch {
475                branches, default, ..
476            } => {
477                let branch_max = branches
478                    .iter()
479                    .map(|(_, b)| Self::node_depth(b))
480                    .max()
481                    .unwrap_or(0);
482                let def_depth = default.as_ref().map_or(0, |d| Self::node_depth(d));
483                1 + branch_max.max(def_depth)
484            }
485            DecisionNode::Guard { then, else_, .. } => {
486                1 + Self::node_depth(then).max(Self::node_depth(else_))
487            }
488        }
489    }
490    fn count_nodes(node: &DecisionNode) -> usize {
491        match node {
492            DecisionNode::Leaf(_) | DecisionNode::Fail => 1,
493            DecisionNode::Switch {
494                branches, default, ..
495            } => {
496                let sum: usize = branches.iter().map(|(_, b)| Self::count_nodes(b)).sum();
497                1 + sum + default.as_ref().map_or(0, |d| Self::count_nodes(d))
498            }
499            DecisionNode::Guard { then, else_, .. } => {
500                1 + Self::count_nodes(then) + Self::count_nodes(else_)
501            }
502        }
503    }
504    fn node_has_default(node: &DecisionNode) -> bool {
505        match node {
506            DecisionNode::Leaf(_) | DecisionNode::Fail => false,
507            DecisionNode::Switch {
508                branches, default, ..
509            } => {
510                if default.is_some() {
511                    return true;
512                }
513                branches.iter().any(|(_, b)| Self::node_has_default(b))
514            }
515            DecisionNode::Guard { then, else_, .. } => {
516                Self::node_has_default(then) || Self::node_has_default(else_)
517            }
518        }
519    }
520    fn count_leaves(node: &DecisionNode) -> usize {
521        match node {
522            DecisionNode::Leaf(_) => 1,
523            DecisionNode::Fail => 0,
524            DecisionNode::Switch {
525                branches, default, ..
526            } => {
527                let sum: usize = branches.iter().map(|(_, b)| Self::count_leaves(b)).sum();
528                sum + default.as_ref().map_or(0, |d| Self::count_leaves(d))
529            }
530            DecisionNode::Guard { then, else_, .. } => {
531                Self::count_leaves(then) + Self::count_leaves(else_)
532            }
533        }
534    }
535}
536/// A node in the decision tree.
537#[derive(Debug, Clone)]
538#[allow(dead_code)]
539pub enum DecisionNode {
540    /// Leaf node: produce this expression.
541    Leaf(Expr),
542    /// Switch on constructor of a variable.
543    Switch {
544        /// Variable to switch on.
545        var: Name,
546        /// Branches for each constructor.
547        branches: Vec<(Name, Box<DecisionNode>)>,
548        /// Default branch (for wildcard / variable patterns).
549        default: Option<Box<DecisionNode>>,
550    },
551    /// Guard check.
552    Guard {
553        /// Guard condition expression.
554        condition: Expr,
555        /// Branch if guard evaluates to true.
556        then: Box<DecisionNode>,
557        /// Branch if guard evaluates to false.
558        else_: Box<DecisionNode>,
559    },
560    /// Failure: no pattern matched (unreachable if exhaustive).
561    Fail,
562}
563/// Tracks which literal values appear in a set of patterns.
564#[allow(dead_code)]
565#[derive(Debug, Clone, Default)]
566pub struct LiteralSet {
567    /// Natural number literals seen.
568    pub nats: Vec<u64>,
569    /// String literals seen.
570    pub strings: Vec<String>,
571    /// Whether a wildcard has been seen (closes the literal set).
572    pub has_wildcard: bool,
573}
574#[allow(dead_code)]
575impl LiteralSet {
576    /// Create an empty literal set.
577    pub fn new() -> Self {
578        Self::default()
579    }
580    /// Add a literal to the set.
581    pub fn add_literal(&mut self, lit: &oxilean_kernel::Literal) {
582        match lit {
583            oxilean_kernel::Literal::Nat(n) => {
584                if !self.nats.contains(n) {
585                    self.nats.push(*n);
586                }
587            }
588            oxilean_kernel::Literal::Str(s) => {
589                if !self.strings.contains(s) {
590                    self.strings.push(s.clone());
591                }
592            }
593        }
594    }
595    /// Mark that a wildcard was seen.
596    pub fn add_wildcard(&mut self) {
597        self.has_wildcard = true;
598    }
599    /// Check if a specific natural number literal is covered.
600    pub fn covers_nat(&self, n: u64) -> bool {
601        self.has_wildcard || self.nats.contains(&n)
602    }
603    /// Return the total number of specific literals seen.
604    pub fn num_specific(&self) -> usize {
605        self.nats.len() + self.strings.len()
606    }
607}
608/// Classification of an elaborated pattern.
609#[allow(dead_code)]
610#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
611pub enum PatternKind {
612    /// Wildcard pattern.
613    Wild,
614    /// Variable binding.
615    Variable,
616    /// Constructor application.
617    Constructor,
618    /// Literal value.
619    Literal,
620    /// Or-pattern.
621    Or,
622    /// As-pattern.
623    As,
624    /// Inaccessible (dot) pattern.
625    Inaccessible,
626}
627#[allow(dead_code)]
628impl PatternKind {
629    /// Classify an elaborated pattern.
630    pub fn of(pat: &ElabPattern) -> Self {
631        match pat {
632            ElabPattern::Wild => PatternKind::Wild,
633            ElabPattern::Var(_, _, _) => PatternKind::Variable,
634            ElabPattern::Ctor(_, _, _) => PatternKind::Constructor,
635            ElabPattern::Lit(_) => PatternKind::Literal,
636            ElabPattern::Or(_, _) => PatternKind::Or,
637            ElabPattern::As(_, _, _) => PatternKind::As,
638            ElabPattern::Inaccessible(_) => PatternKind::Inaccessible,
639        }
640    }
641    /// Return true if this pattern kind can bind variables.
642    pub fn can_bind(&self) -> bool {
643        matches!(self, PatternKind::Variable | PatternKind::As)
644    }
645    /// Return true if this pattern kind is a "catch-all" (always matches).
646    pub fn is_catch_all(&self) -> bool {
647        matches!(self, PatternKind::Wild | PatternKind::Variable)
648    }
649}
650/// Result of exhaustiveness checking.
651#[derive(Clone, Debug)]
652pub struct ExhaustivenessResult {
653    /// Whether the patterns are exhaustive.
654    pub is_exhaustive: bool,
655    /// Missing constructors/patterns if not exhaustive.
656    pub missing: Vec<MissingPattern>,
657}
658/// A single row in the pattern matrix.
659#[derive(Clone, Debug)]
660#[allow(dead_code)]
661pub struct MatrixRow {
662    pub patterns: Vec<ElabPattern>,
663    pub rhs_idx: usize,
664}
665/// Tracks which match arms have been covered by test inputs.
666#[allow(dead_code)]
667#[derive(Debug, Clone, Default)]
668pub struct MatchCoverage {
669    /// Number of arms in the match.
670    pub num_arms: usize,
671    /// Which arms have been hit.
672    pub hit: Vec<bool>,
673}
674#[allow(dead_code)]
675impl MatchCoverage {
676    /// Create a coverage tracker for a match with `n` arms.
677    pub fn new(n: usize) -> Self {
678        Self {
679            num_arms: n,
680            hit: vec![false; n],
681        }
682    }
683    /// Record that arm `i` was hit.
684    pub fn record_hit(&mut self, i: usize) {
685        if i < self.num_arms {
686            self.hit[i] = true;
687        }
688    }
689    /// Return the number of arms hit.
690    pub fn arms_hit(&self) -> usize {
691        self.hit.iter().filter(|&&h| h).count()
692    }
693    /// Return true if all arms have been hit.
694    pub fn is_full_coverage(&self) -> bool {
695        self.hit.iter().all(|&h| h)
696    }
697    /// Return the indices of arms that have NOT been hit.
698    pub fn uncovered_arms(&self) -> Vec<usize> {
699        self.hit
700            .iter()
701            .enumerate()
702            .filter(|(_, &h)| !h)
703            .map(|(i, _)| i)
704            .collect()
705    }
706    /// Coverage percentage (0.0 to 1.0).
707    pub fn coverage_pct(&self) -> f64 {
708        if self.num_arms == 0 {
709            1.0
710        } else {
711            self.arms_hit() as f64 / self.num_arms as f64
712        }
713    }
714}
715/// Pretty-printer for elaborated patterns.
716#[allow(dead_code)]
717pub struct PatternPrinter {
718    /// Indent width for nested patterns.
719    pub indent: usize,
720}
721#[allow(dead_code)]
722impl PatternPrinter {
723    /// Create a new printer with default indent of 2.
724    pub fn new() -> Self {
725        Self { indent: 2 }
726    }
727    /// Create a printer with a custom indent.
728    pub fn with_indent(indent: usize) -> Self {
729        Self { indent }
730    }
731    /// Print an elaborated pattern to a string.
732    pub fn print(&self, pat: &ElabPattern) -> String {
733        self.print_inner(pat, 0)
734    }
735    fn print_inner(&self, pat: &ElabPattern, _depth: usize) -> String {
736        match pat {
737            ElabPattern::Wild => "_".to_string(),
738            ElabPattern::Var(_, name, _) => format!("{}", name),
739            ElabPattern::Lit(lit) => match lit {
740                oxilean_kernel::Literal::Nat(n) => format!("{}", n),
741                oxilean_kernel::Literal::Str(s) => format!("\"{}\"", s),
742            },
743            ElabPattern::Ctor(name, sub, _) => {
744                if sub.is_empty() {
745                    format!("{}", name)
746                } else {
747                    let args: Vec<String> = sub
748                        .iter()
749                        .map(|s| self.print_inner(s, _depth + 1))
750                        .collect();
751                    format!("({} {})", name, args.join(" "))
752                }
753            }
754            ElabPattern::Or(a, b) => {
755                format!(
756                    "({} | {})",
757                    self.print_inner(a, _depth),
758                    self.print_inner(b, _depth)
759                )
760            }
761            ElabPattern::As(_, name, inner) => {
762                format!("({} @ {})", self.print_inner(inner, _depth), name)
763            }
764            ElabPattern::Inaccessible(e) => format!(".({})", e),
765        }
766    }
767    /// Print a list of patterns separated by newlines.
768    pub fn print_all(&self, patterns: &[ElabPattern]) -> String {
769        patterns
770            .iter()
771            .enumerate()
772            .map(|(i, p)| format!("  arm {}: {}", i, self.print(p)))
773            .collect::<Vec<_>>()
774            .join("\n")
775    }
776}
777/// Pattern match compiler.
778///
779/// Compiles surface-level patterns into decision trees for efficient matching.
780pub struct PatternCompiler {
781    /// Fresh variable counter.
782    pub(crate) next_var: u32,
783}
784impl PatternCompiler {
785    /// Create a new pattern compiler.
786    pub fn new() -> Self {
787        Self { next_var: 0 }
788    }
789    /// Generate a fresh variable name.
790    pub fn fresh_var(&mut self) -> Name {
791        let n = self.next_var;
792        self.next_var += 1;
793        Name::str(format!("_pat{}", n))
794    }
795    /// Compile surface-level patterns to a decision tree.
796    pub fn compile(
797        &mut self,
798        patterns: &[(Located<Pattern>, Located<SurfaceExpr>)],
799    ) -> Result<DecisionTree, String> {
800        DecisionTree::new(patterns)
801    }
802    /// Compile from elaborated match equations.
803    #[allow(dead_code)]
804    pub fn compile_equations(
805        &mut self,
806        equations: &[MatchEquation],
807    ) -> Result<DecisionTree, String> {
808        DecisionTree::from_equations(equations)
809    }
810    /// Compile from match arms (with guards).
811    #[allow(dead_code)]
812    pub fn from_match_arms(
813        &mut self,
814        ctx: &mut ElabContext,
815        _scrutinee_ty: &Expr,
816        arms: &[MatchArm],
817    ) -> Result<(DecisionTree, MatchResult), String> {
818        let mut equations = Vec::new();
819        for (i, arm) in arms.iter().enumerate() {
820            let expected_ty = Expr::Sort(Level::succ(Level::zero()));
821            let (elab_pat, _bindings) = elaborate_pattern(ctx, &arm.pattern.value, &expected_ty)?;
822            let rhs = surface_to_placeholder(&arm.rhs.value);
823            let guard_expr = arm.guard.as_ref().map(|g| surface_to_placeholder(&g.value));
824            let _ = guard_expr;
825            equations.push(MatchEquation {
826                patterns: vec![elab_pat],
827                rhs,
828                arm_idx: i,
829            });
830        }
831        let tree = DecisionTree::from_equations(&equations)?;
832        let expr = tree.compile();
833        let patterns_located: Vec<Located<Pattern>> =
834            arms.iter().map(|a| a.pattern.clone()).collect();
835        let exhaustiveness = check_exhaustive_full(&patterns_located);
836        let redundant = check_redundant_full(&patterns_located);
837        let result = MatchResult {
838            expr,
839            defs: Vec::new(),
840            equations,
841            missing_patterns: exhaustiveness.missing,
842            redundant_arms: redundant,
843        };
844        Ok((tree, result))
845    }
846}
847/// A missing pattern discovered during exhaustiveness checking.
848#[derive(Clone, Debug)]
849pub struct MissingPattern {
850    /// Constructor name (or "wildcard" for general missing).
851    pub ctor_name: Name,
852    /// Sub-patterns within the constructor.
853    pub sub_patterns: Vec<ElabPattern>,
854}
855/// Simulates runtime pattern matching against an elaborated pattern.
856///
857/// This is used for testing and verification, not for actual codegen.
858#[allow(dead_code)]
859pub struct PatternMatcher {
860    /// Whether to allow partial matches (for debugging).
861    pub partial_ok: bool,
862}
863#[allow(dead_code)]
864impl PatternMatcher {
865    /// Create a new pattern matcher.
866    pub fn new() -> Self {
867        Self { partial_ok: false }
868    }
869    /// Check if a pattern would match a given literal expression.
870    pub fn matches_literal(&self, pat: &ElabPattern, lit: &oxilean_kernel::Literal) -> bool {
871        match pat {
872            ElabPattern::Wild | ElabPattern::Var(_, _, _) => true,
873            ElabPattern::Lit(l) => l == lit,
874            ElabPattern::Or(a, b) => self.matches_literal(a, lit) || self.matches_literal(b, lit),
875            ElabPattern::As(_, _, inner) => self.matches_literal(inner, lit),
876            ElabPattern::Ctor(_, _, _) | ElabPattern::Inaccessible(_) => false,
877        }
878    }
879    /// Find the first arm index that matches a given literal.
880    pub fn first_match_idx(
881        &self,
882        arms: &[ElabPattern],
883        lit: &oxilean_kernel::Literal,
884    ) -> Option<usize> {
885        arms.iter().position(|p| self.matches_literal(p, lit))
886    }
887    /// Return all arms that match a given literal.
888    pub fn all_match_idxs(
889        &self,
890        arms: &[ElabPattern],
891        lit: &oxilean_kernel::Literal,
892    ) -> Vec<usize> {
893        arms.iter()
894            .enumerate()
895            .filter(|(_, p)| self.matches_literal(p, lit))
896            .map(|(i, _)| i)
897            .collect()
898    }
899}
oxilean_elab/pattern_match/types.rs

oxilean_elab/pattern_match/
types.rs
