diff --git a/Justfile b/Justfile index 74eea41..45f69b3 100644 --- a/Justfile +++ b/Justfile @@ -1,5 +1,5 @@ -// SPDX-License-Identifier: MPL-2.0 -// Copyright (c) Jonathan D.A. Jewell +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) Jonathan D.A. Jewell # betlang - Development Tasks # AUTHORITY: AUTHORITY_STACK.mustfile-nickel.scm # All operations MUST be invoked via `just `. @@ -84,6 +84,34 @@ test-tooling: clean-tooling: cargo clean +# --- Rust toolchain recipes (the working compiler/interpreter pipeline) ------ +# These drive the real multi-crate Rust implementation under compiler/, runtime/ +# and tools/. (The Racket recipes above target the historical core/*.rkt tree.) + +# Build the entire Rust workspace (all crates) +build-rust: + cargo build --workspace + +# Test the entire Rust workspace +test-rust: + cargo test --workspace + +# Type-check a betlang source file with the Rust checker +check FILE: + cargo run -q -p bet -- check {{FILE}} + +# Run a betlang source file with the Rust interpreter +run FILE: + cargo run -q -p bet -- run {{FILE}} + +# Compile a betlang source file to a backend (TARGET = js | llvm | beam) +compile FILE TARGET="js": + cargo run -q -p bet -- compile {{FILE}} --target {{TARGET}} + +# Start the Rust REPL +repl-rust: + cargo run -q -p bet -- repl + # ============================================================================ # PROOFS (formal verification — see docs/AFFINESCRIPT-ALIGNMENT.adoc) # ============================================================================ diff --git a/bindings/chapel/Cargo.toml b/bindings/chapel/Cargo.toml index 156b375..58cddcc 100644 --- a/bindings/chapel/Cargo.toml +++ b/bindings/chapel/Cargo.toml @@ -18,6 +18,7 @@ libc = "0.2" # Core rand.workspace = true rand_distr.workspace = true +rand_pcg.workspace = true # seedable PCG generator for `bet_seed` [build-dependencies] cbindgen = "0.28" diff --git a/bindings/chapel/build.rs b/bindings/chapel/build.rs index a1d3ee3..4483bd5 100644 --- a/bindings/chapel/build.rs +++ b/bindings/chapel/build.rs @@ -10,6 +10,15 @@ fn main() { .with_language(cbindgen::Language::C) .with_include_guard("BET_CHAPEL_H") .with_documentation(true) + // Preserve the SPDX/copyright header on the generated file. cbindgen + // overwrites include/betlang.h wholesale on every build; without this + // the licence header is silently stripped each time (an automated + // licence edit, which estate policy forbids — keep it manual & stable). + .with_header( + "// SPDX-License-Identifier: MPL-2.0\n\ + // Copyright (c) Jonathan D.A. Jewell \n\ + // GENERATED by cbindgen (build.rs) — do not edit by hand.", + ) .generate() .expect("Unable to generate bindings") .write_to_file("include/betlang.h"); diff --git a/bindings/chapel/include/betlang.h b/bindings/chapel/include/betlang.h index 4e4243a..7a2c338 100644 --- a/bindings/chapel/include/betlang.h +++ b/bindings/chapel/include/betlang.h @@ -1,5 +1,7 @@ // SPDX-License-Identifier: MPL-2.0 // Copyright (c) Jonathan D.A. Jewell +// GENERATED by cbindgen (build.rs) — do not edit by hand. + #ifndef BET_CHAPEL_H #define BET_CHAPEL_H @@ -143,4 +145,4 @@ void bet_seed(uint64_t seed); */ const char *bet_version(void); -#endif /* BET_CHAPEL_H */ +#endif /* BET_CHAPEL_H */ diff --git a/compiler/bet-check/src/lib.rs b/compiler/bet-check/src/lib.rs index 763b3d1..d09bbb9 100644 --- a/compiler/bet-check/src/lib.rs +++ b/compiler/bet-check/src/lib.rs @@ -837,7 +837,10 @@ fn check_bet(bet: &BetExpr, env: &mut CheckEnv, span: Span) -> CompileResult 'a`.) + Ok(Type::Dist(Box::new(env.resolve(&t0)))) } /// Check a weighted bet: branches unify, weights must be numeric. @@ -863,7 +866,8 @@ fn check_weighted_bet( for i in 1..branch_types.len() { env.unify(&branch_types[0], &branch_types[i], Some(span))?; } - Ok(env.resolve(&branch_types[0])) + // Weighted bet, like uniform bet, is a distribution: `Dist T`. + Ok(Type::Dist(Box::new(env.resolve(&branch_types[0])))) } /// Check a conditional bet: condition is Bool/Ternary, all branches unify. @@ -892,7 +896,9 @@ fn check_conditional_bet( env.unify(&true_ty, &f0, Some(span))?; env.unify(&true_ty, &f1, Some(span))?; env.unify(&true_ty, &f2, Some(span))?; - Ok(env.resolve(&true_ty)) + // Conditional bet also yields a distribution over `T`: point-mass on the + // `if_true` value when the condition holds, else the ternary distribution. + Ok(Type::Dist(Box::new(env.resolve(&true_ty)))) } // ============================================ @@ -1265,7 +1271,11 @@ mod tests { ], }; let result = check_expr(&dummy(Expr::Bet(bet)), &mut env); - assert_eq!(result.expect("TODO: handle error"), Type::Int); + // `bet` introduces probabilistic choice, so its type is `Dist Int`. + assert_eq!( + result.expect("TODO: handle error"), + Type::Dist(Box::new(Type::Int)) + ); } #[test] @@ -1699,9 +1709,11 @@ mod tests { ); } - /// The core primitive bridges to Echo by composition at the type level: - /// `echo(bet a b c) : Echo T`. (Runtime branch-tag retention — `bet_echo` — - /// remains deferred; the *type* story needs no new primitive.) + /// The core primitive bridges to Echo by composition at the type level. + /// Since `bet a b c : Dist T`, the composite is `echo(bet a b c) : Echo (Dist T)` + /// — the retained-loss residue over the *distribution*. (Runtime branch-tag + /// retention — `bet_echo` — remains deferred; the *type* story needs no new + /// primitive.) #[test] fn test_bet_echo_bridge_by_composition() { let mut env = CheckEnv::new(); @@ -1714,8 +1726,8 @@ mod tests { }; let e = call("echo", vec![dummy(Expr::Bet(bet))]); assert_eq!( - check_expr(&e, &mut env).expect("echo (bet 1 2 3) : Echo Int"), - Type::Echo(Box::new(Type::Int)) + check_expr(&e, &mut env).expect("echo (bet 1 2 3) : Echo (Dist Int)"), + Type::Echo(Box::new(Type::Dist(Box::new(Type::Int)))) ); } diff --git a/compiler/bet-codegen/src/lib.rs b/compiler/bet-codegen/src/lib.rs index 551f15e..b46bcb2 100644 --- a/compiler/bet-codegen/src/lib.rs +++ b/compiler/bet-codegen/src/lib.rs @@ -102,24 +102,36 @@ pub fn codegen_module(module: &Module, target: Target) -> CompileResult &'static str { r#"// === Betlang Runtime Preamble === -// Uniform ternary choice among exactly 3 alternatives +// Uniform ternary choice among exactly 3 alternatives. +// `bet` has type `Dist T`: it returns a *distribution object* (sample with +// `__bet_sample`), not an eager draw — consistent with the checker/interpreter. function __bet_uniform(a, b, c) { - const r = Math.random(); - if (r < 1/3) return a; - if (r < 2/3) return b; - return c; + return { + name: 'bet', + sample() { + const r = Math.random(); + if (r < 1/3) return a; + if (r < 2/3) return b; + return c; + }, + }; } -// Weighted ternary choice (weights normalised internally) +// Weighted ternary choice (weights normalised internally). Returns a Dist. function __bet_weighted(alts, weights) { - const total = weights.reduce((s, w) => s + w, 0); - const r = Math.random() * total; - let cumul = 0; - for (let i = 0; i < alts.length; i++) { - cumul += weights[i]; - if (r < cumul) return alts[i]; - } - return alts[alts.length - 1]; + return { + name: 'weighted_bet', + sample() { + const total = weights.reduce((s, w) => s + w, 0); + const r = Math.random() * total; + let cumul = 0; + for (let i = 0; i < alts.length; i++) { + cumul += weights[i]; + if (r < cumul) return alts[i]; + } + return alts[alts.length - 1]; + }, + }; } // --- Distribution objects --- diff --git a/compiler/bet-eval/Cargo.toml b/compiler/bet-eval/Cargo.toml index 9567189..175de10 100644 --- a/compiler/bet-eval/Cargo.toml +++ b/compiler/bet-eval/Cargo.toml @@ -8,6 +8,9 @@ license.workspace = true [dependencies] bet-syntax = { path = "../bet-syntax" } bet-core = { path = "../bet-core" } +bet-rt = { path = "../../runtime/bet-rt" } # the unified runtime Value (Dist, …) +bet-rand = { path = "../../runtime/bet-rand" } # centralised ternary/weighted RNG +im.workspace = true # bet_rt::Value::List is im::Vector rand.workspace = true rand_distr.workspace = true thiserror.workspace = true diff --git a/compiler/bet-eval/src/lib.rs b/compiler/bet-eval/src/lib.rs index f2b03bb..136f45d 100644 --- a/compiler/bet-eval/src/lib.rs +++ b/compiler/bet-eval/src/lib.rs @@ -2,45 +2,30 @@ // Copyright (c) Jonathan D.A. Jewell //! Interpreter for Betlang //! -//! Evaluates Betlang AST nodes directly, supporting probabilistic operations. +//! Tree-walking evaluator over the betlang AST. It uses the **shared runtime +//! value type** `bet_rt::value::Value` (re-exported here as `Value`) so the +//! interpreter and the embeddable runtime (`bet-rt`, used by the FFI bindings) +//! speak the same values — one runtime, not two. //! -//! Author: Jonathan D.A. Jewell +//! Probabilistic semantics: `bet { a, b, c }` evaluates to a **distribution** +//! (`Value::Dist`, typed `Dist T`), matching the Rust checker and the mechanised +//! Lean rule `tBet : … → Ty.dist T`. `sample : Dist T -> T` draws from it. +//! +//! Closures: betlang lambdas are AST closures, but `bet_rt::value::Closure` +//! holds a native `Box) -> Value>`. We *closure-convert*: a +//! lambda becomes a native closure that re-invokes `eval` on the captured body +//! and environment. Evaluation errors inside a closure surface as `Value::Error` +//! (the native closure has no `Result` channel) and are re-raised by `apply`. #![forbid(unsafe_code)] use bet_syntax::ast::*; use bet_core::{ValueEnv, CompileError, CompileResult}; -use rand::prelude::*; +use bet_rt::value::{Closure, Distribution, Ternary}; +use im::Vector; use std::sync::Arc; -/// Runtime value -#[derive(Debug, Clone)] -pub enum Value { - Unit, - Bool(bool), - Ternary(TernaryVal), - Int(i64), - Float(f64), - String(Arc), - List(Vec), - Tuple(Vec), - Closure(Arc), -} - -/// Ternary logic value for the evaluator -#[derive(Debug, Clone, Copy, PartialEq)] -pub enum TernaryVal { - True, - False, - Unknown, -} - -/// A closure capturing its environment -#[derive(Debug)] -pub struct Closure { - pub params: Vec, - pub body: Expr, - pub env: ValueEnv, -} +/// The unified runtime value (shared with `bet-rt` and the FFI bindings). +pub use bet_rt::value::Value; /// Evaluate an expression in the given environment pub fn eval(expr: &Expr, env: &mut ValueEnv) -> CompileResult { @@ -52,21 +37,21 @@ pub fn eval(expr: &Expr, env: &mut ValueEnv) -> CompileResult { Expr::Float(f) => Ok(Value::Float(*f)), Expr::String(s) => Ok(Value::String(Arc::new(s.clone()))), Expr::Ternary(t) => Ok(Value::Ternary(match t { - TernaryValue::True => TernaryVal::True, - TernaryValue::False => TernaryVal::False, - TernaryValue::Unknown => TernaryVal::Unknown, + TernaryValue::True => Ternary::True, + TernaryValue::False => Ternary::False, + TernaryValue::Unknown => Ternary::Unknown, })), // --- Variables --- Expr::Var(sym) => { let name = sym.as_str(); - env.lookup(&name).ok_or_else(|| CompileError::UndefinedVariable { + env.lookup(&name).ok_or(CompileError::UndefinedVariable { name, span: None, }) } - // --- Bet expressions --- + // --- Bet expressions (produce distributions, type `Dist T`) --- Expr::Bet(bet) => eval_bet(bet, env), Expr::WeightedBet(wb) => eval_weighted_bet(wb, env), Expr::ConditionalBet(cb) => eval_conditional_bet(cb, env), @@ -81,7 +66,7 @@ pub fn eval(expr: &Expr, env: &mut ValueEnv) -> CompileResult { // --- If --- Expr::If(ifexpr) => { let cond = eval(&ifexpr.condition.node, env)?; - if is_truthy(&cond) { + if cond.is_truthy() { eval(&ifexpr.then_branch.node, env) } else { eval(&ifexpr.else_branch.node, env) @@ -101,31 +86,30 @@ pub fn eval(expr: &Expr, env: &mut ValueEnv) -> CompileResult { eval_unop(*op, v) } - // --- Lambda --- + // --- Lambda (closure-converted into a native runtime closure) --- Expr::Lambda(lam) => { - let params: Vec = lam.params.iter().map(|p| pattern_name(&p.node)).collect(); - Ok(Value::Closure(Arc::new(Closure { - params, - body: lam.body.node.clone(), - env: env.clone(), - }))) + let params: Vec = + lam.params.iter().map(|p| pattern_name(&p.node)).collect(); + Ok(make_closure(params, lam.body.node.clone(), env.clone())) } // --- Application --- Expr::App(func, args) => { let f = eval(&func.node, env)?; - let mut arg_vals = Vec::new(); + let mut arg_vals = Vec::with_capacity(args.len()); for a in args { arg_vals.push(eval(&a.node, env)?); } apply(f, arg_vals) } - // --- Sample --- + // --- Sample: eliminate a distribution (`Dist T -> T`) --- Expr::Sample(dist_expr) => { - let dist = eval(&dist_expr.node, env)?; - // For now, just return the value (distributions not fully modelled) - Ok(dist) + let v = eval(&dist_expr.node, env)?; + v.sample().map_err(|message| CompileError::Runtime { + message, + span: None, + }) } // --- Tuples and Lists --- @@ -134,10 +118,10 @@ pub fn eval(expr: &Expr, env: &mut ValueEnv) -> CompileResult { .iter() .map(|e| eval(&e.node, env)) .collect::>()?; - Ok(Value::Tuple(vals)) + Ok(Value::Tuple(Arc::new(vals))) } Expr::List(elems) => { - let vals: Vec = elems + let vals: Vector = elems .iter() .map(|e| eval(&e.node, env)) .collect::>()?; @@ -148,14 +132,16 @@ pub fn eval(expr: &Expr, env: &mut ValueEnv) -> CompileResult { Expr::Parallel(n_expr, body) => { let n = match eval(&n_expr.node, env)? { Value::Int(n) => n as usize, - _ => return Err(CompileError::Runtime { - message: "parallel count must be an integer".to_string(), - span: None, - }), + _ => { + return Err(CompileError::Runtime { + message: "parallel count must be an integer".to_string(), + span: None, + }) + } }; - let mut results = Vec::with_capacity(n); + let mut results = Vector::new(); for _ in 0..n { - results.push(eval(&body.node, env)?); + results.push_back(eval(&body.node, env)?); } Ok(Value::List(results)) } @@ -163,29 +149,94 @@ pub fn eval(expr: &Expr, env: &mut ValueEnv) -> CompileResult { // --- Type annotation (ignored at runtime) --- Expr::Annotate(inner, _) => eval(&inner.node, env), - // Catch-all for unimplemented nodes - _ => Ok(Value::Unit), + // Unimplemented forms (Do, Match, Observe, Infer, Record, Field, Index, + // echo operations, …). Surfaced explicitly rather than silently + // evaluating to `Unit` (which produced wrong results with no signal). + other => Err(CompileError::Runtime { + message: format!( + "interpreter (bet-eval): expression form not yet implemented: {}", + expr_form_name(other) + ), + span: None, + }), + } +} + +/// Short, stable name of an expression's syntactic form, for diagnostics. +fn expr_form_name(expr: &Expr) -> &'static str { + match expr { + Expr::Do(_) => "do-block", + Expr::Match(_) => "match", + Expr::Observe(_, _) => "observe", + Expr::Infer(_) => "infer", + Expr::Record(_) => "record", + Expr::Field(_, _) => "field-access", + Expr::Index(_, _) => "index", + _ => "this expression", } } // --------------------------------------------------------------------------- -// Bet evaluation +// Closures (AST -> native closure conversion) +// --------------------------------------------------------------------------- + +/// Build a runtime closure from a betlang lambda by capturing its body AST and +/// defining environment, and re-invoking `eval` on application. +fn make_closure(params: Vec, body: Expr, captured: ValueEnv) -> Value { + let call_params = params.clone(); + Value::Closure(Arc::new(Closure { + params, + name: None, + body: Box::new(move |args: Vec| { + let mut local = captured.clone(); + for (p, a) in call_params.iter().zip(args.into_iter()) { + local.bind(p.clone(), a); + } + match eval(&body, &mut local) { + Ok(v) => v, + // No Result channel in the native closure: encode the failure + // as an Error value; `apply` re-raises it as a CompileError. + Err(err) => Value::Error(Arc::new(err.to_string())), + } + }), + })) +} + +fn apply(func: Value, args: Vec) -> CompileResult { + match func { + Value::Closure(closure) => match (closure.body)(args) { + Value::Error(e) => Err(CompileError::Runtime { + message: e.as_ref().clone(), + span: None, + }), + v => Ok(v), + }, + Value::Native(native) => (native.func)(args).map_err(|message| CompileError::Runtime { + message, + span: None, + }), + other => Err(CompileError::Runtime { + message: format!("Cannot apply non-function: {}", other.type_name()), + span: None, + }), + } +} + +// --------------------------------------------------------------------------- +// Bet evaluation — each form builds a `Value::Dist` // --------------------------------------------------------------------------- fn eval_bet(bet: &BetExpr, env: &mut ValueEnv) -> CompileResult { - let values: Vec = bet - .alternatives - .iter() - .map(|alt| eval(&alt.node, env)) - .collect::>()?; - - let idx = thread_rng().gen_range(0..3); - Ok(values.into_iter().nth(idx).expect("TODO: handle error")) + let v0 = eval(&bet.alternatives[0].node, env)?; + let v1 = eval(&bet.alternatives[1].node, env)?; + let v2 = eval(&bet.alternatives[2].node, env)?; + // Uniform ternary distribution (sampled via bet-rt's RNG-backed sampler). + Ok(Value::bet(v0, v1, v2)) } fn eval_weighted_bet(wb: &WeightedBetExpr, env: &mut ValueEnv) -> CompileResult { - let mut values = Vec::new(); - let mut weights = Vec::new(); + let mut values: Vec = Vec::new(); + let mut weights: Vec = Vec::new(); for (val_expr, wt_expr) in &wb.alternatives { values.push(eval(&val_expr.node, env)?); @@ -198,15 +249,7 @@ fn eval_weighted_bet(wb: &WeightedBetExpr, env: &mut ValueEnv) -> Compile } let total: f64 = weights.iter().sum(); - let r: f64 = thread_rng().gen::() * total; - let mut cumul = 0.0; - for (i, w) in weights.iter().enumerate() { - cumul += w; - if r < cumul { - return Ok(values.into_iter().nth(i).expect("TODO: handle error")); - } - } - Ok(values.into_iter().last().expect("TODO: handle error")) + Ok(categorical_dist(values, weights, total)) } fn eval_conditional_bet( @@ -214,19 +257,45 @@ fn eval_conditional_bet( env: &mut ValueEnv, ) -> CompileResult { let cond = eval(&cb.condition.node, env)?; - if is_truthy(&cond) { - eval(&cb.if_true.node, env) + if cond.is_truthy() { + // Point-mass distribution on the deterministic branch value. + let v = eval(&cb.if_true.node, env)?; + Ok(point_mass(v)) } else { - let values: Vec = cb - .if_false - .iter() - .map(|alt| eval(&alt.node, env)) - .collect::>()?; - let idx = thread_rng().gen_range(0..3); - Ok(values.into_iter().nth(idx).expect("TODO: handle error")) + let v0 = eval(&cb.if_false[0].node, env)?; + let v1 = eval(&cb.if_false[1].node, env)?; + let v2 = eval(&cb.if_false[2].node, env)?; + Ok(Value::bet(v0, v1, v2)) } } +/// A categorical distribution over `values` with the given (unnormalised) +/// `weights`. Supports any number of alternatives. +fn categorical_dist(values: Vec, weights: Vec, total: f64) -> Value { + Value::Dist(Arc::new(Distribution { + sampler: Box::new(move || { + let r = bet_rand::uniform(0.0, total); + let mut cumul = 0.0; + for (i, w) in weights.iter().enumerate() { + cumul += w; + if r < cumul { + return values[i].clone(); + } + } + values.last().cloned().unwrap_or(Value::Unit) + }), + name: "weighted_bet".to_string(), + })) +} + +/// A point-mass distribution: sampling always yields `v`. +fn point_mass(v: Value) -> Value { + Value::Dist(Arc::new(Distribution { + sampler: Box::new(move || v.clone()), + name: "pure".to_string(), + })) +} + // --------------------------------------------------------------------------- // Operators // --------------------------------------------------------------------------- @@ -284,15 +353,17 @@ fn eval_binop(op: BinOp, lhs: Value, rhs: Value) -> CompileResult { Ok(Value::String(Arc::new(format!("{}{}", a, b)))) } - // List operations + // List operations (`bet_rt::Value::List` is an `im::Vector`) (BinOp::Cons, val, Value::List(list)) => { - let mut new_list = vec![val.clone()]; - new_list.extend(list.iter().cloned()); + let mut new_list = list.clone(); + new_list.push_front(val.clone()); Ok(Value::List(new_list)) } (BinOp::Append, Value::List(a), Value::List(b)) => { let mut new_list = a.clone(); - new_list.extend(b.iter().cloned()); + for v in b.iter() { + new_list.push_back(v.clone()); + } Ok(Value::List(new_list)) } @@ -309,9 +380,9 @@ fn eval_unop(op: UnOp, val: Value) -> CompileResult { (UnOp::Neg, Value::Float(f)) => Ok(Value::Float(-f)), (UnOp::Not, Value::Bool(b)) => Ok(Value::Bool(!b)), (UnOp::Not, Value::Ternary(t)) => Ok(Value::Ternary(match t { - TernaryVal::True => TernaryVal::False, - TernaryVal::False => TernaryVal::True, - TernaryVal::Unknown => TernaryVal::Unknown, + Ternary::True => Ternary::False, + Ternary::False => Ternary::True, + Ternary::Unknown => Ternary::Unknown, })), _ => Err(CompileError::Runtime { message: format!("Unsupported unary operation {:?} on {:?}", op, val), @@ -324,17 +395,6 @@ fn eval_unop(op: UnOp, val: Value) -> CompileResult { // Helpers // --------------------------------------------------------------------------- -fn is_truthy(val: &Value) -> bool { - match val { - Value::Bool(b) => *b, - Value::Int(i) => *i != 0, - Value::Float(f) => *f != 0.0, - Value::Ternary(TernaryVal::True) => true, - Value::Unit => false, - _ => true, - } -} - fn bind_pattern(pat: &Pattern, val: Value, env: &mut ValueEnv) -> CompileResult<()> { match pat { Pattern::Var(sym) => { @@ -350,8 +410,8 @@ fn bind_pattern(pat: &Pattern, val: Value, env: &mut ValueEnv) -> Compile span: None, }); } - for (p, v) in pats.iter().zip(vals) { - bind_pattern(&p.node, v, env)?; + for (p, v) in pats.iter().zip(vals.iter()) { + bind_pattern(&p.node, v.clone(), env)?; } Ok(()) } else { @@ -373,56 +433,6 @@ fn pattern_name(pat: &Pattern) -> String { } } -fn apply(func: Value, args: Vec) -> CompileResult { - match func { - Value::Closure(closure) => { - let mut new_env = closure.env.clone(); - for (param, arg) in closure.params.iter().zip(args) { - new_env.bind(param.clone(), arg); - } - eval(&closure.body, &mut new_env) - } - _ => Err(CompileError::Runtime { - message: format!("Cannot apply non-function: {:?}", func), - span: None, - }), - } -} - -impl std::fmt::Display for Value { - fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { - match self { - Value::Unit => write!(f, "()"), - Value::Bool(b) => write!(f, "{}", b), - Value::Ternary(t) => write!(f, "{:?}", t), - Value::Int(i) => write!(f, "{}", i), - Value::Float(x) => write!(f, "{}", x), - Value::String(s) => write!(f, "\"{}\"", s), - Value::List(l) => { - write!(f, "[")?; - for (i, v) in l.iter().enumerate() { - if i > 0 { - write!(f, ", ")?; - } - write!(f, "{}", v)?; - } - write!(f, "]") - } - Value::Tuple(t) => { - write!(f, "(")?; - for (i, v) in t.iter().enumerate() { - if i > 0 { - write!(f, ", ")?; - } - write!(f, "{}", v)?; - } - write!(f, ")") - } - Value::Closure(_) => write!(f, ""), - } - } -} - #[cfg(test)] mod tests { use super::*; @@ -436,7 +446,7 @@ mod tests { #[test] fn test_eval_int() { let mut env = ValueEnv::new(); - let val = eval(&Expr::Int(42), &mut env).expect("TODO: handle error"); + let val = eval(&Expr::Int(42), &mut env).expect("eval int"); assert!(matches!(val, Value::Int(42))); } @@ -448,7 +458,7 @@ mod tests { Box::new(dummy(Expr::Int(3))), Box::new(dummy(Expr::Int(7))), ); - let val = eval(&expr, &mut env).expect("TODO: handle error"); + let val = eval(&expr, &mut env).expect("eval add"); assert!(matches!(val, Value::Int(10))); } @@ -466,12 +476,12 @@ mod tests { ))), is_rec: false, }); - let val = eval(&expr, &mut env).expect("TODO: handle error"); + let val = eval(&expr, &mut env).expect("eval let"); assert!(matches!(val, Value::Int(10))); } #[test] - fn test_eval_bet() { + fn test_eval_bet_is_distribution() { let mut env = ValueEnv::new(); let expr = Expr::Bet(BetExpr { alternatives: [ @@ -480,11 +490,25 @@ mod tests { Box::new(dummy(Expr::Int(3))), ], }); - // Should return one of 1, 2, or 3 + // `bet` now evaluates to a distribution (Dist Int), not a drawn value. + let val = eval(&expr, &mut env).expect("eval bet"); + assert!(matches!(val, Value::Dist(_))); + } + + #[test] + fn test_eval_sample_of_bet() { + let mut env = ValueEnv::new(); + // sample(bet { 1, 2, 3 }) draws one of 1, 2, 3. + let expr = Expr::Sample(Box::new(dummy(Expr::Bet(BetExpr { + alternatives: [ + Box::new(dummy(Expr::Int(1))), + Box::new(dummy(Expr::Int(2))), + Box::new(dummy(Expr::Int(3))), + ], + })))); for _ in 0..100 { - let val = eval(&expr, &mut env).expect("TODO: handle error"); - match val { - Value::Int(n) => assert!(n >= 1 && n <= 3), + match eval(&expr, &mut env).expect("eval sample") { + Value::Int(n) => assert!((1..=3).contains(&n)), other => panic!("Expected Int, got {other:?}"), } } @@ -498,7 +522,7 @@ mod tests { then_branch: Box::new(dummy(Expr::Int(1))), else_branch: Box::new(dummy(Expr::Int(0))), }); - let val = eval(&expr, &mut env).expect("TODO: handle error"); + let val = eval(&expr, &mut env).expect("eval if"); assert!(matches!(val, Value::Int(1))); } @@ -516,7 +540,7 @@ mod tests { }))), vec![dummy(Expr::Int(41))], ); - let val = eval(&expr, &mut env).expect("TODO: handle error"); + let val = eval(&expr, &mut env).expect("eval lambda apply"); assert!(matches!(val, Value::Int(42))); } } diff --git a/compiler/bet-parse/src/lib.rs b/compiler/bet-parse/src/lib.rs index 7bf4bdd..5180797 100644 --- a/compiler/bet-parse/src/lib.rs +++ b/compiler/bet-parse/src/lib.rs @@ -36,9 +36,25 @@ pub enum ParseError { UnexpectedToken { found: String, expected: Vec, + /// Byte offsets of the offending token (start, end). + start: usize, + end: usize, }, } +impl ParseError { + /// Byte-offset range `(start, end)` of the error in the source, when known. + /// Used by tooling (LSP) to place a precise diagnostic; `None` falls back + /// to the start of the document. + pub fn offsets(&self) -> Option<(usize, usize)> { + match self { + ParseError::Parse { location, .. } => Some((*location, *location + 1)), + ParseError::UnexpectedToken { start, end, .. } => Some((*start, *end)), + ParseError::Lexer(_) | ParseError::UnexpectedEof => None, + } + } +} + /// Result of parsing with error recovery: partial AST + diagnostics. pub struct ParseOutput { pub module: Module, @@ -70,6 +86,8 @@ fn convert_lalrpop_error(e: lalrpop_util::ParseError) -> ParseError::UnexpectedToken { found: format!("{:?}", token.1), expected, + start: token.0, + end: token.2, } } lalrpop_util::ParseError::ExtraToken { token } => ParseError::Parse { diff --git a/compiler/bet-wasm/src/lib.rs b/compiler/bet-wasm/src/lib.rs index 8620f3a..1e18c1f 100644 --- a/compiler/bet-wasm/src/lib.rs +++ b/compiler/bet-wasm/src/lib.rs @@ -552,9 +552,9 @@ impl WasmBackend { func.instruction(&Instruction::I32Const(0)); } } - WasmType::I64 => func.instruction(&Instruction::I64Const(0)), - WasmType::F32 => func.instruction(&Instruction::F32Const(0.0)), - WasmType::F64 => func.instruction(&Instruction::F64Const(0.0)), + WasmType::I64 => { func.instruction(&Instruction::I64Const(0)); } + WasmType::F32 => { func.instruction(&Instruction::F32Const(0.0)); } + WasmType::F64 => { func.instruction(&Instruction::F64Const(0.0)); } } } diff --git a/docs/decisions/2026-06-15-betlang-wiring-and-bet-dist-t.adoc b/docs/decisions/2026-06-15-betlang-wiring-and-bet-dist-t.adoc new file mode 100644 index 0000000..8f1366b --- /dev/null +++ b/docs/decisions/2026-06-15-betlang-wiring-and-bet-dist-t.adoc @@ -0,0 +1,221 @@ +// SPDX-License-Identifier: MPL-2.0 +// Owner: Jonathan D.A. Jewell +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) += Design-decision log — betlang wiring pass & `bet : Dist T` (2026-06-15) +:toc: + +A consolidated, ADR-style log of the 2026-06-15 betlang session: a wire-first +pass across the toolchain, the decision to make `bet : Dist T` canonical and +unify the interpreter onto `bet-rt`'s value type, the proof work, and the +reconciliation with a parallel session that landed its own TP-5 + checker +hardening. Recorded so the *encounters on the journey* — not just the final +state — survive as decisions. + +Each entry is `Context → Decision → Consequences`. Status legend: +LANDED (in this branch), CANONICAL (owner-adjudicated), DEFERRED, SURFACED +(owner decision pending). + +== ADR-0: Ground truth — betlang is the Rust workspace, not the Racket DSL + +*Context.* The root `CLAUDE.md` described betlang as a minimal Racket DSL +(`core/betlang.rkt`, `repl/shell.rkt`). The actual project is a multi-crate +*Rust* compiler (`bet-syntax → bet-parse → bet-check → bet-eval / bet-codegen / +bet-wasm`), a Lean 4 metatheory, a Julia backend, and LSP/DAP tooling, with +`racket` not even installed. A 17-agent audit + direct reads established what +actually works versus what is built-in-isolation. + +*Decision.* Treat the Rust/Lean reality as authoritative for engineering work. +Two orchestrator "facts" were corrected on the journey: Lean is *4.15.0 and +matches* the `lean-toolchain` pin (the "v4.15 vs 4.13" mismatch was a phantom — +`elan` overrides per-directory; `lake build` is green), and TP-4's `substTop` +is a *proved theorem*, zero axioms (the "single classified axiom" was already +discharged). + +*Consequences.* The wiring pass (ADR-5) connects the orphaned Rust components. +The "Racket is authoritative" declaration in `Justfile` / `AUTHORITY_STACK` / +`CLAUDE.md` was left untouched — see ADR-8 (SURFACED). + +== ADR-1: `bet` has type `Dist T` (CANONICAL) + +*Context.* The Lean proof (`proofs/BetLang.lean`) mechanises `tBet : … → +HasType … (Ty.dist T)` — `bet` introduces a distribution. But the Rust checker +returned the bare branch type `T`, and the interpreter returned a drawn value. +So `Progress`/`Preservation` (TP-1/TP-2) certified a rule the implementation did +not run — a soundness-meaning gap, not just missing work. + +*Decision (owner: option a).* Make `bet : Dist T` canonical across the +implementation, aligning it with the already-correct proof. Eliminate a +distribution with `sample : Dist 'a -> 'a`. Weighted and conditional bets are +distributions too (`Dist T`); a conditional bet is a point-mass on `if_true` +when the condition holds, else the ternary distribution. + +*Consequences.* +* `bet-check`: `check_bet`/`check_weighted_bet`/`check_conditional_bet` now + return `Dist T`. Programs must `sample` before using a drawn value: + `bet { 1,2,3 } + 1` is now correctly rejected (`expected Dist(Int), found Int`). +* `echo(bet a b c) : Echo (Dist T)` (the retained-loss residue is over the + *distribution*). +* TP-1/TP-2 now describe the shipped rule; the proof became load-bearing. + +== ADR-2: One runtime — unify the interpreter onto `bet_rt::Value` (LANDED) + +*Context.* Two independently-built runtimes existed with *different* value +types: `bet-eval` (a tree-walker with its own simple `Value`, used by the CLI) +and `bet-rt` (a richer embeddable runtime — `Dist`/`Map`/`Set`/`Native` — used +only by the FFI bindings). `bet-rt` already had `Value::Dist(Arc)` +and `Value::bet(a,b,c)` — exactly what `bet : Dist T` needs. + +*Decision.* `bet-eval` adopts `bet_rt::value::Value` as its value type (re-exported +as `bet_eval::Value`). `bet` evaluates to a real `Value::Dist`; `sample` draws +via the distribution's sampler. + +*The impedance, and its resolution.* `bet_rt::Closure` holds a *native* +`Box) -> Value + Send + Sync>`, not an AST closure — this is +*why* the two runtimes were separate (compiled-runtime style vs tree-walker). +We *closure-convert*: a betlang lambda becomes a native closure that captures the +body `Expr` + defining environment and re-invokes `eval`. Feasible because +`Symbol` is a `u32` over a global interner, so `Expr` is `Send + Sync + 'static`. +The native closure has no `Result` channel, so an evaluation error inside a +closure is encoded as `Value::Error` and re-raised by `apply` — a documented, +self-consistent degradation (betlang `eval` produces `Value::Error` only via +this mechanism). + +*Consequences.* `bet-rt` and `bet-rand` (previously *zero* dependents) are now +consumed by the interpreter — one runtime, not two. Native functions +(`Value::Native`) and the full data-structure surface come for free. + +== ADR-3: JS codegen emits distribution objects (LANDED) + +*Context.* Under ADR-1, the JS backend was inconsistent: `bet` emitted an +*eager draw* (`__bet_uniform` returned a value) while `__bet_sample` expected a +*distribution object* — so `sample(bet …)` threw "Cannot sample from +non-distribution". + +*Decision.* `__bet_uniform`/`__bet_weighted` return distribution objects with a +`.sample()` method (matching `__bet_dist_normal` and `__bet_sample`). The emitted +*call sites* are unchanged, so the 34 codegen string-tests stay valid; only the +preamble bodies change. + +*Consequences.* Generated JS executes correctly end-to-end: +`bet compile examples/dice.bet --target js` produces JavaScript whose `sample` +draws from a real distribution object (verified under deno). + +== ADR-4: Surface interpreter gaps as errors, not silent `Unit` (LANDED) + +*Context.* `bet-eval` had a catch-all `_ => Ok(Value::Unit)` collapsing every +unimplemented form (`Do`, `Match`, `Observe`, `Infer`, `Record`, `Field`, +`Index`, echo ops) to `Unit` — silently wrong results with no signal. + +*Decision.* Replace it with an explicit `Runtime` error naming the construct +(`expr_form_name`). `Sample` is documented as identity-on-non-Dist (the checker +guarantees it only ever sees a `Dist`). + +*Consequences.* "We know what works and what does not" — the interpreter now +*tells* you when it hits an unimplemented form. + +== ADR-5: Wire-first pass across the toolchain (LANDED) + +The orphan/breakage map from the audit, each fixed and verified: + +[cols="1,4"] +|=== +| Area | Change + +| Justfile +| Was *unparseable* (`//` comment on line 1 — `just` rejected the whole file). + Fixed to `#`; added Rust task-runner recipes (`build-rust`, `test-rust`, + `check`, `run`, `compile`, `repl-rust`) alongside the historical Racket ones. + +| Rust workspace +| Was RED. Fixed `bet-wasm` (E0308 match arm), `bet-viz` (`im` dep + + `Histogram`→`Rectangle` for a continuous axis + textplots `Chart`/`Shape` + lifetimes), `bet-chapel` (`rand_pcg` dep). Also fixed *three real + pre-existing `bet-rt` bugs*: a queue returning the wrong end (refill reversed + an already-FIFO `back`), `printf %s` quoting strings (used `Value` Display), + and msgpack decoding a `List` as `Bytes` (untagged-enum variant order). + +| cbindgen / licence +| `bindings/chapel/build.rs` stripped the SPDX header from the generated + `include/betlang.h` on *every* build — an automated licence edit, which estate + policy forbids. Fixed with `.with_header(...)` so the header is preserved. + +| CLI → codegen +| The JS backend (34 tests) was dead surface. Added `bet compile + --target js\|llvm\|beam [--out]`. + +| LSP → parser/checker +| `document.ast()` was a stub returning the source string; `bet-parse`/`bet-check` + were commented out as "LALR grammar conflicts" (obsolete — the parser builds, + 164 tests pass). Wired the real parser + type checker; diagnostics now surface + real parse *and* type errors with precise spans (enhanced + `ParseError::UnexpectedToken` to carry byte offsets, which also helps the CLI). + +| interpreter → bet-rand +| `bet-rand` (zero dependents) now backs `bet`/weighted/conditional RNG — + centralised, seedable later. +|=== + +A first working `.bet` example (`examples/dice.bet`) was added — none existed +(`examples/*` were stale `.rkt`). betlang comments are `--` / `{- -}`. + +== ADR-6: TP-5 — echo metatheory; richer surface split to TP-5b (CANONICAL) + +*Context.* Two sessions independently implemented TP-5 in `proofs/BetLang.lean`. +The parallel session landed a *lean* core: `echoIntro` / `echoElim` (the +`echo_output` counit), the `echoElimIntro` β-rule, congruences, `canonical_echo`, +and Progress/Preservation re-established. This session had built a *richer* +version: all six operations as primitives plus the three comonad laws and the +functor identity, proved as `MultiStep` confluence (the ungraded operational +shadow of `EchoGradedComonad.agda`). + +*Decision (owner-adjudicated).* The parallel session's intro/elim core is the +canonical *TP-5*. The richer surface — `echo_map`/`echo_duplicate`/ +`echo_to_residue`/`sample_echo` composed from `echoIntro`/`echoElim`, plus the +comonad laws — becomes *TP-5b* (P3, deferred). This branch keeps origin's +`BetLang.lean` untouched; it does not re-land the richer version. + +*Consequences.* `PROOF-STATUS.md` records TP-5 done (intro/elim) and TP-5b +remaining. The richer comonad-law development is preserved in this session's +history (local commit `964d106`) and this log, as the reference implementation +for whoever discharges TP-5b. Both echo-types caveats stand: the *graded* +comonad framing for the shipped 3-grade object is retracted upstream +(R-2026-05-18); the loss-combining variance (comonad / monad / adjunction) is +open in `echo-types/experimental/echo-additive` (R2/R3, author-gated). + +== ADR-7: Parallel-session reconciliation (LANDED on this branch) + +*Context.* While this session worked locally, a parallel session pushed five +commits to `origin/main` — its own TP-5 (`da8a232`), checker *let-polymorphism* +(`77ba191`) and *occurs-check* (`431420f`, fixing the unsoundness the audit +flagged), plus estate/licence and CI work — then a merge `b31f7a6`. That merge +reconciled the TP-5/checker collisions but *dropped this session's wiring*. + +*Decision.* Follow the estate parallel-session discipline (review, don't +compete; reconcile surgically). Branch off the current `origin/main`; bring this +session's 24 non-colliding wiring files; keep origin's `BetLang.lean` (TP-5) and +checker base (occurs-check + let-poly — complementary, *kept*); re-apply only the +small `bet : Dist T` delta on top of the reconciled checker. `docs/echo-types.adoc` +was left at origin's baseline (owner-managed; this session's edits were stale +under the TP-5/TP-5b split). + +*Consequences.* The reconciled branch builds clean: 317 workspace tests pass, +`lake build` green, banned-pattern scan clean. The occurs-check + let-poly the +parallel session added are exactly what the audit said the checker lacked — the +two streams are complementary, not redundant. + +== ADR-8: Deferred / surfaced for the owner + +* *Racket → Rust authority (SURFACED).* `Justfile` / `AUTHORITY_STACK.mustfile` + / `CLAUDE.md` still declare Racket authoritative. Rust recipes were *added* + alongside, not substituted; flipping the declaration is an owner decision. +* *Runtime operational model (DEFERRED).* The Lean proof models `bet → distPure + vᵢ` (draw-then-wrap); the interpreter and JS codegen use a *distribution-object* + model. The typing (`bet : Dist T`) is shared; both are valid operational + semantics for the same typed calculus. A materialised runtime residue payload + for echo remains future work. +* *TP-5b (DEFERRED, P3).* Richer echo surface + comonad laws (see ADR-6). +* *SEM-1 / STAT-1 / STAT-2 (DEFERRED).* Analytic obligations that realistically + need Mathlib — an architectural decision to keep the proof core hermetic vs. + add a separate Mathlib-dependent lake target. +* *ABI-1..5 (DEFERRED, P1).* Idris2 FFI proofs; need a `proof-check-idris2` + recipe + CI wired first, and manual MPL licence care on the exemplar copy. diff --git a/examples/dice.bet b/examples/dice.bet new file mode 100644 index 0000000..35adb63 --- /dev/null +++ b/examples/dice.bet @@ -0,0 +1,19 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) Jonathan D.A. Jewell +-- +-- dice.bet — a minimal working betlang example for the Rust toolchain. +-- +-- Verified with the `bet` CLI: +-- just check examples/dice.bet (type-checks) +-- just run examples/dice.bet (interprets) +-- just compile examples/dice.bet js (emits runnable JavaScript) + +-- A `bet` is a *distribution* (type `Dist T`), not a drawn value. +-- Uniform ternary bet: equally likely 1, 2, or 3. +let roll = bet { 1, 2, 3 } + +-- Weighted ternary bet: weights need not be normalised. +let loaded = bet { 1 @ 0.6, 2 @ 0.3, 3 @ 0.1 } + +-- `sample : Dist T -> T` draws a value; arithmetic is over the drawn values. +let total = (sample roll) + (sample loaded) diff --git a/lakefile.lean b/lakefile.lean index f4b51b0..1beee49 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -3,10 +3,13 @@ -- -- Lake build for the BetLang Lean 4 formalisation. -- --- The mechanisation is deliberately pure-core Lean 4 (no Mathlib): the --- only soundness-relevant escape hatch is the single classified axiom --- `substTop_preserves_typing` (see docs/proof-debt.adoc). Keeping the --- dependency surface empty makes `lake build` fast and hermetic in CI. +-- The mechanisation is deliberately pure-core Lean 4 (no Mathlib) and +-- AXIOM-FREE: the former classified axiom `substTop_preserves_typing` has +-- been discharged to a proved `theorem` (TP-4; see docs/proof-debt.adoc), so +-- no `axiom` declarations remain. Every theorem — including the echo-comonad +-- metatheory (TP-5) — depends only on the standard Lean kernel axioms. +-- Keeping the dependency surface empty makes `lake build` fast and hermetic +-- in CI. -- -- The canonical source lives at `proofs/BetLang.lean` (referenced by -- docs/proof-debt.adoc); we point the library root there rather than diff --git a/runtime/bet-rt/src/data.rs b/runtime/bet-rt/src/data.rs index 4b4ad8a..baab33f 100644 --- a/runtime/bet-rt/src/data.rs +++ b/runtime/bet-rt/src/data.rs @@ -615,8 +615,10 @@ pub mod queue { if self.back.is_empty() { return None; } - // Reverse back into front - let new_front: Vector = self.back.iter().cloned().rev().collect(); + // Move `back` into `front`. `enqueue` appends with `push_back`, + // so `back` is already in arrival (FIFO) order — do NOT reverse, + // or `dequeue` would return the most-recently-enqueued element. + let new_front: Vector = self.back.iter().cloned().collect(); let value = new_front.head()?.clone(); Some(( value, @@ -640,7 +642,9 @@ pub mod queue { /// Peek at front without removing pub fn peek(&self) -> Option { if self.front.is_empty() { - self.back.last().cloned() + // `back` is in FIFO order (see `dequeue`); the front of the + // queue is its head, not its last element. + self.back.head().cloned() } else { self.front.head().cloned() } diff --git a/runtime/bet-rt/src/io.rs b/runtime/bet-rt/src/io.rs index 78d7d77..742a5ba 100644 --- a/runtime/bet-rt/src/io.rs +++ b/runtime/bet-rt/src/io.rs @@ -449,7 +449,12 @@ pub mod stdio { Some('s') => { chars.next(); if arg_idx < args.len() { - result.push_str(&format!("{}", args[arg_idx])); + // `%s` emits the raw string content (C-style); the + // `Value` Display form quotes strings, which is wrong here. + match &args[arg_idx] { + Value::String(s) => result.push_str(s), + other => result.push_str(&format!("{}", other)), + } arg_idx += 1; } } diff --git a/runtime/bet-rt/src/serial.rs b/runtime/bet-rt/src/serial.rs index fdda3d6..1cbbe06 100644 --- a/runtime/bet-rt/src/serial.rs +++ b/runtime/bet-rt/src/serial.rs @@ -273,7 +273,16 @@ pub mod msgpack { use rmp_serde::{self, Deserializer, Serializer}; use serde::{Deserialize, Serialize}; - /// Intermediate representation for serde + /// Intermediate representation for serde. + /// + /// This is an `untagged` enum, so on deserialize serde tries variants in + /// declaration order and takes the first that succeeds. `Array` MUST come + /// before `Bytes`: rmp-serde encodes a `Vec` as a msgpack *array* (not + /// `bin`) by default, so a serialized `List` of small ints would otherwise + /// match `Bytes(Vec)` first and a `List` would round-trip to `Bytes`. + /// (Fully distinguishing `Value::Bytes` from `Value::List` on the wire would + /// require `serde_bytes`/msgpack `bin`; not pulled in for this peripheral + /// path, so a genuine `Bytes` currently round-trips as a `List`.) #[derive(Serialize, Deserialize)] #[serde(untagged)] enum MsgPackValue { @@ -282,8 +291,8 @@ pub mod msgpack { Int(i64), Float(f64), String(String), - Bytes(Vec), Array(Vec), + Bytes(Vec), Map(std::collections::HashMap), } diff --git a/runtime/bet-viz/Cargo.toml b/runtime/bet-viz/Cargo.toml index 62b06b9..e05a2d4 100644 --- a/runtime/bet-viz/Cargo.toml +++ b/runtime/bet-viz/Cargo.toml @@ -8,6 +8,9 @@ license.workspace = true [dependencies] bet-rt = { path = "../bet-rt" } +# Data structures (immutable Vector, matching bet-rt's Value collections) +im.workspace = true + # Core thiserror.workspace = true serde = { workspace = true, features = ["derive"] } diff --git a/runtime/bet-viz/src/lib.rs b/runtime/bet-viz/src/lib.rs index 96725ec..8a548dc 100644 --- a/runtime/bet-viz/src/lib.rs +++ b/runtime/bet-viz/src/lib.rs @@ -309,18 +309,16 @@ pub fn histogram(data: &Vector, bins: usize, config: &PlotConfig) -> VizR .draw() .map_err(|e| VizError::RenderError(e.to_string()))?; + // Draw bars as filled rectangles. `Histogram::vertical` requires a + // `DiscreteRanged` x-axis; our axis is a continuous `f64` range, so we + // render the bins directly as `Rectangle`s on the cartesian plane. + let bar_style = config.line_color.filled(); chart - .draw_series( - Histogram::vertical(&chart) - .style(config.line_color.filled()) - .margin(1) - .data( - counts - .iter() - .enumerate() - .map(|(i, &c)| (min_val + i as f64 * bin_width, c)), - ), - ) + .draw_series(counts.iter().enumerate().map(|(i, &c)| { + let x0 = min_val + i as f64 * bin_width; + let x1 = x0 + bin_width; + Rectangle::new([(x0, 0u32), (x1, c)], bar_style.clone()) + })) .map_err(|e| VizError::RenderError(e.to_string()))?; root.present() diff --git a/runtime/bet-viz/src/terminal.rs b/runtime/bet-viz/src/terminal.rs index bc056ac..e7ada9d 100644 --- a/runtime/bet-viz/src/terminal.rs +++ b/runtime/bet-viz/src/terminal.rs @@ -73,11 +73,16 @@ pub fn term_line_plot(x: &[f32], y: &[f32], config: &TermPlotConfig) -> VizResul output.push('\n'); } - // Use textplots for ASCII rendering - let chart = Chart::new(config.width * 2, config.height, points[0].0, points.last().expect("TODO: handle error").0) - .lineplot(&Shape::Lines(&points)); - - output.push_str(&format!("{}", chart)); + // Use textplots for ASCII rendering. Bind the chart and shape to locals so + // neither is dropped while `lineplot`'s `&mut Chart` is still in use. + let mut chart = Chart::new( + config.width * 2, + config.height, + points[0].0, + points.last().expect("TODO: handle error").0, + ); + let shape = Shape::Lines(&points); + output.push_str(&format!("{}", chart.lineplot(&shape))); Ok(output) } @@ -179,10 +184,9 @@ pub fn term_scatter(x: &[f32], y: &[f32], config: &TermPlotConfig) -> VizResult< let x_min = x.iter().cloned().fold(f32::INFINITY, f32::min); let x_max = x.iter().cloned().fold(f32::NEG_INFINITY, f32::max); - let chart = Chart::new(config.width * 2, config.height, x_min, x_max) - .lineplot(&Shape::Points(&points)); - - output.push_str(&format!("{}", chart)); + let mut chart = Chart::new(config.width * 2, config.height, x_min, x_max); + let shape = Shape::Points(&points); + output.push_str(&format!("{}", chart.lineplot(&shape))); Ok(output) } diff --git a/tools/bet-cli/Cargo.toml b/tools/bet-cli/Cargo.toml index ae410b2..d205806 100644 --- a/tools/bet-cli/Cargo.toml +++ b/tools/bet-cli/Cargo.toml @@ -15,6 +15,7 @@ bet-parse = { path = "../../compiler/bet-parse" } bet-eval = { path = "../../compiler/bet-eval" } bet-check = { path = "../../compiler/bet-check" } bet-core = { path = "../../compiler/bet-core" } +bet-codegen = { path = "../../compiler/bet-codegen" } serde_json = "1.0" clap.workspace = true diff --git a/tools/bet-cli/src/main.rs b/tools/bet-cli/src/main.rs index 1d15b1b..2844694 100644 --- a/tools/bet-cli/src/main.rs +++ b/tools/bet-cli/src/main.rs @@ -69,6 +69,20 @@ enum Commands { write: bool, }, + /// Compile a file to a target backend (currently JavaScript) + Compile { + /// The file to compile + file: PathBuf, + + /// Target backend: js (default), llvm, beam + #[arg(long, default_value = "js")] + target: String, + + /// Write output to this path (instead of stdout) + #[arg(short, long)] + out: Option, + }, + /// Show version information Version, } @@ -103,6 +117,9 @@ fn main() -> Result<()> { Some(Commands::Fmt { file, write }) => { format_file(&file, write) } + Some(Commands::Compile { file, target, out }) => { + compile_file(&file, &target, out.as_ref()) + } Some(Commands::Version) => { print_version(); Ok(()) @@ -147,6 +164,52 @@ fn run_file(path: &PathBuf) -> Result<()> { Ok(()) } +/// Compile a file to a target backend and write the generated code. +/// +/// Pipeline: parse → type-check (warnings only) → `bet_codegen::codegen_module`. +/// JavaScript is fully supported; LLVM/BEAM are placeholder backends. +fn compile_file(path: &PathBuf, target: &str, out: Option<&PathBuf>) -> Result<()> { + use bet_codegen::Target; + + let target = match target.to_ascii_lowercase().as_str() { + "js" | "javascript" => Target::JavaScript, + "llvm" => Target::Llvm, + "beam" | "erlang" => Target::Beam, + other => { + return Err(miette::miette!( + "unknown target '{}': expected one of js, llvm, beam", + other + )) + } + }; + + let source = std::fs::read_to_string(path).into_diagnostic()?; + let module = bet_parse::parse(&source).map_err(|e| miette::miette!("{}", e))?; + + // Type-check first (warnings only — compilation proceeds regardless, matching `run`). + if let Err(e) = bet_check::check_module(&module) { + eprintln!("Warning: type check error: {}", e); + } + + let output = + bet_codegen::codegen_module(&module, target).map_err(|e| miette::miette!("{}", e))?; + + match out { + Some(out_path) => { + std::fs::write(out_path, &output.code).into_diagnostic()?; + eprintln!( + "Compiled {} → {} ({:?})", + path.display(), + out_path.display(), + output.target + ); + } + None => print!("{}", output.code), + } + + Ok(()) +} + /// Parse a file and display the AST in the requested output format. /// /// Supported formats: diff --git a/tools/bet-lsp/Cargo.toml b/tools/bet-lsp/Cargo.toml index 8230204..0ef0481 100644 --- a/tools/bet-lsp/Cargo.toml +++ b/tools/bet-lsp/Cargo.toml @@ -26,9 +26,10 @@ once_cell = "1.19" serde = { version = "1", features = ["derive"] } serde_json = "1" -# Betlang compiler components -# Note: bet-parse has LALR grammar conflicts, using simplified parsing for now +# Betlang compiler components — wired to the real parser + checker. +# (The historical "LALR grammar conflicts" note is obsolete: bet-parse builds +# clean, its 164 tests pass, and the `bet` CLI parses/checks with it.) bet-syntax = { path = "../../compiler/bet-syntax" } -# bet-parse = { path = "../../compiler/bet-parse" } +bet-parse = { path = "../../compiler/bet-parse" } bet-core = { path = "../../compiler/bet-core" } -# bet-check = { path = "../../compiler/bet-check" } +bet-check = { path = "../../compiler/bet-check" } diff --git a/tools/bet-lsp/src/document.rs b/tools/bet-lsp/src/document.rs index 46b911d..94547c8 100644 --- a/tools/bet-lsp/src/document.rs +++ b/tools/bet-lsp/src/document.rs @@ -5,6 +5,9 @@ use once_cell::sync::OnceCell; use tower_lsp::lsp_types::Url; +use bet_parse::ParseError; +use bet_syntax::ast::Module; + use crate::utils::LineIndex; /// Document state with lazy-evaluated caches @@ -14,11 +17,8 @@ pub struct DocumentState { pub source: String, pub line_index: LineIndex, - // Lazy-evaluated caches - // Note: Actual parsing would use bet-parse crate - // For now, we store parse results as strings (simplified) - tokens: OnceCell, String>>, - ast: OnceCell>, + /// Lazy, cached parse result from the real `bet-parse` parser. + parsed: OnceCell>, } impl DocumentState { @@ -31,33 +31,16 @@ impl DocumentState { version, source, line_index, - tokens: OnceCell::new(), - ast: OnceCell::new(), + parsed: OnceCell::new(), } } - /// Get tokens (lazy evaluation) - pub fn tokens(&self) -> &Result, String> { - self.tokens.get_or_init(|| { - // Simplified tokenization - would use bet-parse in production - let tokens: Vec = self - .source - .split_whitespace() - .map(String::from) - .collect(); - Ok(tokens) - }) - } - - /// Get AST (lazy evaluation) - pub fn ast(&self) -> &Result { - self.ast.get_or_init(|| { - // Simplified AST parsing - would use bet-parse in production - match self.tokens() { - Ok(_) => Ok(self.source.clone()), - Err(e) => Err(e.clone()), - } - }) + /// Parse the document with the real betlang parser (lazy, cached). + /// + /// Returns the parsed `Module` on success, or the `ParseError` (which + /// carries byte offsets via [`ParseError::offsets`]) on failure. + pub fn parsed(&self) -> &Result { + self.parsed.get_or_init(|| bet_parse::parse(&self.source)) } /// Get word at position (for completion/hover) diff --git a/tools/bet-lsp/src/handlers/diagnostics.rs b/tools/bet-lsp/src/handlers/diagnostics.rs index c5c3b60..559e35b 100644 --- a/tools/bet-lsp/src/handlers/diagnostics.rs +++ b/tools/bet-lsp/src/handlers/diagnostics.rs @@ -1,14 +1,13 @@ // SPDX-License-Identifier: MPL-2.0 // Copyright (c) Jonathan D.A. Jewell -//! Diagnostics handler — produces parse-level and structural diagnostics -//! for betlang documents. -//! -//! Performs lightweight lexical analysis to detect common errors without -//! requiring the full LALR parser (which has known grammar conflicts). +//! Diagnostics handler — surfaces real parse and type-check diagnostics for +//! betlang documents, produced by the `bet-parse` parser and `bet-check` +//! type checker (not lexical heuristics). use tower_lsp::lsp_types::*; use crate::backend::Backend; +use crate::utils::range_from_offsets; /// Publish diagnostics for a document. pub async fn publish_diagnostics(backend: &Backend, uri: &Url) { @@ -20,7 +19,19 @@ pub async fn publish_diagnostics(backend: &Backend, uri: &Url) { .await; } -/// Collect all diagnostics for a document. +/// A small default range at the start of the document, used when an error +/// carries no usable source span. +fn fallback_range() -> Range { + Range { + start: Position::new(0, 0), + end: Position::new(0, 1), + } +} + +/// Collect parse + type diagnostics for a document. +/// +/// Pipeline mirrors `bet run`/`bet check`: parse with `bet-parse`; on success, +/// type-check with `bet-check`. Each error is mapped to its real source span. fn collect_diagnostics(backend: &Backend, uri: &Url) -> Vec { let mut diagnostics = Vec::new(); @@ -29,199 +40,42 @@ fn collect_diagnostics(backend: &Backend, uri: &Url) -> Vec { None => return diagnostics, }; - // Check tokenization - if let Err(err) = doc.tokens() { - diagnostics.push(Diagnostic { - range: Range { - start: Position::new(0, 0), - end: Position::new(0, 1), - }, - severity: Some(DiagnosticSeverity::ERROR), - code: Some(NumberOrString::String("lex-error".into())), - source: Some("bet-lsp".into()), - message: err.clone(), - ..Default::default() - }); - return diagnostics; - } - - // Check basic parsing - if let Err(err) = doc.ast() { - diagnostics.push(Diagnostic { - range: Range { - start: Position::new(0, 0), - end: Position::new(0, 1), - }, - severity: Some(DiagnosticSeverity::ERROR), - code: Some(NumberOrString::String("parse-error".into())), - source: Some("bet-lsp".into()), - message: err.clone(), - ..Default::default() - }); - return diagnostics; - } + match doc.parsed() { + Err(parse_err) => { + let range = parse_err + .offsets() + .and_then(|(start, end)| range_from_offsets(start, end, &doc.line_index)) + .unwrap_or_else(fallback_range); - // Structural analysis - let source = &doc.source; - let mut paren_depth: i32 = 0; - let mut brace_depth: i32 = 0; - let mut bracket_depth: i32 = 0; - let mut in_string = false; - - for (line_idx, line) in source.lines().enumerate() { - let ln = line_idx as u32; - - for (col_idx, ch) in line.char_indices() { - if ch == '"' { - in_string = !in_string; - continue; - } - if in_string { - continue; - } - match ch { - '(' => paren_depth += 1, - ')' => { - paren_depth -= 1; - if paren_depth < 0 { - diagnostics.push(Diagnostic { - range: Range { - start: Position::new(ln, col_idx as u32), - end: Position::new(ln, col_idx as u32 + 1), - }, - severity: Some(DiagnosticSeverity::ERROR), - code: Some(NumberOrString::String("unmatched-paren".into())), - source: Some("bet-lsp".into()), - message: "Unmatched closing parenthesis".into(), - ..Default::default() - }); - } - } - '{' => brace_depth += 1, - '}' => { - brace_depth -= 1; - if brace_depth < 0 { - diagnostics.push(Diagnostic { - range: Range { - start: Position::new(ln, col_idx as u32), - end: Position::new(ln, col_idx as u32 + 1), - }, - severity: Some(DiagnosticSeverity::ERROR), - code: Some(NumberOrString::String("unmatched-brace".into())), - source: Some("bet-lsp".into()), - message: "Unmatched closing brace".into(), - ..Default::default() - }); - } - } - '[' => bracket_depth += 1, - ']' => { - bracket_depth -= 1; - if bracket_depth < 0 { - diagnostics.push(Diagnostic { - range: Range { - start: Position::new(ln, col_idx as u32), - end: Position::new(ln, col_idx as u32 + 1), - }, - severity: Some(DiagnosticSeverity::ERROR), - code: Some(NumberOrString::String("unmatched-bracket".into())), - source: Some("bet-lsp".into()), - message: "Unmatched closing bracket".into(), - ..Default::default() - }); - } - } - _ => {} - } - } - - // Check for bet expressions with wrong arity (not exactly 3) - let trimmed = line.trim(); - if trimmed.starts_with("bet ") || trimmed.starts_with("(bet ") { - // Count comma-separated alternatives in braces - if let Some(brace_start) = trimmed.find('{') { - if let Some(brace_end) = trimmed.rfind('}') { - let inner = &trimmed[brace_start + 1..brace_end]; - let alt_count = inner.split(',').count(); - if alt_count != 3 && !inner.trim().is_empty() { - diagnostics.push(Diagnostic { - range: Range { - start: Position::new(ln, 0), - end: Position::new(ln, line.len() as u32), - }, - severity: Some(DiagnosticSeverity::WARNING), - code: Some(NumberOrString::String("ternary-arity".into())), - source: Some("bet-lsp".into()), - message: format!( - "bet expression has {} alternatives (expected 3 — ternary)", - alt_count - ), - ..Default::default() - }); - } - } - } - } - - // Check for unclosed string on a single line - let quote_count = trimmed.chars().filter(|&c| c == '"').count(); - if quote_count % 2 != 0 { diagnostics.push(Diagnostic { - range: Range { - start: Position::new(ln, 0), - end: Position::new(ln, line.len() as u32), - }, + range, severity: Some(DiagnosticSeverity::ERROR), - code: Some(NumberOrString::String("unclosed-string".into())), + code: Some(NumberOrString::String("parse-error".into())), source: Some("bet-lsp".into()), - message: "Unclosed string literal".into(), + message: parse_err.to_string(), ..Default::default() }); } - } + Ok(module) => { + // Parse succeeded — run the real type checker. + if let Err(type_err) = bet_check::check_module(module) { + let range = type_err + .span() + .and_then(|sp| { + range_from_offsets(sp.start as usize, sp.end as usize, &doc.line_index) + }) + .unwrap_or_else(fallback_range); - // Report unbalanced delimiters at end of document - if paren_depth > 0 { - let last_line = source.lines().count().saturating_sub(1) as u32; - diagnostics.push(Diagnostic { - range: Range { - start: Position::new(last_line, 0), - end: Position::new(last_line, 1), - }, - severity: Some(DiagnosticSeverity::ERROR), - code: Some(NumberOrString::String("unmatched-paren".into())), - source: Some("bet-lsp".into()), - message: format!("{} unclosed parenthesis(es)", paren_depth), - ..Default::default() - }); - } - if brace_depth > 0 { - let last_line = source.lines().count().saturating_sub(1) as u32; - diagnostics.push(Diagnostic { - range: Range { - start: Position::new(last_line, 0), - end: Position::new(last_line, 1), - }, - severity: Some(DiagnosticSeverity::ERROR), - code: Some(NumberOrString::String("unmatched-brace".into())), - source: Some("bet-lsp".into()), - message: format!("{} unclosed brace(s)", brace_depth), - ..Default::default() - }); - } - if bracket_depth > 0 { - let last_line = source.lines().count().saturating_sub(1) as u32; - diagnostics.push(Diagnostic { - range: Range { - start: Position::new(last_line, 0), - end: Position::new(last_line, 1), - }, - severity: Some(DiagnosticSeverity::ERROR), - code: Some(NumberOrString::String("unmatched-bracket".into())), - source: Some("bet-lsp".into()), - message: format!("{} unclosed bracket(s)", bracket_depth), - ..Default::default() - }); + diagnostics.push(Diagnostic { + range, + severity: Some(DiagnosticSeverity::ERROR), + code: Some(NumberOrString::String("type-error".into())), + source: Some("bet-lsp".into()), + message: type_err.to_string(), + ..Default::default() + }); + } + } } diagnostics diff --git a/tools/bet-lsp/tests/integration_test.rs b/tools/bet-lsp/tests/integration_test.rs index 875f60d..b23c343 100644 --- a/tools/bet-lsp/tests/integration_test.rs +++ b/tools/bet-lsp/tests/integration_test.rs @@ -18,24 +18,28 @@ fn test_document_state_creation() { } #[test] -fn test_document_tokens() { +fn test_document_parses_valid_source() { let uri = Url::parse("file:///test.bet").unwrap(); - let source = "bet { a, b, c }".to_string(); + let source = "let r = bet { a, b, c }".to_string(); let doc = DocumentState::new(uri, source, 1); - let tokens = doc.tokens(); - assert!(tokens.is_ok()); - assert!(tokens.as_ref().unwrap().len() > 0); + // Uses the real bet-parse parser (not a stub). + assert!(doc.parsed().is_ok()); } #[test] -fn test_document_ast() { +fn test_document_reports_parse_error() { let uri = Url::parse("file:///test.bet").unwrap(); - let source = "bet { a, b, c }".to_string(); + // `let` with no binding name is a syntax error. + let source = "let = bet { a, b, c }".to_string(); let doc = DocumentState::new(uri, source.clone(), 1); - let ast = doc.ast(); - assert!(ast.is_ok()); + let parsed = doc.parsed(); + assert!(parsed.is_err()); + // The error carries a usable byte offset for LSP diagnostics. + if let Err(e) = parsed { + assert!(e.offsets().is_some()); + } } #[test] diff --git a/tools/proof-scan.sh b/tools/proof-scan.sh index 6d38c23..cb18407 100755 --- a/tools/proof-scan.sh +++ b/tools/proof-scan.sh @@ -14,10 +14,12 @@ # assert_total — Idris2 # unsafeCoerce — Haskell / Lean # -# NOTE: `axiom` is intentionally NOT banned. BetLang has exactly one -# classified necessary axiom (`substTop_preserves_typing`), triaged in -# docs/proof-debt.adoc under standards#203. AffineScript's banned list -# likewise permits explicit axioms. +# NOTE: `axiom` is intentionally NOT banned by policy (standards#203, as in +# AffineScript's banned list). HOWEVER, BetLang currently has ZERO axiom +# declarations: the formerly-classified `substTop_preserves_typing` has been +# discharged to a proved `theorem` (TP-4), and every theorem — including the +# echo-comonad metatheory (TP-5) — depends only on the standard Lean kernel +# axioms. Any future classified `axiom` must be triaged in docs/proof-debt.adoc. # # Comment-awareness: Lean line comments (`-- ...`) are stripped before # matching so that prose like "all theorems are fully proved — no sorry"