From b6df4d146285cfedaa96177858494548ddadbf67 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 10 Nov 2026 18:44:57 +0000 Subject: [PATCH 1/2] feat(desugar): a type alias and an extern type follow the rule of data types Owner decision 2026-11-10: a module names a `type` alias or an extern type when it declares it, or when it imports the module that declares it. An alias must also be `pub`. An extern type is public, as an extern function is. An import list must name the type. Each module used to see each alias and each extern type of the program, with no import. A data type, an alias and an extern type are now in the one type table of the scope of a module, so a declaration of a name shadows an imported type of each kind. A type that a module cannot name is refused by name: "unknown type `Feet`". No program of the corpus changed. New test: a_module_names_an_alias_or_an_extern_type_only_through_an_import. 624 tests pass; the all-target count is 621. Co-Authored-By: Claude Fable 5.2 Claude-Session: https://claude.ai/code/session_0136P7ZmKrYLDC4WHi2yt11u --- TEST-NEEDS.adoc | 6 +- src/ephapax-cli/tests/run_wasm.rs | 99 +++++++++++++ src/ephapax-desugar/src/lib.rs | 233 +++++++++++++++--------------- src/ephapax-driver/src/lib.rs | 4 +- 4 files changed, 218 insertions(+), 124 deletions(-) diff --git a/TEST-NEEDS.adoc b/TEST-NEEDS.adoc index 20cfd5d..a6e1ebb 100644 --- a/TEST-NEEDS.adoc +++ b/TEST-NEEDS.adoc @@ -21,9 +21,9 @@ compliance, 16 tests) performance, correctness, 13 tests) * Benchmarks: `+src/ephapax-parser/benches/parse_bench.rs+`, `+src/ephapax-vram-cache/benches/cache_bench.rs+` -* Total: *620 tests* (`+cargo test --workspace --all-targets+`); +* Total: *621 tests* (`+cargo test --workspace --all-targets+`); pass/fail enforced by `+rust-ci.yml+` -* Documented all-target tests: 620 +* Documented all-target tests: 621 === CRG Testing Taxonomy — Status @@ -83,7 +83,7 @@ eliminator-fork invariant + its gated capstone, per PROOF-NEEDS.adoc §4) ==== Build & Execution * [x] cargo build — compiles -* [x] cargo test –workspace –all-targets — 620 pass, 0 fail +* [x] cargo test –workspace –all-targets — 621 pass, 0 fail * [x] idris2/ephapax-parse-tests.ipkg — compiles AND runs green (2026-07-07, idris2 0.8.0 + zig-built libephapax_tokbuf.so); CI-gated compile-only by abi-verify.yml `+idris2-parse-front+` (runtime run stays diff --git a/src/ephapax-cli/tests/run_wasm.rs b/src/ephapax-cli/tests/run_wasm.rs index 346f631..0c53800 100644 --- a/src/ephapax-cli/tests/run_wasm.rs +++ b/src/ephapax-cli/tests/run_wasm.rs @@ -508,6 +508,105 @@ fn a_module_names_a_data_type_only_through_a_pub_import() { } } +/// A `type` alias and an extern type follow the rule of data types (owner +/// decision 2026-11-10): a module names one when it declares it, or when +/// it imports the module that declares it. An alias must also be `pub`; +/// an extern type is public, as an extern function is. Each module used +/// to see each alias and each extern type of the program. +#[test] +fn a_module_names_an_alias_or_an_extern_type_only_through_an_import() { + let tmp = tempfile::tempdir().expect("tempdir"); + let write = + |name: &str, text: &str| std::fs::write(tmp.path().join(name), text).expect("write module"); + write( + "lib.eph", + "module lib\n\npub type Meters = I32\n\ntype Feet = I32\n\n\ + pub fn double(m: Meters): Meters = m + m\n\n\ + pub fn feet(n: I32): Feet = n\n", + ); + write( + "host.eph", + "module host\n\nextern \"c\" {\n type Handle\n fn open(n: I32): Handle\n \ + fn close(h: Handle): I32\n}\n", + ); + write( + "mid.eph", + "module mid\n\nimport host\n\npub fn via(n: I32): I32 = close(open(n))\n", + ); + let keep = "fn keep(m: Meters): Meters = m\n"; + let pass = "fn pass(h: Handle): Handle = h\n"; + + // (imports and declarations, `main` body, output) + for (head, main, want) in [ + (format!("import lib\n\n{keep}"), "double(keep(4))", "8"), + // An import list names the alias. + ( + format!("import lib(Meters, double)\n\n{keep}"), + "double(keep(4))", + "8", + ), + // A function of `lib` has the private alias in its signature. + ("import lib\n".to_string(), "feet(3)", "3"), + // A declaration of the module shadows an imported alias. + ( + "import lib\n\ndata Meters = M(I32)\n".to_string(), + "match M(5) of | M(n) => n end", + "5", + ), + ] { + write( + "app.eph", + &format!("module app\n\n{head}\nfn main(): I32 = {main}\n"), + ); + for args in [&["run", "app.eph"][..], &["run", "--interp", "app.eph"]] { + assert_eq!(stdout_of(tmp.path(), args), want, "{main} under {args:?}"); + } + } + + // (imports and declarations, text of the load error; `None`: it compiles). + // The host of `run` does not have `open`, so these programs do not run. + let main = "close(pass(open(1)))"; + for (head, error) in [ + (format!("import host\n\n{pass}"), None), + (format!("import host(Handle, open, close)\n\n{pass}"), None), + // The import list does not name the type. + ( + format!("import host(open, close)\n\n{pass}"), + Some("unknown type `Handle`"), + ), + // An extern type of a module that this module does not import. + ( + format!("import mid\n\n{pass}"), + Some("unknown type `Handle`"), + ), + // A private alias, and an alias that the import list does not name. + ( + "import lib\n\nfn keep(f: Feet): Feet = f\n".to_string(), + Some("unknown type `Feet`"), + ), + ( + format!("import lib(double)\n\n{keep}"), + Some("unknown type `Meters`"), + ), + ] { + let body = if head.contains("Handle") { main } else { "0" }; + write( + "app.eph", + &format!("module app\n\n{head}\nfn main(): I32 = {body}\n"), + ); + let out = ephapax(tmp.path(), &["compile", "app.eph"]); + let stderr = String::from_utf8_lossy(&out.stderr); + match error { + None => assert!(out.status.success(), "{head}: stderr:\n{stderr}"), + Some(error) => assert!( + !out.status.success() && stderr.contains(error), + "{head}: exit {:?}, stderr:\n{stderr}", + out.status.code() + ), + } + } +} + /// v2 plan rung E7: an arm with a false guard gives the value to the next /// arm, as wasm and in the interpreter. The desugarer used to take a /// guarded constructor arm without a look at its guard. diff --git a/src/ephapax-desugar/src/lib.rs b/src/ephapax-desugar/src/lib.rs index e386e6d..8e3a3a8 100644 --- a/src/ephapax-desugar/src/lib.rs +++ b/src/ephapax-desugar/src/lib.rs @@ -160,26 +160,46 @@ struct ConstructorInfo { home: SmolStr, } -/// A data type as its module declares it. +/// A named type as its module declares it. #[derive(Debug, Clone)] -struct DataInfo { - params: Vec, - ctors: Vec, - /// Key of the module that declares the type. The names in the - /// fields of `ctors` are names in the scope of that module. +struct TypeInfo { + def: TypeDef, + /// Key of the module that declares the type. The names in `def` are + /// names in the scope of that module. home: SmolStr, - /// `pub data`: a module that imports `home` can name the type. + /// A module that imports `home` can name the type: `pub data`, + /// `pub type`, and each extern type (as each extern function). public: bool, } -/// The data types and the constructors that one module can name: its +/// What a type name stands for. +#[derive(Debug, Clone)] +enum TypeDef { + /// `data Foo(a) = A | B(a)`. + Data { + params: Vec, + ctors: Vec, + }, + /// `type Foo = T`, with `T` in surface form: `desugar_named_type` + /// expands it on demand. Record and sum declarations are already + /// lowered to `Prod`/`Sum`/`Tuple` by `parse_type_decl`. + Alias(SurfaceTy), + /// `extern "abi" { type Foo }`: nominal and opaque. It resolves to + /// `Ty::Var("Foo")`, a rigid type variable that unifies only with + /// itself, so a `Window` is never an `IpcChannel`. + Extern, +} + +/// The named types and the constructors that one module can name: its /// own, and the public ones of the modules that it imports. #[derive(Debug, Clone, Default)] struct Scope { /// Constructor name → info constructors: HashMap, - /// Data type name → declaration - types: HashMap, + /// Type name → declaration. A data type, an alias and an extern + /// type share the one table: a later declaration of a name shadows + /// an earlier one of each kind. + types: HashMap, } /// The key of a module in the registry. `Foo.Bar` and `Foo/Bar` name the @@ -193,31 +213,13 @@ fn module_key(name: &str) -> SmolStr { /// Maps constructor names to their encoding information. This is built /// from `DataDecl` nodes and used to desugar `Construct` and `Match`. /// Each module has its own [`Scope`], as it has for functions: a module -/// names a data type of another module only when it imports that module -/// and the type is `pub`. +/// names a data type, a `type` alias or an extern type of another module +/// only when it imports that module and the type is public. #[derive(Debug, Clone, Default)] pub struct DataRegistry { /// Module key → what the module can name. The key is the empty /// string for declarations registered with no module. scopes: HashMap, - /// Names declared via `extern "abi" { type Foo }` blocks. - /// - /// Extern types are nominal and opaque: the desugar pass resolves - /// `SurfaceTy::Named { name: "Foo", args: [] }` to `Ty::Var("Foo")` - /// rather than emitting an `UnknownType` error. The type checker - /// then treats them as rigid type variables that only unify with - /// themselves (so values of type `Window` cannot be confused with - /// `IpcChannel`, etc.). - extern_types: std::collections::HashSet, - /// `type Foo = T` aliases — captured in their pre-desugar surface - /// form so `desugar_named_type` can recursively expand them on - /// demand. The stored value is whatever the parser produced for the - /// alias body (record/sum decls already pre-lowered to `Prod`/`Sum`/ - /// `Tuple` by `parse_type_decl`). An alias is visible in each module. - /// Each entry has the key of the module that declares the alias: the - /// body expands in the scope of that module, and a module that - /// declares an alias of the same name gets its own. - type_aliases: HashMap>, } impl DataRegistry { @@ -240,31 +242,44 @@ impl DataRegistry { }, ); } - scope.types.insert( - decl.name.clone(), - DataInfo { - params: decl.params.clone(), - ctors: decl.constructors.clone(), - home: home.into(), - public: decl.visibility == SurfaceVisibility::Public, - }, - ); + let def = TypeDef::Data { + params: decl.params.clone(), + ctors: decl.constructors.clone(), + }; + let public = decl.visibility == SurfaceVisibility::Public; + self.register_type(home, &decl.name, def, public); + } + + /// Give the type name `name` its meaning in the module `home`. + fn register_type(&mut self, home: &str, name: &SmolStr, def: TypeDef, public: bool) { + let home: SmolStr = home.into(); + let info = TypeInfo { + def, + home: home.clone(), + public, + }; + let scope = self.scopes.entry(home).or_default(); + scope.types.insert(name.clone(), info); } - /// Bring the public data types that the module `from` declares, with - /// their constructors, into the scope of the module `into`. A list of - /// `names` that is not empty limits the import to the types in it. - /// Returns the names of the imported types. + /// Bring the public types that the module `from` declares, and the + /// constructors of its data types, into the scope of the module + /// `into`. A list of `names` that is not empty limits the import to + /// the types in it. Returns the names of the imported types. fn import(&mut self, into: &str, from: &str, names: &[SmolStr]) -> HashSet { let Some(source) = self.scopes.get(from) else { return HashSet::new(); }; let mut imported = Scope::default(); - for (name, data) in &source.types { - if !data.public || data.home != from || !(names.is_empty() || names.contains(name)) { + for (name, info) in &source.types { + if !info.public || info.home != from || !(names.is_empty() || names.contains(name)) { continue; } - for ctor in &data.ctors { + let TypeDef::Data { ctors, .. } = &info.def else { + imported.types.insert(name.clone(), info.clone()); + continue; + }; + for ctor in ctors { // A later data type of `from` can have a constructor of // the same name: the constructor is then not of `name`. let info = source.constructors.get(&ctor.name); @@ -274,7 +289,7 @@ impl DataRegistry { .insert(ctor.name.clone(), info.clone()); } } - imported.types.insert(name.clone(), data.clone()); + imported.types.insert(name.clone(), info.clone()); } let types = imported.types.keys().cloned().collect(); let scope = self.scopes.entry(into.into()).or_default(); @@ -283,30 +298,16 @@ impl DataRegistry { types } - /// Register an opaque extern type name (from - /// `extern "abi" { type Foo }`). - pub fn register_extern_type(&mut self, name: &SmolStr) { - self.extern_types.insert(name.clone()); - } - - /// Register a `type Foo = T` alias of the module `home` in surface - /// form. Lookups in `desugar_named_type` find the entry and - /// recursively desugar it. - pub fn register_type_alias(&mut self, home: &str, name: SmolStr, ty: SurfaceTy) { - let entries = self.type_aliases.entry(name).or_default(); - entries.retain(|(module, _)| module != home); - entries.push((home.into(), ty)); + /// Register the opaque type `name` of an extern block of the module + /// `home`. + pub fn register_extern_type(&mut self, home: &str, name: &SmolStr) { + self.register_type(home, name, TypeDef::Extern, true); } - /// The alias `name` as the module `scope` sees it, with the key of - /// the module that declares it: the alias of `scope`, or else the - /// alias that was registered last. - fn lookup_type_alias(&self, scope: &str, name: &str) -> Option<&(SmolStr, SurfaceTy)> { - let entries = self.type_aliases.get(name)?; - entries - .iter() - .find(|(module, _)| module == scope) - .or(entries.last()) + /// Register the alias `type name = ty` of the module `home`. `public` + /// is `pub type`: a module that imports `home` can name the alias. + pub fn register_type_alias(&mut self, home: &str, name: SmolStr, ty: SurfaceTy, public: bool) { + self.register_type(home, &name, TypeDef::Alias(ty), public); } /// Look up a constructor by its name in the module `scope`. @@ -314,15 +315,10 @@ impl DataRegistry { self.scopes.get(scope)?.constructors.get(name) } - /// Look up a data type by its name in the module `scope`. - fn get_type_ctors(&self, scope: &str, name: &str) -> Option<&DataInfo> { + /// Look up a type by its name in the module `scope`. + fn get_type(&self, scope: &str, name: &str) -> Option<&TypeInfo> { self.scopes.get(scope)?.types.get(name) } - - /// Is this name a registered extern (opaque) type? - fn is_extern_type(&self, name: &str) -> bool { - self.extern_types.contains(name) - } } // ========================================================================= @@ -402,12 +398,15 @@ impl Desugarer { /// The constructors of the data type of the constructor `info`. fn ctors_of(&self, info: &ConstructorInfo) -> Result, DesugarError> { - self.registry - .get_type_ctors(&info.home, &info.data_name) - .map(|data| data.ctors.clone()) - .ok_or_else(|| DesugarError::UnknownType { + match self.registry.get_type(&info.home, &info.data_name) { + Some(TypeInfo { + def: TypeDef::Data { ctors, .. }, + .. + }) => Ok(ctors.clone()), + _ => Err(DesugarError::UnknownType { name: info.data_name.to_string(), - }) + }), + } } /// Run `f` with the names of the module `home` in scope: the names @@ -433,14 +432,14 @@ impl Desugarer { .map(|i| last_segment(i.module.as_str())) .collect(); - // The public data types of each imported module, in the order of - // the imports: a later one shadows an earlier one, and a - // declaration of this module shadows both. + // The public types of each imported module, in the order of the + // imports: a later one shadows an earlier one, and a declaration + // of this module shadows both. let key = module_key(&module.name); // The imports of the core module: the type checker reads each // name in an import list as a function, so the list keeps only - // the names that are not data types. An import that names only - // data types imports no function. + // the names that are not types. An import that names only types + // imports no function. let mut imports = Vec::with_capacity(module.imports.len()); for import in &module.imports { let types = self @@ -465,13 +464,18 @@ impl Desugarer { SurfaceDecl::Extern { items, .. } => { for item in items { if let SurfaceExternItem::Type { name } = item { - self.registry.register_extern_type(name); + self.registry.register_extern_type(&key, name); } } } - SurfaceDecl::Type { name, ty, .. } => { + SurfaceDecl::Type { + name, + visibility, + ty, + } => { + let public = *visibility == SurfaceVisibility::Public; self.registry - .register_type_alias(&key, name.clone(), ty.clone()); + .register_type_alias(&key, name.clone(), ty.clone(), public); } _ => {} } @@ -955,39 +959,29 @@ impl Desugarer { return Ok(Ty::Base(BaseTy::I32)); } - if self.registry.is_extern_type(name.as_str()) { - return Ok(Ty::Var(name.clone())); - } - - // `type Foo = T` aliases — recursively desugar the stored surface - // form. Aliases are monomorphic here (parameterised aliases would - // carry their args via the body). - let alias = self + let info = self .registry - .lookup_type_alias(&self.scope.borrow(), name.as_str()) - .cloned(); - if let Some((home, aliased)) = alias { - if !args.is_empty() { - return Err(DesugarError::TypeArityMismatch { - name: name.to_string(), - expected: 0, - got: args.len(), - }); - } - return self.with_expansion(name, &home, |this| this.desugar_ty(&aliased)); - } - - let DataInfo { - params, - ctors, - home, - .. - } = self - .registry - .get_type_ctors(&self.scope.borrow(), name.as_str()) + .get_type(&self.scope.borrow(), name.as_str()) .ok_or_else(|| DesugarError::UnknownType { name: name.to_string(), })?; + let home = &info.home; + let (params, ctors) = match &info.def { + TypeDef::Extern => return Ok(Ty::Var(name.clone())), + // Aliases are monomorphic here (parameterised aliases would + // carry their args via the body). + TypeDef::Alias(aliased) => { + if !args.is_empty() { + return Err(DesugarError::TypeArityMismatch { + name: name.to_string(), + expected: 0, + got: args.len(), + }); + } + return self.with_expansion(name, home, |this| this.desugar_ty(aliased)); + } + TypeDef::Data { params, ctors } => (params, ctors), + }; if params.len() != args.len() { return Err(DesugarError::TypeArityMismatch { @@ -2536,6 +2530,7 @@ mod expansion_regressions { } else { named(&format!("A{}", i + 1)) }, + false, ); } let desugarer = Desugarer::with_registry(registry.clone()); @@ -2543,7 +2538,7 @@ mod expansion_regressions { desugarer.desugar_ty(&named("A0")).unwrap(), Ty::Base(BaseTy::I32) ); - registry.register_type_alias("", "A64".into(), named("A0")); + registry.register_type_alias("", "A64".into(), named("A0"), false); assert!(matches!( Desugarer::with_registry(registry).desugar_ty(&named("A0")), Err(DesugarError::RecursiveType { .. }) diff --git a/src/ephapax-driver/src/lib.rs b/src/ephapax-driver/src/lib.rs index 07cb674..14f9b1e 100644 --- a/src/ephapax-driver/src/lib.rs +++ b/src/ephapax-driver/src/lib.rs @@ -224,8 +224,8 @@ pub fn parse_source( )?; // One DataRegistry for all modules: it gives each module its own - // scope, with the `pub data` types of the modules that it imports. - // An `extern type` is visible in each module. + // scope, with the public types of the modules that it imports + // (`pub data`, `pub type`, and each extern type). let mut desugarer = Desugarer::with_registry(DataRegistry::new()); let mut modules = Vec::with_capacity(resolved.len()); for m in resolved { From 58632c325c7b1ec2e5650855ad24e7e8efdaeaec Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 10 Nov 2026 18:44:57 +0000 Subject: [PATCH 2/2] docs(claude-md): the commit signing rule says what is in the repository Owner ruling 2026-11-10. The rule said that each commit has a signature of the owner key. Each commit on main is a squash merge that GitHub signs with its own key. The owner key signs the commits that the owner makes on a local computer. A cloud session signs with its session key, and no private key of the owner goes into such a session. Co-Authored-By: Claude Fable 5.2 Claude-Session: https://claude.ai/code/session_0136P7ZmKrYLDC4WHi2yt11u --- CLAUDE.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CLAUDE.md b/CLAUDE.md index 534fe9c..3b6bb7e 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -70,7 +70,7 @@ Proof and design history is in `formal/PRESERVATION-DESIGN.adoc`; current status - Formal-proof work spans Coq, Idris2, and the applicable estate policy. Checker output is evidence only for the exact proposition and assumptions run; a green build does not establish general language soundness. - The legacy preservation closure plan is obsolete. `formal/PRESERVATION-DESIGN.adoc` is design/history, not a proof result; `formal/PRESERVATION-HANDOFF.adoc` is historical diagnosis only. - Modality and `linear_to_affine` artifacts are mechanised, but no unconditional L1/L2 preservation theorem is established. The modality-polymorphic L1 statement is refuted as stated; see `PROOF-NEEDS.adoc` and the EXPLAINME ledger. -- All commits GPG-signed (key `4A03639C1EB1F86C7F0C97A91835A14A2867091E`), email `6759885+hyperpolymath@users.noreply.github.com`. Auto-merge ON for every PR. +- Commit signing (owner ruling 2026-11-10). Each commit on `main` is a squash merge made on github.com: GitHub signs it with its own key, and it shows as Verified. The owner key `4A03639C1EB1F86C7F0C97A91835A14A2867091E` (email `6759885+hyperpolymath@users.noreply.github.com`) signs the commits that the owner makes on a local computer. A cloud agent session signs its branch commits with its own session key; never put a private key of the owner into such a session. Auto-merge ON for every PR. ---