oxilean_kernel/type_erasure/
types.rs

1//! Auto-generated module
2//!
3//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)
4
5use super::functions::*;
6
7use std::collections::{BTreeSet, HashMap};
8
9/// Tracks which de Bruijn indices are live at a given program point.
10#[allow(dead_code)]
11pub struct ErasedLiveness {
12    live: std::collections::BTreeSet<u32>,
13}
14#[allow(dead_code)]
15impl ErasedLiveness {
16    /// Creates a new empty liveness set.
17    pub fn new() -> Self {
18        Self {
19            live: std::collections::BTreeSet::new(),
20        }
21    }
22    /// Marks de Bruijn index `i` as live.
23    pub fn mark_live(&mut self, i: u32) {
24        self.live.insert(i);
25    }
26    /// Returns `true` if de Bruijn index `i` is live.
27    pub fn is_live(&self, i: u32) -> bool {
28        self.live.contains(&i)
29    }
30    /// Returns the number of live indices.
31    pub fn count(&self) -> usize {
32        self.live.len()
33    }
34    /// Merges another liveness set into this one (union).
35    pub fn merge(&mut self, other: &ErasedLiveness) {
36        for &i in &other.live {
37            self.live.insert(i);
38        }
39    }
40    /// Returns the maximum live index, or `None` if empty.
41    pub fn max_live(&self) -> Option<u32> {
42        self.live.iter().next_back().copied()
43    }
44}
45/// High-level AST node wrapping an erased expression with source metadata.
46#[allow(dead_code)]
47#[allow(missing_docs)]
48pub struct ErasedAst {
49    /// The underlying erased expression.
50    pub expr: ErasedExpr,
51    /// A human-readable label for debugging.
52    pub label: String,
53    /// Estimated stack depth needed to evaluate this node.
54    pub stack_depth: usize,
55}
56#[allow(dead_code)]
57impl ErasedAst {
58    /// Creates a new AST node.
59    pub fn new(expr: ErasedExpr, label: impl Into<String>) -> Self {
60        let depth = erased_expr_depth(&expr);
61        Self {
62            expr,
63            label: label.into(),
64            stack_depth: depth as usize,
65        }
66    }
67    /// Returns the size of the wrapped expression.
68    pub fn size(&self) -> usize {
69        erased_expr_apps(&self.expr)
70    }
71}
72/// A pass pipeline combining multiple transformation passes.
73#[allow(dead_code)]
74#[allow(missing_docs)]
75pub struct ErasurePass {
76    pub name: String,
77    pub total_transforms: u64,
78}
79#[allow(dead_code)]
80impl ErasurePass {
81    /// Create a new pipeline.
82    pub fn new(name: impl Into<String>) -> Self {
83        ErasurePass {
84            name: name.into(),
85            total_transforms: 0,
86        }
87    }
88    /// Run the full erasure pipeline on an expression.
89    pub fn run(&mut self, expr: ErasedExprExt) -> ErasedExprExt {
90        let mut opt = ErasedOptimizer::new(1000);
91        let result = opt.optimize(expr);
92        self.total_transforms += opt.total_transforms();
93        result
94    }
95    /// Run the pipeline on a module.
96    pub fn run_module(&mut self, mut module: ErasedModule) -> ErasedModule {
97        let new_decls = module
98            .decls
99            .drain(..)
100            .map(|decl| match decl {
101                ErasedDecl::Def { name, body } => {
102                    let new_body = self.run(body);
103                    ErasedDecl::Def {
104                        name,
105                        body: new_body,
106                    }
107                }
108                other => other,
109            })
110            .collect();
111        module.decls = new_decls;
112        module
113    }
114}
115/// Tuple constructor and projector for erased expressions.
116#[allow(dead_code)]
117pub struct ErasedTupleOps;
118#[allow(dead_code)]
119impl ErasedTupleOps {
120    /// Construct a pair (2-tuple).
121    pub fn make_pair(a: ErasedExprExt, b: ErasedExprExt) -> ErasedExprExt {
122        ErasedExprExt::App(
123            Box::new(ErasedExprExt::App(
124                Box::new(ErasedExprExt::Const("Prod.mk".to_string())),
125                Box::new(a),
126            )),
127            Box::new(b),
128        )
129    }
130    /// First projection (fst) application.
131    pub fn fst(pair: ErasedExprExt) -> ErasedExprExt {
132        ErasedExprExt::App(
133            Box::new(ErasedExprExt::Const("Prod.fst".to_string())),
134            Box::new(pair),
135        )
136    }
137    /// Second projection (snd) application.
138    pub fn snd(pair: ErasedExprExt) -> ErasedExprExt {
139        ErasedExprExt::App(
140            Box::new(ErasedExprExt::Const("Prod.snd".to_string())),
141            Box::new(pair),
142        )
143    }
144    /// Construct an n-tuple by nesting pairs.
145    pub fn n_tuple(exprs: Vec<ErasedExprExt>) -> ErasedExprExt {
146        assert!(!exprs.is_empty(), "n_tuple: empty tuple");
147        let mut iter = exprs.into_iter().rev();
148        let last = iter
149            .next()
150            .expect("iterator must have at least one element");
151        iter.fold(last, |acc, e| Self::make_pair(e, acc))
152    }
153}
154/// Performs beta reduction on erased expressions.
155#[allow(dead_code)]
156#[allow(missing_docs)]
157pub struct ErasedBetaReducer {
158    pub steps: u64,
159    pub max_steps: u64,
160}
161#[allow(dead_code)]
162impl ErasedBetaReducer {
163    /// Create a reducer with a step limit.
164    pub fn new(max_steps: u64) -> Self {
165        ErasedBetaReducer {
166            steps: 0,
167            max_steps,
168        }
169    }
170    /// Perform one step of beta reduction.
171    pub fn step(&mut self, expr: ErasedExprExt) -> ErasedExprExt {
172        if self.steps >= self.max_steps {
173            return expr;
174        }
175        match expr {
176            ErasedExprExt::App(f, arg) => match *f {
177                ErasedExprExt::Lam(body) => {
178                    self.steps += 1;
179                    subst_bvar0(*body, *arg)
180                }
181                other_f => ErasedExprExt::App(Box::new(other_f), arg),
182            },
183            ErasedExprExt::Lam(b) => ErasedExprExt::Lam(Box::new(self.step(*b))),
184            other => other,
185        }
186    }
187    /// Return whether the step limit has been reached.
188    pub fn is_exhausted(&self) -> bool {
189        self.steps >= self.max_steps
190    }
191}
192/// A map from expression ids to their erased forms.
193#[allow(dead_code)]
194pub struct ErasedTypeMap {
195    entries: Vec<(u64, ErasedExprExt)>,
196}
197#[allow(dead_code)]
198impl ErasedTypeMap {
199    /// Create an empty map.
200    pub fn new() -> Self {
201        ErasedTypeMap {
202            entries: Vec::new(),
203        }
204    }
205    /// Insert a mapping.
206    pub fn insert(&mut self, id: u64, erased: ErasedExprExt) {
207        if let Some(e) = self.entries.iter_mut().find(|(i, _)| *i == id) {
208            e.1 = erased;
209        } else {
210            self.entries.push((id, erased));
211        }
212    }
213    /// Look up by id.
214    pub fn get(&self, id: u64) -> Option<&ErasedExprExt> {
215        self.entries.iter().find(|(i, _)| *i == id).map(|(_, e)| e)
216    }
217    /// Return the number of entries.
218    pub fn len(&self) -> usize {
219        self.entries.len()
220    }
221    /// Return whether empty.
222    pub fn is_empty(&self) -> bool {
223        self.entries.is_empty()
224    }
225}
226/// A single arm of an erased match expression.
227#[allow(dead_code)]
228#[allow(missing_docs)]
229#[derive(Debug, Clone)]
230pub struct ErasedMatchArm {
231    pub pattern: ErasedPattern,
232    pub body: ErasedExprExt,
233}
234#[allow(dead_code)]
235impl ErasedMatchArm {
236    /// Create a new match arm.
237    pub fn new(pattern: ErasedPattern, body: ErasedExprExt) -> Self {
238        ErasedMatchArm { pattern, body }
239    }
240    /// Return whether this arm is a catch-all.
241    pub fn is_catch_all(&self) -> bool {
242        self.pattern.is_irrefutable()
243    }
244}
245/// Represents a captured environment for a closure in erased code.
246#[allow(dead_code)]
247#[allow(missing_docs)]
248pub struct ErasedClosureEnv {
249    /// Captured variable names.
250    pub captures: Vec<String>,
251    /// Their corresponding erased values.
252    pub values: Vec<ErasedExprExt>,
253}
254#[allow(dead_code)]
255impl ErasedClosureEnv {
256    /// Creates a new empty closure environment.
257    pub fn new() -> Self {
258        Self {
259            captures: Vec::new(),
260            values: Vec::new(),
261        }
262    }
263    /// Adds a captured variable binding.
264    pub fn capture(&mut self, name: impl Into<String>, val: ErasedExprExt) {
265        self.captures.push(name.into());
266        self.values.push(val);
267    }
268    /// Look up a captured variable by name.
269    pub fn lookup(&self, name: &str) -> Option<&ErasedExprExt> {
270        self.captures
271            .iter()
272            .position(|n| n == name)
273            .map(|i| &self.values[i])
274    }
275    /// Returns the number of captured variables.
276    pub fn size(&self) -> usize {
277        self.captures.len()
278    }
279}
280/// Runs a sequence of `ErasedPass` implementations in order.
281#[allow(dead_code)]
282pub struct PipelineRunner {
283    passes: Vec<Box<dyn ErasedPass>>,
284}
285#[allow(dead_code)]
286impl PipelineRunner {
287    /// Creates a new empty pipeline runner.
288    pub fn new() -> Self {
289        Self { passes: Vec::new() }
290    }
291    /// Adds a pass to the pipeline.
292    pub fn add_pass(&mut self, pass: Box<dyn ErasedPass>) {
293        self.passes.push(pass);
294    }
295    /// Runs all passes on `expr` in order.
296    pub fn run_all(&mut self, expr: ErasedExpr) -> ErasedExpr {
297        let mut current = expr;
298        for pass in self.passes.iter_mut() {
299            current = pass.run(current);
300        }
301        current
302    }
303    /// Runs all passes on each declaration in `module`.
304    pub fn run_on_module(&mut self, decls: &mut Vec<ErasedDecl>) {
305        for pass in self.passes.iter_mut() {
306            pass.run_on_module(decls);
307        }
308    }
309    /// Returns the number of registered passes.
310    pub fn num_passes(&self) -> usize {
311        self.passes.len()
312    }
313}
314/// Inline simple constants in an erased expression.
315#[allow(dead_code)]
316#[allow(missing_docs)]
317pub struct ErasedInliner {
318    /// Map from constant name to its erased definition.
319    defs: Vec<(String, ErasedExprExt)>,
320    pub inlined: u64,
321}
322#[allow(dead_code)]
323impl ErasedInliner {
324    /// Create an inliner with definitions.
325    pub fn new() -> Self {
326        ErasedInliner {
327            defs: Vec::new(),
328            inlined: 0,
329        }
330    }
331    /// Register a constant definition.
332    pub fn register(&mut self, name: &str, def: ErasedExprExt) {
333        self.defs.push((name.to_string(), def));
334    }
335    /// Inline constants in an expression.
336    pub fn inline(&mut self, expr: ErasedExprExt) -> ErasedExprExt {
337        match expr {
338            ErasedExprExt::Const(ref name) => {
339                if let Some((_, def)) = self.defs.iter().find(|(n, _)| n == name) {
340                    self.inlined += 1;
341                    def.clone()
342                } else {
343                    expr
344                }
345            }
346            ErasedExprExt::Lam(b) => ErasedExprExt::Lam(Box::new(self.inline(*b))),
347            ErasedExprExt::App(f, x) => {
348                ErasedExprExt::App(Box::new(self.inline(*f)), Box::new(self.inline(*x)))
349            }
350            ErasedExprExt::Let(v, b) => {
351                ErasedExprExt::Let(Box::new(self.inline(*v)), Box::new(self.inline(*b)))
352            }
353            other => other,
354        }
355    }
356}
357/// An erasure context tracking which variables are types vs terms.
358#[allow(dead_code)]
359pub struct ErasureContext {
360    /// True if variable at index is a type (should be erased).
361    type_vars: Vec<bool>,
362}
363#[allow(dead_code)]
364impl ErasureContext {
365    /// Create an empty context.
366    pub fn new() -> Self {
367        ErasureContext {
368            type_vars: Vec::new(),
369        }
370    }
371    /// Push a variable; `is_type` indicates whether it should be erased.
372    pub fn push(&mut self, is_type: bool) {
373        self.type_vars.push(is_type);
374    }
375    /// Pop the last variable.
376    pub fn pop(&mut self) {
377        self.type_vars.pop();
378    }
379    /// Return whether the variable at De Bruijn index `i` is a type.
380    pub fn is_type_at(&self, i: u32) -> bool {
381        let len = self.type_vars.len();
382        if (i as usize) < len {
383            self.type_vars[len - 1 - i as usize]
384        } else {
385            false
386        }
387    }
388    /// Return the current depth.
389    pub fn depth(&self) -> usize {
390        self.type_vars.len()
391    }
392}
393/// A simple code generator for erased expressions (stub).
394#[allow(dead_code)]
395#[allow(missing_docs)]
396pub struct ErasedCodegen {
397    pub output: String,
398    indent: usize,
399}
400#[allow(dead_code)]
401impl ErasedCodegen {
402    /// Create a new code generator.
403    pub fn new() -> Self {
404        ErasedCodegen {
405            output: String::new(),
406            indent: 0,
407        }
408    }
409    /// Emit a line with current indentation.
410    pub fn emit(&mut self, line: &str) {
411        for _ in 0..self.indent {
412            self.output.push_str("  ");
413        }
414        self.output.push_str(line);
415        self.output.push('\n');
416    }
417    /// Generate code for an expression.
418    pub fn gen_expr(&mut self, expr: &ErasedExprExt) -> String {
419        match expr {
420            ErasedExprExt::Lit(n) => n.to_string(),
421            ErasedExprExt::BVar(i) => format!("v{}", i),
422            ErasedExprExt::FVar(name) => name.clone(),
423            ErasedExprExt::Const(name) => name.clone(),
424            ErasedExprExt::Unit => "()".to_string(),
425            ErasedExprExt::TypeErased => "_".to_string(),
426            ErasedExprExt::Lam(b) => format!("(fun x -> {})", self.gen_expr(b)),
427            ErasedExprExt::App(f, x) => {
428                format!("({} {})", self.gen_expr(f), self.gen_expr(x))
429            }
430            ErasedExprExt::Let(v, b) => {
431                format!("(let _ = {} in {})", self.gen_expr(v), self.gen_expr(b))
432            }
433            ErasedExprExt::CtorTag(t) => format!("Ctor({})", t),
434        }
435    }
436    /// Generate code for a module.
437    pub fn gen_module(&mut self, module: &ErasedModule) {
438        self.emit(&format!("(* Module: {} *)", module.name));
439        for decl in &module.decls {
440            match decl {
441                ErasedDecl::Def { name, body } => {
442                    let body_str = self.gen_expr(body);
443                    self.emit(&format!("let {} = {}", name, body_str));
444                }
445                ErasedDecl::Axiom { name } => {
446                    self.emit(&format!("let {} = failwith \"axiom\"", name));
447                }
448                ErasedDecl::Inductive { name, ctor_count } => {
449                    self.emit(&format!(
450                        "(* Inductive {} with {} ctors *)",
451                        name, ctor_count
452                    ));
453                }
454            }
455        }
456    }
457}
458/// Environment for erased computation (parallel binding arrays).
459#[allow(dead_code)]
460pub struct ErasedEnv {
461    names: Vec<String>,
462    values: Vec<ErasedExpr>,
463}
464#[allow(dead_code)]
465impl ErasedEnv {
466    /// Create an empty environment.
467    pub fn new() -> Self {
468        ErasedEnv {
469            names: Vec::new(),
470            values: Vec::new(),
471        }
472    }
473    /// Bind a name to an expression.
474    pub fn bind(&mut self, name: &str, val: ErasedExpr) {
475        self.names.push(name.to_string());
476        self.values.push(val);
477    }
478    /// Look up a name (returns the most recent binding).
479    pub fn get(&self, name: &str) -> Option<&ErasedExpr> {
480        self.names
481            .iter()
482            .rev()
483            .zip(self.values.iter().rev())
484            .find(|(n, _)| n.as_str() == name)
485            .map(|(_, v)| v)
486    }
487    /// Return the number of bindings.
488    pub fn len(&self) -> usize {
489        self.names.len()
490    }
491    /// Return whether the environment is empty.
492    pub fn is_empty(&self) -> bool {
493        self.names.is_empty()
494    }
495}
496/// A collection of erased declarations forming a module.
497#[allow(dead_code)]
498#[allow(missing_docs)]
499pub struct ErasedModule {
500    pub name: String,
501    pub decls: Vec<ErasedDecl>,
502}
503#[allow(dead_code)]
504impl ErasedModule {
505    /// Create an empty module.
506    pub fn new(name: impl Into<String>) -> Self {
507        ErasedModule {
508            name: name.into(),
509            decls: Vec::new(),
510        }
511    }
512    /// Add a declaration.
513    pub fn add(&mut self, decl: ErasedDecl) {
514        self.decls.push(decl);
515    }
516    /// Find a declaration by name.
517    pub fn find(&self, name: &str) -> Option<&ErasedDecl> {
518        self.decls.iter().find(|d| d.name() == name)
519    }
520    /// Return the number of declarations.
521    pub fn len(&self) -> usize {
522        self.decls.len()
523    }
524    /// Return whether the module is empty.
525    pub fn is_empty(&self) -> bool {
526        self.decls.is_empty()
527    }
528    /// Return all function names.
529    pub fn function_names(&self) -> Vec<&str> {
530        self.decls
531            .iter()
532            .filter(|d| d.is_def())
533            .map(|d| d.name())
534            .collect()
535    }
536}
537/// A heap-allocated object in the erased runtime.
538#[allow(dead_code)]
539#[allow(missing_docs)]
540#[derive(Debug, Clone)]
541pub enum ErasedHeapObj {
542    /// A boxed literal value.
543    Lit(u64),
544    /// A constructor tag + fields.
545    Ctor { tag: u32, fields: Vec<usize> },
546    /// A closure.
547    Closure {
548        arity: u32,
549        fn_ptr: usize,
550        num_caps: u32,
551    },
552    /// A string constant.
553    Str(String),
554    /// A thunk (unevaluated expression).
555    Thunk { code: usize },
556}
557impl ErasedHeapObj {
558    /// Return `true` if this is a constructor object.
559    #[allow(dead_code)]
560    pub fn is_ctor(&self) -> bool {
561        matches!(self, ErasedHeapObj::Ctor { .. })
562    }
563    /// Return `true` if this is a closure.
564    #[allow(dead_code)]
565    pub fn is_closure(&self) -> bool {
566        matches!(self, ErasedHeapObj::Closure { .. })
567    }
568    /// Return `true` if this is a thunk.
569    #[allow(dead_code)]
570    pub fn is_thunk(&self) -> bool {
571        matches!(self, ErasedHeapObj::Thunk { .. })
572    }
573    /// Return the tag if this is a constructor, else `None`.
574    #[allow(dead_code)]
575    pub fn ctor_tag(&self) -> Option<u32> {
576        if let ErasedHeapObj::Ctor { tag, .. } = self {
577            Some(*tag)
578        } else {
579            None
580        }
581    }
582}
583/// A simple optimizer that chains beta reduction, inlining, and DCE.
584#[allow(dead_code)]
585pub struct ErasedOptimizer {
586    reducer: ErasedBetaReducer,
587    dce: ErasedDCE,
588}
589#[allow(dead_code)]
590impl ErasedOptimizer {
591    /// Create an optimizer.
592    pub fn new(max_steps: u64) -> Self {
593        ErasedOptimizer {
594            reducer: ErasedBetaReducer::new(max_steps),
595            dce: ErasedDCE::new(),
596        }
597    }
598    /// Run all optimization passes on an expression.
599    pub fn optimize(&mut self, expr: ErasedExprExt) -> ErasedExprExt {
600        let after_beta = self.reducer.step(expr);
601        self.dce.elim(after_beta)
602    }
603    /// Return total transformations applied.
604    pub fn total_transforms(&self) -> u64 {
605        self.reducer.steps + self.dce.eliminated
606    }
607}
608/// An erased expression node with only runtime-relevant information.
609#[allow(dead_code)]
610#[derive(Debug, Clone, PartialEq, Eq)]
611pub enum ErasedExprExt {
612    /// A bound variable (De Bruijn index).
613    BVar(u32),
614    /// A free variable by name.
615    FVar(String),
616    /// A literal integer value.
617    Lit(u64),
618    /// A constructor tag (for inductive types).
619    CtorTag(u32),
620    /// A lambda abstraction.
621    Lam(Box<ErasedExprExt>),
622    /// An application.
623    App(Box<ErasedExprExt>, Box<ErasedExprExt>),
624    /// A global constant reference.
625    Const(String),
626    /// A let binding.
627    Let(Box<ErasedExprExt>, Box<ErasedExprExt>),
628    /// A type-erased placeholder (occurs when types are erased).
629    TypeErased,
630    /// A unit value.
631    Unit,
632}
633impl ErasedExprExt {
634    /// Return true if this expression is a literal.
635    #[allow(dead_code)]
636    pub fn is_lit(&self) -> bool {
637        matches!(self, ErasedExprExt::Lit(_))
638    }
639    /// Return true if this is a lambda.
640    #[allow(dead_code)]
641    pub fn is_lam(&self) -> bool {
642        matches!(self, ErasedExprExt::Lam(_))
643    }
644    /// Return true if this is an application.
645    #[allow(dead_code)]
646    pub fn is_app(&self) -> bool {
647        matches!(self, ErasedExprExt::App(_, _))
648    }
649    /// Return true if this is type-erased.
650    #[allow(dead_code)]
651    pub fn is_type_erased(&self) -> bool {
652        *self == ErasedExprExt::TypeErased
653    }
654    /// Count the total number of nodes in the expression tree.
655    #[allow(dead_code)]
656    pub fn size(&self) -> usize {
657        match self {
658            ErasedExprExt::Lam(b) => 1 + b.size(),
659            ErasedExprExt::App(f, x) => 1 + f.size() + x.size(),
660            ErasedExprExt::Let(v, b) => 1 + v.size() + b.size(),
661            _ => 1,
662        }
663    }
664}
665/// Dead-code elimination for erased expressions.
666#[allow(dead_code)]
667#[allow(missing_docs)]
668pub struct ErasedDCE {
669    pub eliminated: u64,
670}
671#[allow(dead_code)]
672impl ErasedDCE {
673    /// Create a DCE pass.
674    pub fn new() -> Self {
675        ErasedDCE { eliminated: 0 }
676    }
677    /// Eliminate TypeErased nodes from applications.
678    pub fn elim(&mut self, expr: ErasedExprExt) -> ErasedExprExt {
679        match expr {
680            ErasedExprExt::App(f, x) => {
681                let f = self.elim(*f);
682                let x = self.elim(*x);
683                if x == ErasedExprExt::TypeErased {
684                    self.eliminated += 1;
685                    f
686                } else {
687                    ErasedExprExt::App(Box::new(f), Box::new(x))
688                }
689            }
690            ErasedExprExt::Lam(b) => {
691                let b = self.elim(*b);
692                if b == ErasedExprExt::TypeErased {
693                    self.eliminated += 1;
694                    ErasedExprExt::TypeErased
695                } else {
696                    ErasedExprExt::Lam(Box::new(b))
697                }
698            }
699            ErasedExprExt::Let(v, b) => {
700                let v = self.elim(*v);
701                let b = self.elim(*b);
702                ErasedExprExt::Let(Box::new(v), Box::new(b))
703            }
704            other => other,
705        }
706    }
707}
708/// A stack-based evaluator for erased expressions.
709#[allow(dead_code)]
710pub struct ErasedStack {
711    stack: Vec<ErasedExpr>,
712}
713#[allow(dead_code)]
714impl ErasedStack {
715    /// Create an empty stack.
716    pub fn new() -> Self {
717        ErasedStack { stack: Vec::new() }
718    }
719    /// Push an expression onto the stack.
720    pub fn push(&mut self, expr: ErasedExpr) {
721        self.stack.push(expr);
722    }
723    /// Pop an expression from the stack.
724    pub fn pop(&mut self) -> Option<ErasedExpr> {
725        self.stack.pop()
726    }
727    /// Peek at the top expression.
728    pub fn peek(&self) -> Option<&ErasedExpr> {
729        self.stack.last()
730    }
731    /// Return the stack depth.
732    pub fn depth(&self) -> usize {
733        self.stack.len()
734    }
735    /// Return whether the stack is empty.
736    pub fn is_empty(&self) -> bool {
737        self.stack.is_empty()
738    }
739}
740/// A flat representation of a spine: `f a0 a1 … aN`.
741#[allow(dead_code)]
742#[allow(missing_docs)]
743pub struct ErasedFlatApp {
744    /// The head of the application.
745    pub head: ErasedExpr,
746    /// The argument list.
747    pub args: Vec<ErasedExpr>,
748}
749#[allow(dead_code)]
750impl ErasedFlatApp {
751    /// Flattens an `ErasedExpr` into its head and argument list.
752    pub fn from_expr(mut expr: ErasedExpr) -> Self {
753        let mut args = Vec::new();
754        loop {
755            match expr {
756                ErasedExpr::App(f, a) => {
757                    args.push(*a);
758                    expr = *f;
759                }
760                other => {
761                    args.reverse();
762                    return Self { head: other, args };
763                }
764            }
765        }
766    }
767    /// Rebuilds a left-spine `App` chain from the flat representation.
768    pub fn into_expr(self) -> ErasedExpr {
769        let mut result = self.head;
770        for arg in self.args {
771            result = ErasedExpr::App(Box::new(result), Box::new(arg));
772        }
773        result
774    }
775    /// Returns the total arity (number of arguments).
776    pub fn arity(&self) -> usize {
777        self.args.len()
778    }
779}
780/// A small-step interpreter for erased expressions.
781#[allow(dead_code)]
782#[allow(missing_docs)]
783pub struct ErasedInterpreter {
784    pub steps: u64,
785    pub max_steps: u64,
786    scope: ErasedScope,
787}
788#[allow(dead_code)]
789impl ErasedInterpreter {
790    /// Create a new interpreter.
791    pub fn new(max_steps: u64) -> Self {
792        ErasedInterpreter {
793            steps: 0,
794            max_steps,
795            scope: ErasedScope::new(),
796        }
797    }
798    /// Evaluate an expression to a value.
799    pub fn eval(&mut self, expr: ErasedExprExt) -> Option<ErasedValue> {
800        if self.steps >= self.max_steps {
801            return None;
802        }
803        self.steps += 1;
804        match expr {
805            ErasedExprExt::Lit(n) => Some(ErasedValue::Int(n)),
806            ErasedExprExt::Unit => Some(ErasedValue::Unit),
807            ErasedExprExt::TypeErased => Some(ErasedValue::Unit),
808            ErasedExprExt::Lam(b) => Some(ErasedValue::Closure {
809                body: b,
810                env: Vec::new(),
811            }),
812            ErasedExprExt::BVar(_) => None,
813            ErasedExprExt::FVar(name) => self.scope.lookup(&name).cloned(),
814            ErasedExprExt::Const(_) => None,
815            ErasedExprExt::CtorTag(t) => Some(ErasedValue::Ctor(t, Vec::new())),
816            ErasedExprExt::App(f, x) => {
817                let f_val = self.eval(*f)?;
818                let x_val = self.eval(*x)?;
819                match f_val {
820                    ErasedValue::Closure { body, env: _ } => {
821                        let subst =
822                            subst_bvar0(*body, ErasedExprExt::Lit(x_val.as_int().unwrap_or(0)));
823                        self.eval(subst)
824                    }
825                    ErasedValue::Ctor(t, mut fields) => {
826                        fields.push(x_val);
827                        Some(ErasedValue::Ctor(t, fields))
828                    }
829                    _ => None,
830                }
831            }
832            ErasedExprExt::Let(v, b) => {
833                let v_val = self.eval(*v)?;
834                let subst = subst_bvar0(*b, ErasedExprExt::Lit(v_val.as_int().unwrap_or(0)));
835                self.eval(subst)
836            }
837        }
838    }
839    /// Return whether the step limit was exceeded.
840    pub fn is_exhausted(&self) -> bool {
841        self.steps >= self.max_steps
842    }
843}
844/// Pools integer literals to avoid duplication in the erased IR.
845#[allow(dead_code)]
846pub struct ErasedConstantPool {
847    pool: Vec<i64>,
848    index: std::collections::HashMap<i64, usize>,
849}
850#[allow(dead_code)]
851impl ErasedConstantPool {
852    /// Creates an empty constant pool.
853    pub fn new() -> Self {
854        Self {
855            pool: Vec::new(),
856            index: std::collections::HashMap::new(),
857        }
858    }
859    /// Interns `val` and returns its pool index.
860    pub fn intern(&mut self, val: i64) -> usize {
861        if let Some(&idx) = self.index.get(&val) {
862            return idx;
863        }
864        let idx = self.pool.len();
865        self.pool.push(val);
866        self.index.insert(val, idx);
867        idx
868    }
869    /// Returns the value at pool index `idx`, or `None`.
870    pub fn get(&self, idx: usize) -> Option<i64> {
871        self.pool.get(idx).copied()
872    }
873    /// Returns the total number of interned constants.
874    pub fn len(&self) -> usize {
875        self.pool.len()
876    }
877    /// Returns `true` if the pool is empty.
878    pub fn is_empty(&self) -> bool {
879        self.pool.is_empty()
880    }
881}
882/// Prints an erased expression to a structured string format.
883#[allow(dead_code)]
884#[allow(missing_docs)]
885pub struct ErasedPrinter {
886    pub output: String,
887    depth: usize,
888}
889#[allow(dead_code)]
890impl ErasedPrinter {
891    /// Create a new printer.
892    pub fn new() -> Self {
893        ErasedPrinter {
894            output: String::new(),
895            depth: 0,
896        }
897    }
898    /// Print an expression.
899    pub fn print(&mut self, expr: &ErasedExprExt) {
900        let s = pretty_print_erased(expr);
901        for _ in 0..self.depth {
902            self.output.push_str("  ");
903        }
904        self.output.push_str(&s);
905        self.output.push('\n');
906    }
907    /// Return the printed output.
908    pub fn result(&self) -> &str {
909        &self.output
910    }
911    /// Clear the output.
912    pub fn clear(&mut self) {
913        self.output.clear();
914        self.depth = 0;
915    }
916}
917/// Performs type erasure on kernel expressions.
918pub struct TypeEraser {
919    config: EraseConfig,
920}
921impl TypeEraser {
922    /// Create a type eraser with the default configuration.
923    pub fn new() -> Self {
924        TypeEraser {
925            config: EraseConfig::default(),
926        }
927    }
928    /// Create a type eraser with a custom configuration.
929    pub fn with_config(config: EraseConfig) -> Self {
930        TypeEraser { config }
931    }
932    /// Erase a sort (universe level) — always becomes `TypeErased`.
933    pub fn erase_sort(&self) -> ErasedExpr {
934        ErasedExpr::TypeErased
935    }
936    /// Erase a Pi-type — types are always erased to `TypeErased`.
937    pub fn erase_pi(&self) -> ErasedExpr {
938        ErasedExpr::TypeErased
939    }
940    /// Wrap a lambda body in a `Lam` node (type annotation already dropped).
941    pub fn erase_lam_body(&self, body: ErasedExpr) -> ErasedExpr {
942        ErasedExpr::Lam(Box::new(body))
943    }
944    /// Build an erased application from an already-erased function and argument.
945    pub fn erase_app(f: ErasedExpr, arg: ErasedExpr) -> ErasedExpr {
946        ErasedExpr::App(Box::new(f), Box::new(arg))
947    }
948    /// Erase a natural-number literal.
949    pub fn erase_lit(n: u64) -> ErasedExpr {
950        ErasedExpr::Lit(n)
951    }
952    /// Optimise an erased expression by beta-reducing `TypeErased` applications.
953    ///
954    /// When the function position of an `App` is `TypeErased`, the whole
955    /// application is also `TypeErased` (the argument is a type).  This
956    /// recursively simplifies the tree.
957    pub fn optimize(&self, expr: ErasedExpr) -> ErasedExpr {
958        match expr {
959            ErasedExpr::App(f, arg) => {
960                let f_opt = self.optimize(*f);
961                let arg_opt = self.optimize(*arg);
962                match f_opt {
963                    ErasedExpr::TypeErased => ErasedExpr::TypeErased,
964                    _ => {
965                        if !self.config.keep_props && arg_opt == ErasedExpr::TypeErased {
966                            if let ErasedExpr::Lam(body) = f_opt {
967                                return self.optimize(subst_bvar(
968                                    *body,
969                                    0,
970                                    &ErasedExpr::TypeErased,
971                                ));
972                            }
973                        }
974                        ErasedExpr::App(Box::new(f_opt), Box::new(arg_opt))
975                    }
976                }
977            }
978            ErasedExpr::Lam(body) => ErasedExpr::Lam(Box::new(self.optimize(*body))),
979            ErasedExpr::Let(val, body) => ErasedExpr::Let(
980                Box::new(self.optimize(*val)),
981                Box::new(self.optimize(*body)),
982            ),
983            other => other,
984        }
985    }
986}
987/// A pattern in an erased match expression.
988#[allow(dead_code)]
989#[derive(Debug, Clone, PartialEq, Eq)]
990pub enum ErasedPattern {
991    /// Match any value (wildcard).
992    Wildcard,
993    /// Match a specific constructor tag.
994    Ctor(u32, Vec<ErasedPattern>),
995    /// Match a specific integer literal.
996    Lit(u64),
997    /// Bind a variable.
998    Var(String),
999}
1000impl ErasedPattern {
1001    /// Return the depth of the pattern.
1002    #[allow(dead_code)]
1003    pub fn depth(&self) -> usize {
1004        match self {
1005            ErasedPattern::Ctor(_, pats) => 1 + pats.iter().map(|p| p.depth()).max().unwrap_or(0),
1006            _ => 1,
1007        }
1008    }
1009    /// Return true if this pattern always matches.
1010    #[allow(dead_code)]
1011    pub fn is_irrefutable(&self) -> bool {
1012        matches!(self, ErasedPattern::Wildcard | ErasedPattern::Var(_))
1013    }
1014}
1015/// A substitution map from de Bruijn index to erased expression.
1016#[allow(dead_code)]
1017pub struct ErasedSubstMap {
1018    map: std::collections::HashMap<u32, ErasedExpr>,
1019}
1020#[allow(dead_code)]
1021impl ErasedSubstMap {
1022    /// Creates a new empty substitution map.
1023    pub fn new() -> Self {
1024        Self {
1025            map: std::collections::HashMap::new(),
1026        }
1027    }
1028    /// Inserts a substitution for de Bruijn index `i`.
1029    pub fn insert(&mut self, i: u32, expr: ErasedExpr) {
1030        self.map.insert(i, expr);
1031    }
1032    /// Looks up the substitution for de Bruijn index `i`.
1033    pub fn get(&self, i: u32) -> Option<&ErasedExpr> {
1034        self.map.get(&i)
1035    }
1036    /// Returns the number of entries in the map.
1037    pub fn len(&self) -> usize {
1038        self.map.len()
1039    }
1040    /// Returns `true` if the map is empty.
1041    pub fn is_empty(&self) -> bool {
1042        self.map.is_empty()
1043    }
1044}
1045/// Configuration for the type eraser.
1046#[derive(Debug, Clone, PartialEq, Eq, Default)]
1047pub struct EraseConfig {
1048    /// When true, keep `Prop`-sorted terms (proofs) as `TypeErased` rather
1049    /// than dropping them entirely.
1050    pub keep_props: bool,
1051    /// When true, inline small definitions before erasure.
1052    pub inline_defs: bool,
1053}
1054/// A normalizer for erased expressions (beta + delta reduction).
1055#[allow(dead_code)]
1056#[allow(missing_docs)]
1057pub struct ErasedNormalizer {
1058    pub beta_steps: u64,
1059    pub const_folds: u64,
1060    max_beta: u64,
1061}
1062#[allow(dead_code)]
1063impl ErasedNormalizer {
1064    /// Create a normalizer with a beta step limit.
1065    pub fn new(max_beta: u64) -> Self {
1066        ErasedNormalizer {
1067            beta_steps: 0,
1068            const_folds: 0,
1069            max_beta,
1070        }
1071    }
1072    /// Normalize an expression to weak head normal form (stub).
1073    pub fn whnf(&mut self, expr: ErasedExpr) -> ErasedExpr {
1074        if self.beta_steps >= self.max_beta {
1075            return expr;
1076        }
1077        match expr {
1078            ErasedExpr::App(f, x) => {
1079                let f_whnf = self.whnf(*f);
1080                match f_whnf {
1081                    ErasedExpr::Lam(_b) => {
1082                        self.beta_steps += 1;
1083                        self.whnf(*x)
1084                    }
1085                    other_f => ErasedExpr::App(Box::new(other_f), x),
1086                }
1087            }
1088            other => other,
1089        }
1090    }
1091    /// Constant-fold addition: Nat.add (Lit a) (Lit b) → Lit (a+b).
1092    pub fn const_fold_add(&mut self, expr: ErasedExpr) -> ErasedExpr {
1093        match &expr {
1094            ErasedExpr::App(f, x) => {
1095                if let ErasedExpr::App(g, a) = f.as_ref() {
1096                    if let ErasedExpr::Const(name) = g.as_ref() {
1097                        if name == "Nat.add" {
1098                            if let (ErasedExpr::Lit(av), ErasedExpr::Lit(bv)) =
1099                                (a.as_ref(), x.as_ref())
1100                            {
1101                                self.const_folds += 1;
1102                                return ErasedExpr::Lit(av.saturating_add(*bv));
1103                            }
1104                        }
1105                    }
1106                }
1107                expr
1108            }
1109            _ => expr,
1110        }
1111    }
1112}
1113/// A-normal form converter for erased expressions.
1114#[allow(dead_code)]
1115#[allow(missing_docs)]
1116pub struct AnfConverter {
1117    fresh_counter: u64,
1118    pub let_count: u64,
1119}
1120#[allow(dead_code)]
1121impl AnfConverter {
1122    /// Create a new converter.
1123    pub fn new() -> Self {
1124        AnfConverter {
1125            fresh_counter: 0,
1126            let_count: 0,
1127        }
1128    }
1129    /// Generate a fresh variable name.
1130    pub fn fresh(&mut self) -> String {
1131        let name = format!("_anf_{}", self.fresh_counter);
1132        self.fresh_counter += 1;
1133        name
1134    }
1135    /// Convert an expression to ANF.
1136    pub fn convert(&mut self, expr: ErasedExprExt) -> ErasedExprExt {
1137        match expr {
1138            ErasedExprExt::App(f, x) => {
1139                let f = self.convert(*f);
1140                let x = self.convert(*x);
1141                if !is_atom(&f) {
1142                    let _v = self.fresh();
1143                    self.let_count += 1;
1144                    ErasedExprExt::Let(
1145                        Box::new(f),
1146                        Box::new(ErasedExprExt::App(
1147                            Box::new(ErasedExprExt::BVar(0)),
1148                            Box::new(shift_up(x, 1)),
1149                        )),
1150                    )
1151                } else {
1152                    ErasedExprExt::App(Box::new(f), Box::new(x))
1153                }
1154            }
1155            ErasedExprExt::Lam(b) => ErasedExprExt::Lam(Box::new(self.convert(*b))),
1156            other => other,
1157        }
1158    }
1159}
1160/// An erased value (runtime representation after full reduction).
1161#[allow(dead_code)]
1162#[allow(missing_docs)]
1163#[derive(Debug, Clone, PartialEq)]
1164pub enum ErasedValue {
1165    /// An integer literal.
1166    Int(u64),
1167    /// A constructor applied to arguments.
1168    Ctor(u32, Vec<ErasedValue>),
1169    /// A closure (lambda) with its captured environment.
1170    Closure {
1171        body: Box<ErasedExprExt>,
1172        env: Vec<ErasedValue>,
1173    },
1174    /// A unit value.
1175    Unit,
1176    /// An unresolved thunk.
1177    Thunk(Box<ErasedExprExt>),
1178}
1179#[allow(dead_code)]
1180impl ErasedValue {
1181    /// Return true if this is an integer.
1182    pub fn is_int(&self) -> bool {
1183        matches!(self, ErasedValue::Int(_))
1184    }
1185    /// Return true if this is a constructor.
1186    pub fn is_ctor(&self) -> bool {
1187        matches!(self, ErasedValue::Ctor(_, _))
1188    }
1189    /// Return the integer value if this is Int, else None.
1190    pub fn as_int(&self) -> Option<u64> {
1191        if let ErasedValue::Int(n) = self {
1192            Some(*n)
1193        } else {
1194            None
1195        }
1196    }
1197}
1198/// Bit manipulation operations for erased literal values.
1199#[allow(dead_code)]
1200pub struct ErasedBitOps;
1201#[allow(dead_code)]
1202impl ErasedBitOps {
1203    /// Fold a list of literals with bitwise AND.
1204    pub fn fold_and(vals: &[u64]) -> u64 {
1205        vals.iter().fold(u64::MAX, |acc, &v| acc & v)
1206    }
1207    /// Fold a list of literals with bitwise OR.
1208    pub fn fold_or(vals: &[u64]) -> u64 {
1209        vals.iter().fold(0u64, |acc, &v| acc | v)
1210    }
1211    /// Fold a list of literals with a binary operation.
1212    pub fn fold_binop<F: Fn(u64, u64) -> u64>(vals: &[u64], init: u64, f: F) -> u64 {
1213        vals.iter().fold(init, |acc, &v| f(acc, v))
1214    }
1215}
1216/// Rename all free variables in an expression using a substitution map.
1217#[allow(dead_code)]
1218#[allow(missing_docs)]
1219pub struct ErasedRenamer {
1220    map: Vec<(String, String)>,
1221    pub renames: u64,
1222}
1223#[allow(dead_code)]
1224impl ErasedRenamer {
1225    /// Create a renamer with a substitution map.
1226    pub fn new(map: Vec<(String, String)>) -> Self {
1227        ErasedRenamer { map, renames: 0 }
1228    }
1229    /// Apply the renaming to an expression.
1230    pub fn rename(&mut self, expr: ErasedExprExt) -> ErasedExprExt {
1231        match expr {
1232            ErasedExprExt::FVar(name) => {
1233                if let Some(new) = self
1234                    .map
1235                    .iter()
1236                    .find(|(old, _)| old == &name)
1237                    .map(|(_, n)| n.clone())
1238                {
1239                    self.renames += 1;
1240                    ErasedExprExt::FVar(new)
1241                } else {
1242                    ErasedExprExt::FVar(name)
1243                }
1244            }
1245            ErasedExprExt::Const(name) => {
1246                if let Some(new) = self
1247                    .map
1248                    .iter()
1249                    .find(|(old, _)| old == &name)
1250                    .map(|(_, n)| n.clone())
1251                {
1252                    self.renames += 1;
1253                    ErasedExprExt::Const(new)
1254                } else {
1255                    ErasedExprExt::Const(name)
1256                }
1257            }
1258            ErasedExprExt::Lam(b) => ErasedExprExt::Lam(Box::new(self.rename(*b))),
1259            ErasedExprExt::App(f, x) => {
1260                ErasedExprExt::App(Box::new(self.rename(*f)), Box::new(self.rename(*x)))
1261            }
1262            ErasedExprExt::Let(v, b) => {
1263                ErasedExprExt::Let(Box::new(self.rename(*v)), Box::new(self.rename(*b)))
1264            }
1265            other => other,
1266        }
1267    }
1268}
1269/// A kernel expression with type information erased.
1270#[derive(Debug, Clone, PartialEq, Eq)]
1271pub enum ErasedExpr {
1272    /// Erased free variable.
1273    Var(String),
1274    /// Bound variable (de Bruijn index).
1275    BVar(u32),
1276    /// Lambda without type annotation.
1277    Lam(Box<ErasedExpr>),
1278    /// Application.
1279    App(Box<ErasedExpr>, Box<ErasedExpr>),
1280    /// Let binding without type.
1281    Let(Box<ErasedExpr>, Box<ErasedExpr>),
1282    /// Global constant reference.
1283    Const(String),
1284    /// Literal natural number.
1285    Lit(u64),
1286    /// String literal.
1287    StrLit(String),
1288    /// Placeholder for erased types (sorts, pi-types, etc.).
1289    TypeErased,
1290}
1291/// Describes a call site in the erased IR.
1292#[allow(dead_code)]
1293#[allow(missing_docs)]
1294pub struct ErasedCallSite {
1295    /// Name of the callee constant.
1296    pub callee: String,
1297    /// Arity of the call (number of arguments supplied).
1298    pub arity: usize,
1299    /// Whether this is a tail call.
1300    pub is_tail: bool,
1301}
1302#[allow(dead_code)]
1303impl ErasedCallSite {
1304    /// Creates a new call site descriptor.
1305    pub fn new(callee: impl Into<String>, arity: usize, is_tail: bool) -> Self {
1306        Self {
1307            callee: callee.into(),
1308            arity,
1309            is_tail,
1310        }
1311    }
1312    /// Returns `true` if the call is a self-recursive tail call.
1313    pub fn is_self_tail(&self, current: &str) -> bool {
1314        self.is_tail && self.callee == current
1315    }
1316}
1317/// Checks size bounds on erased expressions.
1318#[allow(dead_code)]
1319#[allow(missing_docs)]
1320pub struct ErasedSizeBound {
1321    pub max_size: usize,
1322}
1323#[allow(dead_code)]
1324impl ErasedSizeBound {
1325    /// Create a size checker.
1326    pub fn new(max_size: usize) -> Self {
1327        ErasedSizeBound { max_size }
1328    }
1329    /// Return whether an expression is within the size bound.
1330    pub fn check(&self, expr: &ErasedExprExt) -> bool {
1331        expr.size() <= self.max_size
1332    }
1333    /// Return the size of an expression.
1334    pub fn size_of(&self, expr: &ErasedExprExt) -> usize {
1335        expr.size()
1336    }
1337}
1338/// Statistics collected during type erasure.
1339#[derive(Debug, Clone, Default)]
1340pub struct ErasureStats {
1341    /// Number of sorts (universes) erased.
1342    pub sorts_erased: usize,
1343    /// Number of Pi-types erased.
1344    pub pis_erased: usize,
1345    /// Number of computational terms kept.
1346    pub terms_kept: usize,
1347}
1348impl ErasureStats {
1349    /// Create a zeroed statistics record.
1350    pub fn new() -> Self {
1351        ErasureStats::default()
1352    }
1353    /// Record one erased sort.
1354    pub fn add_sort(&mut self) {
1355        self.sorts_erased += 1;
1356    }
1357    /// Record one erased Pi-type.
1358    pub fn add_pi(&mut self) {
1359        self.pis_erased += 1;
1360    }
1361    /// Record one kept computational term.
1362    pub fn add_term(&mut self) {
1363        self.terms_kept += 1;
1364    }
1365    /// Fraction of nodes that were erased (sorts + pis out of total).
1366    ///
1367    /// Returns `0.0` when no nodes have been recorded.
1368    pub fn ratio_erased(&self) -> f64 {
1369        let total = self.sorts_erased + self.pis_erased + self.terms_kept;
1370        if total == 0 {
1371            0.0
1372        } else {
1373            (self.sorts_erased + self.pis_erased) as f64 / total as f64
1374        }
1375    }
1376}
1377/// A reachability tracker for erased expressions.
1378#[allow(dead_code)]
1379pub struct ErasedReachability {
1380    reachable: Vec<String>,
1381    roots: Vec<String>,
1382}
1383#[allow(dead_code)]
1384impl ErasedReachability {
1385    /// Create a new tracker.
1386    pub fn new() -> Self {
1387        ErasedReachability {
1388            reachable: Vec::new(),
1389            roots: Vec::new(),
1390        }
1391    }
1392    /// Add a root (entry point).
1393    pub fn add_root(&mut self, name: &str) {
1394        if !self.roots.contains(&name.to_string()) {
1395            self.roots.push(name.to_string());
1396            self.mark_reachable(name);
1397        }
1398    }
1399    /// Mark a constant as reachable.
1400    pub fn mark_reachable(&mut self, name: &str) {
1401        if !self.reachable.contains(&name.to_string()) {
1402            self.reachable.push(name.to_string());
1403        }
1404    }
1405    /// Return whether a constant is reachable.
1406    pub fn is_reachable(&self, name: &str) -> bool {
1407        self.reachable.contains(&name.to_string())
1408    }
1409    /// Return all reachable names.
1410    pub fn reachable_names(&self) -> &[String] {
1411        &self.reachable
1412    }
1413    /// Return the number of reachable declarations.
1414    pub fn reachable_count(&self) -> usize {
1415        self.reachable.len()
1416    }
1417    /// Process a module: mark all consts reachable from roots as reachable.
1418    pub fn analyze_module(&mut self, module: &ErasedModule) {
1419        let root_names = self.roots.clone();
1420        for root in &root_names {
1421            if let Some(ErasedDecl::Def { body, .. }) = module.find(root) {
1422                for c in collect_consts(body) {
1423                    self.mark_reachable(&c);
1424                }
1425            }
1426        }
1427    }
1428}
1429/// A chain of let-bindings produced by ANF conversion.
1430#[allow(dead_code)]
1431#[allow(missing_docs)]
1432pub struct ErasedLetChain {
1433    /// The binding pairs: (name_hint, rhs).
1434    pub bindings: Vec<(String, ErasedExprExt)>,
1435    /// The final body after all bindings.
1436    pub body: ErasedExprExt,
1437}
1438#[allow(dead_code)]
1439impl ErasedLetChain {
1440    /// Create an empty chain with the given body.
1441    pub fn new(body: ErasedExprExt) -> Self {
1442        Self {
1443            bindings: Vec::new(),
1444            body,
1445        }
1446    }
1447    /// Push a new binding onto the chain (outermost = last).
1448    pub fn push(&mut self, name: impl Into<String>, rhs: ErasedExprExt) {
1449        self.bindings.push((name.into(), rhs));
1450    }
1451    /// Convert the chain back into nested `ErasedExprExt::Let` nodes.
1452    pub fn into_expr(self) -> ErasedExprExt {
1453        let mut result = self.body;
1454        for (_name, rhs) in self.bindings.into_iter().rev() {
1455            result = ErasedExprExt::Let(Box::new(rhs), Box::new(result));
1456        }
1457        result
1458    }
1459    /// Returns the number of bindings in the chain.
1460    pub fn len(&self) -> usize {
1461        self.bindings.len()
1462    }
1463    /// Returns `true` if there are no bindings.
1464    pub fn is_empty(&self) -> bool {
1465        self.bindings.is_empty()
1466    }
1467}
1468/// Constant folding for erased arithmetic expressions.
1469#[allow(dead_code)]
1470#[allow(missing_docs)]
1471pub struct ErasedConstFolder {
1472    pub folds: u64,
1473}
1474#[allow(dead_code)]
1475impl ErasedConstFolder {
1476    /// Create a constant folder.
1477    pub fn new() -> Self {
1478        ErasedConstFolder { folds: 0 }
1479    }
1480    /// Try to constant-fold an application of a built-in operator.
1481    pub fn fold_add(&mut self, expr: ErasedExprExt) -> ErasedExprExt {
1482        match expr {
1483            ErasedExprExt::App(f, x) => {
1484                let f = self.fold_add(*f);
1485                let x = self.fold_add(*x);
1486                match (&f, &x) {
1487                    (ErasedExprExt::App(g, a), ErasedExprExt::Lit(b)) => {
1488                        if let ErasedExprExt::Const(name) = g.as_ref() {
1489                            if name == "Nat.add" {
1490                                if let ErasedExprExt::Lit(av) = a.as_ref() {
1491                                    self.folds += 1;
1492                                    return ErasedExprExt::Lit(av.saturating_add(*b));
1493                                }
1494                            }
1495                        }
1496                        ErasedExprExt::App(
1497                            Box::new(ErasedExprExt::App(
1498                                Box::new(*g.clone()),
1499                                Box::new(*a.clone()),
1500                            )),
1501                            Box::new(x),
1502                        )
1503                    }
1504                    _ => ErasedExprExt::App(Box::new(f), Box::new(x)),
1505                }
1506            }
1507            ErasedExprExt::Lam(b) => ErasedExprExt::Lam(Box::new(self.fold_add(*b))),
1508            other => other,
1509        }
1510    }
1511}
1512/// An erased module declaration.
1513#[allow(dead_code)]
1514#[allow(missing_docs)]
1515#[derive(Debug, Clone)]
1516pub enum ErasedDecl {
1517    /// A function definition.
1518    Def { name: String, body: ErasedExprExt },
1519    /// An axiom (no body).
1520    Axiom { name: String },
1521    /// An inductive type with constructor count.
1522    Inductive { name: String, ctor_count: u32 },
1523}
1524#[allow(dead_code)]
1525impl ErasedDecl {
1526    /// Return the name of this declaration.
1527    pub fn name(&self) -> &str {
1528        match self {
1529            ErasedDecl::Def { name, .. } => name,
1530            ErasedDecl::Axiom { name } => name,
1531            ErasedDecl::Inductive { name, .. } => name,
1532        }
1533    }
1534    /// Return true if this is a function definition.
1535    pub fn is_def(&self) -> bool {
1536        matches!(self, ErasedDecl::Def { .. })
1537    }
1538}
1539/// A scope for erased code: a stack of local bindings.
1540#[allow(dead_code)]
1541pub struct ErasedScope {
1542    vars: Vec<(String, ErasedValue)>,
1543}
1544#[allow(dead_code)]
1545impl ErasedScope {
1546    /// Create an empty scope.
1547    pub fn new() -> Self {
1548        ErasedScope { vars: Vec::new() }
1549    }
1550    /// Bind a variable.
1551    pub fn bind(&mut self, name: &str, val: ErasedValue) {
1552        self.vars.push((name.to_string(), val));
1553    }
1554    /// Look up a variable.
1555    pub fn lookup(&self, name: &str) -> Option<&ErasedValue> {
1556        self.vars
1557            .iter()
1558            .rev()
1559            .find(|(n, _)| n == name)
1560            .map(|(_, v)| v)
1561    }
1562    /// Return the scope depth.
1563    pub fn depth(&self) -> usize {
1564        self.vars.len()
1565    }
1566    /// Push a checkpoint and return it (index into vars).
1567    pub fn save(&self) -> usize {
1568        self.vars.len()
1569    }
1570    /// Restore to a checkpoint.
1571    pub fn restore(&mut self, checkpoint: usize) {
1572        self.vars.truncate(checkpoint);
1573    }
1574}
oxilean_kernel/type_erasure/types.rs

oxilean_kernel/type_erasure/
types.rs
