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
Original file line number Diff line number Diff line change
@@ -0,0 +1,25 @@
module gunbc.guarantee_stall.member_kind_door_binding_executed_by_no_claim_stall

import gunbc.guarantee_rung { Mitigatable, MechanicallyPreventable }
import gunbc.guarantee_stall { GuaranteeStall, AwaitsOneGrounding, BoundedPopulation, climbs_when }

// A NEW LINK THAT HAS NEVER EXECUTED, RECORDED AS A STALL -- NOT A DROP: no rung stood here and none is claimed to have
// fallen. gunbc#13513 carries the authored data-vs-fn kind from normalize to the mandatory_tag gate
// (NormalizedTree.member_declarations -> member_kind_channel_of_tree -> ResolvedTree.member_kinds). The legs
// normalize -> member_kind_channel_of_tree -> gate execute in test.long.mandatory_tag_gate_witness. The leg from
// v2.compiler.name_resolve resolve_in_context (subject_member_kind_channel) through ResolvedTree.member_kinds to
// v2.compiler.compile validate_then_compile's mandatory_tag_root_lens_with_provenance binding is compiled and
// typechecked and executed by no claim: a door-grain control through compile_source_root_ingest_with_admission was
// refused with member_not_a_binder by a roster lens ahead of mandatory_tag on even a trivial single-module extdeps.*
// subject, a refusal independent of #13513 and filed as its own item. Each removed door-grain witness measured roughly
// 470-560k eval steps against the 72300 new-witness budget, so it is a long-lane witness once runnable.
data member_kind_door_binding_executed_by_no_claim_stall: GuaranteeStall = GuaranteeStall {
subject: "door-grain mandatory_tag provenance: the resolve_in_context -> ResolvedTree.member_kinds -> validate_then_compile mandatory_tag_root_lens_with_provenance link is executed by no claim",
current: Mitigatable,
ceiling: MechanicallyPreventable,
blocker: AwaitsOneGrounding { grounding: "the door accepting a minimal extdeps.* subject past every roster lens (the member_not_a_binder door refusal, its own item), which makes the door-grain controls runnable" },
population: BoundedPopulation { members: [
"v2.compiler.name_resolve resolve_in_context subject_member_kind_channel -> v2.compiler.resolve ResolvedTree.member_kinds -> v2.compiler.compile validate_then_compile mandatory_tag_root_lens_with_provenance, for every extdeps.* subject compiled through compile_source_root_ingest_with_admission"
] },
next_rung_trigger: climbs_when(capability: "a minimal extdeps.* subject is accepted through compile_source_root_ingest_with_admission past every roster lens, and the door-grain mandatory_tag clean and zero-arg-fn impersonation controls execute on the long lane. SUFFICIENT FOR: deleting the ResolvedTree.member_kinds binding (or resolve_in_context's subject_member_kind_channel) turns a door-grain control red. A control that supplies the channel, runs a lens directly, or reaches the gate below the door retires nothing")
}
2 changes: 2 additions & 0 deletions dag/gunbc/guarantee_stall/roster.dag
Original file line number Diff line number Diff line change
Expand Up @@ -76,6 +76,7 @@ import gunbc.guarantee_stall.text_carrier_render_not_keyed_on_identity_stall { t
import gunbc.guarantee_stall.free_semigroup_text_crossing_decided_by_spelling_stall { free_semigroup_text_crossing_decided_by_spelling_stall }
import gunbc.guarantee_stall.emitted_inline_crate_path_edges_unreturned_stall { emitted_inline_crate_path_edges_unreturned_stall }
import gunbc.guarantee_stall.compile_pool_provision_wired_but_unreachable_stall { compile_pool_provision_wired_but_unreachable_stall }
import gunbc.guarantee_stall.member_kind_door_binding_executed_by_no_claim_stall { member_kind_door_binding_executed_by_no_claim_stall }
import gunbc.guarantee_stall.filesystem_read_outcome_node_grain_census_stall { filesystem_read_outcome_node_grain_census_stall }

// THE COHORT PROVENANCE NOTES BELOW WERE AUTHORED WHEN EVERY ROW SAT IN ONE FILE, and they are
Expand Down Expand Up @@ -248,6 +249,7 @@ data all_guarantee_stalls: List<GuaranteeStall> = [
browser_ready_labels_fleet_route_stall,
accumulator_copy_untyped_combiner_refusals_stall,
keyed_apply_patch_rebuilds_rows_per_hunk_stall,
member_kind_door_binding_executed_by_no_claim_stall,
filesystem_read_outcome_node_grain_census_stall,
]

Expand Down
28 changes: 24 additions & 4 deletions src/v2/compiler/00_compile.dag
Original file line number Diff line number Diff line change
Expand Up @@ -200,7 +200,8 @@ import v2.extdeps.languages.dag {
import v2.lens.complexity_accumulator_copy.compile_gate { accumulator_copy_compile_gate }
import v2.lens.determinism { determinism_compile_gate }
import v2.lens.machine_shape { machine_shape_compile_gate }
import v2.lens.mandatory_tag { mandatory_tag_compile_gate }
import v2.lens.mandatory_tag { mandatory_tag_compile_gate, mandatory_tag_compile_gate_with_provenance }
import v2.std.member_declaration_kind { MemberKindChannel, no_member_declaration_kinds }
import v2.lens.undecidable_verdict_collapse { undecidable_verdict_collapse_compile_gate }
import v2.lens.fact_density { fact_density_hollow_alias_gate }
import v2.lens.unit_modeling { unit_modeling_gate }
Expand Down Expand Up @@ -795,6 +796,20 @@ fn machine_shape_root_gate(tree: InferredTree) -> Outcome<Witness<Node>> {
machine_shape_compile_gate(node: tree.root)
}

// The compile door's binding of the mandatory_tag gate: the same gate, handed the member-kind provenance
// the resolved subject carries (ResolvedTree.member_kinds).
fn mandatory_tag_root_lens_with_provenance(lens: CompileLens, channel: MemberKindChannel) -> CompileLens {
if lens.identity == mandatory_tag_lens.identity {
CompileLens {
identity: lens.identity,
grain: lens.grain,
gate: fn(tree) { mandatory_tag_compile_gate_with_provenance(node: tree.root, channel: channel) }
}
} else {
lens
}
}

fn mandatory_tag_root_gate(tree: InferredTree) -> Outcome<Witness<Node>> {
mandatory_tag_compile_gate(node: tree.root)
}
Expand Down Expand Up @@ -1042,9 +1057,13 @@ fn validate_then_compile(
bind_outcome(
o: run_required_lens_gates(
inferred: inferred,
lenses: list_append(
left: required_lenses_at_grain(grain: CompileLensRoot),
right: lenses_at_grain(lenses: lenses, grain: CompileLensRoot)
lenses: fold(
list_append(
left: required_lenses_at_grain(grain: CompileLensRoot),
right: lenses_at_grain(lenses: lenses, grain: CompileLensRoot)
),
init: [],
f: fn(acc, l) { list_snoc_item(xs: acc, item: mandatory_tag_root_lens_with_provenance(lens: l, channel: source.member_kinds)) }
)
),
f: fn(root_witnesses) {
Expand Down Expand Up @@ -3506,6 +3525,7 @@ fn native_module_resolve_verdict(
symbol_index: shared.symbol_index,
closure_declarations: closure.declarations,
unavailable_providers: closure.refused,
member_kinds: no_member_declaration_kinds(),
lexical: lexical
)
},
Expand Down
5 changes: 3 additions & 2 deletions src/v2/compiler/03_ingest.dag
Original file line number Diff line number Diff line change
Expand Up @@ -38,6 +38,7 @@ import v2.compiler.translate { coerce_grounded_node }
import v2.compiler.target_serialize { target_bundle_child }
import v2.std.inhabitant_neutralization { neutralize_core_for_target }
import v2.std.node { Edge, Authored, StructuralLabel, Node, Positional, Symbol, TypeNode, Conj }
import v2.std.member_declaration_kind { no_member_declaration_kinds }
import v2.std.diagnostic {
Accepted,
Diagnostic,
Expand Down Expand Up @@ -337,7 +338,7 @@ fn parse_tree_to_target_model_bridge(parse_tree: ParseTree, source_model: Target
o: parse_tree_to_emitted_node(parse_tree: parse_tree, source_model: source_model),
f: fn(emitted) {
bind_outcome(
o: infer_and_discharge(tree: ResolvedTree { root: emitted, symbol_index: empty_symbol_index(), resolved_declarations: empty_symbol_index(), lexical_bindings: empty_map(), unavailable_providers: [] }),
o: infer_and_discharge(tree: ResolvedTree { root: emitted, symbol_index: empty_symbol_index(), resolved_declarations: empty_symbol_index(), lexical_bindings: empty_map(), unavailable_providers: [], member_kinds: no_member_declaration_kinds() }),
f: fn(inferred) {
bind_outcome(
o: coerce_grounded_node(source: emitted, tree: inferred, target: source_model),
Expand All @@ -362,7 +363,7 @@ fn cross_language_compile(
o: neutralize_core_for_target(core: core, target: target_model),
f: fn(neutralized) {
bind_outcome(
o: infer_and_discharge(tree: ResolvedTree { root: neutralized, symbol_index: empty_symbol_index(), resolved_declarations: empty_symbol_index(), lexical_bindings: empty_map(), unavailable_providers: [] }),
o: infer_and_discharge(tree: ResolvedTree { root: neutralized, symbol_index: empty_symbol_index(), resolved_declarations: empty_symbol_index(), lexical_bindings: empty_map(), unavailable_providers: [], member_kinds: no_member_declaration_kinds() }),
f: fn(inferred) {
emit(tree: inferred, target: target_model)
}
Expand Down
29 changes: 23 additions & 6 deletions src/v2/compiler/03_name_resolve.dag
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@ module v2.compiler.name_resolve

import std.types { List }
import v2.std.language_model { LanguageModel }
import v2.std.member_declaration_kind { MemberKindChannel, no_member_declaration_kinds }

import v2.compiler.symbol_index_fill { symbol_index_fill_module_declarations, symbol_index_fill_module_roots }
import v2.compiler.normalized_tree { NormalizedTree, normalized_tree_roots_to_binding_sources }
Expand All @@ -16,6 +17,7 @@ import v2.compiler.resolve {
ResolveNodeWalk,
ResolveWalkRefused,
ClosureProviderRefusal,
member_kind_channel_of_tree,
ResolvedTree,
resolved_tree_outcome,
resolve_walk_prefix_pending,
Expand Down Expand Up @@ -695,6 +697,16 @@ fn subject_module_root_for_name(
}
}

// The subject root's member-kind channel, read from the validated roots by the subject's own name. A subject
// with no root there has no provenance to give, which is Unavailable and not a refusal here: the module-not-found
// refusal already belongs to admission.
fn subject_member_kind_channel(roots: ValidatedModuleRoots, name: QualifiedName) -> Outcome<MemberKindChannel> {
match map_lookup(m: roots.by_name, key: name) {
Present { value: root } => member_kind_channel_of_tree(tree: root)
Absent => Accepted { value: no_member_declaration_kinds(), diagnostics: v2.std.diagnostic.None }
}
}

fn namespace_admission_initial_state(
policy: NameResolutionPolicy,
canonical_symbols: PointwisePower<Symbol>,
Expand Down Expand Up @@ -936,12 +948,17 @@ fn resolve_in_context(context: Outcome<ResolutionContext>, admission: Admission)
Accepted { value: shared, diagnostics: d } =>
let closure = closure_declarations_demand(shared: shared)
ContextResolved {
resolved: resolved_tree_outcome(
w: walked.walk,
symbol_index: shared.symbol_index,
closure_declarations: closure.declarations,
unavailable_providers: closure.refused
),
resolved: match subject_member_kind_channel(roots: shared.roots, name: admission.subject.name) {
Rejected { diagnostics: r } => Rejected { diagnostics: r }
Accepted { value: channel, diagnostics: _ } =>
resolved_tree_outcome(
w: walked.walk,
symbol_index: shared.symbol_index,
closure_declarations: closure.declarations,
unavailable_providers: closure.refused,
member_kinds: channel
)
},
context: Accepted { value: closure.context, diagnostics: d }
}
}
Expand Down
61 changes: 58 additions & 3 deletions src/v2/compiler/03_normalize.dag
Original file line number Diff line number Diff line change
Expand Up @@ -75,15 +75,23 @@ import v2.compiler.normalized_tree {
NormalizedTree,
admit_census_tree,
admit_normalized_tree,
admit_retention_free
admit_retention_free,
normalized_tree_with_member_declarations
}
import v2.std.member_declaration_kind { DeclaredDataMember, DeclaredFnMember, DeclaredMember }
import v2.compiler.test_marker_capture { test_marker_capture }
import v2.compiler.namespace_graft {
module_header_containment_graft,
namespace_graft_is_graft_candidate
namespace_graft_collect_unit_nodes_against,
namespace_graft_is_graft_candidate,
namespace_graft_top_level_item_alternative_emitted_ids
}
import v2.extdeps.languages.dag {
dag_grammar_root,
dag_surface_kw_then_ident_from_captured,
import_binding_rows_from_decl_node,
namespace_graft_unwrap_module_working_root,
parse_production_captured_child_optional,
parse_production_emitted_identity_optional
}
import std.types { List }
Expand Down Expand Up @@ -408,6 +416,47 @@ fn type_declaration_kind_capture(nodes: List<Node>) -> FreeMonoid<DeclaredTypeKi
)
}

// THE AUTHORED KIND OF EACH TOP-LEVEL MEMBER, read from the parse for the reason type_declaration_kind_capture
// is: lowering turns `data x: T = v` and `fn x() -> T { v }` into one shape (a named nullary Arrow), so
// after normalize nothing in the Node says which was authored. The population is the graft's own unit
// census (namespace_graft_collect_unit_nodes_against over the module's working root, the same units the
// graft partitions into members), NOT every node of the parse: a declaration nested in another unit is
// not a member of the module. A data or fn unit whose name cannot be read contributes no row, so a
// consumer asking for it finds it not declared and refuses, never a fabricated kind.
// v2.std.member_declaration_kind MemberKindChannel is what carries these to a later grain.
fn member_declaration_capture(tree: ParseTree) -> FreeMonoid<DeclaredMember> {
let unit_ids = namespace_graft_top_level_item_alternative_emitted_ids(productions: dag_grammar_root().productions)
fold_list(
xs: namespace_graft_collect_unit_nodes_against(node: namespace_graft_unwrap_module_working_root(root: tree), unit_ids: unit_ids),
empty: Empty,
cons: fn(acc, unit) {
match parse_production_emitted_identity_optional(node: unit) {
Absent => acc
Present { value: id } =>
if (id == ^dag_surface_data_decl) || (id == ^dag_surface_fn_decl) {
match parse_production_captured_child_optional(node: unit) {
Absent => acc
Present { value: captured } =>
match dag_surface_kw_then_ident_from_captured(captured: captured) {
Absent => acc
Present { value: name } =>
list_snoc_item(
xs: acc,
item: DeclaredMember {
name: name,
kind: if id == ^dag_surface_data_decl { DeclaredDataMember } else { DeclaredFnMember }
}
)
}
}
} else {
acc
}
}
}
)
}

// WHICH MODIFIERS EACH TYPE DECLARATION'S SLOT CARRIES, read from the parse tree for the reason
// type_declaration_kind_capture is: lowering leaves no trace of the slot in the node. The question is
// answered by the lowering's own reader (v2.compiler.body_lowering_fold
Expand Down Expand Up @@ -507,7 +556,13 @@ fn normalize_with(parse_tree: ParseTree, source: NormalizeAllocatorSource) -> Ou
) {
Rejected { diagnostics: r } => Rejected { diagnostics: r }
Accepted { value: tree, diagnostics: d2 } =>
Accepted { value: ScopedNormalizedTree { tree: tree, allocator: allocated.allocator }, diagnostics: d2 }
Accepted {
value: ScopedNormalizedTree {
tree: normalized_tree_with_member_declarations(tree: tree, members: member_declaration_capture(tree: parse_tree)),
allocator: allocated.allocator
},
diagnostics: d2
}
}
}
}
Expand Down
Loading