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
185 changes: 150 additions & 35 deletions src/v2/compiler/body_lowering_fold.dag
Original file line number Diff line number Diff line change
Expand Up @@ -468,28 +468,34 @@ fn body_lower_is_metadata_preserved_emitted(emitted: Symbol) -> Bool {

// THE SAME SHAPE AS #8828, ONE NODE CLASS OVER: a shell with no body to lower FROM ITS OWN NODE was
// arriving at the unregistered-producer arm, so 'this production has no body-producer yet' and
// 'this production is structure, not a body' were one state. The five identities below are
// declaration and literal STRUCTURE -- a coproduct variant, a type-alias right-hand side, a
// field-declaration block, an fn type, and a record literal's named field. Four of them are type
// syntax, which has no Behavior to lower to at all; the fifth carries an expression that the
// bottom-up fold has ALREADY lowered before this node is reached, so preserving the shell preserves
// a lowered child, never an unlowered one. Preserving is what
// 'this production is structure, not a body' were one state. The identities
// body_lower_is_structure_preserved_emitted enumerates are declaration and literal STRUCTURE:
// type syntax with no Behavior to lower to, and expression shells whose children the
// bottom-up fold has already lowered, so preserving the shell preserves a lowered child,
// never an unlowered one. Preserving is what
// body_lower_is_metadata_preserved_emitted already does for the OUTER declarations these sit inside
// (dag_surface_type_decl, dag_surface_data_decl) -- the classification was written per node and the
// fold reaches inside, so every interior of an already-preserved declaration re-entered the
// dispatch and fell to the else arm.
//
// FOLD ORDER IS THE LOAD-BEARING ASSUMPTION FOR dag_surface_field_init, AND FOR IT ALONE. The other
// four are safe by what they ARE -- type syntax with no Behavior to lower to. field_init is safe by
// WHEN this dispatch reaches it: normalize_node_ctx folds children first and passes the FOLDED node
// to body_lower_finish_for_normalize, so the expression is already lowered by the time the shell is
// preserved. There is a live path in that same function where dispatch sees an UNFOLDED node -- the
// deferred arm passes `folded: n` and does not fold children -- so adding field_init to
// FOLD ORDER IS THE LOAD-BEARING ASSUMPTION FOR dag_surface_field_init, AND FOR THE TWO
// FUNCTION-VALUE SHELLS THAT SIT IN EXPRESSION POSITION (dag_surface_arrow_lambda,
// dag_surface_fn_literal). Those two were arriving at the unregistered-producer arm from a
// data initializer, so a lambda that already lowers as a call argument or fn-body field produced
// wrapper-retention diagnostics only because the DATA declaration's interior re-entered
// dispatch. Preserving the shell after the child fold keeps the production identity later
// consumers (fold_lowering's fn_literal search) still find, and does not emit retention.
// Type syntax is safe by what it IS -- no Behavior to lower to. field_init
// and the function-value shells are safe by WHEN this dispatch reaches them: normalize_node_ctx
// folds children first and passes the FOLDED node to body_lower_finish_for_normalize. There is a
// live path in that same function where dispatch sees an UNFOLDED node -- the deferred arm passes
// `folded: n` and does not fold children -- so adding these identities to
// body_lower_is_deferred_lower_at_normalize, or otherwise dispatching before the child fold, would
// preserve a shell around an UNLOWERED expression. NONE OF THE THREE WITNESSES WOULD CATCH THAT:
// their field values are the literal 1, which lowers to itself, so the reordered and the current
// fold produce the same tree for exactly those sources. Stated here rather than covered, because an
// assumption named in the carrier is worth more than a witness that does not actually cover it.
// preserve a shell around an UNLOWERED expression. NONE OF THE THREE WITNESSES WOULD CATCH THAT
// for field_init: their field values are the literal 1, which lowers to itself, so the reordered
// and the current fold produce the same tree for exactly those sources. The function-value rows
// would catch it. Stated here rather than covered for field_init, because an assumption named in
// the carrier is worth more than a witness that does not actually cover it.
// RUNG: this is a scope correction to a classifier, not a climb. The retained arm remains the
// counted frontier for a body shape with no producer, and that is the discriminating control: an
// emitted identity in none of these lists still retains, so the arm is not widened into an
Expand All @@ -505,6 +511,8 @@ fn body_lower_is_structure_preserved_emitted(emitted: Symbol) -> Bool {
|| (emitted == ^dag_surface_field_init)
|| (emitted == ^dag_surface_where_refinement_clause)
|| (emitted == ^dag_surface_where_predicate)
|| (emitted == ^dag_surface_arrow_lambda)
|| (emitted == ^dag_surface_fn_literal)
}

// A where-clause on a type-variant is a parse-projection sibling of the base
Expand Down Expand Up @@ -2913,28 +2921,74 @@ fn body_lower_wire_match_arm_capture(arm_capture: Node) -> Outcome<Node> {
}
}

// A comma-list Repeat tail is Seq(Repeat(optional-comma + item), optional trailing comma).
// One arm leaves that Repeat empty (empty Conj) and the trailing comma Optional empty.
// Those nodes are skipped BEFORE extract, so an extract refusal is never discarded and an
// unknown shape never becomes "no arm here" (review 63228: default-true exhausted was a
// silent dropped arm). Skip is only: empty Conj, a comma atom, Optional whose element skips,
// or a sequence whose both sides skip. Anything else is handed to extract, and its Rejected stands.
fn body_lower_match_arm_repeat_elem_is_separator(node: Node) -> Bool {
let stripped = body_lower_deep_unwrap_optional(node: node)
if is_empty_conj_root(n: stripped) {
true
} else {
match node_atom_identity_optional(node: stripped) {
Present { value: id } => id == ^dag_token_comma
Absent =>
match sugar_sequence_pair_optional(node: stripped) {
Present { value: pair } =>
body_lower_match_arm_repeat_elem_is_separator(node: pair.left)
&& body_lower_match_arm_repeat_elem_is_separator(node: pair.right)
Absent =>
match find_named_child(
root: stripped,
name: ^grammar_optional_element_node_projection
) {
Accepted { value: child, diagnostics: _ } =>
body_lower_match_arm_repeat_elem_is_separator(node: child)
Rejected { diagnostics: _ } => false
}
}
}
}
}

fn body_lower_collect_match_arms_from_repeat_tail(repeat_capture: Node) -> Outcome<List<Node>> {
if is_empty_conj_root(n: repeat_capture) {
outcome_accepted(value: Empty)
} else {
match find_named_child(root: repeat_capture, name: ^grammar_sequence_left_node_projection) {
Accepted { value: head, diagnostics: _ } =>
match body_lower_extract_comma_list_arm_head(node: head) {
Rejected { diagnostics: r } => Rejected { diagnostics: r }
Accepted { value: arm, diagnostics: d } =>
match find_named_child(root: repeat_capture, name: ^grammar_sequence_right_node_projection) {
Accepted { value: tail, diagnostics: _ } =>
match body_lower_collect_match_arms_from_repeat_tail(repeat_capture: tail) {
Rejected { diagnostics: r } => Rejected { diagnostics: r }
Accepted { value: rest, diagnostics: rd } =>
Accepted {
value: list_append(left: [arm], right: rest),
diagnostics: diagnostics_merge(outer: d, inner: rd)
}
}
Rejected { diagnostics: _ } =>
Accepted { value: [arm], diagnostics: d }
}
if body_lower_match_arm_repeat_elem_is_separator(node: head) {
match find_named_child(
root: repeat_capture,
name: ^grammar_sequence_right_node_projection
) {
Accepted { value: tail, diagnostics: _ } =>
body_lower_collect_match_arms_from_repeat_tail(repeat_capture: tail)
Rejected { diagnostics: _ } => outcome_accepted(value: Empty)
}
} else {
match body_lower_extract_comma_list_arm_head(node: head) {
Rejected { diagnostics: r } => Rejected { diagnostics: r }
Accepted { value: arm, diagnostics: d } =>
match find_named_child(
root: repeat_capture,
name: ^grammar_sequence_right_node_projection
) {
Accepted { value: tail, diagnostics: _ } =>
match body_lower_collect_match_arms_from_repeat_tail(repeat_capture: tail) {
Rejected { diagnostics: r } => Rejected { diagnostics: r }
Accepted { value: rest, diagnostics: rd } =>
Accepted {
value: list_append(left: [arm], right: rest),
diagnostics: diagnostics_merge(outer: d, inner: rd)
}
}
Rejected { diagnostics: _ } =>
Accepted { value: [arm], diagnostics: d }
}
}
}
Rejected { diagnostics: _ } => outcome_accepted(value: Empty)
}
Expand Down Expand Up @@ -4365,11 +4419,30 @@ fn body_lower_try_match_from_captured(captured: Node) -> Outcome<Optional<Node>>
}
}

fn body_lower_match_spine_has_lbrace(spine: Node) -> Bool {
match body_lower_match_arms_after_lbrace_optional(spine: spine) {
Rejected { diagnostics: _ } => true
Accepted { value: arms_opt, diagnostics: _ } =>
match arms_opt {
Present { value: _ } => true
Absent => false
}
}
}

fn body_lower_match_capture_heads_spine(spine: Node) -> Bool {
match body_lower_match_spine_left(spine: spine) {
Present { value: left } =>
match node_atom_identity_optional(node: body_lower_deep_unwrap_optional(node: left)) {
Present { value: id } => id == ^dag_token_kw_match
Present { value: id } =>
if id == ^dag_token_kw_match {
match body_lower_match_spine_right(spine: spine) {
Present { value: right } => body_lower_match_spine_has_lbrace(spine: right)
Absent => false
}
} else {
false
}
Absent => false
}
Absent => false
Expand All @@ -4381,7 +4454,24 @@ fn body_lowering_match_spine_identity_absent_fixture_spine() -> Node {
kind: TypeNode { connective: Atom { identity: ^dag_token_kw_match } },
children: []
)
let tail = node_synthetic(kind: TypeNode { connective: Conj }, children: [])
let lbrace = node_synthetic(
kind: TypeNode { connective: Atom { identity: ^dag_token_lbrace } },
children: []
)
let empty_interior = node_synthetic(kind: TypeNode { connective: Conj }, children: [])
let braced = node_synthetic(
kind: TypeNode { connective: Conj },
children: [
Edge {
label: Named { name: ^grammar_sequence_left_node_projection },
target: lbrace
},
Edge {
label: Named { name: ^grammar_sequence_right_node_projection },
target: empty_interior
}
]
)
node_synthetic(
kind: TypeNode { connective: Conj },
children: [
Expand All @@ -4391,7 +4481,7 @@ fn body_lowering_match_spine_identity_absent_fixture_spine() -> Node {
},
Edge {
label: Named { name: ^grammar_sequence_right_node_projection },
target: tail
target: braced
}
]
)
Expand All @@ -4403,6 +4493,31 @@ fn body_lowering_match_spine_identity_absent_sniff_holds() -> Bool {
)
}

fn body_lowering_match_field_name_spine() -> Node {
let match_kw = node_synthetic(
kind: TypeNode { connective: Atom { identity: ^dag_token_kw_match } },
children: []
)
let empty_suffix = node_synthetic(kind: TypeNode { connective: Conj }, children: [])
node_synthetic(
kind: TypeNode { connective: Conj },
children: [
Edge {
label: Named { name: ^grammar_sequence_left_node_projection },
target: match_kw
},
Edge {
label: Named { name: ^grammar_sequence_right_node_projection },
target: empty_suffix
}
]
)
}

fn body_lowering_match_field_name_spine_does_not_sniff_holds() -> Bool {
!body_lower_match_capture_heads_spine(spine: body_lowering_match_field_name_spine())
}

fn body_lowering_match_spine_identity_absent_dispatch_holds() -> Bool {
let fixture = body_lowering_match_spine_identity_absent_fixture_spine()
if !body_lower_match_capture_heads_spine(spine: fixture) {
Expand Down
37 changes: 37 additions & 0 deletions src/v2/test/claim/body_lowering/data_initializer_fn_value_test.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,37 @@
module v2.test.claim.body_lowering.data_initializer_fn_value

import v2.test.claim.body_lowering.normalize_outcome_helpers {
body_lowering_normalize_outcome
}

data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly

// Cause R: a function value in a data-record field wrapper-retained at admit_normalized_tree
// because dag_surface_arrow_lambda and dag_surface_fn_literal had no producer. The identical
// record literal inside a fn body already accepted. The shells are now structure-preserved after
// the child fold, same door as field_init.
//
// The two data-record claims stay off floor_cost_debt so they remain ordinary-floor
// regression controls for the classifier widening (review 63356).

fn normalize_outcome(src: String) -> String {
body_lowering_normalize_outcome(src: src, file: ^data_initializer_fn_value_subject)
}

data src_data_lambda_field: String = "module m.t\ntype A { meet: fn(Int, Int) -> Int }\ndata d: A = A { meet: (a, b) => a }\n"

data src_data_fn_literal_field: String = "module m.t\ntype A { meet: fn(Int, Int) -> Int }\ndata d: A = A { meet: fn(a, b) { a } }\n"

data src_lambda_in_fn_body: String = "module m.t\ntype A {\n meet: fn(Int, Int) -> Int\n}\nfn f() -> A {\n A {\n meet: (a, b) => a\n }\n}\n"

test fn data_record_arrow_lambda_field_is_not_retained_holds() -> Bool {
normalize_outcome(src: src_data_lambda_field) == "ACCEPTED"
}

test fn data_record_fn_literal_field_is_not_retained_holds() -> Bool {
normalize_outcome(src: src_data_fn_literal_field) == "ACCEPTED"
}

test fn lambda_in_fn_body_control_holds() -> Bool {
normalize_outcome(src: src_lambda_in_fn_body) == "ACCEPTED"
}
53 changes: 53 additions & 0 deletions src/v2/test/claim/body_lowering/match_as_field_name_test.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,53 @@
module v2.test.claim.body_lowering.match_as_field_name

import v2.compiler.body_lowering_fold {
body_lowering_match_field_name_spine_does_not_sniff_holds
}
import v2.test.claim.body_lowering.normalize_outcome_helpers {
body_lowering_normalize_outcome
}

data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly

// Cause F: a field literally named match, accessed as r.match, was sniffed as a
// match-expression because kw_match headed an identity-absent sequence. The sniff now
// requires a following lbrace. r.loop and r.type already accepted; they stay the
// keyword-as-binder control.

fn normalize_outcome(src: String) -> String {
body_lowering_normalize_outcome(src: src, file: ^match_as_field_name_subject)
}

data src_field_named_match: String = "module m.t\ntype R {\n match: Int\n other: Int\n}\nfn f(r: R) -> Int {\n r.match\n}\n"

data src_field_renamed_other: String = "module m.t\ntype R {\n other: Int\n}\nfn f(r: R) -> Int {\n r.other\n}\n"

data src_field_named_loop: String = "module m.t\ntype R {\n loop: Int\n}\nfn f(r: R) -> Int {\n r.loop\n}\n"

data src_field_named_type: String = "module m.t\ntype R {\n type: Int\n}\nfn f(r: R) -> Int {\n r.type\n}\n"

data src_infix_field_named_match: String = "module m.t\ntype R {\n match: Int\n}\nfn f(a: R, b: R) -> Bool {\n a.match == b.match\n}\n"

test fn field_named_match_normalizes_holds() -> Bool {
normalize_outcome(src: src_field_named_match) == "ACCEPTED"
}

test fn field_renamed_other_control_holds() -> Bool {
normalize_outcome(src: src_field_renamed_other) == "ACCEPTED"
}

test fn field_named_loop_control_holds() -> Bool {
normalize_outcome(src: src_field_named_loop) == "ACCEPTED"
}

test fn field_named_type_control_holds() -> Bool {
normalize_outcome(src: src_field_named_type) == "ACCEPTED"
}

test fn infix_field_named_match_normalizes_holds() -> Bool {
normalize_outcome(src: src_infix_field_named_match) == "ACCEPTED"
}

test fn match_keyword_after_dot_is_not_a_match_expr_sniff_holds() -> Bool {
body_lowering_match_field_name_spine_does_not_sniff_holds()
}
25 changes: 25 additions & 0 deletions src/v2/test/claim/body_lowering/normalize_outcome_helpers.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,25 @@
module v2.test.claim.body_lowering.normalize_outcome_helpers

import v2.compiler.normalize { normalize }
import v2.compiler.parse { parse_module }
import v2.compiler.tokenize { tokenize }
import v2.extdeps.languages.dag { dag_language_model }
import v2.std.compilers.lexing { symbol_lexeme }
import v2.std.diagnostic { Accepted, Rejected }
import v2.std.node { Symbol }

fn body_lowering_normalize_outcome(src: String, file: Symbol) -> String {
let lm = dag_language_model()
match tokenize(text: src, file: file, rules: lm.lex) {
Rejected { diagnostics: _ } => "TOKENIZE_REFUSED"
Accepted { value: ts, diagnostics: _ } =>
match parse_module(tokens: ts, grammar: lm.grammar) {
Rejected { diagnostics: _ } => "PARSE_REFUSED"
Accepted { value: artifact, diagnostics: _ } =>
match normalize(parse_tree: artifact.tree) {
Rejected { diagnostics: ds } => symbol_lexeme(sym: ds.head.reason)
Accepted { value: _, diagnostics: _ } => "ACCEPTED"
}
}
}
}
Loading
Loading