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
9 changes: 2 additions & 7 deletions src/v2/cli/if_arm_reader_differential.dag
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,7 @@ import v2.extdeps.languages.dag {
ParseSubtreeAbsent,
ParseSubtreeFound,
dag_lex,
dag_surface_identity_is_top_level_item,
dag_surface_kw_then_ident_from_captured,
parse_production_captured_child_optional,
parse_production_emitted_identity_optional
Expand Down Expand Up @@ -280,13 +281,7 @@ fn iard_declaration_name(shell: Node, emitted: Symbol) -> String {
}

fn iard_is_declaration(id: Symbol) -> Bool {
(id == ^dag_surface_fn_decl)
|| (id == ^dag_surface_test_fn_decl)
|| (id == ^dag_surface_data_decl)
|| (id == ^dag_surface_type_decl)
|| (id == ^dag_surface_alias_decl)
|| (id == ^dag_surface_service_decl)
|| (id == ^dag_surface_resource_decl)
dag_surface_identity_is_top_level_item(id: id)
}

// EVERY if_expr IN THE TREE, IN PRE-ORDER, WITH ITS ENCLOSING DECLARATION. Nested ifs are visited:
Expand Down
172 changes: 98 additions & 74 deletions src/v2/extdeps/languages/dag.dag
Original file line number Diff line number Diff line change
Expand Up @@ -3113,28 +3113,67 @@ fn dag_grammar_resource_decl_expr() -> GrammarExpr {
)
}

fn dag_grammar_top_level_item_expr() -> GrammarExpr {
dag_grammar_choice(
left: dag_grammar_nonterminal(production: ^dag_production_import_decl),
right: dag_grammar_choice(
left: dag_grammar_nonterminal(production: ^dag_production_alias_decl),
right: dag_grammar_choice(
left: dag_grammar_nonterminal(production: ^dag_production_type_decl),
right: dag_grammar_choice(
left: dag_grammar_nonterminal(production: ^dag_production_data_decl),
right: dag_grammar_choice(
left: dag_grammar_nonterminal(production: ^dag_production_fn_decl),
right: dag_grammar_choice(
left: dag_grammar_nonterminal(production: ^dag_production_test_fn_decl),
right: dag_grammar_choice(
left: dag_grammar_nonterminal(production: ^dag_production_service_decl),
right: dag_grammar_nonterminal(production: ^dag_production_resource_decl)
)
)
)
)
)
// THE TOP-LEVEL DECLARATION ROWS: one list is the authority for which productions inhabit a
// module as items, for the choice the module grammar repeats, and for which emitted identities
// are declaration members rather than record binders.
fn dag_grammar_top_level_item_productions() -> List<GrammarProduction> {
[
dag_grammar_production(
name: ^dag_production_import_decl,
expression: dag_grammar_import_decl_expr(),
emitted: ^dag_surface_import_decl
),
dag_grammar_production(
name: ^dag_production_alias_decl,
expression: dag_grammar_alias_decl_expr(),
emitted: ^dag_surface_alias_decl
),
dag_grammar_production(
name: ^dag_production_type_decl,
expression: dag_grammar_type_decl_expr(),
emitted: ^dag_surface_type_decl
),
dag_grammar_production(
name: ^dag_production_data_decl,
expression: dag_grammar_data_decl_expr(),
emitted: ^dag_surface_data_decl
),
dag_grammar_production(
name: ^dag_production_fn_decl,
expression: dag_grammar_fn_decl_expr(),
emitted: ^dag_surface_fn_decl
),
dag_grammar_production(
name: ^dag_production_test_fn_decl,
expression: dag_grammar_test_fn_decl_expr(),
emitted: ^dag_surface_test_fn_decl
),
dag_grammar_production(
name: ^dag_production_service_decl,
expression: dag_grammar_service_decl_expr(),
emitted: ^dag_surface_service_decl
),
dag_grammar_production(
name: ^dag_production_resource_decl,
expression: dag_grammar_resource_decl_expr(),
emitted: ^dag_surface_resource_decl
)
]
}

fn dag_grammar_choice_of_production_names(names: List<Symbol>) -> GrammarExpr {
match names {
Cons { head: first, tail: rest } =>
fold(rest, init: dag_grammar_nonterminal(production: first), f: fn(acc, name) {
dag_grammar_choice(left: acc, right: dag_grammar_nonterminal(production: name))
})
Empty => dag_grammar_nonterminal(production: ^dag_production_top_level_item)
}
}

fn dag_grammar_top_level_item_expr() -> GrammarExpr {
dag_grammar_choice_of_production_names(
names: list_map(xs: dag_grammar_top_level_item_productions(), f: fn(p) { p.name })
)
}

Expand Down Expand Up @@ -3368,46 +3407,6 @@ fn dag_grammar_root() -> GrammarRoot {
expression: dag_grammar_top_level_item_expr(),
emitted: ^dag_surface_top_level_item
)
let import_decl = dag_grammar_production(
name: ^dag_production_import_decl,
expression: dag_grammar_import_decl_expr(),
emitted: ^dag_surface_import_decl
)
let alias_decl = dag_grammar_production(
name: ^dag_production_alias_decl,
expression: dag_grammar_alias_decl_expr(),
emitted: ^dag_surface_alias_decl
)
let type_decl = dag_grammar_production(
name: ^dag_production_type_decl,
expression: dag_grammar_type_decl_expr(),
emitted: ^dag_surface_type_decl
)
let data_decl = dag_grammar_production(
name: ^dag_production_data_decl,
expression: dag_grammar_data_decl_expr(),
emitted: ^dag_surface_data_decl
)
let fn_decl = dag_grammar_production(
name: ^dag_production_fn_decl,
expression: dag_grammar_fn_decl_expr(),
emitted: ^dag_surface_fn_decl
)
let test_fn_decl = dag_grammar_production(
name: ^dag_production_test_fn_decl,
expression: dag_grammar_test_fn_decl_expr(),
emitted: ^dag_surface_test_fn_decl
)
let service_decl = dag_grammar_production(
name: ^dag_production_service_decl,
expression: dag_grammar_service_decl_expr(),
emitted: ^dag_surface_service_decl
)
let resource_decl = dag_grammar_production(
name: ^dag_production_resource_decl,
expression: dag_grammar_resource_decl_expr(),
emitted: ^dag_surface_resource_decl
)
let resource_body_entry = dag_grammar_production(
name: ^dag_production_resource_body_entry,
expression: dag_grammar_resource_body_entry_expr(),
Expand Down Expand Up @@ -3823,19 +3822,12 @@ fn dag_grammar_root() -> GrammarRoot {
)
GrammarRoot {
start: ^dag_production_module,
productions: [
module_prod,
module_header,
top_level_item,
import_decl,
alias_decl,
type_decl,
data_decl,
fn_decl,
test_fn_decl,
service_decl,
productions: list_append(
left: [module_prod, module_header, top_level_item],
right: list_append(
left: dag_grammar_top_level_item_productions(),
right: [
service_body_entry,
resource_decl,
resource_body_entry,
resource_kind,
resource_mode,
Expand Down Expand Up @@ -3917,7 +3909,9 @@ fn dag_grammar_root() -> GrammarRoot {
if_expr,
fn_literal,
arrow_lambda
],
]
)
),
sync_tokens: dag_sync_tokens()
}
}
Expand Down Expand Up @@ -6774,6 +6768,36 @@ fn parse_production_emitted_identity_optional(node: Node) -> Optional<Symbol> {
}
}

fn dag_surface_identity_is_top_level_item(id: Symbol) -> Bool {
fold_list(
xs: dag_grammar_top_level_item_productions(),
empty: false,
cons: fn(acc, production) {
acc || match node_atom_identity_optional(node: production.emitted) {
Present { value: emitted } => emitted == id
Absent => false
}
}
)
}

// Parse identities that inhabit a module as Authored members and are not record binders:
// the module surface and graft-body stamp as the only explicit extras, plus every emitted
// identity of dag_grammar_top_level_item_productions. Identity only — a missing stamp is
// false, never a Conj-shape guess (DESIGN §5: refuse the member, never widen to the container).
fn dag_surface_identity_is_module_member(id: Symbol) -> Bool {
(id == ^dag_surface_module)
|| (id == ^namespace_graft_module_body)
|| dag_surface_identity_is_top_level_item(id: id)
}

fn dag_node_is_module_member_surface(node: Node) -> Bool {
match parse_production_emitted_identity_optional(node: node) {
Present { value: id } => dag_surface_identity_is_module_member(id: id)
Absent => false
}
}

fn dag_node_is_fn_decl(node: Node) -> Bool {
match parse_production_emitted_identity_optional(node: node) {
Present { value: id } => id == ^dag_surface_fn_decl
Expand Down
15 changes: 11 additions & 4 deletions src/v2/lens/reference_derived_residency_reading.dag
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,7 @@ import std.decl_ref { DeclarationRef }
import v2.std.algebra { length }
import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly }
import std.optional { Absent, Optional, Present, optional_absent, optional_present }
import v2.extdeps.languages.dag { dag_node_is_module_member_surface }
import v2.std.node_query { member_edge_type_node }
import v2.std.node {
Arrow,
Expand Down Expand Up @@ -168,7 +169,9 @@ fn decl_first_unrecognised_atom(decl: Node) -> Optional<Symbol> {
}

// A Named member that is not a binder is read first: the carrier declares no type for it, and that
// refuses the whole reading rather than letting the remaining fields decide it.
// refuses the whole reading rather than letting the remaining fields decide it. Identity-stamped
// module or declaration members (v2.extdeps.languages.dag dag_node_is_module_member_surface) are
// skipped per target; a hand-built field on the same Conj is still refused.
fn decl_first_member_not_a_binder(decl: Node) -> Optional<Symbol> {
match decl.kind {
TypeNode { connective: _ } =>
Expand All @@ -180,9 +183,13 @@ fn decl_first_member_not_a_binder(decl: Node) -> Optional<Symbol> {
Positional => acc
StructuralLabel { label: _ } => acc
Authored { name: nm } =>
match member_edge_type_node(e: edge) {
Present { value: _ } => acc
Absent => optional_present(value: nm)
if dag_node_is_module_member_surface(node: edge.target) {
acc
} else {
match member_edge_type_node(e: edge) {
Present { value: _ } => acc
Absent => optional_present(value: nm)
}
}
}
}
Expand Down
107 changes: 106 additions & 1 deletion src/v2/test/claim/reference_derived_residency_reading_test.dag
Original file line number Diff line number Diff line change
Expand Up @@ -34,7 +34,13 @@ import v2.lens.reference_derived_residency_reading { carrier_reading_from_type_d
import v2.std.diagnostic { Accepted, Rejected }
import std.optional { Absent, Present }
import v2.std.qualified_name { qualified_name_snoc }
import v2.extdeps.languages.dag { qualified_name_from_module_node }
import v2.extdeps.languages.dag {
qualified_name_from_module_node,
dag_named_edge,
dag_surface_edge,
dag_surface_identity_is_module_member,
dag_surface_identity_is_top_level_item,
}
import v2.std.symbol_index { empty_symbol_index, symbol_index_lookup }
import v2.test.claim.reference_derived_graph_fixture { xl4_fixture_trees, xl4_item_at, consumer_field_bare_local_path }
import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly }
Expand Down Expand Up @@ -238,6 +244,105 @@ test fn an_alias_typed_field_is_not_readable() -> Bool {
!readability_is_recognised(r: reading_of(decl_name: "ReferenceDerivedPool", decl: alias_typed_declaration()))
}

fn identity_stamped(id: Symbol) -> Node {
Node {
kind: TypeNode { connective: Conj },
children: [dag_named_edge(name: ^grammar_production_identity_node_projection, target: atom(identity: id))],
occurrence_id: OccurrenceSynthetic,
}
}

fn module_container_with_surface_members() -> Node {
Node {
kind: TypeNode { connective: Conj },
children: [
dag_surface_edge(edge: ^dag_surface_module_header, target: atom(identity: ^dag_surface_module_header)),
Edge { label: Authored { name: ^bit }, target: identity_stamped(id: ^dag_surface_fn_decl) },
Edge { label: Authored { name: ^nested }, target: identity_stamped(id: ^dag_surface_module) },
Edge { label: Authored { name: ^probe }, target: identity_stamped(id: ^dag_surface_test_fn_decl) },
Edge { label: Authored { name: ^Flag }, target: identity_stamped(id: ^dag_surface_data_decl) },
Edge { label: Authored { name: ^Wrapper }, target: identity_stamped(id: ^dag_surface_type_decl) },
Edge { label: Authored { name: ^Alias }, target: identity_stamped(id: ^dag_surface_alias_decl) },
],
occurrence_id: OccurrenceSynthetic,
}
}

fn mixed_declaration_and_hand_built_field() -> Node {
Node {
kind: TypeNode { connective: Conj },
children: [
Edge { label: Authored { name: ^Flag }, target: identity_stamped(id: ^dag_surface_data_decl) },
Edge { label: Authored { name: ^trees }, target: atom(identity: ^Node) },
],
occurrence_id: OccurrenceSynthetic,
}
}

fn conj_with_header_edge_and_hand_built_field() -> Node {
Node {
kind: TypeNode { connective: Conj },
children: [
dag_surface_edge(edge: ^dag_surface_module_header, target: atom(identity: ^dag_surface_module_header)),
Edge { label: Authored { name: ^trees }, target: atom(identity: ^Node) },
],
occurrence_id: OccurrenceSynthetic,
}
}

fn hand_built_record_field_declaration() -> Node {
record_of(fields: [Edge { label: Authored { name: ^trees }, target: atom(identity: ^Node) }])
}

fn readability_is_member_not_a_binder(r: ProducerCarrierReading, expected: Symbol) -> Bool {
match r.readability {
CarrierMemberNotABinder { member: member } => member == expected
CarrierTypeRecognized => false
CarrierTypeUnrecognized { spelling: _ } => false
}
}

// A MODULE CONTAINER IS NOT A RECORD PAYLOAD. Its Authored members are dag_surface_module nodes and
// declarations; asking member_edge_type_node of them used to mint CarrierMemberNotABinder.
test fn a_module_container_is_not_read_as_a_non_binder_record() -> Bool {
readability_is_recognised(r: reading_of(decl_name: "ModuleContainer", decl: module_container_with_surface_members()))
}

// THE RED THE SKIP MUST NOT ERASE: a hand-built name-to-type field on a genuine record still reports
// CarrierMemberNotABinder, named.
test fn a_hand_built_record_field_still_reports_member_not_a_binder() -> Bool {
readability_is_member_not_a_binder(
r: reading_of(decl_name: "HandBuiltCarrier", decl: hand_built_record_field_declaration()),
expected: ^trees,
)
}

// A HEADER EDGE ON THE CONJ IS NOT A CONTAINER-WIDE SKIP. The member that is not identity-stamped
// is still CarrierMemberNotABinder; skipping the whole Conj because it carries a header is the
// widen the door-lens ruling forbids.
test fn a_header_edge_on_a_conj_does_not_skip_a_hand_built_field() -> Bool {
readability_is_member_not_a_binder(
r: reading_of(decl_name: "HeaderAndField", decl: conj_with_header_edge_and_hand_built_field()),
expected: ^trees,
)
}

test fn top_level_item_identities_come_from_the_grammar_rows() -> Bool {
dag_surface_identity_is_top_level_item(id: ^dag_surface_data_decl)
&& dag_surface_identity_is_top_level_item(id: ^dag_surface_import_decl)
&& !dag_surface_identity_is_top_level_item(id: ^dag_surface_module)
&& dag_surface_identity_is_module_member(id: ^dag_surface_module)
}

// A DATA DECLARATION SIBLING DOES NOT WIDEN THE SKIP. The identity-stamped member is skipped;
// the hand-built field on the same Conj is still CarrierMemberNotABinder.
test fn a_data_decl_member_does_not_skip_a_hand_built_sibling() -> Bool {
readability_is_member_not_a_binder(
r: reading_of(decl_name: "Mixed", decl: mixed_declaration_and_hand_built_field()),
expected: ^trees,
)
}

// THE BLOCKING ARM. Under the earlier derivation this qualified -- both axes fell through to their
// admitting values -- so a producer could buy the admission by renaming a type while the same corpus
// stayed resident (review 68724). It must refuse, and it must refuse NAMING the carrier and the
Expand Down
Loading