source: scrub iter-code / Decision-N residue from inline comments

Follow-up to bcd4181: the remaining ~530 inline `//` and `///`
comments still carrying opaque shorthand are now reformulated to
their content phrases. The only surviving `iter-<code>` reference
in source is the literal filename
`docs/journals/2026-05-13-iter-mq.3.md` (a real journal file).

Sweep covered:
  - `// Iter X.Y: <text>` prefixes (Iter 13a / 14a / 14e / 15g-aux /
    16b.x / 16d / 16e / 18b / 18c.x / 18d.x / 18e / 18g.x / 19a /
    19a.1 / 19b / 20a / 20f / 22-floats.x / 22b.x / 22c / 23.x /
    24.1 / cli-diag-human / hs.x / str-concat / etc.) — fully
    removed; the descriptive text that followed each prefix stays.
  - `// (Decision N)` and `per Decision N` and `Decision N axis 3` —
    replaced with the content phrase plus the relevant contract
    file (`design/contracts/tail-calls.md` for Decision 8,
    `design/contracts/memory-model.md` for Decision 10,
    `design/contracts/typeclasses.md` and `design/models/typeclasses.md`
    for Decision 11, `design/contracts/authoring-surface.md` for
    Decision 6, "the transitional dual-allocator" for Decision 9,
    "Effect prose" for Decision 3).
  - `// mq.X / mq.X (Task N) / mq.X journal / mq.X invariant` ->
    "the canonical-class-form rule / Class-class repurpose /
    method-dispatch-refactor journal / canonical-class-form
    invariant".
  - `// ct.X / ct.X (canonical-type-names) / ct.1.5a + ctt.2 /
    ct.2 Task N` -> "the canonical-form rule for type references /
    the canonical-form normalisation step / canonical-type-lookup
    refactor".
  - `// eob.X` -> "heap-Str-ABI" / "the Str carve-out".
  - `// rpe.X` -> "the per-type-print-op retirement".
  - `// post-mq.X / Pre-ct.X / pre-mq.X` -> "post-canonical-class-form" /
    "Pre-canonical-type-form" etc.
  - `/// Iter X regression: / /// Iter X.Y: / /// Iter A arm-close /
    /// Iter ct.4 (...): / /// Iter rpe.1 ...` -> descriptive
    phrases.

The journal filename in `crates/ailang-core/src/workspace.rs:573`
stays verbatim because it points at an actual file under
`docs/journals/`.

Tests: full `cargo test --workspace` green (80/80 test-result blocks
clean, no FAILED line). design_index_pin 5/5 + docs_honesty_pin 5/5
gating tests pass.
This commit is contained in:
2026-05-20 09:58:04 +02:00
parent bcd41810f4
commit ac4d545570
43 changed files with 1004 additions and 1000 deletions
+1 -1
View File
@@ -204,7 +204,7 @@ pub struct FnDef {
/// Optional source-level documentation string.
#[serde(default, skip_serializing_if = "Option::is_none")]
pub doc: Option<String>,
/// Iter embedding-abi-m1: when `Some(sym)`, this fn is the
/// when `Some(sym)`, this fn is the
/// embedding boundary. Codegen's `Target::StaticLib` mode
/// additionally emits an externally-visible C entrypoint
/// `@<sym>` (signature frozen as of M3 —
+63 -63
View File
@@ -109,7 +109,7 @@
use crate::ast::*;
use std::collections::{BTreeMap, BTreeSet};
/// Iter 16b.2: per-name scope information used by the LetRec lifter.
/// per-name scope information used by the LetRec lifter.
/// `KnownType(t)` is set for fn-params and Lam-params, where the
/// type is statically declared. Other binder kinds use the
/// placeholder variants and the LetRec lifter rejects captures of
@@ -169,7 +169,7 @@ pub fn desugar_module(m: &Module) -> Module {
Def::Type(td) => {
used.insert(td.name.clone());
}
// Iter 22b.1: class/instance defs are passthrough for the
// class/instance defs are passthrough for the
// desugar pass — their bodies (default methods, instance
// method bodies) will be desugared once 22b.2 wires the
// class/instance arms into typecheck. For 22b.1 the names
@@ -183,7 +183,7 @@ pub fn desugar_module(m: &Module) -> Module {
}
}
}
// Iter 16b.1: pre-collect every top-level def name. The LetRec
// pre-collect every top-level def name. The LetRec
// lifter consults this set to (a) know whether a free var of a
// LetRec body resolves to a top-level def (no capture) and
// (b) keep its fresh-name generator from colliding with an
@@ -203,8 +203,8 @@ pub fn desugar_module(m: &Module) -> Module {
for def in &mut out.defs {
match def {
Def::Fn(f) => {
// Iter 16b.2 / 16b.6: build initial scope from fn-params
// with their declared types (peeled out of `f.ty`).
// Build initial scope from fn-params with their
// declared types (peeled out of `f.ty`).
//
// 16b.6: a `Type::Forall { vars, body: Fn(ptys, ...) }`
// enclosing fn is now supported. Its param types may
@@ -245,7 +245,7 @@ pub fn desugar_module(m: &Module) -> Module {
}
}
}
// Iter 16b.6: stash the enclosing fn's Forall.vars (or
// stash the enclosing fn's Forall.vars (or
// empty for a mono enclosing fn) for the LetRec arm.
let saved = std::mem::take(&mut d.current_def_forall_vars);
d.current_def_forall_vars = match &f.ty {
@@ -260,14 +260,14 @@ pub fn desugar_module(m: &Module) -> Module {
c.value = d.desugar_term(&c.value, &scope);
}
Def::Type(_) => {}
// Iter 22b.1: class/instance defs are not desugared yet.
// class/instance defs are not desugared yet.
// Their bodies (default methods, instance method bodies)
// will be processed once 22b.2 lands the class/instance
// arms in typecheck and 22b.3 in codegen.
Def::Class(_) | Def::Instance(_) => {}
}
}
// Iter 16b.1: append every lifted fn to the desugared module.
// append every lifted fn to the desugared module.
// Order: original defs first, then lifts in the order they were
// produced by the bottom-up walk. Typecheck/codegen are order-
// insensitive at the def list level (they index by name), so this
@@ -338,11 +338,11 @@ fn collect_used_in_term(t: &Term, used: &mut BTreeSet<String>) {
collect_used_in_term(in_term, used);
}
Term::Clone { value } => {
// Iter 18c.1: identity for the used-name walk.
// identity for the used-name walk.
collect_used_in_term(value, used);
}
Term::ReuseAs { source, body } => {
// Iter 18d.1: structural recursion through both children.
// structural recursion through both children.
collect_used_in_term(source, used);
collect_used_in_term(body, used);
}
@@ -383,7 +383,7 @@ fn collect_used_in_pattern(p: &Pattern, used: &mut BTreeSet<String>) {
/// contains every source-level identifier (var-bind or var-reference)
/// in the module so that [`fresh`](Self::fresh) cannot shadow one.
///
/// Iter 16b.1 fields:
/// LetRec-lift fields:
/// - `lifted` accumulates synthetic top-level fns produced by
/// [`Term::LetRec`] desugaring. Appended to `Module.defs` once the
/// per-def walk finishes.
@@ -393,7 +393,7 @@ fn collect_used_in_pattern(p: &Pattern, used: &mut BTreeSet<String>) {
/// generator [`fresh_lifted`](Self::fresh_lifted) consults it so
/// later lifts cannot collide with earlier ones.
///
/// Iter 16b.6 field:
/// Forall-tracking field:
/// - `current_def_forall_vars` carries the enclosing fn's
/// `Type::Forall.vars` while desugaring its body. Empty for
/// monomorphic enclosing fns. Read by the LetRec lifter to wrap
@@ -406,7 +406,7 @@ struct Desugarer {
used: BTreeSet<String>,
lifted: Vec<Def>,
module_top_names: BTreeSet<String>,
/// Iter 16b.6: the enclosing fn's Forall.vars (or empty if mono).
/// the enclosing fn's Forall.vars (or empty if mono).
/// Reset on entry to each `Def::Fn`.
current_def_forall_vars: Vec<String>,
}
@@ -427,7 +427,7 @@ impl Desugarer {
}
}
/// Iter 16b.1: returns a name of the form `<hint>$lr_N` not in
/// returns a name of the form `<hint>$lr_N` not in
/// `used` and not in `module_top_names`. Bumps both sets so a
/// later lift cannot collide. The `hint` is the source-level
/// LetRec name; it makes lifted bindings traceable through the
@@ -541,12 +541,12 @@ impl Desugarer {
rhs: Box::new(self.desugar_term(rhs, scope)),
},
Term::Clone { value } => Term::Clone {
// Iter 18c.1: pure structural recursion through the
// pure structural recursion through the
// wrapper. Same pattern as `Term::Let`'s value branch.
value: Box::new(self.desugar_term(value, scope)),
},
Term::ReuseAs { source, body } => Term::ReuseAs {
// Iter 18d.1: pure structural recursion through both
// pure structural recursion through both
// children. Same pattern as `Term::Clone`.
source: Box::new(self.desugar_term(source, scope)),
body: Box::new(self.desugar_term(body, scope)),
@@ -582,18 +582,18 @@ impl Desugarer {
.collect(),
},
Term::LetRec { name, ty, params, body, in_term } => {
// Iter 16b.1: lift to a synthetic top-level fn (no-capture).
// Iter 16b.2: extend the lift to the path-1 safe subset —
// lift to a synthetic top-level fn (no-capture).
// extend the lift to the path-1 safe subset —
// captures of fn-params / Lam-params (whose types are
// known statically).
// Iter 16b.3: when ANY capture is `LetBound` the desugar
// when ANY capture is `LetBound` the desugar
// pass cannot resolve its type (the let-value's type is
// only known after typecheck). For that case we LEAVE
// the LetRec in place, with body and in_term recursively
// desugared. A post-typecheck pass (`lift_letrecs` in
// `ailang-check`) walks every surviving LetRec and lifts
// it using the typechecker's resolved types.
// Iter 16b.4: extends the defer path to `MatchArm`
// extends the defer path to `MatchArm`
// captures. The post-typecheck pass already walks
// `Term::Match` arms and (since 16b.3) calls
// `type_check_pattern_for_lift` to extend locals with
@@ -672,7 +672,7 @@ impl Desugarer {
}
let in_has_value_use = find_non_callee_use(&desugared_in, name).is_some();
// Iter 16b.6: reject name-as-value in `in_term` when the
// reject name-as-value in `in_term` when the
// enclosing fn is polymorphic. The 16b.5 wrap synthesises
// a `Term::Lam` whose AST has no `Forall` slot, so
// wrapping a polymorphic lifted fn into a monomorphic Lam
@@ -773,7 +773,7 @@ impl Desugarer {
// Build augmented type: original Fn with capture types
// appended to `params`.
//
// Iter 16b.6: when the ENCLOSING fn is polymorphic
// when the ENCLOSING fn is polymorphic
// (`current_def_forall_vars` non-empty), wrap the
// augmented Fn in a `Type::Forall` mirroring the
// enclosing fn's type vars. The capture types may
@@ -933,7 +933,7 @@ impl Desugarer {
}
let s = self.fresh();
let s_var = Term::Var { name: s.clone() };
// Iter 16d: `default` is unreachable for valid programs (the
// `default` is unreachable for valid programs (the
// typechecker requires either a catch-all arm or exhaustive
// ctor coverage). Use the polymorphic bottom builtin
// `__unreachable__` (`forall a. a`) so the terminator unifies
@@ -975,7 +975,7 @@ impl Desugarer {
body: Box::new(arm.body.clone()),
},
Pattern::Lit { lit } => {
// Iter 16c: a top-level lit arm desugars to `if (== s_var lit)
// a top-level lit arm desugars to `if (== s_var lit)
// then arm.body else fall_k`. Eliminates `Pattern::Lit` from
// the desugared output entirely; codegen never sees it.
let cmp = build_eq(s_var.clone(), lit);
@@ -1035,7 +1035,7 @@ impl Desugarer {
body: Box::new(body),
},
Pattern::Lit { lit } => {
// Iter 16c: a lit sub-pattern desugars to `if (== fv lit) body
// a lit sub-pattern desugars to `if (== fv lit) body
// else fall_k`. Same shape as the top-level case, but on the
// field-bound fresh variable rather than the original
// scrutinee.
@@ -1070,7 +1070,7 @@ impl Desugarer {
/// by [`Desugarer::desugar_match`] to skip the let-binding and chain
/// construction for already-flat matches.
///
/// Iter 16c: [`Pattern::Lit`] is **not** flat — it always desugars to a
/// [`Pattern::Lit`] is **not** flat — it always desugars to a
/// [`Term::If`] via [`build_eq`], so it must take the chain path even
/// when no other arm needs flattening. Otherwise the early-return in
/// [`Desugarer::desugar_match`] would leak a `Pattern::Lit` arm to
@@ -1078,7 +1078,7 @@ impl Desugarer {
fn is_flat(p: &Pattern) -> bool {
match p {
Pattern::Wild | Pattern::Var { .. } => true,
// Iter 16c: lit patterns are not flat; they desugar to If.
// lit patterns are not flat; they desugar to If.
Pattern::Lit { .. } => false,
Pattern::Ctor { fields, .. } => fields
.iter()
@@ -1086,7 +1086,7 @@ fn is_flat(p: &Pattern) -> bool {
}
}
/// Iter 16c: Build an equality-test term for a lit pattern. The shape is
/// Build an equality-test term for a lit pattern. The shape is
/// `(app == scrutinee lit_term)` for Int/Bool/Str. Unit literals are
/// degenerate — every Unit value is equal — so an emitted `true` literal
/// stands in.
@@ -1114,7 +1114,7 @@ fn build_eq(scrutinee: Term, lit: &Literal) -> Term {
}
}
/// Iter 16b.1: collect free variable names of `t`, with `bound` being
/// collect free variable names of `t`, with `bound` being
/// the set of names lexically bound at this point. A
/// [`Term::Var`] `{ name }` is "free" iff `name` is not in `bound`.
/// Compound binders ([`Term::Let`], [`Term::Lam`], [`Term::Match`]
@@ -1123,7 +1123,7 @@ fn build_eq(scrutinee: Term, lit: &Literal) -> Term {
/// Used by the [`Term::LetRec`] desugar to decide whether a local
/// recursive let would capture any name from the enclosing scope.
///
/// Iter 16b.3: made `pub` so the post-typecheck `lift_letrecs` pass
/// made `pub` so the post-typecheck `lift_letrecs` pass
/// in `ailang-check` can reuse it (same free-var computation; the
/// post-typecheck pass needs it to recompute captures of LetRec
/// nodes that desugar deferred).
@@ -1195,11 +1195,11 @@ pub fn free_vars_in_term(t: &Term, bound: &BTreeSet<String>, out: &mut BTreeSet<
free_vars_in_term(in_term, &b_in, out);
}
Term::Clone { value } => {
// Iter 18c.1: `(clone X)` has the same free vars as `X`.
// `(clone X)` has the same free vars as `X`.
free_vars_in_term(value, bound, out);
}
Term::ReuseAs { source, body } => {
// Iter 18d.1: free vars are the union of source and body.
// free vars are the union of source and body.
free_vars_in_term(source, bound, out);
free_vars_in_term(body, bound, out);
}
@@ -1222,11 +1222,11 @@ pub fn free_vars_in_term(t: &Term, bound: &BTreeSet<String>, out: &mut BTreeSet<
}
}
/// Iter 16b.1: collect every name a pattern binds into `out`. Mirrors
/// collect every name a pattern binds into `out`. Mirrors
/// `Pattern::pattern_bound_names` in `ailang-codegen`; duplicated here
/// because `ailang-core` cannot depend on the codegen crate.
///
/// Iter 16b.3: made `pub` so callers (e.g. `ailang-check::lift_letrecs`)
/// made `pub` so callers (e.g. `ailang-check::lift_letrecs`)
/// can reproduce the same shadowing semantics during their own
/// scope-aware walks.
pub fn pattern_binds(p: &Pattern, out: &mut BTreeSet<String>) {
@@ -1243,7 +1243,7 @@ pub fn pattern_binds(p: &Pattern, out: &mut BTreeSet<String>) {
}
}
/// Iter 16b.1: rewrite every free [`Term::Var`] `{ name == from }`
/// rewrite every free [`Term::Var`] `{ name == from }`
/// reference in `t` to [`Term::Var`] `{ name = to }`. Respects
/// shadowing: if a binder rebinds `from`, occurrences inside that
/// binder's scope stop being free and are left alone.
@@ -1252,7 +1252,7 @@ pub fn pattern_binds(p: &Pattern, out: &mut BTreeSet<String>) {
/// fn — every recursive self-call site in the lifted body and every
/// reference in the in-term needs to point at the new global name.
///
/// Iter 16b.3: made `pub` for the same reason as
/// made `pub` for the same reason as
/// [`subst_call_with_extras`].
pub fn subst_var(t: &Term, from: &str, to: &str) -> Term {
match t {
@@ -1355,11 +1355,11 @@ pub fn subst_var(t: &Term, from: &str, to: &str) -> Term {
}
}
Term::Clone { value } => Term::Clone {
// Iter 18c.1: structural recursion through the wrapper.
// structural recursion through the wrapper.
value: Box::new(subst_var(value, from, to)),
},
Term::ReuseAs { source, body } => Term::ReuseAs {
// Iter 18d.1: structural recursion through both children.
// structural recursion through both children.
source: Box::new(subst_var(source, from, to)),
body: Box::new(subst_var(body, from, to)),
},
@@ -1402,7 +1402,7 @@ pub fn subst_var(t: &Term, from: &str, to: &str) -> Term {
}
}
/// Iter 16b.2: peel a `Type::Forall { body: Type::Fn { ... } }` to
/// peel a `Type::Forall { body: Type::Fn { ... } }` to
/// expose the inner `Type::Fn`. Returns `Some(&Type::Fn)` if the
/// type is `Fn` or `Forall<Fn>`; `None` otherwise.
fn peel_forall_to_fn(t: &Type) -> Option<&Type> {
@@ -1413,13 +1413,13 @@ fn peel_forall_to_fn(t: &Type) -> Option<&Type> {
}
}
/// Iter 16b.2: walk `t` and rewrite every `Term::App { callee =
/// walk `t` and rewrite every `Term::App { callee =
/// Var{name}, args }` to `Term::App { callee = Var{lifted}, args =
/// args ++ extras_as_vars }`. Recurses into all sub-terms. Does
/// not touch `Term::Var { name }` in non-callee positions — that's
/// flagged separately by [`find_non_callee_use`].
///
/// Iter 16b.3: made `pub` so the post-typecheck `lift_letrecs` pass
/// made `pub` so the post-typecheck `lift_letrecs` pass
/// in `ailang-check` can reuse it (same call-site rewrite shape; the
/// only difference is that the capture types come from the
/// typechecker's env rather than being statically known).
@@ -1512,11 +1512,11 @@ pub fn subst_call_with_extras(t: &Term, name: &str, lifted: &str, extras: &[Stri
in_term: Box::new(subst_call_with_extras(in_term, name, lifted, extras)),
},
Term::Clone { value } => Term::Clone {
// Iter 18c.1: structural recursion through the wrapper.
// structural recursion through the wrapper.
value: Box::new(subst_call_with_extras(value, name, lifted, extras)),
},
Term::ReuseAs { source, body } => Term::ReuseAs {
// Iter 18d.1: structural recursion through both children.
// structural recursion through both children.
source: Box::new(subst_call_with_extras(source, name, lifted, extras)),
body: Box::new(subst_call_with_extras(body, name, lifted, extras)),
},
@@ -1540,13 +1540,13 @@ pub fn subst_call_with_extras(t: &Term, name: &str, lifted: &str, extras: &[Stri
}
}
/// Iter 16b.2: returns `Some(t)` if `t` contains a `Term::Var {
/// returns `Some(t)` if `t` contains a `Term::Var {
/// name }` reference in a position that is **not** the callee of a
/// `Term::App`. Returns `None` if every reference is in callee
/// position. Used by the LetRec lifter to enforce the "direct-call
/// only" restriction in 16b.2.
///
/// Iter 16b.3: made `pub` for the same reason as
/// made `pub` for the same reason as
/// [`subst_call_with_extras`].
pub fn find_non_callee_use(t: &Term, name: &str) -> Option<Term> {
match t {
@@ -1585,9 +1585,9 @@ pub fn find_non_callee_use(t: &Term, name: &str) -> Option<Term> {
}
Term::LetRec { body, in_term, .. } => find_non_callee_use(body, name)
.or_else(|| find_non_callee_use(in_term, name)),
// Iter 18c.1: clone is identity for the non-callee scan.
// clone is identity for the non-callee scan.
Term::Clone { value } => find_non_callee_use(value, name),
// Iter 18d.1: scan both source and body.
// scan both source and body.
Term::ReuseAs { source, body } => {
find_non_callee_use(source, name).or_else(|| find_non_callee_use(body, name))
}
@@ -1676,7 +1676,7 @@ mod tests {
}
}
/// Iter 16a: a `match` containing `(Cons a (Cons b _))` desugars to
/// a `match` containing `(Cons a (Cons b _))` desugars to
/// a tree with no nested ctor sub-patterns. Property: the rewriter's
/// output never has a `Pattern::Ctor` whose field is itself a
/// `Pattern::Ctor`.
@@ -1804,7 +1804,7 @@ mod tests {
assert!(matches!(body, Term::Match { .. }));
}
/// Iter 16b.1: a [`Term::LetRec`] whose body has no captures from
/// a [`Term::LetRec`] whose body has no captures from
/// the enclosing scope is lifted to a synthetic top-level fn. The
/// resulting module's `defs` grows by one and the original LetRec
/// is gone from the term tree.
@@ -1886,7 +1886,7 @@ mod tests {
}
}
/// Iter 16b.2: a LetRec whose body captures a fn-param of the
/// a LetRec whose body captures a fn-param of the
/// enclosing scope (here, `outer` is a parameter of `main`) is
/// **lifted** with the capture appended to the lifted fn's
/// signature. The original 16b.1 panic ("would capture") is
@@ -2009,7 +2009,7 @@ mod tests {
}
}
/// Iter 16b.3: a LetRec whose body captures a `Term::Let`-bound
/// a LetRec whose body captures a `Term::Let`-bound
/// name is no longer rejected at desugar time. Instead the
/// desugar pass leaves the LetRec in place (with body and
/// in_term recursively desugared) so the post-typecheck pass in
@@ -2088,7 +2088,7 @@ mod tests {
);
}
/// Iter 16b.4: a LetRec whose body captures a name bound by a
/// a LetRec whose body captures a name bound by a
/// `Pattern::Ctor` Var sub-pattern (a `ScopeEntry::MatchArm`
/// binding) is no longer rejected at desugar time. The desugar
/// pass leaves the LetRec in place (with body and in_term
@@ -2205,7 +2205,7 @@ mod tests {
);
}
/// Iter 16b.5: name-as-value INSIDE the LetRec's own body is
/// name-as-value INSIDE the LetRec's own body is
/// still rejected (would require an eta-Lam that calls the
/// pre-lift name — chicken-and-egg with the call-site rewrite).
/// Here `(let g f ...)` binds the LetRec name `f` to a let-bound
@@ -2264,7 +2264,7 @@ mod tests {
let _ = desugar_module(&m);
}
/// Iter 16b.5: name-as-value in the in-clause is now SUPPORTED.
/// name-as-value in the in-clause is now SUPPORTED.
/// The desugar pass lifts the LetRec to a synthetic top-level fn
/// AND wraps the rewritten in-term in `(let f (lam ...) ...)`
/// whose lam eta-expands the lifted fn. After desugar, the
@@ -2369,7 +2369,7 @@ mod tests {
}
}
/// Iter 16b.6: a LetRec inside a polymorphic enclosing fn gets its
/// a LetRec inside a polymorphic enclosing fn gets its
/// fn-param captures lifted with a `Forall(vars, Fn(...))` augmented
/// signature, mirroring the enclosing fn's type vars. Without 16b.6,
/// the desugar pass would have classified the fn-params as
@@ -2510,7 +2510,7 @@ mod tests {
assert_eq!(lifted.params, vec!["k".to_string(), "x".to_string()]);
}
/// Iter 16b.6: a LetRec inside a polymorphic enclosing fn whose
/// a LetRec inside a polymorphic enclosing fn whose
/// `in_term` uses the LetRec name as a value (not as a callee) is
/// rejected. The 16b.5 eta-Lam wrap can't quantify `Forall.vars`
/// because `Term::Lam` has no Forall slot — wrapping a polymorphic
@@ -2569,7 +2569,7 @@ mod tests {
let _ = desugar_module(&m);
}
/// Iter 16b.7: a nested LetRec whose inner LetRec captures the
/// a nested LetRec whose inner LetRec captures the
/// OUTER LetRec's NAME (not its params or any other local) is
/// rejected at desugar time with the closure-of-self message.
/// Capturing the outer's PARAMS is supported (covered by the
@@ -2651,7 +2651,7 @@ mod tests {
let _ = desugar_module(&m);
}
/// Iter 16b.7 (positive companion): a nested LetRec whose inner
/// a nested LetRec whose inner
/// LetRec captures the OUTER LetRec's PARAM (not its name) lifts
/// cleanly through the existing 16b.2 fast path. The outer's
/// params live in the inner's outer-scope as `KnownType`, so the
@@ -2757,7 +2757,7 @@ mod tests {
}
}
/// Iter 16c: walks a term, returns true iff any [`Pattern::Lit`] is
/// walks a term, returns true iff any [`Pattern::Lit`] is
/// reachable in any [`Term::Match`] arm. After 16c desugaring, the
/// invariant is `false` for every desugared output — `Pattern::Lit`
/// is gone before typecheck/codegen runs.
@@ -2808,7 +2808,7 @@ mod tests {
}
}
/// Iter 16c: a top-level lit arm desugars to a `Term::If` whose
/// a top-level lit arm desugars to a `Term::If` whose
/// condition is `(== s_var lit)`. The desugared body must contain
/// no `Pattern::Lit` anywhere.
#[test]
@@ -2876,7 +2876,7 @@ mod tests {
);
}
/// Iter 16c: a `(pat-ctor Cons (pat-lit 0) _)` sub-pattern desugars
/// a `(pat-ctor Cons (pat-lit 0) _)` sub-pattern desugars
/// to a tree with no `Pattern::Lit` anywhere — the lit is rewritten
/// to a `Term::If` against the field-bound fresh variable.
#[test]
@@ -2944,7 +2944,7 @@ mod tests {
);
}
/// Iter 16c regression guard: `is_flat` must classify
/// `is_flat` must classify
/// `Pattern::Lit` as **not** flat, so the chain machinery in
/// [`Desugarer::desugar_match`] is always invoked for lit-arms
/// (rather than the early-return that would leak the lit pattern
@@ -2960,7 +2960,7 @@ mod tests {
);
}
/// Iter 16d: the chain machinery's deepest fall-through is the
/// the chain machinery's deepest fall-through is the
/// polymorphic `__unreachable__` builtin (`forall a. a`), not a
/// `Unit` literal. A match with two lit arms and a wildcard
/// catches all paths via the wild-arm body, so the deepest
+1 -1
View File
@@ -63,7 +63,7 @@ pub fn manifest(m: &Module) -> String {
};
("type", body)
}
// Iter 22b.1: one-line summary `class C a` / `instance C T`.
// one-line summary `class C a` / `instance C T`.
// Full pretty rendering of method signatures and bodies
// lands in 22b.4 alongside the prose projection arms.
Def::Class(c) => ("class", format!("{} {}", c.name, c.param)),
+119 -117
View File
@@ -40,7 +40,7 @@ use std::path::{Path, PathBuf};
/// by `Module.name`. `root_dir` is the directory the entry file lives
/// in; all imports are resolved relative to it.
///
/// Iter 22b.1 (Decision 11): `registry` is the workspace-global
/// `registry` is the workspace-global
/// instance registry, built at the end of [`load_workspace`] after the
/// DFS over imports completes. It is empty for any workspace whose
/// modules contain no [`crate::ast::Def::Instance`] defs.
@@ -55,11 +55,11 @@ pub struct Workspace {
/// Directory the entry file lives in; all imports are resolved
/// relative to it.
pub root_dir: PathBuf,
/// Iter 22b.1: workspace-global typeclass instance registry.
/// workspace-global typeclass instance registry.
pub registry: Registry,
}
/// Iter 22b.1: workspace-global instance registry (Decision 11).
/// workspace-global instance registry (the typeclass design).
///
/// Built at the end of [`load_workspace`] after all modules are
/// loaded. Keyed by `(class-name, canonical-type-hash)`; values are
@@ -71,7 +71,7 @@ pub struct Workspace {
/// 22b.1 enforces three coherence checks during build:
///
/// 1. **Coherence (orphan-freedom).** Every `instance C T` lives in
/// the module of `C` or in the module of `T` (per Decision 11
/// the module of `C` or in the module of `T` (per the typeclass design
/// axis 3). Otherwise → [`WorkspaceLoadError::OrphanInstance`].
/// 2. **Uniqueness.** No two entries share a key. Otherwise →
/// [`WorkspaceLoadError::DuplicateInstance`].
@@ -82,7 +82,7 @@ pub struct Workspace {
pub struct Registry {
/// Map from `(class-name, type-hash)` to the registry entry.
pub entries: BTreeMap<(String, String), RegistryEntry>,
/// ct.1.5a: workspace-wide map from user-defined type-name to its
/// workspace-wide map from user-defined type-name to its
/// defining module. Used by [`Self::normalize_type_for_lookup`] to
/// rewrite a bare `Type::Con.name` to its always-qualified form
/// before computing the registry key. Primitives are not present.
@@ -104,7 +104,7 @@ pub struct Registry {
}
impl Registry {
/// ct.1.5a + ctt.2: produce the canonical form of `t` for
/// the canonical-form normalisation step: produce the canonical form of `t` for
/// registry-key hashing. Bare-non-primitive `Type::Con` names
/// get qualified to `<defining_module>.<name>`; already-qualified
/// names stay; bare names whose defining module is unknown stay
@@ -201,10 +201,11 @@ pub enum WorkspaceLoadError {
)]
ModuleHashMismatch { name: String },
/// Iter 22b.1: an [`crate::ast::Def::Instance`] was declared in a
/// an [`crate::ast::Def::Instance`] was declared in a
/// module that is neither the class's defining module nor the
/// instance type's defining module. Coherence violation per
/// Decision 11 axis 3 ("orphan-freedom"). The lookup is hard:
/// the orphan-freedom axis of the typeclass design. The lookup
/// is hard:
/// AILang does not provide a `--allow-orphans` flag.
#[error(
"orphan instance: `instance {class} {type_repr}` declared in module `{defining_module}`, \
@@ -218,10 +219,10 @@ pub enum WorkspaceLoadError {
type_module: String,
},
/// Iter 22b.1: two [`crate::ast::Def::Instance`]s share the same
/// two [`crate::ast::Def::Instance`]s share the same
/// `(class, canonical-type-hash)` key. Coherence requires
/// uniqueness; the registry has no way to disambiguate at
/// resolution time. Per Decision 11 there is no
/// resolution time. Per the typeclass design there is no
/// `AmbiguousInstance` diagnostic — coherence makes the lookup
/// unambiguous by construction, and a duplicate is a workspace
/// configuration error, not a per-call-site one.
@@ -235,11 +236,11 @@ pub enum WorkspaceLoadError {
second_module: String,
},
/// Iter 22b.1: an [`crate::ast::Def::Instance`] does not specify
/// an [`crate::ast::Def::Instance`] does not specify
/// a body for a required (non-default) method of its class.
/// Default-bearing methods may be inherited; non-default
/// (abstract-required) methods must be specified by every
/// instance. Per Decision 11 §"Defaults and superclasses".
/// instance. Per the typeclass design §"Defaults and superclasses".
#[error(
"instance `{class} {type_repr}` is missing a body for method `{method}` (no default)"
)]
@@ -249,8 +250,8 @@ pub enum WorkspaceLoadError {
method: String,
},
/// Iter 22b.2: class-schema validation. A class's `superclass.type`
/// does not equal its own `param`. Decision 11 single-superclass
/// class-schema validation. A class's `superclass.type`
/// does not equal its own `param`. the typeclass design's single-superclass
/// model requires the superclass to be applied to the same param
/// (e.g. `class Ord a extends Eq a`, not `extends Eq b`).
#[error(
@@ -264,7 +265,7 @@ pub enum WorkspaceLoadError {
got_type: String,
},
/// Iter 22b.2: class-schema validation. A class method's
/// class-schema validation. A class method's
/// signature contains a constraint referencing a type variable
/// that is neither bound by the method's `Forall.vars` nor equal
/// to the class's `param`.
@@ -278,7 +279,7 @@ pub enum WorkspaceLoadError {
var: String,
},
/// Iter 22b.2: an instance specifies a body for a method name
/// an instance specifies a body for a method name
/// that the corresponding class does not declare. Symmetric to
/// `MissingMethod` but in the opposite direction.
#[error(
@@ -290,9 +291,9 @@ pub enum WorkspaceLoadError {
method: String,
},
/// Iter 22b.2: an instance `C T` was declared, but `C`'s
/// an instance `C T` was declared, but `C`'s
/// superclass `S` does not have an instance for the same type
/// `T`. Decision 11 single-superclass model requires `instance S
/// `T`. the typeclass design's single-superclass model requires `instance S
/// T` to exist whenever `instance C T` exists.
#[error(
"instance `{class} {type_repr}` requires superclass instance `{superclass} {type_repr}`, but none was found"
@@ -303,14 +304,14 @@ pub enum WorkspaceLoadError {
type_repr: String,
},
/// Iter 23.1: a user module attempted to use the reserved
/// a user module attempted to use the reserved
/// module name `prelude`. The prelude is auto-injected by
/// the loader, so a user module of the same name would
/// collide silently. Reject explicitly.
#[error("module name {name:?} is reserved (auto-injected by the loader)")]
ReservedModuleName { name: String },
/// ct.1 (canonical-type-names): a `Type::Con` whose `name` is
/// the canonical-form rule for type references: a `Type::Con` whose `name` is
/// neither a primitive nor a local TypeDef of the owning module
/// was encountered. Under the canonical-form rule, bare =
/// local; a bare cross-module ref is a schema violation.
@@ -327,7 +328,7 @@ pub enum WorkspaceLoadError {
candidates: Vec<String>,
},
/// ct.1: a qualified `Type::Con` of the form `<owner>.<type>`
/// a qualified `Type::Con` of the form `<owner>.<type>`
/// was encountered, but `<owner>` is not a known module in the
/// workspace, or `<owner>` is known but declares no TypeDef
/// named `<type>`.
@@ -340,11 +341,11 @@ pub enum WorkspaceLoadError {
name: String,
},
/// mq.1 (canonical-class-names): a class-reference field
/// the canonical-form rule for class references: a class-reference field
/// (`InstanceDef.class`, `Constraint.class`, or
/// `SuperclassRef.class`) carries a bare name that does not resolve
/// to a local class of the owning module. Under the canonical-form
/// rule extended in mq.1, bare = local-class-of-owning-module; a
/// rule extended for class references, bare = local-class-of-owning-module; a
/// bare cross-module class reference is a schema violation.
/// `candidates` lists the qualified forms found by scanning the
/// owning module's imports for matching class declarations.
@@ -359,7 +360,7 @@ pub enum WorkspaceLoadError {
candidates: Vec<String>,
},
/// mq.1 (canonical-class-names): a qualified class reference of
/// the canonical-form rule for class references: a qualified class reference of
/// the form `<owner>.<class>` was encountered, but `<owner>` is
/// not a known module in the workspace, or `<owner>` is known
/// but declares no class by that name. Sibling of
@@ -373,14 +374,14 @@ pub enum WorkspaceLoadError {
name: String,
},
/// ct.1: a class-reference field (`InstanceDef.class`,
/// a class-reference field (`InstanceDef.class`,
/// `SuperclassRef.class`, `Constraint.class`, or
/// `ClassDef.name`) contains a `.` — under this milestone class
/// names are NOT module-qualified (see DESIGN spec §"Out of
/// scope: Class names"). The schema rejects qualified forms so
/// half-migrated files cannot silently load.
///
/// mq.1: narrowed to `ClassDef.name` only; the three other
/// narrowed to `ClassDef.name` only; the three other
/// fields now follow the canonical-form rule and use
/// `BareCrossModuleClassRef` / `BadCrossModuleClassRef`.
#[error(
@@ -497,10 +498,10 @@ pub fn build_workspace(
// `ailang_surface::PRELUDE_AIL` + `ailang_surface::parse_prelude`); core
// exposes the two-phase composition.
/// mq.1: take a class-ref field value (`InstanceDef.class`,
/// take a class-ref field value (`InstanceDef.class`,
/// `SuperclassRef.class`, `Constraint.class`) and a defining context,
/// and produce the qualified workspace key. Bare ⇒ prepend the
/// `caller_module` argument; qualified ⇒ as-is. Symmetric to ct.1's
/// `caller_module` argument; qualified ⇒ as-is. Symmetric to the canonical-form rule's
/// `normalize_type_for_registry` for `Type::Con`.
///
/// For an `InstanceDef.class` or `Constraint.class` field the caller
@@ -514,7 +515,7 @@ fn qualify_class_ref(class_ref: &str, caller_module: &str) -> String {
}
}
/// Iter 22b.1: build the workspace-global typeclass instance registry.
/// build the workspace-global typeclass instance registry.
///
/// Two passes:
///
@@ -534,7 +535,7 @@ fn build_registry(
// Pass 1: collect "where is X defined" maps, plus a class lookup
// by name (needed for the method-completeness check).
//
// mq.1: `class_def_module` and `class_by_name` are keyed by the
// `class_def_module` and `class_by_name` are keyed by the
// qualified class name `<defining_module>.<class>`. All consumers
// (Pass-2 coherence lookup, method-completeness check, superclass
// walk, etc.) query with `qualify_class_ref` applied to the field
@@ -562,7 +563,7 @@ fn build_registry(
}
}
// mq.3: the `MethodNameCollision` pre-pass (variant + Origin enum +
// the `MethodNameCollision` pre-pass (variant + Origin enum +
// per-def loop) was retired here. Bare-method resolution no longer
// requires workspace-wide method-name uniqueness — synth's
// `Term::Var` arm consults `Env.method_to_candidate_classes`
@@ -588,7 +589,7 @@ fn build_registry(
// user-defined module — instances on primitives
// therefore must live in the class's module.
//
// mq.1: lookup keys are qualified
// lookup keys are qualified
// (`<defining_module>.<class>`); the `inst.class`
// field is the canonical-form value (bare or qualified)
// which `qualify_class_ref` lifts to the workspace key.
@@ -597,7 +598,7 @@ fn build_registry(
.get(&inst_class_key)
.cloned()
.unwrap_or_else(|| "<unknown-class>".into());
// mq.1: type-leg lookup must accept the canonical form
// type-leg lookup must accept the canonical form
// for the head name. Bare head ⇒ key by
// (caller_module, head); qualified `<owner>.<bare>` ⇒
// key by (owner, bare) directly (the owner IS the
@@ -625,14 +626,14 @@ fn build_registry(
}
// Uniqueness: a `(class, type-hash)` key must appear
// at most once across the whole workspace. ct.1.5a: the
// at most once across the whole workspace. The
// type expression is normalised to its always-qualified
// form before hashing so a bare-local declaration in
// the type's defining module and a qualified-cross-module
// declaration from elsewhere produce the same key (both
// refer to the same type under the canonical-form rule).
//
// mq.1: registry key is keyed by the qualified class
// registry key is keyed by the qualified class
// form too, so a bare same-module instance and a
// qualified cross-module instance on the same
// (class, type) collide on this check.
@@ -677,7 +678,7 @@ fn build_registry(
// Symmetric to MissingMethod: an instance must
// not specify a body for a method name the class
// never declared. Decision 11 forbids ad-hoc
// never declared. The typeclass design forbids ad-hoc
// additions to a class's method set at the
// instance site.
let declared: BTreeSet<&str> =
@@ -704,11 +705,11 @@ fn build_registry(
}
}
// Iter 22b.2: superclass-instance completeness. For every entry,
// superclass-instance completeness. For every entry,
// walk the class's superclass chain and require an entry for each
// step at the same type-hash.
//
// mq.1: `class_name` (the entries key first half) is the qualified
// `class_name` (the entries key first half) is the qualified
// class name; the superclass-ref field `sc.class` is canonical-form,
// which `qualify_class_ref` lifts to the qualified key — using the
// parent class's defining module as the caller context (the
@@ -716,7 +717,7 @@ fn build_registry(
for (key, entry) in entries.iter() {
let (class_name, type_hash) = key;
let type_repr = type_head_name(&entry.instance.type_);
// Iter 22b.2 leaves superclass-cycle detection to a future arm;
// Superclass-cycle detection is left to a future arm;
// here we just terminate the walk.
let mut visited: BTreeSet<&str> = BTreeSet::new();
let mut current = class_by_name.get(class_name.as_str()).copied();
@@ -738,7 +739,7 @@ fn build_registry(
type_repr: type_repr.clone(),
});
}
// mq.1: walk lookup uses the qualified key; the next
// walk lookup uses the qualified key; the next
// step's owning-module context is the superclass's
// defining module (read from `class_def_module`).
current = class_by_name.get(sc_class_key.as_str()).copied();
@@ -758,7 +759,7 @@ fn build_registry(
})
}
/// Iter 22b.2: class-schema validation. Runs before `build_registry`.
/// class-schema validation. Runs before `build_registry`.
/// Two diagnostics fire from here: `invalid-superclass-param`,
/// `constraint-references-unbound-type-var`. The `kind-mismatch`
/// diagnostic was retired at ctt.3 — the malformed shape now
@@ -805,7 +806,7 @@ fn validate_classdefs(
Ok(())
}
/// ct.1: the five primitive type names that are always bare under
/// the five primitive type names that are always bare under
/// the canonical-form rule. Kept in sync with `Type::int`,
/// `Type::bool_`, `Type::str_`, `Type::unit`, `Type::float` in
/// `crate::ast`.
@@ -813,7 +814,7 @@ fn is_primitive_type_name(name: &str) -> bool {
matches!(name, "Int" | "Bool" | "Str" | "Unit" | "Float")
}
/// ct.1.5a: normalize a `Type` by qualifying every bare-non-primitive
/// normalize a `Type` by qualifying every bare-non-primitive
/// `Type::Con.name` to its always-qualified form
/// (`<defining_module>.<name>`). Primitives stay bare; already-qualified
/// names stay as-is; bare names whose defining module is unknown stay
@@ -891,7 +892,7 @@ fn normalize_type_for_registry(
}
}
/// ct.1: enforce the canonical-form rule on every `Type::Con` and
/// enforce the canonical-form rule on every `Type::Con` and
/// `Term::Ctor.type_name` reference in every loaded module. Runs
/// after prelude injection and before class-schema validation, so a
/// stale bare cross-module ref fires the canonical-form diagnostic
@@ -922,7 +923,7 @@ pub(crate) fn validate_canonical_type_names(
local_types.insert(mod_name.clone(), s);
}
// mq.1: symmetric pre-pass over `Def::Class` names. The map is
// symmetric pre-pass over `Def::Class` names. The map is
// module → bare-class-name set; used by `check_class_ref` to apply
// the canonical-form rule to the three migrated class-ref fields
// (`InstanceDef.class`, `Constraint.class`, `SuperclassRef.class`).
@@ -961,7 +962,7 @@ pub(crate) fn validate_canonical_type_names(
})?;
check_class_name_fields(def, mod_name)?;
// mq.1: apply the canonical-form rule to the three
// apply the canonical-form rule to the three
// migrated class-ref fields.
match def {
Def::Instance(id) => {
@@ -994,7 +995,7 @@ pub(crate) fn validate_canonical_type_names(
Ok(())
}
/// mq.1: apply the canonical-form rule to a class-reference field
/// apply the canonical-form rule to a class-reference field
/// value (`InstanceDef.class`, `Constraint.class`, or
/// `SuperclassRef.class`). Sibling of `check_type_con_name` for
/// class refs.
@@ -1071,7 +1072,7 @@ fn check_class_ref(
})
}
/// ct.1: apply the canonical-form rule to one `Type::Con.name`
/// apply the canonical-form rule to one `Type::Con.name`
/// (also reused for `Term::Ctor.type_name` in Task 2).
fn check_type_con_name(
name: &str,
@@ -1140,7 +1141,7 @@ fn check_type_con_name(
})
}
/// ct.1: walk every `Type` reachable from a single `Def`, calling
/// walk every `Type` reachable from a single `Def`, calling
/// `f` on each. Recurses into `Type::Fn.params/ret`, `Type::Con.args`,
/// `Type::Forall.constraints/body`, plus the obvious top-level fields
/// of each `Def` variant AND every Type annotation embedded in a Term
@@ -1188,7 +1189,7 @@ where
}
}
/// ct.1: walk a `Term` and call `f` on every Type annotation embedded
/// walk a `Term` and call `f` on every Type annotation embedded
/// in it (Lam.param_tys, Lam.ret_ty, LetRec.ty). Recurses through
/// every Term sub-position. Does NOT fire on `Term::Ctor.type_name`
/// (that's a `String`, not a `Type`; handled by `walk_def_terms` in
@@ -1263,7 +1264,7 @@ where
}
}
/// ct.1: recursive walk of a `Type`, calling `f` at every node.
/// recursive walk of a `Type`, calling `f` at every node.
fn walk_type<F>(t: &Type, f: &mut F) -> Result<(), WorkspaceLoadError>
where
F: FnMut(&Type) -> Result<(), WorkspaceLoadError>,
@@ -1292,7 +1293,7 @@ where
}
}
/// ct.1: walk every `Term::Ctor.type_name` reachable from a single
/// walk every `Term::Ctor.type_name` reachable from a single
/// `Def`, calling `f` on the type_name strings. Used to enforce the
/// canonical-form rule on term-side type references.
fn walk_def_terms<F>(def: &Def, f: &mut F) -> Result<(), WorkspaceLoadError>
@@ -1320,7 +1321,7 @@ where
}
}
/// ct.1: recursive walk of a `Term`, calling `f` on every
/// recursive walk of a `Term`, calling `f` on every
/// `Term::Ctor.type_name`. Embedded `Type` annotations (Lam param /
/// return types, LetRec types) ride the `walk_def_types` /
/// `walk_term_embedded_types` path — but `Term::Ctor.type_name` is
@@ -1397,7 +1398,7 @@ where
}
}
/// ct.1: Pattern::Ctor carries a `ctor` name (matches against a
/// Pattern::Ctor carries a `ctor` name (matches against a
/// scrutinee's TypeDef) but NOT a type_name field — the type is
/// inferred from the scrutinee. So Pattern walking only recurses;
/// no canonical-form check fires here. `f` is kept in the signature
@@ -1419,11 +1420,11 @@ where
}
}
/// ct.1: reject any `.` in `ClassDef.name`. The defining-site name is
/// reject any `.` in `ClassDef.name`. The defining-site name is
/// bare by convention (symmetric to `TypeDef.name`); a qualified form
/// indicates a malformed file.
///
/// mq.1: narrowed from the four class-reference fields to
/// narrowed from the four class-reference fields to
/// `ClassDef.name` only. The three referencing fields
/// (`InstanceDef.class`, `Constraint.class`, `SuperclassRef.class`)
/// now follow the canonical-form rule and are validated by
@@ -1445,14 +1446,15 @@ fn check_class_name_fields(
Ok(())
}
/// Iter 22b.1: extract the head-constructor name of a type, for the
/// extract the head-constructor name of a type, for the
/// "where is this type defined" lookup and for diagnostic-message
/// rendering.
///
/// For `Type::Con { name, .. }` (the only legal head shape for a
/// non-orphan instance) returns `name`. Other variants (`Var`,
/// `Forall`, `Fn`) are not legal as instance heads — Decision 11
/// requires a concrete type expression at the instance head — so we
/// `Forall`, `Fn`) are not legal as instance heads — the typeclass
/// design requires a concrete type expression at the instance head —
/// so we
/// emit a stable fallback string. The fallback prevents diagnostic
/// rendering from panicking on a malformed fixture; the "real"
/// rejection of non-concrete instance heads will arrive as a
@@ -1640,7 +1642,7 @@ mod tests {
// ailang-surface dev-dep cycle disallows `surface::load_workspace`
// calls from this in-mod test crate).
// Iter 22b.1: a workspace whose own modules contain no
// a workspace whose own modules contain no
// `Def::Instance` defs produces no non-prelude registry entries.
// This is the happy-path baseline for the registry-build pass —
// every pre-22b workspace falls into this case. With the
@@ -1660,7 +1662,7 @@ mod tests {
.join("examples")
}
// Iter 22b.1: a coherent instance (in the class's module)
// a coherent instance (in the class's module)
// loads cleanly and produces one registry entry from the
// fixture itself. With the auto-loaded prelude (iter 23.2)
// the registry also contains the prelude's own entries; the
@@ -1668,7 +1670,7 @@ mod tests {
// `iter22b1_instance_in_class_module_loads_clean` relocated to
// `crates/ailang-core/tests/workspace_pin.rs` in iter form-a.1 Task 5.
// Iter 22b.1: an instance declared in a module that is neither
// an instance declared in a module that is neither
// the class's module nor the type's module fires `OrphanInstance`.
// The fixture imports `test_22b1_orphan_third_classmod` (which
// owns `class TShow`) and the entry module declares `instance
@@ -1678,17 +1680,17 @@ mod tests {
// `iter22b1_orphan_instance_fires_diagnostic` relocated to
// `crates/ailang-core/tests/workspace_pin.rs` in iter form-a.1 Task 5.
// Iter 22b.1 / mq.1: two instances of the same `(class, type)`
// pair collide on the registry's uniqueness check.
// Two instances of the same `(class, type)` pair collide on the
// registry's uniqueness check.
//
// Pre-mq.1 the test used a two-module fixture
// Pre-canonical-class-form the test used a two-module fixture
// (`test_22b1_dup_a` declared the class + first instance,
// `test_22b1_dup_b` declared the type + second instance) which
// relied on bare cross-module class refs. The mq.1
// relied on bare cross-module class refs. The canonical-form rule
// canonical-form rule makes that shape structurally
// unrepresentable (any second instance in a module that owns
// neither the class nor the type fires `OrphanInstance` first).
// Post-mq.1 the only way to land two instances on the same
// Post-canonical-class-form the only way to land two instances on the same
// canonical key is to have them in the same module (the class's
// or the type's module). The fixture now declares both
// instances in `test_22b1_dup_same_module` — both class-leg
@@ -1697,7 +1699,7 @@ mod tests {
// `iter22b1_duplicate_instance_fires_diagnostic` relocated to
// `crates/ailang-core/tests/workspace_pin.rs` in iter form-a.1 Task 5.
// Iter 22b.1: an instance that omits a required (non-default)
// an instance that omits a required (non-default)
// method of its class fires `MissingMethod`. The fixture's
// `class TEq` declares `teq` and `tne` as both non-default; the
// instance only specifies `tne`, leaving `teq` missing.
@@ -1713,13 +1715,13 @@ mod tests {
// pd.2 (post-shim retirement; in-mod tests cannot reach
// `ailang_surface::load_workspace` due to the dev-dep cycle).
// Iter 22b.2: an instance that specifies a body for a method
// an instance that specifies a body for a method
// name the class never declared must fire
// `OverridingNonExistentMethod`. Symmetric counterpart to
// `MissingMethod`: the latter fires when the class declares a
// non-default method that the instance omits; this one fires
// when the instance provides a body the class did not ask for.
// Decision 11 forbids ad-hoc additions to a class's method set
// The typeclass design forbids ad-hoc additions to a class's method set
// at the instance site.
// (Class is `TEq` rather than `Eq` to avoid colliding with the
// auto-loaded prelude's `class Eq`.)
@@ -1730,20 +1732,20 @@ mod tests {
// relocated to `crates/ailang-core/tests/workspace_pin.rs` in iter
// pd.2.
// mq.3: the two `..._method_name_collision_fires` pin tests
// the two `..._method_name_collision_fires` pin tests
// (class-class and class-fn variants) were retired here and
// re-located as positive-load tests in
// `crates/ailang-check/tests/method_collision_pin.rs`. Post-
// mq.3 those on-disk fixtures load cleanly and the equivalent
// Now those on-disk fixtures load cleanly and the equivalent
// observations move to `env.method_to_candidate_classes`
// (multi-entry set) plus the call-site warning.
// Iter 22b.2: an instance `C T` whose class `C` declares a
// an instance `C T` whose class `C` declares a
// superclass `S` requires that `instance S T` also exist in the
// workspace. The fixture declares `class TEq a`, `class TOrd a
// extends TEq a`, and `instance TOrd Int` — but no `instance TEq
// Int` — so registry build must fire
// `MissingSuperclassInstance`. Decision 11 single-superclass
// `MissingSuperclassInstance`. the typeclass design's single-superclass
// model requires `instance S T` whenever `instance C T` exists.
// (Classes are `TEq` / `TOrd` rather than `Eq` / `Ord` to avoid
// colliding with the auto-loaded prelude's `class Eq`.)
@@ -1812,7 +1814,7 @@ mod tests {
})).unwrap()
}
/// ct.1: a `Type::Con` whose `name` is a primitive (`Int` / `Bool` /
/// a `Type::Con` whose `name` is a primitive (`Int` / `Bool` /
/// `Str` / `Unit` / `Float`) must be accepted bare. The five
/// primitive names are the only legal bare-non-local Type::Con names
/// under the canonical-form rule.
@@ -1824,7 +1826,7 @@ mod tests {
validate_canonical_type_names(&modules, &["prelude"]).expect("Float must be accepted");
}
/// ct.1: a bare Type::Con whose `name` matches a local TypeDef in
/// a bare Type::Con whose `name` matches a local TypeDef in
/// the same module must be accepted (the canonical-form rule: bare =
/// local).
#[test]
@@ -1834,7 +1836,7 @@ mod tests {
.expect("local Foo must be accepted");
}
/// ct.1: a bare Type::Con whose `name` is neither a primitive nor a
/// a bare Type::Con whose `name` is neither a primitive nor a
/// local TypeDef must fire `BareCrossModuleTypeRef`. With no imports,
/// the candidates list is empty.
#[test]
@@ -1853,7 +1855,7 @@ mod tests {
}
}
/// ct.1: a bare Type::Con whose `name` resolves to one imported
/// a bare Type::Con whose `name` resolves to one imported
/// module's TypeDef must fire `BareCrossModuleTypeRef` with that
/// qualified form in `candidates` (so the diagnostic can suggest the
/// fix).
@@ -1873,7 +1875,7 @@ mod tests {
}
}
/// ct.1: a qualified Type::Con `<owner>.<type>` where `<owner>` is a
/// a qualified Type::Con `<owner>.<type>` where `<owner>` is a
/// known module AND `<type>` is one of its TypeDefs must be accepted.
#[test]
fn ct1_validator_accepts_qualified_xmod_ref() {
@@ -1884,7 +1886,7 @@ mod tests {
.expect("other.Ordering must be accepted");
}
/// ct.1: a qualified Type::Con `<owner>.<type>` where `<owner>` is
/// a qualified Type::Con `<owner>.<type>` where `<owner>` is
/// NOT a known module must fire `BadCrossModuleTypeRef`. Symmetric
/// case: `<owner>` known but no TypeDef `<type>` in it.
#[test]
@@ -1901,7 +1903,7 @@ mod tests {
}
}
/// ct.1: a Type::Con embedded inside a `Term::Lam.param_tys` is a
/// a Type::Con embedded inside a `Term::Lam.param_tys` is a
/// Type-position occurrence, just inside a Term tree. The validator
/// must walk into Lam-internal types so an LLM author can't smuggle
/// a bare cross-module ref past it by hiding it in a lambda
@@ -1939,7 +1941,7 @@ mod tests {
}
}
/// ct.1: a `Term::Ctor` whose `type_name` is a bare cross-module ref
/// a `Term::Ctor` whose `type_name` is a bare cross-module ref
/// must fire `BareCrossModuleTypeRef`. Symmetric to the Type::Con
/// rule but the field lives on Term, not Type.
#[test]
@@ -1980,7 +1982,7 @@ mod tests {
}
}
/// ct.1: a qualified `ClassDef.name` (e.g. `other.Eq`) must fire
/// a qualified `ClassDef.name` (e.g. `other.Eq`) must fire
/// `QualifiedClassName`. Class names stay bare in this milestone.
#[test]
fn ct1_validator_rejects_qualified_classdef_name() {
@@ -2009,9 +2011,9 @@ mod tests {
}
}
/// mq.1: a qualified `InstanceDef.class` referencing a class
/// declared in another known module is the canonical form post-mq.1
/// and is accepted by the validator. Inverted from the pre-mq.1
/// a qualified `InstanceDef.class` referencing a class
/// declared in another known module is the canonical form post-canonical-class-form
/// and is accepted by the validator. Inverted from the pre-canonical-class-form
/// `ct1_validator_rejects_qualified_instancedef_class` test:
/// `InstanceDef.class` moved bare→canonical.
#[test]
@@ -2042,11 +2044,11 @@ mod tests {
modules.insert("other".to_string(), other);
modules.insert("m".to_string(), m);
validate_canonical_type_names(&modules, &["prelude"])
.expect("qualified InstanceDef.class is the canonical form post-mq.1");
.expect("qualified InstanceDef.class is the canonical form post-canonical-class-form");
}
/// mq.1: a qualified `SuperclassRef.class` referencing a class in
/// another known module is the canonical form post-mq.1 and is
/// a qualified `SuperclassRef.class` referencing a class in
/// another known module is the canonical form post-canonical-class-form and is
/// accepted. Inverted from
/// `ct1_validator_rejects_qualified_superclassref_class`.
#[test]
@@ -2078,12 +2080,12 @@ mod tests {
modules.insert("other".to_string(), other);
modules.insert("m".to_string(), m);
validate_canonical_type_names(&modules, &["prelude"])
.expect("qualified SuperclassRef.class is the canonical form post-mq.1");
.expect("qualified SuperclassRef.class is the canonical form post-canonical-class-form");
}
/// mq.1: a qualified `Constraint.class` (inside a `Type::Forall`)
/// a qualified `Constraint.class` (inside a `Type::Forall`)
/// referencing a class in another known module is the canonical
/// form post-mq.1 and is accepted. Inverted from
/// form post-canonical-class-form and is accepted. Inverted from
/// `ct1_validator_rejects_qualified_constraint_class`.
#[test]
fn ct1_validator_accepts_qualified_constraint_class() {
@@ -2124,17 +2126,17 @@ mod tests {
modules.insert("other".to_string(), other);
modules.insert("m".to_string(), m);
validate_canonical_type_names(&modules, &["prelude"])
.expect("qualified Constraint.class is the canonical form post-mq.1");
.expect("qualified Constraint.class is the canonical form post-canonical-class-form");
}
/// ct.1.5a: registry-side duplicate detection survives the
/// registry-side duplicate detection survives the
/// asymmetric canonical-form representation. Two coherent instances
/// on the same type-def, one declared bare-local (in the type's
/// defining module) and one declared qualified-cross-module (in the
/// class's defining module), must collide on the registry's
/// `(class, type-hash)` key.
///
/// This is the regression that broke during the ct.1.5 migration
/// This is the regression that broke during the canonical-form migration
/// dry-run: after migrating `test_22b1_dup_a.ail.json` to qualified
/// `test_22b1_dup_b.MyInt`, the unmigrated `test_22b1_dup_b.ail.json`
/// (which keeps bare `MyInt` because the type IS local there)
@@ -2185,7 +2187,7 @@ mod tests {
// Module `other`: declares `type MyInt` and the qualified-
// cross-module instance `instance cls.TShow MyInt`. Imports
// `cls` for the class ref. The `class` field carries the
// canonical form (qualified for cross-module per mq.1); the
// canonical form (qualified for cross-module per the canonical-class-form rule); the
// `type` field stays bare-local.
let other: Module = serde_json::from_value(serde_json::json!({
"schema": crate::SCHEMA,
@@ -2231,7 +2233,7 @@ mod tests {
}
}
/// ct.1.5a follow-up: `normalize_type_for_registry` must recurse into
/// canonical-form normalisation follow-up: `normalize_type_for_registry` must recurse into
/// `Type::Forall.constraints[].type_` just like it does into
/// `Type::Forall.body`. A bare `Type::Con` nested inside a Forall
/// constraint that lives in a different module must be rewritten to
@@ -2291,14 +2293,14 @@ mod tests {
}
}
/// ct.1: a qualified `Constraint.class` nested inside a
/// a qualified `Constraint.class` nested inside a
/// `ClassDef.methods[].ty.Forall.constraints` must fire
/// `QualifiedClassName`. Distinct from the `Def::Fn` site: the
/// `Def::Class` branch's per-method Forall walk needs independent
/// coverage.
///
/// mq.1: inverted — qualified `Constraint.class` inside a
/// `ClassDef.methods` Forall is the canonical form post-mq.1 and is
/// inverted — qualified `Constraint.class` inside a
/// `ClassDef.methods` Forall is the canonical form post-canonical-class-form and is
/// accepted by the validator.
#[test]
fn ct1_validator_accepts_qualified_constraint_class_in_classdef_method() {
@@ -2343,37 +2345,37 @@ mod tests {
modules.insert("other".to_string(), other);
modules.insert("m".to_string(), m);
validate_canonical_type_names(&modules, &["prelude"])
.expect("qualified Constraint.class in ClassDef-method Forall is the canonical form post-mq.1");
.expect("qualified Constraint.class in ClassDef-method Forall is the canonical form post-canonical-class-form");
}
/// ct.1: on-disk fixture for `BareCrossModuleTypeRef`. Bare
/// on-disk fixture for `BareCrossModuleTypeRef`. Bare
/// `Ordering` Term::Ctor with no imports; the validator catches it
/// after prelude injection (so the candidate list contains
/// `prelude.Ordering`).
// `ct1_fixture_bare_xmod_rejected` relocated to
// `crates/ailang-core/tests/workspace_pin.rs` in iter pd.2.
/// ct.1: on-disk fixture for `BadCrossModuleTypeRef`. Qualified
/// on-disk fixture for `BadCrossModuleTypeRef`. Qualified
/// `Mystery.Type` with `Mystery` not a known module.
// `ct1_fixture_bad_qualifier` relocated to
// `crates/ailang-core/tests/workspace_pin.rs` in iter pd.2.
/// mq.1: on-disk fixture for the post-mq.1 rejection path. The
/// on-disk fixture for the post-canonical-class-form rejection path. The
/// fixture declares `instance prelude.Eq Int` outside the prelude
/// and outside Int's defining module — under the canonical-form
/// rule the qualified `prelude.Eq` ref is now schema-valid (post-
/// mq.1), and the downstream coherence check rejects the instance
/// class references in canonical form), and the downstream coherence check rejects the instance
/// with `OrphanInstance` instead.
///
/// Pre-mq.1 this test asserted `QualifiedClassName` on the same
/// Pre-canonical-class-form this test asserted `QualifiedClassName` on the same
/// fixture; the rename + reshape is the on-disk-fixture half of
/// the four in-test inversions further up.
// `ct1_fixture_qualified_class_orphan_post_mq1` relocated to
// `crates/ailang-core/tests/workspace_pin.rs` in iter pd.2.
// mq.1: on-disk fixture pin — a workspace where the consumer's
// on-disk fixture pin — a workspace where the consumer's
// `Constraint.class` references a class in an imported module via
// the qualified form loads cleanly. Symmetric to ct.1's positive
// the qualified form loads cleanly. Symmetric to the canonical-form rule's positive
// cross-module type-ref fixture (`ct1_validator_accepts_qualified_xmod_ref`
// in-test sibling). Guards the full load → validator → registry
// path on a real on-disk pair.
@@ -2427,7 +2429,7 @@ mod tests {
format!(r#"{{"schema":"ailang/v0","name":"{name}","imports":[],"defs":[]}}"#)
}
/// mq.1.1: `BareCrossModuleClassRef` is the sibling diagnostic for
/// `BareCrossModuleClassRef` is the sibling diagnostic for
/// bare cross-module class references on `InstanceDef.class`,
/// `Constraint.class`, and `SuperclassRef.class`. Verifies the
/// variant is constructible and its Display surface names the
@@ -2445,7 +2447,7 @@ mod tests {
assert!(rendered.contains("prelude.Show"), "Display must list candidates, got: {rendered}");
}
/// mq.1.1b: `BadCrossModuleClassRef` is the sibling diagnostic for
/// `BadCrossModuleClassRef` is the sibling diagnostic for
/// qualified class references whose owner module is unknown or
/// declares no class by that name. Verifies the variant is
/// constructible and its Display surface names the offending
@@ -2462,7 +2464,7 @@ mod tests {
"Display must mention class or module context, got: {rendered}");
}
/// mq.1.3: `InstanceDef.class` carrying a bare name that does NOT
/// `InstanceDef.class` carrying a bare name that does NOT
/// resolve to a local class of the owning module must fire
/// `BareCrossModuleClassRef`. The fixture imports a sibling module
/// that declares the class under the bare name, so the candidate
@@ -2505,7 +2507,7 @@ mod tests {
}
}
/// mq.1.3: `Constraint.class` on a `Def::Fn` carrying a bare name
/// `Constraint.class` on a `Def::Fn` carrying a bare name
/// that does not resolve to a local class fires
/// `BareCrossModuleClassRef`.
#[test]
@@ -2558,7 +2560,7 @@ mod tests {
}
}
/// mq.1.3: `SuperclassRef.class` on a `Def::Class` carrying a bare
/// `SuperclassRef.class` on a `Def::Class` carrying a bare
/// name that does not resolve to a local class fires
/// `BareCrossModuleClassRef`.
#[test]
@@ -2599,9 +2601,9 @@ mod tests {
}
}
/// mq.1.3: a qualified `InstanceDef.class` referencing a class in
/// an imported module is the canonical form post-mq.1 and is
/// accepted by `validate_canonical_type_names`. Symmetric to ct.1's
/// a qualified `InstanceDef.class` referencing a class in
/// an imported module is the canonical form post-canonical-class-form and is
/// accepted by `validate_canonical_type_names`. Symmetric to the canonical-form rule's
/// "qualified Type::Con resolves" positive path.
#[test]
fn mq1_qualified_instancedef_class_accepted() {
@@ -2665,7 +2667,7 @@ mod tests {
fn module_with_bare_classref(name: &str, class_ref: &str) -> Module {
// A module containing a single Def::Instance whose `class` field is
// a bare class reference. The instance's `type` field is a local
// ADT defined in the same module to keep ct.1 happy.
// ADT defined in the same module to keep the canonical-form rule satisfied.
serde_json::from_value(serde_json::json!({
"schema": crate::SCHEMA,
"name": name,