Skip to content
Closed
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
25 changes: 25 additions & 0 deletions src/v2/lens/common/record_field_carrier.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,25 @@
module v2.lens.common.record_field_carrier

import std.optional { Absent, Present }
import v2.std.node { Node }
import v2.extdeps.languages.dag {
namespace_graft_spine_chain_reaches_module_body,
parse_production_emitted_identity_optional
}

// THE CARRIER PREDICATE THE UNIT-MODELING AND LIFECYCLE-CARRIER LENSES SHARE. Both fold every
// TypeNode's Authored children through member_edge_type_node and refuse a child that is not a
// binder. A module shell, a marked module body, and a namespace-graft spine are TypeNode Conj
// containers whose Authored members are modules and declarations, not record fields; judging them
// as payloads is the member_not_a_binder door refusal on valid modules (compile_door_cause_ownership
// member_not_a_binder row). Production identity Present covers the shell and the marked body;
// the spine is the remaining unmarked single-Named-Conj chain that ends at that body
// (namespace_graft_spine_chain_reaches_module_body — shape alone would misread an inline nested
// record, so the body mark is the discriminator).

fn node_is_module_surface_or_namespace_container(node: Node) -> Bool {
match parse_production_emitted_identity_optional(node: node) {
Present { value: _ } => true
Absent => namespace_graft_spine_chain_reaches_module_body(node: node)
}
}
18 changes: 18 additions & 0 deletions src/v2/lens/fact_density.dag
Original file line number Diff line number Diff line change
Expand Up @@ -52,9 +52,27 @@ fn connective_is_kernel_ambient_atom(c: Connective) -> Bool {
}
}

// Graft identity atoms stand for no type denotation (namespace_graft_fold_spine /
// namespace_graft_module_body_marker_node). Treating them as hollow aliases unmasks
// fact_density_hollow_alias_locus on every valid module once the sibling lenses stop
// refusing the parent shell as member_not_a_binder.
fn connective_is_surface_identity_atom(c: Connective) -> Bool {
match c {
Atom { identity: id } =>
(id == ^dag_surface_module) || (id == ^namespace_graft_module_body)
Conj => false
Disj => false
Arrow => false
Cardinality => false
Instantiation => false
}
}

fn connective_spec_fact(c: Connective, named_facts: Nat) -> SourceSpecReadFact {
if connective_is_kernel_ambient_atom(c: c) {
KernelAmbientAtom
} else if connective_is_surface_identity_atom(c: c) {
NotATypeCarrier
} else {
density_fact(named_facts: named_facts)
}
Expand Down
17 changes: 11 additions & 6 deletions src/v2/lens/lifecycle_carrier.dag
Original file line number Diff line number Diff line change
Expand Up @@ -24,6 +24,7 @@ import v2.std.node {
symbol_lexeme,
StructuralLabel,
}
import v2.lens.common.record_field_carrier { node_is_module_surface_or_namespace_container }
import v2.std.node_query { edge_field_type_name, member_edge_type_node, member_not_a_binder_diagnostic }
import std.optional {
Absent,
Expand Down Expand Up @@ -130,12 +131,16 @@ fn field_lifecycle_violation(carrier: Node, edge: Edge) -> Optional<Diagnostic>
}

fn carrier_first_lifecycle_violation(carrier: Node) -> Optional<Diagnostic> {
match carrier.kind {
TypeNode { connective: _ } =>
fold(carrier.children, init: optional_absent(), f: fn(acc, edge) {
optional_prefer_first_present(left: acc, right: field_lifecycle_violation(carrier: carrier, edge: edge))
})
ComputationNode { behavior: _ } => Absent
if node_is_module_surface_or_namespace_container(node: carrier) {
optional_absent()
} else {
match carrier.kind {
TypeNode { connective: _ } =>
fold(carrier.children, init: optional_absent(), f: fn(acc, edge) {
optional_prefer_first_present(left: acc, right: field_lifecycle_violation(carrier: carrier, edge: edge))
})
ComputationNode { behavior: _ } => Absent
}
}
}

Expand Down
7 changes: 7 additions & 0 deletions src/v2/lens/mandatory_tag.dag
Original file line number Diff line number Diff line change
Expand Up @@ -58,6 +58,13 @@ import v2.extdeps.languages.dag {
// supersedes the host module parse (the dissolution trigger named by the deleted cli_run.rs
// scaffold block).
//
// DOOR-GRAIN CONTROLS ARE AUTHORABLE ONCE THE SUBTREE ROSTER STOPS REFUSING MODULE
// CONTAINERS (v2.lens.common.record_field_carrier; gunbc#13513). A grafted module tree is no
// longer refused as member_not_a_binder before this root-grain gate runs, so a RED/GREEN pair
// through compile_source_root_ingest_with_admission / validate_then_compile can name this
// lens's reasons. The production callers remain the ones below; native-eval prepare still
// does not owe this gate per module.
//
// NATIVE-EVAL PREPARE DOES NOT OWE THIS GATE PER MODULE (valiant-ram-872, DESIGN section 6b).
// CompileLensRoot is a compile-door obligation: the single gate surface is
// validate_then_compile (v2.compiler.compile required_lens_grain_note). Its production
Expand Down
17 changes: 11 additions & 6 deletions src/v2/lens/unit_modeling.dag
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@ import v2.lens.common.construction_justification { ConstructionJustification, Wa
import std.disposition { SingleAuthority }

import v2.std.witness { Holds }
import v2.lens.common.record_field_carrier { node_is_module_surface_or_namespace_container }
import v2.std.node_query { edge_field_type_name, member_edge_type_node, member_not_a_binder_diagnostic }
import v2.std.diagnostic { node_locus, outcome_accepted, outcome_rejected }
import std.optional { optional_absent, optional_present, optional_prefer_first_present }
Expand Down Expand Up @@ -114,12 +115,16 @@ fn field_unit_violation(carrier: Node, edge: Edge) -> Optional<Diagnostic> {
}

fn carrier_first_unit_violation(carrier: Node) -> Optional<Diagnostic> {
match carrier.kind {
TypeNode { connective: _ } =>
fold(carrier.children, init: optional_absent(), f: fn(acc, edge) {
optional_prefer_first_present(left: acc, right: field_unit_violation(carrier: carrier, edge: edge))
})
ComputationNode { behavior: _ } => Absent
if node_is_module_surface_or_namespace_container(node: carrier) {
optional_absent()
} else {
match carrier.kind {
TypeNode { connective: _ } =>
fold(carrier.children, init: optional_absent(), f: fn(acc, edge) {
optional_prefer_first_present(left: acc, right: field_unit_violation(carrier: carrier, edge: edge))
})
ComputationNode { behavior: _ } => Absent
}
}
}

Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,22 @@
module v2.test.lens_fact_density.surface_identity_atom_not_a_type_carrier

import std.occurrence_identity { OccurrenceSynthetic }
import v2.lens.fact_density { NotATypeCarrier, carrier_spec_fact }
import v2.std.node { Atom, Node, Symbol, TypeNode }

data surface_module_identity_atom: Node = Node {
kind: TypeNode { connective: Atom { identity: ^dag_surface_module } },
children: [],
occurrence_id: OccurrenceSynthetic
}

data surface_body_identity_atom: Node = Node {
kind: TypeNode { connective: Atom { identity: ^namespace_graft_module_body } },
children: [],
occurrence_id: OccurrenceSynthetic
}

test fn surface_identity_atoms_are_not_hollow_aliases() -> Bool {
(carrier_spec_fact(carrier: surface_module_identity_atom) == NotATypeCarrier)
&& (carrier_spec_fact(carrier: surface_body_identity_atom) == NotATypeCarrier)
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,159 @@
module v2.test.lens_unit_modeling.module_container_is_not_a_record_carrier

import std.occurrence_identity { OccurrenceSynthetic }
import v2.compiler.compile {
CompileLensSubtree,
required_lenses_at_grain,
run_required_lens_gates_on_subtree
}
import v2.compiler.infer { InferredTree }
import v2.extdeps.languages.dag {
dag_grammar_atom,
dag_named_edge,
namespace_graft_namespace_body_node
}
import v2.lens.lifecycle_carrier { lifecycle_carrier_gate }
import v2.lens.unit_modeling { unit_modeling_gate }
import v2.std.diagnostic { Accepted, Rejected }
import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly }
import v2.std.node {
Atom,
Authored,
Conj,
Edge,
Node,
Symbol,
TypeNode
}
import v2.test.lens_common.infer_fixture {
claim_inferred_facts,
claim_inferred_tree
}

data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly

data mc_source: Node = Node {
kind: TypeNode { connective: Conj },
children: [],
occurrence_id: OccurrenceSynthetic
}

data mc_marked_body: Node = namespace_graft_namespace_body_node(edges: [], source: mc_source)

data mc_inner_segment: Node = Node {
kind: TypeNode { connective: Conj },
children: [
Edge {
label: Authored { name: ^x },
target: mc_marked_body
}
],
occurrence_id: OccurrenceSynthetic
}

data mc_spine: Node = Node {
kind: TypeNode { connective: Conj },
children: [
Edge {
label: Authored { name: ^extdeps },
target: mc_inner_segment
}
],
occurrence_id: OccurrenceSynthetic
}

data mc_module_shell: Node = Node {
kind: TypeNode { connective: Conj },
children: [
dag_named_edge(
name: ^grammar_production_identity_node_projection,
target: dag_grammar_atom(id: ^dag_surface_module)
),
dag_named_edge(
name: ^grammar_production_captured_node_projection,
target: mc_spine
)
],
occurrence_id: OccurrenceSynthetic
}

fn mc_shell_tree() -> InferredTree {
claim_inferred_tree(
root: mc_module_shell,
facts: claim_inferred_facts(
type_symbol: ^mc_shell_type_sym,
algebra_symbol: ^mc_shell_algebra_sym,
descent_symbol: ^mc_shell_descent_sym
)
)
}

data mc_text_atom: Node = Node {
kind: TypeNode { connective: Atom { identity: ^Text } },
children: [],
occurrence_id: OccurrenceSynthetic
}

data mc_malformed_field_root: Node = Node {
kind: TypeNode { connective: Conj },
children: [
Edge {
label: Authored { name: ^x },
target: mc_text_atom
}
],
occurrence_id: OccurrenceSynthetic
}

fn mc_malformed_field_tree() -> InferredTree {
claim_inferred_tree(
root: mc_malformed_field_root,
facts: claim_inferred_facts(
type_symbol: ^mc_malformed_type_sym,
algebra_symbol: ^mc_malformed_algebra_sym,
descent_symbol: ^mc_malformed_descent_sym
)
)
}

test fn a_module_shell_is_not_refused_as_member_not_a_binder() -> Bool {
match unit_modeling_gate(node: mc_module_shell) {
Accepted { value: _, diagnostics: _ } =>
match lifecycle_carrier_gate(node: mc_module_shell) {
Accepted { value: _, diagnostics: _ } => true
Rejected { diagnostics: _ } => false
}
Rejected { diagnostics: _ } => false
}
}

test fn a_namespace_spine_is_not_refused_as_member_not_a_binder() -> Bool {
match unit_modeling_gate(node: mc_spine) {
Accepted { value: _, diagnostics: _ } =>
match lifecycle_carrier_gate(node: mc_spine) {
Accepted { value: _, diagnostics: _ } => true
Rejected { diagnostics: _ } => false
}
Rejected { diagnostics: _ } => false
}
}

test fn a_grafted_module_tree_clears_the_subtree_roster_of_member_not_a_binder() -> Bool {
match run_required_lens_gates_on_subtree(
inferred: mc_shell_tree(),
lenses: required_lenses_at_grain(grain: CompileLensSubtree)
) {
Accepted { value: _, diagnostics: _ } => true
Rejected { diagnostics: d } => d.head.reason != ^member_not_a_binder
}
}

test fn a_hand_built_field_is_still_member_not_a_binder_on_the_subtree_roster() -> Bool {
match run_required_lens_gates_on_subtree(
inferred: mc_malformed_field_tree(),
lenses: required_lenses_at_grain(grain: CompileLensSubtree)
) {
Rejected { diagnostics: d } => d.head.reason == ^member_not_a_binder
Accepted { value: _, diagnostics: _ } => false
}
}
2 changes: 1 addition & 1 deletion src/v2/workflow/compile_door_cause_ownership.dag
Original file line number Diff line number Diff line change
Expand Up @@ -57,7 +57,7 @@ data known_frontier_causes: List<CauseOwnership> = [
CauseOwnership {
cause: ^member_not_a_binder,
lane: MigrationOwned,
flip_trigger: "RETIRED WHEN v2.lens.lifecycle_carrier and v2.lens.unit_modeling narrow their carrier predicate so that a node whose Authored members are module surface nodes (a container of modules, not a record or payload type) is never judged as a record carrier; this row is then deleted and the door-ledger long test's member_not_a_binder count returns to zero. DIAGNOSIS (advisories step 2, bold-lynx-438): reading the fatal element exposed this cause on dag/std/error_primitives.dag and dag/std/bit.dag. Each refusal is located at the TARGET of the offending member edge, a synthetic dag_surface_module node: both lenses fold every TypeNode's Authored children through v2.std.node_query member_edge_type_node and refuse a child that is not a binder, and a node carrying modules as Authored members reaches that fold. That is a lens defect (the carrier predicate admits a module container), not a correct refusal of these subjects. It was masked at head grain by parse_grammar_choice_overlap_residue. The fix is owned by its own work item, not this row"
flip_trigger: "RETIRED WHEN the door-ledger long test's member_not_a_binder count returns to zero, at which point this row is deleted. The lens predicate is narrowed: v2.lens.common.record_field_carrier node_is_module_surface_or_namespace_container keeps module shells, marked bodies and graft spines out of unit_modeling and lifecycle_carrier, and fact_density treats ^dag_surface_module / ^namespace_graft_module_body identity atoms as NotATypeCarrier. DIAGNOSIS (advisories step 2, bold-lynx-438): the cause on dag/std/error_primitives.dag and dag/std/bit.dag was located at a synthetic dag_surface_module node — a container of modules judged as a record. Door-grain mandatory_tag controls that were blocked on this refusal (gunbc#13513) are now authorable: the subtree roster no longer refuses a grafted module tree with member_not_a_binder (v2.test.lens_unit_modeling.module_container_is_not_a_record_carrier)."
},
CauseOwnership {
cause: ^parse_g0_tokens_remain,
Expand Down
Loading