Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions dag/gunbc/plans/dag_v2_defork_audit.dag
Original file line number Diff line number Diff line change
Expand Up @@ -108,10 +108,10 @@ fn dag_v2_defork_audit_body() -> List<MarkdownBlock> {
li(text: "**Root B — generic-inference keystone + de-fork (THIS lane).** Phased, in order:"),
]),
ol(items: [
li(text: "**Keystone first:** fix v2 generic-alias instantiation so `type X = FreeMonoid<Symbol>` resolves (today it fails *\"variant not found in type FreeMonoid\"* at the definition site — `src/v2/std/qualified_name.dag`, `catalog.dag` `fold_list`, `ParseTable`). This is load-bearing resolver/infer work (`03_resolve`/`04_infer`) — model-before-implement, escalate before touching under any pre-dating brief."),
li(text: "**Keystone (partially landed via #5552):** simple generic-alias instantiation resolves — `type X = FreeMonoid<Symbol>` defines and construct/match/use-site works (proven by `generic_alias_coproduct_instantiation_test.dag`); `qualified_name.dag` is fully dissolved (incl. the v1 seed host-builtins made generic — `free_monoid_symbol_*`). **Still open:** raw variant-matching a value bound from a recursive `Cons.tail` field still fails *\"variant not found in type FreeMonoid\"* (`04_infer` fixpoint gap) — consumers avoid it via the `list_head`/algebra idiom; `catalog.dag` `fold_list`/`ParseTable` still await it. This residue is load-bearing resolver/infer work (`03_resolve`/`04_infer`) — model-before-implement, escalate before touching under any pre-dating brief."),
li(text: "**Definition unification:** make the coproduct the single authority in `std/algebra.dag`, delete the dag record-of-methods *definition* (re-express its surface as inhabitance), introduce the aliases. Only after the keystone lands (so the aliases compile). jolly-cat's Root A emit-seam should already be in by here — coordinate the `algebra.dag` touch."),
li(text: "**Repoints** (mechanical once 1–2 land): `nat`/`integer`/`float` (numeric tower `Int = GroupCompletion<Nat>`), `logic`, `effects` (operation-axis ⊕ idempotency-axis grounding), `verification` (entangled with #5428 + `Value::Null` — may stay last). Per the #5511 per-concept census above."),
li(text: "**Dissolve the 🟡 markers:** `qualified_name.dag` (`QnEmpty/QnCons` → `Empty/Cons`, `qualified_name_eq/for_all/singleton` → FreeMonoid ops), `catalog.dag` `fold_list`. The self_gen8 3 ignores fold into the def-unification PR — their premise flips from \"stays_unemitted\" to \"expects grounded `List<T>=Vec<T>` emission\" (`node://adhoc-9d2bb9c3-e7b`)."),
li(text: "**Dissolve the 🟡 markers:** `qualified_name.dag` — **DONE** (`QnEmpty/QnCons` → `Empty/Cons`, `qualified_name_eq/for_all/singleton` → FreeMonoid ops + structural `==`, v1 seed bridge made generic); `catalog.dag` `fold_list` still awaits the recursive-tail resolver residue. The self_gen8 3 ignores fold into the def-unification PR — their premise flips from \"stays_unemitted\" to \"expects grounded `List<T>=Vec<T>` emission\" (`node://adhoc-9d2bb9c3-e7b`)."),
]),
h3(text: "Fences (DESIGN §3/§6, and the #5516 respawn-mandate lesson)"),
ul(items: [
Expand Down
2 changes: 1 addition & 1 deletion docs/plans/dag-v2-defork-audit.md
Original file line number Diff line number Diff line change
Expand Up @@ -141,7 +141,7 @@ The operator ruled the FreeMonoid/algebra single authority that category (b) was
- **Root A — grounding (jolly-cat owns, build-now).** The `src/v1/05_emit_rust.dag` emit-seam (`rust_seed_host_container_base`/`rust_named_type_base`/`rust_corpus_repr`) generalized to String/FreeMonoid → host `Vec`. **Emit-layer only — does NOT change `std/algebra.dag` definitions**, so it runs concurrently with Root B without conflict. Kills ~48% of the 16,071 self-host cargo errors (String+List). The carrier-independent tail (import-dedup E0252, closure-Debug) rides here too.
- **Root B — generic-inference keystone + de-fork (THIS lane).** Phased, in order:

1. **Keystone first:** fix v2 generic-alias instantiation so `type X = FreeMonoid<Symbol>` resolves (today it fails *"variant not found in type FreeMonoid"* at the definition site — `src/v2/std/qualified_name.dag`, `catalog.dag` `fold_list`, `ParseTable`). This is load-bearing resolver/infer work (`03_resolve`/`04_infer`) — model-before-implement, escalate before touching under any pre-dating brief.
1. **Keystone (partially landed via #5552):** simple generic-alias instantiation now resolves — `type X = FreeMonoid<Symbol>` defines and construct/match/use-site works (proven by `generic_alias_coproduct_instantiation_test.dag`), and the `QualifiedName` hand-roll is dissolved (QnEmpty/QnCons → Empty/Cons, trio → FreeMonoid ops + `==`, incl. the v1 seed host-builtins made generic). **Still open:** raw variant-matching a value bound from a recursive `Cons.tail` field still fails *"variant not found in type FreeMonoid"* (`04_infer` fixpoint gap) — consumers avoid it via the `list_head`/algebra idiom; `catalog.dag` `fold_list`/`ParseTable` still await it. This residue is load-bearing resolver/infer work (`03_resolve`/`04_infer`) — model-before-implement, escalate before touching under any pre-dating brief.
2. **Definition unification:** make the coproduct the single authority in `std/algebra.dag`, delete the dag record-of-methods *definition* (re-express its surface as inhabitance), introduce the aliases. Only after the keystone lands (so the aliases compile). jolly-cat's Root A emit-seam should already be in by here — coordinate the `algebra.dag` touch.
3. **Repoints** (mechanical once 1–2 land): `nat`/`integer`/`float` (numeric tower `Int = GroupCompletion<Nat>`), `logic`, `effects` (operation-axis ⊕ idempotency-axis grounding), `verification` (entangled with #5428 + `Value::Null` — may stay last). Per the #5511 per-concept census above.
4. **Dissolve the 🟡 markers:** `qualified_name.dag` (`QnEmpty/QnCons` → `Empty/Cons`, `qualified_name_eq/for_all/singleton` → FreeMonoid ops), `catalog.dag` `fold_list`. The self_gen8 3 ignores fold into the def-unification PR — their premise flips from "stays_unemitted" to "expects grounded `List<T>=Vec<T>` emission" (`node://adhoc-9d2bb9c3-e7b`).
Expand Down
2 changes: 1 addition & 1 deletion docs/plans/fold-ergonomics.md
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,7 @@ The fold is not aspirational here — it is the actual architecture, at scale:
**Root B — generic inference is weak, so the fold is awkward to reach (the friction).** Two concrete failures:

- generic fn-param results mis-infer as kernel `Witness`/`Optional` → must route through a typed param (the `resolve_probe` workaround in `staging.dag`; same in `target_model.dag`);
- generic type-alias instantiation fails — `type QualifiedName = FreeMonoid<Symbol>` won't define ("variant not found in type `FreeMonoid`") → **55 lines of hand-rolled `qualified_name_eq`/`for_all`** (`qualified_name.dag:25–57`), and it is the *same* root that makes v2 still hand-roll `ParseTable`.
- generic type-alias instantiation — **partially fixed by #5552**: `type QualifiedName = FreeMonoid<Symbol>` now defines, and simple construct/match/use-site instantiation resolves (proven by `generic_alias_coproduct_instantiation_test.dag`); the hand-rolled `qualified_name_eq`/`for_all`/`singleton` were dissolved into `FreeMonoid` ops + structural `==` (QualifiedName seed de-fork). **Remaining resolver gap:** raw variant-matching a value *bound from a `Cons.tail` field* (or a nested `tail: Empty` pattern) on a recursive `FreeMonoid` still corrupts resolution ("variant not found in type `FreeMonoid`") — thread tails through the algebra (`list_head`/`list_tail`/`fold`) instead, the idiom all `FreeMonoid` consumers already use. It is the *same* root that makes v2 still hand-roll `ParseTable`.

Root A is the fail-open class the lane retires; Root B is the friction that keeps producing it.

Expand Down
46 changes: 23 additions & 23 deletions src/v1/stage0/src/cli_run.rs
Original file line number Diff line number Diff line change
Expand Up @@ -375,28 +375,28 @@ pub fn source_path_for_module_path(module_path: String) -> String {
.unwrap_or_else(|| panic!("module_path_index: unknown module path '{module_path}'"))
}

pub fn qualified_name_value_to_module_path(value: &v1_interpreter::Value) -> String {
v1_interpreter::qualified_name_value_to_module_path(value)
pub fn free_monoid_symbol_value_to_dotted_string(value: &v1_interpreter::Value) -> String {
v1_interpreter::free_monoid_symbol_value_to_dotted_string(value)
}

pub fn qualified_name_value_from_dotted_string(
pub fn free_monoid_symbol_value_from_dotted_string(
ctx: &v1_interpreter::InterpContext,
dotted: &str,
) -> v1_interpreter::Value {
use v1_interpreter::{sorted_fields, Value};

let qn_variant = |variant: &str, fields: Vec<_>| Value::Variant {
type_name: ctx.sym("QualifiedName"),
let fm_variant = |variant: &str, fields: Vec<_>| Value::Variant {
type_name: ctx.sym("FreeMonoid"),
variant_name: ctx.sym(variant),
fields: Rc::new(fields),
};
if dotted.is_empty() {
return qn_variant("QnEmpty", vec![]);
return fm_variant("Empty", vec![]);
}
let mut qn = qn_variant("QnEmpty", vec![]);
let mut qn = fm_variant("Empty", vec![]);
for seg in dotted.split('.').rev() {
qn = qn_variant(
"QnCons",
qn = fm_variant(
"Cons",
sorted_fields(vec![
(ctx.sym("head"), Value::Str(seg.to_string())),
(ctx.sym("tail"), qn),
Expand Down Expand Up @@ -5985,34 +5985,34 @@ pub fn parse_source_root_entry_admission(source: &str) -> Result<SourceRootEntry
.ok_or_else(|| "entry source missing `module` declaration".to_string())
}

fn emit_qualified_name_dag(segments: &[String]) -> String {
fn free_monoid_symbol_emit_dag(segments: &[String]) -> String {
if segments.is_empty() {
return "QnEmpty".to_string();
return "Empty".to_string();
}
let mut out = String::from("QnEmpty");
let mut out = String::from("Empty");
for seg in segments.iter().rev() {
out = format!("QnCons {{ head: ^{seg}, tail: {out} }}");
out = format!("Cons {{ head: ^{seg}, tail: {out} }}");
}
out
}

#[cfg(test)]
mod manifest_emit_tests {
use super::{
dag_embedded_dag_source_escape, dag_manifest_scalar_escape, emit_qualified_name_dag,
dag_embedded_dag_source_escape, dag_manifest_scalar_escape, free_monoid_symbol_emit_dag,
};

#[test]
fn emit_qualified_name_dag_three_segment_path() {
fn free_monoid_symbol_emit_dag_three_segment_path() {
assert_eq!(
emit_qualified_name_dag(&["v2".into(), "compiler".into(), "compile".into()]),
"QnCons { head: ^v2, tail: QnCons { head: ^compiler, tail: QnCons { head: ^compile, tail: QnEmpty } } }"
free_monoid_symbol_emit_dag(&["v2".into(), "compiler".into(), "compile".into()]),
"Cons { head: ^v2, tail: Cons { head: ^compiler, tail: Cons { head: ^compile, tail: Empty } } }"
);
}

#[test]
fn emit_qualified_name_dag_empty_is_qn_empty() {
assert_eq!(emit_qualified_name_dag(&[]), "QnEmpty");
fn free_monoid_symbol_emit_dag_empty_is_empty_variant() {
assert_eq!(free_monoid_symbol_emit_dag(&[]), "Empty");
}

#[test]
Expand Down Expand Up @@ -6092,7 +6092,7 @@ fn emit_import_admission_list(imports: &[Vec<String>]) -> String {
for import in imports.iter().rev() {
out = format!(
"Cons {{\n head: Import {{\n target: {},\n visibility: ImportVisible\n }},\n tail: {out}\n}}",
emit_qualified_name_dag(import)
free_monoid_symbol_emit_dag(import)
);
}
out
Expand All @@ -6101,7 +6101,7 @@ fn emit_import_admission_list(imports: &[Vec<String>]) -> String {
fn emit_source_root_entry_admission_data(admission: &SourceRootEntryAdmission) -> String {
format!(
"data host_compiler_closure_admission: Admission = Admission {{\n subject: ResolutionSubject {{\n name: {}\n }},\n imports: {}\n}}\n\n\n",
emit_qualified_name_dag(&admission.subject),
free_monoid_symbol_emit_dag(&admission.subject),
emit_import_admission_list(&admission.imports)
)
}
Expand Down Expand Up @@ -6290,7 +6290,7 @@ pub fn emit_source_root_ingest_manifest(
out.push_str(" ImportVisible,\n");
out.push_str(" ResolutionSubject\n");
out.push_str("}\n");
out.push_str("import v2.std.qualified_name { QnCons, QnEmpty }\n");
out.push_str("import v2.std.algebra { Cons, Empty }\n");
}
out.push('\n');
out.push_str(&format!(
Expand Down Expand Up @@ -9050,7 +9050,7 @@ pub fn shell_argv_nodes_for_operation(
}

pub fn qualified_name_resolves_in_derived_module_set(qn: &crate::v1_interpreter::Value) -> bool {
let module_path = qualified_name_value_to_module_path(qn);
let module_path = free_monoid_symbol_value_to_dotted_string(qn);
!module_path.is_empty()
&& build_module_path_index_from_witness_roots().contains_key(&module_path)
}
Expand Down
2 changes: 1 addition & 1 deletion src/v1/stage0/src/coproduct_reflection.rs
Original file line number Diff line number Diff line change
Expand Up @@ -355,7 +355,7 @@ pub fn eval_qualified_name_from_dotted_string(
args.first().map(|(_, v)| v),
"qualified_name_from_dotted_string",
)?;
Ok(crate::cli_run::qualified_name_value_from_dotted_string(
Ok(crate::cli_run::free_monoid_symbol_value_from_dotted_string(
ctx, &dotted,
))
}
Expand Down
16 changes: 8 additions & 8 deletions src/v1/stage0/src/external_authority_project.rs
Original file line number Diff line number Diff line change
Expand Up @@ -126,14 +126,14 @@ pub fn external_authority_scheme_identity_for_module_path(module_path: String) -
pub fn external_authority_anchor_kind_for_qualified_name(
qn: &crate::v1_interpreter::Value,
) -> String {
let module_path = crate::cli_run::qualified_name_value_to_module_path(qn);
let module_path = crate::cli_run::free_monoid_symbol_value_to_dotted_string(qn);
external_authority_anchor_kind_for_module_path(module_path)
}

pub fn external_authority_scheme_identity_for_qualified_name(
qn: &crate::v1_interpreter::Value,
) -> String {
let module_path = crate::cli_run::qualified_name_value_to_module_path(qn);
let module_path = crate::cli_run::free_monoid_symbol_value_to_dotted_string(qn);
external_authority_scheme_identity_for_module_path(module_path)
}

Expand All @@ -145,7 +145,7 @@ pub fn external_authority_locator_for_module_path(module_path: String) -> String
}

pub fn external_authority_locator_for_qualified_name(qn: &crate::v1_interpreter::Value) -> String {
let module_path = crate::cli_run::qualified_name_value_to_module_path(qn);
let module_path = crate::cli_run::free_monoid_symbol_value_to_dotted_string(qn);
external_authority_locator_for_module_path(module_path)
}

Expand All @@ -164,7 +164,7 @@ pub fn qualified_name_value_from_module_path(
ctx: &crate::v1_interpreter::InterpContext,
module_path: &str,
) -> crate::v1_interpreter::Value {
crate::cli_run::qualified_name_value_from_dotted_string(ctx, module_path)
crate::cli_run::free_monoid_symbol_value_from_dotted_string(ctx, module_path)
}

pub fn derived_extdeps_modules_value(
Expand Down Expand Up @@ -214,7 +214,7 @@ pub fn is_backfill_pending_for_module_path(module_path: &str) -> bool {
}

pub fn is_backfill_pending_for_qualified_name(qn: &crate::v1_interpreter::Value) -> bool {
let module_path = crate::cli_run::qualified_name_value_to_module_path(qn);
let module_path = crate::cli_run::free_monoid_symbol_value_to_dotted_string(qn);
is_backfill_pending_for_module_path(&module_path)
}

Expand All @@ -236,7 +236,7 @@ pub fn is_machinery_exempt_for_module_path(module_path: &str) -> bool {
}

pub fn is_machinery_exempt_for_qualified_name(qn: &crate::v1_interpreter::Value) -> bool {
let module_path = crate::cli_run::qualified_name_value_to_module_path(qn);
let module_path = crate::cli_run::free_monoid_symbol_value_to_dotted_string(qn);
is_machinery_exempt_for_module_path(&module_path)
}

Expand All @@ -251,7 +251,7 @@ pub fn is_clean_tree_roster_excluded_for_module_path(module_path: &str) -> bool
}

pub fn is_clean_tree_roster_excluded_for_qualified_name(qn: &crate::v1_interpreter::Value) -> bool {
let module_path = crate::cli_run::qualified_name_value_to_module_path(qn);
let module_path = crate::cli_run::free_monoid_symbol_value_to_dotted_string(qn);
is_clean_tree_roster_excluded_for_module_path(&module_path)
}

Expand Down Expand Up @@ -350,7 +350,7 @@ pub fn external_authority_anchor_shadow_masked_for_module_path(module_path: Stri
pub fn external_authority_anchor_shadow_masked_for_qualified_name(
qn: &crate::v1_interpreter::Value,
) -> bool {
let module_path = crate::cli_run::qualified_name_value_to_module_path(qn);
let module_path = crate::cli_run::free_monoid_symbol_value_to_dotted_string(qn);
external_authority_anchor_shadow_masked_for_module_path(module_path)
}

Expand Down
20 changes: 9 additions & 11 deletions src/v1/stage0/src/v1_interpreter.rs
Original file line number Diff line number Diff line change
Expand Up @@ -129,18 +129,18 @@ fn resolve_sym(sym: Symbol) -> String {
.unwrap_or_else(|| format!("#{}", sym.0))
}

pub fn qualified_name_value_to_module_path(value: &Value) -> String {
pub fn free_monoid_symbol_value_to_dotted_string(value: &Value) -> String {
match value {
Value::Variant {
variant_name,
fields,
..
} => {
let variant = resolve_sym(*variant_name);
if variant == "QnEmpty" {
if variant == "Empty" {
return String::new();
}
if variant == "QnCons" {
if variant == "Cons" {
let head = fields
.iter()
.find(|(k, _)| resolve_sym(*k) == "head")
Expand All @@ -166,26 +166,24 @@ pub fn qualified_name_value_to_module_path(value: &Value) -> String {
}
_ => None,
})
.unwrap_or_else(|| {
panic!("qualified_name_to_module_path: QnCons.head not Str")
});
.unwrap_or_else(|| panic!("free_monoid_symbol_to_dotted: Cons.head not Str"));
let tail = fields
.iter()
.find(|(k, _)| resolve_sym(*k) == "tail")
.map(|(_, v)| v)
.expect("qualified_name_to_module_path: QnCons.tail missing");
let rest = qualified_name_value_to_module_path(tail);
.expect("free_monoid_symbol_to_dotted: Cons.tail missing");
let rest = free_monoid_symbol_value_to_dotted_string(tail);
if rest.is_empty() {
head
} else {
format!("{head}.{rest}")
}
} else {
panic!("qualified_name_to_module_path: unexpected variant '{variant}'");
panic!("free_monoid_symbol_to_dotted: unexpected variant '{variant}'");
}
}
other => {
panic!("qualified_name_to_module_path: expected QualifiedName variant, got {other:?}")
panic!("free_monoid_symbol_to_dotted: expected FreeMonoid variant, got {other:?}")
}
}
}
Expand Down Expand Up @@ -5668,7 +5666,7 @@ fn eval_builtin(
msg: "extdeps_shape_transport_policy_facts_for_qualified_name requires a QualifiedName"
.to_string(),
})?;
let module_path = crate::cli_run::qualified_name_value_to_module_path(qn);
let module_path = crate::cli_run::free_monoid_symbol_value_to_dotted_string(qn);
let facts = crate::cli_run::extdeps_shape_transport_policy_module_facts(&module_path);
let argv_items: Vec<Value> = facts
.argv_facts
Expand Down
2 changes: 1 addition & 1 deletion src/v1/tests/src/source_root_ingest_manifest_host_test.rs
Original file line number Diff line number Diff line change
Expand Up @@ -47,7 +47,7 @@ fn manifest_entry_admission_qualified_name_is_well_formed() {
let manifest = fs::read_to_string(&manifest_path).expect("read manifest");
assert!(
manifest.contains(
"QnCons { head: ^v2, tail: QnCons { head: ^compiler, tail: QnCons { head: ^compile, tail: QnEmpty } } }"
"Cons { head: ^v2, tail: Cons { head: ^compiler, tail: Cons { head: ^compile, tail: Empty } } }"
),
"manifest admission subject QN malformed:\n{manifest}"
);
Expand Down
Loading
Loading