emit: cross-module use emission (E0425 imports)

src/v1/05_emit_rust.dag

@@ -2404,7 +2404,12 @@ fn is_emittable_parametric_type_alias_item(item: Node, item_text: String, source
 
 fn emit_specific_import_block(import_module: String, mod_name: String, filtered_names: List<String>, emit_info: EmitGraphInfo, registry: Map<String, ItemInfo>, local_names: List<String>, export_sets: Map<String, Map<String, Bool>>, typed_modules: List<TypedModule>, source_indices: Map<String, NewlineIndex>, module_index: ModuleIndex) -> String {
   let type_summaries = emit_info.type_summaries
-  let deduped_names = unique_strings(items: filtered_names |> filter(n => local_names |> all(ln => ln != n)))
+  // Container kinds (List/Set/Map/Witness) have source `type List = FreeMonoid`
+  // decls (so the registry reports them as importable), but the emitter renders
+  // them INLINE as their host carrier (Vec/...) and never emits a Rust `type`
+  // for them. A `use crate::std_types::List` is therefore unresolved (E0432).
+  // Drop them from the use-set; container references render structurally.
+  let deduped_names = unique_strings(items: filtered_names |> filter(n => local_names |> all(ln => ln != n)) |> filter(n => is_container_type(name: n) == false))
   if deduped_names |> count == 0 {
     ""
   } else {
@@ -7574,6 +7579,38 @@ fn data_value_has_cross_refs(value: Node) -> Bool {
   }
 }
 
+// A `data` decl whose annotation is a closed alias renders from the RESOLVED
+// inferred type (the brand/alias peel target), not the authored annotation —
+// e.g. `data min_cargo_version: CargoToolVersionFloor` renders return type
+// `SemVerConstraint` (CargoToolVersionFloor = SemVerConstraint, defined in
+// extdeps.version.semver). render_rust_type_with_applied_binding emits the bare
+// peel-target name, but the importing module's use-set only carries the authored
+// import (CargoToolVersionFloor), so the bare reference is unresolved (E0425).
+// Qualify a cross-module simple nominal to crate::<def_mod>::<name>, mirroring
+// render_rust_alias_rhs_type's cross-module qualification. Conservative: only the
+// bare-name case (rendered string == authored name, no generics/Rc wrap) and only
+// non-kernel/non-container names whose defining module differs from the local one.
+fn rust_data_def_qualify_cross_module(raw_ty_str: String, render_type_node: Node, module_name: String, registry: Map<String, ItemInfo>, source_indices: Map<String, NewlineIndex>) -> String {
+  let resolved_name = authored_name_at(source_indices: source_indices, node: render_type_node)
+  if render_type_node.connective == NoConnective
+    && (render_type_node.children |> count) == 0
+    && (render_type_node.params |> count) == 0
+    && resolved_name != ""
+    && raw_ty_str == resolved_name
+    && is_kernel_type(name: resolved_name) == false
+    && is_container_type(name: resolved_name) == false {
+    let local_mod = module_to_filename(name: module_name)
+    let def_mod = item_defining_module_filename(name: resolved_name, registry: registry, fallback: local_mod)
+    if def_mod != local_mod {
+      concat("crate::", def_mod, "::", resolved_name)
+    } else {
+      raw_ty_str
+    }
+  } else {
+    raw_ty_str
+  }
+}
+
 fn emit_data_def(name: String, type_node: Node, value: Node, registry: Map<String, ItemInfo>, scope: InferScope, depth: Int, shared_types: Set<String>, emit_info: EmitGraphInfo) -> String {
   let annotation_type_node = type_node
   let render_type_node = if annotation_type_node.children |> count > 0 {
@@ -7594,7 +7631,9 @@ fn emit_data_def(name: String, type_node: Node, value: Node, registry: Map<Strin
         else { concat("BoundedLattice<", top_type_name, ">") }
       Absent => raw_ty_str
     }
-  } else { raw_ty_str }
+  } else {
+    rust_data_def_qualify_cross_module(raw_ty_str: raw_ty_str, render_type_node: render_type_node, module_name: scope.module_name, registry: registry, source_indices: scope.type_env.source_indices)
+  }
   let fn_name = to_snake(name: name)
   let needs_rc = set_contains(shared_types, authored_name_at(source_indices: scope.type_env.source_indices, node: type_node))
   // shared-type data accessors return Rc<T> when body stores Rc::new(...) (e.g. TestClaim via call).

src/v1/stage0/src/compiler_tests.rs

@@ -50,11 +50,7 @@ mod compiler_tests {
                         .unwrap()
                         .to_string_lossy()
                         .to_string();
-                    // Test fixtures (e.g. fact_cardinality_split_brace.dag) are not modules;
-                    // exclude them so the self_* whole-tree module scans don't try to parse
-                    // them as modules and panic. The only .dag under src/v1/**/tests/ is the
-                    // fixture, so this skips exactly it (#5124 added the fixture; the cargo-test
-                    // CI gate surfaced the panic). No real module lives under a tests/ dir.
+                    // Test fixtures (e.g. fact_cardinality_split_brace.dag) are not modules.
                     if rel.contains("/tests/") {
                         continue;
                     }

src/v1/stage0/src/extdeps_cargo.rs

@@ -3,7 +3,12 @@
 
 use self::CargoDepSource::*;
 use self::CargoTarget::*;
+use self::RustEdition::*;
 use self::TestHarness::*;
+pub use crate::extdeps_cargo_version::{
+    CargoPackageVersion, CargoToolVersionFloor, CargoVersionRequirement,
+};
+pub use crate::std_types::FilePathParts;
 use crate::v1_rt;
 use crate::v1_rt::Witness;
 use crate::v1_rt::Witness::{Holds, Violates};
@@ -13,19 +18,58 @@ use std::collections::BTreeSet;
 use std::collections::HashMap;
 use std::rc::Rc;
 
+#[derive(
+    Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, serde::Serialize, serde::Deserialize,
+)]
+#[serde(tag = "_variant")]
+pub enum RustEdition {
+    Edition2015,
+    Edition2018,
+    Edition2021,
+    Edition2024,
+}
+
+pub fn rust_edition_str(edition: RustEdition) -> String {
+    match edition {
+        RustEdition::Edition2015 => "2015".to_string(),
+        RustEdition::Edition2018 => "2018".to_string(),
+        RustEdition::Edition2021 => "2021".to_string(),
+        RustEdition::Edition2024 => "2024".to_string(),
+    }
+}
+
+pub fn default_rust_edition() -> RustEdition {
+    thread_local! {
+        static CACHED: RustEdition = {
+            RustEdition::Edition2021
+        };
+    }
+    CACHED.with(|c: &RustEdition| c.clone())
+}
+
+pub fn min_cargo_version() -> SemVerConstraint {
+    thread_local! {
+        static CACHED: SemVerConstraint = {
+            serde_json::from_value(serde_json::json!(">= 1.56"))
+                .expect("valid data definition")
+        };
+    }
+    CACHED.with(|c: &SemVerConstraint| c.clone())
+}
+
 #[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)]
 pub struct CargoPackage {
     pub name: String,
-    pub version: String,
-    pub edition: String,
+    pub version: Box<CargoPackageVersion>,
+    pub edition: RustEdition,
     pub path: String,
 }
 
 #[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)]
 #[serde(tag = "_variant")]
 pub enum CargoDepSource {
     RegistryDep {
-        version: String,
+        version: Box<CargoVersionRequirement>,
         features: Rc<Vec<String>>,
     },
     LocalPathDep {
@@ -60,6 +104,64 @@ impl CargoTarget {
     }
 }
 
+pub fn cargo_target_source_path(
+    target: Rc<CargoTarget>,
+    package_name: String,
+) -> Rc<FilePathParts> {
+    match (*target).clone() {
+        CargoTarget::Lib => Rc::new(FilePathParts {
+            segments: Rc::new(vec!["src".to_string(), "lib.rs".to_string()]),
+        }),
+        CargoTarget::Bin { name: name, .. } => {
+            if (name.clone() == package_name) {
+                Rc::new(FilePathParts {
+                    segments: Rc::new(vec!["src".to_string(), "main.rs".to_string()]),
+                })
+            } else {
+                Rc::new(FilePathParts {
+                    segments: Rc::new(vec![
+                        "src".to_string(),
+                        "bin".to_string(),
+                        v1_rt::concat(name.clone(), ".rs".to_string()),
+                    ]),
+                })
+            }
+        }
+        CargoTarget::CargoTest { name: name, .. } => Rc::new(FilePathParts {
+            segments: Rc::new(vec![
+                "tests".to_string(),
+                v1_rt::concat(name.clone(), ".rs".to_string()),
+            ]),
+        }),
+        CargoTarget::Example { name: name, .. } => Rc::new(FilePathParts {
+            segments: Rc::new(vec![
+                "examples".to_string(),
+                v1_rt::concat(name.clone(), ".rs".to_string()),
+            ]),
+        }),
+        CargoTarget::Bench { name: name, .. } => Rc::new(FilePathParts {
+            segments: Rc::new(vec![
+                "benches".to_string(),
+                v1_rt::concat(name.clone(), ".rs".to_string()),
+            ]),
+        }),
+    }
+}
+
+pub fn rust_module_candidate_paths(stem: String) -> Rc<Vec<Rc<FilePathParts>>> {
+    Rc::new(vec![
+        Rc::new(FilePathParts {
+            segments: Rc::new(vec![
+                "src".to_string(),
+                v1_rt::concat(stem.clone(), ".rs".to_string()),
+            ]),
+        }),
+        Rc::new(FilePathParts {
+            segments: Rc::new(vec!["src".to_string(), stem.clone(), "mod.rs".to_string()]),
+        }),
+    ])
+}
+
 pub type CargoProfile = String;
 
 pub fn canonical_profiles() -> Rc<Vec<String>> {
@@ -86,15 +188,6 @@ pub enum TestHarness {
     NoHarness,
 }
 
-pub fn default_edition() -> String {
-    thread_local! {
-        static CACHED: String = {
-            "2021".to_string()
-        };
-    }
-    CACHED.with(|c: &String| c.clone())
-}
-
 pub fn default_profile() -> String {
     thread_local! {
         static CACHED: String = {
@@ -103,3 +196,10 @@ pub fn default_profile() -> String {
     }
     CACHED.with(|c: &String| c.clone())
 }
+
+pub struct Edition2015;
+pub struct Edition2018;
+pub struct Edition2021;
+pub struct Edition2024;
+pub struct Harness;
+pub struct NoHarness;

src/v1/stage0/src/extdeps_cargo_version.rs

@@ -17,27 +17,27 @@ pub type CargoVersionRequirement = SemVerConstraint;
 
 pub type CargoToolVersionFloor = SemVerConstraint;
 
-pub fn default_stage0_package_version() -> Rc<FreeMonoid<Nat>> {
+pub fn default_stage0_package_version() -> String {
     thread_local! {
-        static CACHED: Rc<FreeMonoid<Nat>> = {
+        static CACHED: String = {
             "0.1.0".to_string()
         };
     }
-    CACHED.with(|c: &Rc<FreeMonoid<Nat>>| c.clone())
+    CACHED.with(|c: &String| c.clone())
 }
 
-pub fn render_cargo_package_version_field(version: CargoPackageVersion) -> Rc<FreeMonoid<Nat>> {
+pub fn render_cargo_package_version_field(version: CargoPackageVersion) -> String {
     v1_rt::concat(
         v1_rt::concat("version = \"".to_string(), version),
         "\"".to_string(),
     )
 }
 
-pub fn render_cargo_version_requirement_toml(req: CargoVersionRequirement) -> Rc<FreeMonoid<Nat>> {
+pub fn render_cargo_version_requirement_toml(req: CargoVersionRequirement) -> String {
     v1_rt::concat(v1_rt::concat("\"".to_string(), req), "\"".to_string())
 }
 
-pub fn render_cargo_package_header_prefix(name: Rc<FreeMonoid<Nat>>) -> Rc<FreeMonoid<Nat>> {
+pub fn render_cargo_package_header_prefix(name: String) -> String {
     v1_rt::concat(
         v1_rt::concat(
             v1_rt::concat("[package]\nname = \"".to_string(), name),

src/v1/stage0/src/extdeps_languages_dag_emit.rs

@@ -14,13 +14,13 @@ pub fn dag_keywords() -> Rc<HashMap<String, String>> {
     thread_local! {
         static CACHED: Rc<HashMap<String, String>> = {
             let mut __m = HashMap::new();
-            __m.insert("true".to_string(), "true".to_string());
-            __m.insert("false".to_string(), "false".to_string());
-            __m.insert("null".to_string(), "none".to_string());
-            __m.insert("and".to_string(), "&&".to_string());
-            __m.insert("or".to_string(), "||".to_string());
-            __m.insert("not".to_string(), "!".to_string());
-            __m.insert("div".to_string(), "/".to_string());
+            __m.insert("true", "true".to_string());
+            __m.insert("false", "false".to_string());
+            __m.insert("null", "none".to_string());
+            __m.insert("and", "&&".to_string());
+            __m.insert("or", "||".to_string());
+            __m.insert("not", "!".to_string());
+            __m.insert("div", "/".to_string());
             Rc::new(__m)
         };
     }
@@ -31,15 +31,15 @@ pub fn dag_container_templates() -> Rc<HashMap<String, String>> {
     thread_local! {
         static CACHED: Rc<HashMap<String, String>> = {
             let mut __m = HashMap::new();
-            __m.insert("list".to_string(), "List<{0}>".to_string());
-            __m.insert("set".to_string(), "Set<{0}>".to_string());
-            __m.insert("non_empty_list".to_string(), "NonEmptyList<{0}>".to_string());
-            __m.insert("non_empty_set".to_string(), "NonEmptySet<{0}>".to_string());
-            __m.insert("optional".to_string(), "{0}?".to_string());
-            __m.insert("map".to_string(), "Map<{0}, {1}>".to_string());
-            __m.insert("free_monoid".to_string(), "List<{0}>".to_string());
-            __m.insert("partial_function".to_string(), "Map<{0}, {1}>".to_string());
-            __m.insert("boolean_algebra".to_string(), "Bool".to_string());
+            __m.insert("list", "List<{0}>".to_string());
+            __m.insert("set", "Set<{0}>".to_string());
+            __m.insert("non_empty_list", "NonEmptyList<{0}>".to_string());
+            __m.insert("non_empty_set", "NonEmptySet<{0}>".to_string());
+            __m.insert("optional", "{0}?".to_string());
+            __m.insert("map", "Map<{0}, {1}>".to_string());
+            __m.insert("free_monoid", "List<{0}>".to_string());
+            __m.insert("partial_function", "Map<{0}, {1}>".to_string());
+            __m.insert("boolean_algebra", "Bool".to_string());
             Rc::new(__m)
         };
     }