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

iter 23.1.3: implicit prelude import + symmetric bare-type-name imports-fallback in Term::Ctor synth

Browse Source
This commit is contained in:
Brummel
2026-05-10 21:24:16 +02:00
parent 927f7ea38f
commit 842df380a4
2 changed files with 178 additions and 7 deletions
Download Patch File Download Diff File Expand all files Collapse all files
crates/ailang-check/src/lib.rs
+171 -6
View File
@@ -443,6 +443,18 @@ pub enum CheckError {
candidates: Vec<String>,
},
/// Iter 23.1.3: a bare `Term::Ctor.type_name` did not resolve
/// against the current module's local `env.types` and resolved
/// against type defs in two or more imported modules. The author
/// must qualify the type-name (e.g. write `std_maybe.Maybe` instead
/// of bare `Maybe`). Code: `ambiguous-type`.
/// `ctx`: `{"type_name": "<n>", "candidates": ["m1.T", "m2.T"]}`.
#[error("ambiguous type `{type_name}`: declared in {candidates:?}")]
AmbiguousType {
type_name: String,
candidates: Vec<String>,
},
/// Iter 18d.1: a `Term::ReuseAs { body, .. }` was found whose `body`
/// is not an allocating Term variant (i.e. not `Term::Ctor` and not
/// `Term::Lam`). `(reuse-as ...)` only makes sense when the body
@@ -542,6 +554,7 @@ impl CheckError {
CheckError::InvalidDefName { .. } => "invalid-def-name",
CheckError::TailCallNotInTailPosition => "tail-call-not-in-tail-position",
CheckError::AmbiguousCtor { .. } => "ambiguous-ctor",
CheckError::AmbiguousType { .. } => "ambiguous-type",
CheckError::ReuseAsNonAllocatingBody { .. } => "reuse-as-non-allocating-body",
CheckError::MissingConstraint { .. } => "missing-constraint",
CheckError::NoInstance { .. } => "no-instance",
@@ -583,6 +596,9 @@ impl CheckError {
CheckError::AmbiguousCtor { ctor, candidates } => {
serde_json::json!({"ctor": ctor, "candidates": candidates})
}
CheckError::AmbiguousType { type_name, candidates } => {
serde_json::json!({"type_name": type_name, "candidates": candidates})
}
CheckError::ReuseAsNonAllocatingBody { got, .. } => {
serde_json::json!({"got": got})
}
@@ -1179,6 +1195,16 @@ pub fn build_check_env(ws: &Workspace) -> Env {
let key = imp.alias.clone().unwrap_or_else(|| imp.module.clone());
import_map.insert(key, imp.module.clone());
}
// Iter 23.1: the prelude module is implicitly imported into
// every non-prelude module. A user-declared explicit
// `import { module: "prelude" }` would already place
// "prelude" in the map above (idempotent insert via entry).
// The prelude module itself does not import itself.
if m.name != "prelude" {
import_map
.entry("prelude".to_string())
.or_insert_with(|| "prelude".to_string());
}
env.module_imports.insert(m.name.clone(), import_map);
}
@@ -1271,6 +1297,15 @@ fn check_in_workspace(
let key = imp.alias.clone().unwrap_or_else(|| imp.module.clone());
import_map.insert(key, imp.module.clone());
}
// Iter 23.1: the prelude module is implicitly imported into
// every non-prelude module's body-check env. Mirrors the
// workspace-flat overlay in `build_check_env`. The prelude
// itself does not import itself.
if m.name != "prelude" {
import_map
.entry("prelude".to_string())
.or_insert_with(|| "prelude".to_string());
}
env.imports = import_map;
env.current_module = m.name.clone();
@@ -1913,6 +1948,12 @@ pub(crate) fn synth(
// (and any other locally-named cross-module type-cons) are
// qualified before substitution / unification.
let owning_module: Option<String>;
// Iter 23.1.3: the name embedded in the result `Type::Con`.
// Defaults to the user-written `type_name` (qualified form
// for the `module.Type` branch, bare for the local branch),
// and is upgraded to `imp.Type` when the bare-name
// imports-fallback resolves through an imported module.
let mut result_type_name: String = type_name.clone();
let td = if type_name.matches('.').count() == 1 {
let (prefix, suffix) = type_name.split_once('.').expect("checked");
let target_module = match env.imports.get(prefix) {
@@ -1930,12 +1971,51 @@ pub(crate) fn synth(
.ok_or_else(|| CheckError::UnknownType(type_name.clone()))?;
owning_module = Some(target_module);
td
} else {
} else if let Some(td) = env.types.get(type_name) {
// Local hit: original Iter 13 behaviour.
owning_module = None;
env.types
.get(type_name)
.ok_or_else(|| CheckError::UnknownType(type_name.clone()))?
.clone()
td.clone()
} else {
// Iter 23.1.3: bare type-name not present locally —
// scan imported modules for a type by this name.
// Symmetric to `Pattern::Ctor`'s fallback at this
// file's ~lib.rs:2453; required so an LLM author can
// write `(con Ordering LT)` against a prelude type
// without qualifying it as `prelude.Ordering`. The
// result `Type::Con` carries the qualified name so
// that downstream `Pattern::Ctor` resolution (which
// already produces qualified names from its own
// imports-fallback) lines up against the scrutinee.
let mut hits: Vec<(String, String, TypeDef)> = Vec::new();
for imp in env.imports.values() {
if let Some(tys) = env.module_types.get(imp) {
if let Some(td) = tys.get(type_name) {
hits.push((
format!("{imp}.{type_name}"),
imp.clone(),
td.clone(),
));
}
}
}
match hits.len() {
0 => {
return Err(CheckError::UnknownType(type_name.clone()));
}
1 => {
let (qname, owner, td) =
hits.into_iter().next().expect("len == 1");
owning_module = Some(owner);
result_type_name = qname;
td
}
_ => {
return Err(CheckError::AmbiguousType {
type_name: type_name.clone(),
candidates: hits.into_iter().map(|(q, _, _)| q).collect(),
});
}
}
};
let cdef = td
.ctors
@@ -1990,7 +2070,7 @@ pub(crate) fn synth(
unify(&exp_inst, &actual, subst)?;
}
Ok(Type::Con {
name: type_name.clone(),
name: result_type_name,
args: type_args,
})
}
@@ -3713,6 +3793,91 @@ mod tests {
assert!(diags.is_empty(), "expected green; got {diags:?}");
}
/// Iter 23.1: the prelude module is implicitly imported into
/// every user module. A user module that pattern-matches on
/// `LT` / `EQ` / `GT` without an explicit
/// `import { module: "prelude" }` must typecheck cleanly.
#[test]
fn user_module_can_pattern_match_on_prelude_ordering_bare() {
let prelude = Module {
schema: SCHEMA.into(),
name: "prelude".into(),
imports: vec![],
defs: vec![Def::Type(TypeDef {
name: "Ordering".into(),
vars: vec![],
ctors: vec![
Ctor { name: "LT".into(), fields: vec![] },
Ctor { name: "EQ".into(), fields: vec![] },
Ctor { name: "GT".into(), fields: vec![] },
],
doc: None,
drop_iterative: false,
})],
};
let consumer = Module {
schema: SCHEMA.into(),
name: "user".into(),
imports: vec![],
defs: vec![fn_def(
"from_lt",
Type::Fn {
params: vec![],
ret: Box::new(Type::int()),
effects: vec![],
param_modes: vec![],
ret_mode: ParamMode::Implicit,
},
vec![],
Term::Match {
scrutinee: Box::new(Term::Ctor {
type_name: "Ordering".into(),
ctor: "LT".into(),
args: vec![],
}),
arms: vec![
Arm {
pat: Pattern::Ctor {
ctor: "LT".into(),
fields: vec![],
},
body: Term::Lit { lit: Literal::Int { value: 1 } },
},
Arm {
pat: Pattern::Ctor {
ctor: "EQ".into(),
fields: vec![],
},
body: Term::Lit { lit: Literal::Int { value: 2 } },
},
Arm {
pat: Pattern::Ctor {
ctor: "GT".into(),
fields: vec![],
},
body: Term::Lit { lit: Literal::Int { value: 3 } },
},
],
},
)],
};
let mut modules = BTreeMap::new();
modules.insert("prelude".into(), prelude);
modules.insert("user".into(), consumer);
let ws = Workspace {
entry: "user".into(),
modules,
root_dir: std::path::PathBuf::from("."),
registry: ailang_core::workspace::Registry::default(),
};
let diags = check_workspace(&ws);
assert!(
diags.is_empty(),
"user module must typecheck bare-LT without explicit prelude import; got: {:?}",
diags
);
}
/// Iter 14e: a `Term::App { tail: true, .. }` that genuinely sits
/// in tail position (as the rhs of a `Seq` that is the body of a
/// `Match` arm that is the body of the fn) must pass.
crates/ailang-check/tests/env_construction_pin.rs
+7 -1
View File
@@ -72,13 +72,19 @@ fn build_env_inline_pre_refactor(ws: &ailang_core::workspace::Workspace) -> Env
}
env.module_types = module_types;
// env.module_imports — per-module alias map.
// env.module_imports — per-module alias map. Iter 23.1: every
// non-prelude module implicitly imports the prelude module.
for m in ws.modules.values() {
let mut import_map: BTreeMap<String, String> = BTreeMap::new();
for imp in &m.imports {
let key = imp.alias.clone().unwrap_or_else(|| imp.module.clone());
import_map.insert(key, imp.module.clone());
}
if m.name != "prelude" {
import_map
.entry("prelude".to_string())
.or_insert_with(|| "prelude".to_string());
}
env.module_imports.insert(m.name.clone(), import_map);
}