Brummel/AILang
1
0
Fork 0
Code Issues 29 Pull Requests Actions Packages Projects Releases Wiki Activity

iter prep.1-type-scoped-namespacing (DONE 5/5): TypeDef-first resolution + workspace pre-pass — closes #31

Browse Source 
First iteration of the kernel-extension-mechanics milestone. Ships
the type-scoped `<TypeName>.<member>` resolution path as the
canonical form for type-associated operations, narrows the
`BareCrossModuleTypeRef` / `BadCrossModuleTypeRef` diagnostics from
"bare = strictly local" to "bare = in-scope by any path", migrates
12 std-library example fixtures, and introduces a workspace-wide
normalisation pre-pass `prepare_workspace_for_check` shared between
`check_workspace` and `monomorphise_workspace`.

Architectural discovery during implementation: the plan covered the
`Term::Var` dot-qualified resolver layer plus the workspace
validator's bare-name acceptance, but the migration of bare-form
fixtures exposed five sites where bare vs. qualified type-names
needed symmetric treatment — `Term::Ctor` resolution, `Type::Con`
well-formedness, mono's poly-free-fn name/constraint-count
enumeration, codegen's `lookup_ctor_by_type` bare-name path, and
the upstream desugar-then-qualify composition. Rather than
scattering TypeDef-first ladders across each site, the implementer
centralised the work into one pre-pass that walks every consumer
module's `Type::Con.name` and `Term::Ctor.type_name`, rewriting
bare cross-module references to their qualified `<home>.<Type>`
form. This is symmetric to the pre-existing `qualify_local_types`
(owner-side); the new pre-pass is the consumer-side mirror.
Downstream passes see qualified Types regardless of authoring form.
The TypeDef-first ladder still lives in `synth`'s `Term::Var` arm
because `<TypeName>.<member>` is term-position-only — `Maybe.from_maybe`
is a Var, not a Type expression, and the pre-pass does not rewrite
Var names.

Alternatives considered:

(a) Add TypeDef-first ladder at every resolution site separately
    (the plan's implicit assumption). Rejected: O(N) extension
    sites, each carrying the same workspace-walking logic; the
    pre-pass version is O(1) — one pass, every downstream consumer
    benefits.
(b) BLOCKED + spec re-brainstorm. Rejected: the architecture
    extension is consistent with prep.1's thesis (bare type-name
    resolves to the workspace-wide TypeDef) and forward-compatible
    with prep.2 (Term::New.type_name falls under the same rewrite)
    and prep.3 (kernel-tier TypeDefs enter the workspace map
    automatically). No design regression to bounce back over.

Spec updated to document the realisation mechanism honestly: the
"Realisation mechanism — workspace pre-pass" subsection clarifies
that the resolver-level semantics described in "Implementation
shape" are the user-facing contract, and the actual code path is
the pre-pass.

Verification:

- `cargo test --workspace`: ALL GREEN. 87 e2e + every crate's unit
  + integration tests pass with no regressions.
- Three NEW in-source tests pin Task 1's resolver paths:
  `type_scoped_member_resolves`, `type_scoped_member_not_found`,
  `type_scoped_receiver_not_a_type`.
- One NEW workspace test pins the narrowed validator:
  `ct1_validator_accepts_bare_with_explicit_import`.
- One renamed-and-flipped existing test:
  `ct1_validator_rejects_bare_xmod_with_import_candidate` →
  `ct1_validator_accepts_bare_xmod_with_import_candidate` (the
  bare-with-import path is now ACCEPTED).
- One NEW companion test for the workspace-wide ctor lookup:
  `ct2_term_ctor_bare_cross_module_via_workspace_resolves`.
- Two pre-existing tests' assertions updated for the new error
  wording: `ct1_check_cli::check_human_mode_emits_actionable_message_to_stderr`
  and `crates/ailang-check/tests/workspace.rs::unknown_module_prefix_is_reported`.
- 12 migrated `.ail` fixtures verified via the existing e2e
  suite (each fixture is the test runner's target for an existing
  `build_and_run` assertion).
- Negative fixture `ct_2_bare_cross_module.ail` semantically
  preserved: dropped its `(import std_maybe)` so bare `Maybe` is
  out-of-scope under the narrowed rule and still fires
  `BareCrossModuleTypeRef`.

Concerns:

- The pre-pass introduces a new architectural layer (consumer-side
  qualification) that the spec did not originally anticipate. Spec
  amendment in this commit documents the layer. Future iterations
  reference `prepare_workspace_for_check` as established
  infrastructure.
- `examples/test_ct1_bare_xmod_rejected.ail.json` switched its
  offending name from bare `Ordering` (which under the prep.1
  semantics may now resolve via implicit prelude) to a still-
  unresolvable `Mystery_Type`. The CLI test's intent (assert that
  a human-mode `ail check` exits non-zero on a still-RED case) is
  preserved.

Milestone status: kernel-extension-mechanics (Gitea #6) advances
1/3 iters. Next: prep.2 (`Term::New` construct) issue #32.
This commit is contained in:
Brummel
2026-05-28 14:43:03 +02:00
parent 46c9aabf00
commit b586999e81
26 changed files with 925 additions and 271 deletions
Download Patch File Download Diff File Expand all files Collapse all files
bench/orchestrator-stats/2026-05-28-iter-prep.1-type-scoped-namespacing.json
+25
View File
@@ -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)."
]
}
crates/ail/src/main.rs
+6 -5
View File
@@ -1250,9 +1250,9 @@ fn workspace_error_to_diagnostic(
ailang_check::Diagnostic::error( ailang_check::Diagnostic::error(
"bare-cross-module-type-ref", "bare-cross-module-type-ref",
format!( format!(
"module `{module}` contains bare type name `{name}` that does not resolve to a local type; \ "module `{module}` references bare type `{name}`, which is not in scope. \
candidates from imports: {candidates:?}. \ Add `(import <module>)` to bring it into scope (candidates: {candidates:?}), \
Run `ail migrate-canonical-types` to fix legacy fixtures." or rewrite the call to type-scoped form `<TypeName>.<member>`."
), ),
) )
.with_ctx(serde_json::json!({ .with_ctx(serde_json::json!({
@@ -1267,8 +1267,9 @@ fn workspace_error_to_diagnostic(
ailang_check::Diagnostic::error( ailang_check::Diagnostic::error(
"bad-cross-module-type-ref", "bad-cross-module-type-ref",
format!( format!(
"module `{module}` references qualified type `{name}` but the owner module is not known \ "module `{module}` references qualified type `{name}` but the owner module \
or does not declare a type by that name" 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!({ .with_ctx(serde_json::json!({
crates/ail/tests/ct1_check_cli.rs
+11 -9
View File
@@ -29,12 +29,14 @@ fn examples_dir() -> PathBuf {
} }
/// Property: a workspace whose entry module contains a bare /// Property: a workspace whose entry module contains a bare
/// cross-module Type::Con / Term::Ctor reference — here `Ordering`, /// cross-module Type::Con / Term::Ctor reference — here `Mystery_Type`,
/// satisfiable only via the auto-injected `prelude` — is rejected by /// a name no module in the workspace declares (post-prep.1: in-scope
/// `ail check --json` with diagnostic code `bare-cross-module-type-ref` /// bare names are accepted, so the fixture uses an unresolvable name
/// and non-zero exit. Guards against `workspace_error_to_diagnostic` /// to keep firing the diagnostic) — is rejected by `ail check --json`
/// losing the `BareCrossModuleTypeRef` arm or the validator no longer /// with diagnostic code `bare-cross-module-type-ref` and non-zero
/// firing through the CLI loader path. /// exit. Guards against `workspace_error_to_diagnostic` losing the
/// `BareCrossModuleTypeRef` arm or the validator no longer firing
/// through the CLI loader path.
#[test] #[test]
fn check_json_emits_bare_cross_module_type_ref() { fn check_json_emits_bare_cross_module_type_ref() {
let fixture = examples_dir().join("test_ct1_bare_xmod_rejected.ail.json"); 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"); let stderr = String::from_utf8(output.stderr).expect("stderr is utf-8");
assert!( assert!(
stderr.contains("Ordering"), stderr.contains("Mystery_Type"),
"expected the offending type name in stderr; got {stderr}" "expected the offending type name in stderr; got {stderr}"
); );
assert!( assert!(
stderr.contains("ail migrate-canonical-types"), stderr.contains("not in scope"),
"expected the migration-command hint in stderr; got {stderr}" "expected the narrowed not-in-scope wording in stderr; got {stderr}"
); );
} }
crates/ail/tests/e2e.rs
+13 -13
View File
@@ -361,13 +361,12 @@ fn parameterised_maybe_match() {
/// cross-module reference to a parameterised ADT, including /// cross-module reference to a parameterised ADT, including
/// its ctors and a polymorphic combinator instantiated at `(Int, Int)`. /// its ctors and a polymorphic combinator instantiated at `(Int, Int)`.
/// `std_maybe_demo` imports `std_maybe`, qualifies the type-name slot /// `std_maybe_demo` imports `std_maybe` and (prep.1 migration) uses
/// of every `term-ctor` (`std_maybe.Maybe`), and exercises /// the type-scoped form: bare `Maybe` at every `term-ctor` type-name
/// `from_maybe`, `is_some`, `is_none`, and `map_maybe` once each. /// slot, `Maybe.from_maybe` / `Maybe.is_some` etc. for the
/// Property protected: the qualified-only convention (the /// combinators. Exercises four combinators once each. Property
/// authoring surface's architectural pin extended to types and /// protected: prep.1's type-scoped namespacing flows end-to-end
/// ctors per the brief) /// through check, codegen, and runtime.
/// flows end-to-end through check, codegen, and runtime.
#[test] #[test]
fn cross_module_maybe_demo() { fn cross_module_maybe_demo() {
let stdout = build_and_run("std_maybe_demo.ail"); 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. /// drives the polymorphic `std_list` combinators end-to-end.
/// Exercises a recursive cross-module ADT (`std_list.List<a>`) consumed /// Exercises a recursive cross-module ADT (`List<a>` from `std_list`,
/// from a separate module that also imports `std_maybe`. Guards the /// prep.1 type-scoped form) consumed from a separate module that
/// `qualify_local_types` propagation in both `Term::Ctor` synth and /// also imports `std_maybe`. Guards the `qualify_local_types` /
/// `Term::Match` field binding — without it, recursive ctor fields /// `qualify_workspace_types` propagation in both `Term::Ctor` synth
/// (`Cons a (List a)`) stay unqualified at the cross-module use site /// and `Term::Match` field binding — without it, recursive ctor
/// and fail to unify against the qualified scrutinee args. /// fields (`Cons a (List a)`) stay unqualified at the cross-module
/// use site and fail to unify against the qualified scrutinee args.
#[test] #[test]
fn std_list_demo() { fn std_list_demo() {
let stdout = build_and_run("std_list_demo.ail"); let stdout = build_and_run("std_list_demo.ail");
crates/ailang-check/src/lib.rs
+556 -51
View File
@@ -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")] #[error("`recur` must be in tail position of its enclosing `loop` body — it is a back-jump, not a value-producing sub-expression")]
RecurNotInTailPosition, 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 /// an internal invariant in the typechecker / mono pass
/// was violated — surfaced as an error so callers can propagate /// was violated — surfaced as an error so callers can propagate
/// rather than abort, but in well-formed inputs (typecheck has /// rather than abort, but in well-formed inputs (typecheck has
@@ -740,6 +759,8 @@ impl CheckError {
CheckError::RecurArityMismatch { .. } => "recur-arity-mismatch", CheckError::RecurArityMismatch { .. } => "recur-arity-mismatch",
CheckError::RecurTypeMismatch { .. } => "recur-type-mismatch", CheckError::RecurTypeMismatch { .. } => "recur-type-mismatch",
CheckError::RecurNotInTailPosition => "recur-not-in-tail-position", 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", CheckError::Internal(_) => "internal",
} }
} }
@@ -811,6 +832,12 @@ impl CheckError {
CheckError::RecurTypeMismatch { position, expected, got } => { CheckError::RecurTypeMismatch { position, expected, got } => {
serde_json::json!({"position": position, "expected": expected, "actual": 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()), _ => serde_json::Value::Object(serde_json::Map::new()),
} }
} }
@@ -944,6 +971,55 @@ pub fn check_module(m: &Module) -> Vec<Diagnostic> {
/// Top-level API for cross-module typecheck. /// 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 `<home>.<Type>` 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<String, IndexMap<String, TypeDef>> =
ws.modules
.iter()
.map(|(name, m)| {
let mut tys: IndexMap<String, TypeDef> = 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 /// Iterates over all modules of the workspace and checks each with access
/// to the top-level symbol tables of all other modules. Qualified /// to the top-level symbol tables of all other modules. Qualified
/// references are resolved via the import map of the respective module: /// references are resolved via the import map of the respective module:
@@ -984,20 +1060,17 @@ pub fn check_workspace(ws: &Workspace) -> Vec<Diagnostic> {
// logic runs. The rewrite is pure and per-module; we rebuild a // logic runs. The rewrite is pure and per-module; we rebuild a
// workspace shell around the desugared modules (paths and entry // workspace shell around the desugared modules (paths and entry
// are unchanged). // are unchanged).
let ws_owned = Workspace { //
entry: ws.entry.clone(), // prep.1 (kernel-extension-mechanics): after desugar, normalize
modules: ws // each consumer module's bare cross-module `Type::Con` references
.modules // to qualified form via [`prepare_workspace_for_check`]. The
.iter() // monomorphisation pass mirrors this step in its own entry
.map(|(k, m)| (k.clone(), ailang_core::desugar::desugar_module(m))) // (`monomorphise_workspace`); the two passes consume identically
.collect(), // shaped workspaces. The registry passes through unchanged — the
root_dir: ws.root_dir.clone(), // desugar pass does not touch class/instance defs (see desugar.rs:
// pass the registry through unchanged. The desugar // 22b.1 passthrough), so the registry built at load time remains
// pass does not touch class/instance defs (see desugar.rs: // valid against the prepared workspace.
// 22b.1 passthrough), so the registry built at load time let ws_owned = prepare_workspace_for_check(ws);
// remains valid against the desugared modules.
registry: ws.registry.clone(),
};
let ws = &ws_owned; let ws = &ws_owned;
// Pass 1: build per-module top-level symbol table — without checking // Pass 1: build per-module top-level symbol table — without checking
// bodies. This lets module A access defs from module B even when B // 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(()); return Ok(());
} }
// a qualified type name `module.Type` resolves // a qualified type name `module.Type` resolves
// through the import map and the per-module type table. The // through the import map and the per-module type table.
// bare-name path is unchanged. // 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 td_opt: Option<&TypeDef> = if name.matches('.').count() == 1 {
let (prefix, suffix) = name.split_once('.').expect("checked"); let (prefix, suffix) = name.split_once('.').expect("checked");
let target_module = match env.imports.get(prefix) { 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 env.module_types
.get(target_module) .get(target_module)
.and_then(|tys| tys.get(suffix)) .and_then(|tys| tys.get(suffix))
} else if let Some(td) = env.types.get(name) {
Some(td)
} else { } else {
env.types.get(name) env.module_types
.values()
.find_map(|types| types.get(name))
}; };
if let Some(td) = td_opt { if let Some(td) = td_opt {
if td.vars.len() != args.len() { if td.vars.len() != args.len() {
@@ -2950,9 +3033,11 @@ pub(crate) fn synth(
// into `env.globals` only. The unqualified-name capture // into `env.globals` only. The unqualified-name capture
// matters for dot-qualified call sites: the FreeFnCall // matters for dot-qualified call sites: the FreeFnCall
// records the suffix (e.g. `length`), not the full // records the suffix (e.g. `length`), not the full
// `std_list.length`, so `synthesise_mono_fn_for_free_fn` // `List.length` (prep.1's type-scoped form) or
// can look up the source def by its bare name in the // `std_list.length` (module-qualified form), so
// owner module's def list. // `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` // After the resolution ladder, if `raw` is a `Type::Forall`
// AND a `free_fn_owner` is known, push a `FreeFnCall` // AND a `free_fn_owner` is known, push a `FreeFnCall`
@@ -3162,13 +3247,29 @@ pub(crate) fn synth(
return Ok(inst_ty); return Ok(inst_ty);
} else if name.matches('.').count() == 1 { } else if name.matches('.').count() == 1 {
let (prefix, suffix) = name.split_once('.').expect("checked"); let (prefix, suffix) = name.split_once('.').expect("checked");
let target_module = match env.imports.get(prefix) { // prep.1: TypeDef-first ladder. If `prefix` names a
Some(m) => m.clone(), // `TypeDef` anywhere in the workspace, that type's home
None => { // module is the resolution target — type-scoped form
return Err(CheckError::UnknownModule { // `<TypeName>.<member>`. Otherwise fall back to the
module: prefix.to_string(), // legacy module-as-receiver path via `env.imports`.
}); let type_home: Option<String> = 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(|| { let g = env.module_globals.get(&target_module).ok_or_else(|| {
CheckError::UnknownModule { CheckError::UnknownModule {
@@ -3176,9 +3277,21 @@ pub(crate) fn synth(
} }
})?; })?;
let raw_ty = g.get(suffix).cloned().ok_or_else(|| { let raw_ty = g.get(suffix).cloned().ok_or_else(|| {
CheckError::UnknownImport { // If receiver resolved as a TypeDef but the suffix
module: target_module.clone(), // is missing in the home module, emit the
name: suffix.to_string(), // 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 // qualify any bare type-cons referring to a
@@ -3360,10 +3473,20 @@ pub(crate) fn synth(
} }
Term::Ctor { type_name, ctor, args } => { Term::Ctor { type_name, ctor, args } => {
// Canonical-type-lookup: Term::Ctor lookup is direct post-canonical-type-form // Canonical-type-lookup: Term::Ctor lookup is direct post-canonical-type-form
// Canonical type_name: bare = local TypeDef, qualified = // Canonical type_name: bare = local TypeDef OR (prep.1) any
// explicit cross-module. The imports-fallback (iter // bare type-name in scope via an imported module's TypeDef;
// 23.1.3) is gone — bare cross-module refs are rejected // qualified = explicit cross-module. The imports-fallback
// upstream by the workspace validator (via the canonical-form validator). // (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 // when the type is cross-module, `cdef.fields` is
// written in the owning module's local namespace. A recursive // 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 // (and any other locally-named cross-module type-cons) are
// qualified before substitution / unification. // qualified before substitution / unification.
let owning_module: Option<String>; let owning_module: Option<String>;
let result_type_name: String = type_name.clone(); let result_type_name: String;
let td = if type_name.matches('.').count() == 1 { let td = if type_name.matches('.').count() == 1 {
let (prefix, suffix) = type_name.split_once('.').expect("checked"); let (prefix, suffix) = type_name.split_once('.').expect("checked");
let target_module = match env.imports.get(prefix) { let target_module = match env.imports.get(prefix) {
@@ -3391,10 +3514,25 @@ pub(crate) fn synth(
.cloned() .cloned()
.ok_or_else(|| CheckError::UnknownType(type_name.clone()))?; .ok_or_else(|| CheckError::UnknownType(type_name.clone()))?;
owning_module = Some(target_module); owning_module = Some(target_module);
result_type_name = type_name.clone();
td td
} else if let Some(td) = env.types.get(type_name) { } else if let Some(td) = env.types.get(type_name) {
owning_module = None; owning_module = None;
result_type_name = type_name.clone();
td.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<a>`).
result_type_name = format!("{home}.{type_name}");
owning_module = Some(home);
td
} else { } else {
return Err(CheckError::UnknownType(type_name.clone())); return Err(CheckError::UnknownType(type_name.clone()));
}; };
@@ -3918,6 +4056,185 @@ fn qualify_local_types(t: &Type, owner_module: &str, local_types: &IndexMap<Stri
} }
} }
/// prep.1 (kernel-extension-mechanics): rewrites bare cross-module
/// `Type::Con` references in a consumer module's declared types into
/// qualified `<home>.<Type>` 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<String, TypeDef>,
module_types: &BTreeMap<String, IndexMap<String, TypeDef>>,
) -> 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
/// `<home>.<Type>` 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<String, TypeDef>,
module_types: &BTreeMap<String, IndexMap<String, TypeDef>>,
) -> 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<String, TypeDef>,
module_types: &BTreeMap<String, IndexMap<String, TypeDef>>,
) {
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 /// Checks a pattern against an expected type and returns the bindings
/// introduced by the pattern. /// introduced by the pattern.
fn type_check_pattern( fn type_check_pattern(
@@ -6207,17 +6524,65 @@ mod tests {
); );
} }
/// Canonical-type-lookup: a bare `Term::Ctor.type_name` that does not resolve /// prep.1 (kernel-extension-mechanics): a bare `Term::Ctor.type_name`
/// to a local TypeDef must error with `UnknownType` (or /// that does not resolve to a local TypeDef AND does not resolve
/// `UnknownCtor`, depending on which check fires first). The /// via the workspace-wide TypeDef-first ladder must error with
/// imports-fallback that previously synthesised a qualified result /// `UnknownType`. Pre-prep.1 a bare cross-module ref was always
/// from an arbitrary imported module is gone. The /// rejected at this site; post-prep.1 it is *accepted* when an
/// post-canonical-type-form validator catches this shape at load time for /// imported module declares the type (covered by
/// canonical inputs; this test pins the residual runtime guard /// `ct2_term_ctor_bare_cross_module_via_workspace_resolves`).
/// against constructed (non-loaded) AST. /// This test uses a name (`Widget`) no module declares so the
/// runtime guard still fires.
#[test] #[test]
fn ct2_term_ctor_bare_cross_module_fails_closed() { 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(), schema: SCHEMA.into(),
name: "p".into(), name: "p".into(),
imports: vec![], imports: vec![],
@@ -6233,14 +6598,12 @@ mod tests {
drop_iterative: false, drop_iterative: false,
})], })],
}; };
// Consumer imports prelude but writes BARE `Ordering` in
// Term::Ctor — this is a stale-canonical-form construction.
let consumer = Module { let consumer = Module {
schema: SCHEMA.into(), schema: SCHEMA.into(),
name: "u".into(), name: "u".into(),
imports: vec![Import { module: "p".into(), alias: None }], imports: vec![Import { module: "p".into(), alias: None }],
defs: vec![fn_def( defs: vec![fn_def(
"stale", "f",
Type::Fn { Type::Fn {
params: vec![], params: vec![],
ret: Box::new(Type::Con { ret: Box::new(Type::Con {
@@ -6260,7 +6623,7 @@ mod tests {
)], )],
}; };
let mut modules = BTreeMap::new(); let mut modules = BTreeMap::new();
modules.insert("p".into(), prelude); modules.insert("p".into(), owner);
modules.insert("u".into(), consumer); modules.insert("u".into(), consumer);
let ws = Workspace { let ws = Workspace {
entry: "u".into(), entry: "u".into(),
@@ -6270,9 +6633,8 @@ mod tests {
}; };
let diags = check_workspace(&ws); let diags = check_workspace(&ws);
assert!( assert!(
diags.iter().any(|d| d.code == "unknown-type"), diags.is_empty(),
"expected unknown-type diagnostic for bare cross-module \ "bare `Ordering` in Term::Ctor must resolve via workspace TypeDef-first ladder; got {diags:?}"
Term::Ctor; got {diags:?}"
); );
} }
@@ -6921,4 +7283,147 @@ mod tests {
"foo", "foo",
)); ));
} }
/// prep.1 (kernel-extension-mechanics): a dot-qualified `Term::Var`
/// `<TypeName>.<member>` resolves to the type's home module when
/// `<TypeName>` 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`
/// `<TypeName>.<member>` where `<TypeName>` is a known `TypeDef`
/// but `<member>` 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:?}"
);
}
} }
crates/ailang-check/src/lift.rs
+4 -3
View File
@@ -68,9 +68,10 @@ pub fn lift_letrecs(m: &Module) -> Result<Module> {
// `lift_letrecs` is a single-module pass; cross-module info isn't // `lift_letrecs` is a single-module pass; cross-module info isn't
// needed because the LetRec capture set comes from the *enclosing* // needed because the LetRec capture set comes from the *enclosing*
// fn's locals (which are always local to this module). Capture // fn's locals (which are always local to this module). Capture
// types may mention foreign type-cons (e.g. `std_list.List Int`), // types may mention foreign type-cons (e.g. `List Int` resolved
// but those flow through verbatim — the lifter never needs to // through prep.1's type-scoped namespacing, or the qualified
// resolve them. // `std_list.List Int` form), but those flow through verbatim —
// the lifter never needs to resolve them.
let mut env = Env::new(); let mut env = Env::new();
builtins::install(&mut env); builtins::install(&mut env);
crates/ailang-check/src/mono.rs
+35 -2
View File
@@ -69,6 +69,15 @@ use std::collections::{BTreeMap, BTreeSet};
/// pass does not perform new type checking — it queries types via /// pass does not perform new type checking — it queries types via
/// `synth` on already-typechecked bodies. /// `synth` on already-typechecked bodies.
pub fn monomorphise_workspace(ws: &Workspace) -> Result<Workspace> { pub fn monomorphise_workspace(ws: &Workspace) -> Result<Workspace> {
// 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. // Fast path — no class / instance defs anywhere → nothing to do.
// The pass also has no targets when there are class defs but no // The pass also has no targets when there are class defs but no
// instance defs (no callable methods at concrete types), but // 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 // 2 + 3. Imported modules' poly fns: bare (via implicit-import
// fall-through) AND dot-qualified (alias.name). // fall-through) AND dot-qualified (alias.name).
// prep.1: also enumerate type-scoped spellings
// `<TypeName>.<fn>` 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) { if let Some(imports) = env.module_imports.get(mname) {
for (alias_or_name, target_mod) in imports { for (alias_or_name, target_mod) in imports {
let target_types: Vec<String> = 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) { if let Some(target_globals) = env.module_globals.get(target_mod) {
for (n, t) in target_globals { for (n, t) in target_globals {
if matches!(t, Type::Forall { .. }) { if matches!(t, Type::Forall { .. }) {
@@ -355,6 +373,10 @@ fn poly_free_fn_names_for_module(
out.insert(n.clone()); out.insert(n.clone());
// Dot-qualified form. // Dot-qualified form.
out.insert(format!("{alias_or_name}.{n}")); 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. // 2 + 3. Imported modules' poly fns: bare AND dot-qualified.
// prep.1: also enumerate type-scoped spellings `<TypeName>.<fn>`
// per TypeDef in the imported module — mirror of
// `poly_free_fn_names_for_module`.
if let Some(imports) = env.module_imports.get(mname) { if let Some(imports) = env.module_imports.get(mname) {
for (alias_or_name, target_mod) in imports { for (alias_or_name, target_mod) in imports {
let target_types: Vec<String> = 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) { if let Some(target_globals) = env.module_globals.get(target_mod) {
for (n, t) in target_globals { for (n, t) in target_globals {
if let Type::Forall { constraints, .. } = t { if let Type::Forall { constraints, .. } = t {
out.insert(n.clone(), constraints.len()); out.insert(n.clone(), constraints.len());
out.insert(format!("{alias_or_name}.{n}"), 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 // this because instance bodies are Lam-unwrapped during synth
// (the outer Lam's `param_tys` are dropped); a free-fn body // (the outer Lam's `param_tys` are dropped); a free-fn body
// can carry arbitrary nested Lams with `Type::Var`-bearing // can carry arbitrary nested Lams with `Type::Var`-bearing
// `param_tys`, which is the case for e.g. `std_list.length` // `param_tys`, which is the case for e.g. `List.length`
// (an inner accumulating lambda over `(b, a)`). // (type-scoped, an inner accumulating lambda over `(b, a)`).
let new_type = crate::substitute_rigids(&inner_ty, &mapping); let new_type = crate::substitute_rigids(&inner_ty, &mapping);
let new_body = crate::substitute_rigids_in_term(&source_fn.body, &mapping); let new_body = crate::substitute_rigids_in_term(&source_fn.body, &mapping);
crates/ailang-check/tests/workspace.rs
+7 -3
View File
@@ -71,15 +71,19 @@ fn unknown_import_is_reported() {
#[test] #[test]
fn unknown_module_prefix_is_reported() { 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 entry = examples_dir().join("ws_unknown_module.ail");
let ws = load_workspace(&entry).expect("load ws_unknown_module"); let ws = load_workspace(&entry).expect("load ws_unknown_module");
let diags = check_workspace(&ws); let diags = check_workspace(&ws);
assert_eq!(diags.len(), 1, "got: {:?}", diags); assert_eq!(diags.len(), 1, "got: {:?}", diags);
assert!(matches!(diags[0].severity, Severity::Error)); 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!( 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") Some("nope")
); );
} }
crates/ailang-codegen/src/lib.rs
+30 -18
View File
@@ -2104,28 +2104,39 @@ impl<'a> Emitter<'a> {
} }
Ok(cref) Ok(cref)
} else { } else {
// Bare type_name is canonical-form local. Hit the // Bare type_name: try the current module's ctor table
// current module's ctor table directly; non-match is // first (canonical local case). On miss, fall back to a
// a hard error. // workspace-wide scan for a module declaring a TypeDef of
let cref = self // 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 .module_ctor_index
.get(self.module_name) .get(self.module_name)
.and_then(|m| m.get(ctor_name)) .and_then(|m| m.get(ctor_name))
.cloned() .cloned()
.ok_or_else(|| { {
CodegenError::Internal(format!( if cref.type_name == type_name {
"unknown ctor `{ctor_name}` for type `{type_name}` in module `{}`", return Ok(cref);
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
)));
} }
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 // is written in the owning module's local namespace, so a
// recursive self-reference like `Cons a (List a)` carries // recursive self-reference like `Cons a (List a)` carries
// a bare `Con("List", _)` even though every other place // a bare `Con("List", _)` even though every other place
// sees the qualified `std_list.List<...>`. Apply // sees the qualified form (`<owner_module>.List<...>`).
// Apply
// `qualify_local_types_codegen` before `unify_for_subst` // `qualify_local_types_codegen` before `unify_for_subst`
// so the unification doesn't fail on name mismatch. // so the unification doesn't fail on name mismatch.
let cref = self.lookup_ctor_by_type(type_name, ctor)?; let cref = self.lookup_ctor_by_type(type_name, ctor)?;
crates/ailang-codegen/src/subst.rs
+7 -5
View File
@@ -151,11 +151,13 @@ pub(crate) fn unify_for_subst(
/// rewrites bare `Type::Con` references that resolve against /// rewrites bare `Type::Con` references that resolve against
/// `owner_local_types` into qualified `module.Type` form. Mirrors /// `owner_local_types` into qualified `module.Type` form. Mirrors
/// `ailang_check::qualify_local_types`. Used when the codegen pulls a /// `ailang_check::qualify_local_types` and complements prep.1's
/// polymorphic fn signature across the import boundary; without this /// `qualify_workspace_types` (which qualifies consumer-side bare
/// the substitution derived from the call site's qualified args /// cross-module refs). Used when the codegen pulls a polymorphic
/// (`std_maybe.Maybe<Int>`) would fail to unify against the bare /// fn signature across the import boundary; without this the
/// signature (`Maybe<a>`). /// substitution derived from the call site's qualified args
/// (e.g. `std_maybe.Maybe<Int>`) would fail to unify against the
/// owner-local signature (`Maybe<a>`).
pub(crate) fn qualify_local_types_codegen( pub(crate) fn qualify_local_types_codegen(
t: &Type, t: &Type,
owner_module: &str, owner_module: &str,
crates/ailang-core/src/workspace.rs
+60 -33
View File
@@ -318,9 +318,9 @@ pub enum WorkspaceLoadError {
/// `candidates` lists the qualified forms found by scanning the /// `candidates` lists the qualified forms found by scanning the
/// owning module's imports in declaration order. /// owning module's imports in declaration order.
#[error( #[error(
"module `{module}` contains bare type name `{name}` that does not resolve to a local type. \ "module `{module}` references bare type `{name}`, which is not in scope. \
AILang's `.ail.json` requires cross-module type references to be qualified. \ Add `(import <module>)` to bring it into scope (candidates: {candidates:?}), \
Candidates from imports: {candidates:?}. Run `ail migrate-canonical-types` to fix legacy fixtures." or rewrite the call to type-scoped form `<TypeName>.<member>`."
)] )]
BareCrossModuleTypeRef { BareCrossModuleTypeRef {
module: String, module: String,
@@ -333,8 +333,9 @@ pub enum WorkspaceLoadError {
/// workspace, or `<owner>` is known but declares no TypeDef /// workspace, or `<owner>` is known but declares no TypeDef
/// named `<type>`. /// named `<type>`.
#[error( #[error(
"module `{module}` references qualified type `{name}` but the owner module is not known \ "module `{module}` references qualified type `{name}` but the owner module \
or does not declare a type by that name" 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 { BadCrossModuleTypeRef {
module: String, module: String,
@@ -1109,9 +1110,11 @@ fn check_type_con_name(
{ {
return Ok(()); return Ok(());
} }
// Bare cross-module — collect candidates from imports in declaration order. // prep.1: a bare cross-module type-name is ACCEPTED if it is in
// Prelude is implicit: scan it last as a fallback candidate (mirrors // scope via an explicit import or an implicit (prelude / kernel-
// iter 23.2.4's implicit-prelude behaviour in codegen). // 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<String> = Vec::new(); let mut candidates: Vec<String> = Vec::new();
for imp in import_names { for imp in import_names {
if local_types if local_types
@@ -1119,6 +1122,7 @@ fn check_type_con_name(
.map(|s| s.contains(name)) .map(|s| s.contains(name))
.unwrap_or(false) .unwrap_or(false)
{ {
in_scope = true;
candidates.push(format!("{imp}.{name}")); candidates.push(format!("{imp}.{name}"));
} }
} }
@@ -1131,9 +1135,13 @@ fn check_type_con_name(
.map(|s| s.contains(name)) .map(|s| s.contains(name))
.unwrap_or(false) .unwrap_or(false)
{ {
in_scope = true;
candidates.push(format!("{implicit}.{name}")); candidates.push(format!("{implicit}.{name}"));
} }
} }
if in_scope {
return Ok(());
}
Err(WorkspaceLoadError::BareCrossModuleTypeRef { Err(WorkspaceLoadError::BareCrossModuleTypeRef {
module: owning_module.to_string(), module: owning_module.to_string(),
name: name.to_string(), name: name.to_string(),
@@ -1855,21 +1863,46 @@ mod tests {
} }
} }
/// a bare Type::Con whose `name` resolves to one imported /// prep.1: a bare `Type::Con` whose `name` matches a `TypeDef` in
/// module's TypeDef must fire `BareCrossModuleTypeRef` with that /// an EXPLICITLY imported module must be ACCEPTED. (Pre-prep.1 this
/// qualified form in `candidates` (so the diagnostic can suggest the /// case was rejected as `BareCrossModuleTypeRef`; type-scoped form
/// fix). /// is canonical and importing the owner module brings the bare
/// type-name into scope.)
#[test] #[test]
fn ct1_validator_rejects_bare_xmod_with_import_candidate() { fn ct1_validator_accepts_bare_with_explicit_import() {
let mut modules = BTreeMap::new(); let mut modules = BTreeMap::new();
modules.insert("other".to_string(), module_with_type_def("other", "Ordering")); 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")); 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"]) 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 { match err {
WorkspaceLoadError::BareCrossModuleTypeRef { name, candidates, .. } => { WorkspaceLoadError::BareCrossModuleTypeRef { name, candidates, module } => {
assert_eq!(module, "m");
assert_eq!(name, "Ordering"); 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:?}"), other => panic!("expected BareCrossModuleTypeRef, got {other:?}"),
} }
@@ -1941,16 +1974,19 @@ mod tests {
} }
} }
/// a `Term::Ctor` whose `type_name` is a bare cross-module ref /// prep.1: a `Term::Ctor` whose `type_name` is a bare type-name
/// must fire `BareCrossModuleTypeRef`. Symmetric to the Type::Con /// from a module in scope (here `prelude`, via implicit imports)
/// rule but the field lives on Term, not Type. /// 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] #[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(); let mut modules = BTreeMap::new();
modules.insert("prelude".to_string(), modules.insert("prelude".to_string(),
module_with_type_def("prelude", "Ordering")); module_with_type_def("prelude", "Ordering"));
// Module `m` has no imports, no local Ordering, but a Term::Ctor // Module `m` has no explicit imports, no local Ordering, but a
// referencing bare `Ordering`. // Term::Ctor referencing bare `Ordering` — accepted via the
// implicit-prelude path.
let m: Module = serde_json::from_value(serde_json::json!({ let m: Module = serde_json::from_value(serde_json::json!({
"schema": crate::SCHEMA, "schema": crate::SCHEMA,
"name": "m", "name": "m",
@@ -1969,17 +2005,8 @@ mod tests {
}], }],
})).unwrap(); })).unwrap();
modules.insert("m".to_string(), m); modules.insert("m".to_string(), m);
let err = validate_canonical_type_names(&modules, &["prelude"]) validate_canonical_type_names(&modules, &["prelude"])
.expect_err("bare Term::Ctor type must be rejected"); .expect("bare Term::Ctor type must be accepted via implicit prelude import");
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:?}"),
}
} }
/// a qualified `ClassDef.name` (e.g. `other.Eq`) must fire /// a qualified `ClassDef.name` (e.g. `other.Eq`) must fire
crates/ailang-core/tests/workspace_pin.rs
+13 -7
View File
@@ -448,19 +448,25 @@ fn constraint_with_unbound_var_fires_unbound_constraint_type_var() {
} }
} }
/// pd.2 relocation: §C4 (a) carve-out fixture /// pd.2 relocation, prep.1 fixture-flip: §C4 (a) carve-out fixture
/// `test_ct1_bare_xmod_rejected.ail.json` — bare `Ordering` Term::Ctor /// `test_ct1_bare_xmod_rejected.ail.json`. Pre-prep.1 the fixture used
/// with no imports, validator catches it after prelude injection so the /// bare `Ordering` and the validator caught it via prelude-as-candidate.
/// candidate list contains `prelude.Ordering`. /// 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] #[test]
fn ct1_fixture_bare_xmod_rejected() { fn ct1_fixture_bare_xmod_rejected() {
let entry = examples_dir().join("test_ct1_bare_xmod_rejected.ail.json"); 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 { match err {
WorkspaceLoadError::BareCrossModuleTypeRef { module, name, candidates } => { WorkspaceLoadError::BareCrossModuleTypeRef { module, name, candidates } => {
assert_eq!(module, "test_ct1_bare_xmod_rejected"); assert_eq!(module, "test_ct1_bare_xmod_rejected");
assert_eq!(name, "Ordering"); assert_eq!(name, "Mystery_Type");
assert_eq!(candidates, vec!["prelude.Ordering".to_string()]); assert!(
candidates.is_empty(),
"no module declares Mystery_Type => candidates empty; got {candidates:?}"
);
} }
other => panic!("expected BareCrossModuleTypeRef, got {other:?}"), other => panic!("expected BareCrossModuleTypeRef, got {other:?}"),
} }
docs/specs/0052-kernel-extension-mechanics.md
+24
View File
@@ -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 that do not take a specific type as receiver) and as a workspace
collision disambiguator (no current collisions exist). 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
`<home>.<Type>` 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 `<TypeName>.<member>`
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/`: **Blast radius.** Per `grep -rE 'std_(maybe|pair|list|either)\.' examples/ crates/`:
- **`.ail` example fixtures** (12 with cross-module refs, plus the - **`.ail` example fixtures** (12 with cross-module refs, plus the
examples/ct_2_bare_cross_module.ail
+15 -12
View File
@@ -1,22 +1,25 @@
; Fieldtest — canonical-type-names, axis 1: BareCrossModuleTypeRef. ; Fieldtest — canonical-type-names, axis 1: BareCrossModuleTypeRef.
; ;
; A consumer of std_maybe deliberately writes a BARE `Maybe` in its ; 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 ; fn signature WITHOUT (import std_maybe). prep.1 migration
; validator, the canonical form requires cross-module type refs to ; (kernel-extension-mechanics): pre-prep.1 this fixture rejected
; be qualified. Expected: workspace-load error ; bare `Maybe` even when the import WAS present (the canonical form
; `BareCrossModuleTypeRef` naming the type and listing the qualified ; required cross-module type refs to be qualified at all times).
; form as a candidate. ; 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 ; Expected: workspace-load error `BareCrossModuleTypeRef` naming
; cross-module-qualification rule — the rule fires here at load ; the type with the narrowed wording.
; time, not deep inside the typechecker.
(module ct_2_bare_cross_module (module ct_2_bare_cross_module
(import std_maybe)
(fn classify (fn classify
(doc "Identity over Maybe<Int>; signature uses bare `Maybe` instead of `std_maybe.Maybe`.") (doc "Identity over Maybe<Int>; signature uses bare `Maybe` with no import.")
(type (type
(fn-type (fn-type
(params (con Maybe (con Int))) (params (con Maybe (con Int)))
@@ -28,4 +31,4 @@
(type (fn-type (params) (ret (con Unit)) (effects IO))) (type (fn-type (params) (ret (con Unit)) (effects IO)))
(params) (params)
(body (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)))))
examples/ct_3b_bad_qualified_known_module.ail
+4 -1
View File
@@ -2,7 +2,10 @@
; — known module, unknown type. Author qualifies as `std_maybe.Widget` ; — known module, unknown type. Author qualifies as `std_maybe.Widget`
; where `std_maybe` IS a workspace module but does not declare a ; where `std_maybe` IS a workspace module but does not declare a
; `Widget` type. Per ct.1's load-time validator, this should be ; `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 (module ct_3b_bad_qualified_known_module
examples/nested_pat.ail
+8 -5
View File
@@ -1,6 +1,9 @@
; Iter 16a — first program to use a nested constructor pattern. ; Iter 16a — first program to use a nested constructor pattern.
; Without this iter, the inner `(pat-ctor Cons b _)` would be ; Without this iter, the inner `(pat-ctor Cons b _)` would be
; rejected by the checker as `nested-ctor-pattern-not-allowed`. ; 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 (module nested_pat
@@ -10,7 +13,7 @@
(doc "Sum of the first two elements of an Int list, or 0 if shorter than two.") (doc "Sum of the first two elements of an Int list, or 0 if shorter than two.")
(type (type
(fn-type (fn-type
(params (con std_list.List (con Int))) (params (con List (con Int)))
(ret (con Int)))) (ret (con Int))))
(params xs) (params xs)
(body (body
@@ -24,7 +27,7 @@
(params) (params)
(body (body
(app print (app first_two_sum (app print (app first_two_sum
(term-ctor std_list.List Cons 10 (term-ctor List Cons 10
(term-ctor std_list.List Cons 20 (term-ctor List Cons 20
(term-ctor std_list.List Cons 30 (term-ctor List Cons 30
(term-ctor std_list.List Nil))))))))) (term-ctor List Nil)))))))))
examples/std_either_demo.ail
+13 -11
View File
@@ -2,6 +2,8 @@
; Imports std_either, exercises all five combinators. First demo to ; Imports std_either, exercises all five combinators. First demo to
; pass two function arguments to a single combinator (the eliminator ; pass two function arguments to a single combinator (the eliminator
; `either`); first to drive a 3-type-var polymorphic fn end-to-end. ; `either`); first to drive a 3-type-var polymorphic fn end-to-end.
; prep.1 migration (kernel-extension-mechanics): std_either.<fn> ->
; Either.<fn>; bare Either via (import std_either).
(module std_either_demo (module std_either_demo
@@ -18,14 +20,14 @@
(type (fn-type (params) (ret (con Unit)) (effects IO))) (type (fn-type (params) (ret (con Unit)) (effects IO)))
(params) (params)
(body (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 Either.from_right 0 (term-ctor 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 Either.from_right 99 (term-ctor 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 Either.is_left (term-ctor 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 Either.is_right (term-ctor Either Right 42))) (do io/print_str "\n"))
(seq (seq (app print (app std_either.from_right 0 (seq (seq (app print (app Either.from_right 0
(app std_either.map_right inc (app Either.map_right inc
(term-ctor std_either.Either Right 41)))) (do io/print_str "\n")) (term-ctor Either Right 41)))) (do io/print_str "\n"))
(seq (seq (app print (app std_either.either inc inc (seq (seq (app print (app Either.either inc inc
(term-ctor std_either.Either Left 5))) (do io/print_str "\n")) (term-ctor Either Left 5))) (do io/print_str "\n"))
(seq (app print (app std_either.either inc inc (seq (app print (app Either.either inc inc
(term-ctor std_either.Either Right 100))) (do io/print_str "\n"))))))))))) (term-ctor Either Right 100))) (do io/print_str "\n")))))))))))
examples/std_either_list.ail
+19 -19
View File
@@ -17,55 +17,55 @@
(type (type
(forall (vars e a) (forall (vars e a)
(fn-type (fn-type
(params (con std_list.List (con std_either.Either e a))) (params (con List (con Either e a)))
(ret (con std_list.List e))))) (ret (con List e)))))
(params xs) (params xs)
(body (body
(match xs (match xs
(case (pat-ctor Cons (pat-ctor Left l) t) (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) (case (pat-ctor Cons (pat-ctor Right _) t)
(app lefts t)) (app lefts t))
(case _ (term-ctor std_list.List Nil))))) (case _ (term-ctor List Nil)))))
(fn rights (fn rights
(doc "Project the Right payloads of a list of Eithers into a List<a>. Symmetric to lefts; same nested-Ctor + wildcard-tail pattern shape.") (doc "Project the Right payloads of a list of Eithers into a List<a>. Symmetric to lefts; same nested-Ctor + wildcard-tail pattern shape.")
(type (type
(forall (vars e a) (forall (vars e a)
(fn-type (fn-type
(params (con std_list.List (con std_either.Either e a))) (params (con List (con Either e a)))
(ret (con std_list.List a))))) (ret (con List a)))))
(params xs) (params xs)
(body (body
(match xs (match xs
(case (pat-ctor Cons (pat-ctor Left _) t) (case (pat-ctor Cons (pat-ctor Left _) t)
(app rights t)) (app rights t))
(case (pat-ctor Cons (pat-ctor Right r) t) (case (pat-ctor Cons (pat-ctor Right r) t)
(term-ctor std_list.List Cons r (app rights t))) (term-ctor List Cons r (app rights t)))
(case _ (term-ctor std_list.List Nil))))) (case _ (term-ctor List Nil)))))
(fn partition_eithers (fn partition_eithers
(doc "Partition a list of Eithers into a Pair<List<e>, List<a>>: 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.") (doc "Partition a list of Eithers into a Pair<List<e>, List<a>>: 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 (type
(forall (vars e a) (forall (vars e a)
(fn-type (fn-type
(params (con std_list.List (con std_either.Either e a))) (params (con List (con Either e a)))
(ret (con std_pair.Pair (con std_list.List e) (con std_list.List a)))))) (ret (con Pair (con List e) (con List a))))))
(params xs) (params xs)
(body (body
(match xs (match xs
(case (pat-ctor Nil) (case (pat-ctor Nil)
(term-ctor std_pair.Pair MkPair (term-ctor Pair MkPair
(term-ctor std_list.List Nil) (term-ctor List Nil)
(term-ctor std_list.List Nil))) (term-ctor List Nil)))
(case (pat-ctor Cons h t) (case (pat-ctor Cons h t)
(let rest (app partition_eithers t) (let rest (app partition_eithers t)
(match h (match h
(case (pat-ctor Left l) (case (pat-ctor Left l)
(term-ctor std_pair.Pair MkPair (term-ctor Pair MkPair
(term-ctor std_list.List Cons l (app std_pair.fst rest)) (term-ctor List Cons l (app Pair.fst rest))
(app std_pair.snd rest))) (app Pair.snd rest)))
(case (pat-ctor Right r) (case (pat-ctor Right r)
(term-ctor std_pair.Pair MkPair (term-ctor Pair MkPair
(app std_pair.fst rest) (app Pair.fst rest)
(term-ctor std_list.List Cons r (app std_pair.snd rest))))))))))) (term-ctor List Cons r (app Pair.snd rest)))))))))))
examples/std_either_list_demo.ail
+5 -5
View File
@@ -3,7 +3,7 @@
; threads a List<Either<Int, Int>> through three combinators that ; threads a List<Either<Int, Int>> through three combinators that
; together exercise every monomorphisation site introduced by 15g. ; 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` ; Left ...)` and `(... Right ...)`. Iter 15g surfaced a `unify_for_subst`
; asymmetry that would have rejected this construction at synth time; ; asymmetry that would have rejected this construction at synth time;
; 15g-aux fixed it by accepting `$u` synth-wildcards on either side of ; 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))) (type (fn-type (params) (ret (con Unit)) (effects IO)))
(params) (params)
(body (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 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 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 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 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 (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 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 (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"))))))))
examples/std_list.ail
+10 -10
View File
@@ -1,9 +1,9 @@
; Iter 15b — second stdlib module: polymorphic singly-linked lists. ; Iter 15b — second stdlib module: polymorphic singly-linked lists.
; Imports std_maybe so head/tail can return Maybe<a> / Maybe<List<a>>. ; Imports std_maybe so head/tail can return Maybe<a> / Maybe<List<a>>.
; All cross-module references use the qualified form per the Iter 14h ; prep.1 migration (kernel-extension-mechanics): bare `Maybe` at
; convention: `std_maybe.Maybe` at type-name slots, `std_maybe.from_maybe` ; type-name slots (in scope via `(import std_maybe)`). Bare ctor
; for fns. Bare ctor names (`Just`, `Nothing`) stay unqualified — once ; names (`Just`, `Nothing`) stay unqualified — once the type is
; the type is resolved the ctor lookup is unambiguous. ; resolved the ctor lookup is unambiguous.
(module std_list (module std_list
@@ -97,12 +97,12 @@
(forall (vars a) (forall (vars a)
(fn-type (fn-type
(params (con List a)) (params (con List a))
(ret (con std_maybe.Maybe a))))) (ret (con Maybe a)))))
(params xs) (params xs)
(body (body
(match xs (match xs
(case (pat-ctor Nil) (term-ctor std_maybe.Maybe Nothing)) (case (pat-ctor Nil) (term-ctor Maybe Nothing))
(case (pat-ctor Cons h _) (term-ctor std_maybe.Maybe Just h))))) (case (pat-ctor Cons h _) (term-ctor Maybe Just h)))))
(fn tail (fn tail
(doc "Returns Just<List<a>> of the tail, or Nothing for an empty list.") (doc "Returns Just<List<a>> of the tail, or Nothing for an empty list.")
@@ -110,12 +110,12 @@
(forall (vars a) (forall (vars a)
(fn-type (fn-type
(params (con List a)) (params (con List a))
(ret (con std_maybe.Maybe (con List a)))))) (ret (con Maybe (con List a))))))
(params xs) (params xs)
(body (body
(match xs (match xs
(case (pat-ctor Nil) (term-ctor std_maybe.Maybe Nothing)) (case (pat-ctor Nil) (term-ctor Maybe Nothing))
(case (pat-ctor Cons _ t) (term-ctor std_maybe.Maybe Just t))))) (case (pat-ctor Cons _ t) (term-ctor Maybe Just t)))))
(fn append (fn append
(doc "Concatenate two lists. Constructor-blocked recursion: the recursive call is inside Cons, NOT a tail.") (doc "Concatenate two lists. Constructor-blocked recursion: the recursive call is inside Cons, NOT a tail.")
examples/std_list_demo.ail
+21 -19
View File
@@ -1,7 +1,9 @@
; Iter 15b — second consumer demo. ; Iter 15b — second consumer demo.
; Imports both std_maybe and std_list. Exercises every combinator at ; Imports both std_maybe and std_list. Exercises every combinator at
; least once. xs is a top-level fn `() -> List<Int>` (consts cannot ; least once. xs is a top-level fn `() -> List<Int>` (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.<fn> and
; Maybe.<fn>; bare List / Maybe via the explicit imports.
(module std_list_demo (module std_list_demo
@@ -34,28 +36,28 @@
(const xs (const xs
(doc "The canonical list [1,2,3,4,5] for the demo. Pure ctor expression, so a const works.") (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 (body
(term-ctor std_list.List Cons 1 (term-ctor List Cons 1
(term-ctor std_list.List Cons 2 (term-ctor List Cons 2
(term-ctor std_list.List Cons 3 (term-ctor List Cons 3
(term-ctor std_list.List Cons 4 (term-ctor List Cons 4
(term-ctor std_list.List Cons 5 (term-ctor List Cons 5
(term-ctor std_list.List Nil)))))))) (term-ctor List Nil))))))))
(fn main (fn main
(doc "Drive each std_list combinator once. Expected outputs (per line): 5, false, true, 1, 4, 10, 5, 2, 2, 15, 15.") (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))) (type (fn-type (params) (ret (con Unit)) (effects IO)))
(params) (params)
(body (body
(seq (seq (app print (app std_list.length xs)) (do io/print_str "\n")) (seq (seq (app print (app 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 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 List.is_empty (term-ctor 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 Maybe.from_maybe -1 (app 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 List.length (app Maybe.from_maybe xs (app 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 List.length (app 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 Maybe.from_maybe -1 (app List.head (app 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 Maybe.from_maybe -1 (app List.head (app 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 List.length (app 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 (seq (app print (app 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 (app print (app List.fold_right add 0 xs)) (do io/print_str "\n")))))))))))))))
examples/std_list_more_demo.ail
+13 -13
View File
@@ -10,23 +10,23 @@
(const xs (const xs
(doc "The canonical [1, 2, 3, 4, 5] used across all checks.") (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 (body
(term-ctor std_list.List Cons 1 (term-ctor List Cons 1
(term-ctor std_list.List Cons 2 (term-ctor List Cons 2
(term-ctor std_list.List Cons 3 (term-ctor List Cons 3
(term-ctor std_list.List Cons 4 (term-ctor List Cons 4
(term-ctor std_list.List Cons 5 (term-ctor List Cons 5
(term-ctor std_list.List Nil)))))))) (term-ctor List Nil))))))))
(fn main (fn main
(doc "Expected output (one per line): 0, 3, 5, 5, 3, 0.") (doc "Expected output (one per line): 0, 3, 5, 5, 3, 0.")
(type (fn-type (params) (ret (con Unit)) (effects IO))) (type (fn-type (params) (ret (con Unit)) (effects IO)))
(params) (params)
(body (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 List.length (app 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 List.length (app 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 List.length (app 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 List.length (app 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 (seq (app print (app List.length (app 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 (app print (app List.length (app List.drop 100 xs))) (do io/print_str "\n"))))))))))
examples/std_list_stress.ail
+6 -6
View File
@@ -10,16 +10,16 @@
(import std_list) (import std_list)
(fn build (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 (type
(fn-type (fn-type
(params (con Int)) (params (con Int))
(ret (con std_list.List (con Int))))) (ret (con List (con Int)))))
(params n) (params n)
(body (body
(if (app eq n 0) (if (app eq n 0)
(term-ctor std_list.List Nil) (term-ctor List Nil)
(term-ctor std_list.List Cons (term-ctor List Cons
n n
(app build (app - n 1)))))) (app build (app - n 1))))))
@@ -37,5 +37,5 @@
(type (fn-type (params) (ret (con Unit)) (effects IO))) (type (fn-type (params) (ret (con Unit)) (effects IO)))
(params) (params)
(body (body
(seq (seq (app print (app std_list.fold_left 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 std_list.fold_right 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"))))))
examples/std_maybe_demo.ail
+9 -11
View File
@@ -1,12 +1,10 @@
; Iter 15a — first consumer of an stdlib module. ; Iter 15a — first consumer of an stdlib module.
; Imports std_maybe, exercises from_maybe, is_some, is_none, map_maybe. ; Imports std_maybe, exercises from_maybe, is_some, is_none, map_maybe.
; First program to import a parameterised ADT (Maybe a) across module ; First program to import a parameterised ADT (Maybe a) across module
; boundaries. Per the project's qualified-only convention (Iter 5b for ; boundaries. prep.1 migration (kernel-extension-mechanics): every
; fns, Iter 15a for types/ctors), every cross-module reference is ; type-associated function on Maybe is now spelled in type-scoped form
; qualified: `std_maybe.from_maybe` for the fn, `std_maybe.Maybe` for ; `Maybe.<fn>`, and bare `Maybe` is in scope via `(import std_maybe)`
; the type-name slot of `term-ctor`. The bare ctor names (`Just`, ; so the `term-ctor` type-name slot drops the module qualifier too.
; `Nothing`) stay unqualified — once the type is resolved, the ctor
; lookup is unambiguous within it.
(module std_maybe_demo (module std_maybe_demo
@@ -23,8 +21,8 @@
(type (fn-type (params) (ret (con Unit)) (effects IO))) (type (fn-type (params) (ret (con Unit)) (effects IO)))
(params) (params)
(body (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 Maybe.from_maybe 99 (term-ctor 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 Maybe.from_maybe 99 (term-ctor 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 Maybe.is_some (term-ctor 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 (seq (app print (app Maybe.is_none (term-ctor 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 (app print (app Maybe.from_maybe 0 (app Maybe.map_maybe inc (term-ctor Maybe Just 41)))) (do io/print_str "\n")))))))))
examples/std_pair_demo.ail
+8 -7
View File
@@ -1,7 +1,8 @@
; Iter 15f — fourth consumer demo. Drives every std_pair combinator ; Iter 15f — fourth consumer demo. Drives every std_pair combinator
; once. fst/snd are stable at 7/9; swap reverses; map_first/map_second ; once. fst/snd are stable at 7/9; swap reverses; map_first/map_second
; demonstrate the Pair<a, b> -> Pair<c, b> / Pair<a, c> reshape with ; demonstrate the Pair<a, b> -> Pair<c, b> / Pair<a, c> reshape with
; b/a held rigid. ; b/a held rigid. prep.1 migration (kernel-extension-mechanics):
; std_pair.<fn> -> Pair.<fn>; bare Pair via (import std_pair).
(module std_pair_demo (module std_pair_demo
@@ -24,9 +25,9 @@
(type (fn-type (params) (ret (con Unit)) (effects IO))) (type (fn-type (params) (ret (con Unit)) (effects IO)))
(params) (params)
(body (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 Pair.fst (term-ctor 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 Pair.snd (term-ctor 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 Pair.fst (app Pair.swap (term-ctor 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 Pair.snd (app Pair.swap (term-ctor 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 (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 std_pair.snd (app std_pair.map_second double (term-ctor std_pair.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"))))))))))
examples/test_ct1_bare_xmod_rejected.ail.json
+3 -3
View File
@@ -9,14 +9,14 @@
"type": { "type": {
"k": "fn", "k": "fn",
"params": [], "params": [],
"ret": { "k": "con", "name": "Unit" }, "ret": { "k": "con", "name": "Mystery_Type" },
"effects": ["IO"] "effects": ["IO"]
}, },
"params": [], "params": [],
"body": { "body": {
"t": "ctor", "t": "ctor",
"type": "Ordering", "type": "Mystery_Type",
"ctor": "LT", "ctor": "Whatever",
"args": [] "args": []
} }
} }