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
83 changes: 83 additions & 0 deletions src/v3/compiler/src/dag.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1653,6 +1653,10 @@ fn classify_call_argument(
return relation;
}

if let Some(relation) = match_payload_field_projection_descent_relation(dag, param, arg) {
return relation;
}

SubValueRelation::SubValueUnknown
}

Expand Down Expand Up @@ -1729,6 +1733,85 @@ fn match_payload_descent_relation(
None
}

/// Phase-1 broadening Slice 2: classify recursive-call arguments produced by
/// a single `FieldProject` transform whose input is the payload port of a
/// match arm whose scrutinee is the parameter directly. This is the
/// record-payload sibling of [`match_payload_descent_relation`]'s
/// positional-payload case.
///
/// Surface shape:
///
/// ```ignore
/// type EpRec = EpLeaf | EpNode { left: EpRec }
/// fn ep_depth(t: EpRec) -> Int =
/// match t { EpNode { left: l } => ep_depth(l), EpLeaf => 0 }
/// ```
///
/// `lower.rs` lowers `EpNode { left: l }` by allocating a payload binding
/// and synthesizing a `FieldProject { field_label: "left", .. }` transform
/// whose input is the payload port (see `lower_field_projection_from_port`).
/// The recursive call's argument is therefore the projection's output port,
/// not the payload port itself — Slice 1's direct-equality check misses it.
///
/// Same fail-closed discipline + structural-fact derivation as Slice 1.
/// `field_name` here is the `FieldProject.field_label` — already structural,
/// established by the lowering, NOT a user-pattern-binding name. The label
/// must also appear in the variant's `Conj` children (validation; if not, the
/// projection isn't on this variant's payload). Cross-slice invariants
/// preserved: no new `CallPattern` variant, no `TransformNode` widening,
/// fail-closed discipline.
fn match_payload_field_projection_descent_relation(
dag: &Dag,
param: PortId,
arg: PortId,
) -> Option<SubValueRelation> {
let Behavior::Transform(transform) = dag.resolve_producer_opt(&arg)? else {
return None;
};
let TransformTarget::FieldProject { field_label, .. } = &transform.target else {
return None;
};
if transform.inputs.len() != 1 {
return None;
}
let projected_input = transform.inputs[0];

for branch in dag.nodes().iter().filter_map(Behavior::as_branch) {
if branch.input != param {
continue;
}
for path in &branch.paths {
let Some(binding) = &path.binding else {
continue;
};
if binding.payload_port != projected_input {
continue;
}
let facts = variant_structural_facts(dag, &path.pattern)?;
// Validate the projection's structural label appears in the
// resolved variant's Conj field set; otherwise this isn't a
// descent on the variant payload.
let payload_ty = facts
.payload_fields
.iter()
.find(|(label, _)| label == field_label)
.map(|(_, ty)| *ty)?;
let element_type = named_type_name(dag, payload_ty)?;
return Some(SubValueRelation::StrictSubValue {
field: InductiveField {
type_name: facts.type_name,
variant_name: facts.variant_name,
field_name: field_label.clone(),
shape: RecursionShape::DirectRecursion,
element_type,
},
factor: ShrinkFactor::UnitShrink,
});
}
}
None
}

/// Authoritative variant-structural facts derived from a resolved variant
/// declaration. Returns `None` for `UnresolvedVariant` and for `ResolvedVariant`
/// whose parent `Disj` cannot be located by scanning declarations — same
Expand Down
58 changes: 58 additions & 0 deletions src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs
Original file line number Diff line number Diff line change
Expand Up @@ -614,6 +614,64 @@ fn ep_count(xs: EpList) -> Int =
}
}

#[test]
fn e_p_per_call_descent_evidence_classifies_match_field_projection_self_call_as_strict_sub_value() {
// Phase-1 broadening Slice 2 — record-payload sibling of Slice 1.
// For `match t { EpNode { left: l } => ep_depth(l) }`, `lower.rs`
// synthesizes a FieldProject transform between the payload port and the
// user-scope name `l`, so the recursive arg is one indirection beyond the
// payload port that Slice 1's direct-equality check catches.
//
// Same structural-fact discipline as Slice 1: field_name is the
// FieldProject.field_label (the lowered Conj field label, NOT the user's
// `l` binding name), and type_name/variant_name come from the parent-Disj
// lookup of the resolved variant declaration.
let dag = compile_to_dag(
"\
type EpRec = EpLeaf | EpNode { left: EpRec }
fn ep_depth(t: EpRec) -> Int =
match t { EpNode { left: l } => ep_depth(l), EpLeaf => 0 }
",
"e_p_match_field_projection.v3",
)
.expect("recursive record-payload fixture compiles");

let entries = per_call_descent_evidence(&dag);
let depth = entries
.iter()
.find(|entry| entry.caller == "ep_depth" && entry.callee == "ep_depth")
.expect("expected ep_depth self-call evidence in per-call side table");

assert_eq!(depth.evidence.len(), 1);
match &depth.evidence[0] {
SubValueRelation::StrictSubValue { field, factor } => {
assert_eq!(
field.field_name, "left",
"FieldProject.field_label is the variant Conj's structural field name"
);
assert_eq!(
field.variant_name, "EpNode",
"variant_name comes from the parent Disj's variant label"
);
assert_eq!(
field.type_name, "EpRec",
"type_name is the parent Disj declaration name"
);
assert_eq!(
field.element_type, "EpRec",
"element_type is the resolved name of the projected field's type"
);
assert_eq!(
factor,
&ShrinkFactor::UnitShrink,
"record-payload field-projection descent is a unit-shrink: \
one constructor + one field peeled"
);
}
other => panic!("expected StrictSubValue for ep_depth(l), got {other:?}"),
}
}

#[test]
fn e_p_per_call_descent_evidence_fails_closed_for_non_self_call() {
let dag = compile_to_dag(
Expand Down
Loading