From 3723495d8adfeb670e7b95e812a5c32c534b71bc Mon Sep 17 00:00:00 2001 From: Brummel Date: Mon, 11 May 2026 01:04:39 +0200 Subject: [PATCH] iter ct.1.2: validator extends to Term::Ctor.type_name --- crates/ailang-core/src/workspace.rs | 159 ++++++++++++++++++++++++++++ 1 file changed, 159 insertions(+) diff --git a/crates/ailang-core/src/workspace.rs b/crates/ailang-core/src/workspace.rs index dc3fc17..eac0fe6 100644 --- a/crates/ailang-core/src/workspace.rs +++ b/crates/ailang-core/src/workspace.rs @@ -819,6 +819,11 @@ pub(crate) fn validate_canonical_type_names( } Ok(()) })?; + walk_def_terms(def, &mut |type_name: &str| { + check_type_con_name( + type_name, mod_name, &local_types, &import_names, + ) + })?; } } @@ -1028,6 +1033,119 @@ where } } +/// ct.1: walk every `Term::Ctor.type_name` reachable from a single +/// `Def`, calling `f` on the type_name strings. Used to enforce the +/// canonical-form rule on term-side type references. +fn walk_def_terms(def: &Def, f: &mut F) -> Result<(), WorkspaceLoadError> +where + F: FnMut(&str) -> Result<(), WorkspaceLoadError>, +{ + match def { + Def::Fn(fd) => walk_term(&fd.body, f), + Def::Const(cd) => walk_term(&cd.value, f), + Def::Type(_) => Ok(()), + Def::Class(cd) => { + for cm in &cd.methods { + if let Some(body) = &cm.default { + walk_term(body, f)?; + } + } + Ok(()) + } + Def::Instance(id) => { + for im in &id.methods { + walk_term(&im.body, f)?; + } + Ok(()) + } + } +} + +/// ct.1: recursive walk of a `Term`, calling `f` on every +/// `Term::Ctor.type_name`. Embedded `Type` annotations (Lam param / +/// return types, LetRec types) ride the `walk_def_types` / +/// `walk_term_embedded_types` path — but `Term::Ctor.type_name` is +/// a `String`, not a `Type`, so it lives here. +fn walk_term(t: &Term, f: &mut F) -> Result<(), WorkspaceLoadError> +where + F: FnMut(&str) -> Result<(), WorkspaceLoadError>, +{ + match t { + Term::Lit { .. } | Term::Var { .. } => Ok(()), + Term::App { callee, args, .. } => { + walk_term(callee, f)?; + for a in args { + walk_term(a, f)?; + } + Ok(()) + } + Term::Let { value, body, .. } => { + walk_term(value, f)?; + walk_term(body, f) + } + Term::LetRec { body, in_term, .. } => { + walk_term(body, f)?; + walk_term(in_term, f) + } + Term::If { cond, then, else_ } => { + walk_term(cond, f)?; + walk_term(then, f)?; + walk_term(else_, f) + } + Term::Do { args, .. } => { + for a in args { + walk_term(a, f)?; + } + Ok(()) + } + Term::Ctor { type_name, args, .. } => { + f(type_name)?; + for a in args { + walk_term(a, f)?; + } + Ok(()) + } + Term::Match { scrutinee, arms } => { + walk_term(scrutinee, f)?; + for arm in arms { + walk_pattern(&arm.pat, f)?; + walk_term(&arm.body, f)?; + } + Ok(()) + } + Term::Lam { body, .. } => walk_term(body, f), + Term::Seq { lhs, rhs } => { + walk_term(lhs, f)?; + walk_term(rhs, f) + } + Term::Clone { value } => walk_term(value, f), + Term::ReuseAs { source, body } => { + walk_term(source, f)?; + walk_term(body, f) + } + } +} + +/// ct.1: Pattern::Ctor carries a `ctor` name (matches against a +/// scrutinee's TypeDef) but NOT a type_name field — the type is +/// inferred from the scrutinee. So Pattern walking only recurses; +/// no canonical-form check fires here. +fn walk_pattern(p: &crate::ast::Pattern, f: &mut F) -> Result<(), WorkspaceLoadError> +where + F: FnMut(&str) -> Result<(), WorkspaceLoadError>, +{ + use crate::ast::Pattern; + match p { + Pattern::Wild | Pattern::Var { .. } | Pattern::Lit { .. } => Ok(()), + Pattern::Ctor { fields, .. } => { + for sub in fields { + walk_pattern(sub, f)?; + } + Ok(()) + } + } +} + /// Iter 22b.1: extract the head-constructor name of a type, for the /// "where is this type defined" lookup and for diagnostic-message /// rendering. @@ -1885,4 +2003,45 @@ mod tests { other => panic!("expected BareCrossModuleTypeRef, got {other:?}"), } } + + /// ct.1: a `Term::Ctor` whose `type_name` is a bare cross-module ref + /// must fire `BareCrossModuleTypeRef`. Symmetric to the Type::Con + /// rule but the field lives on Term, not Type. + #[test] + fn ct1_validator_rejects_bare_term_ctor_type_name() { + let mut modules = BTreeMap::new(); + modules.insert("prelude".to_string(), + module_with_type_def("prelude", "Ordering")); + // Module `m` has no imports, no local Ordering, but a Term::Ctor + // referencing bare `Ordering`. + let m: Module = serde_json::from_value(serde_json::json!({ + "schema": crate::SCHEMA, + "name": "m", + "imports": [], + "defs": [{ + "kind": "fn", + "name": "f", + "type": { "k": "fn", "params": [], "ret": { "k": "con", "name": "Unit" }, "effects": [] }, + "params": [], + "body": { + "t": "ctor", + "type": "Ordering", + "ctor": "LT", + "args": [] + } + }], + })).unwrap(); + modules.insert("m".to_string(), m); + let err = validate_canonical_type_names(&modules) + .expect_err("bare Term::Ctor type must be rejected"); + match err { + WorkspaceLoadError::BareCrossModuleTypeRef { module, name, candidates } => { + assert_eq!(module, "m"); + assert_eq!(name, "Ordering"); + assert_eq!(candidates, vec!["prelude.Ordering".to_string()], + "prelude is implicit-fallback"); + } + other => panic!("expected BareCrossModuleTypeRef, got {other:?}"), + } + } }