oxilean_codegen/lcnf/
types.rs

1//! Auto-generated module
2//!
3//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)
4
5use super::functions::*;
6use oxilean_kernel::Name;
7use std::collections::{HashMap, HashSet};
8
9/// Metadata about an LCNF module.
10#[derive(Clone, Debug, Default)]
11pub struct LcnfModuleMetadata {
12    /// Number of declarations converted.
13    pub decl_count: usize,
14    /// Number of lambdas lifted.
15    pub lambdas_lifted: usize,
16    /// Number of proofs erased.
17    pub proofs_erased: usize,
18    /// Number of types erased.
19    pub types_erased: usize,
20    /// Total LCNF let bindings generated.
21    pub let_bindings: usize,
22}
23/// An argument to a function call or constructor in LCNF.
24///
25/// In ANF, arguments must be "atomic" — either variables or literals.
26#[derive(Clone, PartialEq, Eq, Hash, Debug)]
27pub enum LcnfArg {
28    /// A variable reference.
29    Var(LcnfVarId),
30    /// A literal value.
31    Lit(LcnfLit),
32    /// An erased argument (placeholder for proof terms).
33    Erased,
34    /// A type argument (may be erased depending on config).
35    Type(LcnfType),
36}
37/// An LCNF module — a collection of declarations.
38#[derive(Clone, Debug, Default)]
39pub struct LcnfModule {
40    /// Top-level function declarations.
41    pub fun_decls: Vec<LcnfFunDecl>,
42    /// External declarations (axioms, opaques).
43    pub extern_decls: Vec<LcnfExternDecl>,
44    /// Name of the module.
45    pub name: String,
46    /// Metadata about the conversion.
47    pub metadata: LcnfModuleMetadata,
48}
49/// Configuration for pretty-printing LCNF.
50#[derive(Clone, Debug)]
51pub struct PrettyConfig {
52    pub indent: usize,
53    pub max_width: usize,
54    pub show_types: bool,
55    pub show_erased: bool,
56}
57/// A unique variable identifier in LCNF.
58#[derive(Clone, Copy, PartialEq, Eq, Hash, Debug)]
59pub struct LcnfVarId(pub u64);
60/// Collector that finds all free variables in an LCNF expression.
61pub struct FreeVarCollector {
62    pub(super) bound: HashSet<LcnfVarId>,
63    pub(super) free: HashSet<LcnfVarId>,
64}
65impl FreeVarCollector {
66    pub(super) fn new() -> Self {
67        FreeVarCollector {
68            bound: HashSet::new(),
69            free: HashSet::new(),
70        }
71    }
72    pub(super) fn collect_from_arg(&mut self, arg: &LcnfArg) {
73        if let LcnfArg::Var(id) = arg {
74            if !self.bound.contains(id) {
75                self.free.insert(*id);
76            }
77        }
78    }
79    pub(super) fn collect_from_let_value(&mut self, val: &LcnfLetValue) {
80        match val {
81            LcnfLetValue::App(func, args) => {
82                self.collect_from_arg(func);
83                for arg in args {
84                    self.collect_from_arg(arg);
85                }
86            }
87            LcnfLetValue::Proj(_, _, var) => {
88                if !self.bound.contains(var) {
89                    self.free.insert(*var);
90                }
91            }
92            LcnfLetValue::Ctor(_, _, args) => {
93                for arg in args {
94                    self.collect_from_arg(arg);
95                }
96            }
97            LcnfLetValue::FVar(id) => {
98                if !self.bound.contains(id) {
99                    self.free.insert(*id);
100                }
101            }
102            LcnfLetValue::Lit(_)
103            | LcnfLetValue::Erased
104            | LcnfLetValue::Reset(_)
105            | LcnfLetValue::Reuse(_, _, _, _) => {}
106        }
107    }
108    pub(super) fn collect_expr(&mut self, expr: &LcnfExpr) {
109        match expr {
110            LcnfExpr::Let {
111                id, value, body, ..
112            } => {
113                self.collect_from_let_value(value);
114                self.bound.insert(*id);
115                self.collect_expr(body);
116            }
117            LcnfExpr::Case {
118                scrutinee,
119                alts,
120                default,
121                ..
122            } => {
123                if !self.bound.contains(scrutinee) {
124                    self.free.insert(*scrutinee);
125                }
126                for alt in alts {
127                    let saved = self.bound.clone();
128                    for param in &alt.params {
129                        self.bound.insert(param.id);
130                    }
131                    self.collect_expr(&alt.body);
132                    self.bound = saved;
133                }
134                if let Some(def) = default {
135                    self.collect_expr(def);
136                }
137            }
138            LcnfExpr::Return(arg) => self.collect_from_arg(arg),
139            LcnfExpr::Unreachable => {}
140            LcnfExpr::TailCall(func, args) => {
141                self.collect_from_arg(func);
142                for arg in args {
143                    self.collect_from_arg(arg);
144                }
145            }
146        }
147    }
148}
149/// LCNF type representation.
150///
151/// Types in LCNF are simplified compared to kernel types.
152/// Proof-irrelevant types and universes are erased.
153#[derive(Clone, PartialEq, Eq, Hash, Debug)]
154pub enum LcnfType {
155    /// Erased type (proof-irrelevant or computationally irrelevant).
156    Erased,
157    /// A type variable or named type.
158    Var(String),
159    /// Function type: params -> return.
160    Fun(Vec<LcnfType>, Box<LcnfType>),
161    /// Constructor/inductive type with type arguments.
162    Ctor(String, Vec<LcnfType>),
163    /// Object type (boxed/heap-allocated).
164    Object,
165    /// Natural number type.
166    Nat,
167    /// Signed integer type.
168    Int,
169    /// String type.
170    LcnfString,
171    /// Unit type (erased value placeholder).
172    Unit,
173    /// Irrelevant (computationally meaningless, e.g. proofs).
174    Irrelevant,
175}
176/// Counts how many times each variable is used (referenced).
177pub struct UsageCounter {
178    pub(super) counts: HashMap<LcnfVarId, usize>,
179}
180impl UsageCounter {
181    pub(super) fn new() -> Self {
182        UsageCounter {
183            counts: HashMap::new(),
184        }
185    }
186    pub(super) fn count_arg(&mut self, arg: &LcnfArg) {
187        if let LcnfArg::Var(id) = arg {
188            *self.counts.entry(*id).or_insert(0) += 1;
189        }
190    }
191    pub(super) fn count_let_value(&mut self, val: &LcnfLetValue) {
192        match val {
193            LcnfLetValue::App(func, args) => {
194                self.count_arg(func);
195                for arg in args {
196                    self.count_arg(arg);
197                }
198            }
199            LcnfLetValue::Proj(_, _, var) => {
200                *self.counts.entry(*var).or_insert(0) += 1;
201            }
202            LcnfLetValue::Ctor(_, _, args) => {
203                for arg in args {
204                    self.count_arg(arg);
205                }
206            }
207            LcnfLetValue::FVar(id) => {
208                *self.counts.entry(*id).or_insert(0) += 1;
209            }
210            LcnfLetValue::Lit(_)
211            | LcnfLetValue::Erased
212            | LcnfLetValue::Reset(_)
213            | LcnfLetValue::Reuse(_, _, _, _) => {}
214        }
215    }
216    pub(super) fn count_expr(&mut self, expr: &LcnfExpr) {
217        match expr {
218            LcnfExpr::Let { value, body, .. } => {
219                self.count_let_value(value);
220                self.count_expr(body);
221            }
222            LcnfExpr::Case {
223                scrutinee,
224                alts,
225                default,
226                ..
227            } => {
228                *self.counts.entry(*scrutinee).or_insert(0) += 1;
229                for alt in alts {
230                    self.count_expr(&alt.body);
231                }
232                if let Some(def) = default {
233                    self.count_expr(def);
234                }
235            }
236            LcnfExpr::Return(arg) => self.count_arg(arg),
237            LcnfExpr::Unreachable => {}
238            LcnfExpr::TailCall(func, args) => {
239                self.count_arg(func);
240                for arg in args {
241                    self.count_arg(arg);
242                }
243            }
244        }
245    }
246}
247/// A let-bound value in LCNF.
248///
249/// In ANF, every complex operation is let-bound so that
250/// arguments to subsequent operations are always atomic.
251#[derive(Clone, PartialEq, Debug)]
252pub enum LcnfLetValue {
253    /// Function application: `f(args...)`.
254    App(LcnfArg, Vec<LcnfArg>),
255    /// Projection: `proj_idx(struct_var)`.
256    Proj(String, u32, LcnfVarId),
257    /// Constructor application: `Ctor(args...)`.
258    Ctor(String, u32, Vec<LcnfArg>),
259    /// Literal value.
260    Lit(LcnfLit),
261    /// Erased value.
262    Erased,
263    /// A free variable reference (unresolved).
264    FVar(LcnfVarId),
265    /// Reset (free fields of) a unique object, returning a reusable memory slot.
266    /// Used by the reset-reuse optimization to recycle allocations.
267    Reset(LcnfVarId),
268    /// Reuse a freed slot to construct a new value.
269    /// `Reuse(slot, ctor_name, ctor_tag, args)` — like `Ctor` but using pre-allocated memory.
270    Reuse(LcnfVarId, String, u32, Vec<LcnfArg>),
271}
272/// A mapping from variable IDs to replacement arguments.
273#[derive(Clone, Debug, Default)]
274pub struct Substitution(pub HashMap<LcnfVarId, LcnfArg>);
275impl Substitution {
276    pub fn new() -> Self {
277        Substitution(HashMap::new())
278    }
279    pub fn insert(&mut self, var: LcnfVarId, arg: LcnfArg) {
280        self.0.insert(var, arg);
281    }
282    pub fn get(&self, var: &LcnfVarId) -> Option<&LcnfArg> {
283        self.0.get(var)
284    }
285    pub fn contains(&self, var: &LcnfVarId) -> bool {
286        self.0.contains_key(var)
287    }
288    pub fn compose(&self, other: &Substitution) -> Substitution {
289        let mut result = HashMap::new();
290        for (var, arg) in &self.0 {
291            result.insert(*var, substitute_arg(arg, other));
292        }
293        for (var, arg) in &other.0 {
294            result.entry(*var).or_insert_with(|| arg.clone());
295        }
296        Substitution(result)
297    }
298    pub fn is_empty(&self) -> bool {
299        self.0.is_empty()
300    }
301}
302/// A parameter declaration in LCNF.
303#[derive(Clone, PartialEq, Eq, Hash, Debug)]
304pub struct LcnfParam {
305    /// The variable ID for this parameter.
306    pub id: LcnfVarId,
307    /// The name hint for this parameter.
308    pub name: String,
309    /// The type of this parameter.
310    pub ty: LcnfType,
311    /// Whether this parameter is erased (proof-irrelevant).
312    pub erased: bool,
313    /// Whether this parameter is borrowed (no RC inc/dec needed).
314    pub borrowed: bool,
315}
316/// Records the site where a variable is defined.
317#[derive(Clone, Debug, PartialEq)]
318pub struct DefinitionSite {
319    pub var: LcnfVarId,
320    pub name: String,
321    pub ty: LcnfType,
322    pub depth: usize,
323}
324/// A case alternative (branch) in LCNF.
325#[derive(Clone, PartialEq, Debug)]
326pub struct LcnfAlt {
327    /// The constructor name for this alternative.
328    pub ctor_name: String,
329    /// The constructor tag (index in the inductive type).
330    pub ctor_tag: u32,
331    /// Parameters bound by the constructor.
332    pub params: Vec<LcnfParam>,
333    /// The body of this alternative.
334    pub body: LcnfExpr,
335}
336/// An external (axiom/opaque) declaration.
337#[derive(Clone, PartialEq, Debug)]
338pub struct LcnfExternDecl {
339    /// Name of the external declaration.
340    pub name: String,
341    /// Parameters.
342    pub params: Vec<LcnfParam>,
343    /// Return type.
344    pub ret_type: LcnfType,
345}
346/// A top-level function declaration in LCNF.
347#[derive(Clone, PartialEq, Debug)]
348pub struct LcnfFunDecl {
349    /// The fully qualified name of this function.
350    pub name: String,
351    /// The original kernel name.
352    pub original_name: Option<Name>,
353    /// Parameters of this function.
354    pub params: Vec<LcnfParam>,
355    /// Return type.
356    pub ret_type: LcnfType,
357    /// The function body in LCNF.
358    pub body: LcnfExpr,
359    /// Whether this function is recursive.
360    pub is_recursive: bool,
361    /// Whether this function was lifted from a nested lambda.
362    pub is_lifted: bool,
363    /// Inlining cost heuristic (lower = more likely to inline).
364    pub inline_cost: usize,
365}
366/// Errors that can occur when validating LCNF.
367#[derive(Clone, Debug, PartialEq)]
368pub enum ValidationError {
369    UnboundVariable(LcnfVarId),
370    DuplicateBinding(LcnfVarId),
371    EmptyCase,
372    InvalidTag(String, u32),
373    NonAtomicArgument,
374}
375/// A builder for constructing LCNF expressions incrementally.
376pub struct LcnfBuilder {
377    pub(super) next_id: u64,
378    pub(super) bindings: Vec<(LcnfVarId, String, LcnfType, LcnfLetValue)>,
379}
380impl LcnfBuilder {
381    pub fn new() -> Self {
382        LcnfBuilder {
383            next_id: 0,
384            bindings: Vec::new(),
385        }
386    }
387    pub fn with_start_id(start: u64) -> Self {
388        LcnfBuilder {
389            next_id: start,
390            bindings: Vec::new(),
391        }
392    }
393    pub fn fresh_var(&mut self, _name: &str, _ty: LcnfType) -> LcnfVarId {
394        let id = LcnfVarId(self.next_id);
395        self.next_id += 1;
396        id
397    }
398    pub fn let_bind(&mut self, name: &str, ty: LcnfType, val: LcnfLetValue) -> LcnfVarId {
399        let id = LcnfVarId(self.next_id);
400        self.next_id += 1;
401        self.bindings.push((id, name.to_string(), ty, val));
402        id
403    }
404    pub fn let_app(
405        &mut self,
406        name: &str,
407        ty: LcnfType,
408        func: LcnfArg,
409        args: Vec<LcnfArg>,
410    ) -> LcnfVarId {
411        self.let_bind(name, ty, LcnfLetValue::App(func, args))
412    }
413    pub fn let_ctor(
414        &mut self,
415        name: &str,
416        ty: LcnfType,
417        ctor: &str,
418        tag: u32,
419        args: Vec<LcnfArg>,
420    ) -> LcnfVarId {
421        self.let_bind(name, ty, LcnfLetValue::Ctor(ctor.to_string(), tag, args))
422    }
423    pub fn let_proj(
424        &mut self,
425        name: &str,
426        ty: LcnfType,
427        type_name: &str,
428        idx: u32,
429        var: LcnfVarId,
430    ) -> LcnfVarId {
431        self.let_bind(
432            name,
433            ty,
434            LcnfLetValue::Proj(type_name.to_string(), idx, var),
435        )
436    }
437    pub fn build_return(self, arg: LcnfArg) -> LcnfExpr {
438        self.wrap_bindings(LcnfExpr::Return(arg))
439    }
440    pub fn build_case(
441        self,
442        scrutinee: LcnfVarId,
443        scrutinee_ty: LcnfType,
444        alts: Vec<LcnfAlt>,
445        default: Option<LcnfExpr>,
446    ) -> LcnfExpr {
447        self.wrap_bindings(LcnfExpr::Case {
448            scrutinee,
449            scrutinee_ty,
450            alts,
451            default: default.map(Box::new),
452        })
453    }
454    pub fn build_tail_call(self, func: LcnfArg, args: Vec<LcnfArg>) -> LcnfExpr {
455        self.wrap_bindings(LcnfExpr::TailCall(func, args))
456    }
457    pub(super) fn wrap_bindings(self, terminal: LcnfExpr) -> LcnfExpr {
458        let mut result = terminal;
459        for (id, name, ty, value) in self.bindings.into_iter().rev() {
460            result = LcnfExpr::Let {
461                id,
462                name,
463                ty,
464                value,
465                body: Box::new(result),
466            };
467        }
468        result
469    }
470    pub fn peek_next_id(&self) -> u64 {
471        self.next_id
472    }
473    pub fn binding_count(&self) -> usize {
474        self.bindings.len()
475    }
476}
477/// A cost model for estimating runtime cost.
478#[derive(Clone, Debug)]
479pub struct CostModel {
480    pub let_cost: u64,
481    pub app_cost: u64,
482    pub case_cost: u64,
483    pub return_cost: u64,
484    pub branch_penalty: u64,
485}
486/// Literal values in LCNF.
487#[derive(Clone, PartialEq, Eq, Hash, Debug)]
488pub enum LcnfLit {
489    /// Natural number literal.
490    Nat(u64),
491    /// Signed integer literal.
492    Int(i64),
493    /// String literal.
494    Str(String),
495}
496/// Core LCNF expression in administrative normal form.
497#[derive(Clone, PartialEq, Debug)]
498pub enum LcnfExpr {
499    /// Let binding: `let x : ty := val; body`.
500    Let {
501        /// The variable being bound.
502        id: LcnfVarId,
503        /// Name hint.
504        name: String,
505        /// Type of the binding.
506        ty: LcnfType,
507        /// The value being bound.
508        value: LcnfLetValue,
509        /// The continuation expression.
510        body: Box<LcnfExpr>,
511    },
512    /// Case split (pattern match).
513    Case {
514        /// The scrutinee variable.
515        scrutinee: LcnfVarId,
516        /// The type of the scrutinee.
517        scrutinee_ty: LcnfType,
518        /// The alternatives.
519        alts: Vec<LcnfAlt>,
520        /// Default alternative (if not all constructors covered).
521        default: Option<Box<LcnfExpr>>,
522    },
523    /// Return a value (terminal expression).
524    Return(LcnfArg),
525    /// Unreachable code (after exhaustive match).
526    Unreachable,
527    /// Function application in tail position.
528    TailCall(LcnfArg, Vec<LcnfArg>),
529}
oxilean_codegen/lcnf/types.rs

oxilean_codegen/lcnf/
types.rs
