Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 3 additions & 1 deletion DESIGN.md
Original file line number Diff line number Diff line change
Expand Up @@ -1489,7 +1489,9 @@ show 42.0<M> -- "42.0 M"
show 3.14 -- "3.14"
```

When the unit is polymorphic (inside a unit-generic function), `show` prints just the number.
`Int` units are appended the same way, including the built-in `Ms` that clock operations carry — `now : IO {clock} Int<Ms>`, so `show` on a timestamp reads `"1783814121719 Ms"`. Use `stripUnit` to print the bare number.

When the unit is polymorphic (inside a unit-generic function), `show` prints just the number: the function body is compiled once, for every unit its caller may instantiate.

The compiler uses a canonical form for unit strings: alphabetical numerator, alphabetical denominator, powers collapsed. This same canonical form determines type equality (`m * s` = `s * m`).

Expand Down
28 changes: 27 additions & 1 deletion crates/knot-compiler/src/codegen.rs
Original file line number Diff line number Diff line change
Expand Up @@ -305,6 +305,12 @@ pub struct Codegen {
// path: `literal` (the `IN (?, …)` list form) and `dynamic` (the
// `IN (SELECT value FROM json_each(?))` form). See `infer::ElemPushdownOk`.
elem_pushdown_ok: crate::infer::ElemPushdownOk,

// `show` call sites whose argument has a concrete unit of measure:
// app_span -> canonical unit string (e.g. "M", "M/S^2"). Units are erased
// here, so the string from inference is the only carrier of the unit into
// the emitted code.
show_unit_strings: crate::infer::ShowUnitStrings,
}

/// A top-level constant declared as a signature with no body
Expand Down Expand Up @@ -602,6 +608,7 @@ pub fn compile(
type_info: &crate::infer::TypeInfo,
elem_pushdown_ok: &crate::infer::ElemPushdownOk,
trait_call_targets: &crate::infer::TraitCallTargets,
show_unit_strings: &crate::infer::ShowUnitStrings,
compile_time_overrides: &HashMap<String, String>,
) -> Result<Vec<u8>, Vec<knot::diagnostic::Diagnostic>> {
crate::stack::grow(|| {
Expand All @@ -616,6 +623,7 @@ pub fn compile(
type_info,
elem_pushdown_ok,
trait_call_targets,
show_unit_strings,
compile_time_overrides,
)
})
Expand All @@ -633,6 +641,7 @@ fn compile_inner(
type_info: &crate::infer::TypeInfo,
elem_pushdown_ok: &crate::infer::ElemPushdownOk,
trait_call_targets: &crate::infer::TraitCallTargets,
show_unit_strings: &crate::infer::ShowUnitStrings,
compile_time_overrides: &HashMap<String, String>,
) -> Result<Vec<u8>, Vec<knot::diagnostic::Diagnostic>> {
let mut cg = Codegen::new();
Expand Down Expand Up @@ -667,6 +676,7 @@ fn compile_inner(
.collect();
cg.from_json_targets = from_json_targets.clone();
cg.elem_pushdown_ok = elem_pushdown_ok.clone();
cg.show_unit_strings = show_unit_strings.clone();
cg.source_refinements = type_env.source_refinements.clone();
for (name, fields) in &type_env.constructors {
let field_strs: Vec<(String, String)> = fields
Expand Down Expand Up @@ -937,6 +947,7 @@ impl Codegen {
source_refinements: HashMap::new(),
from_json_targets: HashMap::new(),
elem_pushdown_ok: crate::infer::ElemPushdownOk::default(),
show_unit_strings: HashMap::new(),
}
}

Expand Down Expand Up @@ -1024,6 +1035,7 @@ impl Codegen {
self.declare_rt("knot_print", &[p], &[p]);
self.declare_rt("knot_println", &[p], &[p]);
self.declare_rt("knot_value_show", &[p], &[p]);
self.declare_rt("knot_value_show_unit", &[p, p, p], &[p]);
self.declare_rt("knot_guard_failed", &[], &[]);

// Constructor declaration order (backs structural `Ord` on ADTs)
Expand Down Expand Up @@ -6679,7 +6691,21 @@ impl Codegen {
}
ast::ExprKind::Var(name) if name == "show" => {
if compiled_args.len() == 1 {
self.call_rt(builder, "knot_value_show", &[compiled_args[0]])
// A `show` whose argument's type carried a concrete unit
// gets the unit appended: `show 42.0<M>` → "42.0 M". The
// unit is erased from the value, so inference resolved it
// per call site and it is emitted as a string constant.
match self.show_unit_strings.get(&expr.span).cloned() {
Some(unit) => {
let (unit_ptr, unit_len) = self.string_ptr(builder, &unit);
self.call_rt(
builder,
"knot_value_show_unit",
&[compiled_args[0], unit_ptr, unit_len],
)
}
None => self.call_rt(builder, "knot_value_show", &[compiled_args[0]]),
}
} else {
self.call_rt(builder, "knot_value_unit", &[])
}
Expand Down
61 changes: 52 additions & 9 deletions crates/knot-compiler/src/infer.rs
Original file line number Diff line number Diff line change
Expand Up @@ -118,6 +118,13 @@ pub type RefinedTypeInfoMap = HashMap<String, knot::ast::Expr>;
/// genuinely unknown until run time.
pub type TraitCallTargets = HashMap<(Span, String), String>;

/// Maps `show` call-site spans to the canonical unit string of the argument
/// (e.g. `"M"`, `"M/S^2"`). Only concrete units appear: units are erased at
/// runtime, so this is the sole channel by which the unit reaches the emitted
/// code. Codegen emits `knot_value_show_unit` for spans found here and plain
/// `knot_value_show` for the rest.
pub type ShowUnitStrings = HashMap<Span, String>;

/// Maps declaration names to their inferred type display strings.
pub type TypeInfo = HashMap<String, String>;

Expand Down Expand Up @@ -593,6 +600,12 @@ struct Infer {
/// Each entry records (app_span, return_type_var).
from_json_calls: Vec<(Span, TyVar)>,

/// Tracks `show` application sites so their argument's unit of measure can
/// be resolved after inference. Each entry records (app_span, arg_ty); the
/// arg type is recorded unresolved because a unit variable may only be
/// solved by a later constraint. See `show_unit_strings`.
show_calls: Vec<(Span, Ty)>,

/// Trait method → trait name mapping (e.g. "display" → "Display").
trait_method_traits: HashMap<String, String>,

Expand Down Expand Up @@ -705,9 +718,6 @@ struct Infer {
/// Whether we are currently processing a type annotation (so undeclared
/// unit names are treated as polymorphic unit variables).
in_type_annotation: bool,
/// Maps show call-site spans to their unit display strings (for codegen).
#[allow(dead_code)]
pub show_unit_strings: HashMap<Span, String>,

// ── Refined types ─────────────────────────────────────────────
/// Refined type metadata: type_name → (base Ty, predicate Expr).
Expand Down Expand Up @@ -775,6 +785,7 @@ impl Infer {
traverse_calls: Vec::new(),
from_json_calls: Vec::new(),
trait_call_vars: Vec::new(),
show_calls: Vec::new(),
trait_method_traits: HashMap::new(),
trait_method_param_vars: HashMap::new(),
known_impls: HashSet::new(),
Expand All @@ -800,7 +811,6 @@ impl Infer {
declared_units: HashMap::new(),
annotation_unit_vars: HashMap::new(),
in_type_annotation: false,
show_unit_strings: HashMap::new(),
refined_types: HashMap::new(),
refine_vars: Vec::new(),
suppress_refine_intro: None,
Expand Down Expand Up @@ -4943,6 +4953,16 @@ impl Infer {
self.from_json_calls.push((expr.span, *v));
}

// Track `show` calls so the argument's unit can be resolved
// once inference finishes and handed to codegen — the unit is
// erased before runtime, so this is the only chance to capture
// it. Recorded unresolved: `show (a * b)` may not know its unit
// until a later constraint solves the operands' unit vars.
if let ast::ExprKind::Var(name) = &func.node
&& name == "show" {
self.show_calls.push((expr.span, arg_ty.clone()));
}

// Track full `traverse f rel` applications: the resolved
// result type names the applicative, which codegen passes to
// the runtime to pick the right `pure []` for empty inputs.
Expand Down Expand Up @@ -10370,11 +10390,11 @@ fn value_references_source_inner(
///
/// Runs on a grown stack: a desugared `do` block nests one `__bind` per
/// statement, and `infer_expr` recurses through every level.
pub fn check(module: &mut ast::Module) -> (Vec<Diagnostic>, MonadInfo, TypeInfo, LocalTypeInfo, RefineTargets, RefinedTypeInfoMap, FromJsonTargets, ElemPushdownOk, TraitCallTargets) {
pub fn check(module: &mut ast::Module) -> (Vec<Diagnostic>, MonadInfo, TypeInfo, LocalTypeInfo, RefineTargets, RefinedTypeInfoMap, FromJsonTargets, ElemPushdownOk, TraitCallTargets, ShowUnitStrings) {
crate::stack::grow(|| check_inner(module))
}

fn check_inner(module: &mut ast::Module) -> (Vec<Diagnostic>, MonadInfo, TypeInfo, LocalTypeInfo, RefineTargets, RefinedTypeInfoMap, FromJsonTargets, ElemPushdownOk, TraitCallTargets) {
fn check_inner(module: &mut ast::Module) -> (Vec<Diagnostic>, MonadInfo, TypeInfo, LocalTypeInfo, RefineTargets, RefinedTypeInfoMap, FromJsonTargets, ElemPushdownOk, TraitCallTargets, ShowUnitStrings) {
let mut infer = Infer::new();

// Phase 1: Collect type aliases, data types, constructors
Expand Down Expand Up @@ -10675,11 +10695,34 @@ fn check_inner(module: &mut ast::Module) -> (Vec<Diagnostic>, MonadInfo, TypeInf
}
}

// Phase 8: Resolve the unit of measure at each `show` call site. Units are
// a compile-time overlay — fully erased by codegen — so a unit suffix can
// only be printed if it is captured here and emitted as a constant.
let mut show_unit_strings = ShowUnitStrings::new();
for (span, ty) in std::mem::take(&mut infer.show_calls) {
// Peel aliases so a refined/aliased numeric (`type Metres = Float<M>`)
// still shows its unit.
let resolved = infer.apply(&ty);
let unit = match resolved.peel_alias() {
Ty::IntUnit(u) | Ty::FloatUnit(u) => infer.apply_unit(u),
_ => continue,
};
// A unit still carrying variables is polymorphic — inside a unit-generic
// function the concrete unit is not known at this call site, and DESIGN
// specifies `show` prints just the number there. `apply` already folds a
// dimensionless unit back to plain `Int`/`Float`, so the emptiness check
// is only a guard against a hand-built `IntUnit(dimensionless)`.
if !unit.vars.is_empty() || unit.is_dimensionless() {
continue;
}
show_unit_strings.insert(span, unit.display());
}

let type_info = infer.extract_type_info();
let local_type_info = infer.extract_local_type_info();
let elem_pushdown_ok = infer.elem_pushdown_ok.clone();

(infer.to_diagnostics(), monad_info, type_info, local_type_info, refine_targets, refined_type_info, from_json_targets, elem_pushdown_ok, trait_call_targets)
(infer.to_diagnostics(), monad_info, type_info, local_type_info, refine_targets, refined_type_info, from_json_targets, elem_pushdown_ok, trait_call_targets, show_unit_strings)
}


Expand Down Expand Up @@ -11115,14 +11158,14 @@ mod tests {
fn check_src(src: &str) -> Vec<Diagnostic> {
let mut module = parse(src);
crate::desugar::desugar(&mut module);
let (diags, _monad_info, _type_info, _local_types, _refine_targets, _refined_types, _from_json, _elem_pushdown, _trait_calls) = check(&mut module);
let (diags, _monad_info, _type_info, _local_types, _refine_targets, _refined_types, _from_json, _elem_pushdown, _trait_calls, _show_units) = check(&mut module);
diags
}

fn type_info_for(src: &str) -> TypeInfo {
let mut module = parse(src);
crate::desugar::desugar(&mut module);
let (_diags, _monad_info, type_info, _local_types, _refine_targets, _refined_types, _from_json, _elem_pushdown, _trait_calls) = check(&mut module);
let (_diags, _monad_info, type_info, _local_types, _refine_targets, _refined_types, _from_json, _elem_pushdown, _trait_calls, _show_units) = check(&mut module);
type_info
}

Expand Down
4 changes: 2 additions & 2 deletions crates/knot-compiler/src/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -377,7 +377,7 @@ fn cmd_build(source_file: &str, output_override: Option<&std::path::Path>, overr
let type_env = types::TypeEnv::from_module(&module);

// Type inference
let (infer_diags, monad_info, type_info, _local_types, refine_targets, refined_types, from_json_targets, elem_pushdown_ok, trait_call_targets) = infer::check(&mut module);
let (infer_diags, monad_info, type_info, _local_types, refine_targets, refined_types, from_json_targets, elem_pushdown_ok, trait_call_targets, show_unit_strings) = infer::check(&mut module);
if !infer_diags.is_empty() {
for diag in &infer_diags {
eprintln!("{}", diag.render(&source, &filename));
Expand Down Expand Up @@ -440,7 +440,7 @@ fn cmd_build(source_file: &str, output_override: Option<&std::path::Path>, overr
}

// Code generation
let obj_bytes = match codegen::compile(&module, &type_env, source_file, &monad_info, &refine_targets, &refined_types, &from_json_targets, &type_info, &elem_pushdown_ok, &trait_call_targets, overrides) {
let obj_bytes = match codegen::compile(&module, &type_env, source_file, &monad_info, &refine_targets, &refined_types, &from_json_targets, &type_info, &elem_pushdown_ok, &trait_call_targets, &show_unit_strings, overrides) {
Ok(bytes) => bytes,
Err(diags) => {
for diag in &diags {
Expand Down
2 changes: 1 addition & 1 deletion crates/knot-compiler/tests/regress_analysis_fixes.rs
Original file line number Diff line number Diff line change
Expand Up @@ -34,7 +34,7 @@ fn parse(src: &str) -> knot::ast::Module {
fn check_src(src: &str) -> Vec<Diagnostic> {
let mut module = parse(src);
knot_compiler::desugar::desugar(&mut module);
let (diags, _monad, _type_info, _local, _refine, _refined, _json, _elem, _trait_calls) =
let (diags, _monad, _type_info, _local, _refine, _refined, _json, _elem, _trait_calls, _show_units) =
knot_compiler::infer::check(&mut module);
diags
}
Expand Down
7 changes: 4 additions & 3 deletions crates/knot-compiler/tests/regress_backend_fixes.rs
Original file line number Diff line number Diff line change
Expand Up @@ -137,11 +137,12 @@ main = do
"#,
);
assert!(ok, "program failed:\nstdout: {stdout}\nstderr: {stderr}");
// The outer `t` is a clock timestamp (a large integer), not a row.
// The outer `t` is a clock timestamp (a large integer), not a row. `now`
// is typed `IO {clock} Int<Ms>`, so `show` appends its unit: "<digits> Ms".
let first = stdout.lines().next().unwrap_or("");
let digits = first.trim_matches('"').trim_end_matches(" Ms");
assert!(
first.trim_matches('"').chars().all(|c| c.is_ascii_digit())
&& !first.is_empty(),
!digits.is_empty() && digits.chars().all(|c| c.is_ascii_digit()),
"expected the outer `t` (timestamp) to be printed, got:\n{stdout}"
);
}
Expand Down
3 changes: 2 additions & 1 deletion crates/knot-compiler/tests/regress_deep_do.rs
Original file line number Diff line number Diff line change
Expand Up @@ -115,7 +115,7 @@ fn deep_do_block_reaches_codegen_without_overflow() {
knot_compiler::desugar::desugar(&mut module);

let type_env = knot_compiler::types::TypeEnv::from_module(&module);
let (diags, monad_info, type_info, _local, refine_targets, refined, from_json, elem, trait_calls) =
let (diags, monad_info, type_info, _local, refine_targets, refined, from_json, elem, trait_calls, show_units) =
knot_compiler::infer::check(&mut module);
assert!(errors(&diags).is_empty(), "{:?}", errors(&diags));

Expand All @@ -130,6 +130,7 @@ fn deep_do_block_reaches_codegen_without_overflow() {
&type_info,
&elem,
&trait_calls,
&show_units,
&std::collections::HashMap::new(),
)
.expect("codegen should succeed on a deep do block");
Expand Down
2 changes: 1 addition & 1 deletion crates/knot-compiler/tests/regress_infer.rs
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,7 @@ fn check_full(
) -> (Vec<Diagnostic>, knot_compiler::infer::RefineTargets) {
let mut module = parse(src);
knot_compiler::desugar::desugar(&mut module);
let (diags, _monad, _type_info, _local, refine_targets, _refined, _json, _elem, _trait_calls) =
let (diags, _monad, _type_info, _local, refine_targets, _refined, _json, _elem, _trait_calls, _show_units) =
knot_compiler::infer::check(&mut module);
(diags, refine_targets)
}
Expand Down
2 changes: 1 addition & 1 deletion crates/knot-compiler/tests/regress_infer_fixes.rs
Original file line number Diff line number Diff line change
Expand Up @@ -26,7 +26,7 @@ fn parse(src: &str) -> knot::ast::Module {
fn check_src(src: &str) -> Vec<Diagnostic> {
let mut module = parse(src);
knot_compiler::desugar::desugar(&mut module);
let (diags, _monad, _type_info, _local, _targets, _refined, _json, _elem, _trait_calls) =
let (diags, _monad, _type_info, _local, _targets, _refined, _json, _elem, _trait_calls, _show_units) =
knot_compiler::infer::check(&mut module);
diags
}
Expand Down
2 changes: 1 addition & 1 deletion crates/knot-compiler/tests/regress_infer_fixes2.rs
Original file line number Diff line number Diff line change
Expand Up @@ -41,7 +41,7 @@ fn check_src(src: &str) -> Vec<Diagnostic> {
let mut module = parse(src);
knot_compiler::base::inject_prelude(&mut module);
knot_compiler::desugar::desugar(&mut module);
let (diags, _monad, _type_info, _local, _targets, _refined, _json, _elem, _trait_calls) =
let (diags, _monad, _type_info, _local, _targets, _refined, _json, _elem, _trait_calls, _show_units) =
knot_compiler::infer::check(&mut module);
diags
}
Expand Down
2 changes: 1 addition & 1 deletion crates/knot-compiler/tests/regress_infer_fixes3.rs
Original file line number Diff line number Diff line change
Expand Up @@ -25,7 +25,7 @@ fn check_src(src: &str) -> Vec<Diagnostic> {
let mut module = parse(src);
knot_compiler::base::inject_prelude(&mut module);
knot_compiler::desugar::desugar(&mut module);
let (diags, _monad, _type_info, _local, _targets, _refined, _json, _elem, _trait_calls) =
let (diags, _monad, _type_info, _local, _targets, _refined, _json, _elem, _trait_calls, _show_units) =
knot_compiler::infer::check(&mut module);
diags
}
Expand Down
2 changes: 1 addition & 1 deletion crates/knot-compiler/tests/regress_infer_fixes4.rs
Original file line number Diff line number Diff line change
Expand Up @@ -28,7 +28,7 @@ fn check_src(src: &str) -> Vec<Diagnostic> {
let mut module = parse(src);
knot_compiler::base::inject_prelude(&mut module);
knot_compiler::desugar::desugar(&mut module);
let (diags, _monad, _type_info, _local, _targets, _refined, _json, _elem, _trait_calls) =
let (diags, _monad, _type_info, _local, _targets, _refined, _json, _elem, _trait_calls, _show_units) =
knot_compiler::infer::check(&mut module);
diags
}
Expand Down
2 changes: 1 addition & 1 deletion crates/knot-compiler/tests/regress_infer_fixes5.rs
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,7 @@ fn check_src(src: &str) -> Vec<Diagnostic> {
let mut module = parse(src);
knot_compiler::base::inject_prelude(&mut module);
knot_compiler::desugar::desugar(&mut module);
let (diags, _monad, _type_info, _local, _targets, _refined, _json, _elem, _trait_calls) =
let (diags, _monad, _type_info, _local, _targets, _refined, _json, _elem, _trait_calls, _show_units) =
knot_compiler::infer::check(&mut module);
diags
}
Expand Down
2 changes: 1 addition & 1 deletion crates/knot-compiler/tests/regress_infer_fixes6.rs
Original file line number Diff line number Diff line change
Expand Up @@ -30,7 +30,7 @@ fn check_src(src: &str) -> Vec<Diagnostic> {
let mut module = parse(src);
knot_compiler::base::inject_prelude(&mut module);
knot_compiler::desugar::desugar(&mut module);
let (diags, _monad, _type_info, _local, _targets, _refined, _json, _elem, _trait_calls) =
let (diags, _monad, _type_info, _local, _targets, _refined, _json, _elem, _trait_calls, _show_units) =
knot_compiler::infer::check(&mut module);
diags
}
Expand Down
2 changes: 1 addition & 1 deletion crates/knot-compiler/tests/regress_knot_issues.rs
Original file line number Diff line number Diff line change
Expand Up @@ -39,7 +39,7 @@ fn check_src(src: &str) -> Vec<Diagnostic> {
let mut module = parse(src);
knot_compiler::base::inject_prelude(&mut module);
knot_compiler::desugar::desugar(&mut module);
let (diags, _monad, _type_info, _local, _refine, _refined, _json, _elem, _trait_calls) =
let (diags, _monad, _type_info, _local, _refine, _refined, _json, _elem, _trait_calls, _show_units) =
knot_compiler::infer::check(&mut module);
diags
}
Expand Down
Loading
Loading