From ba837eadbd0eb238e31f62a35dbabf7e94784d39 Mon Sep 17 00:00:00 2001 From: LukasK Date: Mon, 6 Apr 2026 08:04:16 +0000 Subject: [PATCH 1/6] feat: add names arena and thread 'names lifetime through IR Introduces a dedicated `names_arena: Bump` that owns all identifier strings for the lifetime of the pipeline. Only `lexer::Lexer` calls `alloc_str`; every downstream layer (parser, checker, staging) reuses the existing `&Name` references without re-allocating. To express this, AST and core IR types gain a separate `'n` lifetime parameter for name references, distinct from the structural allocation lifetime `'a`. The elaboration bound changes from `'src: 'core` to `'n: 'core`, which lets `ast_arena` be dropped before `core_arena` in the pipeline, as intended. Closes #28 Co-Authored-By: Claude Sonnet 4.6 --- cli/src/main.rs | 17 +-- compiler/src/checker/ctx.rs | 43 +++++--- compiler/src/checker/elaborate.rs | 47 ++++---- compiler/src/checker/infer.rs | 127 +++++++++++----------- compiler/src/checker/mod.rs | 2 +- compiler/src/checker/test/helpers.rs | 14 +-- compiler/src/checker/test/mod.rs | 2 +- compiler/src/core/alpha_eq.rs | 2 +- compiler/src/core/mod.rs | 86 +++++++-------- compiler/src/core/pretty.rs | 16 +-- compiler/src/core/value.rs | 92 ++++++++++------ compiler/src/lexer/mod.rs | 7 +- compiler/src/lexer/test/fuzz.rs | 8 +- compiler/src/parser/ast.rs | 56 +++++----- compiler/src/parser/mod.rs | 74 +++++++------ compiler/src/parser/test/mod.rs | 14 +-- compiler/src/staging/mod.rs | 157 +++++++++++++-------------- compiler/tests/snap.rs | 2 +- 18 files changed, 402 insertions(+), 364 deletions(-) diff --git a/cli/src/main.rs b/cli/src/main.rs index 6e4d324..75ba50d 100644 --- a/cli/src/main.rs +++ b/cli/src/main.rs @@ -35,11 +35,14 @@ fn stage(file: &PathBuf) -> Result<()> { let source = std::fs::read_to_string(file) .with_context(|| format!("failed to read file: {}", file.display()))?; + // Names arena: owns all identifier strings for the lifetime of the pipeline. + let names_arena = bumpalo::Bump::new(); + // Parse into src_arena; the arena lives until elaboration finishes // consuming the AST, then is dropped. - let src_arena = bumpalo::Bump::new(); - let lexer = lexer::Lexer::new(&source); - let mut parser = parser::Parser::new(lexer, &src_arena); + let ast_arena = bumpalo::Bump::new(); + let lexer = lexer::Lexer::new(&source, &names_arena); + let mut parser = parser::Parser::new(lexer, &ast_arena); let program = parser.parse_program().context("failed to parse program")?; // Elaborate/typecheck into core_arena; the arena lives until staging @@ -47,12 +50,12 @@ fn stage(file: &PathBuf) -> Result<()> { let core_arena = bumpalo::Bump::new(); let core_program = checker::elaborate_program(&core_arena, &program).context("failed to elaborate program")?; - drop(src_arena); + drop(ast_arena); // Unstage into out_arena; core_arena is no longer needed after this. - let out_arena = bumpalo::Bump::new(); - let staged = - staging::unstage_program(&out_arena, &core_program).context("failed to stage program")?; + let staged_arena = bumpalo::Bump::new(); + let staged = staging::unstage_program(&staged_arena, &core_program) + .context("failed to stage program")?; drop(core_arena); // Print the staged result, then out_arena is dropped at end of scope. diff --git a/compiler/src/checker/ctx.rs b/compiler/src/checker/ctx.rs index 760e2d0..eb91ec1 100644 --- a/compiler/src/checker/ctx.rs +++ b/compiler/src/checker/ctx.rs @@ -12,31 +12,31 @@ use crate::core::{self, value}; /// Phase is not stored here — it is threaded as an argument to `infer`/`check` /// since it shifts locally when entering `Quote`, `Splice`, or `Lift`. #[derive(Debug)] -pub struct Ctx<'core, 'globals> { +pub struct Ctx<'names, 'core, 'globals> { /// Arena for allocating core terms pub arena: &'core bumpalo::Bump, /// Local variable names (oldest first), for error messages. - pub names: Vec<&'core core::Name>, + pub names: Vec<&'names core::Name>, /// Evaluation environment (oldest first): values of locals. /// `env[env.len() - 1 - ix]` = value of `Var(Ix(ix))`. - pub env: value::Env<'core>, + pub env: value::Env<'names, 'core>, /// Types of locals as semantic values (oldest first). /// `types[types.len() - 1 - ix]` = type of `Var(Ix(ix))`. - pub types: Vec>, + pub types: Vec>, /// Global function types: name -> Pi term. /// Storing `&Term` (always a Pi) unifies type lookup for globals and locals. /// Borrowed independently of the arena so the map can live on the stack. - pub globals: &'globals HashMap<&'core core::Name, &'core core::Pi<'core>>, + pub globals: &'globals HashMap<&'names core::Name, &'core core::Pi<'names, 'core>>, } -impl<'core, 'globals> Ctx<'core, 'globals> { +impl<'names, 'core, 'globals> Ctx<'names, 'core, 'globals> { pub const fn new( arena: &'core bumpalo::Bump, - globals: &'globals HashMap<&'core core::Name, &'core core::Pi<'core>>, + globals: &'globals HashMap<&'names core::Name, &'core core::Pi<'names, 'core>>, ) -> Self { Ctx { arena, @@ -48,7 +48,7 @@ impl<'core, 'globals> Ctx<'core, 'globals> { } /// Allocate a term in the core arena - pub fn alloc(&self, term: core::Term<'core>) -> &'core core::Term<'core> { + pub fn alloc(&self, term: core::Term<'names, 'core>) -> &'core core::Term<'names, 'core> { self.arena.alloc(term) } @@ -67,14 +67,18 @@ impl<'core, 'globals> Ctx<'core, 'globals> { /// Push a local variable onto the context, given its type as a term. /// Evaluates the type term in the current environment. - pub fn push_local(&mut self, name: &'core core::Name, ty: &'core core::Term<'core>) { + pub fn push_local(&mut self, name: &'names core::Name, ty: &'core core::Term<'names, 'core>) { let ty_val = value::eval(self.arena, &self.env, ty); self.push_local_val(name, ty_val); } /// Push a local variable onto the context, given its type as a Value. /// The variable itself is a fresh rigid (neutral) variable — use for lambda/pi params. - pub fn push_local_val(&mut self, name: &'core core::Name, ty_val: value::Value<'core>) { + pub fn push_local_val( + &mut self, + name: &'names core::Name, + ty_val: value::Value<'names, 'core>, + ) { self.env.push(value::Value::Rigid(self.depth().as_lvl())); self.types.push(ty_val); self.names.push(name); @@ -84,9 +88,9 @@ impl<'core, 'globals> Ctx<'core, 'globals> { /// Use for `let x = e` bindings so that dependent references to `x` evaluate correctly. pub fn push_let_binding( &mut self, - name: &'core core::Name, - ty_val: value::Value<'core>, - expr_val: value::Value<'core>, + name: &'names core::Name, + ty_val: value::Value<'names, 'core>, + expr_val: value::Value<'names, 'core>, ) { self.env.push(expr_val); self.types.push(ty_val); @@ -104,8 +108,8 @@ impl<'core, 'globals> Ctx<'core, 'globals> { /// Searches from the most recently pushed variable inward to handle shadowing. pub fn lookup_local( &self, - name: &'_ core::Name, - ) -> Option<(de_bruijn::Ix, &value::Value<'core>)> { + name: &core::Name, + ) -> Option<(de_bruijn::Ix, &value::Value<'names, 'core>)> { for (i, local_name) in self.names.iter().enumerate().rev() { if *local_name == name { let ix = de_bruijn::Lvl::new(i).ix_at(self.depth()); @@ -120,17 +124,20 @@ impl<'core, 'globals> Ctx<'core, 'globals> { } /// Helper to create a lifted type [[T]] - pub fn lift_ty(&self, inner: &'core core::Term<'core>) -> &'core core::Term<'core> { + pub fn lift_ty( + &self, + inner: &'core core::Term<'names, 'core>, + ) -> &'core core::Term<'names, 'core> { self.arena.alloc(core::Term::Lift(inner)) } /// Evaluate a term in the current environment. - pub fn eval(&self, term: &'core core::Term<'core>) -> value::Value<'core> { + pub fn eval(&self, term: &'core core::Term<'names, 'core>) -> value::Value<'names, 'core> { value::eval(self.arena, &self.env, term) } /// Quote a value back to a term at the current depth. - pub fn quote_val(&self, val: &value::Value<'core>) -> &'core core::Term<'core> { + pub fn quote_val(&self, val: &value::Value<'names, 'core>) -> &'core core::Term<'names, 'core> { value::quote(self.arena, self.depth(), val) } } diff --git a/compiler/src/checker/elaborate.rs b/compiler/src/checker/elaborate.rs index 66dfd54..1edf7bd 100644 --- a/compiler/src/checker/elaborate.rs +++ b/compiler/src/checker/elaborate.rs @@ -9,19 +9,18 @@ use super::Ctx; use super::infer; /// Elaborate one function's signature into a `Pi` (the globals table entry). -fn elaborate_sig<'src, 'core>( - arena: &'core bumpalo::Bump, - func: &ast::Function<'src>, -) -> Result<&'core core::Pi<'core>> { - let empty_globals = HashMap::new(); +fn elaborate_sig<'n, 'a, 'c>( + arena: &'c bumpalo::Bump, + func: &ast::Function<'n, 'a>, +) -> Result<&'c core::Pi<'n, 'c>> { + let empty_globals: HashMap<&'n core::Name, &'c core::Pi<'n, 'c>> = HashMap::new(); let mut ctx = Ctx::new(arena, &empty_globals); - let params: &'core [(&'core core::Name, &'core core::Term<'core>)] = arena - .alloc_slice_try_fill_iter(func.params.iter().map(|p| -> Result<_> { - let param_name = core::Name::new(arena.alloc_str(p.name.as_str())); + let params: &'c [(&'n core::Name, &'c core::Term<'n, 'c>)] = + arena.alloc_slice_try_fill_iter(func.params.iter().map(|p| -> Result<_> { let (param_ty, _) = infer::infer(&mut ctx, func.phase, p.ty)?; - ctx.push_local(param_name, param_ty); - Ok((param_name, param_ty)) + ctx.push_local(p.name, param_ty); + Ok((p.name, param_ty)) }))?; let body_ty = infer::check( @@ -39,14 +38,14 @@ fn elaborate_sig<'src, 'core>( } /// Pass 1: collect all top-level function signatures into a globals table. -pub fn collect_signatures<'src, 'core>( +pub fn collect_signatures<'n, 'a, 'core>( arena: &'core bumpalo::Bump, - program: &ast::Program<'src>, -) -> Result>> { - let mut globals: HashMap<&'core core::Name, &'core core::Pi<'core>> = HashMap::new(); + program: &ast::Program<'n, 'a>, +) -> Result>> { + let mut globals: HashMap<&'n core::Name, &'core core::Pi<'n, 'core>> = HashMap::new(); for func in program.functions { - let name = core::Name::new(arena.alloc_str(func.name.as_str())); + let name = func.name; ensure!( !globals.contains_key(&name), @@ -62,14 +61,14 @@ pub fn collect_signatures<'src, 'core>( } /// Pass 2: elaborate all function bodies with the full globals table available. -fn elaborate_bodies<'src, 'core>( +fn elaborate_bodies<'n, 'a, 'core>( arena: &'core bumpalo::Bump, - program: &ast::Program<'src>, - globals: &HashMap<&'core core::Name, &'core core::Pi<'core>>, -) -> Result> { - let functions: &'core [core::Function<'core>] = + program: &ast::Program<'n, 'a>, + globals: &HashMap<&'n core::Name, &'core core::Pi<'n, 'core>>, +) -> Result> { + let functions: &'core [core::Function<'n, 'core>] = arena.alloc_slice_try_fill_iter(program.functions.iter().map(|func| -> Result<_> { - let name = core::Name::new(arena.alloc_str(func.name.as_str())); + let name = func.name; let pi = *globals.get(&name).expect("signature missing from pass 1"); // Build a fresh context borrowing the stack-owned globals map. @@ -93,10 +92,10 @@ fn elaborate_bodies<'src, 'core>( } /// Elaborate the entire program in two passes -pub fn elaborate_program<'core>( +pub fn elaborate_program<'n, 'core>( arena: &'core bumpalo::Bump, - program: &ast::Program<'_>, -) -> Result> { + program: &ast::Program<'n, '_>, +) -> Result> { let globals = collect_signatures(arena, program)?; elaborate_bodies(arena, program, &globals) } diff --git a/compiler/src/checker/infer.rs b/compiler/src/checker/infer.rs index f5ad85f..390d641 100644 --- a/compiler/src/checker/infer.rs +++ b/compiler/src/checker/infer.rs @@ -1,10 +1,10 @@ -use anyhow::{Context as _, Result, anyhow, bail, ensure}; +use anyhow::{anyhow, bail, ensure, Context as _, Result}; use crate::common::de_bruijn; -use crate::core::{self, IntType, IntWidth, Lam, Phase, Pi, Prim, value}; +use crate::core::{self, value, IntType, IntWidth, Lam, Phase, Pi, Prim}; use crate::parser::ast; -use super::{Ctx, builtin_prim_ty}; +use super::{builtin_prim_ty, Ctx}; /// Infer the type of a surface term, returning both the elaborated core term /// and its type as a semantic value. @@ -12,11 +12,11 @@ use super::{Ctx, builtin_prim_ty}; clippy::too_many_lines, reason = "large match over all surface term variants" )] -pub fn infer<'src, 'core>( - ctx: &mut Ctx<'core, '_>, +pub fn infer<'names, 'a, 'core>( + ctx: &mut Ctx<'names, 'core, '_>, phase: Phase, - term: &'src ast::Term<'src>, -) -> Result<(&'core core::Term<'core>, value::Value<'core>)> { + term: &'a ast::Term<'names, 'a>, +) -> Result<(&'core core::Term<'names, 'core>, value::Value<'names, 'core>)> { match term { // ------------------------------------------------------------------ Var ast::Term::Var(name) => { @@ -44,7 +44,6 @@ pub fn infer<'src, 'core>( } // Globals — bare reference without call if let Some(pi) = ctx.globals.get(name).copied() { - let name = core::Name::new(ctx.arena.alloc_str(name.as_str())); let ty = value::eval_pi(ctx.arena, &[], pi); return Ok((ctx.alloc(core::Term::Global(name)), ty)); } @@ -90,8 +89,8 @@ pub fn infer<'src, 'core>( ); // Check each arg against its domain (evaluated with prior arg values). - let mut arg_vals: Vec> = Vec::with_capacity(args.len()); - let mut core_args: Vec<&'core core::Term<'core>> = Vec::with_capacity(args.len()); + let mut arg_vals: Vec> = Vec::with_capacity(args.len()); + let mut core_args: Vec<&'core core::Term<'names, 'core>> = Vec::with_capacity(args.len()); for (i, (arg, (_, domain_cl))) in args.iter().zip(vpi.params.iter()).enumerate() { let domain_val = value::inst_n(ctx.arena, domain_cl, &arg_vals); let core_arg = check_val(ctx, phase, arg, domain_val) @@ -178,10 +177,10 @@ pub fn infer<'src, 'core>( ); let depth_before = ctx.depth(); - let mut elaborated_params: Vec<(&'core core::Name, &'core core::Term<'core>)> = + let mut elaborated_params: Vec<(&'names core::Name, &'core core::Term<'names, 'core>)> = Vec::new(); for p in *params { - let param_name = core::Name::new(ctx.arena.alloc_str(p.name.as_str())); + let param_name = p.name; let param_ty = check_universe(ctx, Phase::Meta, p.ty)?; elaborated_params.push((param_name, param_ty)); ctx.push_local(param_name, param_ty); @@ -212,11 +211,11 @@ pub fn infer<'src, 'core>( ); let depth_before = ctx.depth(); - let mut elaborated_params: Vec<(&'core core::Name, &'core core::Term<'core>)> = + let mut elaborated_params: Vec<(&'names core::Name, &'core core::Term<'names, 'core>)> = Vec::new(); for p in *params { - let param_name = core::Name::new(ctx.arena.alloc_str(p.name.as_str())); + let param_name = p.name; let (param_ty, _) = infer(ctx, Phase::Meta, p.ty)?; elaborated_params.push((param_name, param_ty)); ctx.push_local(param_name, param_ty); @@ -325,7 +324,10 @@ pub fn infer<'src, 'core>( } /// Check exhaustiveness of `arms` given the scrutinee type `scrut_ty`. -fn check_exhaustiveness(scrut_ty: &value::Value<'_>, arms: &[ast::MatchArm<'_>]) -> Result<()> { +fn check_exhaustiveness( + scrut_ty: &value::Value<'_, '_>, + arms: &[ast::MatchArm<'_, '_>], +) -> Result<()> { let mut covered_lits: Option> = match scrut_ty { value::Value::Prim(Prim::IntTy(ty)) => match ty.width { IntWidth::U0 => Some(vec![false; 1]), @@ -362,32 +364,29 @@ fn check_exhaustiveness(scrut_ty: &value::Value<'_>, arms: &[ast::MatchArm<'_>]) } /// Elaborate a match pattern into a core pattern. -fn elaborate_pat<'core>(ctx: &Ctx<'core, '_>, pat: &ast::Pat<'_>) -> core::Pat<'core> { +fn elaborate_pat<'n>(pat: &ast::Pat<'n>) -> core::Pat<'n> { match pat { ast::Pat::Lit(n) => core::Pat::Lit(*n), ast::Pat::Name(name) => match name.as_str() { "_" => core::Pat::Wildcard, - s => { - let bound = core::Name::new(ctx.arena.alloc_str(s)); - core::Pat::Bind(bound) - } + _ => core::Pat::Bind(name), }, } } /// Elaborate a single `let` binding. -fn elaborate_let<'src, 'core, T, F, G, W>( - ctx: &mut Ctx<'core, '_>, +fn elaborate_let<'n, 'a, 'core, T, F, G, W>( + ctx: &mut Ctx<'n, 'core, '_>, phase: Phase, - stmt: &'src ast::Let<'src>, + stmt: &'a ast::Let<'n, 'a>, cont: F, body_of: G, wrap: W, ) -> Result where - F: FnOnce(&mut Ctx<'core, '_>) -> Result, - G: FnOnce(&T) -> &'core core::Term<'core>, - W: FnOnce(&'core core::Term<'core>, T) -> T, + F: FnOnce(&mut Ctx<'n, 'core, '_>) -> Result, + G: FnOnce(&T) -> &'core core::Term<'n, 'core>, + W: FnOnce(&'core core::Term<'n, 'core>, T) -> T, { let (core_expr, bind_ty_val) = if let Some(ann) = stmt.ty { let (ty, _) = infer(ctx, phase, ann)?; @@ -404,7 +403,7 @@ where let bind_ty_term = ctx.quote_val(&bind_ty_val); // Evaluate the bound expression so dependent references to this binding work correctly. let expr_val = ctx.eval(core_expr); - let bind_name = core::Name::new(ctx.arena.alloc_str(stmt.name.as_str())); + let bind_name = stmt.name; ctx.push_let_binding(bind_name, bind_ty_val, expr_val); let cont_result = cont(ctx); ctx.pop_local(); @@ -421,12 +420,12 @@ where } /// Elaborate a sequence of `let` bindings followed by a trailing expression (infer mode). -fn infer_block<'src, 'core>( - ctx: &mut Ctx<'core, '_>, +fn infer_block<'n, 'a, 'core>( + ctx: &mut Ctx<'n, 'core, '_>, phase: Phase, - stmts: &'src [ast::Let<'src>], - expr: &'src ast::Term<'src>, -) -> Result<(&'core core::Term<'core>, value::Value<'core>)> { + stmts: &'a [ast::Let<'n, 'a>], + expr: &'a ast::Term<'n, 'a>, +) -> Result<(&'core core::Term<'n, 'core>, value::Value<'n, 'core>)> { match stmts { [] => infer(ctx, phase, expr), [first, rest @ ..] => elaborate_let( @@ -441,14 +440,14 @@ fn infer_block<'src, 'core>( } /// Elaborate a sequence of `let` bindings followed by a trailing expression (check mode). -fn check_block_val<'src, 'core>( - ctx: &mut Ctx<'core, '_>, +fn check_block_val<'n, 'a, 'core>( + ctx: &mut Ctx<'n, 'core, '_>, phase: Phase, - stmts: &'src [ast::Let<'src>], - expr: &'src ast::Term<'src>, - expected: value::Value<'core>, - expected_term: Option<&'core core::Term<'core>>, -) -> Result<&'core core::Term<'core>> { + stmts: &'a [ast::Let<'n, 'a>], + expr: &'a ast::Term<'n, 'a>, + expected: value::Value<'n, 'core>, + expected_term: Option<&'core core::Term<'n, 'core>>, +) -> Result<&'core core::Term<'n, 'core>> { match stmts { [] => check_val_impl(ctx, phase, expr, expected, expected_term), [first, rest @ ..] => elaborate_let( @@ -466,11 +465,11 @@ fn check_block_val<'src, 'core>( /// /// Equivalent to `check(ctx, phase, term, Type)` for meta phase or /// `check(ctx, phase, term, VmType)` for object phase. -fn check_universe<'src, 'core>( - ctx: &mut Ctx<'core, '_>, +fn check_universe<'n, 'a, 'core>( + ctx: &mut Ctx<'n, 'core, '_>, phase: Phase, - term: &'src ast::Term<'src>, -) -> Result<&'core core::Term<'core>> { + term: &'a ast::Term<'n, 'a>, +) -> Result<&'core core::Term<'n, 'core>> { let universe: &core::Term = match phase { Phase::Meta => &core::Term::TYPE, Phase::Object => &core::Term::VM_TYPE, @@ -482,23 +481,23 @@ fn check_universe<'src, 'core>( /// /// This is a convenience wrapper for callers that have an expected type as a `&Term`. /// It also threads the expected term through for dependent-type arm refinement. -pub fn check<'src, 'core>( - ctx: &mut Ctx<'core, '_>, +pub fn check<'n, 'a, 'core>( + ctx: &mut Ctx<'n, 'core, '_>, phase: Phase, - term: &'src ast::Term<'src>, - expected: &'core core::Term<'core>, -) -> Result<&'core core::Term<'core>> { + term: &'a ast::Term<'n, 'a>, + expected: &'core core::Term<'n, 'core>, +) -> Result<&'core core::Term<'n, 'core>> { let expected_val = ctx.eval(expected); check_val_impl(ctx, phase, term, expected_val, Some(expected)) } /// Check `term` against `expected` (as a semantic Value), returning the elaborated core term. -pub fn check_val<'src, 'core>( - ctx: &mut Ctx<'core, '_>, +pub fn check_val<'n, 'a, 'core>( + ctx: &mut Ctx<'n, 'core, '_>, phase: Phase, - term: &'src ast::Term<'src>, - expected: value::Value<'core>, -) -> Result<&'core core::Term<'core>> { + term: &'a ast::Term<'n, 'a>, + expected: value::Value<'n, 'core>, +) -> Result<&'core core::Term<'n, 'core>> { check_val_impl(ctx, phase, term, expected, None) } @@ -508,13 +507,13 @@ pub fn check_val<'src, 'core>( clippy::too_many_lines, reason = "large match over all surface term variants" )] -fn check_val_impl<'src, 'core>( - ctx: &mut Ctx<'core, '_>, +fn check_val_impl<'n, 'a, 'core>( + ctx: &mut Ctx<'n, 'core, '_>, phase: Phase, - term: &'src ast::Term<'src>, - expected: value::Value<'core>, - expected_term: Option<&'core core::Term<'core>>, -) -> Result<&'core core::Term<'core>> { + term: &'a ast::Term<'n, 'a>, + expected: value::Value<'n, 'core>, + expected_term: Option<&'core core::Term<'n, 'core>>, +) -> Result<&'core core::Term<'n, 'core>> { match term { // ------------------------------------------------------------------ Lit ast::Term::Lit(n) => match &expected { @@ -666,12 +665,12 @@ fn check_val_impl<'src, 'core>( vpi.params.len() ); - let mut elaborated_params: Vec<(&'core core::Name, &'core core::Term<'core>)> = + let mut elaborated_params: Vec<(&'n core::Name, &'core core::Term<'n, 'core>)> = Vec::new(); - let mut arg_vals: Vec> = Vec::new(); + let mut arg_vals: Vec> = Vec::new(); for (p, (_, domain_cl)) in params.iter().zip(vpi.params.iter()) { - let param_name = core::Name::new(ctx.arena.alloc_str(p.name.as_str())); + let param_name = p.name; let (annotated_ty, _) = infer(ctx, Phase::Meta, p.ty)?; let annotated_ty_val = ctx.eval(annotated_ty); let expected_domain = value::inst_n(ctx.arena, domain_cl, &arg_vals); @@ -720,10 +719,10 @@ fn check_val_impl<'src, 'core>( _ => None, }; - let core_arms: &'core [core::Arm<'core>] = + let core_arms: &'core [core::Arm<'n, 'core>] = ctx.arena .alloc_slice_try_fill_iter(arms.iter().map(|arm| -> Result<_> { - let core_pat = elaborate_pat(ctx, &arm.pat); + let core_pat = elaborate_pat(&arm.pat); let arm_expected = match (&scrut_refine, &core_pat, expected_term) { (Some((lvl, int_ty)), core::Pat::Lit(n), Some(ety)) => { diff --git a/compiler/src/checker/mod.rs b/compiler/src/checker/mod.rs index 6741adf..2f556d3 100644 --- a/compiler/src/checker/mod.rs +++ b/compiler/src/checker/mod.rs @@ -14,7 +14,7 @@ mod infer; pub(crate) fn builtin_prim_ty( name: &'_ core::Name, phase: Phase, -) -> Option<&'static core::Term<'static>> { +) -> Option<&'static core::Term<'static, 'static>> { Some(match name.as_str() { "u0" => core::Term::int_ty(IntWidth::U0, phase), "u1" => core::Term::int_ty(IntWidth::U1, phase), diff --git a/compiler/src/checker/test/helpers.rs b/compiler/src/checker/test/helpers.rs index 893eda7..cf35500 100644 --- a/compiler/src/checker/test/helpers.rs +++ b/compiler/src/checker/test/helpers.rs @@ -3,8 +3,8 @@ use super::*; /// Helper to create a test context with empty globals -pub fn test_ctx(arena: &bumpalo::Bump) -> Ctx<'_, '_> { - static EMPTY: std::sync::OnceLock>> = +pub fn test_ctx(arena: &bumpalo::Bump) -> Ctx<'_, '_, '_> { + static EMPTY: std::sync::OnceLock>> = std::sync::OnceLock::new(); let globals = EMPTY.get_or_init(HashMap::new); Ctx::new(arena, globals) @@ -13,15 +13,15 @@ pub fn test_ctx(arena: &bumpalo::Bump) -> Ctx<'_, '_> { /// Helper to create a test context with a given globals table. /// /// The caller must ensure `globals` outlives the returned `Ctx`. -pub fn test_ctx_with_globals<'core, 'globals>( +pub fn test_ctx_with_globals<'names, 'core, 'globals>( arena: &'core bumpalo::Bump, - globals: &'globals HashMap<&'core Name, &'core core::Pi<'core>>, -) -> Ctx<'core, 'globals> { + globals: &'globals HashMap<&'names Name, &'core core::Pi<'names, 'core>>, +) -> Ctx<'names, 'core, 'globals> { Ctx::new(arena, globals) } /// Helper: build a Pi for a function `fn f() -> u64` (no params, meta phase). -pub fn sig_no_params_returns_u64(arena: &bumpalo::Bump) -> &core::Pi<'_> { +pub fn sig_no_params_returns_u64(arena: &bumpalo::Bump) -> &core::Pi<'_, '_> { arena.alloc(Pi { params: &[], body_ty: &core::Term::U64_META, @@ -30,7 +30,7 @@ pub fn sig_no_params_returns_u64(arena: &bumpalo::Bump) -> &core::Pi<'_> { } /// Helper: build a Pi for `fn f(x: u32) -> u64`. -pub fn sig_one_param_returns_u64(arena: &bumpalo::Bump) -> &core::Pi<'_> { +pub fn sig_one_param_returns_u64(arena: &bumpalo::Bump) -> &core::Pi<'_, '_> { let params = arena.alloc_slice_fill_iter([(core::Name::new("x"), &core::Term::U32_META as &core::Term)]); arena.alloc(Pi { diff --git a/compiler/src/checker/test/mod.rs b/compiler/src/checker/test/mod.rs index 20bc908..576b158 100644 --- a/compiler/src/checker/test/mod.rs +++ b/compiler/src/checker/test/mod.rs @@ -11,7 +11,7 @@ use std::collections::HashMap; use super::*; use crate::common::de_bruijn; -use crate::core::{self, IntType, IntWidth, Name, Pat, Pi, Prim, value}; +use crate::core::{self, value, IntType, IntWidth, Name, Pat, Pi, Prim}; use crate::parser::ast::{self, BinOp, FunName, MatchArm, Phase}; mod helpers; diff --git a/compiler/src/core/alpha_eq.rs b/compiler/src/core/alpha_eq.rs index 5bf3fb6..c632391 100644 --- a/compiler/src/core/alpha_eq.rs +++ b/compiler/src/core/alpha_eq.rs @@ -1,7 +1,7 @@ use super::Term; /// Alpha-equality: structural equality ignoring `param_name` fields in Pi/Lam. -pub fn alpha_eq(a: &Term<'_>, b: &Term<'_>) -> bool { +pub fn alpha_eq(a: &Term<'_, '_>, b: &Term<'_, '_>) -> bool { // Fast path: pointer equality if std::ptr::eq(a, b) { return true; diff --git a/compiler/src/core/mod.rs b/compiler/src/core/mod.rs index ed807c4..09fff27 100644 --- a/compiler/src/core/mod.rs +++ b/compiler/src/core/mod.rs @@ -9,15 +9,15 @@ pub use prim::{IntType, IntWidth, Prim}; /// Match pattern in the core IR #[derive(Debug, Clone, PartialEq, Eq)] -pub enum Pat<'a> { +pub enum Pat<'n> { Lit(u64), - Bind(&'a Name), // named binding + Bind(&'n Name), // named binding Wildcard, // _ pattern } -impl<'a> Pat<'a> { +impl<'n> Pat<'n> { /// Return the name bound by this pattern, if any. - pub const fn bound_name(&self) -> Option<&'a Name> { + pub const fn bound_name(&self) -> Option<&'n Name> { match self { Pat::Bind(name) => Some(*name), Pat::Lit(_) | Pat::Wildcard => None, @@ -27,31 +27,31 @@ impl<'a> Pat<'a> { /// Match arm #[derive(Clone, Debug, PartialEq, Eq)] -pub struct Arm<'a> { - pub pat: Pat<'a>, - pub body: &'a Term<'a>, +pub struct Arm<'n, 't> { + pub pat: Pat<'n>, + pub body: &'t Term<'n, 't>, } /// Elaborated top-level function definition. #[derive(Debug)] -pub struct Function<'a> { - pub name: &'a Name, +pub struct Function<'n, 't> { + pub name: &'n Name, /// Function type: phase, params, and return type. - pub ty: &'a Pi<'a>, - pub body: &'a Term<'a>, + pub ty: &'t Pi<'n, 't>, + pub body: &'t Term<'n, 't>, } -impl<'a> Function<'a> { +impl<'n, 'a> Function<'n, 'a> { /// Return the function's Pi type. - pub const fn pi(&self) -> &Pi<'a> { + pub const fn pi(&self) -> &Pi<'n, 'a> { self.ty } } /// Elaborated program: a sequence of top-level function definitions #[derive(Debug)] -pub struct Program<'a> { - pub functions: &'a [Function<'a>], +pub struct Program<'n, 'a> { + pub functions: &'a [Function<'n, 'a>], } /// Function or primitive application: `func(args...)` @@ -64,9 +64,9 @@ pub struct Program<'a> { /// An empty `args` slice represents a zero-argument call and is distinct from /// a bare reference to `func`. #[derive(Debug, PartialEq, Eq)] -pub struct App<'a> { - pub func: &'a Term<'a>, - pub args: &'a [&'a Term<'a>], +pub struct App<'n, 'a> { + pub func: &'a Term<'n, 'a>, + pub args: &'a [&'a Term<'n, 'a>], } /// Dependent function type: `fn(params...) -> body_ty` @@ -75,38 +75,38 @@ pub struct App<'a> { /// This allows the globals table to store `&Term` directly, unifying type lookup /// for globals and locals. #[derive(Debug, PartialEq, Eq)] -pub struct Pi<'a> { - pub params: &'a [(&'a Name, &'a Term<'a>)], // (name, type) pairs - pub body_ty: &'a Term<'a>, +pub struct Pi<'n, 'a> { + pub params: &'a [(&'n Name, &'a Term<'n, 'a>)], // (name, type) pairs + pub body_ty: &'a Term<'n, 'a>, pub phase: Phase, } /// Lambda abstraction: |params...| body #[derive(Debug, PartialEq, Eq)] -pub struct Lam<'a> { - pub params: &'a [(&'a Name, &'a Term<'a>)], // (name, type) pairs - pub body: &'a Term<'a>, +pub struct Lam<'n, 'a> { + pub params: &'a [(&'n Name, &'a Term<'n, 'a>)], // (name, type) pairs + pub body: &'a Term<'n, 'a>, } /// Let binding with explicit type annotation and a body. #[derive(Debug, PartialEq, Eq)] -pub struct Let<'a> { - pub name: &'a Name, - pub ty: &'a Term<'a>, - pub expr: &'a Term<'a>, - pub body: &'a Term<'a>, +pub struct Let<'n, 'a> { + pub name: &'n Name, + pub ty: &'a Term<'n, 'a>, + pub expr: &'a Term<'n, 'a>, + pub body: &'a Term<'n, 'a>, } /// Pattern match. #[derive(Debug, PartialEq, Eq)] -pub struct Match<'a> { - pub scrutinee: &'a Term<'a>, - pub arms: &'a [Arm<'a>], +pub struct Match<'n, 'a> { + pub scrutinee: &'a Term<'n, 'a>, + pub arms: &'a [Arm<'n, 'a>], } /// Core term / type (terms and types are unified) #[derive(Debug, PartialEq, Eq, derive_more::From)] -pub enum Term<'a> { +pub enum Term<'n, 'a> { /// Local variable, identified by De Bruijn index (0 = innermost binder) Var(de_bruijn::Ix), /// Built-in type or operation (not applied) @@ -115,16 +115,16 @@ pub enum Term<'a> { /// Numeric literal with its integer type Lit(u64, IntType), /// Global function reference - Global(&'a Name), + Global(&'n Name), /// Function or primitive application: func(args...) #[from] - App(App<'a>), + App(App<'n, 'a>), /// Dependent function type: fn(x: A) -> B #[from] - Pi(Pi<'a>), + Pi(Pi<'n, 'a>), /// Lambda abstraction: |x: A| body #[from] - Lam(Lam<'a>), + Lam(Lam<'n, 'a>), /// Lift: [[T]] — meta type representing object-level code of type T Lift(&'a Self), /// Quotation: #(t) — produce object-level code from a meta expression @@ -133,13 +133,13 @@ pub enum Term<'a> { Splice(&'a Self), /// Let binding with explicit type annotation and a body #[from] - Let(Let<'a>), + Let(Let<'n, 'a>), /// Pattern match #[from] - Match(Match<'a>), + Match(Match<'n, 'a>), } -impl Term<'static> { +impl Term<'static, 'static> { // Integer types at meta phase pub const U0_META: Self = Self::Prim(Prim::IntTy(IntType::U0_META)); pub const U1_META: Self = Self::Prim(Prim::IntTy(IntType::U1_META)); @@ -195,12 +195,12 @@ impl Term<'static> { } } -impl<'a> Term<'a> { +impl<'n, 'a> Term<'n, 'a> { pub const fn new_app(func: &'a Self, args: &'a [&'a Self]) -> Self { Self::App(App { func, args }) } - pub const fn new_let(name: &'a Name, ty: &'a Self, expr: &'a Self, body: &'a Self) -> Self { + pub const fn new_let(name: &'n Name, ty: &'a Self, expr: &'a Self, body: &'a Self) -> Self { Self::Let(Let { name, ty, @@ -209,7 +209,7 @@ impl<'a> Term<'a> { }) } - pub const fn new_match(scrutinee: &'a Self, arms: &'a [Arm<'a>]) -> Self { + pub const fn new_match(scrutinee: &'a Self, arms: &'a [Arm<'n, 'a>]) -> Self { Self::Match(Match { scrutinee, arms }) } } diff --git a/compiler/src/core/pretty.rs b/compiler/src/core/pretty.rs index 340ebea..0b53b0d 100644 --- a/compiler/src/core/pretty.rs +++ b/compiler/src/core/pretty.rs @@ -13,13 +13,13 @@ fn write_indent(f: &mut fmt::Formatter<'_>, depth: usize) -> fmt::Result { // ── Core formatting ─────────────────────────────────────────────────────────── -impl<'a> Term<'a> { +impl<'n> Term<'n, '_> { /// Print `self` in **statement position**: emits leading indentation, then /// the term content. `Let` and `Match` are printed without an enclosing `{ }` /// (the caller is responsible for any surrounding braces). fn fmt_term( &self, - env: &mut Vec<&'a Name>, + env: &mut Vec<&'n Name>, indent: usize, f: &mut fmt::Formatter<'_>, ) -> fmt::Result { @@ -41,7 +41,7 @@ impl<'a> Term<'a> { /// a new indented block (e.g. `Let` / `Match`). fn fmt_term_inline( &self, - env: &mut Vec<&'a Name>, + env: &mut Vec<&'n Name>, indent: usize, f: &mut fmt::Formatter<'_>, ) -> fmt::Result { @@ -171,7 +171,7 @@ impl<'a> Term<'a> { /// syntactically valid as sub-expressions. fn fmt_expr( &self, - env: &mut Vec<&'a Name>, + env: &mut Vec<&'n Name>, indent: usize, f: &mut fmt::Formatter<'_>, ) -> fmt::Result { @@ -197,11 +197,11 @@ impl<'a> Term<'a> { } } -impl<'a> Arm<'a> { +impl<'n> Arm<'n, '_> { /// Print a single match arm. fn fmt_arm( &self, - env: &mut Vec<&'a Name>, + env: &mut Vec<&'n Name>, indent: usize, f: &mut fmt::Formatter<'_>, ) -> fmt::Result { @@ -225,7 +225,7 @@ impl<'a> Arm<'a> { // ── Display impls ───────────────────────────────────────────────────────────── -impl fmt::Display for Program<'_> { +impl fmt::Display for Program<'_, '_> { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { for (i, func) in self.functions.iter().enumerate() { if i > 0 { @@ -237,7 +237,7 @@ impl fmt::Display for Program<'_> { } } -impl fmt::Display for Function<'_> { +impl fmt::Display for Function<'_, '_> { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { let pi = self.pi(); diff --git a/compiler/src/core/value.rs b/compiler/src/core/value.rs index 87d5d55..87e0fe4 100644 --- a/compiler/src/core/value.rs +++ b/compiler/src/core/value.rs @@ -8,19 +8,19 @@ use bumpalo::Bump; use super::prim::IntType; use super::{Lam, Name, Pat, Pi, Prim, Term}; -use crate::common::{Phase, de_bruijn}; +use crate::common::{de_bruijn, Phase}; /// Working evaluation environment: index 0 = outermost binding, last = innermost. /// `Var(Ix(i))` maps to `env[env.len() - 1 - i]`. -pub type Env<'a> = Vec>; +pub type Env<'n, 'a> = Vec>; /// Semantic value — result of evaluating a term or type. #[derive(Clone, Debug)] -pub enum Value<'a> { +pub enum Value<'n, 'a> { /// Neutral: stuck on a local variable (identified by De Bruijn level) Rigid(de_bruijn::Lvl), /// Neutral: global function reference (not inlined during type-checking) - Global(&'a Name), + Global(&'n Name), /// Neutral: unapplied or partially applied primitive Prim(Prim), /// Neutral: stuck application (callee cannot reduce further) @@ -28,9 +28,9 @@ pub enum Value<'a> { /// Canonical: integer literal value Lit(u64, IntType), /// Canonical: lambda abstraction - Lam(VLam<'a>), + Lam(VLam<'n, 'a>), /// Canonical: dependent function type - Pi(VPi<'a>), + Pi(VPi<'n, 'a>), /// Canonical: lifted object type `[[T]]` Lift(&'a Self), /// Canonical: quoted object code `#(t)` @@ -46,9 +46,9 @@ pub enum Value<'a> { /// type of the i-th parameter (supporting dependent telescopes). /// `closure` takes all `params.len()` arguments. #[derive(Clone, Debug)] -pub struct VLam<'a> { - pub params: &'a [(&'a Name, Closure<'a>)], - pub closure: Closure<'a>, +pub struct VLam<'n, 'a> { + pub params: &'a [(&'n Name, Closure<'n, 'a>)], + pub closure: Closure<'n, 'a>, } /// Pi (dependent function type) value. @@ -56,25 +56,29 @@ pub struct VLam<'a> { /// Same telescope layout as `VLam`: `params[i].1` is instantiated with `args[0..i]` /// to yield the domain of the i-th parameter. `ret_closure` takes all `params.len()` args. #[derive(Clone, Debug)] -pub struct VPi<'a> { - pub params: &'a [(&'a Name, Closure<'a>)], - pub ret_closure: Closure<'a>, +pub struct VPi<'n, 'a> { + pub params: &'a [(&'n Name, Closure<'n, 'a>)], + pub ret_closure: Closure<'n, 'a>, pub phase: Phase, } /// A closure: snapshot of the environment at creation time, plus an unevaluated body. #[derive(Clone, Debug)] -pub struct Closure<'a> { +pub struct Closure<'n, 'a> { /// Arena-allocated environment snapshot (index 0 = outermost). - pub env: &'a [Value<'a>], + pub env: &'a [Value<'n, 'a>], /// Unevaluated body term. - pub body: &'a Term<'a>, + pub body: &'a Term<'n, 'a>, } /// Evaluate a term in an environment, producing a semantic value. /// /// `env[env.len() - 1 - ix]` gives the value for `Var(Ix(ix))`. -pub fn eval<'a>(arena: &'a Bump, env: &[Value<'a>], term: &'a Term<'a>) -> Value<'a> { +pub fn eval<'n, 'a>( + arena: &'a Bump, + env: &[Value<'n, 'a>], + term: &'a Term<'n, 'a>, +) -> Value<'n, 'a> { match term { Term::Var(ix) => { let lvl = ix.lvl_at(de_bruijn::Depth::new(env.len())); @@ -93,7 +97,8 @@ pub fn eval<'a>(arena: &'a Bump, env: &[Value<'a>], term: &'a Term<'a>) -> Value Term::App(app) => { let func_val = eval(arena, env, app.func); - let arg_vals: Vec> = app.args.iter().map(|a| eval(arena, env, a)).collect(); + let arg_vals: Vec> = + app.args.iter().map(|a| eval(arena, env, a)).collect(); apply_many(arena, func_val, &arg_vals) } @@ -120,7 +125,7 @@ pub fn eval<'a>(arena: &'a Bump, env: &[Value<'a>], term: &'a Term<'a>) -> Value Term::Let(let_) => { let val = eval(arena, env, let_.expr); - let mut env2: Vec> = env.to_vec(); + let mut env2: Vec> = env.to_vec(); env2.push(val); eval(arena, &env2, let_.body) } @@ -165,9 +170,13 @@ pub fn eval<'a>(arena: &'a Bump, env: &[Value<'a>], term: &'a Term<'a>) -> Value /// All parameter domain closures share the same base environment snapshot. /// Each domain closure's body uses De Bruijn indices to reference preceding /// parameters, so they are correctly differentiated despite sharing the base env. -pub fn eval_pi<'a>(arena: &'a Bump, env: &[Value<'a>], pi: &'a Pi<'a>) -> Value<'a> { +pub fn eval_pi<'n, 'a>( + arena: &'a Bump, + env: &[Value<'n, 'a>], + pi: &'a Pi<'n, 'a>, +) -> Value<'n, 'a> { let env_snapshot = arena.alloc_slice_fill_iter(env.iter().cloned()); - let params: Vec<(&'a Name, Closure<'a>)> = pi + let params: Vec<(&'n Name, Closure<'n, 'a>)> = pi .params .iter() .map(|&(name, ty_term)| { @@ -191,9 +200,9 @@ pub fn eval_pi<'a>(arena: &'a Bump, env: &[Value<'a>], pi: &'a Pi<'a>) -> Value< } /// Evaluate a multi-param Lam into a multi-param `Value::Lam` (no currying). -fn eval_lam<'a>(arena: &'a Bump, env: &[Value<'a>], lam: &'a Lam<'a>) -> Value<'a> { +fn eval_lam<'n, 'a>(arena: &'a Bump, env: &[Value<'n, 'a>], lam: &'a Lam<'n, 'a>) -> Value<'n, 'a> { let env_snapshot = arena.alloc_slice_fill_iter(env.iter().cloned()); - let params: Vec<(&'a Name, Closure<'a>)> = lam + let params: Vec<(&'n Name, Closure<'n, 'a>)> = lam .params .iter() .map(|&(name, ty_term)| { @@ -220,7 +229,11 @@ fn eval_lam<'a>(arena: &'a Bump, env: &[Value<'a>], lam: &'a Lam<'a>) -> Value<' /// For `Value::Lam` and `Value::Pi`, all args are pushed into the closure env at once. /// For neutrals, a stuck `App` node is produced. Each call site is its own `App` node; /// args are NOT flattened into existing `App` nodes to preserve call-site identity. -pub fn apply_many<'a>(arena: &'a Bump, func: Value<'a>, args: &[Value<'a>]) -> Value<'a> { +pub fn apply_many<'n, 'a>( + arena: &'a Bump, + func: Value<'n, 'a>, + args: &[Value<'n, 'a>], +) -> Value<'n, 'a> { match func { Value::Lam(vlam) => inst_n(arena, &vlam.closure, args), Value::Pi(vpi) => inst_n(arena, &vpi.ret_closure, args), @@ -249,7 +262,11 @@ pub fn apply_many<'a>(arena: &'a Bump, func: Value<'a>, args: &[Value<'a>]) -> V } /// Instantiate a closure with N arguments: extend env with all args, eval body. -pub fn inst_n<'a>(arena: &'a Bump, closure: &Closure<'a>, args: &[Value<'a>]) -> Value<'a> { +pub fn inst_n<'n, 'a>( + arena: &'a Bump, + closure: &Closure<'n, 'a>, + args: &[Value<'n, 'a>], +) -> Value<'n, 'a> { let mut env = closure.env.to_vec(); env.extend_from_slice(args); eval(arena, &env, closure.body) @@ -257,14 +274,14 @@ pub fn inst_n<'a>(arena: &'a Bump, closure: &Closure<'a>, args: &[Value<'a>]) -> /// Quote a telescope (sequence of named parameters with closures). /// Returns the quoted parameters, final depth, and the rigid values built during the process. -fn quote_telescope<'a>( +fn quote_telescope<'n, 'a>( arena: &'a Bump, initial_depth: de_bruijn::Depth, - params: &[(&'a Name, Closure<'a>)], + params: &[(&'n Name, Closure<'n, 'a>)], ) -> ( - Vec<(&'a Name, &'a Term<'a>)>, + Vec<(&'n Name, &'a Term<'n, 'a>)>, de_bruijn::Depth, - Vec>, + Vec>, ) { let mut rigid_vals = Vec::new(); let mut quoted_params = Vec::new(); @@ -284,7 +301,11 @@ fn quote_telescope<'a>( /// Convert a value back to a term (for error reporting and definitional equality). /// /// `depth` is the current De Bruijn depth (number of locally-bound variables in scope). -pub fn quote<'a>(arena: &'a Bump, depth: de_bruijn::Depth, val: &Value<'a>) -> &'a Term<'a> { +pub fn quote<'n, 'a>( + arena: &'a Bump, + depth: de_bruijn::Depth, + val: &Value<'n, 'a>, +) -> &'a Term<'n, 'a> { match val { Value::Rigid(lvl) => { let ix = lvl.ix_at(depth); @@ -295,7 +316,7 @@ pub fn quote<'a>(arena: &'a Bump, depth: de_bruijn::Depth, val: &Value<'a>) -> & Value::Lit(n, it) => arena.alloc(Term::Lit(*n, *it)), Value::App(f, args) => { let qf = quote(arena, depth, f); - let qargs: Vec<&'a Term<'a>> = args + let qargs: Vec<&'a Term<'n, 'a>> = args .iter() .map(|a| quote(arena, depth, a) as &'a _) .collect(); @@ -338,20 +359,25 @@ pub fn quote<'a>(arena: &'a Bump, depth: de_bruijn::Depth, val: &Value<'a>) -> & } /// Definitional equality: quote both values and compare structurally. -pub fn val_eq<'a>(arena: &'a Bump, depth: de_bruijn::Depth, a: &Value<'a>, b: &Value<'a>) -> bool { +pub fn val_eq<'n, 'a>( + arena: &'a Bump, + depth: de_bruijn::Depth, + a: &Value<'n, 'a>, + b: &Value<'n, 'a>, +) -> bool { let ta = quote(arena, depth, a); let tb = quote(arena, depth, b); super::alpha_eq::alpha_eq(ta, tb) } /// Evaluate a term in the empty environment. -pub fn eval_closed<'a>(arena: &'a Bump, term: &'a Term<'a>) -> Value<'a> { +pub fn eval_closed<'n, 'a>(arena: &'a Bump, term: &'a Term<'n, 'a>) -> Value<'n, 'a> { eval(arena, &[], term) } /// Extract the Phase from a Value that represents a universe (Type or `VmType`), /// if it is indeed a type universe. -pub const fn value_phase(val: &Value<'_>) -> Option { +pub const fn value_phase(val: &Value<'_, '_>) -> Option { match val { Value::Prim(Prim::IntTy(it)) => Some(it.phase), Value::Prim(Prim::U(_)) | Value::Lift(_) | Value::Pi(_) => Some(Phase::Meta), diff --git a/compiler/src/lexer/mod.rs b/compiler/src/lexer/mod.rs index 79197d2..f00d396 100644 --- a/compiler/src/lexer/mod.rs +++ b/compiler/src/lexer/mod.rs @@ -9,11 +9,12 @@ mod token; pub struct Lexer<'a> { input: &'a str, + names: &'a bumpalo::Bump, } impl<'a> Lexer<'a> { - pub const fn new(input: &'a str) -> Self { - Self { input } + pub const fn new(input: &'a str, names: &'a bumpalo::Bump) -> Self { + Self { input, names } } #[inline] @@ -54,7 +55,7 @@ impl<'a> Lexer<'a> { Token::KEYWORDS .iter() .find(|(kw, _)| *kw == ident) - .map_or(Token::Ident(Name::new(ident)), |(_, tok)| *tok) + .map_or(Token::Ident(Name::new(self.names.alloc_str(ident))), |(_, tok)| *tok) } #[inline] diff --git a/compiler/src/lexer/test/fuzz.rs b/compiler/src/lexer/test/fuzz.rs index cecffc5..a41700e 100644 --- a/compiler/src/lexer/test/fuzz.rs +++ b/compiler/src/lexer/test/fuzz.rs @@ -1,10 +1,13 @@ +use bumpalo::Bump; + use crate::lexer::Lexer; use bolero::check; #[test] fn lexer() { check!().with_type::().for_each(|input: &String| { - let lexer = Lexer::new(input); + let names = Bump::new(); + let lexer = Lexer::new(input, &names); let tokens = lexer.collect::>(); if tokens.iter().any(Result::is_ok) { eprintln!("[len={:3}] {input:?} {tokens:?}", input.len()); @@ -15,7 +18,8 @@ fn lexer() { #[test] fn token() { check!().with_type::().for_each(|input: &String| { - let token = Lexer::new(input).next(); + let names = Bump::new(); + let token = Lexer::new(input, &names).next(); if let Some(Ok(token)) = token { let len = input.len(); eprintln!("[len={len:03}] {input:?}: {token:?}"); diff --git a/compiler/src/parser/ast.rs b/compiler/src/parser/ast.rs index dc85299..32daa93 100644 --- a/compiler/src/parser/ast.rs +++ b/compiler/src/parser/ast.rs @@ -2,9 +2,9 @@ pub use crate::common::{Assoc, BinOp, Name, Phase, UnOp}; /// Function or operator reference #[derive(Clone, Copy, derive_more::Debug)] -pub enum FunName<'a> { +pub enum FunName<'n, 'a> { #[debug("{_0:?}")] - Term(&'a Term<'a>), + Term(&'a Term<'n, 'a>), #[debug("{_0:?}")] BinOp(BinOp), #[debug("{_0:?}")] @@ -12,68 +12,68 @@ pub enum FunName<'a> { } #[derive(derive_more::Debug)] -pub enum Pat<'a> { +pub enum Pat<'n> { #[debug("{_0:?}")] - Name(&'a Name), + Name(&'n Name), #[debug("{_0:?}")] Lit(u64), } #[derive(Debug)] -pub struct MatchArm<'a> { - pub pat: Pat<'a>, - pub body: &'a Term<'a>, +pub struct MatchArm<'n, 'a> { + pub pat: Pat<'n>, + pub body: &'a Term<'n, 'a>, } #[derive(Debug)] -pub struct Let<'a> { - pub name: &'a Name, - pub ty: Option<&'a Term<'a>>, - pub expr: &'a Term<'a>, +pub struct Let<'n, 'a> { + pub name: &'n Name, + pub ty: Option<&'a Term<'n, 'a>>, + pub expr: &'a Term<'n, 'a>, } #[derive(Debug)] -pub struct Param<'a> { - pub name: &'a Name, - pub ty: &'a Term<'a>, +pub struct Param<'n, 'a> { + pub name: &'n Name, + pub ty: &'a Term<'n, 'a>, } #[derive(Debug)] -pub struct Function<'a> { +pub struct Function<'n, 'a> { pub phase: Phase, - pub name: &'a Name, - pub params: &'a [Param<'a>], - pub ret_ty: &'a Term<'a>, - pub body: &'a Term<'a>, + pub name: &'n Name, + pub params: &'a [Param<'n, 'a>], + pub ret_ty: &'a Term<'n, 'a>, + pub body: &'a Term<'n, 'a>, } #[derive(Debug)] -pub struct Program<'a> { - pub functions: &'a [Function<'a>], +pub struct Program<'n, 'a> { + pub functions: &'a [Function<'n, 'a>], } #[derive(derive_more::Debug)] -pub enum Term<'a> { +pub enum Term<'n, 'a> { #[debug("{_0:?}")] Lit(u64), #[debug("{_0:?}")] - Var(&'a Name), + Var(&'n Name), App { - func: FunName<'a>, + func: FunName<'n, 'a>, args: &'a [&'a Self], }, /// Function type: `fn(name: ty, ...) -> ret_ty` Pi { - params: &'a [Param<'a>], + params: &'a [Param<'n, 'a>], ret_ty: &'a Self, }, /// Lambda: `|params| body` Lam { - params: &'a [Param<'a>], + params: &'a [Param<'n, 'a>], body: &'a Self, }, @@ -85,11 +85,11 @@ pub enum Term<'a> { Match { scrutinee: &'a Self, - arms: &'a [MatchArm<'a>], + arms: &'a [MatchArm<'n, 'a>], }, Block { - stmts: &'a [Let<'a>], + stmts: &'a [Let<'n, 'a>], expr: &'a Self, }, } diff --git a/compiler/src/parser/mod.rs b/compiler/src/parser/mod.rs index f751848..423482c 100644 --- a/compiler/src/parser/mod.rs +++ b/compiler/src/parser/mod.rs @@ -10,35 +10,35 @@ use crate::parser::ast::{ pub mod ast; -pub struct Parser<'a, I> +pub struct Parser<'n, 'a, I> where - I: Iterator>>, + I: Iterator>>, { tokens: Peekable, arena: &'a bumpalo::Bump, } -impl<'a, I> Parser<'a, I> +impl<'n, 'a, I> Parser<'n, 'a, I> where - I: Iterator>>, + I: Iterator>>, { pub fn new(tokens: I, arena: &'a bumpalo::Bump) -> Self { let tokens = tokens.peekable(); Self { tokens, arena } } - fn peek(&mut self) -> Option> { + fn peek(&mut self) -> Option> { self.tokens.peek().and_then(|r| r.as_ref().ok().copied()) } - fn next(&mut self) -> Option>> { + fn next(&mut self) -> Option>> { self.tokens.next() } /// Helper for extracting a token with a custom validation closure fn expect_token(&mut self, description: &str, f: F) -> Result where - F: FnOnce(Token<'a>) -> Option, + F: FnOnce(Token<'n>) -> Option, { match self.next() { Some(Ok(token)) => { @@ -49,13 +49,13 @@ where } } - fn take(&mut self, expected: Token<'a>) -> Result> { + fn take(&mut self, expected: Token<'n>) -> Result> { self.expect_token(&format!("{expected:?}"), |token| { (token == expected).then_some(token) }) } - fn take_ident(&mut self) -> Result<&'a Name> { + fn take_ident(&mut self) -> Result<&'n Name> { self.expect_token("identifier", |token| { if let Token::Ident(name) = token { Some(name) @@ -66,7 +66,7 @@ where } /// Consume a token if it matches the expected token - fn consume_if(&mut self, token: Token<'a>) -> bool { + fn consume_if(&mut self, token: Token<'n>) -> bool { if matches!(self.peek(), Some(t) if t == token) { self.next(); true @@ -76,12 +76,12 @@ where } /// Allocate a term and return a reference to it - fn alloc(&self, term: Term<'a>) -> &'a Term<'a> { + fn alloc(&self, term: Term<'n, 'a>) -> &'a Term<'n, 'a> { &*self.arena.alloc(term) } /// Parse a quoted expression: #(...) - fn parse_quoted_expr(&mut self) -> Result> { + fn parse_quoted_expr(&mut self) -> Result> { let expr = self.parse_expr().context("parsing quoted expression")?; self.take(Token::RParen) .context("expected ')' after quotation")?; @@ -89,13 +89,13 @@ where } /// Parse a quoted block: #{...} - fn parse_quoted_block(&mut self) -> Result> { + fn parse_quoted_block(&mut self) -> Result> { let (stmts, expr) = self.parse_block_inner()?; Ok(Term::Quote(self.alloc(Term::Block { stmts, expr }))) } /// Parse a spliced expression: $(...) - fn parse_spliced_expr(&mut self) -> Result> { + fn parse_spliced_expr(&mut self) -> Result> { let expr = self.parse_expr().context("parsing spliced expression")?; self.take(Token::RParen) .context("expected ')' after splice")?; @@ -103,13 +103,13 @@ where } /// Parse a spliced block: ${...} - fn parse_spliced_block(&mut self) -> Result> { + fn parse_spliced_block(&mut self) -> Result> { let (stmts, expr) = self.parse_block_inner()?; Ok(Term::Splice(self.alloc(Term::Block { stmts, expr }))) } /// Parse a lifted expression: [[...]] - fn parse_lifted_expr(&mut self) -> Result> { + fn parse_lifted_expr(&mut self) -> Result> { let expr = self.parse_expr().context("parsing lifted expression")?; self.take(Token::DoubleRBracket) .context("expected ']]' after lifted expression")?; @@ -117,7 +117,7 @@ where } /// Parse a comma-separated list of items bounded by a terminator token - fn parse_separated_list(&mut self, terminator: Token<'a>, mut parser: F) -> Result> + fn parse_separated_list(&mut self, terminator: Token<'n>, mut parser: F) -> Result> where F: FnMut(&mut Self) -> Result, { @@ -134,7 +134,7 @@ where Ok(items) } - pub fn parse_program(&mut self) -> Result> { + pub fn parse_program(&mut self) -> Result> { let mut functions = Vec::new(); while self.peek().is_some() { let fun = self.parse_fn_def()?; @@ -144,7 +144,7 @@ where Ok(Program { functions }) } - fn parse_fn_def(&mut self) -> Result> { + fn parse_fn_def(&mut self) -> Result> { let phase = if self.consume_if(Token::Code) { Phase::Object } else { @@ -158,7 +158,11 @@ where .with_context(|| format!("in function `{name}`")) } - fn parse_fn_def_after_name(&mut self, phase: Phase, name: &'a Name) -> Result> { + fn parse_fn_def_after_name( + &mut self, + phase: Phase, + name: &'n Name, + ) -> Result> { self.take(Token::LParen).context("expected '('")?; let params = self.parse_params()?; self.take(Token::RParen).context("expected ')'")?; @@ -180,7 +184,7 @@ where }) } - fn parse_params(&mut self) -> Result<&'a [Param<'a>]> { + fn parse_params(&mut self) -> Result<&'a [Param<'n, 'a>]> { let params = self.parse_separated_list(Token::RParen, |parser| { let name = parser.take_ident().context("expected parameter name")?; parser @@ -193,13 +197,13 @@ where Ok(self.arena.alloc_slice_fill_iter(params)) } - fn parse_block(&mut self) -> Result<&'a Term<'a>> { + fn parse_block(&mut self) -> Result<&'a Term<'n, 'a>> { self.take(Token::LBrace).context("expected '{'")?; let (stmts, expr) = self.parse_block_inner()?; Ok(self.alloc(Term::Block { stmts, expr })) } - fn parse_block_inner(&mut self) -> Result<(&'a [Let<'a>], &'a Term<'a>)> { + fn parse_block_inner(&mut self) -> Result<(&'a [Let<'n, 'a>], &'a Term<'n, 'a>)> { let mut stmts = Vec::new(); while self.peek() == Some(Token::Let) { @@ -214,7 +218,7 @@ where Ok((stmts, expr)) } - fn parse_let_stmt(&mut self) -> Result> { + fn parse_let_stmt(&mut self) -> Result> { self.take(Token::Let).context("expected 'let'")?; let name = self.take_ident().context("expected variable name")?; let ty = if self.consume_if(Token::Colon) { @@ -232,15 +236,15 @@ where Ok(Let { name, ty, expr }) } - fn parse_expr(&mut self) -> Result<&'a Term<'a>> { + fn parse_expr(&mut self) -> Result<&'a Term<'n, 'a>> { Ok(self.arena.alloc(self.parse_expr_owned()?)) } - fn parse_expr_owned(&mut self) -> Result> { + fn parse_expr_owned(&mut self) -> Result> { self.parse_expr_prec(Precedence::MIN) } - fn parse_expr_prec(&mut self, min_prec: Precedence) -> Result> { + fn parse_expr_prec(&mut self, min_prec: Precedence) -> Result> { let mut lhs = if let Some(op) = self.match_unop() { self.next(); let expr = self @@ -333,7 +337,7 @@ where } /// Parse a function call with arguments - fn parse_function_call(&mut self, name: &'a Name) -> Result> { + fn parse_function_call(&mut self, name: &'n Name) -> Result> { let args = self.parse_separated_list(Token::RParen, |parser| { parser.parse_expr().context("parsing function argument") })?; @@ -347,7 +351,7 @@ where } /// Parse a parenthesized expression - fn parse_paren_expr(&mut self) -> Result> { + fn parse_paren_expr(&mut self) -> Result> { let expr = self .parse_expr_owned() .context("parsing expression in parentheses")?; @@ -357,7 +361,7 @@ where } /// Parse a match expression - fn parse_match_expr(&mut self) -> Result> { + fn parse_match_expr(&mut self) -> Result> { let scrutinee = self.parse_expr().context("parsing match scrutinee")?; self.take(Token::LBrace) .context("expected '{' after match expression")?; @@ -371,7 +375,7 @@ where /// Parse a function type: `fn(params) -> ret_ty` /// /// Called after consuming the `fn` token. Each param is `name: type`. - fn parse_fn_type(&mut self) -> Result> { + fn parse_fn_type(&mut self) -> Result> { self.take(Token::LParen) .context("expected '(' in function type")?; let params = self.parse_params()?; @@ -388,7 +392,7 @@ where /// Parse a lambda expression: `|params| body` /// /// Called after consuming the `|` token. Each param is `name: type`. - fn parse_lambda(&mut self) -> Result> { + fn parse_lambda(&mut self) -> Result> { let params_vec = self.parse_separated_list(Token::Bar, |parser| { let name = parser .take_ident() @@ -415,7 +419,7 @@ where clippy::wildcard_enum_match_arm, reason = "unrecognised tokens are intentionally caught by the wildcard arm" )] - fn parse_atom_owned(&mut self) -> Result> { + fn parse_atom_owned(&mut self) -> Result> { let token = self.next().context("expected expression")??; match token { Token::Num(n) => Ok(Term::Lit(n)), @@ -445,7 +449,7 @@ where } } - fn parse_match_arms(&mut self) -> Result>> { + fn parse_match_arms(&mut self) -> Result>> { let mut arms = Vec::new(); while self.peek().is_some() && !matches!(self.peek(), Some(Token::RBrace)) { let pat = self.parse_pattern().context("parsing match pattern")?; @@ -465,7 +469,7 @@ where clippy::wildcard_enum_match_arm, reason = "unrecognised tokens are intentionally caught by the wildcard arm" )] - fn parse_pattern(&mut self) -> Result> { + fn parse_pattern(&mut self) -> Result> { let token = self.next().context("expected pattern")??; match token { Token::Num(n) => Ok(Pat::Lit(n)), diff --git a/compiler/src/parser/test/mod.rs b/compiler/src/parser/test/mod.rs index 4ae36b6..bf1e66a 100644 --- a/compiler/src/parser/test/mod.rs +++ b/compiler/src/parser/test/mod.rs @@ -18,7 +18,7 @@ use crate::parser::ast::{BinOp, FunName}; fn parse_expr(input: &str) -> String { let arena = bumpalo::Bump::new(); - let lexer = Lexer::new(input); + let lexer = Lexer::new(input, &arena); let mut parser = Parser::new(lexer, &arena); let expr = parser.parse_expr().unwrap(); format!("{expr:#?}\n") @@ -36,7 +36,7 @@ fn expr(#[files("src/parser/test/expr/*.input.txt")] path: PathBuf) { #[test] fn parse_trivial_block() { let arena = bumpalo::Bump::new(); - let lexer = Lexer::new("{ 0 + 1 }"); + let lexer = Lexer::new("{ 0 + 1 }", &arena); let mut parser = Parser::new(lexer, &arena); let expr = parser.parse_expr().unwrap(); match expr { @@ -48,7 +48,7 @@ fn parse_trivial_block() { #[test] fn parse_simple_fn() { let arena = bumpalo::Bump::new(); - let lexer = Lexer::new("fn add(x: u32, y: u32) -> u32 { x + y }"); + let lexer = Lexer::new("fn add(x: u32, y: u32) -> u32 { x + y }", &arena); let mut parser = Parser::new(lexer, &arena); let program = parser.parse_program().unwrap(); assert_eq!(program.functions.len(), 1); @@ -60,7 +60,7 @@ fn parse_simple_fn() { #[test] fn parse_simple_fn_and_junk() { let arena = bumpalo::Bump::new(); - let lexer = Lexer::new("fn foo() -> u32 { 0 } wat"); + let lexer = Lexer::new("fn foo() -> u32 { 0 } wat", &arena); let mut parser = Parser::new(lexer, &arena); let program = parser.parse_program(); assert!(program.is_err()); @@ -69,7 +69,7 @@ fn parse_simple_fn_and_junk() { #[test] fn parse_expr_prec() { let arena = bumpalo::Bump::new(); - let lexer = Lexer::new("1 + 2 * 3"); + let lexer = Lexer::new("1 + 2 * 3", &arena); let mut parser = Parser::new(lexer, &arena); let expr = parser.parse_expr().unwrap(); match expr { @@ -84,7 +84,7 @@ fn parse_expr_prec() { #[test] fn parse_expr_prec2() { let arena = bumpalo::Bump::new(); - let lexer = Lexer::new("1 * 2 + 3"); + let lexer = Lexer::new("1 * 2 + 3", &arena); let mut parser = Parser::new(lexer, &arena); let expr = parser.parse_expr().unwrap(); match expr { @@ -99,7 +99,7 @@ fn parse_expr_prec2() { #[test] fn parse_expr_paren() { let arena = bumpalo::Bump::new(); - let lexer = Lexer::new("1 * (2 + 3)"); + let lexer = Lexer::new("1 * (2 + 3)", &arena); let mut parser = Parser::new(lexer, &arena); let expr = parser.parse_expr().unwrap(); match expr { diff --git a/compiler/src/staging/mod.rs b/compiler/src/staging/mod.rs index db64c87..c209142 100644 --- a/compiler/src/staging/mod.rs +++ b/compiler/src/staging/mod.rs @@ -19,7 +19,7 @@ use crate::parser::ast::Phase; /// forbidden in Splic (the type-checker enforces this); `eval_obj` eagerly /// evaluates under binders by extending the environment with fresh level variables. #[derive(Clone, Debug)] -enum ObjVal<'a> { +enum ObjVal<'n, 'a> { /// Local variable identified by De Bruijn level (absolute, context-independent). Var(de_bruijn::Lvl), /// Integer literal. @@ -27,12 +27,12 @@ enum ObjVal<'a> { /// Unapplied primitive. Prim(Prim), /// Global function reference. - Global(&'a Name), + Global(&'n Name), /// Application. App(&'a Self, &'a [Self]), /// Let binding. Let { - name: &'a Name, + name: &'n Name, ty: &'a Self, expr: &'a Self, body: &'a Self, @@ -40,14 +40,14 @@ enum ObjVal<'a> { /// Pattern match. Match { scrutinee: &'a Self, - arms: &'a [ObjArm<'a>], + arms: &'a [ObjArm<'n, 'a>], }, } #[derive(Clone, Debug)] -struct ObjArm<'a> { - pat: Pat<'a>, - body: &'a ObjVal<'a>, +struct ObjArm<'n, 'a> { + pat: Pat<'n>, + body: &'a ObjVal<'n, 'a>, } // ── Meta-level values ───────────────────────────────────────────────────────── @@ -62,22 +62,22 @@ struct ObjArm<'a> { /// they are automatically discarded after staging; only the final `Term` output /// from `quote_obj` survives in the output arena. #[derive(Clone, Debug)] -enum MetaVal<'eval> { +enum MetaVal<'names, 'eval> { /// A concrete integer value computed at meta (compile) time. Lit(u64), /// Quoted object-level code as a semantic value. /// /// Uses De Bruijn levels internally, so it can be spliced into any depth /// without adjustment. Allocated in the eval arena. - Quote(&'eval ObjVal<'eval>), + Quote(&'eval ObjVal<'names, 'eval>), /// A type term passed as a type argument (dependent types: types are values). /// The type term itself is not inspected during evaluation. Ty, /// A closure: a lambda body captured with its environment. Closure { - body: &'eval Term<'eval>, + body: &'eval Term<'names, 'eval>, arity: usize, - env: Vec>, + env: Vec>, obj_depth: de_bruijn::Depth, }, } @@ -86,9 +86,9 @@ enum MetaVal<'eval> { /// A binding stored in the evaluation environment, indexed by De Bruijn level. #[derive(Clone, Debug)] -enum Binding<'eval> { +enum Binding<'names, 'eval> { /// A meta-level variable bound to a concrete `MetaVal`. - Meta(MetaVal<'eval>), + Meta(MetaVal<'names, 'eval>), /// An object-level variable. Obj(de_bruijn::Lvl), } @@ -98,12 +98,12 @@ enum Binding<'eval> { /// Bindings are stored oldest-first. `Var(Ix(i))` refers to /// `bindings[bindings.len() - 1 - i]` — the `i`-th binding from the end. #[derive(Debug)] -struct Env<'eval> { - bindings: Vec>, +struct Env<'names, 'eval> { + bindings: Vec>, obj_depth: de_bruijn::Depth, } -impl<'eval> Env<'eval> { +impl<'names, 'eval> Env<'names, 'eval> { const fn new(obj_depth: de_bruijn::Depth) -> Self { Env { bindings: Vec::new(), @@ -112,7 +112,7 @@ impl<'eval> Env<'eval> { } /// Look up the binding for `Var(Ix(ix))`. - fn get_ix(&self, ix: de_bruijn::Ix) -> &Binding<'eval> { + fn get_ix(&self, ix: de_bruijn::Ix) -> &Binding<'names, 'eval> { let depth = de_bruijn::Depth::new(self.bindings.len()); let lvl = ix.lvl_at(depth); let i = lvl.as_usize(); @@ -129,7 +129,7 @@ impl<'eval> Env<'eval> { } /// Push a meta-level binding bound to the given value. - fn push_meta(&mut self, val: MetaVal<'eval>) { + fn push_meta(&mut self, val: MetaVal<'names, 'eval>) { self.bindings.push(Binding::Meta(val)); } @@ -147,22 +147,22 @@ impl<'eval> Env<'eval> { // ── Globals table ───────────────────────────────────────────────────────────── /// Everything the evaluator needs to know about a top-level function. -struct GlobalDef<'a> { - ty: &'a Pi<'a>, - body: &'a Term<'a>, +struct GlobalDef<'n, 'a> { + ty: &'a Pi<'n, 'a>, + body: &'a Term<'n, 'a>, } -type Globals<'a> = HashMap<&'a Name, GlobalDef<'a>>; +type Globals<'n, 'a> = HashMap<&'n Name, GlobalDef<'n, 'a>>; // ── Meta-level evaluator ────────────────────────────────────────────────────── /// Evaluate a meta-level `term` to a `MetaVal`. -fn eval_meta<'eval>( +fn eval_meta<'names, 'eval>( eval_arena: &'eval Bump, - globals: &Globals<'eval>, - env: &mut Env<'eval>, - term: &'eval Term<'eval>, -) -> Result> { + globals: &Globals<'names, 'eval>, + env: &mut Env<'names, 'eval>, + term: &'eval Term<'names, 'eval>, +) -> Result> { match term { // ── Variable ───────────────────────────────────────────────────────── Term::Var(ix) => match env.get_ix(*ix) { @@ -197,7 +197,7 @@ fn eval_meta<'eval>( Term::Prim(prim) => eval_meta_prim(eval_arena, globals, env, *prim, app.args), _ => { let func_val = eval_meta(eval_arena, globals, env, app.func)?; - let arg_vals: Vec> = app + let arg_vals: Vec> = app .args .iter() .map(|a| eval_meta(eval_arena, globals, env, a)) @@ -242,10 +242,10 @@ fn eval_meta<'eval>( } /// Convert a global function definition into a closure value. -const fn global_to_closure<'eval>( - def: &GlobalDef<'eval>, +const fn global_to_closure<'names, 'eval>( + def: &GlobalDef<'names, 'eval>, obj_depth: de_bruijn::Depth, -) -> MetaVal<'eval> { +) -> MetaVal<'names, 'eval> { MetaVal::Closure { body: def.body, arity: def.ty.params.len(), @@ -255,12 +255,12 @@ const fn global_to_closure<'eval>( } /// Apply a closure value to N arguments simultaneously. -fn apply_closure_n<'eval>( +fn apply_closure_n<'names, 'eval>( eval_arena: &'eval Bump, - globals: &Globals<'eval>, - func_val: MetaVal<'eval>, - args: &[MetaVal<'eval>], -) -> Result> { + globals: &Globals<'names, 'eval>, + func_val: MetaVal<'names, 'eval>, + args: &[MetaVal<'names, 'eval>], +) -> Result> { match func_val { MetaVal::Closure { body, @@ -284,11 +284,11 @@ fn apply_closure_n<'eval>( } } -fn eval_lit<'eval>( +fn eval_lit<'names, 'eval>( eval_arena: &'eval Bump, - globals: &Globals<'eval>, - env: &mut Env<'eval>, - arg: &'eval Term<'eval>, + globals: &Globals<'names, 'eval>, + env: &mut Env<'names, 'eval>, + arg: &'eval Term<'names, 'eval>, ) -> Result { eval_meta(eval_arena, globals, env, arg).map(|v| match v { MetaVal::Lit(n) => n, @@ -298,11 +298,11 @@ fn eval_lit<'eval>( }) } -fn eval_bin_args<'eval>( +fn eval_bin_args<'names, 'eval>( eval_arena: &'eval Bump, - globals: &Globals<'eval>, - env: &mut Env<'eval>, - args: &'eval [&'eval Term<'eval>], + globals: &Globals<'names, 'eval>, + env: &mut Env<'names, 'eval>, + args: &'eval [&'eval Term<'names, 'eval>], ) -> Result<(u64, u64)> { let [lhs, rhs] = args else { panic!("binary primitive requires exactly 2 arguments (typechecker invariant)") @@ -313,13 +313,13 @@ fn eval_bin_args<'eval>( } /// Evaluate a primitive operation at meta level. -fn eval_meta_prim<'eval>( +fn eval_meta_prim<'names, 'eval>( eval_arena: &'eval Bump, - globals: &Globals<'eval>, - env: &mut Env<'eval>, + globals: &Globals<'names, 'eval>, + env: &mut Env<'names, 'eval>, prim: Prim, - args: &'eval [&'eval Term<'eval>], -) -> Result> { + args: &'eval [&'eval Term<'names, 'eval>], +) -> Result> { match prim { // ── Arithmetic ──────────────────────────────────────────────────────── Prim::Add(IntType { width, .. }) => { @@ -442,13 +442,13 @@ const fn mask_to_width(width: IntWidth, val: u64) -> u64 { } /// Evaluate a meta-level `match` expression. -fn eval_meta_match<'eval>( +fn eval_meta_match<'names, 'eval>( eval_arena: &'eval Bump, - globals: &Globals<'eval>, - env: &mut Env<'eval>, + globals: &Globals<'names, 'eval>, + env: &mut Env<'names, 'eval>, n: u64, - arms: &'eval [Arm<'eval>], -) -> Result> { + arms: &'eval [Arm<'names, 'eval>], +) -> Result> { for arm in arms { match &arm.pat { Pat::Lit(m) => { @@ -478,12 +478,12 @@ fn eval_meta_match<'eval>( /// /// All `ObjVal` nodes are allocated in `eval_arena` (a temporary arena); they are /// discarded once `quote_obj` has converted them to output `Term` nodes. -fn eval_obj<'eval>( +fn eval_obj<'names, 'eval>( eval_arena: &'eval Bump, - globals: &Globals<'eval>, - env: &mut Env<'eval>, - term: &'eval Term<'eval>, -) -> Result<&'eval ObjVal<'eval>> { + globals: &Globals<'names, 'eval>, + env: &mut Env<'names, 'eval>, + term: &'eval Term<'names, 'eval>, +) -> Result<&'eval ObjVal<'names, 'eval>> { match term { // ── Variable ───────────────────────────────────────────────────────── Term::Var(ix) => match env.get_ix(*ix) { @@ -520,7 +520,7 @@ fn eval_obj<'eval>( // ── App ─────────────────────────────────────────────────────────────── Term::App(app) => { let func_val = eval_obj(eval_arena, globals, env, app.func)?; - let arg_vals: &'eval [ObjVal<'eval>] = eval_arena.alloc_slice_try_fill_iter( + let arg_vals: &'eval [ObjVal<'names, 'eval>] = eval_arena.alloc_slice_try_fill_iter( app.args .iter() .map(|arg| eval_obj(eval_arena, globals, env, arg).cloned()), @@ -558,7 +558,7 @@ fn eval_obj<'eval>( // ── Match ──────────────────────────────────────────────────────────── Term::Match(match_) => { let scrutinee_val = eval_obj(eval_arena, globals, env, match_.scrutinee)?; - let arm_vals: &'eval [ObjArm<'eval>] = eval_arena.alloc_slice_try_fill_iter( + let arm_vals: &'eval [ObjArm<'_, 'eval>] = eval_arena.alloc_slice_try_fill_iter( match_.arms.iter().map(|arm| -> Result<_> { let has_binding = arm.pat.bound_name().is_some(); if has_binding { @@ -593,20 +593,16 @@ fn eval_obj<'eval>( /// Convert an `ObjVal` back to a `Term` by translating De Bruijn levels to indices. /// /// `depth` is the number of object-level variables currently in scope. -/// Names are copied into the output arena here — `eval_obj` stores bare references -/// into the (temporary) eval arena; this is the single place they migrate to `'out`. -fn quote_obj<'out>( +fn quote_obj<'names, 'out>( out_arena: &'out Bump, depth: de_bruijn::Depth, - val: &ObjVal<'_>, -) -> &'out Term<'out> { + val: &ObjVal<'names, '_>, +) -> &'out Term<'names, 'out> { match val { ObjVal::Var(lvl) => out_arena.alloc(Term::Var(lvl.ix_at(depth))), ObjVal::Lit(n, it) => out_arena.alloc(Term::Lit(*n, *it)), ObjVal::Prim(p) => out_arena.alloc(Term::Prim(*p)), - ObjVal::Global(name) => { - out_arena.alloc(Term::Global(Name::new(out_arena.alloc_str(name.as_str())))) - } + ObjVal::Global(name) => out_arena.alloc(Term::Global(name)), ObjVal::App(func, args) => { let qfunc = quote_obj(out_arena, depth, func); let qargs = out_arena @@ -622,8 +618,7 @@ fn quote_obj<'out>( let qty = quote_obj(out_arena, depth, ty); let qexpr = quote_obj(out_arena, depth, expr); let qbody = quote_obj(out_arena, depth.succ(), body); - let out_name = Name::new(out_arena.alloc_str(name.as_str())); - out_arena.alloc(Term::new_let(out_name, qty, qexpr, qbody)) + out_arena.alloc(Term::new_let(name, qty, qexpr, qbody)) } ObjVal::Match { scrutinee, arms } => { let qscrutinee = quote_obj(out_arena, depth, scrutinee); @@ -635,7 +630,7 @@ fn quote_obj<'out>( }; let out_pat = match &arm.pat { Pat::Lit(n) => Pat::Lit(*n), - Pat::Bind(name) => Pat::Bind(Name::new(out_arena.alloc_str(name.as_str()))), + Pat::Bind(name) => Pat::Bind(name), Pat::Wildcard => Pat::Wildcard, }; Arm { @@ -652,13 +647,13 @@ fn quote_obj<'out>( /// Unstage an elaborated program. /// -/// - `out_arena`: output arena; the returned `Program<'out>` is allocated here. +/// - `out_arena`: output arena; the returned `Program` is allocated here. /// - `program`: input core program; may be dropped once this function returns. -pub fn unstage_program<'out, 'core>( +pub fn unstage_program<'names, 'out, 'core>( out_arena: &'out Bump, - program: &'core Program<'core>, -) -> Result> { - let globals: Globals<'_> = program + program: &'core Program<'names, 'core>, +) -> Result> { + let globals: Globals<'names, '_> = program .functions .iter() .map(|f| { @@ -672,7 +667,7 @@ pub fn unstage_program<'out, 'core>( }) .collect(); - let staged_fns: Vec> = program + let staged_fns: Vec> = program .functions .iter() .filter(|f| f.pi().phase.is_object()) @@ -685,11 +680,11 @@ pub fn unstage_program<'out, 'core>( let mut env = Env::new(de_bruijn::Depth::ZERO); let staged_params = out_arena.alloc_slice_try_fill_iter(pi.params.iter().map( - |(n, ty)| -> Result<(&'out Name, &'out Term<'out>)> { + |(n, ty)| -> Result<(&'names Name, &'out Term<'names, 'out>)> { let ty_val = eval_obj(&eval_arena, &globals, &mut env, ty)?; let staged_ty = quote_obj(out_arena, env.obj_depth, ty_val); env.push_obj(); - Ok((Name::new(out_arena.alloc_str(n.as_str())), staged_ty)) + Ok((n, staged_ty)) }, ))?; @@ -700,7 +695,7 @@ pub fn unstage_program<'out, 'core>( let staged_body = quote_obj(out_arena, env.obj_depth, body_val); Ok(Function { - name: Name::new(out_arena.alloc_str(f.name.as_str())), + name: f.name, ty: out_arena.alloc(Pi { params: staged_params, body_ty: staged_ret_ty, diff --git a/compiler/tests/snap.rs b/compiler/tests/snap.rs index a4726fa..f12b15f 100644 --- a/compiler/tests/snap.rs +++ b/compiler/tests/snap.rs @@ -24,7 +24,7 @@ fn snap(#[files("tests/snap/*/*/0_input.splic")] path: PathBuf) { let arena = Bump::new(); // ── Phase 1: Lex ──────────────────────────────────────────────────────── - let lex_result: Result, _> = Lexer::new(&input).collect(); + let lex_result: Result, _> = Lexer::new(&input, &arena).collect(); let lex_snap = match &lex_result { Ok(tokens) => { use std::fmt::Write as _; From f5bc8bc82c7fea02b865e56b03640916af6826bd Mon Sep 17 00:00:00 2001 From: LukasK Date: Mon, 6 Apr 2026 08:23:33 +0000 Subject: [PATCH 2/6] refactor: rename single-letter lifetimes to descriptive names MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - `'n` → `'names` everywhere (names arena) - `'a` → `'ast` in parser and checker function signatures (AST arena) - `'a` → `'eval` for ObjVal/ObjArm in staging (eval arena) - `'a` → `'names` for Token and Lexer (names arena) - `'c` → `'core` in elaborate_sig (core arena) - `'t` → `'a` in core::Arm and core::Function (normalise with other structs) The `'a` parameter in core IR type definitions (Term, Pi, Lam, etc.) remains `'a` as it is polymorphic over 'core/'eval/'out. Co-Authored-By: Claude Sonnet 4.6 --- compiler/src/checker/elaborate.rs | 36 ++++++------ compiler/src/checker/infer.rs | 88 ++++++++++++++--------------- compiler/src/core/mod.rs | 84 +++++++++++++-------------- compiler/src/core/pretty.rs | 12 ++-- compiler/src/core/value.rs | 94 +++++++++++++++---------------- compiler/src/lexer/mod.rs | 28 ++++----- compiler/src/lexer/token.rs | 4 +- compiler/src/parser/ast.rs | 72 +++++++++++------------ compiler/src/parser/mod.rs | 76 ++++++++++++------------- compiler/src/staging/mod.rs | 32 +++++------ 10 files changed, 263 insertions(+), 263 deletions(-) diff --git a/compiler/src/checker/elaborate.rs b/compiler/src/checker/elaborate.rs index 1edf7bd..e0665f3 100644 --- a/compiler/src/checker/elaborate.rs +++ b/compiler/src/checker/elaborate.rs @@ -9,14 +9,14 @@ use super::Ctx; use super::infer; /// Elaborate one function's signature into a `Pi` (the globals table entry). -fn elaborate_sig<'n, 'a, 'c>( - arena: &'c bumpalo::Bump, - func: &ast::Function<'n, 'a>, -) -> Result<&'c core::Pi<'n, 'c>> { - let empty_globals: HashMap<&'n core::Name, &'c core::Pi<'n, 'c>> = HashMap::new(); +fn elaborate_sig<'names, 'ast, 'core>( + arena: &'core bumpalo::Bump, + func: &ast::Function<'names, 'ast>, +) -> Result<&'core core::Pi<'names, 'core>> { + let empty_globals: HashMap<&'names core::Name, &'core core::Pi<'names, 'core>> = HashMap::new(); let mut ctx = Ctx::new(arena, &empty_globals); - let params: &'c [(&'n core::Name, &'c core::Term<'n, 'c>)] = + let params: &'core [(&'names core::Name, &'core core::Term<'names, 'core>)] = arena.alloc_slice_try_fill_iter(func.params.iter().map(|p| -> Result<_> { let (param_ty, _) = infer::infer(&mut ctx, func.phase, p.ty)?; ctx.push_local(p.name, param_ty); @@ -38,11 +38,11 @@ fn elaborate_sig<'n, 'a, 'c>( } /// Pass 1: collect all top-level function signatures into a globals table. -pub fn collect_signatures<'n, 'a, 'core>( +pub fn collect_signatures<'names, 'ast, 'core>( arena: &'core bumpalo::Bump, - program: &ast::Program<'n, 'a>, -) -> Result>> { - let mut globals: HashMap<&'n core::Name, &'core core::Pi<'n, 'core>> = HashMap::new(); + program: &ast::Program<'names, 'ast>, +) -> Result>> { + let mut globals: HashMap<&'names core::Name, &'core core::Pi<'names, 'core>> = HashMap::new(); for func in program.functions { let name = func.name; @@ -61,12 +61,12 @@ pub fn collect_signatures<'n, 'a, 'core>( } /// Pass 2: elaborate all function bodies with the full globals table available. -fn elaborate_bodies<'n, 'a, 'core>( +fn elaborate_bodies<'names, 'ast, 'core>( arena: &'core bumpalo::Bump, - program: &ast::Program<'n, 'a>, - globals: &HashMap<&'n core::Name, &'core core::Pi<'n, 'core>>, -) -> Result> { - let functions: &'core [core::Function<'n, 'core>] = + program: &ast::Program<'names, 'ast>, + globals: &HashMap<&'names core::Name, &'core core::Pi<'names, 'core>>, +) -> Result> { + let functions: &'core [core::Function<'names, 'core>] = arena.alloc_slice_try_fill_iter(program.functions.iter().map(|func| -> Result<_> { let name = func.name; let pi = *globals.get(&name).expect("signature missing from pass 1"); @@ -92,10 +92,10 @@ fn elaborate_bodies<'n, 'a, 'core>( } /// Elaborate the entire program in two passes -pub fn elaborate_program<'n, 'core>( +pub fn elaborate_program<'names, 'core>( arena: &'core bumpalo::Bump, - program: &ast::Program<'n, '_>, -) -> Result> { + program: &ast::Program<'names, '_>, +) -> Result> { let globals = collect_signatures(arena, program)?; elaborate_bodies(arena, program, &globals) } diff --git a/compiler/src/checker/infer.rs b/compiler/src/checker/infer.rs index 390d641..3d45282 100644 --- a/compiler/src/checker/infer.rs +++ b/compiler/src/checker/infer.rs @@ -12,10 +12,10 @@ use super::{builtin_prim_ty, Ctx}; clippy::too_many_lines, reason = "large match over all surface term variants" )] -pub fn infer<'names, 'a, 'core>( +pub fn infer<'names, 'ast, 'core>( ctx: &mut Ctx<'names, 'core, '_>, phase: Phase, - term: &'a ast::Term<'names, 'a>, + term: &'ast ast::Term<'names, 'ast>, ) -> Result<(&'core core::Term<'names, 'core>, value::Value<'names, 'core>)> { match term { // ------------------------------------------------------------------ Var @@ -364,7 +364,7 @@ fn check_exhaustiveness( } /// Elaborate a match pattern into a core pattern. -fn elaborate_pat<'n>(pat: &ast::Pat<'n>) -> core::Pat<'n> { +fn elaborate_pat<'names>(pat: &ast::Pat<'names>) -> core::Pat<'names> { match pat { ast::Pat::Lit(n) => core::Pat::Lit(*n), ast::Pat::Name(name) => match name.as_str() { @@ -375,18 +375,18 @@ fn elaborate_pat<'n>(pat: &ast::Pat<'n>) -> core::Pat<'n> { } /// Elaborate a single `let` binding. -fn elaborate_let<'n, 'a, 'core, T, F, G, W>( - ctx: &mut Ctx<'n, 'core, '_>, +fn elaborate_let<'names, 'ast, 'core, T, F, G, W>( + ctx: &mut Ctx<'names, 'core, '_>, phase: Phase, - stmt: &'a ast::Let<'n, 'a>, + stmt: &'ast ast::Let<'names, 'ast>, cont: F, body_of: G, wrap: W, ) -> Result where - F: FnOnce(&mut Ctx<'n, 'core, '_>) -> Result, - G: FnOnce(&T) -> &'core core::Term<'n, 'core>, - W: FnOnce(&'core core::Term<'n, 'core>, T) -> T, + F: FnOnce(&mut Ctx<'names, 'core, '_>) -> Result, + G: FnOnce(&T) -> &'core core::Term<'names, 'core>, + W: FnOnce(&'core core::Term<'names, 'core>, T) -> T, { let (core_expr, bind_ty_val) = if let Some(ann) = stmt.ty { let (ty, _) = infer(ctx, phase, ann)?; @@ -420,12 +420,12 @@ where } /// Elaborate a sequence of `let` bindings followed by a trailing expression (infer mode). -fn infer_block<'n, 'a, 'core>( - ctx: &mut Ctx<'n, 'core, '_>, +fn infer_block<'names, 'ast, 'core>( + ctx: &mut Ctx<'names, 'core, '_>, phase: Phase, - stmts: &'a [ast::Let<'n, 'a>], - expr: &'a ast::Term<'n, 'a>, -) -> Result<(&'core core::Term<'n, 'core>, value::Value<'n, 'core>)> { + stmts: &'ast [ast::Let<'names, 'ast>], + expr: &'ast ast::Term<'names, 'ast>, +) -> Result<(&'core core::Term<'names, 'core>, value::Value<'names, 'core>)> { match stmts { [] => infer(ctx, phase, expr), [first, rest @ ..] => elaborate_let( @@ -440,14 +440,14 @@ fn infer_block<'n, 'a, 'core>( } /// Elaborate a sequence of `let` bindings followed by a trailing expression (check mode). -fn check_block_val<'n, 'a, 'core>( - ctx: &mut Ctx<'n, 'core, '_>, +fn check_block_val<'names, 'ast, 'core>( + ctx: &mut Ctx<'names, 'core, '_>, phase: Phase, - stmts: &'a [ast::Let<'n, 'a>], - expr: &'a ast::Term<'n, 'a>, - expected: value::Value<'n, 'core>, - expected_term: Option<&'core core::Term<'n, 'core>>, -) -> Result<&'core core::Term<'n, 'core>> { + stmts: &'ast [ast::Let<'names, 'ast>], + expr: &'ast ast::Term<'names, 'ast>, + expected: value::Value<'names, 'core>, + expected_term: Option<&'core core::Term<'names, 'core>>, +) -> Result<&'core core::Term<'names, 'core>> { match stmts { [] => check_val_impl(ctx, phase, expr, expected, expected_term), [first, rest @ ..] => elaborate_let( @@ -465,11 +465,11 @@ fn check_block_val<'n, 'a, 'core>( /// /// Equivalent to `check(ctx, phase, term, Type)` for meta phase or /// `check(ctx, phase, term, VmType)` for object phase. -fn check_universe<'n, 'a, 'core>( - ctx: &mut Ctx<'n, 'core, '_>, +fn check_universe<'names, 'ast, 'core>( + ctx: &mut Ctx<'names, 'core, '_>, phase: Phase, - term: &'a ast::Term<'n, 'a>, -) -> Result<&'core core::Term<'n, 'core>> { + term: &'ast ast::Term<'names, 'ast>, +) -> Result<&'core core::Term<'names, 'core>> { let universe: &core::Term = match phase { Phase::Meta => &core::Term::TYPE, Phase::Object => &core::Term::VM_TYPE, @@ -481,23 +481,23 @@ fn check_universe<'n, 'a, 'core>( /// /// This is a convenience wrapper for callers that have an expected type as a `&Term`. /// It also threads the expected term through for dependent-type arm refinement. -pub fn check<'n, 'a, 'core>( - ctx: &mut Ctx<'n, 'core, '_>, +pub fn check<'names, 'ast, 'core>( + ctx: &mut Ctx<'names, 'core, '_>, phase: Phase, - term: &'a ast::Term<'n, 'a>, - expected: &'core core::Term<'n, 'core>, -) -> Result<&'core core::Term<'n, 'core>> { + term: &'ast ast::Term<'names, 'ast>, + expected: &'core core::Term<'names, 'core>, +) -> Result<&'core core::Term<'names, 'core>> { let expected_val = ctx.eval(expected); check_val_impl(ctx, phase, term, expected_val, Some(expected)) } /// Check `term` against `expected` (as a semantic Value), returning the elaborated core term. -pub fn check_val<'n, 'a, 'core>( - ctx: &mut Ctx<'n, 'core, '_>, +pub fn check_val<'names, 'ast, 'core>( + ctx: &mut Ctx<'names, 'core, '_>, phase: Phase, - term: &'a ast::Term<'n, 'a>, - expected: value::Value<'n, 'core>, -) -> Result<&'core core::Term<'n, 'core>> { + term: &'ast ast::Term<'names, 'ast>, + expected: value::Value<'names, 'core>, +) -> Result<&'core core::Term<'names, 'core>> { check_val_impl(ctx, phase, term, expected, None) } @@ -507,13 +507,13 @@ pub fn check_val<'n, 'a, 'core>( clippy::too_many_lines, reason = "large match over all surface term variants" )] -fn check_val_impl<'n, 'a, 'core>( - ctx: &mut Ctx<'n, 'core, '_>, +fn check_val_impl<'names, 'ast, 'core>( + ctx: &mut Ctx<'names, 'core, '_>, phase: Phase, - term: &'a ast::Term<'n, 'a>, - expected: value::Value<'n, 'core>, - expected_term: Option<&'core core::Term<'n, 'core>>, -) -> Result<&'core core::Term<'n, 'core>> { + term: &'ast ast::Term<'names, 'ast>, + expected: value::Value<'names, 'core>, + expected_term: Option<&'core core::Term<'names, 'core>>, +) -> Result<&'core core::Term<'names, 'core>> { match term { // ------------------------------------------------------------------ Lit ast::Term::Lit(n) => match &expected { @@ -665,9 +665,9 @@ fn check_val_impl<'n, 'a, 'core>( vpi.params.len() ); - let mut elaborated_params: Vec<(&'n core::Name, &'core core::Term<'n, 'core>)> = + let mut elaborated_params: Vec<(&'names core::Name, &'core core::Term<'names, 'core>)> = Vec::new(); - let mut arg_vals: Vec> = Vec::new(); + let mut arg_vals: Vec> = Vec::new(); for (p, (_, domain_cl)) in params.iter().zip(vpi.params.iter()) { let param_name = p.name; @@ -719,7 +719,7 @@ fn check_val_impl<'n, 'a, 'core>( _ => None, }; - let core_arms: &'core [core::Arm<'n, 'core>] = + let core_arms: &'core [core::Arm<'names, 'core>] = ctx.arena .alloc_slice_try_fill_iter(arms.iter().map(|arm| -> Result<_> { let core_pat = elaborate_pat(&arm.pat); diff --git a/compiler/src/core/mod.rs b/compiler/src/core/mod.rs index 09fff27..601a8e6 100644 --- a/compiler/src/core/mod.rs +++ b/compiler/src/core/mod.rs @@ -9,15 +9,15 @@ pub use prim::{IntType, IntWidth, Prim}; /// Match pattern in the core IR #[derive(Debug, Clone, PartialEq, Eq)] -pub enum Pat<'n> { +pub enum Pat<'names> { Lit(u64), - Bind(&'n Name), // named binding + Bind(&'names Name), // named binding Wildcard, // _ pattern } -impl<'n> Pat<'n> { +impl<'names> Pat<'names> { /// Return the name bound by this pattern, if any. - pub const fn bound_name(&self) -> Option<&'n Name> { + pub const fn bound_name(&self) -> Option<&'names Name> { match self { Pat::Bind(name) => Some(*name), Pat::Lit(_) | Pat::Wildcard => None, @@ -27,31 +27,31 @@ impl<'n> Pat<'n> { /// Match arm #[derive(Clone, Debug, PartialEq, Eq)] -pub struct Arm<'n, 't> { - pub pat: Pat<'n>, - pub body: &'t Term<'n, 't>, +pub struct Arm<'names, 'a> { + pub pat: Pat<'names>, + pub body: &'a Term<'names, 'a>, } /// Elaborated top-level function definition. #[derive(Debug)] -pub struct Function<'n, 't> { - pub name: &'n Name, +pub struct Function<'names, 'a> { + pub name: &'names Name, /// Function type: phase, params, and return type. - pub ty: &'t Pi<'n, 't>, - pub body: &'t Term<'n, 't>, + pub ty: &'a Pi<'names, 'a>, + pub body: &'a Term<'names, 'a>, } -impl<'n, 'a> Function<'n, 'a> { +impl<'names, 'a> Function<'names, 'a> { /// Return the function's Pi type. - pub const fn pi(&self) -> &Pi<'n, 'a> { + pub const fn pi(&self) -> &Pi<'names, 'a> { self.ty } } /// Elaborated program: a sequence of top-level function definitions #[derive(Debug)] -pub struct Program<'n, 'a> { - pub functions: &'a [Function<'n, 'a>], +pub struct Program<'names, 'a> { + pub functions: &'a [Function<'names, 'a>], } /// Function or primitive application: `func(args...)` @@ -64,9 +64,9 @@ pub struct Program<'n, 'a> { /// An empty `args` slice represents a zero-argument call and is distinct from /// a bare reference to `func`. #[derive(Debug, PartialEq, Eq)] -pub struct App<'n, 'a> { - pub func: &'a Term<'n, 'a>, - pub args: &'a [&'a Term<'n, 'a>], +pub struct App<'names, 'a> { + pub func: &'a Term<'names, 'a>, + pub args: &'a [&'a Term<'names, 'a>], } /// Dependent function type: `fn(params...) -> body_ty` @@ -75,38 +75,38 @@ pub struct App<'n, 'a> { /// This allows the globals table to store `&Term` directly, unifying type lookup /// for globals and locals. #[derive(Debug, PartialEq, Eq)] -pub struct Pi<'n, 'a> { - pub params: &'a [(&'n Name, &'a Term<'n, 'a>)], // (name, type) pairs - pub body_ty: &'a Term<'n, 'a>, +pub struct Pi<'names, 'a> { + pub params: &'a [(&'names Name, &'a Term<'names, 'a>)], // (name, type) pairs + pub body_ty: &'a Term<'names, 'a>, pub phase: Phase, } /// Lambda abstraction: |params...| body #[derive(Debug, PartialEq, Eq)] -pub struct Lam<'n, 'a> { - pub params: &'a [(&'n Name, &'a Term<'n, 'a>)], // (name, type) pairs - pub body: &'a Term<'n, 'a>, +pub struct Lam<'names, 'a> { + pub params: &'a [(&'names Name, &'a Term<'names, 'a>)], // (name, type) pairs + pub body: &'a Term<'names, 'a>, } /// Let binding with explicit type annotation and a body. #[derive(Debug, PartialEq, Eq)] -pub struct Let<'n, 'a> { - pub name: &'n Name, - pub ty: &'a Term<'n, 'a>, - pub expr: &'a Term<'n, 'a>, - pub body: &'a Term<'n, 'a>, +pub struct Let<'names, 'a> { + pub name: &'names Name, + pub ty: &'a Term<'names, 'a>, + pub expr: &'a Term<'names, 'a>, + pub body: &'a Term<'names, 'a>, } /// Pattern match. #[derive(Debug, PartialEq, Eq)] -pub struct Match<'n, 'a> { - pub scrutinee: &'a Term<'n, 'a>, - pub arms: &'a [Arm<'n, 'a>], +pub struct Match<'names, 'a> { + pub scrutinee: &'a Term<'names, 'a>, + pub arms: &'a [Arm<'names, 'a>], } /// Core term / type (terms and types are unified) #[derive(Debug, PartialEq, Eq, derive_more::From)] -pub enum Term<'n, 'a> { +pub enum Term<'names, 'a> { /// Local variable, identified by De Bruijn index (0 = innermost binder) Var(de_bruijn::Ix), /// Built-in type or operation (not applied) @@ -115,16 +115,16 @@ pub enum Term<'n, 'a> { /// Numeric literal with its integer type Lit(u64, IntType), /// Global function reference - Global(&'n Name), + Global(&'names Name), /// Function or primitive application: func(args...) #[from] - App(App<'n, 'a>), + App(App<'names, 'a>), /// Dependent function type: fn(x: A) -> B #[from] - Pi(Pi<'n, 'a>), + Pi(Pi<'names, 'a>), /// Lambda abstraction: |x: A| body #[from] - Lam(Lam<'n, 'a>), + Lam(Lam<'names, 'a>), /// Lift: [[T]] — meta type representing object-level code of type T Lift(&'a Self), /// Quotation: #(t) — produce object-level code from a meta expression @@ -133,10 +133,10 @@ pub enum Term<'n, 'a> { Splice(&'a Self), /// Let binding with explicit type annotation and a body #[from] - Let(Let<'n, 'a>), + Let(Let<'names, 'a>), /// Pattern match #[from] - Match(Match<'n, 'a>), + Match(Match<'names, 'a>), } impl Term<'static, 'static> { @@ -195,12 +195,12 @@ impl Term<'static, 'static> { } } -impl<'n, 'a> Term<'n, 'a> { +impl<'names, 'a> Term<'names, 'a> { pub const fn new_app(func: &'a Self, args: &'a [&'a Self]) -> Self { Self::App(App { func, args }) } - pub const fn new_let(name: &'n Name, ty: &'a Self, expr: &'a Self, body: &'a Self) -> Self { + pub const fn new_let(name: &'names Name, ty: &'a Self, expr: &'a Self, body: &'a Self) -> Self { Self::Let(Let { name, ty, @@ -209,7 +209,7 @@ impl<'n, 'a> Term<'n, 'a> { }) } - pub const fn new_match(scrutinee: &'a Self, arms: &'a [Arm<'n, 'a>]) -> Self { + pub const fn new_match(scrutinee: &'a Self, arms: &'a [Arm<'names, 'a>]) -> Self { Self::Match(Match { scrutinee, arms }) } } diff --git a/compiler/src/core/pretty.rs b/compiler/src/core/pretty.rs index 0b53b0d..17546a9 100644 --- a/compiler/src/core/pretty.rs +++ b/compiler/src/core/pretty.rs @@ -13,13 +13,13 @@ fn write_indent(f: &mut fmt::Formatter<'_>, depth: usize) -> fmt::Result { // ── Core formatting ─────────────────────────────────────────────────────────── -impl<'n> Term<'n, '_> { +impl<'names> Term<'names, '_> { /// Print `self` in **statement position**: emits leading indentation, then /// the term content. `Let` and `Match` are printed without an enclosing `{ }` /// (the caller is responsible for any surrounding braces). fn fmt_term( &self, - env: &mut Vec<&'n Name>, + env: &mut Vec<&'names Name>, indent: usize, f: &mut fmt::Formatter<'_>, ) -> fmt::Result { @@ -41,7 +41,7 @@ impl<'n> Term<'n, '_> { /// a new indented block (e.g. `Let` / `Match`). fn fmt_term_inline( &self, - env: &mut Vec<&'n Name>, + env: &mut Vec<&'names Name>, indent: usize, f: &mut fmt::Formatter<'_>, ) -> fmt::Result { @@ -171,7 +171,7 @@ impl<'n> Term<'n, '_> { /// syntactically valid as sub-expressions. fn fmt_expr( &self, - env: &mut Vec<&'n Name>, + env: &mut Vec<&'names Name>, indent: usize, f: &mut fmt::Formatter<'_>, ) -> fmt::Result { @@ -197,11 +197,11 @@ impl<'n> Term<'n, '_> { } } -impl<'n> Arm<'n, '_> { +impl<'names> Arm<'names, '_> { /// Print a single match arm. fn fmt_arm( &self, - env: &mut Vec<&'n Name>, + env: &mut Vec<&'names Name>, indent: usize, f: &mut fmt::Formatter<'_>, ) -> fmt::Result { diff --git a/compiler/src/core/value.rs b/compiler/src/core/value.rs index 87e0fe4..6ef6a2c 100644 --- a/compiler/src/core/value.rs +++ b/compiler/src/core/value.rs @@ -12,15 +12,15 @@ use crate::common::{de_bruijn, Phase}; /// Working evaluation environment: index 0 = outermost binding, last = innermost. /// `Var(Ix(i))` maps to `env[env.len() - 1 - i]`. -pub type Env<'n, 'a> = Vec>; +pub type Env<'names, 'a> = Vec>; /// Semantic value — result of evaluating a term or type. #[derive(Clone, Debug)] -pub enum Value<'n, 'a> { +pub enum Value<'names, 'a> { /// Neutral: stuck on a local variable (identified by De Bruijn level) Rigid(de_bruijn::Lvl), /// Neutral: global function reference (not inlined during type-checking) - Global(&'n Name), + Global(&'names Name), /// Neutral: unapplied or partially applied primitive Prim(Prim), /// Neutral: stuck application (callee cannot reduce further) @@ -28,9 +28,9 @@ pub enum Value<'n, 'a> { /// Canonical: integer literal value Lit(u64, IntType), /// Canonical: lambda abstraction - Lam(VLam<'n, 'a>), + Lam(VLam<'names, 'a>), /// Canonical: dependent function type - Pi(VPi<'n, 'a>), + Pi(VPi<'names, 'a>), /// Canonical: lifted object type `[[T]]` Lift(&'a Self), /// Canonical: quoted object code `#(t)` @@ -46,9 +46,9 @@ pub enum Value<'n, 'a> { /// type of the i-th parameter (supporting dependent telescopes). /// `closure` takes all `params.len()` arguments. #[derive(Clone, Debug)] -pub struct VLam<'n, 'a> { - pub params: &'a [(&'n Name, Closure<'n, 'a>)], - pub closure: Closure<'n, 'a>, +pub struct VLam<'names, 'a> { + pub params: &'a [(&'names Name, Closure<'names, 'a>)], + pub closure: Closure<'names, 'a>, } /// Pi (dependent function type) value. @@ -56,29 +56,29 @@ pub struct VLam<'n, 'a> { /// Same telescope layout as `VLam`: `params[i].1` is instantiated with `args[0..i]` /// to yield the domain of the i-th parameter. `ret_closure` takes all `params.len()` args. #[derive(Clone, Debug)] -pub struct VPi<'n, 'a> { - pub params: &'a [(&'n Name, Closure<'n, 'a>)], - pub ret_closure: Closure<'n, 'a>, +pub struct VPi<'names, 'a> { + pub params: &'a [(&'names Name, Closure<'names, 'a>)], + pub ret_closure: Closure<'names, 'a>, pub phase: Phase, } /// A closure: snapshot of the environment at creation time, plus an unevaluated body. #[derive(Clone, Debug)] -pub struct Closure<'n, 'a> { +pub struct Closure<'names, 'a> { /// Arena-allocated environment snapshot (index 0 = outermost). - pub env: &'a [Value<'n, 'a>], + pub env: &'a [Value<'names, 'a>], /// Unevaluated body term. - pub body: &'a Term<'n, 'a>, + pub body: &'a Term<'names, 'a>, } /// Evaluate a term in an environment, producing a semantic value. /// /// `env[env.len() - 1 - ix]` gives the value for `Var(Ix(ix))`. -pub fn eval<'n, 'a>( +pub fn eval<'names, 'a>( arena: &'a Bump, - env: &[Value<'n, 'a>], - term: &'a Term<'n, 'a>, -) -> Value<'n, 'a> { + env: &[Value<'names, 'a>], + term: &'a Term<'names, 'a>, +) -> Value<'names, 'a> { match term { Term::Var(ix) => { let lvl = ix.lvl_at(de_bruijn::Depth::new(env.len())); @@ -97,7 +97,7 @@ pub fn eval<'n, 'a>( Term::App(app) => { let func_val = eval(arena, env, app.func); - let arg_vals: Vec> = + let arg_vals: Vec> = app.args.iter().map(|a| eval(arena, env, a)).collect(); apply_many(arena, func_val, &arg_vals) } @@ -125,7 +125,7 @@ pub fn eval<'n, 'a>( Term::Let(let_) => { let val = eval(arena, env, let_.expr); - let mut env2: Vec> = env.to_vec(); + let mut env2: Vec> = env.to_vec(); env2.push(val); eval(arena, &env2, let_.body) } @@ -170,13 +170,13 @@ pub fn eval<'n, 'a>( /// All parameter domain closures share the same base environment snapshot. /// Each domain closure's body uses De Bruijn indices to reference preceding /// parameters, so they are correctly differentiated despite sharing the base env. -pub fn eval_pi<'n, 'a>( +pub fn eval_pi<'names, 'a>( arena: &'a Bump, - env: &[Value<'n, 'a>], - pi: &'a Pi<'n, 'a>, -) -> Value<'n, 'a> { + env: &[Value<'names, 'a>], + pi: &'a Pi<'names, 'a>, +) -> Value<'names, 'a> { let env_snapshot = arena.alloc_slice_fill_iter(env.iter().cloned()); - let params: Vec<(&'n Name, Closure<'n, 'a>)> = pi + let params: Vec<(&'names Name, Closure<'names, 'a>)> = pi .params .iter() .map(|&(name, ty_term)| { @@ -200,9 +200,9 @@ pub fn eval_pi<'n, 'a>( } /// Evaluate a multi-param Lam into a multi-param `Value::Lam` (no currying). -fn eval_lam<'n, 'a>(arena: &'a Bump, env: &[Value<'n, 'a>], lam: &'a Lam<'n, 'a>) -> Value<'n, 'a> { +fn eval_lam<'names, 'a>(arena: &'a Bump, env: &[Value<'names, 'a>], lam: &'a Lam<'names, 'a>) -> Value<'names, 'a> { let env_snapshot = arena.alloc_slice_fill_iter(env.iter().cloned()); - let params: Vec<(&'n Name, Closure<'n, 'a>)> = lam + let params: Vec<(&'names Name, Closure<'names, 'a>)> = lam .params .iter() .map(|&(name, ty_term)| { @@ -229,11 +229,11 @@ fn eval_lam<'n, 'a>(arena: &'a Bump, env: &[Value<'n, 'a>], lam: &'a Lam<'n, 'a> /// For `Value::Lam` and `Value::Pi`, all args are pushed into the closure env at once. /// For neutrals, a stuck `App` node is produced. Each call site is its own `App` node; /// args are NOT flattened into existing `App` nodes to preserve call-site identity. -pub fn apply_many<'n, 'a>( +pub fn apply_many<'names, 'a>( arena: &'a Bump, - func: Value<'n, 'a>, - args: &[Value<'n, 'a>], -) -> Value<'n, 'a> { + func: Value<'names, 'a>, + args: &[Value<'names, 'a>], +) -> Value<'names, 'a> { match func { Value::Lam(vlam) => inst_n(arena, &vlam.closure, args), Value::Pi(vpi) => inst_n(arena, &vpi.ret_closure, args), @@ -262,11 +262,11 @@ pub fn apply_many<'n, 'a>( } /// Instantiate a closure with N arguments: extend env with all args, eval body. -pub fn inst_n<'n, 'a>( +pub fn inst_n<'names, 'a>( arena: &'a Bump, - closure: &Closure<'n, 'a>, - args: &[Value<'n, 'a>], -) -> Value<'n, 'a> { + closure: &Closure<'names, 'a>, + args: &[Value<'names, 'a>], +) -> Value<'names, 'a> { let mut env = closure.env.to_vec(); env.extend_from_slice(args); eval(arena, &env, closure.body) @@ -274,14 +274,14 @@ pub fn inst_n<'n, 'a>( /// Quote a telescope (sequence of named parameters with closures). /// Returns the quoted parameters, final depth, and the rigid values built during the process. -fn quote_telescope<'n, 'a>( +fn quote_telescope<'names, 'a>( arena: &'a Bump, initial_depth: de_bruijn::Depth, - params: &[(&'n Name, Closure<'n, 'a>)], + params: &[(&'names Name, Closure<'names, 'a>)], ) -> ( - Vec<(&'n Name, &'a Term<'n, 'a>)>, + Vec<(&'names Name, &'a Term<'names, 'a>)>, de_bruijn::Depth, - Vec>, + Vec>, ) { let mut rigid_vals = Vec::new(); let mut quoted_params = Vec::new(); @@ -301,11 +301,11 @@ fn quote_telescope<'n, 'a>( /// Convert a value back to a term (for error reporting and definitional equality). /// /// `depth` is the current De Bruijn depth (number of locally-bound variables in scope). -pub fn quote<'n, 'a>( +pub fn quote<'names, 'a>( arena: &'a Bump, depth: de_bruijn::Depth, - val: &Value<'n, 'a>, -) -> &'a Term<'n, 'a> { + val: &Value<'names, 'a>, +) -> &'a Term<'names, 'a> { match val { Value::Rigid(lvl) => { let ix = lvl.ix_at(depth); @@ -316,7 +316,7 @@ pub fn quote<'n, 'a>( Value::Lit(n, it) => arena.alloc(Term::Lit(*n, *it)), Value::App(f, args) => { let qf = quote(arena, depth, f); - let qargs: Vec<&'a Term<'n, 'a>> = args + let qargs: Vec<&'a Term<'names, 'a>> = args .iter() .map(|a| quote(arena, depth, a) as &'a _) .collect(); @@ -359,11 +359,11 @@ pub fn quote<'n, 'a>( } /// Definitional equality: quote both values and compare structurally. -pub fn val_eq<'n, 'a>( +pub fn val_eq<'names, 'a>( arena: &'a Bump, depth: de_bruijn::Depth, - a: &Value<'n, 'a>, - b: &Value<'n, 'a>, + a: &Value<'names, 'a>, + b: &Value<'names, 'a>, ) -> bool { let ta = quote(arena, depth, a); let tb = quote(arena, depth, b); @@ -371,7 +371,7 @@ pub fn val_eq<'n, 'a>( } /// Evaluate a term in the empty environment. -pub fn eval_closed<'n, 'a>(arena: &'a Bump, term: &'a Term<'n, 'a>) -> Value<'n, 'a> { +pub fn eval_closed<'names, 'a>(arena: &'a Bump, term: &'a Term<'names, 'a>) -> Value<'names, 'a> { eval(arena, &[], term) } diff --git a/compiler/src/lexer/mod.rs b/compiler/src/lexer/mod.rs index f00d396..6b6609e 100644 --- a/compiler/src/lexer/mod.rs +++ b/compiler/src/lexer/mod.rs @@ -7,13 +7,13 @@ pub use token::Token; pub mod testutils; mod token; -pub struct Lexer<'a> { - input: &'a str, - names: &'a bumpalo::Bump, +pub struct Lexer<'names> { + input: &'names str, + names: &'names bumpalo::Bump, } -impl<'a> Lexer<'a> { - pub const fn new(input: &'a str, names: &'a bumpalo::Bump) -> Self { +impl<'names> Lexer<'names> { + pub const fn new(input: &'names str, names: &'names bumpalo::Bump) -> Self { Self { input, names } } @@ -34,7 +34,7 @@ impl<'a> Lexer<'a> { } } - fn split_pred bool>(&mut self, pred: F) -> &'a str { + fn split_pred bool>(&mut self, pred: F) -> &'names str { let len = self.input.find(pred).unwrap_or(self.input.len()); let (token, rest) = self.input.split_at(len); self.input = rest; @@ -45,12 +45,12 @@ impl<'a> Lexer<'a> { c.is_ascii_alphanumeric() || c == '_' } - fn read_number(&mut self) -> Result> { + fn read_number(&mut self) -> Result> { let num_str = self.split_pred(|c| !c.is_ascii_digit()); Ok(Token::Num(num_str.parse()?)) } - fn read_ident(&mut self) -> Token<'a> { + fn read_ident(&mut self) -> Token<'names> { let ident = self.split_pred(|c| !Self::is_ident_char(c)); Token::KEYWORDS .iter() @@ -59,7 +59,7 @@ impl<'a> Lexer<'a> { } #[inline] - fn read_token_impl(&mut self) -> Option>> { + fn read_token_impl(&mut self) -> Option>> { let c = self.input.chars().next()?; // Try matching symbols (longer first due to table order) @@ -84,7 +84,7 @@ impl<'a> Lexer<'a> { } #[inline] - fn read_token(&mut self) -> Option>> { + fn read_token(&mut self) -> Option>> { let orig_len = self.input.len(); let result = self.read_token_impl(); assert!( @@ -95,16 +95,16 @@ impl<'a> Lexer<'a> { } #[inline] - fn next(&mut self) -> Option>> { + fn next(&mut self) -> Option>> { self.skip_whitespace(); self.read_token() } } -impl<'a> Iterator for Lexer<'a> { - type Item = Result>; +impl<'names> Iterator for Lexer<'names> { + type Item = Result>; - fn next(&mut self) -> Option>> { + fn next(&mut self) -> Option>> { self.next() } } diff --git a/compiler/src/lexer/token.rs b/compiler/src/lexer/token.rs index 33492ac..3081863 100644 --- a/compiler/src/lexer/token.rs +++ b/compiler/src/lexer/token.rs @@ -1,7 +1,7 @@ use crate::common::Name; #[derive(Clone, Copy, Debug, PartialEq, Eq)] -pub enum Token<'a> { +pub enum Token<'names> { Fn, Code, Let, @@ -38,7 +38,7 @@ pub enum Token<'a> { DoubleRBracket, DArrow, Num(u64), - Ident(&'a Name), + Ident(&'names Name), } impl Token<'static> { diff --git a/compiler/src/parser/ast.rs b/compiler/src/parser/ast.rs index 32daa93..0e07656 100644 --- a/compiler/src/parser/ast.rs +++ b/compiler/src/parser/ast.rs @@ -2,9 +2,9 @@ pub use crate::common::{Assoc, BinOp, Name, Phase, UnOp}; /// Function or operator reference #[derive(Clone, Copy, derive_more::Debug)] -pub enum FunName<'n, 'a> { +pub enum FunName<'names, 'ast> { #[debug("{_0:?}")] - Term(&'a Term<'n, 'a>), + Term(&'ast Term<'names, 'ast>), #[debug("{_0:?}")] BinOp(BinOp), #[debug("{_0:?}")] @@ -12,84 +12,84 @@ pub enum FunName<'n, 'a> { } #[derive(derive_more::Debug)] -pub enum Pat<'n> { +pub enum Pat<'names> { #[debug("{_0:?}")] - Name(&'n Name), + Name(&'names Name), #[debug("{_0:?}")] Lit(u64), } #[derive(Debug)] -pub struct MatchArm<'n, 'a> { - pub pat: Pat<'n>, - pub body: &'a Term<'n, 'a>, +pub struct MatchArm<'names, 'ast> { + pub pat: Pat<'names>, + pub body: &'ast Term<'names, 'ast>, } #[derive(Debug)] -pub struct Let<'n, 'a> { - pub name: &'n Name, - pub ty: Option<&'a Term<'n, 'a>>, - pub expr: &'a Term<'n, 'a>, +pub struct Let<'names, 'ast> { + pub name: &'names Name, + pub ty: Option<&'ast Term<'names, 'ast>>, + pub expr: &'ast Term<'names, 'ast>, } #[derive(Debug)] -pub struct Param<'n, 'a> { - pub name: &'n Name, - pub ty: &'a Term<'n, 'a>, +pub struct Param<'names, 'ast> { + pub name: &'names Name, + pub ty: &'ast Term<'names, 'ast>, } #[derive(Debug)] -pub struct Function<'n, 'a> { +pub struct Function<'names, 'ast> { pub phase: Phase, - pub name: &'n Name, - pub params: &'a [Param<'n, 'a>], - pub ret_ty: &'a Term<'n, 'a>, - pub body: &'a Term<'n, 'a>, + pub name: &'names Name, + pub params: &'ast [Param<'names, 'ast>], + pub ret_ty: &'ast Term<'names, 'ast>, + pub body: &'ast Term<'names, 'ast>, } #[derive(Debug)] -pub struct Program<'n, 'a> { - pub functions: &'a [Function<'n, 'a>], +pub struct Program<'names, 'ast> { + pub functions: &'ast [Function<'names, 'ast>], } #[derive(derive_more::Debug)] -pub enum Term<'n, 'a> { +pub enum Term<'names, 'ast> { #[debug("{_0:?}")] Lit(u64), #[debug("{_0:?}")] - Var(&'n Name), + Var(&'names Name), App { - func: FunName<'n, 'a>, - args: &'a [&'a Self], + func: FunName<'names, 'ast>, + args: &'ast [&'ast Self], }, /// Function type: `fn(name: ty, ...) -> ret_ty` Pi { - params: &'a [Param<'n, 'a>], - ret_ty: &'a Self, + params: &'ast [Param<'names, 'ast>], + ret_ty: &'ast Self, }, /// Lambda: `|params| body` Lam { - params: &'a [Param<'n, 'a>], - body: &'a Self, + params: &'ast [Param<'names, 'ast>], + body: &'ast Self, }, - Quote(&'a Self), + Quote(&'ast Self), - Splice(&'a Self), + Splice(&'ast Self), - Lift(&'a Self), + Lift(&'ast Self), Match { - scrutinee: &'a Self, - arms: &'a [MatchArm<'n, 'a>], + scrutinee: &'ast Self, + arms: &'ast [MatchArm<'names, 'ast>], }, Block { - stmts: &'a [Let<'n, 'a>], - expr: &'a Self, + stmts: &'ast [Let<'names, 'ast>], + expr: &'ast Self, }, } diff --git a/compiler/src/parser/mod.rs b/compiler/src/parser/mod.rs index 423482c..497851f 100644 --- a/compiler/src/parser/mod.rs +++ b/compiler/src/parser/mod.rs @@ -10,35 +10,35 @@ use crate::parser::ast::{ pub mod ast; -pub struct Parser<'n, 'a, I> +pub struct Parser<'names, 'ast, I> where - I: Iterator>>, + I: Iterator>>, { tokens: Peekable, - arena: &'a bumpalo::Bump, + arena: &'ast bumpalo::Bump, } -impl<'n, 'a, I> Parser<'n, 'a, I> +impl<'names, 'ast, I> Parser<'names, 'ast, I> where - I: Iterator>>, + I: Iterator>>, { - pub fn new(tokens: I, arena: &'a bumpalo::Bump) -> Self { + pub fn new(tokens: I, arena: &'ast bumpalo::Bump) -> Self { let tokens = tokens.peekable(); Self { tokens, arena } } - fn peek(&mut self) -> Option> { + fn peek(&mut self) -> Option> { self.tokens.peek().and_then(|r| r.as_ref().ok().copied()) } - fn next(&mut self) -> Option>> { + fn next(&mut self) -> Option>> { self.tokens.next() } /// Helper for extracting a token with a custom validation closure fn expect_token(&mut self, description: &str, f: F) -> Result where - F: FnOnce(Token<'n>) -> Option, + F: FnOnce(Token<'names>) -> Option, { match self.next() { Some(Ok(token)) => { @@ -49,13 +49,13 @@ where } } - fn take(&mut self, expected: Token<'n>) -> Result> { + fn take(&mut self, expected: Token<'names>) -> Result> { self.expect_token(&format!("{expected:?}"), |token| { (token == expected).then_some(token) }) } - fn take_ident(&mut self) -> Result<&'n Name> { + fn take_ident(&mut self) -> Result<&'names Name> { self.expect_token("identifier", |token| { if let Token::Ident(name) = token { Some(name) @@ -66,7 +66,7 @@ where } /// Consume a token if it matches the expected token - fn consume_if(&mut self, token: Token<'n>) -> bool { + fn consume_if(&mut self, token: Token<'names>) -> bool { if matches!(self.peek(), Some(t) if t == token) { self.next(); true @@ -76,12 +76,12 @@ where } /// Allocate a term and return a reference to it - fn alloc(&self, term: Term<'n, 'a>) -> &'a Term<'n, 'a> { + fn alloc(&self, term: Term<'names, 'ast>) -> &'ast Term<'names, 'ast> { &*self.arena.alloc(term) } /// Parse a quoted expression: #(...) - fn parse_quoted_expr(&mut self) -> Result> { + fn parse_quoted_expr(&mut self) -> Result> { let expr = self.parse_expr().context("parsing quoted expression")?; self.take(Token::RParen) .context("expected ')' after quotation")?; @@ -89,13 +89,13 @@ where } /// Parse a quoted block: #{...} - fn parse_quoted_block(&mut self) -> Result> { + fn parse_quoted_block(&mut self) -> Result> { let (stmts, expr) = self.parse_block_inner()?; Ok(Term::Quote(self.alloc(Term::Block { stmts, expr }))) } /// Parse a spliced expression: $(...) - fn parse_spliced_expr(&mut self) -> Result> { + fn parse_spliced_expr(&mut self) -> Result> { let expr = self.parse_expr().context("parsing spliced expression")?; self.take(Token::RParen) .context("expected ')' after splice")?; @@ -103,13 +103,13 @@ where } /// Parse a spliced block: ${...} - fn parse_spliced_block(&mut self) -> Result> { + fn parse_spliced_block(&mut self) -> Result> { let (stmts, expr) = self.parse_block_inner()?; Ok(Term::Splice(self.alloc(Term::Block { stmts, expr }))) } /// Parse a lifted expression: [[...]] - fn parse_lifted_expr(&mut self) -> Result> { + fn parse_lifted_expr(&mut self) -> Result> { let expr = self.parse_expr().context("parsing lifted expression")?; self.take(Token::DoubleRBracket) .context("expected ']]' after lifted expression")?; @@ -117,7 +117,7 @@ where } /// Parse a comma-separated list of items bounded by a terminator token - fn parse_separated_list(&mut self, terminator: Token<'n>, mut parser: F) -> Result> + fn parse_separated_list(&mut self, terminator: Token<'names>, mut parser: F) -> Result> where F: FnMut(&mut Self) -> Result, { @@ -134,7 +134,7 @@ where Ok(items) } - pub fn parse_program(&mut self) -> Result> { + pub fn parse_program(&mut self) -> Result> { let mut functions = Vec::new(); while self.peek().is_some() { let fun = self.parse_fn_def()?; @@ -144,7 +144,7 @@ where Ok(Program { functions }) } - fn parse_fn_def(&mut self) -> Result> { + fn parse_fn_def(&mut self) -> Result> { let phase = if self.consume_if(Token::Code) { Phase::Object } else { @@ -161,8 +161,8 @@ where fn parse_fn_def_after_name( &mut self, phase: Phase, - name: &'n Name, - ) -> Result> { + name: &'names Name, + ) -> Result> { self.take(Token::LParen).context("expected '('")?; let params = self.parse_params()?; self.take(Token::RParen).context("expected ')'")?; @@ -184,7 +184,7 @@ where }) } - fn parse_params(&mut self) -> Result<&'a [Param<'n, 'a>]> { + fn parse_params(&mut self) -> Result<&'ast [Param<'names, 'ast>]> { let params = self.parse_separated_list(Token::RParen, |parser| { let name = parser.take_ident().context("expected parameter name")?; parser @@ -197,13 +197,13 @@ where Ok(self.arena.alloc_slice_fill_iter(params)) } - fn parse_block(&mut self) -> Result<&'a Term<'n, 'a>> { + fn parse_block(&mut self) -> Result<&'ast Term<'names, 'ast>> { self.take(Token::LBrace).context("expected '{'")?; let (stmts, expr) = self.parse_block_inner()?; Ok(self.alloc(Term::Block { stmts, expr })) } - fn parse_block_inner(&mut self) -> Result<(&'a [Let<'n, 'a>], &'a Term<'n, 'a>)> { + fn parse_block_inner(&mut self) -> Result<(&'ast [Let<'names, 'ast>], &'ast Term<'names, 'ast>)> { let mut stmts = Vec::new(); while self.peek() == Some(Token::Let) { @@ -218,7 +218,7 @@ where Ok((stmts, expr)) } - fn parse_let_stmt(&mut self) -> Result> { + fn parse_let_stmt(&mut self) -> Result> { self.take(Token::Let).context("expected 'let'")?; let name = self.take_ident().context("expected variable name")?; let ty = if self.consume_if(Token::Colon) { @@ -236,15 +236,15 @@ where Ok(Let { name, ty, expr }) } - fn parse_expr(&mut self) -> Result<&'a Term<'n, 'a>> { + fn parse_expr(&mut self) -> Result<&'ast Term<'names, 'ast>> { Ok(self.arena.alloc(self.parse_expr_owned()?)) } - fn parse_expr_owned(&mut self) -> Result> { + fn parse_expr_owned(&mut self) -> Result> { self.parse_expr_prec(Precedence::MIN) } - fn parse_expr_prec(&mut self, min_prec: Precedence) -> Result> { + fn parse_expr_prec(&mut self, min_prec: Precedence) -> Result> { let mut lhs = if let Some(op) = self.match_unop() { self.next(); let expr = self @@ -337,7 +337,7 @@ where } /// Parse a function call with arguments - fn parse_function_call(&mut self, name: &'n Name) -> Result> { + fn parse_function_call(&mut self, name: &'names Name) -> Result> { let args = self.parse_separated_list(Token::RParen, |parser| { parser.parse_expr().context("parsing function argument") })?; @@ -351,7 +351,7 @@ where } /// Parse a parenthesized expression - fn parse_paren_expr(&mut self) -> Result> { + fn parse_paren_expr(&mut self) -> Result> { let expr = self .parse_expr_owned() .context("parsing expression in parentheses")?; @@ -361,7 +361,7 @@ where } /// Parse a match expression - fn parse_match_expr(&mut self) -> Result> { + fn parse_match_expr(&mut self) -> Result> { let scrutinee = self.parse_expr().context("parsing match scrutinee")?; self.take(Token::LBrace) .context("expected '{' after match expression")?; @@ -375,7 +375,7 @@ where /// Parse a function type: `fn(params) -> ret_ty` /// /// Called after consuming the `fn` token. Each param is `name: type`. - fn parse_fn_type(&mut self) -> Result> { + fn parse_fn_type(&mut self) -> Result> { self.take(Token::LParen) .context("expected '(' in function type")?; let params = self.parse_params()?; @@ -392,7 +392,7 @@ where /// Parse a lambda expression: `|params| body` /// /// Called after consuming the `|` token. Each param is `name: type`. - fn parse_lambda(&mut self) -> Result> { + fn parse_lambda(&mut self) -> Result> { let params_vec = self.parse_separated_list(Token::Bar, |parser| { let name = parser .take_ident() @@ -419,7 +419,7 @@ where clippy::wildcard_enum_match_arm, reason = "unrecognised tokens are intentionally caught by the wildcard arm" )] - fn parse_atom_owned(&mut self) -> Result> { + fn parse_atom_owned(&mut self) -> Result> { let token = self.next().context("expected expression")??; match token { Token::Num(n) => Ok(Term::Lit(n)), @@ -449,7 +449,7 @@ where } } - fn parse_match_arms(&mut self) -> Result>> { + fn parse_match_arms(&mut self) -> Result>> { let mut arms = Vec::new(); while self.peek().is_some() && !matches!(self.peek(), Some(Token::RBrace)) { let pat = self.parse_pattern().context("parsing match pattern")?; @@ -469,7 +469,7 @@ where clippy::wildcard_enum_match_arm, reason = "unrecognised tokens are intentionally caught by the wildcard arm" )] - fn parse_pattern(&mut self) -> Result> { + fn parse_pattern(&mut self) -> Result> { let token = self.next().context("expected pattern")??; match token { Token::Num(n) => Ok(Pat::Lit(n)), diff --git a/compiler/src/staging/mod.rs b/compiler/src/staging/mod.rs index c209142..cd4376b 100644 --- a/compiler/src/staging/mod.rs +++ b/compiler/src/staging/mod.rs @@ -19,7 +19,7 @@ use crate::parser::ast::Phase; /// forbidden in Splic (the type-checker enforces this); `eval_obj` eagerly /// evaluates under binders by extending the environment with fresh level variables. #[derive(Clone, Debug)] -enum ObjVal<'n, 'a> { +enum ObjVal<'names, 'eval> { /// Local variable identified by De Bruijn level (absolute, context-independent). Var(de_bruijn::Lvl), /// Integer literal. @@ -27,27 +27,27 @@ enum ObjVal<'n, 'a> { /// Unapplied primitive. Prim(Prim), /// Global function reference. - Global(&'n Name), + Global(&'names Name), /// Application. - App(&'a Self, &'a [Self]), + App(&'eval Self, &'eval [Self]), /// Let binding. Let { - name: &'n Name, - ty: &'a Self, - expr: &'a Self, - body: &'a Self, + name: &'names Name, + ty: &'eval Self, + expr: &'eval Self, + body: &'eval Self, }, /// Pattern match. Match { - scrutinee: &'a Self, - arms: &'a [ObjArm<'n, 'a>], + scrutinee: &'eval Self, + arms: &'eval [ObjArm<'names, 'eval>], }, } #[derive(Clone, Debug)] -struct ObjArm<'n, 'a> { - pat: Pat<'n>, - body: &'a ObjVal<'n, 'a>, +struct ObjArm<'names, 'eval> { + pat: Pat<'names>, + body: &'eval ObjVal<'names, 'eval>, } // ── Meta-level values ───────────────────────────────────────────────────────── @@ -147,12 +147,12 @@ impl<'names, 'eval> Env<'names, 'eval> { // ── Globals table ───────────────────────────────────────────────────────────── /// Everything the evaluator needs to know about a top-level function. -struct GlobalDef<'n, 'a> { - ty: &'a Pi<'n, 'a>, - body: &'a Term<'n, 'a>, +struct GlobalDef<'names, 'a> { + ty: &'a Pi<'names, 'a>, + body: &'a Term<'names, 'a>, } -type Globals<'n, 'a> = HashMap<&'n Name, GlobalDef<'n, 'a>>; +type Globals<'names, 'a> = HashMap<&'names Name, GlobalDef<'names, 'a>>; // ── Meta-level evaluator ────────────────────────────────────────────────────── From 7fbb1647f618d1cfd6cce7504301d676c5fa5fd8 Mon Sep 17 00:00:00 2001 From: LukasK Date: Mon, 6 Apr 2026 08:24:07 +0000 Subject: [PATCH 3/6] chore: fmt --- compiler/src/checker/elaborate.rs | 4 +- compiler/src/checker/infer.rs | 75 +++++++++++++++++-------------- compiler/src/checker/test/mod.rs | 2 +- compiler/src/core/mod.rs | 2 +- compiler/src/core/value.rs | 8 +++- compiler/src/lexer/mod.rs | 8 ++-- compiler/src/parser/mod.rs | 10 ++++- 7 files changed, 63 insertions(+), 46 deletions(-) diff --git a/compiler/src/checker/elaborate.rs b/compiler/src/checker/elaborate.rs index e0665f3..55507f1 100644 --- a/compiler/src/checker/elaborate.rs +++ b/compiler/src/checker/elaborate.rs @@ -16,8 +16,8 @@ fn elaborate_sig<'names, 'ast, 'core>( let empty_globals: HashMap<&'names core::Name, &'core core::Pi<'names, 'core>> = HashMap::new(); let mut ctx = Ctx::new(arena, &empty_globals); - let params: &'core [(&'names core::Name, &'core core::Term<'names, 'core>)] = - arena.alloc_slice_try_fill_iter(func.params.iter().map(|p| -> Result<_> { + let params: &'core [(&'names core::Name, &'core core::Term<'names, 'core>)] = arena + .alloc_slice_try_fill_iter(func.params.iter().map(|p| -> Result<_> { let (param_ty, _) = infer::infer(&mut ctx, func.phase, p.ty)?; ctx.push_local(p.name, param_ty); Ok((p.name, param_ty)) diff --git a/compiler/src/checker/infer.rs b/compiler/src/checker/infer.rs index 3d45282..7461ac2 100644 --- a/compiler/src/checker/infer.rs +++ b/compiler/src/checker/infer.rs @@ -1,10 +1,10 @@ -use anyhow::{anyhow, bail, ensure, Context as _, Result}; +use anyhow::{Context as _, Result, anyhow, bail, ensure}; use crate::common::de_bruijn; -use crate::core::{self, value, IntType, IntWidth, Lam, Phase, Pi, Prim}; +use crate::core::{self, IntType, IntWidth, Lam, Phase, Pi, Prim, value}; use crate::parser::ast; -use super::{builtin_prim_ty, Ctx}; +use super::{Ctx, builtin_prim_ty}; /// Infer the type of a surface term, returning both the elaborated core term /// and its type as a semantic value. @@ -16,7 +16,10 @@ pub fn infer<'names, 'ast, 'core>( ctx: &mut Ctx<'names, 'core, '_>, phase: Phase, term: &'ast ast::Term<'names, 'ast>, -) -> Result<(&'core core::Term<'names, 'core>, value::Value<'names, 'core>)> { +) -> Result<( + &'core core::Term<'names, 'core>, + value::Value<'names, 'core>, +)> { match term { // ------------------------------------------------------------------ Var ast::Term::Var(name) => { @@ -90,7 +93,8 @@ pub fn infer<'names, 'ast, 'core>( // Check each arg against its domain (evaluated with prior arg values). let mut arg_vals: Vec> = Vec::with_capacity(args.len()); - let mut core_args: Vec<&'core core::Term<'names, 'core>> = Vec::with_capacity(args.len()); + let mut core_args: Vec<&'core core::Term<'names, 'core>> = + Vec::with_capacity(args.len()); for (i, (arg, (_, domain_cl))) in args.iter().zip(vpi.params.iter()).enumerate() { let domain_val = value::inst_n(ctx.arena, domain_cl, &arg_vals); let core_arg = check_val(ctx, phase, arg, domain_val) @@ -425,7 +429,10 @@ fn infer_block<'names, 'ast, 'core>( phase: Phase, stmts: &'ast [ast::Let<'names, 'ast>], expr: &'ast ast::Term<'names, 'ast>, -) -> Result<(&'core core::Term<'names, 'core>, value::Value<'names, 'core>)> { +) -> Result<( + &'core core::Term<'names, 'core>, + value::Value<'names, 'core>, +)> { match stmts { [] => infer(ctx, phase, expr), [first, rest @ ..] => elaborate_let( @@ -719,38 +726,38 @@ fn check_val_impl<'names, 'ast, 'core>( _ => None, }; - let core_arms: &'core [core::Arm<'names, 'core>] = - ctx.arena - .alloc_slice_try_fill_iter(arms.iter().map(|arm| -> Result<_> { - let core_pat = elaborate_pat(&arm.pat); - - let arm_expected = match (&scrut_refine, &core_pat, expected_term) { - (Some((lvl, int_ty)), core::Pat::Lit(n), Some(ety)) => { - let mut env = ctx.env.clone(); - *env.get_mut(lvl.as_usize()) - .expect("scrutinee level must be in scope") = - value::Value::Lit(*n, *int_ty); - value::eval(ctx.arena, &env, ety) - } - _ => expected.clone(), - }; - - if let Some(bname) = core_pat.bound_name() { - ctx.push_local(bname, scrut_ty_term); + let core_arms: &'core [core::Arm<'names, 'core>] = ctx + .arena + .alloc_slice_try_fill_iter(arms.iter().map(|arm| -> Result<_> { + let core_pat = elaborate_pat(&arm.pat); + + let arm_expected = match (&scrut_refine, &core_pat, expected_term) { + (Some((lvl, int_ty)), core::Pat::Lit(n), Some(ety)) => { + let mut env = ctx.env.clone(); + *env.get_mut(lvl.as_usize()) + .expect("scrutinee level must be in scope") = + value::Value::Lit(*n, *int_ty); + value::eval(ctx.arena, &env, ety) } + _ => expected.clone(), + }; - let arm_result = check_val(ctx, phase, arm.body, arm_expected); + if let Some(bname) = core_pat.bound_name() { + ctx.push_local(bname, scrut_ty_term); + } - if core_pat.bound_name().is_some() { - ctx.pop_local(); - } + let arm_result = check_val(ctx, phase, arm.body, arm_expected); + + if core_pat.bound_name().is_some() { + ctx.pop_local(); + } - let core_body = arm_result?; - Ok(core::Arm { - pat: core_pat, - body: core_body, - }) - }))?; + let core_body = arm_result?; + Ok(core::Arm { + pat: core_pat, + body: core_body, + }) + }))?; Ok(ctx.alloc(core::Term::new_match(core_scrutinee, core_arms))) } diff --git a/compiler/src/checker/test/mod.rs b/compiler/src/checker/test/mod.rs index 576b158..20bc908 100644 --- a/compiler/src/checker/test/mod.rs +++ b/compiler/src/checker/test/mod.rs @@ -11,7 +11,7 @@ use std::collections::HashMap; use super::*; use crate::common::de_bruijn; -use crate::core::{self, value, IntType, IntWidth, Name, Pat, Pi, Prim}; +use crate::core::{self, IntType, IntWidth, Name, Pat, Pi, Prim, value}; use crate::parser::ast::{self, BinOp, FunName, MatchArm, Phase}; mod helpers; diff --git a/compiler/src/core/mod.rs b/compiler/src/core/mod.rs index 601a8e6..f7757e7 100644 --- a/compiler/src/core/mod.rs +++ b/compiler/src/core/mod.rs @@ -12,7 +12,7 @@ pub use prim::{IntType, IntWidth, Prim}; pub enum Pat<'names> { Lit(u64), Bind(&'names Name), // named binding - Wildcard, // _ pattern + Wildcard, // _ pattern } impl<'names> Pat<'names> { diff --git a/compiler/src/core/value.rs b/compiler/src/core/value.rs index 6ef6a2c..98c845e 100644 --- a/compiler/src/core/value.rs +++ b/compiler/src/core/value.rs @@ -8,7 +8,7 @@ use bumpalo::Bump; use super::prim::IntType; use super::{Lam, Name, Pat, Pi, Prim, Term}; -use crate::common::{de_bruijn, Phase}; +use crate::common::{Phase, de_bruijn}; /// Working evaluation environment: index 0 = outermost binding, last = innermost. /// `Var(Ix(i))` maps to `env[env.len() - 1 - i]`. @@ -200,7 +200,11 @@ pub fn eval_pi<'names, 'a>( } /// Evaluate a multi-param Lam into a multi-param `Value::Lam` (no currying). -fn eval_lam<'names, 'a>(arena: &'a Bump, env: &[Value<'names, 'a>], lam: &'a Lam<'names, 'a>) -> Value<'names, 'a> { +fn eval_lam<'names, 'a>( + arena: &'a Bump, + env: &[Value<'names, 'a>], + lam: &'a Lam<'names, 'a>, +) -> Value<'names, 'a> { let env_snapshot = arena.alloc_slice_fill_iter(env.iter().cloned()); let params: Vec<(&'names Name, Closure<'names, 'a>)> = lam .params diff --git a/compiler/src/lexer/mod.rs b/compiler/src/lexer/mod.rs index 6b6609e..39d9729 100644 --- a/compiler/src/lexer/mod.rs +++ b/compiler/src/lexer/mod.rs @@ -52,10 +52,10 @@ impl<'names> Lexer<'names> { fn read_ident(&mut self) -> Token<'names> { let ident = self.split_pred(|c| !Self::is_ident_char(c)); - Token::KEYWORDS - .iter() - .find(|(kw, _)| *kw == ident) - .map_or(Token::Ident(Name::new(self.names.alloc_str(ident))), |(_, tok)| *tok) + Token::KEYWORDS.iter().find(|(kw, _)| *kw == ident).map_or( + Token::Ident(Name::new(self.names.alloc_str(ident))), + |(_, tok)| *tok, + ) } #[inline] diff --git a/compiler/src/parser/mod.rs b/compiler/src/parser/mod.rs index 497851f..5690a1e 100644 --- a/compiler/src/parser/mod.rs +++ b/compiler/src/parser/mod.rs @@ -117,7 +117,11 @@ where } /// Parse a comma-separated list of items bounded by a terminator token - fn parse_separated_list(&mut self, terminator: Token<'names>, mut parser: F) -> Result> + fn parse_separated_list( + &mut self, + terminator: Token<'names>, + mut parser: F, + ) -> Result> where F: FnMut(&mut Self) -> Result, { @@ -203,7 +207,9 @@ where Ok(self.alloc(Term::Block { stmts, expr })) } - fn parse_block_inner(&mut self) -> Result<(&'ast [Let<'names, 'ast>], &'ast Term<'names, 'ast>)> { + fn parse_block_inner( + &mut self, + ) -> Result<(&'ast [Let<'names, 'ast>], &'ast Term<'names, 'ast>)> { let mut stmts = Vec::new(); while self.peek() == Some(Token::Let) { From ea011a3bef4f44b922706a37c1c8e086d6af6388 Mon Sep 17 00:00:00 2001 From: LukasK Date: Mon, 6 Apr 2026 08:24:38 +0000 Subject: [PATCH 4/6] chore: .gitignore --- .gitignore | 1 + 1 file changed, 1 insertion(+) diff --git a/.gitignore b/.gitignore index 623ef91..b2eaf88 100644 --- a/.gitignore +++ b/.gitignore @@ -4,3 +4,4 @@ scratch/ posts/ .claude/settings.local.json .claude/worktrees/ +.opencode/package-lock.json From 548f1f782bb09a762f4a2d3ef243995b43771e28 Mon Sep 17 00:00:00 2001 From: LukasK Date: Mon, 6 Apr 2026 08:28:13 +0000 Subject: [PATCH 5/6] refactor: split Lexer into two lifetimes and drop source text after parsing Lexer<'src, 'names> separates the source text lifetime from the names arena lifetime. The iterator now yields Token<'names>, making it clear that produced tokens outlive the source string. In the CLI pipeline, source is dropped immediately after parse_program returns, since all identifier strings are interned in names_arena. Co-Authored-By: Claude Sonnet 4.6 --- cli/src/main.rs | 1 + compiler/src/lexer/mod.rs | 12 ++++++------ 2 files changed, 7 insertions(+), 6 deletions(-) diff --git a/cli/src/main.rs b/cli/src/main.rs index 75ba50d..565a674 100644 --- a/cli/src/main.rs +++ b/cli/src/main.rs @@ -44,6 +44,7 @@ fn stage(file: &PathBuf) -> Result<()> { let lexer = lexer::Lexer::new(&source, &names_arena); let mut parser = parser::Parser::new(lexer, &ast_arena); let program = parser.parse_program().context("failed to parse program")?; + drop(source); // Elaborate/typecheck into core_arena; the arena lives until staging // finishes consuming the core IR, then is dropped. diff --git a/compiler/src/lexer/mod.rs b/compiler/src/lexer/mod.rs index 39d9729..eea709d 100644 --- a/compiler/src/lexer/mod.rs +++ b/compiler/src/lexer/mod.rs @@ -7,13 +7,13 @@ pub use token::Token; pub mod testutils; mod token; -pub struct Lexer<'names> { - input: &'names str, +pub struct Lexer<'src, 'names> { + input: &'src str, names: &'names bumpalo::Bump, } -impl<'names> Lexer<'names> { - pub const fn new(input: &'names str, names: &'names bumpalo::Bump) -> Self { +impl<'src, 'names> Lexer<'src, 'names> { + pub const fn new(input: &'src str, names: &'names bumpalo::Bump) -> Self { Self { input, names } } @@ -34,7 +34,7 @@ impl<'names> Lexer<'names> { } } - fn split_pred bool>(&mut self, pred: F) -> &'names str { + fn split_pred bool>(&mut self, pred: F) -> &'src str { let len = self.input.find(pred).unwrap_or(self.input.len()); let (token, rest) = self.input.split_at(len); self.input = rest; @@ -101,7 +101,7 @@ impl<'names> Lexer<'names> { } } -impl<'names> Iterator for Lexer<'names> { +impl<'names> Iterator for Lexer<'_, 'names> { type Item = Result>; fn next(&mut self) -> Option>> { From aff27f7d7a407dfef57c3fd10019b872d312c278 Mon Sep 17 00:00:00 2001 From: LukasK Date: Mon, 6 Apr 2026 10:18:13 +0000 Subject: [PATCH 6/6] refactor: inline redundant param_name variable in Pi and Lam elaboration Co-Authored-By: Claude Sonnet 4.6 --- compiler/src/checker/infer.rs | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) diff --git a/compiler/src/checker/infer.rs b/compiler/src/checker/infer.rs index 7461ac2..53264e2 100644 --- a/compiler/src/checker/infer.rs +++ b/compiler/src/checker/infer.rs @@ -184,10 +184,9 @@ pub fn infer<'names, 'ast, 'core>( let mut elaborated_params: Vec<(&'names core::Name, &'core core::Term<'names, 'core>)> = Vec::new(); for p in *params { - let param_name = p.name; let param_ty = check_universe(ctx, Phase::Meta, p.ty)?; - elaborated_params.push((param_name, param_ty)); - ctx.push_local(param_name, param_ty); + elaborated_params.push((p.name, param_ty)); + ctx.push_local(p.name, param_ty); } let core_ret_ty = check_universe(ctx, Phase::Meta, ret_ty)?; @@ -219,10 +218,9 @@ pub fn infer<'names, 'ast, 'core>( Vec::new(); for p in *params { - let param_name = p.name; let (param_ty, _) = infer(ctx, Phase::Meta, p.ty)?; - elaborated_params.push((param_name, param_ty)); - ctx.push_local(param_name, param_ty); + elaborated_params.push((p.name, param_ty)); + ctx.push_local(p.name, param_ty); } let (core_body, body_ty) = infer(ctx, phase, body)?;