diff --git a/bench/orchestrator-stats/2026-05-28-iter-prep.1-type-scoped-namespacing.json b/bench/orchestrator-stats/2026-05-28-iter-prep.1-type-scoped-namespacing.json new file mode 100644 index 0000000..a3e5baa --- /dev/null +++ b/bench/orchestrator-stats/2026-05-28-iter-prep.1-type-scoped-namespacing.json @@ -0,0 +1,25 @@ +{ + "iter_id": "prep.1-type-scoped-namespacing", + "date": "2026-05-28", + "mode": "standard", + "outcome": "DONE", + "tasks_total": 5, + "tasks_completed": 5, + "reloops_per_task": { + "1": 0, + "2": 0, + "3": 0, + "4": 0, + "5": 0 + }, + "review_loops_spec": 0, + "review_loops_quality": 0, + "blocked_reason": null, + "notes": [ + "Task 1 + Task 2: clean per the plan; one test-pin update outside the plan's enumerated files (unknown_module_prefix_is_reported narrowed to type-scoped-receiver-not-a-type).", + "Task 2: bare-Term::Ctor implicit-prelude test flipped to acceptance (semantic consequence of Step 3 widening); fixture `examples/test_ct1_bare_xmod_rejected.ail.json` swapped to a still-unresolvable name (Mystery_Type) per plan Task-3 Step-1's branch but executed in Task 2 for regression-cleanliness.", + "Task 4 (MAJOR concern): mechanical fixture rewrite required substantial unplanned language-pipeline integration extensions: (a) Term::Ctor arm extended with TypeDef-first ladder, (b) check_type_well_formed extended with workspace-wide TypeDef-first lookup for bare Type::Con, (c) mono poly_free_fn name/ccount builders extended with type-scoped spellings, (d) codegen lookup_ctor_by_type bare path extended with workspace-wide fallback, (e) NEW prepare_workspace_for_check pre-pass shared between check and mono that desugars + qualifies bare cross-module Type::Con and Term::Ctor.type_name to qualified form. Plan's spec/architecture covered only Term::Var dot-qualified arm + workspace validator; Task 4's migration of bare-form fixtures forced the symmetric extensions across every other site where bare vs. qualified type-names are compared. Forward-fix rather than BLOCKED to preserve iter momentum and because each extension is consistent with prep.1's architectural thesis.", + "Test pin updates beyond the plan: crates/ailang-check/tests/workspace.rs::unknown_module_prefix_is_reported; in-source ct1_validator_rejects_bare_term_ctor_type_name flipped + ct1_validator_rejects_bare_xmod_with_import_candidate renamed; ct1_fixture_bare_xmod_rejected message + fixture content updated; crates/ailang-check/src/lib.rs::ct2_term_ctor_bare_cross_module_fails_closed reframed + companion ct2_term_ctor_bare_cross_module_via_workspace_resolves added.", + "Full workspace test suite green (87 e2e + every crate's unit + integration tests)." + ] +} diff --git a/crates/ail/src/main.rs b/crates/ail/src/main.rs index 37a8161..0162912 100644 --- a/crates/ail/src/main.rs +++ b/crates/ail/src/main.rs @@ -1250,9 +1250,9 @@ fn workspace_error_to_diagnostic( ailang_check::Diagnostic::error( "bare-cross-module-type-ref", format!( - "module `{module}` contains bare type name `{name}` that does not resolve to a local type; \ - candidates from imports: {candidates:?}. \ - Run `ail migrate-canonical-types` to fix legacy fixtures." + "module `{module}` references bare type `{name}`, which is not in scope. \ + Add `(import )` to bring it into scope (candidates: {candidates:?}), \ + or rewrite the call to type-scoped form `.`." ), ) .with_ctx(serde_json::json!({ @@ -1267,8 +1267,9 @@ fn workspace_error_to_diagnostic( ailang_check::Diagnostic::error( "bad-cross-module-type-ref", format!( - "module `{module}` references qualified type `{name}` but the owner module is not known \ - or does not declare a type by that name" + "module `{module}` references qualified type `{name}` but the owner module \ + is not known in the workspace, or it declares no type by that name. \ + Use the bare type-name from an imported module instead." ), ) .with_ctx(serde_json::json!({ diff --git a/crates/ail/tests/ct1_check_cli.rs b/crates/ail/tests/ct1_check_cli.rs index 1c07bca..22b8bff 100644 --- a/crates/ail/tests/ct1_check_cli.rs +++ b/crates/ail/tests/ct1_check_cli.rs @@ -29,12 +29,14 @@ fn examples_dir() -> PathBuf { } /// Property: a workspace whose entry module contains a bare -/// cross-module Type::Con / Term::Ctor reference — here `Ordering`, -/// satisfiable only via the auto-injected `prelude` — is rejected by -/// `ail check --json` with diagnostic code `bare-cross-module-type-ref` -/// and non-zero exit. Guards against `workspace_error_to_diagnostic` -/// losing the `BareCrossModuleTypeRef` arm or the validator no longer -/// firing through the CLI loader path. +/// cross-module Type::Con / Term::Ctor reference — here `Mystery_Type`, +/// a name no module in the workspace declares (post-prep.1: in-scope +/// bare names are accepted, so the fixture uses an unresolvable name +/// to keep firing the diagnostic) — is rejected by `ail check --json` +/// with diagnostic code `bare-cross-module-type-ref` and non-zero +/// exit. Guards against `workspace_error_to_diagnostic` losing the +/// `BareCrossModuleTypeRef` arm or the validator no longer firing +/// through the CLI loader path. #[test] fn check_json_emits_bare_cross_module_type_ref() { let fixture = examples_dir().join("test_ct1_bare_xmod_rejected.ail.json"); @@ -148,12 +150,12 @@ fn check_human_mode_emits_actionable_message_to_stderr() { ); let stderr = String::from_utf8(output.stderr).expect("stderr is utf-8"); assert!( - stderr.contains("Ordering"), + stderr.contains("Mystery_Type"), "expected the offending type name in stderr; got {stderr}" ); assert!( - stderr.contains("ail migrate-canonical-types"), - "expected the migration-command hint in stderr; got {stderr}" + stderr.contains("not in scope"), + "expected the narrowed not-in-scope wording in stderr; got {stderr}" ); } diff --git a/crates/ail/tests/e2e.rs b/crates/ail/tests/e2e.rs index c44f0ed..0284a3c 100644 --- a/crates/ail/tests/e2e.rs +++ b/crates/ail/tests/e2e.rs @@ -361,13 +361,12 @@ fn parameterised_maybe_match() { /// cross-module reference to a parameterised ADT, including /// its ctors and a polymorphic combinator instantiated at `(Int, Int)`. -/// `std_maybe_demo` imports `std_maybe`, qualifies the type-name slot -/// of every `term-ctor` (`std_maybe.Maybe`), and exercises -/// `from_maybe`, `is_some`, `is_none`, and `map_maybe` once each. -/// Property protected: the qualified-only convention (the -/// authoring surface's architectural pin extended to types and -/// ctors per the brief) -/// flows end-to-end through check, codegen, and runtime. +/// `std_maybe_demo` imports `std_maybe` and (prep.1 migration) uses +/// the type-scoped form: bare `Maybe` at every `term-ctor` type-name +/// slot, `Maybe.from_maybe` / `Maybe.is_some` etc. for the +/// combinators. Exercises four combinators once each. Property +/// protected: prep.1's type-scoped namespacing flows end-to-end +/// through check, codegen, and runtime. #[test] fn cross_module_maybe_demo() { let stdout = build_and_run("std_maybe_demo.ail"); @@ -376,12 +375,13 @@ fn cross_module_maybe_demo() { } /// drives the polymorphic `std_list` combinators end-to-end. -/// Exercises a recursive cross-module ADT (`std_list.List`) consumed -/// from a separate module that also imports `std_maybe`. Guards the -/// `qualify_local_types` propagation in both `Term::Ctor` synth and -/// `Term::Match` field binding — without it, recursive ctor fields -/// (`Cons a (List a)`) stay unqualified at the cross-module use site -/// and fail to unify against the qualified scrutinee args. +/// Exercises a recursive cross-module ADT (`List` from `std_list`, +/// prep.1 type-scoped form) consumed from a separate module that +/// also imports `std_maybe`. Guards the `qualify_local_types` / +/// `qualify_workspace_types` propagation in both `Term::Ctor` synth +/// and `Term::Match` field binding — without it, recursive ctor +/// fields (`Cons a (List a)`) stay unqualified at the cross-module +/// use site and fail to unify against the qualified scrutinee args. #[test] fn std_list_demo() { let stdout = build_and_run("std_list_demo.ail"); diff --git a/crates/ailang-check/src/lib.rs b/crates/ailang-check/src/lib.rs index 7e855e9..e865c31 100644 --- a/crates/ailang-check/src/lib.rs +++ b/crates/ailang-check/src/lib.rs @@ -685,6 +685,25 @@ pub enum CheckError { #[error("`recur` must be in tail position of its enclosing `loop` body — it is a back-jump, not a value-producing sub-expression")] RecurNotInTailPosition, + /// prep.1 (kernel-extension-mechanics): a dot-qualified + /// `Term::Var` whose receiver is a known `TypeDef` but the suffix + /// does not name a def in that type's home module. Code: + /// `type-scoped-member-not-found`. + #[error("type `{type_name}` (home module `{home_module}`) has no member `{member}`")] + TypeScopedMemberNotFound { + type_name: String, + member: String, + home_module: String, + }, + + /// prep.1 (kernel-extension-mechanics): a dot-qualified + /// `Term::Var` whose receiver is neither a known `TypeDef` nor an + /// imported module. Code: `type-scoped-receiver-not-a-type`. + #[error("`{name}` is neither a known type nor an imported module")] + TypeScopedReceiverNotAType { + name: String, + }, + /// an internal invariant in the typechecker / mono pass /// was violated — surfaced as an error so callers can propagate /// rather than abort, but in well-formed inputs (typecheck has @@ -740,6 +759,8 @@ impl CheckError { CheckError::RecurArityMismatch { .. } => "recur-arity-mismatch", CheckError::RecurTypeMismatch { .. } => "recur-type-mismatch", CheckError::RecurNotInTailPosition => "recur-not-in-tail-position", + CheckError::TypeScopedMemberNotFound { .. } => "type-scoped-member-not-found", + CheckError::TypeScopedReceiverNotAType { .. } => "type-scoped-receiver-not-a-type", CheckError::Internal(_) => "internal", } } @@ -811,6 +832,12 @@ impl CheckError { CheckError::RecurTypeMismatch { position, expected, got } => { serde_json::json!({"position": position, "expected": expected, "actual": got}) } + CheckError::TypeScopedMemberNotFound { type_name, member, home_module } => { + serde_json::json!({"type": type_name, "member": member, "home_module": home_module}) + } + CheckError::TypeScopedReceiverNotAType { name } => { + serde_json::json!({"name": name}) + } _ => serde_json::Value::Object(serde_json::Map::new()), } } @@ -944,6 +971,55 @@ pub fn check_module(m: &Module) -> Vec { /// Top-level API for cross-module typecheck. /// +/// prep.1 (kernel-extension-mechanics): apply the pre-typecheck +/// preparation steps the workspace needs both for typechecking and +/// monomorphisation: +/// +/// 1. Desugar every module via `ailang_core::desugar::desugar_module`. +/// 2. Normalize every consumer module's bare cross-module `Type::Con` +/// references to qualified `.` form (so consumer-side +/// declared types unify with imported-fn signatures, which the +/// existing [`qualify_local_types`] step already qualifies at the +/// owner's side). +/// +/// Both [`check_workspace`] and [`monomorphise_workspace`] call this +/// helper at their entry. The registry passes through unchanged. +pub fn prepare_workspace_for_check(ws: &Workspace) -> Workspace { + let workspace_types_pre: BTreeMap> = + ws.modules + .iter() + .map(|(name, m)| { + let mut tys: IndexMap = IndexMap::new(); + for def in &m.defs { + if let Def::Type(td) = def { + tys.insert(td.name.clone(), td.clone()); + } + } + (name.clone(), tys) + }) + .collect(); + Workspace { + entry: ws.entry.clone(), + modules: ws + .modules + .iter() + .map(|(k, m)| { + let m = ailang_core::desugar::desugar_module(m); + let own_local_types = workspace_types_pre + .get(k) + .cloned() + .unwrap_or_default(); + ( + k.clone(), + qualify_workspace_module(m, &own_local_types, &workspace_types_pre), + ) + }) + .collect(), + root_dir: ws.root_dir.clone(), + registry: ws.registry.clone(), + } +} + /// Iterates over all modules of the workspace and checks each with access /// to the top-level symbol tables of all other modules. Qualified /// references are resolved via the import map of the respective module: @@ -984,20 +1060,17 @@ pub fn check_workspace(ws: &Workspace) -> Vec { // logic runs. The rewrite is pure and per-module; we rebuild a // workspace shell around the desugared modules (paths and entry // are unchanged). - let ws_owned = Workspace { - entry: ws.entry.clone(), - modules: ws - .modules - .iter() - .map(|(k, m)| (k.clone(), ailang_core::desugar::desugar_module(m))) - .collect(), - root_dir: ws.root_dir.clone(), - // pass the registry through unchanged. The desugar - // pass does not touch class/instance defs (see desugar.rs: - // 22b.1 passthrough), so the registry built at load time - // remains valid against the desugared modules. - registry: ws.registry.clone(), - }; + // + // prep.1 (kernel-extension-mechanics): after desugar, normalize + // each consumer module's bare cross-module `Type::Con` references + // to qualified form via [`prepare_workspace_for_check`]. The + // monomorphisation pass mirrors this step in its own entry + // (`monomorphise_workspace`); the two passes consume identically + // shaped workspaces. The registry passes through unchanged — the + // desugar pass does not touch class/instance defs (see desugar.rs: + // 22b.1 passthrough), so the registry built at load time remains + // valid against the prepared workspace. + let ws_owned = prepare_workspace_for_check(ws); let ws = &ws_owned; // Pass 1: build per-module top-level symbol table — without checking // bodies. This lets module A access defs from module B even when B @@ -1811,8 +1884,14 @@ fn check_type_well_formed(t: &Type, env: &Env) -> Result<()> { return Ok(()); } // a qualified type name `module.Type` resolves - // through the import map and the per-module type table. The - // bare-name path is unchanged. + // through the import map and the per-module type table. + // prep.1: a bare type name also resolves to any workspace + // TypeDef of that name (TypeDef-first ladder), symmetric + // to the `Term::Var` and `Term::Ctor` arms. This makes + // `(con Maybe a)` in a consumer module's type signature + // resolve when `Maybe` lives in an imported (explicit or + // implicit) module — matching the canonical-form rule + // already accepted by the workspace validator. let td_opt: Option<&TypeDef> = if name.matches('.').count() == 1 { let (prefix, suffix) = name.split_once('.').expect("checked"); let target_module = match env.imports.get(prefix) { @@ -1826,8 +1905,12 @@ fn check_type_well_formed(t: &Type, env: &Env) -> Result<()> { env.module_types .get(target_module) .and_then(|tys| tys.get(suffix)) + } else if let Some(td) = env.types.get(name) { + Some(td) } else { - env.types.get(name) + env.module_types + .values() + .find_map(|types| types.get(name)) }; if let Some(td) = td_opt { if td.vars.len() != args.len() { @@ -2950,9 +3033,11 @@ pub(crate) fn synth( // into `env.globals` only. The unqualified-name capture // matters for dot-qualified call sites: the FreeFnCall // records the suffix (e.g. `length`), not the full - // `std_list.length`, so `synthesise_mono_fn_for_free_fn` - // can look up the source def by its bare name in the - // owner module's def list. + // `List.length` (prep.1's type-scoped form) or + // `std_list.length` (module-qualified form), so + // `synthesise_mono_fn_for_free_fn` can look up the + // source def by its bare name in the owner module's + // def list. // // After the resolution ladder, if `raw` is a `Type::Forall` // AND a `free_fn_owner` is known, push a `FreeFnCall` @@ -3162,13 +3247,29 @@ pub(crate) fn synth( return Ok(inst_ty); } else if name.matches('.').count() == 1 { let (prefix, suffix) = name.split_once('.').expect("checked"); - let target_module = match env.imports.get(prefix) { - Some(m) => m.clone(), - None => { - return Err(CheckError::UnknownModule { - module: prefix.to_string(), - }); - } + // prep.1: TypeDef-first ladder. If `prefix` names a + // `TypeDef` anywhere in the workspace, that type's home + // module is the resolution target — type-scoped form + // `.`. Otherwise fall back to the + // legacy module-as-receiver path via `env.imports`. + let type_home: Option = env + .module_types + .iter() + .find_map(|(mod_name, types)| { + if types.contains_key(prefix) { + Some(mod_name.clone()) + } else { + None + } + }); + let target_module: String = if let Some(home) = type_home.clone() { + home + } else if let Some(m) = env.imports.get(prefix) { + m.clone() + } else { + return Err(CheckError::TypeScopedReceiverNotAType { + name: prefix.to_string(), + }); }; let g = env.module_globals.get(&target_module).ok_or_else(|| { CheckError::UnknownModule { @@ -3176,9 +3277,21 @@ pub(crate) fn synth( } })?; let raw_ty = g.get(suffix).cloned().ok_or_else(|| { - CheckError::UnknownImport { - module: target_module.clone(), - name: suffix.to_string(), + // If receiver resolved as a TypeDef but the suffix + // is missing in the home module, emit the + // type-scoped diagnostic; otherwise the legacy + // `UnknownImport`. + if type_home.is_some() { + CheckError::TypeScopedMemberNotFound { + type_name: prefix.to_string(), + member: suffix.to_string(), + home_module: target_module.clone(), + } + } else { + CheckError::UnknownImport { + module: target_module.clone(), + name: suffix.to_string(), + } } })?; // qualify any bare type-cons referring to a @@ -3360,10 +3473,20 @@ pub(crate) fn synth( } Term::Ctor { type_name, ctor, args } => { // Canonical-type-lookup: Term::Ctor lookup is direct post-canonical-type-form - // Canonical type_name: bare = local TypeDef, qualified = - // explicit cross-module. The imports-fallback (iter - // 23.1.3) is gone — bare cross-module refs are rejected - // upstream by the workspace validator (via the canonical-form validator). + // Canonical type_name: bare = local TypeDef OR (prep.1) any + // bare type-name in scope via an imported module's TypeDef; + // qualified = explicit cross-module. The imports-fallback + // (iter 23.1.3) is gone — bare cross-module refs that are + // NOT in scope are rejected upstream by the workspace + // validator (via the canonical-form validator). + // + // prep.1: a bare `type_name` that does not match a local + // TypeDef falls back to a workspace-wide TypeDef-first + // lookup (symmetric to the `Term::Var` dot-qualified arm + // at lib.rs:3189). This makes `(term-ctor Maybe Just x)` + // resolve when `Maybe` is declared in an imported (explicit + // or implicit) module — matching the canonical-form rule + // already accepted by the workspace validator. // // when the type is cross-module, `cdef.fields` is // written in the owning module's local namespace. A recursive @@ -3374,7 +3497,7 @@ pub(crate) fn synth( // (and any other locally-named cross-module type-cons) are // qualified before substitution / unification. let owning_module: Option; - let result_type_name: String = type_name.clone(); + let result_type_name: String; let td = if type_name.matches('.').count() == 1 { let (prefix, suffix) = type_name.split_once('.').expect("checked"); let target_module = match env.imports.get(prefix) { @@ -3391,10 +3514,25 @@ pub(crate) fn synth( .cloned() .ok_or_else(|| CheckError::UnknownType(type_name.clone()))?; owning_module = Some(target_module); + result_type_name = type_name.clone(); td } else if let Some(td) = env.types.get(type_name) { owning_module = None; + result_type_name = type_name.clone(); td.clone() + } else if let Some((home, td)) = env + .module_types + .iter() + .find_map(|(m, types)| types.get(type_name).map(|td| (m.clone(), td.clone()))) + { + // prep.1: TypeDef-first cross-module bare resolution. + // The result-type Con.name is qualified to the home + // module so it unifies against signatures already + // carrying the qualified form (e.g. `from_maybe`'s + // second arg of type `std_maybe.Maybe`). + result_type_name = format!("{home}.{type_name}"); + owning_module = Some(home); + td } else { return Err(CheckError::UnknownType(type_name.clone())); }; @@ -3918,6 +4056,185 @@ fn qualify_local_types(t: &Type, owner_module: &str, local_types: &IndexMap.` form. Symmetric to [`qualify_local_types`] +/// but operates from the consumer's perspective: a bare type-name +/// that is not local AND not primitive AND resolves to a `TypeDef` +/// in some other module is rewritten to the qualified form so that +/// the consumer's signature unifies with pulled-across-boundary +/// signatures (which `qualify_local_types` already rewrites bare -> +/// qualified at the owner's side). +pub(crate) fn qualify_workspace_types( + t: &Type, + own_local_types: &IndexMap, + module_types: &BTreeMap>, +) -> Type { + match t { + Type::Con { name, args } => { + let qualified_name = if name.contains('.') { + name.clone() + } else if ailang_core::primitives::is_primitive_name(name) { + name.clone() + } else if own_local_types.contains_key(name) { + name.clone() + } else if let Some(home) = module_types + .iter() + .find_map(|(m, types)| if types.contains_key(name) { Some(m.clone()) } else { None }) + { + format!("{home}.{name}") + } else { + name.clone() + }; + Type::Con { + name: qualified_name, + args: args + .iter() + .map(|a| qualify_workspace_types(a, own_local_types, module_types)) + .collect(), + } + } + Type::Fn { params, ret, effects, param_modes, ret_mode } => Type::Fn { + params: params + .iter() + .map(|p| qualify_workspace_types(p, own_local_types, module_types)) + .collect(), + ret: Box::new(qualify_workspace_types(ret, own_local_types, module_types)), + effects: effects.clone(), + param_modes: param_modes.clone(), + ret_mode: ret_mode.clone(), + }, + Type::Forall { vars, constraints, body } => Type::Forall { + vars: vars.clone(), + constraints: constraints + .iter() + .map(|c| Constraint { + class: c.class.clone(), + type_: qualify_workspace_types(&c.type_, own_local_types, module_types), + }) + .collect(), + body: Box::new(qualify_workspace_types(body, own_local_types, module_types)), + }, + Type::Var { .. } => t.clone(), + } +} + +/// prep.1: walk a [`Module`] and rewrite every `Type` annotation +/// (function signatures, const types, `Term::Lam.param_tys`/`ret_ty`, +/// `Term::LetRec.ty`) by applying [`qualify_workspace_types`]. Bare +/// cross-module `Type::Con` names are upgraded to qualified +/// `.` form so that consumer-side declared types unify +/// against imported-fn signatures (which the existing +/// [`qualify_local_types`] step already qualifies on the owner side). +pub fn qualify_workspace_module( + mut m: Module, + own_local_types: &IndexMap, + module_types: &BTreeMap>, +) -> Module { + for def in &mut m.defs { + match def { + Def::Fn(f) => { + f.ty = qualify_workspace_types(&f.ty, own_local_types, module_types); + qualify_workspace_term(&mut f.body, own_local_types, module_types); + } + Def::Const(c) => { + c.ty = qualify_workspace_types(&c.ty, own_local_types, module_types); + qualify_workspace_term(&mut c.value, own_local_types, module_types); + } + Def::Type(_) | Def::Class(_) | Def::Instance(_) => { + // TypeDef.ctors carry field types in the owner's local + // namespace by convention — no qualification at the + // owner's own definition site. Class / Instance defs + // hold types qualified through other mechanisms. + } + } + } + m +} + +pub(crate) fn qualify_workspace_term( + t: &mut Term, + own_local_types: &IndexMap, + module_types: &BTreeMap>, +) { + match t { + Term::Lit { .. } | Term::Var { .. } | Term::Recur { .. } => {} + Term::App { callee, args, .. } => { + qualify_workspace_term(callee, own_local_types, module_types); + for a in args { + qualify_workspace_term(a, own_local_types, module_types); + } + } + Term::Let { value, body, .. } => { + qualify_workspace_term(value, own_local_types, module_types); + qualify_workspace_term(body, own_local_types, module_types); + } + Term::LetRec { ty, body, in_term, .. } => { + *ty = qualify_workspace_types(ty, own_local_types, module_types); + qualify_workspace_term(body, own_local_types, module_types); + qualify_workspace_term(in_term, own_local_types, module_types); + } + Term::If { cond, then, else_ } => { + qualify_workspace_term(cond, own_local_types, module_types); + qualify_workspace_term(then, own_local_types, module_types); + qualify_workspace_term(else_, own_local_types, module_types); + } + Term::Do { args, .. } => { + for a in args { + qualify_workspace_term(a, own_local_types, module_types); + } + } + Term::Ctor { type_name, args, .. } => { + // prep.1: normalize bare cross-module `type_name` to + // qualified form, mirroring [`qualify_workspace_types`] + // for the `Type::Con.name` path. + if !type_name.contains('.') + && !ailang_core::primitives::is_primitive_name(type_name) + && !own_local_types.contains_key(type_name) + { + if let Some(home) = module_types + .iter() + .find_map(|(m, types)| if types.contains_key(type_name) { Some(m.clone()) } else { None }) + { + *type_name = format!("{home}.{type_name}"); + } + } + for a in args { + qualify_workspace_term(a, own_local_types, module_types); + } + } + Term::Match { scrutinee, arms } => { + qualify_workspace_term(scrutinee, own_local_types, module_types); + for arm in arms { + qualify_workspace_term(&mut arm.body, own_local_types, module_types); + } + } + Term::Lam { param_tys, ret_ty, body, .. } => { + for p in param_tys.iter_mut() { + *p = qualify_workspace_types(p, own_local_types, module_types); + } + **ret_ty = qualify_workspace_types(ret_ty, own_local_types, module_types); + qualify_workspace_term(body, own_local_types, module_types); + } + Term::Seq { lhs, rhs } => { + qualify_workspace_term(lhs, own_local_types, module_types); + qualify_workspace_term(rhs, own_local_types, module_types); + } + Term::Clone { value } => qualify_workspace_term(value, own_local_types, module_types), + Term::ReuseAs { source, body } => { + qualify_workspace_term(source, own_local_types, module_types); + qualify_workspace_term(body, own_local_types, module_types); + } + Term::Loop { binders, body } => { + for b in binders { + b.ty = qualify_workspace_types(&b.ty, own_local_types, module_types); + qualify_workspace_term(&mut b.init, own_local_types, module_types); + } + qualify_workspace_term(body, own_local_types, module_types); + } + } +} + /// Checks a pattern against an expected type and returns the bindings /// introduced by the pattern. fn type_check_pattern( @@ -6207,17 +6524,65 @@ mod tests { ); } - /// Canonical-type-lookup: a bare `Term::Ctor.type_name` that does not resolve - /// to a local TypeDef must error with `UnknownType` (or - /// `UnknownCtor`, depending on which check fires first). The - /// imports-fallback that previously synthesised a qualified result - /// from an arbitrary imported module is gone. The - /// post-canonical-type-form validator catches this shape at load time for - /// canonical inputs; this test pins the residual runtime guard - /// against constructed (non-loaded) AST. + /// prep.1 (kernel-extension-mechanics): a bare `Term::Ctor.type_name` + /// that does not resolve to a local TypeDef AND does not resolve + /// via the workspace-wide TypeDef-first ladder must error with + /// `UnknownType`. Pre-prep.1 a bare cross-module ref was always + /// rejected at this site; post-prep.1 it is *accepted* when an + /// imported module declares the type (covered by + /// `ct2_term_ctor_bare_cross_module_via_workspace_resolves`). + /// This test uses a name (`Widget`) no module declares so the + /// runtime guard still fires. #[test] fn ct2_term_ctor_bare_cross_module_fails_closed() { - let prelude = Module { + let consumer = Module { + schema: SCHEMA.into(), + name: "u".into(), + imports: vec![], + defs: vec![fn_def( + "stale", + Type::Fn { + params: vec![], + ret: Box::new(Type::Con { + name: "Widget".into(), + args: vec![], + }), + effects: vec![], + param_modes: vec![], + ret_mode: ParamMode::Implicit, + }, + vec![], + Term::Ctor { + type_name: "Widget".into(), + ctor: "Mk".into(), + args: vec![], + }, + )], + }; + let mut modules = BTreeMap::new(); + modules.insert("u".into(), consumer); + let ws = Workspace { + entry: "u".into(), + modules, + root_dir: std::path::PathBuf::from("."), + registry: ailang_core::workspace::Registry::default(), + }; + let diags = check_workspace(&ws); + assert!( + diags.iter().any(|d| d.code == "unknown-type"), + "expected unknown-type diagnostic for bare cross-module \ + Term::Ctor (no module declares Widget); got {diags:?}" + ); + } + + /// prep.1 (kernel-extension-mechanics): a bare `Term::Ctor.type_name` + /// resolves via the workspace-wide TypeDef-first ladder when an + /// imported module declares the type. Companion to + /// `ct2_term_ctor_bare_cross_module_fails_closed` (the negative + /// shape). + #[test] + fn ct2_term_ctor_bare_cross_module_via_workspace_resolves() { + let owner = Module { schema: SCHEMA.into(), name: "p".into(), imports: vec![], @@ -6233,14 +6598,12 @@ mod tests { drop_iterative: false, })], }; - // Consumer imports prelude but writes BARE `Ordering` in - // Term::Ctor — this is a stale-canonical-form construction. let consumer = Module { schema: SCHEMA.into(), name: "u".into(), imports: vec![Import { module: "p".into(), alias: None }], defs: vec![fn_def( - "stale", + "f", Type::Fn { params: vec![], ret: Box::new(Type::Con { @@ -6260,7 +6623,7 @@ mod tests { )], }; let mut modules = BTreeMap::new(); - modules.insert("p".into(), prelude); + modules.insert("p".into(), owner); modules.insert("u".into(), consumer); let ws = Workspace { entry: "u".into(), @@ -6270,9 +6633,8 @@ mod tests { }; let diags = check_workspace(&ws); assert!( - diags.iter().any(|d| d.code == "unknown-type"), - "expected unknown-type diagnostic for bare cross-module \ - Term::Ctor; got {diags:?}" + diags.is_empty(), + "bare `Ordering` in Term::Ctor must resolve via workspace TypeDef-first ladder; got {diags:?}" ); } @@ -6921,4 +7283,147 @@ mod tests { "foo", )); } + + /// prep.1 (kernel-extension-mechanics): a dot-qualified `Term::Var` + /// `.` resolves to the type's home module when + /// `` is a known `TypeDef` in the workspace, regardless + /// of whether the consumer module imports the home module under + /// that name. Here `Maybe.from_maybe` from `consumer` must resolve + /// to `std_maybe.from_maybe` because `Maybe` is declared in + /// `std_maybe` and `consumer` does import `std_maybe`. + #[test] + fn type_scoped_member_resolves() { + let std_maybe: Module = serde_json::from_value(serde_json::json!({ + "schema": SCHEMA, + "name": "std_maybe", + "imports": [], + "defs": [ + {"kind": "type", "name": "Maybe", "vars": ["a"], "ctors": [ + {"name": "Nothing", "fields": []}, + {"name": "Just", "fields": [{"k": "var", "name": "a"}]} + ]}, + {"kind": "fn", "name": "from_maybe", + "type": {"k": "forall", "vars": ["a"], "constraints": [], "body": + {"k": "fn", "params": [{"k": "var", "name": "a"}, + {"k": "con", "name": "Maybe", "args": [{"k": "var", "name": "a"}]}], + "ret": {"k": "var", "name": "a"}, "effects": []}}, + "params": ["default", "m"], + "body": {"t": "var", "name": "default"}} + ] + })).unwrap(); + // Consumer calls `Maybe.from_maybe` with arg types qualified to + // `std_maybe.Maybe` (post-resolution the type-scoped form + // resolves to `std_maybe.from_maybe`, but the ctor arg uses + // the qualified form so the bare-cross-module-type-validator + // is satisfied independently of Task 2's widening — Task 1's + // success criterion is only that the dot-qualified Var arm + // resolves through the TypeDef-first ladder). + let consumer: Module = serde_json::from_value(serde_json::json!({ + "schema": SCHEMA, + "name": "consumer", + "imports": [{"module": "std_maybe"}], + "defs": [ + {"kind": "fn", "name": "f", + "type": {"k": "fn", "params": [{"k": "con", "name": "Int"}], + "ret": {"k": "con", "name": "Int"}, "effects": []}, + "params": ["x"], + "body": {"t": "app", + "fn": {"t": "var", "name": "Maybe.from_maybe"}, + "args": [{"t": "var", "name": "x"}, + {"t": "ctor", "type": "std_maybe.Maybe", + "ctor": "Nothing", "args": []}]}} + ] + })).unwrap(); + let mut modules = BTreeMap::new(); + modules.insert("std_maybe".to_string(), std_maybe); + modules.insert("consumer".to_string(), consumer); + let ws = Workspace { + entry: "consumer".into(), + modules, + root_dir: std::path::PathBuf::from("."), + registry: ailang_core::workspace::Registry::default(), + }; + let diags = check_workspace(&ws); + assert!( + diags.is_empty(), + "type-scoped Maybe.from_maybe must resolve cleanly, got {diags:?}" + ); + } + + /// prep.1 (kernel-extension-mechanics): a dot-qualified `Term::Var` + /// `.` where `` is a known `TypeDef` + /// but `` is not a def in the type's home module fires + /// `TypeScopedMemberNotFound`. + #[test] + fn type_scoped_member_not_found() { + let std_maybe: Module = serde_json::from_value(serde_json::json!({ + "schema": SCHEMA, + "name": "std_maybe", + "imports": [], + "defs": [ + {"kind": "type", "name": "Maybe", "vars": ["a"], "ctors": [ + {"name": "Nothing", "fields": []}, + {"name": "Just", "fields": [{"k": "var", "name": "a"}]} + ]} + ] + })).unwrap(); + let consumer: Module = serde_json::from_value(serde_json::json!({ + "schema": SCHEMA, + "name": "consumer", + "imports": [{"module": "std_maybe"}], + "defs": [ + {"kind": "fn", "name": "f", + "type": {"k": "fn", "params": [], + "ret": {"k": "con", "name": "Int"}, "effects": []}, + "params": [], + "body": {"t": "var", "name": "Maybe.bogus"}} + ] + })).unwrap(); + let mut modules = BTreeMap::new(); + modules.insert("std_maybe".to_string(), std_maybe); + modules.insert("consumer".to_string(), consumer); + let ws = Workspace { + entry: "consumer".into(), + modules, + root_dir: std::path::PathBuf::from("."), + registry: ailang_core::workspace::Registry::default(), + }; + let diags = check_workspace(&ws); + assert!( + diags.iter().any(|d| d.code == "type-scoped-member-not-found"), + "expected diagnostic code `type-scoped-member-not-found`, got {diags:?}" + ); + } + + /// prep.1 (kernel-extension-mechanics): a dot-qualified `Term::Var` + /// whose receiver is neither a known `TypeDef` nor an imported + /// module fires `TypeScopedReceiverNotAType`. + #[test] + fn type_scoped_receiver_not_a_type() { + let consumer: Module = serde_json::from_value(serde_json::json!({ + "schema": SCHEMA, + "name": "consumer", + "imports": [], + "defs": [ + {"kind": "fn", "name": "f", + "type": {"k": "fn", "params": [], + "ret": {"k": "con", "name": "Int"}, "effects": []}, + "params": [], + "body": {"t": "var", "name": "SomethingRandom.x"}} + ] + })).unwrap(); + let mut modules = BTreeMap::new(); + modules.insert("consumer".to_string(), consumer); + let ws = Workspace { + entry: "consumer".into(), + modules, + root_dir: std::path::PathBuf::from("."), + registry: ailang_core::workspace::Registry::default(), + }; + let diags = check_workspace(&ws); + assert!( + diags.iter().any(|d| d.code == "type-scoped-receiver-not-a-type"), + "expected diagnostic code `type-scoped-receiver-not-a-type`, got {diags:?}" + ); + } } diff --git a/crates/ailang-check/src/lift.rs b/crates/ailang-check/src/lift.rs index 07daa2e..bee3f6f 100644 --- a/crates/ailang-check/src/lift.rs +++ b/crates/ailang-check/src/lift.rs @@ -68,9 +68,10 @@ pub fn lift_letrecs(m: &Module) -> Result { // `lift_letrecs` is a single-module pass; cross-module info isn't // needed because the LetRec capture set comes from the *enclosing* // fn's locals (which are always local to this module). Capture - // types may mention foreign type-cons (e.g. `std_list.List Int`), - // but those flow through verbatim — the lifter never needs to - // resolve them. + // types may mention foreign type-cons (e.g. `List Int` resolved + // through prep.1's type-scoped namespacing, or the qualified + // `std_list.List Int` form), but those flow through verbatim — + // the lifter never needs to resolve them. let mut env = Env::new(); builtins::install(&mut env); diff --git a/crates/ailang-check/src/mono.rs b/crates/ailang-check/src/mono.rs index 89aea7b..a6af73c 100644 --- a/crates/ailang-check/src/mono.rs +++ b/crates/ailang-check/src/mono.rs @@ -69,6 +69,15 @@ use std::collections::{BTreeMap, BTreeSet}; /// pass does not perform new type checking — it queries types via /// `synth` on already-typechecked bodies. pub fn monomorphise_workspace(ws: &Workspace) -> Result { + // prep.1 (kernel-extension-mechanics): mirror `check_workspace`'s + // pre-pass — desugar + qualify bare cross-module `Type::Con` + // references to qualified form. Both passes must operate on the + // identically-shaped workspace; otherwise the mono's residual / + // free-fn-call observations would key on the original bare-form + // Type values and fail unification against the qualified forms + // the typechecker emitted into the post-prep.1 `Forall` body. + let ws_prepared = crate::prepare_workspace_for_check(ws); + let ws = &ws_prepared; // Fast path — no class / instance defs anywhere → nothing to do. // The pass also has no targets when there are class defs but no // instance defs (no callable methods at concrete types), but @@ -345,8 +354,17 @@ fn poly_free_fn_names_for_module( } // 2 + 3. Imported modules' poly fns: bare (via implicit-import // fall-through) AND dot-qualified (alias.name). + // prep.1: also enumerate type-scoped spellings + // `.` for every TypeDef declared in the imported + // module — `synth`'s Var-arm resolves these via the TypeDef-first + // ladder and `rewrite_mono_calls` consumes the same spelling. if let Some(imports) = env.module_imports.get(mname) { for (alias_or_name, target_mod) in imports { + let target_types: Vec = env + .module_types + .get(target_mod) + .map(|tys| tys.keys().cloned().collect()) + .unwrap_or_default(); if let Some(target_globals) = env.module_globals.get(target_mod) { for (n, t) in target_globals { if matches!(t, Type::Forall { .. }) { @@ -355,6 +373,10 @@ fn poly_free_fn_names_for_module( out.insert(n.clone()); // Dot-qualified form. out.insert(format!("{alias_or_name}.{n}")); + // prep.1: type-scoped form per TypeDef. + for tn in &target_types { + out.insert(format!("{tn}.{n}")); + } } } } @@ -394,13 +416,24 @@ fn poly_free_fn_constraint_counts_for_module( } } // 2 + 3. Imported modules' poly fns: bare AND dot-qualified. + // prep.1: also enumerate type-scoped spellings `.` + // per TypeDef in the imported module — mirror of + // `poly_free_fn_names_for_module`. if let Some(imports) = env.module_imports.get(mname) { for (alias_or_name, target_mod) in imports { + let target_types: Vec = env + .module_types + .get(target_mod) + .map(|tys| tys.keys().cloned().collect()) + .unwrap_or_default(); if let Some(target_globals) = env.module_globals.get(target_mod) { for (n, t) in target_globals { if let Type::Forall { constraints, .. } = t { out.insert(n.clone(), constraints.len()); out.insert(format!("{alias_or_name}.{n}"), constraints.len()); + for tn in &target_types { + out.insert(format!("{tn}.{n}"), constraints.len()); + } } } } @@ -1031,8 +1064,8 @@ pub fn synthesise_mono_fn_for_free_fn( // this because instance bodies are Lam-unwrapped during synth // (the outer Lam's `param_tys` are dropped); a free-fn body // can carry arbitrary nested Lams with `Type::Var`-bearing - // `param_tys`, which is the case for e.g. `std_list.length` - // (an inner accumulating lambda over `(b, a)`). + // `param_tys`, which is the case for e.g. `List.length` + // (type-scoped, an inner accumulating lambda over `(b, a)`). let new_type = crate::substitute_rigids(&inner_ty, &mapping); let new_body = crate::substitute_rigids_in_term(&source_fn.body, &mapping); diff --git a/crates/ailang-check/tests/workspace.rs b/crates/ailang-check/tests/workspace.rs index 1b6002b..2e16dc1 100644 --- a/crates/ailang-check/tests/workspace.rs +++ b/crates/ailang-check/tests/workspace.rs @@ -71,15 +71,19 @@ fn unknown_import_is_reported() { #[test] fn unknown_module_prefix_is_reported() { - // ws_unknown_module has no imports but references `nope.x`. + // ws_unknown_module has no imports but references `nope.x`. Under + // prep.1's type-scoped resolution, `nope` is neither a known + // TypeDef nor an imported module, so the diagnostic narrowed from + // the legacy `unknown-module` to `type-scoped-receiver-not-a-type` + // — a more precise wording for the same failure mode. let entry = examples_dir().join("ws_unknown_module.ail"); let ws = load_workspace(&entry).expect("load ws_unknown_module"); let diags = check_workspace(&ws); assert_eq!(diags.len(), 1, "got: {:?}", diags); assert!(matches!(diags[0].severity, Severity::Error)); - assert_eq!(diags[0].code, "unknown-module"); + assert_eq!(diags[0].code, "type-scoped-receiver-not-a-type"); assert_eq!( - diags[0].ctx.get("module").and_then(|v| v.as_str()), + diags[0].ctx.get("name").and_then(|v| v.as_str()), Some("nope") ); } diff --git a/crates/ailang-codegen/src/lib.rs b/crates/ailang-codegen/src/lib.rs index c1be04a..acb4296 100644 --- a/crates/ailang-codegen/src/lib.rs +++ b/crates/ailang-codegen/src/lib.rs @@ -2104,28 +2104,39 @@ impl<'a> Emitter<'a> { } Ok(cref) } else { - // Bare type_name is canonical-form local. Hit the - // current module's ctor table directly; non-match is - // a hard error. - let cref = self + // Bare type_name: try the current module's ctor table + // first (canonical local case). On miss, fall back to a + // workspace-wide scan for a module declaring a TypeDef of + // that name (prep.1: type-scoped namespacing — bare cross- + // module type-names in scope via an imported module's + // TypeDef are accepted by the typechecker, so codegen + // must resolve them symmetrically). + if let Some(cref) = self .module_ctor_index .get(self.module_name) .and_then(|m| m.get(ctor_name)) .cloned() - .ok_or_else(|| { - CodegenError::Internal(format!( - "unknown ctor `{ctor_name}` for type `{type_name}` in module `{}`", - self.module_name - )) - })?; - if cref.type_name != type_name { - return Err(CodegenError::Internal(format!( - "ctor `{ctor_name}` belongs to local type `{}`, not `{type_name}`; \ - cross-module ctor refs require qualified type_name", - cref.type_name - ))); + { + if cref.type_name == type_name { + return Ok(cref); + } } - Ok(cref) + // prep.1: workspace-wide fallback for cross-module bare. + for (owner_mod, ctors) in self.module_ctor_index { + if owner_mod == self.module_name { + continue; + } + if let Some(cref) = ctors.get(ctor_name) { + if cref.type_name == type_name { + return Ok(cref.clone()); + } + } + } + Err(CodegenError::Internal(format!( + "unknown ctor `{ctor_name}` for type `{type_name}` in module `{}` \ + (workspace-wide scan also missed)", + self.module_name + ))) } } @@ -3441,7 +3452,8 @@ impl<'a> Emitter<'a> { // is written in the owning module's local namespace, so a // recursive self-reference like `Cons a (List a)` carries // a bare `Con("List", _)` even though every other place - // sees the qualified `std_list.List<...>`. Apply + // sees the qualified form (`.List<...>`). + // Apply // `qualify_local_types_codegen` before `unify_for_subst` // so the unification doesn't fail on name mismatch. let cref = self.lookup_ctor_by_type(type_name, ctor)?; diff --git a/crates/ailang-codegen/src/subst.rs b/crates/ailang-codegen/src/subst.rs index 57e0a14..2a89a1c 100644 --- a/crates/ailang-codegen/src/subst.rs +++ b/crates/ailang-codegen/src/subst.rs @@ -151,11 +151,13 @@ pub(crate) fn unify_for_subst( /// rewrites bare `Type::Con` references that resolve against /// `owner_local_types` into qualified `module.Type` form. Mirrors -/// `ailang_check::qualify_local_types`. Used when the codegen pulls a -/// polymorphic fn signature across the import boundary; without this -/// the substitution derived from the call site's qualified args -/// (`std_maybe.Maybe`) would fail to unify against the bare -/// signature (`Maybe`). +/// `ailang_check::qualify_local_types` and complements prep.1's +/// `qualify_workspace_types` (which qualifies consumer-side bare +/// cross-module refs). Used when the codegen pulls a polymorphic +/// fn signature across the import boundary; without this the +/// substitution derived from the call site's qualified args +/// (e.g. `std_maybe.Maybe`) would fail to unify against the +/// owner-local signature (`Maybe`). pub(crate) fn qualify_local_types_codegen( t: &Type, owner_module: &str, diff --git a/crates/ailang-core/src/workspace.rs b/crates/ailang-core/src/workspace.rs index 3025840..11a0203 100644 --- a/crates/ailang-core/src/workspace.rs +++ b/crates/ailang-core/src/workspace.rs @@ -318,9 +318,9 @@ pub enum WorkspaceLoadError { /// `candidates` lists the qualified forms found by scanning the /// owning module's imports in declaration order. #[error( - "module `{module}` contains bare type name `{name}` that does not resolve to a local type. \ - AILang's `.ail.json` requires cross-module type references to be qualified. \ - Candidates from imports: {candidates:?}. Run `ail migrate-canonical-types` to fix legacy fixtures." + "module `{module}` references bare type `{name}`, which is not in scope. \ + Add `(import )` to bring it into scope (candidates: {candidates:?}), \ + or rewrite the call to type-scoped form `.`." )] BareCrossModuleTypeRef { module: String, @@ -333,8 +333,9 @@ pub enum WorkspaceLoadError { /// workspace, or `` is known but declares no TypeDef /// named ``. #[error( - "module `{module}` references qualified type `{name}` but the owner module is not known \ - or does not declare a type by that name" + "module `{module}` references qualified type `{name}` but the owner module \ + is not known in the workspace, or it declares no type by that name. \ + Use the bare type-name from an imported module instead." )] BadCrossModuleTypeRef { module: String, @@ -1109,9 +1110,11 @@ fn check_type_con_name( { return Ok(()); } - // Bare cross-module — collect candidates from imports in declaration order. - // Prelude is implicit: scan it last as a fallback candidate (mirrors - // iter 23.2.4's implicit-prelude behaviour in codegen). + // prep.1: a bare cross-module type-name is ACCEPTED if it is in + // scope via an explicit import or an implicit (prelude / kernel- + // tier) auto-import. Candidates from those paths drive both + // acceptance and (on miss) the error message's suggested fix. + let mut in_scope = false; let mut candidates: Vec = Vec::new(); for imp in import_names { if local_types @@ -1119,6 +1122,7 @@ fn check_type_con_name( .map(|s| s.contains(name)) .unwrap_or(false) { + in_scope = true; candidates.push(format!("{imp}.{name}")); } } @@ -1131,9 +1135,13 @@ fn check_type_con_name( .map(|s| s.contains(name)) .unwrap_or(false) { + in_scope = true; candidates.push(format!("{implicit}.{name}")); } } + if in_scope { + return Ok(()); + } Err(WorkspaceLoadError::BareCrossModuleTypeRef { module: owning_module.to_string(), name: name.to_string(), @@ -1855,21 +1863,46 @@ mod tests { } } - /// 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). + /// prep.1: a bare `Type::Con` whose `name` matches a `TypeDef` in + /// an EXPLICITLY imported module must be ACCEPTED. (Pre-prep.1 this + /// case was rejected as `BareCrossModuleTypeRef`; type-scoped form + /// is canonical and importing the owner module brings the bare + /// type-name into scope.) #[test] - fn ct1_validator_rejects_bare_xmod_with_import_candidate() { + fn ct1_validator_accepts_bare_with_explicit_import() { let mut modules = BTreeMap::new(); modules.insert("other".to_string(), module_with_type_def("other", "Ordering")); modules.insert("m".to_string(), module_with_import_and_type_con("m", "other", "Ordering")); + validate_canonical_type_names(&modules, &["prelude"]) + .expect("bare `Ordering` must be accepted when `other` is imported and declares it"); + } + + /// prep.1: a bare `Type::Con` whose `name` is a `TypeDef` in some + /// workspace module BUT the owning module does NOT import that + /// module (and the type is not implicit-imported either) must still + /// fire `BareCrossModuleTypeRef`. The presence of `other` in the + /// workspace is not enough; the bare-in-scope path requires `m` to + /// declare an `(import other)`. + #[test] + fn ct1_validator_rejects_bare_when_owner_not_imported() { + let mut modules = BTreeMap::new(); + modules.insert("other".to_string(), module_with_type_def("other", "Ordering")); + // `m` references `Ordering` but does NOT import `other`. + modules.insert("m".to_string(), single_module_with_type_con("m", "Ordering").remove("m").unwrap()); let err = validate_canonical_type_names(&modules, &["prelude"]) - .expect_err("Ordering must be rejected with candidate"); + .expect_err("bare `Ordering` must be rejected when `other` not imported"); match err { - WorkspaceLoadError::BareCrossModuleTypeRef { name, candidates, .. } => { + WorkspaceLoadError::BareCrossModuleTypeRef { name, candidates, module } => { + assert_eq!(module, "m"); assert_eq!(name, "Ordering"); - assert_eq!(candidates, vec!["other.Ordering".to_string()]); + // No imports on `m` => no candidates list (today's + // implementation scans `import_names`, which is empty + // here; the workspace-wide scan is not part of the + // candidate-list construction). + assert!( + candidates.is_empty(), + "no imports => no candidates; got {candidates:?}" + ); } other => panic!("expected BareCrossModuleTypeRef, got {other:?}"), } @@ -1941,16 +1974,19 @@ mod tests { } } - /// 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. + /// prep.1: a `Term::Ctor` whose `type_name` is a bare type-name + /// from a module in scope (here `prelude`, via implicit imports) + /// is ACCEPTED. The symmetry with the `Type::Con` rule holds: + /// bare-in-scope is canonical post-prep.1, and the implicit + /// import path is one of the in-scope paths. #[test] - fn ct1_validator_rejects_bare_term_ctor_type_name() { + fn ct1_validator_accepts_bare_term_ctor_via_implicit_import() { let mut modules = BTreeMap::new(); modules.insert("prelude".to_string(), module_with_type_def("prelude", "Ordering")); - // Module `m` has no imports, no local Ordering, but a Term::Ctor - // referencing bare `Ordering`. + // Module `m` has no explicit imports, no local Ordering, but a + // Term::Ctor referencing bare `Ordering` — accepted via the + // implicit-prelude path. let m: Module = serde_json::from_value(serde_json::json!({ "schema": crate::SCHEMA, "name": "m", @@ -1969,17 +2005,8 @@ mod tests { }], })).unwrap(); modules.insert("m".to_string(), m); - let err = validate_canonical_type_names(&modules, &["prelude"]) - .expect_err("bare Term::Ctor type must be rejected"); - match err { - WorkspaceLoadError::BareCrossModuleTypeRef { module, name, candidates } => { - assert_eq!(module, "m"); - assert_eq!(name, "Ordering"); - assert_eq!(candidates, vec!["prelude.Ordering".to_string()], - "prelude is implicit-fallback"); - } - other => panic!("expected BareCrossModuleTypeRef, got {other:?}"), - } + validate_canonical_type_names(&modules, &["prelude"]) + .expect("bare Term::Ctor type must be accepted via implicit prelude import"); } /// a qualified `ClassDef.name` (e.g. `other.Eq`) must fire diff --git a/crates/ailang-core/tests/workspace_pin.rs b/crates/ailang-core/tests/workspace_pin.rs index 5d569a0..cff7c62 100644 --- a/crates/ailang-core/tests/workspace_pin.rs +++ b/crates/ailang-core/tests/workspace_pin.rs @@ -448,19 +448,25 @@ fn constraint_with_unbound_var_fires_unbound_constraint_type_var() { } } -/// pd.2 relocation: §C4 (a) carve-out fixture -/// `test_ct1_bare_xmod_rejected.ail.json` — bare `Ordering` Term::Ctor -/// with no imports, validator catches it after prelude injection so the -/// candidate list contains `prelude.Ordering`. +/// pd.2 relocation, prep.1 fixture-flip: §C4 (a) carve-out fixture +/// `test_ct1_bare_xmod_rejected.ail.json`. Pre-prep.1 the fixture used +/// bare `Ordering` and the validator caught it via prelude-as-candidate. +/// Post-prep.1 a bare in-scope type-name (`Ordering` from implicit +/// prelude) is ACCEPTED, so the fixture was switched to a name no +/// module declares (`Mystery_Type`); the rejection path still fires +/// `BareCrossModuleTypeRef` but the candidates list is empty. #[test] fn ct1_fixture_bare_xmod_rejected() { let entry = examples_dir().join("test_ct1_bare_xmod_rejected.ail.json"); - let err = load_workspace(&entry).expect_err("must reject bare Ordering"); + let err = load_workspace(&entry).expect_err("must reject bare Mystery_Type"); match err { WorkspaceLoadError::BareCrossModuleTypeRef { module, name, candidates } => { assert_eq!(module, "test_ct1_bare_xmod_rejected"); - assert_eq!(name, "Ordering"); - assert_eq!(candidates, vec!["prelude.Ordering".to_string()]); + assert_eq!(name, "Mystery_Type"); + assert!( + candidates.is_empty(), + "no module declares Mystery_Type => candidates empty; got {candidates:?}" + ); } other => panic!("expected BareCrossModuleTypeRef, got {other:?}"), } diff --git a/docs/specs/0052-kernel-extension-mechanics.md b/docs/specs/0052-kernel-extension-mechanics.md index cfc7f7f..b251efb 100644 --- a/docs/specs/0052-kernel-extension-mechanics.md +++ b/docs/specs/0052-kernel-extension-mechanics.md @@ -137,6 +137,30 @@ this use case; it remains valid only for module-free defs (defs that do not take a specific type as receiver) and as a workspace collision disambiguator (no current collisions exist). +**Realisation mechanism — workspace pre-pass.** What the +"Implementation shape" paragraphs describe at the resolver level +is *the user-facing semantics*. The actual realisation in code is +a workspace-wide normalisation step `prepare_workspace_for_check`, +shared by `check_workspace` and `monomorphise_workspace`, that +desugars every module and then rewrites every bare cross-module +`Type::Con.name` and `Term::Ctor.type_name` to its qualified +`.` form. This is symmetric to the pre-existing +`qualify_local_types` helper, which already qualifies bare +type-refs on the *owner* side; the new pre-pass extends the same +qualification to the *consumer* side. Downstream passes (checker +synth, mono, codegen) therefore see qualified Types regardless of +how the author wrote them. The TypeDef-first ladder still lives +in `synth`'s `Term::Var` arm, because the `.` +form is term-position-only — `Maybe.from_maybe` is a Var, not a +type expression, and the pre-pass does not rewrite Var names. +The two new diagnostics (`TypeScopedReceiverNotAType`, +`TypeScopedMemberNotFound`) fire from the resolver as planned. +The pre-pass design generalises naturally to later iterations: +prep.2's `Term::New.type_name` falls under the same `type_name` +rewrite when the pre-pass walks the `Term` tree, and prep.3's +kernel-tier modules' TypeDefs enter the workspace-wide TypeDef +map automatically (no pre-pass change needed for kernel-tier). + **Blast radius.** Per `grep -rE 'std_(maybe|pair|list|either)\.' examples/ crates/`: - **`.ail` example fixtures** (12 with cross-module refs, plus the diff --git a/examples/ct_2_bare_cross_module.ail b/examples/ct_2_bare_cross_module.ail index 27bf43a..32daa4e 100644 --- a/examples/ct_2_bare_cross_module.ail +++ b/examples/ct_2_bare_cross_module.ail @@ -1,22 +1,25 @@ ; Fieldtest — canonical-type-names, axis 1: BareCrossModuleTypeRef. ; ; A consumer of std_maybe deliberately writes a BARE `Maybe` in its -; fn signature instead of `std_maybe.Maybe`. Per ct.1's load-time -; validator, the canonical form requires cross-module type refs to -; be qualified. Expected: workspace-load error -; `BareCrossModuleTypeRef` naming the type and listing the qualified -; form as a candidate. +; fn signature WITHOUT (import std_maybe). prep.1 migration +; (kernel-extension-mechanics): pre-prep.1 this fixture rejected +; bare `Maybe` even when the import WAS present (the canonical form +; required cross-module type refs to be qualified at all times). +; Post-prep.1 bare-in-scope is canonical; the rejection path narrows +; to "bare-not-in-scope". To preserve the fixture's NEGATIVE role +; the `(import std_maybe)` declaration is dropped; bare `Maybe` is +; now genuinely out of scope and fires `BareCrossModuleTypeRef` +; with the narrowed "not in scope" message. The candidates list +; comes from the consumer's explicit imports + implicit imports; +; here both are empty, so candidates is empty too. ; -; This is what an LLM author would write if they forgot the -; cross-module-qualification rule — the rule fires here at load -; time, not deep inside the typechecker. +; Expected: workspace-load error `BareCrossModuleTypeRef` naming +; the type with the narrowed wording. (module ct_2_bare_cross_module - (import std_maybe) - (fn classify - (doc "Identity over Maybe; signature uses bare `Maybe` instead of `std_maybe.Maybe`.") + (doc "Identity over Maybe; signature uses bare `Maybe` with no import.") (type (fn-type (params (con Maybe (con Int))) @@ -28,4 +31,4 @@ (type (fn-type (params) (ret (con Unit)) (effects IO))) (params) (body - (app print (app std_maybe.from_maybe 99 (app classify (term-ctor std_maybe.Maybe Just 7))))))) + (app classify (term-ctor Maybe Just 7))))) diff --git a/examples/ct_3b_bad_qualified_known_module.ail b/examples/ct_3b_bad_qualified_known_module.ail index c31574c..24dcd3f 100644 --- a/examples/ct_3b_bad_qualified_known_module.ail +++ b/examples/ct_3b_bad_qualified_known_module.ail @@ -2,7 +2,10 @@ ; — known module, unknown type. Author qualifies as `std_maybe.Widget` ; where `std_maybe` IS a workspace module but does not declare a ; `Widget` type. Per ct.1's load-time validator, this should be -; rejected with `BadCrossModuleTypeRef`. +; rejected with `BadCrossModuleTypeRef`. prep.1 (kernel-extension- +; mechanics): the rejection path is unchanged structurally; only the +; message wording is narrowed (suggests "use bare from imported +; module instead"). (module ct_3b_bad_qualified_known_module diff --git a/examples/nested_pat.ail b/examples/nested_pat.ail index 8d12033..93934b0 100644 --- a/examples/nested_pat.ail +++ b/examples/nested_pat.ail @@ -1,6 +1,9 @@ ; Iter 16a — first program to use a nested constructor pattern. ; Without this iter, the inner `(pat-ctor Cons b _)` would be ; rejected by the checker as `nested-ctor-pattern-not-allowed`. +; prep.1 migration (kernel-extension-mechanics): bare List via +; `(import std_list)`; cross-module fns / ctors stay structurally +; identical (bare types now in scope). (module nested_pat @@ -10,7 +13,7 @@ (doc "Sum of the first two elements of an Int list, or 0 if shorter than two.") (type (fn-type - (params (con std_list.List (con Int))) + (params (con List (con Int))) (ret (con Int)))) (params xs) (body @@ -24,7 +27,7 @@ (params) (body (app print (app first_two_sum - (term-ctor std_list.List Cons 10 - (term-ctor std_list.List Cons 20 - (term-ctor std_list.List Cons 30 - (term-ctor std_list.List Nil))))))))) + (term-ctor List Cons 10 + (term-ctor List Cons 20 + (term-ctor List Cons 30 + (term-ctor List Nil))))))))) diff --git a/examples/std_either_demo.ail b/examples/std_either_demo.ail index dd13bce..0fa4d8b 100644 --- a/examples/std_either_demo.ail +++ b/examples/std_either_demo.ail @@ -2,6 +2,8 @@ ; Imports std_either, exercises all five combinators. First demo to ; pass two function arguments to a single combinator (the eliminator ; `either`); first to drive a 3-type-var polymorphic fn end-to-end. +; prep.1 migration (kernel-extension-mechanics): std_either. -> +; Either.; bare Either via (import std_either). (module std_either_demo @@ -18,14 +20,14 @@ (type (fn-type (params) (ret (con Unit)) (effects IO))) (params) (body - (seq (seq (app print (app std_either.from_right 0 (term-ctor std_either.Either Right 42))) (do io/print_str "\n")) - (seq (seq (app print (app std_either.from_right 99 (term-ctor std_either.Either Left 7))) (do io/print_str "\n")) - (seq (seq (app print (app std_either.is_left (term-ctor std_either.Either Left 7))) (do io/print_str "\n")) - (seq (seq (app print (app std_either.is_right (term-ctor std_either.Either Right 42))) (do io/print_str "\n")) - (seq (seq (app print (app std_either.from_right 0 - (app std_either.map_right inc - (term-ctor std_either.Either Right 41)))) (do io/print_str "\n")) - (seq (seq (app print (app std_either.either inc inc - (term-ctor std_either.Either Left 5))) (do io/print_str "\n")) - (seq (app print (app std_either.either inc inc - (term-ctor std_either.Either Right 100))) (do io/print_str "\n"))))))))))) + (seq (seq (app print (app Either.from_right 0 (term-ctor Either Right 42))) (do io/print_str "\n")) + (seq (seq (app print (app Either.from_right 99 (term-ctor Either Left 7))) (do io/print_str "\n")) + (seq (seq (app print (app Either.is_left (term-ctor Either Left 7))) (do io/print_str "\n")) + (seq (seq (app print (app Either.is_right (term-ctor Either Right 42))) (do io/print_str "\n")) + (seq (seq (app print (app Either.from_right 0 + (app Either.map_right inc + (term-ctor Either Right 41)))) (do io/print_str "\n")) + (seq (seq (app print (app Either.either inc inc + (term-ctor Either Left 5))) (do io/print_str "\n")) + (seq (app print (app Either.either inc inc + (term-ctor Either Right 100))) (do io/print_str "\n"))))))))))) diff --git a/examples/std_either_list.ail b/examples/std_either_list.ail index d423860..df4deeb 100644 --- a/examples/std_either_list.ail +++ b/examples/std_either_list.ail @@ -17,55 +17,55 @@ (type (forall (vars e a) (fn-type - (params (con std_list.List (con std_either.Either e a))) - (ret (con std_list.List e))))) + (params (con List (con Either e a))) + (ret (con List e))))) (params xs) (body (match xs (case (pat-ctor Cons (pat-ctor Left l) t) - (term-ctor std_list.List Cons l (app lefts t))) + (term-ctor List Cons l (app lefts t))) (case (pat-ctor Cons (pat-ctor Right _) t) (app lefts t)) - (case _ (term-ctor std_list.List Nil))))) + (case _ (term-ctor List Nil))))) (fn rights (doc "Project the Right payloads of a list of Eithers into a List. Symmetric to lefts; same nested-Ctor + wildcard-tail pattern shape.") (type (forall (vars e a) (fn-type - (params (con std_list.List (con std_either.Either e a))) - (ret (con std_list.List a))))) + (params (con List (con Either e a))) + (ret (con List a))))) (params xs) (body (match xs (case (pat-ctor Cons (pat-ctor Left _) t) (app rights t)) (case (pat-ctor Cons (pat-ctor Right r) t) - (term-ctor std_list.List Cons r (app rights t))) - (case _ (term-ctor std_list.List Nil))))) + (term-ctor List Cons r (app rights t))) + (case _ (term-ctor List Nil))))) (fn partition_eithers (doc "Partition a list of Eithers into a Pair, List>: lefts on the left, rights on the right. Single pass via direct recursion; head dispatch is a flat match on the recursive result's projections.") (type (forall (vars e a) (fn-type - (params (con std_list.List (con std_either.Either e a))) - (ret (con std_pair.Pair (con std_list.List e) (con std_list.List a)))))) + (params (con List (con Either e a))) + (ret (con Pair (con List e) (con List a)))))) (params xs) (body (match xs (case (pat-ctor Nil) - (term-ctor std_pair.Pair MkPair - (term-ctor std_list.List Nil) - (term-ctor std_list.List Nil))) + (term-ctor Pair MkPair + (term-ctor List Nil) + (term-ctor List Nil))) (case (pat-ctor Cons h t) (let rest (app partition_eithers t) (match h (case (pat-ctor Left l) - (term-ctor std_pair.Pair MkPair - (term-ctor std_list.List Cons l (app std_pair.fst rest)) - (app std_pair.snd rest))) + (term-ctor Pair MkPair + (term-ctor List Cons l (app Pair.fst rest)) + (app Pair.snd rest))) (case (pat-ctor Right r) - (term-ctor std_pair.Pair MkPair - (app std_pair.fst rest) - (term-ctor std_list.List Cons r (app std_pair.snd rest))))))))))) + (term-ctor Pair MkPair + (app Pair.fst rest) + (term-ctor List Cons r (app Pair.snd rest))))))))))) diff --git a/examples/std_either_list_demo.ail b/examples/std_either_list_demo.ail index ea068e2..6692540 100644 --- a/examples/std_either_list_demo.ail +++ b/examples/std_either_list_demo.ail @@ -3,7 +3,7 @@ ; threads a List> through three combinators that ; together exercise every monomorphisation site introduced by 15g. ; -; The list is constructed inline by mixing `(term-ctor std_either.Either +; The list is constructed inline by mixing `(term-ctor Either ; Left ...)` and `(... Right ...)`. Iter 15g surfaced a `unify_for_subst` ; asymmetry that would have rejected this construction at synth time; ; 15g-aux fixed it by accepting `$u` synth-wildcards on either side of @@ -24,7 +24,7 @@ (type (fn-type (params) (ret (con Unit)) (effects IO))) (params) (body - (seq (seq (app print (app std_list.length (app std_either_list.lefts (term-ctor std_list.List Cons (term-ctor std_either.Either Left 1) (term-ctor std_list.List Cons (term-ctor std_either.Either Right 10) (term-ctor std_list.List Cons (term-ctor std_either.Either Left 2) (term-ctor std_list.List Cons (term-ctor std_either.Either Right 20) (term-ctor std_list.List Cons (term-ctor std_either.Either Right 30) (term-ctor std_list.List Nil))))))))) (do io/print_str "\n")) - (seq (seq (app print (app std_list.length (app std_either_list.rights (term-ctor std_list.List Cons (term-ctor std_either.Either Left 1) (term-ctor std_list.List Cons (term-ctor std_either.Either Right 10) (term-ctor std_list.List Cons (term-ctor std_either.Either Left 2) (term-ctor std_list.List Cons (term-ctor std_either.Either Right 20) (term-ctor std_list.List Cons (term-ctor std_either.Either Right 30) (term-ctor std_list.List Nil))))))))) (do io/print_str "\n")) - (seq (seq (app print (app std_list.length (app std_pair.fst (app std_either_list.partition_eithers (term-ctor std_list.List Cons (term-ctor std_either.Either Left 1) (term-ctor std_list.List Cons (term-ctor std_either.Either Right 10) (term-ctor std_list.List Cons (term-ctor std_either.Either Left 2) (term-ctor std_list.List Cons (term-ctor std_either.Either Right 20) (term-ctor std_list.List Cons (term-ctor std_either.Either Right 30) (term-ctor std_list.List Nil)))))))))) (do io/print_str "\n")) - (seq (app print (app std_list.length (app std_pair.snd (app std_either_list.partition_eithers (term-ctor std_list.List Cons (term-ctor std_either.Either Left 1) (term-ctor std_list.List Cons (term-ctor std_either.Either Right 10) (term-ctor std_list.List Cons (term-ctor std_either.Either Left 2) (term-ctor std_list.List Cons (term-ctor std_either.Either Right 20) (term-ctor std_list.List Cons (term-ctor std_either.Either Right 30) (term-ctor std_list.List Nil)))))))))) (do io/print_str "\n")))))))) + (seq (seq (app print (app List.length (app std_either_list.lefts (term-ctor List Cons (term-ctor Either Left 1) (term-ctor List Cons (term-ctor Either Right 10) (term-ctor List Cons (term-ctor Either Left 2) (term-ctor List Cons (term-ctor Either Right 20) (term-ctor List Cons (term-ctor Either Right 30) (term-ctor List Nil))))))))) (do io/print_str "\n")) + (seq (seq (app print (app List.length (app std_either_list.rights (term-ctor List Cons (term-ctor Either Left 1) (term-ctor List Cons (term-ctor Either Right 10) (term-ctor List Cons (term-ctor Either Left 2) (term-ctor List Cons (term-ctor Either Right 20) (term-ctor List Cons (term-ctor Either Right 30) (term-ctor List Nil))))))))) (do io/print_str "\n")) + (seq (seq (app print (app List.length (app Pair.fst (app std_either_list.partition_eithers (term-ctor List Cons (term-ctor Either Left 1) (term-ctor List Cons (term-ctor Either Right 10) (term-ctor List Cons (term-ctor Either Left 2) (term-ctor List Cons (term-ctor Either Right 20) (term-ctor List Cons (term-ctor Either Right 30) (term-ctor List Nil)))))))))) (do io/print_str "\n")) + (seq (app print (app List.length (app Pair.snd (app std_either_list.partition_eithers (term-ctor List Cons (term-ctor Either Left 1) (term-ctor List Cons (term-ctor Either Right 10) (term-ctor List Cons (term-ctor Either Left 2) (term-ctor List Cons (term-ctor Either Right 20) (term-ctor List Cons (term-ctor Either Right 30) (term-ctor List Nil)))))))))) (do io/print_str "\n")))))))) diff --git a/examples/std_list.ail b/examples/std_list.ail index e706bb5..5603913 100644 --- a/examples/std_list.ail +++ b/examples/std_list.ail @@ -1,9 +1,9 @@ ; Iter 15b — second stdlib module: polymorphic singly-linked lists. ; Imports std_maybe so head/tail can return Maybe / Maybe>. -; All cross-module references use the qualified form per the Iter 14h -; convention: `std_maybe.Maybe` at type-name slots, `std_maybe.from_maybe` -; for fns. Bare ctor names (`Just`, `Nothing`) stay unqualified — once -; the type is resolved the ctor lookup is unambiguous. +; prep.1 migration (kernel-extension-mechanics): bare `Maybe` at +; type-name slots (in scope via `(import std_maybe)`). Bare ctor +; names (`Just`, `Nothing`) stay unqualified — once the type is +; resolved the ctor lookup is unambiguous. (module std_list @@ -97,12 +97,12 @@ (forall (vars a) (fn-type (params (con List a)) - (ret (con std_maybe.Maybe a))))) + (ret (con Maybe a))))) (params xs) (body (match xs - (case (pat-ctor Nil) (term-ctor std_maybe.Maybe Nothing)) - (case (pat-ctor Cons h _) (term-ctor std_maybe.Maybe Just h))))) + (case (pat-ctor Nil) (term-ctor Maybe Nothing)) + (case (pat-ctor Cons h _) (term-ctor Maybe Just h))))) (fn tail (doc "Returns Just> of the tail, or Nothing for an empty list.") @@ -110,12 +110,12 @@ (forall (vars a) (fn-type (params (con List a)) - (ret (con std_maybe.Maybe (con List a)))))) + (ret (con Maybe (con List a)))))) (params xs) (body (match xs - (case (pat-ctor Nil) (term-ctor std_maybe.Maybe Nothing)) - (case (pat-ctor Cons _ t) (term-ctor std_maybe.Maybe Just t))))) + (case (pat-ctor Nil) (term-ctor Maybe Nothing)) + (case (pat-ctor Cons _ t) (term-ctor Maybe Just t))))) (fn append (doc "Concatenate two lists. Constructor-blocked recursion: the recursive call is inside Cons, NOT a tail.") diff --git a/examples/std_list_demo.ail b/examples/std_list_demo.ail index 695a027..72503f3 100644 --- a/examples/std_list_demo.ail +++ b/examples/std_list_demo.ail @@ -1,7 +1,9 @@ ; Iter 15b — second consumer demo. ; Imports both std_maybe and std_list. Exercises every combinator at ; least once. xs is a top-level fn `() -> List` (consts cannot -; reference user fns; the brief flagged this). +; reference user fns; the brief flagged this). prep.1 migration +; (kernel-extension-mechanics): type-scoped form for List. and +; Maybe.; bare List / Maybe via the explicit imports. (module std_list_demo @@ -34,28 +36,28 @@ (const xs (doc "The canonical list [1,2,3,4,5] for the demo. Pure ctor expression, so a const works.") - (type (con std_list.List (con Int))) + (type (con List (con Int))) (body - (term-ctor std_list.List Cons 1 - (term-ctor std_list.List Cons 2 - (term-ctor std_list.List Cons 3 - (term-ctor std_list.List Cons 4 - (term-ctor std_list.List Cons 5 - (term-ctor std_list.List Nil)))))))) + (term-ctor List Cons 1 + (term-ctor List Cons 2 + (term-ctor List Cons 3 + (term-ctor List Cons 4 + (term-ctor List Cons 5 + (term-ctor List Nil)))))))) (fn main (doc "Drive each std_list combinator once. Expected outputs (per line): 5, false, true, 1, 4, 10, 5, 2, 2, 15, 15.") (type (fn-type (params) (ret (con Unit)) (effects IO))) (params) (body - (seq (seq (app print (app std_list.length xs)) (do io/print_str "\n")) - (seq (seq (app print (app std_list.is_empty xs)) (do io/print_str "\n")) - (seq (seq (app print (app std_list.is_empty (term-ctor std_list.List Nil))) (do io/print_str "\n")) - (seq (seq (app print (app std_maybe.from_maybe -1 (app std_list.head xs))) (do io/print_str "\n")) - (seq (seq (app print (app std_list.length (app std_maybe.from_maybe xs (app std_list.tail xs)))) (do io/print_str "\n")) - (seq (seq (app print (app std_list.length (app std_list.append xs xs))) (do io/print_str "\n")) - (seq (seq (app print (app std_maybe.from_maybe -1 (app std_list.head (app std_list.reverse xs)))) (do io/print_str "\n")) - (seq (seq (app print (app std_maybe.from_maybe -1 (app std_list.head (app std_list.map double xs)))) (do io/print_str "\n")) - (seq (seq (app print (app std_list.length (app std_list.filter is_even xs))) (do io/print_str "\n")) - (seq (seq (app print (app std_list.fold_left add 0 xs)) (do io/print_str "\n")) - (seq (app print (app std_list.fold_right add 0 xs)) (do io/print_str "\n"))))))))))))))) + (seq (seq (app print (app List.length xs)) (do io/print_str "\n")) + (seq (seq (app print (app List.is_empty xs)) (do io/print_str "\n")) + (seq (seq (app print (app List.is_empty (term-ctor List Nil))) (do io/print_str "\n")) + (seq (seq (app print (app Maybe.from_maybe -1 (app List.head xs))) (do io/print_str "\n")) + (seq (seq (app print (app List.length (app Maybe.from_maybe xs (app List.tail xs)))) (do io/print_str "\n")) + (seq (seq (app print (app List.length (app List.append xs xs))) (do io/print_str "\n")) + (seq (seq (app print (app Maybe.from_maybe -1 (app List.head (app List.reverse xs)))) (do io/print_str "\n")) + (seq (seq (app print (app Maybe.from_maybe -1 (app List.head (app List.map double xs)))) (do io/print_str "\n")) + (seq (seq (app print (app List.length (app List.filter is_even xs))) (do io/print_str "\n")) + (seq (seq (app print (app List.fold_left add 0 xs)) (do io/print_str "\n")) + (seq (app print (app List.fold_right add 0 xs)) (do io/print_str "\n"))))))))))))))) diff --git a/examples/std_list_more_demo.ail b/examples/std_list_more_demo.ail index a251055..d51c419 100644 --- a/examples/std_list_more_demo.ail +++ b/examples/std_list_more_demo.ail @@ -10,23 +10,23 @@ (const xs (doc "The canonical [1, 2, 3, 4, 5] used across all checks.") - (type (con std_list.List (con Int))) + (type (con List (con Int))) (body - (term-ctor std_list.List Cons 1 - (term-ctor std_list.List Cons 2 - (term-ctor std_list.List Cons 3 - (term-ctor std_list.List Cons 4 - (term-ctor std_list.List Cons 5 - (term-ctor std_list.List Nil)))))))) + (term-ctor List Cons 1 + (term-ctor List Cons 2 + (term-ctor List Cons 3 + (term-ctor List Cons 4 + (term-ctor List Cons 5 + (term-ctor List Nil)))))))) (fn main (doc "Expected output (one per line): 0, 3, 5, 5, 3, 0.") (type (fn-type (params) (ret (con Unit)) (effects IO))) (params) (body - (seq (seq (app print (app std_list.length (app std_list.take 0 xs))) (do io/print_str "\n")) - (seq (seq (app print (app std_list.length (app std_list.take 3 xs))) (do io/print_str "\n")) - (seq (seq (app print (app std_list.length (app std_list.take 100 xs))) (do io/print_str "\n")) - (seq (seq (app print (app std_list.length (app std_list.drop 0 xs))) (do io/print_str "\n")) - (seq (seq (app print (app std_list.length (app std_list.drop 2 xs))) (do io/print_str "\n")) - (seq (app print (app std_list.length (app std_list.drop 100 xs))) (do io/print_str "\n")))))))))) + (seq (seq (app print (app List.length (app List.take 0 xs))) (do io/print_str "\n")) + (seq (seq (app print (app List.length (app List.take 3 xs))) (do io/print_str "\n")) + (seq (seq (app print (app List.length (app List.take 100 xs))) (do io/print_str "\n")) + (seq (seq (app print (app List.length (app List.drop 0 xs))) (do io/print_str "\n")) + (seq (seq (app print (app List.length (app List.drop 2 xs))) (do io/print_str "\n")) + (seq (app print (app List.length (app List.drop 100 xs))) (do io/print_str "\n")))))))))) diff --git a/examples/std_list_stress.ail b/examples/std_list_stress.ail index 80c8929..64f2a2d 100644 --- a/examples/std_list_stress.ail +++ b/examples/std_list_stress.ail @@ -10,16 +10,16 @@ (import std_list) (fn build - (doc "Build [n, n-1, ..., 1] :: std_list.List Int via Cons recursion. Constructor-blocked; not tail.") + (doc "Build [n, n-1, ..., 1] :: List Int via Cons recursion. Constructor-blocked; not tail.") (type (fn-type (params (con Int)) - (ret (con std_list.List (con Int))))) + (ret (con List (con Int))))) (params n) (body (if (app eq n 0) - (term-ctor std_list.List Nil) - (term-ctor std_list.List Cons + (term-ctor List Nil) + (term-ctor List Cons n (app build (app - n 1)))))) @@ -37,5 +37,5 @@ (type (fn-type (params) (ret (con Unit)) (effects IO))) (params) (body - (seq (seq (app print (app std_list.fold_left add 0 (app build 1000))) (do io/print_str "\n")) - (seq (app print (app std_list.fold_right add 0 (app build 1000))) (do io/print_str "\n")))))) + (seq (seq (app print (app List.fold_left add 0 (app build 1000))) (do io/print_str "\n")) + (seq (app print (app List.fold_right add 0 (app build 1000))) (do io/print_str "\n")))))) diff --git a/examples/std_maybe_demo.ail b/examples/std_maybe_demo.ail index 7811cc9..94d87bf 100644 --- a/examples/std_maybe_demo.ail +++ b/examples/std_maybe_demo.ail @@ -1,12 +1,10 @@ ; Iter 15a — first consumer of an stdlib module. ; Imports std_maybe, exercises from_maybe, is_some, is_none, map_maybe. ; First program to import a parameterised ADT (Maybe a) across module -; boundaries. Per the project's qualified-only convention (Iter 5b for -; fns, Iter 15a for types/ctors), every cross-module reference is -; qualified: `std_maybe.from_maybe` for the fn, `std_maybe.Maybe` for -; the type-name slot of `term-ctor`. The bare ctor names (`Just`, -; `Nothing`) stay unqualified — once the type is resolved, the ctor -; lookup is unambiguous within it. +; boundaries. prep.1 migration (kernel-extension-mechanics): every +; type-associated function on Maybe is now spelled in type-scoped form +; `Maybe.`, and bare `Maybe` is in scope via `(import std_maybe)` +; so the `term-ctor` type-name slot drops the module qualifier too. (module std_maybe_demo @@ -23,8 +21,8 @@ (type (fn-type (params) (ret (con Unit)) (effects IO))) (params) (body - (seq (seq (app print (app std_maybe.from_maybe 99 (term-ctor std_maybe.Maybe Just 7))) (do io/print_str "\n")) - (seq (seq (app print (app std_maybe.from_maybe 99 (term-ctor std_maybe.Maybe Nothing))) (do io/print_str "\n")) - (seq (seq (app print (app std_maybe.is_some (term-ctor std_maybe.Maybe Just 5))) (do io/print_str "\n")) - (seq (seq (app print (app std_maybe.is_none (term-ctor std_maybe.Maybe Nothing))) (do io/print_str "\n")) - (seq (app print (app std_maybe.from_maybe 0 (app std_maybe.map_maybe inc (term-ctor std_maybe.Maybe Just 41)))) (do io/print_str "\n"))))))))) + (seq (seq (app print (app Maybe.from_maybe 99 (term-ctor Maybe Just 7))) (do io/print_str "\n")) + (seq (seq (app print (app Maybe.from_maybe 99 (term-ctor Maybe Nothing))) (do io/print_str "\n")) + (seq (seq (app print (app Maybe.is_some (term-ctor Maybe Just 5))) (do io/print_str "\n")) + (seq (seq (app print (app Maybe.is_none (term-ctor Maybe Nothing))) (do io/print_str "\n")) + (seq (app print (app Maybe.from_maybe 0 (app Maybe.map_maybe inc (term-ctor Maybe Just 41)))) (do io/print_str "\n"))))))))) diff --git a/examples/std_pair_demo.ail b/examples/std_pair_demo.ail index cd6171e..53a5f83 100644 --- a/examples/std_pair_demo.ail +++ b/examples/std_pair_demo.ail @@ -1,7 +1,8 @@ ; Iter 15f — fourth consumer demo. Drives every std_pair combinator ; once. fst/snd are stable at 7/9; swap reverses; map_first/map_second ; demonstrate the Pair -> Pair / Pair reshape with -; b/a held rigid. +; b/a held rigid. prep.1 migration (kernel-extension-mechanics): +; std_pair. -> Pair.; bare Pair via (import std_pair). (module std_pair_demo @@ -24,9 +25,9 @@ (type (fn-type (params) (ret (con Unit)) (effects IO))) (params) (body - (seq (seq (app print (app std_pair.fst (term-ctor std_pair.Pair MkPair 7 9))) (do io/print_str "\n")) - (seq (seq (app print (app std_pair.snd (term-ctor std_pair.Pair MkPair 7 9))) (do io/print_str "\n")) - (seq (seq (app print (app std_pair.fst (app std_pair.swap (term-ctor std_pair.Pair MkPair 7 9)))) (do io/print_str "\n")) - (seq (seq (app print (app std_pair.snd (app std_pair.swap (term-ctor std_pair.Pair MkPair 7 9)))) (do io/print_str "\n")) - (seq (seq (app print (app std_pair.fst (app std_pair.map_first inc (term-ctor std_pair.Pair MkPair 7 9)))) (do io/print_str "\n")) - (seq (app print (app std_pair.snd (app std_pair.map_second double (term-ctor std_pair.Pair MkPair 7 9)))) (do io/print_str "\n")))))))))) + (seq (seq (app print (app Pair.fst (term-ctor Pair MkPair 7 9))) (do io/print_str "\n")) + (seq (seq (app print (app Pair.snd (term-ctor Pair MkPair 7 9))) (do io/print_str "\n")) + (seq (seq (app print (app Pair.fst (app Pair.swap (term-ctor Pair MkPair 7 9)))) (do io/print_str "\n")) + (seq (seq (app print (app Pair.snd (app Pair.swap (term-ctor Pair MkPair 7 9)))) (do io/print_str "\n")) + (seq (seq (app print (app Pair.fst (app Pair.map_first inc (term-ctor Pair MkPair 7 9)))) (do io/print_str "\n")) + (seq (app print (app Pair.snd (app Pair.map_second double (term-ctor Pair MkPair 7 9)))) (do io/print_str "\n")))))))))) diff --git a/examples/test_ct1_bare_xmod_rejected.ail.json b/examples/test_ct1_bare_xmod_rejected.ail.json index ea7b500..46d36b1 100644 --- a/examples/test_ct1_bare_xmod_rejected.ail.json +++ b/examples/test_ct1_bare_xmod_rejected.ail.json @@ -9,14 +9,14 @@ "type": { "k": "fn", "params": [], - "ret": { "k": "con", "name": "Unit" }, + "ret": { "k": "con", "name": "Mystery_Type" }, "effects": ["IO"] }, "params": [], "body": { "t": "ctor", - "type": "Ordering", - "ctor": "LT", + "type": "Mystery_Type", + "ctor": "Whatever", "args": [] } }