oxilean_codegen/to_lcnf/
types.rs

1//! Auto-generated module
2//!
3//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)
4
5use crate::lcnf::*;
6use oxilean_kernel::{BinderInfo, Expr, Level, Literal, Name};
7use std::collections::{HashMap, HashSet, VecDeque};
8
9/// Statistics collected during the conversion process.
10#[derive(Clone, Debug, Default)]
11pub struct ConversionStats {
12    /// Total number of kernel expressions visited.
13    pub exprs_visited: usize,
14    /// Number of let bindings generated (ANF intermediaries).
15    pub let_bindings_generated: usize,
16    /// Number of lambdas lifted to top level.
17    pub lambdas_lifted: usize,
18    /// Number of proof terms erased.
19    pub proofs_erased: usize,
20    /// Number of type arguments erased.
21    pub types_erased: usize,
22    /// Number of closures converted.
23    pub closures_converted: usize,
24    /// Maximum nesting depth reached during conversion.
25    pub max_depth: usize,
26    /// Number of tail calls detected.
27    pub tail_calls_detected: usize,
28    /// Number of fresh variables allocated.
29    pub fresh_vars_allocated: usize,
30    /// Number of free variable computations performed.
31    pub free_var_computations: usize,
32}
33/// Internal state for the kernel Expr to LCNF conversion.
34///
35/// Maintains fresh variable counters, name mappings, lifted function
36/// declarations, and accumulated metadata.
37pub struct ToLcnfState {
38    /// Next fresh variable counter.
39    pub(super) next_var: u64,
40    /// Map from kernel name strings to LCNF variable IDs.
41    pub(super) name_map: HashMap<String, LcnfVarId>,
42    /// Map from kernel name strings to LCNF types.
43    pub(super) type_map: HashMap<String, LcnfType>,
44    /// Accumulated lifted function declarations.
45    pub(super) lifted_funs: Vec<LcnfFunDecl>,
46    /// The conversion configuration.
47    pub(super) config: ToLcnfConfig,
48    /// Current nesting depth (for depth limit checks).
49    pub(super) depth: usize,
50    /// Accumulated module metadata.
51    pub(super) metadata: LcnfModuleMetadata,
52    /// Conversion statistics.
53    pub(super) stats: ConversionStats,
54    /// De Bruijn index to variable ID mapping.
55    pub(super) bvar_stack: Vec<LcnfVarId>,
56    /// De Bruijn index to name hint mapping.
57    pub(super) bvar_names: Vec<String>,
58    /// Set of known proof-sorted names for quick lookup.
59    pub(super) proof_names: HashSet<String>,
60    /// Set of known type-sorted names for quick lookup.
61    pub(super) type_names: HashSet<String>,
62    /// Counter for generating lifted function names.
63    pub(super) lift_counter: u64,
64    /// Pending let bindings accumulated during ANF conversion.
65    pub(super) pending_lets: VecDeque<(LcnfVarId, String, LcnfType, LcnfLetValue)>,
66    /// Maximum allowed conversion depth.
67    pub(super) max_depth: usize,
68}
69impl ToLcnfState {
70    /// Create a new conversion state with the given configuration.
71    pub(super) fn new(config: &ToLcnfConfig) -> Self {
72        ToLcnfState {
73            next_var: 0,
74            name_map: HashMap::new(),
75            type_map: HashMap::new(),
76            lifted_funs: Vec::new(),
77            config: config.clone(),
78            depth: 0,
79            metadata: LcnfModuleMetadata::default(),
80            stats: ConversionStats::default(),
81            bvar_stack: Vec::new(),
82            bvar_names: Vec::new(),
83            proof_names: HashSet::new(),
84            type_names: HashSet::new(),
85            lift_counter: 0,
86            pending_lets: VecDeque::new(),
87            max_depth: 1024,
88        }
89    }
90    /// Generate a fresh LCNF variable ID.
91    pub(super) fn fresh_var(&mut self) -> LcnfVarId {
92        let id = LcnfVarId(self.next_var);
93        self.next_var += 1;
94        self.stats.fresh_vars_allocated += 1;
95        id
96    }
97    /// Generate a fresh variable with a name hint, registering it in the name map.
98    pub(super) fn fresh_named_var(&mut self, hint: &str) -> LcnfVarId {
99        let id = self.fresh_var();
100        let name = if self.config.debug_names {
101            format!("{}_{}", hint, id.0)
102        } else {
103            format!("_x{}", id.0)
104        };
105        self.name_map.insert(name, id);
106        id
107    }
108    /// Generate a fresh name for a lifted function.
109    pub(super) fn fresh_lift_name(&mut self, base: &str) -> String {
110        let name = format!("{}_lifted_{}", base, self.lift_counter);
111        self.lift_counter += 1;
112        name
113    }
114    /// Push a de Bruijn variable binding.
115    pub(super) fn push_bvar(&mut self, id: LcnfVarId, name: &str) {
116        self.bvar_stack.push(id);
117        self.bvar_names.push(name.to_string());
118    }
119    /// Pop a de Bruijn variable binding.
120    pub(super) fn pop_bvar(&mut self) {
121        self.bvar_stack.pop();
122        self.bvar_names.pop();
123    }
124    /// Look up a de Bruijn index in the current scope.
125    pub(super) fn lookup_bvar(&self, idx: u32) -> Option<LcnfVarId> {
126        let stack_len = self.bvar_stack.len();
127        if (idx as usize) < stack_len {
128            Some(self.bvar_stack[stack_len - 1 - idx as usize])
129        } else {
130            None
131        }
132    }
133    /// Look up a de Bruijn index name hint in the current scope.
134    pub(super) fn lookup_bvar_name(&self, idx: u32) -> Option<&str> {
135        let stack_len = self.bvar_names.len();
136        if (idx as usize) < stack_len {
137            Some(&self.bvar_names[stack_len - 1 - idx as usize])
138        } else {
139            None
140        }
141    }
142    /// Look up a name in the name map to find its variable ID.
143    pub(super) fn lookup_name(&self, name: &str) -> Option<LcnfVarId> {
144        self.name_map.get(name).copied()
145    }
146    /// Register a name as proof-sorted (will be erased if erase_proofs is enabled).
147    pub(super) fn mark_as_proof(&mut self, name: &str) {
148        self.proof_names.insert(name.to_string());
149    }
150    /// Check if a name is known to be proof-sorted.
151    pub(super) fn is_proof_name(&self, name: &str) -> bool {
152        self.proof_names.contains(name)
153    }
154    /// Register a name as type-sorted (will be erased if erase_types is enabled).
155    pub(super) fn mark_as_type(&mut self, name: &str) {
156        self.type_names.insert(name.to_string());
157    }
158    /// Check if a name is known to be type-sorted.
159    pub(super) fn is_type_name(&self, name: &str) -> bool {
160        self.type_names.contains(name)
161    }
162    /// Enter a deeper nesting level, checking the depth limit.
163    pub(super) fn enter_depth(&mut self) -> Result<(), ConversionError> {
164        self.depth += 1;
165        if self.depth > self.stats.max_depth {
166            self.stats.max_depth = self.depth;
167        }
168        if self.depth > self.max_depth {
169            return Err(ConversionError::DepthLimitExceeded(self.depth));
170        }
171        Ok(())
172    }
173    /// Leave the current nesting level.
174    pub(super) fn leave_depth(&mut self) {
175        if self.depth > 0 {
176            self.depth -= 1;
177        }
178    }
179    /// Wrap a terminal expression with any accumulated pending let bindings.
180    pub(super) fn wrap_pending_lets(&mut self, terminal: LcnfExpr) -> LcnfExpr {
181        let mut result = terminal;
182        while let Some((id, name, ty, value)) = self.pending_lets.pop_back() {
183            result = LcnfExpr::Let {
184                id,
185                name,
186                ty,
187                value,
188                body: Box::new(result),
189            };
190        }
191        result
192    }
193    /// Emit a let binding and return the variable ID referring to it.
194    pub(super) fn emit_let(&mut self, hint: &str, ty: LcnfType, value: LcnfLetValue) -> LcnfVarId {
195        let id = self.fresh_named_var(hint);
196        let name = if self.config.debug_names {
197            format!("{}_{}", hint, id.0)
198        } else {
199            format!("_x{}", id.0)
200        };
201        self.pending_lets.push_back((id, name, ty, value));
202        self.stats.let_bindings_generated += 1;
203        self.metadata.let_bindings += 1;
204        id
205    }
206    /// Get the conversion statistics so far.
207    pub(super) fn get_stats(&self) -> &ConversionStats {
208        &self.stats
209    }
210    /// Finalize and return all accumulated lifted function declarations.
211    pub(super) fn take_lifted_funs(&mut self) -> Vec<LcnfFunDecl> {
212        std::mem::take(&mut self.lifted_funs)
213    }
214}
215/// Context for the lambda lifting pass.
216pub struct LambdaLifter {
217    /// Accumulated lifted function declarations.
218    pub(super) lifted: Vec<LcnfFunDecl>,
219    /// Counter for unique lifted function names.
220    pub(super) lift_counter: u64,
221    /// Mapping from original variable IDs to their replacement after lifting.
222    pub(super) var_remap: HashMap<LcnfVarId, LcnfVarId>,
223    /// Maximum inline size (lambdas smaller than this stay inline).
224    pub(super) max_inline_size: usize,
225}
226impl LambdaLifter {
227    pub(super) fn new(max_inline_size: usize) -> Self {
228        LambdaLifter {
229            lifted: Vec::new(),
230            lift_counter: 0,
231            var_remap: HashMap::new(),
232            max_inline_size,
233        }
234    }
235    /// Generate a unique name for a lifted function.
236    pub(super) fn fresh_name(&mut self, base: &str) -> String {
237        let name = format!("{}_ll_{}", base, self.lift_counter);
238        self.lift_counter += 1;
239        name
240    }
241    /// Run the lambda lifting pass on a module's function declarations.
242    pub(super) fn lift_module(&mut self, decls: &mut Vec<LcnfFunDecl>) {
243        for decl in decls.iter_mut() {
244            self.lift_body(&mut decl.body, &decl.name);
245        }
246        decls.append(&mut self.lifted);
247    }
248    /// Recursively process an LCNF expression, lifting lambdas.
249    pub(super) fn lift_body(&mut self, expr: &mut LcnfExpr, parent_name: &str) {
250        match expr {
251            LcnfExpr::Let { value, body, .. } => {
252                self.lift_let_value(value, parent_name);
253                self.lift_body(body, parent_name);
254            }
255            LcnfExpr::Case { alts, default, .. } => {
256                for alt in alts.iter_mut() {
257                    self.lift_body(&mut alt.body, parent_name);
258                }
259                if let Some(def) = default.as_mut() {
260                    self.lift_body(def, parent_name);
261                }
262            }
263            LcnfExpr::Return(_) | LcnfExpr::Unreachable | LcnfExpr::TailCall(_, _) => {}
264        }
265    }
266    /// Process a let-value for potential lambda lifting.
267    pub(super) fn lift_let_value(&mut self, value: &mut LcnfLetValue, _parent_name: &str) {
268        match value {
269            LcnfLetValue::App(func, args) => {
270                self.remap_arg(func);
271                for arg in args.iter_mut() {
272                    self.remap_arg(arg);
273                }
274            }
275            LcnfLetValue::Ctor(_, _, args) => {
276                for arg in args.iter_mut() {
277                    self.remap_arg(arg);
278                }
279            }
280            LcnfLetValue::Proj(_, _, var) => {
281                if let Some(remapped) = self.var_remap.get(var) {
282                    *var = *remapped;
283                }
284            }
285            LcnfLetValue::FVar(var) => {
286                if let Some(remapped) = self.var_remap.get(var) {
287                    *var = *remapped;
288                }
289            }
290            LcnfLetValue::Lit(_)
291            | LcnfLetValue::Erased
292            | LcnfLetValue::Reset(_)
293            | LcnfLetValue::Reuse(_, _, _, _) => {}
294        }
295    }
296    /// Remap a variable reference if it was previously lifted.
297    pub(super) fn remap_arg(&self, arg: &mut LcnfArg) {
298        if let LcnfArg::Var(id) = arg {
299            if let Some(remapped) = self.var_remap.get(id) {
300                *id = *remapped;
301            }
302        }
303    }
304    /// Compute the set of free LCNF variable IDs in an expression.
305    pub(super) fn free_vars_of_expr(&self, expr: &LcnfExpr) -> HashSet<LcnfVarId> {
306        let mut free = HashSet::new();
307        let mut bound = HashSet::new();
308        self.collect_free_lcnf(expr, &mut free, &mut bound);
309        free
310    }
311    /// Recursively collect free variables in an LCNF expression.
312    pub(super) fn collect_free_lcnf(
313        &self,
314        expr: &LcnfExpr,
315        free: &mut HashSet<LcnfVarId>,
316        bound: &mut HashSet<LcnfVarId>,
317    ) {
318        match expr {
319            LcnfExpr::Let {
320                id, value, body, ..
321            } => {
322                self.collect_free_let_value(value, free, bound);
323                bound.insert(*id);
324                self.collect_free_lcnf(body, free, bound);
325            }
326            LcnfExpr::Case {
327                scrutinee,
328                alts,
329                default,
330                ..
331            } => {
332                if !bound.contains(scrutinee) {
333                    free.insert(*scrutinee);
334                }
335                for alt in alts {
336                    let mut alt_bound = bound.clone();
337                    for p in &alt.params {
338                        alt_bound.insert(p.id);
339                    }
340                    self.collect_free_lcnf(&alt.body, free, &mut alt_bound);
341                }
342                if let Some(def) = default {
343                    self.collect_free_lcnf(def, free, bound);
344                }
345            }
346            LcnfExpr::Return(arg) => {
347                self.collect_free_arg(arg, free, bound);
348            }
349            LcnfExpr::TailCall(func, args) => {
350                self.collect_free_arg(func, free, bound);
351                for a in args {
352                    self.collect_free_arg(a, free, bound);
353                }
354            }
355            LcnfExpr::Unreachable => {}
356        }
357    }
358    /// Collect free variables in a let-value.
359    pub(super) fn collect_free_let_value(
360        &self,
361        value: &LcnfLetValue,
362        free: &mut HashSet<LcnfVarId>,
363        bound: &HashSet<LcnfVarId>,
364    ) {
365        match value {
366            LcnfLetValue::App(func, args) => {
367                self.collect_free_arg(func, free, bound);
368                for a in args {
369                    self.collect_free_arg(a, free, bound);
370                }
371            }
372            LcnfLetValue::Proj(_, _, var) => {
373                if !bound.contains(var) {
374                    free.insert(*var);
375                }
376            }
377            LcnfLetValue::Ctor(_, _, args) => {
378                for a in args {
379                    self.collect_free_arg(a, free, bound);
380                }
381            }
382            LcnfLetValue::FVar(var) => {
383                if !bound.contains(var) {
384                    free.insert(*var);
385                }
386            }
387            LcnfLetValue::Lit(_)
388            | LcnfLetValue::Erased
389            | LcnfLetValue::Reset(_)
390            | LcnfLetValue::Reuse(_, _, _, _) => {}
391        }
392    }
393    /// Collect free variables in an argument.
394    pub(super) fn collect_free_arg(
395        &self,
396        arg: &LcnfArg,
397        free: &mut HashSet<LcnfVarId>,
398        bound: &HashSet<LcnfVarId>,
399    ) {
400        if let LcnfArg::Var(id) = arg {
401            if !bound.contains(id) {
402                free.insert(*id);
403            }
404        }
405    }
406}
407/// Configuration for the kernel Expr to LCNF conversion.
408///
409/// Controls which passes are enabled and how aggressively they are applied.
410#[derive(Clone, Debug)]
411pub struct ToLcnfConfig {
412    /// Whether to erase proof terms (Prop-sorted expressions).
413    pub erase_proofs: bool,
414    /// Whether to erase type arguments.
415    pub erase_types: bool,
416    /// Whether to perform lambda lifting.
417    pub lambda_lift: bool,
418    /// Maximum size (in AST nodes) for a lambda to be left inline.
419    pub max_inline_size: usize,
420    /// Whether to generate debug-friendly names.
421    pub debug_names: bool,
422}
423impl ToLcnfConfig {
424    /// Create a config with all passes enabled.
425    pub fn full() -> Self {
426        ToLcnfConfig {
427            erase_proofs: true,
428            erase_types: true,
429            lambda_lift: true,
430            max_inline_size: 8,
431            debug_names: false,
432        }
433    }
434    /// Create a config with no passes enabled (raw conversion only).
435    pub fn minimal() -> Self {
436        ToLcnfConfig {
437            erase_proofs: false,
438            erase_types: false,
439            lambda_lift: false,
440            max_inline_size: 0,
441            debug_names: true,
442        }
443    }
444    /// Create a config for debugging (names preserved, minimal erasure).
445    pub fn debug() -> Self {
446        ToLcnfConfig {
447            erase_proofs: false,
448            erase_types: false,
449            lambda_lift: false,
450            max_inline_size: 0,
451            debug_names: true,
452        }
453    }
454}
455/// Context for the proof erasure pass.
456pub struct ProofEraser {
457    /// Set of variable IDs known to be proof terms.
458    pub(super) proof_vars: HashSet<LcnfVarId>,
459    /// Number of proofs erased.
460    pub(super) erased_count: usize,
461}
462impl ProofEraser {
463    pub(super) fn new() -> Self {
464        ProofEraser {
465            proof_vars: HashSet::new(),
466            erased_count: 0,
467        }
468    }
469    /// Run proof erasure on a function declaration.
470    pub(super) fn erase_decl(&mut self, decl: &mut LcnfFunDecl) {
471        for param in &decl.params {
472            if param.ty == LcnfType::Irrelevant || param.erased {
473                self.proof_vars.insert(param.id);
474            }
475        }
476        self.erase_expr(&mut decl.body);
477        for param in &mut decl.params {
478            if self.proof_vars.contains(&param.id) {
479                param.erased = true;
480            }
481        }
482    }
483    /// Recursively erase proof terms in an expression.
484    pub(super) fn erase_expr(&mut self, expr: &mut LcnfExpr) {
485        match expr {
486            LcnfExpr::Let {
487                id,
488                ty,
489                value,
490                body,
491                ..
492            } => {
493                if *ty == LcnfType::Irrelevant {
494                    self.proof_vars.insert(*id);
495                    *value = LcnfLetValue::Erased;
496                    self.erased_count += 1;
497                } else {
498                    self.erase_let_value(value);
499                }
500                self.erase_expr(body);
501            }
502            LcnfExpr::Case {
503                scrutinee,
504                alts,
505                default,
506                ..
507            } => {
508                if self.proof_vars.contains(scrutinee) {
509                    if let Some(alt) = alts.first_mut() {
510                        self.erase_expr(&mut alt.body);
511                    }
512                    if let Some(def) = default.as_mut() {
513                        self.erase_expr(def);
514                    }
515                } else {
516                    for alt in alts.iter_mut() {
517                        for p in &alt.params {
518                            if p.ty == LcnfType::Irrelevant || p.erased {
519                                self.proof_vars.insert(p.id);
520                            }
521                        }
522                        self.erase_expr(&mut alt.body);
523                    }
524                    if let Some(def) = default.as_mut() {
525                        self.erase_expr(def);
526                    }
527                }
528            }
529            LcnfExpr::Return(arg) => {
530                self.erase_arg(arg);
531            }
532            LcnfExpr::TailCall(func, args) => {
533                self.erase_arg(func);
534                for a in args.iter_mut() {
535                    self.erase_arg(a);
536                }
537            }
538            LcnfExpr::Unreachable => {}
539        }
540    }
541    /// Erase proof references in a let-value.
542    pub(super) fn erase_let_value(&mut self, value: &mut LcnfLetValue) {
543        match value {
544            LcnfLetValue::App(func, args) => {
545                self.erase_arg(func);
546                for a in args.iter_mut() {
547                    self.erase_arg(a);
548                }
549            }
550            LcnfLetValue::Ctor(_, _, args) => {
551                for a in args.iter_mut() {
552                    self.erase_arg(a);
553                }
554            }
555            LcnfLetValue::Proj(_, _, var) => {
556                if self.proof_vars.contains(var) {
557                    *value = LcnfLetValue::Erased;
558                    self.erased_count += 1;
559                }
560            }
561            LcnfLetValue::FVar(var) => {
562                if self.proof_vars.contains(var) {
563                    *value = LcnfLetValue::Erased;
564                    self.erased_count += 1;
565                }
566            }
567            LcnfLetValue::Lit(_)
568            | LcnfLetValue::Erased
569            | LcnfLetValue::Reset(_)
570            | LcnfLetValue::Reuse(_, _, _, _) => {}
571        }
572    }
573    /// Erase a proof argument reference.
574    pub(super) fn erase_arg(&mut self, arg: &mut LcnfArg) {
575        if let LcnfArg::Var(id) = arg {
576            if self.proof_vars.contains(id) {
577                *arg = LcnfArg::Erased;
578                self.erased_count += 1;
579            }
580        }
581    }
582}
583/// Context for closure conversion.
584///
585/// Closure conversion makes all captured variables explicit by replacing
586/// closures with pairs of (function pointer, environment struct).
587pub struct ClosureConverter {
588    /// Counter for closure struct names.
589    pub(super) closure_counter: u64,
590    /// Generated closure struct declarations (name -> field types).
591    pub(super) closure_structs: HashMap<String, Vec<(String, LcnfType)>>,
592    /// Number of closures converted.
593    pub(super) converted_count: usize,
594}
595impl ClosureConverter {
596    pub(super) fn new() -> Self {
597        ClosureConverter {
598            closure_counter: 0,
599            closure_structs: HashMap::new(),
600            converted_count: 0,
601        }
602    }
603    /// Generate a fresh closure struct name.
604    pub(super) fn fresh_closure_name(&mut self) -> String {
605        let name = format!("Closure_{}", self.closure_counter);
606        self.closure_counter += 1;
607        name
608    }
609    /// Run closure conversion on a module.
610    pub(super) fn convert_module(&mut self, module: &mut LcnfModule) {
611        for decl in &mut module.fun_decls {
612            if decl.is_lifted {
613                self.convert_decl(decl);
614            }
615        }
616    }
617    /// Convert closures in a function declaration.
618    pub(super) fn convert_decl(&mut self, decl: &mut LcnfFunDecl) {
619        let bound: HashSet<LcnfVarId> = decl.params.iter().map(|p| p.id).collect();
620        self.convert_expr(&mut decl.body, &bound);
621    }
622    /// Recursively convert closures in an expression.
623    pub(super) fn convert_expr(&mut self, expr: &mut LcnfExpr, bound: &HashSet<LcnfVarId>) {
624        match expr {
625            LcnfExpr::Let {
626                id, value, body, ..
627            } => {
628                self.convert_let_value(value, bound);
629                let mut new_bound = bound.clone();
630                new_bound.insert(*id);
631                self.convert_expr(body, &new_bound);
632            }
633            LcnfExpr::Case { alts, default, .. } => {
634                for alt in alts.iter_mut() {
635                    let mut alt_bound = bound.clone();
636                    for p in &alt.params {
637                        alt_bound.insert(p.id);
638                    }
639                    self.convert_expr(&mut alt.body, &alt_bound);
640                }
641                if let Some(def) = default.as_mut() {
642                    self.convert_expr(def, bound);
643                }
644            }
645            LcnfExpr::Return(_) | LcnfExpr::Unreachable | LcnfExpr::TailCall(_, _) => {}
646        }
647    }
648    /// Convert closures in a let-value.
649    pub(super) fn convert_let_value(
650        &mut self,
651        value: &mut LcnfLetValue,
652        _bound: &HashSet<LcnfVarId>,
653    ) {
654        if let LcnfLetValue::App(_, args) = value {
655            let has_captured = args.iter().any(|a| matches!(a, LcnfArg::Var(_)));
656            if has_captured {
657                self.converted_count += 1;
658            }
659        }
660    }
661    /// Build a closure environment constructor expression.
662    pub(super) fn build_closure_env(
663        &mut self,
664        captured: &[(LcnfVarId, LcnfType)],
665    ) -> (String, LcnfLetValue) {
666        let closure_name = self.fresh_closure_name();
667        let fields: Vec<(String, LcnfType)> = captured
668            .iter()
669            .enumerate()
670            .map(|(i, (_, ty))| (format!("cap_{}", i), ty.clone()))
671            .collect();
672        self.closure_structs.insert(closure_name.clone(), fields);
673        let args: Vec<LcnfArg> = captured.iter().map(|(id, _)| LcnfArg::Var(*id)).collect();
674        let ctor_val = LcnfLetValue::Ctor(closure_name.clone(), 0, args);
675        (closure_name, ctor_val)
676    }
677}
678/// Errors that can occur during kernel-to-LCNF conversion.
679#[derive(Clone, Debug)]
680pub enum ConversionError {
681    /// Encountered an unsupported expression form.
682    UnsupportedExpr(String),
683    /// A free variable was not found in the current scope.
684    UnboundVariable(String),
685    /// The depth limit for recursive conversion was exceeded.
686    DepthLimitExceeded(usize),
687    /// An invalid binder configuration was encountered.
688    InvalidBinder(String),
689    /// A type conversion error.
690    TypeConversionError(String),
691    /// Lambda lifting failed for the given reason.
692    LambdaLiftError(String),
693    /// Closure conversion failed.
694    ClosureConversionError(String),
695    /// ANF conversion produced an invalid result.
696    AnfConversionError(String),
697    /// Proof erasure encountered an unexpected form.
698    ProofErasureError(String),
699    /// General internal error.
700    InternalError(String),
701}
oxilean_codegen/to_lcnf/types.rs

oxilean_codegen/to_lcnf/
types.rs
