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
9 changes: 5 additions & 4 deletions dag/gunbc/compiler_frontend_program_status.dag
Original file line number Diff line number Diff line change
Expand Up @@ -315,7 +315,7 @@ fn xl2_prerequisite_standing(p: Xl2Prerequisite) -> Xl2PrerequisiteStanding {
BareFieldTypeVisibility => PrerequisiteDelivered {
owner: decl_ref(module_path: "v2.test.claim.declaring_identity_spelling.production_ingest", decl_name: "a_bare_parameter_type_reaches_and_a_bare_field_type_does_too"),
evidence: Xl2PrerequisiteEvidence { pr: 11574, merge_sha: "b705d17c45" as NonEmptyStr, measured_at: "b705d17c45" as NonEmptyStr },
qualification: "BARE field types only. A QUALIFIED field-type mention is still absent from the census (v2.test.claim.declaring_identity_spelling.production_ingest a_qualified_field_type_mention_is_absent_from_the_census_today), so this does not establish field position as a whole." as NonEmptyStr,
qualification: "BARE field types only. The QUALIFIED form is its own row, QualifiedFieldTypeVisibility (v2.test.claim.declaring_identity_spelling.production_ingest a_qualified_field_type_mention_reaches_the_census_holds); together the two establish field position at reach grain." as NonEmptyStr,
}
WholeTreeResolveCensus => PrerequisiteDelivered {
owner: decl_ref(module_path: "v2.test.claim.native_census.whole_tree_census_resolve", decl_name: "census_unbound_module_is_resolve_refused_holds"),
Expand Down Expand Up @@ -381,9 +381,10 @@ fn xl2_prerequisite_standing(p: Xl2Prerequisite) -> Xl2PrerequisiteStanding {
evidence: Xl2PrerequisiteEvidence { pr: 12297, merge_sha: "0579afae7f" as NonEmptyStr, measured_at: "0579afae7f" as NonEmptyStr },
qualification: "delivered at RESOLVE grain: v2.compiler.resolve resolve_pattern_node_walk recognizes `_` at every pattern depth, so resolve no longer emits a spurious unbound row at `_`; an undeclared name in a wildcard arm's body is still the sole refusal at its own atom (an_undeclared_name_in_a_wildcard_arm_body_is_the_sole_refusal_at_its_atom). NOT claimed: a distinct lowered wildcard form -- none exists, the wildcard reaches resolve as the atom `_` and resolve declines to look it up -- so gunbc.recurring_failure_mode.a_wildcard_match_arm_resolves_as_an_unbound_name stays OPEN until the pattern has its own lowered form." as NonEmptyStr,
}
QualifiedFieldTypeVisibility => PrerequisiteOutstanding {
tracked_by: decl_ref(module_path: "v2.test.claim.declaring_identity_spelling.production_ingest", decl_name: "a_qualified_field_type_mention_is_absent_from_the_census_today"),
why: "a qualified field-type mention is absent from the census: qualification no longer hides a mention (a qualified parameter type reaches, a_qualified_type_position_mention_reaches_the_census_holds), but a record declaration's qualified field type is not grafted into the containment tree, so its import-dependent reference never reaches the residual. BareFieldTypeVisibility bounds itself to bare names for this reason. Tracked by the claim that asserts the absence, which reddens when the mention reaches. No fix has merged." as NonEmptyStr,
QualifiedFieldTypeVisibility => PrerequisiteDelivered {
owner: decl_ref(module_path: "v2.test.claim.declaring_identity_spelling.production_ingest", decl_name: "a_qualified_field_type_mention_reaches_the_census_holds"),
evidence: Xl2PrerequisiteEvidence { pr: 12033, merge_sha: "10e01b1169" as NonEmptyStr, measured_at: "14d58480c9" as NonEmptyStr },
qualification: "delivered SILENTLY and found by execution, not by a fix aimed at it: the row that tracked it asserted the ABSENCE and was red on main 14d58480c9 with nothing restating it. Attributed by stage on the row's own two-module fixtures (a scratch probe, not committed): the parse holds the token, the normalized tree holds the whole qualified spine, and v2.compiler.reference_site_collector collect_reference_sites emits exactly one site for it, as for the qualified parameter-type control. The landing cited is the one whose change the probe points at -- gunbc#12033 lowers record fields into declared field identities, whose field type is read by the same body_lower_type_expr_lowered_optional a parameter type is -- located by git log -S and NOT re-executed at its parent, so it is the likely flip, not a measured one. Claimed at REACH grain: the mention reaches the census; whether it BINDS is the second fact the neighbouring rows leave to declaration grafting." as NonEmptyStr,
}
LoweringOccurrenceProjection => PrerequisiteOutstanding {
tracked_by: decl_ref(module_path: "gunbc.recurring_failure_mode.lowering_rebuilds_an_authored_atom_without_its_occurrence", decl_name: "lowering_rebuilds_an_authored_atom_without_its_occurrence"),
Expand Down
13 changes: 6 additions & 7 deletions dag/test/claim/compiler_frontend_program_status_witness_test.dag
Original file line number Diff line number Diff line change
Expand Up @@ -697,7 +697,7 @@ fn xl2_label_is(p: Xl2Prerequisite, want: Xl2Prerequisite) -> Bool {
xl2_prerequisite_label(p: p) == xl2_prerequisite_label(p: want)
}

test fn xl2_prerequisites_partition_into_fifteen_delivered_and_eight_outstanding() -> Bool {
test fn xl2_prerequisites_partition_into_sixteen_delivered_and_seven_outstanding() -> Bool {
count(xl2_prerequisites) == 23
&& xl2_delivered_by(p: PlainCallArgumentReferenceVisibility, pr: 12108, merge_sha: "b0d307c31b")
&& xl2_delivered_by(p: BareFieldTypeVisibility, pr: 11574, merge_sha: "b705d17c45")
Expand All @@ -717,30 +717,29 @@ test fn xl2_prerequisites_partition_into_fifteen_delivered_and_eight_outstanding
&& xl2_outstanding_tracked_by(p: AsCastOperandLowering, decl_name: "as_cast_has_no_lowered_form")
&& xl2_outstanding_tracked_by(p: ElseLessIfStatementLowering, decl_name: "else_less_if_statement_has_no_lowered_form")
&& xl2_delivered_by(p: WildcardMatchArmResolution, pr: 12297, merge_sha: "0579afae7f")
&& xl2_outstanding_tracked_by(p: QualifiedFieldTypeVisibility, decl_name: "a_qualified_field_type_mention_is_absent_from_the_census_today")
&& xl2_delivered_by(p: QualifiedFieldTypeVisibility, pr: 12033, merge_sha: "10e01b1169")
&& xl2_delivered_by(p: MatchEveryArmLowered, pr: 12383, merge_sha: "8ebd8b671d")
&& xl2_delivered_by(p: EnclosingExpressionLoweredWhole, pr: 12436, merge_sha: "d28bf20f0e")
&& xl2_delivered_by(p: DataInitializerMatchScrutineeLowering, pr: 12510, merge_sha: "b768b0f431")
&& xl2_delivered_by(p: MatchArmStatementBodyLowering, pr: 12510, merge_sha: "b768b0f431")
&& count(xl2_prerequisites_outstanding()) == 8
&& count(xl2_prerequisites_outstanding()) == 7
&& all(xl2_prerequisites_outstanding(),
p => xl2_label_is(p: p, want: OptionalAccessorLocatedRefusal)
|| xl2_label_is(p: p, want: LoweringOccurrenceProjection)
|| xl2_label_is(p: p, want: ListLiteralElementVisibility)
|| xl2_label_is(p: p, want: LambdaArgumentValueLowering)
|| xl2_label_is(p: p, want: CaretSymbolOperandLowering)
|| xl2_label_is(p: p, want: AsCastOperandLowering)
|| xl2_label_is(p: p, want: ElseLessIfStatementLowering)
|| xl2_label_is(p: p, want: QualifiedFieldTypeVisibility))
|| xl2_label_is(p: p, want: ElseLessIfStatementLowering))
&& all(xl2_prerequisites,
p => count(xl2_prerequisites |> filter(q => xl2_prerequisite_label(p: q) == xl2_prerequisite_label(p: p))) == 1)
}

// THE INVARIANT THE PARTITION MUST NOT MOVE: prerequisites are necessary, not sufficient, so
// XL-2 stays NotDerivable and the producer literal stays Unavailable with fifteen of twenty-three delivered
// XL-2 stays NotDerivable and the producer literal stays Unavailable with sixteen of twenty-three delivered
// -- and would stay so with twenty-three of twenty-three, because the producer is its own deliverable.
test fn xl2_stays_not_derivable_with_its_prerequisites_mostly_delivered() -> Bool {
count(xl2_prerequisites |> filter(p => xl2_prerequisite_is_delivered(p: p))) == 15
count(xl2_prerequisites |> filter(p => xl2_prerequisite_is_delivered(p: p))) == 16
&& standing_is(want: ClassNotDerivable, s: stage_status(s: StageXL2RootDeletionRehearsal))
&& match rehearsal_producer_standing() {
RehearsalProducerUnavailable { why: _, cause: _ } => true
Expand Down
Loading
Loading