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    /// String type.
168    LcnfString,
169    /// Unit type (erased value placeholder).
170    Unit,
171    /// Irrelevant (computationally meaningless, e.g. proofs).
172    Irrelevant,
173}
174/// Counts how many times each variable is used (referenced).
175pub struct UsageCounter {
176    pub(super) counts: HashMap<LcnfVarId, usize>,
177}
178impl UsageCounter {
179    pub(super) fn new() -> Self {
180        UsageCounter {
181            counts: HashMap::new(),
182        }
183    }
184    pub(super) fn count_arg(&mut self, arg: &LcnfArg) {
185        if let LcnfArg::Var(id) = arg {
186            *self.counts.entry(*id).or_insert(0) += 1;
187        }
188    }
189    pub(super) fn count_let_value(&mut self, val: &LcnfLetValue) {
190        match val {
191            LcnfLetValue::App(func, args) => {
192                self.count_arg(func);
193                for arg in args {
194                    self.count_arg(arg);
195                }
196            }
197            LcnfLetValue::Proj(_, _, var) => {
198                *self.counts.entry(*var).or_insert(0) += 1;
199            }
200            LcnfLetValue::Ctor(_, _, args) => {
201                for arg in args {
202                    self.count_arg(arg);
203                }
204            }
205            LcnfLetValue::FVar(id) => {
206                *self.counts.entry(*id).or_insert(0) += 1;
207            }
208            LcnfLetValue::Lit(_)
209            | LcnfLetValue::Erased
210            | LcnfLetValue::Reset(_)
211            | LcnfLetValue::Reuse(_, _, _, _) => {}
212        }
213    }
214    pub(super) fn count_expr(&mut self, expr: &LcnfExpr) {
215        match expr {
216            LcnfExpr::Let { value, body, .. } => {
217                self.count_let_value(value);
218                self.count_expr(body);
219            }
220            LcnfExpr::Case {
221                scrutinee,
222                alts,
223                default,
224                ..
225            } => {
226                *self.counts.entry(*scrutinee).or_insert(0) += 1;
227                for alt in alts {
228                    self.count_expr(&alt.body);
229                }
230                if let Some(def) = default {
231                    self.count_expr(def);
232                }
233            }
234            LcnfExpr::Return(arg) => self.count_arg(arg),
235            LcnfExpr::Unreachable => {}
236            LcnfExpr::TailCall(func, args) => {
237                self.count_arg(func);
238                for arg in args {
239                    self.count_arg(arg);
240                }
241            }
242        }
243    }
244}
245/// A let-bound value in LCNF.
246///
247/// In ANF, every complex operation is let-bound so that
248/// arguments to subsequent operations are always atomic.
249#[derive(Clone, PartialEq, Debug)]
250pub enum LcnfLetValue {
251    /// Function application: `f(args...)`.
252    App(LcnfArg, Vec<LcnfArg>),
253    /// Projection: `proj_idx(struct_var)`.
254    Proj(String, u32, LcnfVarId),
255    /// Constructor application: `Ctor(args...)`.
256    Ctor(String, u32, Vec<LcnfArg>),
257    /// Literal value.
258    Lit(LcnfLit),
259    /// Erased value.
260    Erased,
261    /// A free variable reference (unresolved).
262    FVar(LcnfVarId),
263    /// Reset (free fields of) a unique object, returning a reusable memory slot.
264    /// Used by the reset-reuse optimization to recycle allocations.
265    Reset(LcnfVarId),
266    /// Reuse a freed slot to construct a new value.
267    /// `Reuse(slot, ctor_name, ctor_tag, args)` — like `Ctor` but using pre-allocated memory.
268    Reuse(LcnfVarId, String, u32, Vec<LcnfArg>),
269}
270/// A mapping from variable IDs to replacement arguments.
271#[derive(Clone, Debug, Default)]
272pub struct Substitution(pub HashMap<LcnfVarId, LcnfArg>);
273impl Substitution {
274    pub fn new() -> Self {
275        Substitution(HashMap::new())
276    }
277    pub fn insert(&mut self, var: LcnfVarId, arg: LcnfArg) {
278        self.0.insert(var, arg);
279    }
280    pub fn get(&self, var: &LcnfVarId) -> Option<&LcnfArg> {
281        self.0.get(var)
282    }
283    pub fn contains(&self, var: &LcnfVarId) -> bool {
284        self.0.contains_key(var)
285    }
286    pub fn compose(&self, other: &Substitution) -> Substitution {
287        let mut result = HashMap::new();
288        for (var, arg) in &self.0 {
289            result.insert(*var, substitute_arg(arg, other));
290        }
291        for (var, arg) in &other.0 {
292            result.entry(*var).or_insert_with(|| arg.clone());
293        }
294        Substitution(result)
295    }
296    pub fn is_empty(&self) -> bool {
297        self.0.is_empty()
298    }
299}
300/// A parameter declaration in LCNF.
301#[derive(Clone, PartialEq, Eq, Hash, Debug)]
302pub struct LcnfParam {
303    /// The variable ID for this parameter.
304    pub id: LcnfVarId,
305    /// The name hint for this parameter.
306    pub name: String,
307    /// The type of this parameter.
308    pub ty: LcnfType,
309    /// Whether this parameter is erased (proof-irrelevant).
310    pub erased: bool,
311    /// Whether this parameter is borrowed (no RC inc/dec needed).
312    pub borrowed: bool,
313}
314/// Records the site where a variable is defined.
315#[derive(Clone, Debug, PartialEq)]
316pub struct DefinitionSite {
317    pub var: LcnfVarId,
318    pub name: String,
319    pub ty: LcnfType,
320    pub depth: usize,
321}
322/// A case alternative (branch) in LCNF.
323#[derive(Clone, PartialEq, Debug)]
324pub struct LcnfAlt {
325    /// The constructor name for this alternative.
326    pub ctor_name: String,
327    /// The constructor tag (index in the inductive type).
328    pub ctor_tag: u32,
329    /// Parameters bound by the constructor.
330    pub params: Vec<LcnfParam>,
331    /// The body of this alternative.
332    pub body: LcnfExpr,
333}
334/// An external (axiom/opaque) declaration.
335#[derive(Clone, PartialEq, Debug)]
336pub struct LcnfExternDecl {
337    /// Name of the external declaration.
338    pub name: String,
339    /// Parameters.
340    pub params: Vec<LcnfParam>,
341    /// Return type.
342    pub ret_type: LcnfType,
343}
344/// A top-level function declaration in LCNF.
345#[derive(Clone, PartialEq, Debug)]
346pub struct LcnfFunDecl {
347    /// The fully qualified name of this function.
348    pub name: String,
349    /// The original kernel name.
350    pub original_name: Option<Name>,
351    /// Parameters of this function.
352    pub params: Vec<LcnfParam>,
353    /// Return type.
354    pub ret_type: LcnfType,
355    /// The function body in LCNF.
356    pub body: LcnfExpr,
357    /// Whether this function is recursive.
358    pub is_recursive: bool,
359    /// Whether this function was lifted from a nested lambda.
360    pub is_lifted: bool,
361    /// Inlining cost heuristic (lower = more likely to inline).
362    pub inline_cost: usize,
363}
364/// Errors that can occur when validating LCNF.
365#[derive(Clone, Debug, PartialEq)]
366pub enum ValidationError {
367    UnboundVariable(LcnfVarId),
368    DuplicateBinding(LcnfVarId),
369    EmptyCase,
370    InvalidTag(String, u32),
371    NonAtomicArgument,
372}
373/// A builder for constructing LCNF expressions incrementally.
374pub struct LcnfBuilder {
375    pub(super) next_id: u64,
376    pub(super) bindings: Vec<(LcnfVarId, String, LcnfType, LcnfLetValue)>,
377}
378impl LcnfBuilder {
379    pub fn new() -> Self {
380        LcnfBuilder {
381            next_id: 0,
382            bindings: Vec::new(),
383        }
384    }
385    pub fn with_start_id(start: u64) -> Self {
386        LcnfBuilder {
387            next_id: start,
388            bindings: Vec::new(),
389        }
390    }
391    pub fn fresh_var(&mut self, _name: &str, _ty: LcnfType) -> LcnfVarId {
392        let id = LcnfVarId(self.next_id);
393        self.next_id += 1;
394        id
395    }
396    pub fn let_bind(&mut self, name: &str, ty: LcnfType, val: LcnfLetValue) -> LcnfVarId {
397        let id = LcnfVarId(self.next_id);
398        self.next_id += 1;
399        self.bindings.push((id, name.to_string(), ty, val));
400        id
401    }
402    pub fn let_app(
403        &mut self,
404        name: &str,
405        ty: LcnfType,
406        func: LcnfArg,
407        args: Vec<LcnfArg>,
408    ) -> LcnfVarId {
409        self.let_bind(name, ty, LcnfLetValue::App(func, args))
410    }
411    pub fn let_ctor(
412        &mut self,
413        name: &str,
414        ty: LcnfType,
415        ctor: &str,
416        tag: u32,
417        args: Vec<LcnfArg>,
418    ) -> LcnfVarId {
419        self.let_bind(name, ty, LcnfLetValue::Ctor(ctor.to_string(), tag, args))
420    }
421    pub fn let_proj(
422        &mut self,
423        name: &str,
424        ty: LcnfType,
425        type_name: &str,
426        idx: u32,
427        var: LcnfVarId,
428    ) -> LcnfVarId {
429        self.let_bind(
430            name,
431            ty,
432            LcnfLetValue::Proj(type_name.to_string(), idx, var),
433        )
434    }
435    pub fn build_return(self, arg: LcnfArg) -> LcnfExpr {
436        self.wrap_bindings(LcnfExpr::Return(arg))
437    }
438    pub fn build_case(
439        self,
440        scrutinee: LcnfVarId,
441        scrutinee_ty: LcnfType,
442        alts: Vec<LcnfAlt>,
443        default: Option<LcnfExpr>,
444    ) -> LcnfExpr {
445        self.wrap_bindings(LcnfExpr::Case {
446            scrutinee,
447            scrutinee_ty,
448            alts,
449            default: default.map(Box::new),
450        })
451    }
452    pub fn build_tail_call(self, func: LcnfArg, args: Vec<LcnfArg>) -> LcnfExpr {
453        self.wrap_bindings(LcnfExpr::TailCall(func, args))
454    }
455    pub(super) fn wrap_bindings(self, terminal: LcnfExpr) -> LcnfExpr {
456        let mut result = terminal;
457        for (id, name, ty, value) in self.bindings.into_iter().rev() {
458            result = LcnfExpr::Let {
459                id,
460                name,
461                ty,
462                value,
463                body: Box::new(result),
464            };
465        }
466        result
467    }
468    pub fn peek_next_id(&self) -> u64 {
469        self.next_id
470    }
471    pub fn binding_count(&self) -> usize {
472        self.bindings.len()
473    }
474}
475/// A cost model for estimating runtime cost.
476#[derive(Clone, Debug)]
477pub struct CostModel {
478    pub let_cost: u64,
479    pub app_cost: u64,
480    pub case_cost: u64,
481    pub return_cost: u64,
482    pub branch_penalty: u64,
483}
484/// Literal values in LCNF.
485#[derive(Clone, PartialEq, Eq, Hash, Debug)]
486pub enum LcnfLit {
487    /// Natural number literal.
488    Nat(u64),
489    /// String literal.
490    Str(String),
491}
492/// Core LCNF expression in administrative normal form.
493#[derive(Clone, PartialEq, Debug)]
494pub enum LcnfExpr {
495    /// Let binding: `let x : ty := val; body`.
496    Let {
497        /// The variable being bound.
498        id: LcnfVarId,
499        /// Name hint.
500        name: String,
501        /// Type of the binding.
502        ty: LcnfType,
503        /// The value being bound.
504        value: LcnfLetValue,
505        /// The continuation expression.
506        body: Box<LcnfExpr>,
507    },
508    /// Case split (pattern match).
509    Case {
510        /// The scrutinee variable.
511        scrutinee: LcnfVarId,
512        /// The type of the scrutinee.
513        scrutinee_ty: LcnfType,
514        /// The alternatives.
515        alts: Vec<LcnfAlt>,
516        /// Default alternative (if not all constructors covered).
517        default: Option<Box<LcnfExpr>>,
518    },
519    /// Return a value (terminal expression).
520    Return(LcnfArg),
521    /// Unreachable code (after exhaustive match).
522    Unreachable,
523    /// Function application in tail position.
524    TailCall(LcnfArg, Vec<LcnfArg>),
525}
oxilean_codegen/lcnf/types.rs

oxilean_codegen/lcnf/
types.rs
