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
122 changes: 59 additions & 63 deletions src/v2/compiler/body_lowering_fold.dag
Original file line number Diff line number Diff line change
Expand Up @@ -3620,7 +3620,7 @@ fn body_lower_value_lowered(node: Node) -> Outcome<Optional<Node>> {
outcome_with_diagnostics(value: optional_present(value: lowered), diagnostics: d)
Absent => body_lower_body_subtree_lower(captured: raw)
}
Rejected { diagnostics: _ } => body_lower_body_subtree_lower(captured: raw)
Rejected { diagnostics: r } => Rejected { diagnostics: r }
}
}
}
Expand Down Expand Up @@ -4965,6 +4965,32 @@ fn body_lower_pattern_lowered(pattern_capture: Node) -> Outcome<Node> {
}
}

// ONE ARM-BODY READER FOR EVERY ARM POSITION. An arm body is a value, so it is read by
// body_lower_value_lowered, whose refusal is carried with its own cause and locus; only a body that
// reader returns Absent for falls to the operand reader. The sequence and spine navigations used to
// differ here: the spine arms (every arm the sequence capture does not reach) went to the operand
// reader alone, so a refused value came back Absent and surfaced as match_arm_navigation_refused
// with the arm as its only locus.
fn body_lower_match_arm_wired(pat_node: Node, body_capture: Node, arm_capture: Node) -> Outcome<Node> {
match body_lower_value_lowered(node: body_capture) {
Rejected { diagnostics: r } => Rejected { diagnostics: r }
Accepted { value: lowered_opt, diagnostics: d } =>
match lowered_opt {
Present { value: body } =>
outcome_with_diagnostics(
value: body_lower_match_arm_wire(pat_node: pat_node, body: body),
diagnostics: d
)
Absent =>
match body_lower_match_arm_body_optional(body_capture: body_capture) {
Present { value: body } =>
outcome_accepted(value: body_lower_match_arm_wire(pat_node: pat_node, body: body))
Absent => body_lower_match_arm_navigation_reject(arm_capture: arm_capture)
}
}
}
}

// THE ARM BODY IS LOWERED BY THE BODY WALKER FIRST. The arm-body reader
// (body_lower_match_arm_body_optional) is an operand reader: it answers a nested `match` or `if`
// in arm position with that form's first atom (`dag_token_kw_if`), which is how every arm of
Expand All @@ -4982,25 +5008,11 @@ fn body_lower_match_arm_wire_from_sequence(stripped: Node) -> Outcome<Node> {
Accepted { value: pat_node, diagnostics: _ } =>
match body_lower_match_arm_body_capture_optional(stripped: stripped) {
Present { value: body_capture } =>
match body_lower_value_lowered(node: body_capture) {
Rejected { diagnostics: r } => Rejected { diagnostics: r }
Accepted { value: lowered_opt, diagnostics: d } =>
match lowered_opt {
Present { value: body } =>
outcome_with_diagnostics(
value: body_lower_match_arm_wire(pat_node: pat_node, body: body),
diagnostics: d
)
Absent =>
match body_lower_match_arm_body_optional(body_capture: body_capture) {
Present { value: body } =>
outcome_accepted(
value: body_lower_match_arm_wire(pat_node: pat_node, body: body)
)
Absent => body_lower_match_arm_navigation_reject(arm_capture: stripped)
}
}
}
body_lower_match_arm_wired(
pat_node: pat_node,
body_capture: body_capture,
arm_capture: stripped
)
Absent => body_lower_match_arm_navigation_reject(arm_capture: stripped)
}
}
Expand All @@ -5018,19 +5030,11 @@ fn body_lower_match_arm_wire_from_sequence(stripped: Node) -> Outcome<Node> {
if arrow == ^dag_token_fat_arrow {
match body_lower_match_spine_right(spine: right) {
Present { value: body_capture } =>
match body_lower_match_arm_body_optional(
body_capture: body_capture
) {
Present { value: body } =>
outcome_accepted(
value: body_lower_match_arm_wire(
pat_node: pat_node,
body: body
)
)
Absent =>
body_lower_match_arm_navigation_reject(arm_capture: stripped)
}
body_lower_match_arm_wired(
pat_node: pat_node,
body_capture: body_capture,
arm_capture: stripped
)
Absent =>
body_lower_match_arm_navigation_reject(arm_capture: stripped)
}
Expand All @@ -5045,19 +5049,11 @@ fn body_lower_match_arm_wire_from_sequence(stripped: Node) -> Outcome<Node> {
match node_atom_identity_optional(node: after_pattern.left) {
Present { value: arrow } =>
if arrow == ^dag_token_fat_arrow {
match body_lower_match_arm_body_optional(
body_capture: after_pattern.right
) {
Present { value: body } =>
outcome_accepted(
value: body_lower_match_arm_wire(
pat_node: pat_node,
body: body
)
)
Absent =>
body_lower_match_arm_navigation_reject(arm_capture: stripped)
}
body_lower_match_arm_wired(
pat_node: pat_node,
body_capture: after_pattern.right,
arm_capture: stripped
)
} else {
body_lower_match_arm_navigation_reject(arm_capture: stripped)
}
Expand All @@ -5083,25 +5079,25 @@ fn body_lower_is_match_arm_navigate_emitted(emitted: Symbol) -> Bool {
|| body_lower_is_pass_through_emitted(emitted: emitted)
}

fn body_lower_match_arm_from_comma_repeat_elem(repeat_elem: Node) -> Outcome<Node> {
let stripped = body_lower_deep_unwrap_optional(node: repeat_elem)
match sugar_sequence_pair_optional(node: stripped) {
Present { value: pair } =>
body_lower_wire_match_arm_capture(
arm_capture: body_lower_postfix_optional_unwrap(node: pair.right)
)
Absent =>
body_lower_wire_match_arm_capture(arm_capture: stripped)
}
}

// AN ARM, OR A COMMA-REPEAT ELEMENT CARRYING ONE, DECIDED BY SHAPE BEFORE ANY ARM IS WIRED. A
// repeat element is Seq(optional-comma, arm), and its left side is a separator
// (body_lower_match_arm_repeat_elem_is_separator); an arm's left side is its pattern, which never
// is. The arm is wired once and its Rejected stands. This reader used to wire the node as an arm
// first and, on ANY refusal, discard the diagnostics and retry it as a repeat element: an arm that
// refused for its own located cause (a list literal in its body) was re-read under the wrong shape
// and surfaced as match_arm_navigation_refused with the arm as its only locus.
fn body_lower_extract_comma_list_arm_head(node: Node) -> Outcome<Node> {
let stripped = body_lower_deep_unwrap_optional(node: node)
match body_lower_wire_match_arm_capture(arm_capture: stripped) {
Rejected { diagnostics: _ } =>
body_lower_match_arm_from_comma_repeat_elem(repeat_elem: stripped)
Accepted { value: arm, diagnostics: d } =>
Accepted { value: arm, diagnostics: d }
match sugar_sequence_pair_optional(node: stripped) {
Present { value: pair } =>
if body_lower_match_arm_repeat_elem_is_separator(node: pair.left) {
body_lower_wire_match_arm_capture(
arm_capture: body_lower_postfix_optional_unwrap(node: pair.right)
)
} else {
body_lower_wire_match_arm_capture(arm_capture: stripped)
}
Absent => body_lower_wire_match_arm_capture(arm_capture: stripped)
}
}

Expand Down
185 changes: 185 additions & 0 deletions src/v2/test/claim/namespace_xl0/match_arm_refusal_carried_test.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,185 @@
module v2.test.claim.namespace_xl0.match_arm_refusal_carried

import v2.compiler.compile { NativeTestContext, native_test_context_from_ingest }
import v2.compiler.source_authority { DagSourceReadWitness, SourceRootIngest }
import v2.std.algebra { fold_list }
import v2.std.artifact { Artifact, SourceFile }
import v2.std.cross_tree.import_model { DagTree }
import v2.std.diagnostic { Accepted, Rejected }
import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly }
import v2.std.logic { Bool }
import v2.std.node { Symbol }
import v2.std.optional { Absent, Optional, Present, optional_absent, optional_present }
import v2.std.text { String }
import std.algebra { Cons, Empty }
import extdeps.communication.medium { Lossless, Medium }

data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly

// AN ARM THAT REFUSES FOR ITS OWN CAUSE KEEPS THAT CAUSE, IN EVERY ARM POSITION.
//
// THE SUBJECT IS THE NATIVE LANE'S FRONT END: which fatal cause a module's file refusal carries.
// v2.compiler.body_lowering_fold body_lower_extract_comma_list_arm_head used to wire a repeat
// element as an arm and, on ANY refusal, discard the diagnostics and retry the same node as a
// comma-repeat element. The first arm does not pass through that reader, so a list literal there
// refused located; in the second arm, or in a comma-separated arm, the list literal's own refusal
// was discarded and the retry under the wrong shape answered body_lowering_reason_match_arm_navigation_refused
// with the arm as its only locus. The reader now decides the shape first (a separator on the left is
// a repeat element; an arm's left is its pattern) and wires the arm once, so its Rejected stands.
//
// The two red modules are a list literal in a second arm, on its own line and comma-separated.
// The controls: the same literal in the FIRST arm refuses located on both sides; and the same two
// layouts with no refusable value are not refused at all, so the shape decision did not stop
// reading ordinary arms.
data marc_second_arm_list_source: String = "module v2.test.marc_second_arm_list\n\nimport v2.std.logic { Bool }\n\nfn marc_g(acc: List<Int>) -> List<Int> { acc }\n\nfn marc_probe(b: Bool, acc: List<Int>) -> List<Int> {\n match b {\n false => acc\n true => marc_g(acc: [])\n }\n}\n"

data marc_comma_arm_list_source: String = "module v2.test.marc_comma_arm_list\n\nimport v2.std.logic { Bool }\n\nfn marc_g(acc: List<Int>) -> List<Int> { acc }\n\nfn marc_probe(b: Bool, acc: List<Int>) -> List<Int> {\n match b { false => acc, true => marc_g(acc: []) }\n}\n"

data marc_first_arm_list_source: String = "module v2.test.marc_first_arm_list\n\nimport v2.std.logic { Bool }\n\nfn marc_g(acc: List<Int>) -> List<Int> { acc }\n\nfn marc_probe(b: Bool, acc: List<Int>) -> List<Int> {\n match b {\n true => marc_g(acc: [])\n false => acc\n }\n}\n"

data marc_second_arm_ctl_source: String = "module v2.test.marc_second_arm_ctl\n\nimport v2.std.logic { Bool }\n\nfn marc_g(acc: List<Int>) -> List<Int> { acc }\n\nfn marc_probe(b: Bool, acc: List<Int>) -> List<Int> {\n match b {\n false => acc\n true => marc_g(acc: acc)\n }\n}\n"

data marc_comma_arm_ctl_source: String = "module v2.test.marc_comma_arm_ctl\n\nimport v2.std.logic { Bool }\n\nfn marc_g(acc: List<Int>) -> List<Int> { acc }\n\nfn marc_probe(b: Bool, acc: List<Int>) -> List<Int> {\n match b { false => acc, true => marc_g(acc: acc) }\n}\n"

fn marc_read(source: String, id: Symbol, unit: Symbol, path: String) -> DagSourceReadWitness {
DagSourceReadWitness {
source: Medium { carried: source, fidelity: Lossless },
artifact: Artifact { kind: SourceFile, id: id, file_path: path },
compilation_unit: unit,
source_root: DagTree
}
}

data marc_ingest: SourceRootIngest = Cons {
head: marc_read(source: marc_second_arm_list_source, id: ^marc_second_arm_list_artifact, unit: ^marc_second_arm_list_cu, path: "src/v2/test/fixture/namespace_xl0/marc_second_arm_list.dag"),
tail: Cons {
head: marc_read(source: marc_comma_arm_list_source, id: ^marc_comma_arm_list_artifact, unit: ^marc_comma_arm_list_cu, path: "src/v2/test/fixture/namespace_xl0/marc_comma_arm_list.dag"),
tail: Cons {
head: marc_read(source: marc_first_arm_list_source, id: ^marc_first_arm_list_artifact, unit: ^marc_first_arm_list_cu, path: "src/v2/test/fixture/namespace_xl0/marc_first_arm_list.dag"),
tail: Cons {
head: marc_read(source: marc_second_arm_ctl_source, id: ^marc_second_arm_ctl_artifact, unit: ^marc_second_arm_ctl_cu, path: "src/v2/test/fixture/namespace_xl0/marc_second_arm_ctl.dag"),
tail: Cons {
head: marc_read(source: marc_comma_arm_ctl_source, id: ^marc_comma_arm_ctl_artifact, unit: ^marc_comma_arm_ctl_cu, path: "src/v2/test/fixture/namespace_xl0/marc_comma_arm_ctl.dag"),
tail: Empty
}
}
}
}
}

// ONE FRONT END FOR EVERY CLAIM. The stored value is one verdict per module: the fatal cause of its
// file refusal, or that it was not refused. No context, Node or closure is kept.
type MarcVerdict
= MarcNotRefused
| MarcFileRefused { fatal_reason: Symbol }

type MarcOutcomes
= MarcContextRefused
| MarcOutcomesDecided {
second_arm_list: MarcVerdict
comma_arm_list: MarcVerdict
first_arm_list: MarcVerdict
second_arm_ctl: MarcVerdict
comma_arm_ctl: MarcVerdict
}

fn marc_verdict_in(context: NativeTestContext, unit: Symbol) -> MarcVerdict {
fold_list(
xs: context.file_refusals,
empty: MarcNotRefused,
cons: fn(acc, refusal) {
if refusal.path == unit { MarcFileRefused { fatal_reason: refusal.fatal_reason } } else { acc }
}
)
}

fn marc_outcomes() -> MarcOutcomes {
match native_test_context_from_ingest(ingest: marc_ingest) {
Rejected { diagnostics: _ } => MarcContextRefused
Accepted { value: context, diagnostics: _ } =>
MarcOutcomesDecided {
second_arm_list: marc_verdict_in(context: context, unit: ^marc_second_arm_list_cu),
comma_arm_list: marc_verdict_in(context: context, unit: ^marc_comma_arm_list_cu),
first_arm_list: marc_verdict_in(context: context, unit: ^marc_first_arm_list_cu),
second_arm_ctl: marc_verdict_in(context: context, unit: ^marc_second_arm_ctl_cu),
comma_arm_ctl: marc_verdict_in(context: context, unit: ^marc_comma_arm_ctl_cu)
}
}
}

// THE CLAIMS ARE RELATIONAL. The subject is that arm POSITION does not change the cause, so the
// second-arm and comma-arm modules must refuse under the SAME cause the first-arm module refuses
// under, and that cause must not be the navigation cause. No claim names the list literal's own
// cause: gunbc#12208 lowers list literals and deletes that cause, and a claim pinned to it would read
// that landing as this defect's return. The specimen is still a list literal because it is the
// shape the corpus specimen (gunbc.accelerator_demo_eval) refused on; if a later change lowers it,
// a_first_arm_specimen_still_refuses_located goes red by name and the specimen value is replaced,
// which is the honest reading rather than the relational claims greening over three accepts.
fn marc_cause(v: MarcVerdict) -> Optional<Symbol> {
match v {
MarcFileRefused { fatal_reason: r } => optional_present(value: r)
MarcNotRefused => optional_absent()
}
}

fn marc_same_located_cause(v: MarcVerdict, first: MarcVerdict) -> Bool {
match marc_cause(v: first) {
Absent => false
Present { value: f } =>
if f == ^body_lowering_reason_match_arm_navigation_refused {
false
} else {
match marc_cause(v: v) {
Present { value: c } => c == f
Absent => false
}
}
}
}

fn marc_is_not_refused(v: MarcVerdict) -> Bool {
match v {
MarcNotRefused => true
MarcFileRefused { fatal_reason: _ } => false
}
}

test fn a_second_arm_refuses_under_the_cause_the_first_arm_reaches() -> Bool {
match marc_outcomes() {
MarcOutcomesDecided { second_arm_list: v, comma_arm_list: _, first_arm_list: f, second_arm_ctl: _, comma_arm_ctl: _ } =>
marc_same_located_cause(v: v, first: f)
MarcContextRefused => false
}
}

test fn a_comma_separated_arm_refuses_under_the_cause_the_first_arm_reaches() -> Bool {
match marc_outcomes() {
MarcOutcomesDecided { second_arm_list: _, comma_arm_list: v, first_arm_list: f, second_arm_ctl: _, comma_arm_ctl: _ } =>
marc_same_located_cause(v: v, first: f)
MarcContextRefused => false
}
}

test fn a_first_arm_specimen_still_refuses_located() -> Bool {
match marc_outcomes() {
MarcOutcomesDecided { second_arm_list: _, comma_arm_list: _, first_arm_list: f, second_arm_ctl: _, comma_arm_ctl: _ } =>
marc_same_located_cause(v: f, first: f)
MarcContextRefused => false
}
}

test fn a_second_arm_with_no_refusable_value_is_not_refused() -> Bool {
match marc_outcomes() {
MarcOutcomesDecided { second_arm_list: _, comma_arm_list: _, first_arm_list: _, second_arm_ctl: v, comma_arm_ctl: _ } =>
marc_is_not_refused(v: v)
MarcContextRefused => false
}
}

test fn a_comma_separated_arm_with_no_refusable_value_is_not_refused() -> Bool {
match marc_outcomes() {
MarcOutcomesDecided { second_arm_list: _, comma_arm_list: _, first_arm_list: _, second_arm_ctl: _, comma_arm_ctl: v } =>
marc_is_not_refused(v: v)
MarcContextRefused => false
}
}
Loading