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
25 changes: 25 additions & 0 deletions dag/test/claim/fn_equality_bound_witness_test.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,25 @@
module test.claim.fn_equality_bound_witness

import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly }

data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly

data fn_equality_bound_witness_note: String = "Executing floor witness for the FN-level PartialEq bound trigger (v1.compiler.emit_rust v1_fn_body_equality_bound_param_names, deciding via v1.compiler.trait_bound_witness v1_equality_bound_param_name). The emitter derives Clone bounds on generic fn params ~30-48 references deep but derived NOTHING for equality, so a generic fn comparing two values of its own type param emitted bare and rustc refused with E0369 'binary operation == cannot be applied to type K'. GROUNDING FOR THE EXPECTED SPELLING, so it is not a measurement copied from this tree: quick-lynx-620 measured the requirement against rustc on the real emission -- hand-adding the bound to the emitted mirror and rebuilding the seed gave zero errors, and the required rendering is `K: Clone + PartialEq`, the equality bound COMPOSING with the separately-derived Clone bound on the same parameter rather than replacing it. THE DISCRIMINATOR IS TYPE RESOLUTION, NOT THE == SPELLING, and the two rows below exist to prove the trigger cannot be satisfied by matching on the operator. earning_comparison_bounds_its_generic_param carries BOTH comparisons in one body, exactly the shape of the real specimen: a concrete closed-enum comparison that must earn nothing, and a comparison of two K values that must earn the bound -- rustc emits exactly ONE E0369 on that real shape, at the second comparison, so the first provably compiles unbounded today. concrete_only_comparison_leaves_generic_param_bare is the sharper negative: a fn that HAS a generic param and HAS a comparison, where the comparison involves only concrete types. A predicate keyed on the presence of == bounds K there and breaks every caller instantiating K with a non-PartialEq type; the type-resolving predicate must leave it bare. That row is what makes the pair discriminating rather than two positives, and it is why the refusals below assert the bounded spelling is ABSENT rather than merely asserting some other spelling is present. Over-approximation is not free here: adding a bound TIGHTENS the emitted signature, so a spurious bound is a real break, while a missed bound only leaves the pre-existing E0369 in place."

fn earning_comparison_bounds_its_generic_param() -> Bool {
compile_dag_rust_emit_check(
"module fn_equality_witness.earning\n\ntype ShapeTag = ShapeAlpha | ShapeBeta\n\ntype CapRow<K> {\n shape: ShapeTag\n keys: List<K>\n}\n\nfn cap_row_has<K>(row: CapRow<K>, shape: ShapeTag, key: K) -> Bool {\n row.shape == shape && (row.keys |> any(k => k == key))\n}\n",
"src/fn_equality_witness_earning.rs",
["fn cap_row_has<K: Clone + PartialEq>"],
["fn cap_row_has<K>", "fn cap_row_has<K: Clone>"]
)
}

fn concrete_only_comparison_leaves_generic_param_bare() -> Bool {
compile_dag_rust_emit_check(
"module fn_equality_witness.concrete\n\ntype ShapeTag = ShapeAlpha | ShapeBeta\n\ntype CapRow<K> {\n shape: ShapeTag\n keys: List<K>\n}\n\nfn cap_row_shape_is<K>(row: CapRow<K>, shape: ShapeTag) -> Bool {\n row.shape == shape\n}\n",
"src/fn_equality_witness_concrete.rs",
["fn cap_row_shape_is"],
["K: PartialEq", "K: Clone + PartialEq"]
)
}
102 changes: 97 additions & 5 deletions src/v1/05_emit_rust.dag
Original file line number Diff line number Diff line change
Expand Up @@ -63,7 +63,7 @@ import v1.compiler.trait_derive_emit {
v1_emit_enum_derives,
v1_emit_struct_from_capability_table, v1_emit_enum_supplemental_impls,
v1_generic_params_needing_clone_bound,
v1_emit_type_params_with_clone_bounds,
v1_emit_type_params_with_clone_bounds, v1_emit_type_params_with_bounds,
v1_clone_bounded_type_params, v1_item_clone_bounded_param_names, v1_item_clone_undecided_head,
v1_map_key_required_type_names, v1_item_field_type_exprs, v1_with_map_key_requirement,
v1_clone_impl_required_type_params,
Expand All @@ -73,7 +73,8 @@ import v1.compiler.trait_derive_emit {
}
import v1.compiler.trait_bound_witness {
v1_rc_match_scrutinee_clone_bound_param_names, v1_union_clone_param_names,
v1_call_forwarding_clone_bound_wrapper_param_names
v1_call_forwarding_clone_bound_wrapper_param_names,
v1_equality_bound_param_name
}

import std.types { is_container_type, is_kernel_type, container_template_algebra }
Expand Down Expand Up @@ -5969,6 +5970,88 @@ fn v1_fn_body_derived_clone_param_names(params: List<Node>, inferred: Node, body
)
}

// Joins the two derivations onto one per-param trait list so a param earning both renders
// `K: Clone + PartialEq`. Clone is listed first so the Clone-only case is byte-identical to what
// the previous single-trait renderer emitted, which is what lets the regen fixed point act as the
// oracle for "equality changed nothing that did not need changing".
fn v1_fn_bounds_by_param(
clone_param_names: List<String>,
eq_param_names: List<String>
) -> Map<String, List<String>> {
let with_clone = clone_param_names |> fold(init: empty_map(), f: (m, n) => map_insert(m, n, ["Clone"]))
eq_param_names |> fold(init: with_clone, f: (m, n) =>
match map_get(m, n) {
Present { value: traits } => map_insert(m, n, concat(traits, ["PartialEq"]))
Absent => map_insert(m, n, ["PartialEq"])
}
)
}

// Node-consuming extraction for the equality bound, kept here rather than in
// v1.compiler.trait_bound_witness for the reason that module's import note gives: the pure core
// lives there, the Node walk lives at the call site, and reversing that would close an
// emit_rust -> trait_bound_witness -> emit_rust cycle.
//
// This is the RECURSIVE BODY WALKER that BoundedToDirectTopLevelMatchBody and
// BoundedToDirectSingleCallLambdaBody both name as their next-rung trigger. Unlike those two it
// declares no depth boundary: the specimen that motivated it puts the earning comparison inside a
// lambda, inside any(), inside a pipeline, inside the && of another lambda inside another any().
//
// The traversal is deliberately GENEROUS and the predicate deliberately EXACT, because the two
// directions have asymmetric cost. binop_left/binop_right are children 0 and 1, so descending
// every child reaches every operand; a node the walk somehow misses simply yields no bound, which
// is the status quo. But a spurious bound tightens the emitted signature and breaks callers, so
// precision must come from v1_equality_bound_param_name's type resolution, never from the shape of
// the walk.
fn v1_fn_body_equality_bound_param_names(
body: Node,
generic_param_names: List<String>,
source_indices: Map<String, NewlineIndex>
) -> List<String> {
let here = match body.expr_data {
ExprBinOp { op: op, algebra_field: _ } =>
if is_equality_comparison(op: op) {
v1_equality_bound_param_name(
left_type_name: v1_resolved_type_name_or_empty(e: binop_left(texpr: body), source_indices: source_indices),
right_type_name: v1_resolved_type_name_or_empty(e: binop_right(texpr: body), source_indices: source_indices),
generic_param_names: generic_param_names
)
} else {
[]
}
_ => []
}
body.children |> fold(init: here, f: (acc, child) =>
v1_union_clone_param_names(
base: acc,
extra: v1_fn_body_equality_bound_param_names(
body: child,
generic_param_names: generic_param_names,
source_indices: source_indices
)
)
)
}

// Matches Eq/Ne bare exactly as is_string_comparison does in this module. The operator is genuinely
// a spelling, so reading it as one is correct; it is the OPERANDS that must be resolved by type.
fn is_equality_comparison(op: BinOp) -> Bool {
match op {
Eq => true
Ne => true
_ => false
}
}

// Empty string means "no resolved type", which is why v1_equality_bound_param_name refuses on it
// rather than letting two unresolved operands compare equal and fabricate a bound.
fn v1_resolved_type_name_or_empty(e: Node, source_indices: Map<String, NewlineIndex>) -> String {
match e.inferred {
Present { value: Resolved { node: rt } } => authored_name_at(source_indices: source_indices, node: rt)
_ => ""
}
}

fn v1_call_forwarding_clone_bound_param_names(
generic_param_names: List<String>,
body: Node,
Expand Down Expand Up @@ -6099,9 +6182,18 @@ fn emit_fn_def(name: String, params: List<Node>, inferred: Node, body: Node, reg
} else {
derived_clone_param_names_with_rc_match
}
let needs_clone_bound = (clone_param_names |> count) > 0
let type_params_str = if needs_clone_bound {
v1_emit_type_params_with_clone_bounds(params: type_params, clone_param_names: clone_param_names, source_indices: si)
let eq_param_names = v1_fn_body_equality_bound_param_names(
body: body,
generic_param_names: generic_param_names,
source_indices: si
)
let bounds_by_param = v1_fn_bounds_by_param(
clone_param_names: clone_param_names,
eq_param_names: eq_param_names
)
let needs_bound = (clone_param_names |> count) > 0 || (eq_param_names |> count) > 0
let type_params_str = if needs_bound {
v1_emit_type_params_with_bounds(params: type_params, bounds_by_param: bounds_by_param, source_indices: si)
} else {
emit_type_params(params: type_params, source_indices: si)
}
Expand Down
118 changes: 109 additions & 9 deletions src/v1/stage0/src/v1_compiler_emit_rust.rs
Original file line number Diff line number Diff line change
Expand Up @@ -118,17 +118,17 @@ pub use crate::v1_compiler_ownership::{
pub use crate::v1_compiler_resolve::get_exported_names;
pub use crate::v1_compiler_runtime_rust::rust_runtime_source;
pub use crate::v1_compiler_trait_bound_witness::{
v1_call_forwarding_clone_bound_wrapper_param_names,
v1_call_forwarding_clone_bound_wrapper_param_names, v1_equality_bound_param_name,
v1_rc_match_scrutinee_clone_bound_param_names, v1_union_clone_param_names,
};
pub use crate::v1_compiler_trait_derive_emit::{
rust_nominal_identity_carrier_shape_eligible, rust_symbol_wrapped_ord_carrier_shape_eligible,
trait_derive_emit_fn_clone_bound_keyed_carrier_module, v1_clone_bounded_type_params,
v1_clone_impl_required_type_params, v1_emit_enum_derives, v1_emit_enum_supplemental_impls,
v1_emit_struct_from_capability_table, v1_emit_type_params_with_clone_bounds,
v1_generic_params_needing_clone_bound, v1_item_clone_bounded_param_names,
v1_item_clone_undecided_head, v1_item_field_type_exprs, v1_map_key_required_type_names,
v1_trait_derive_refuse, v1_with_map_key_requirement,
v1_emit_struct_from_capability_table, v1_emit_type_params_with_bounds,
v1_emit_type_params_with_clone_bounds, v1_generic_params_needing_clone_bound,
v1_item_clone_bounded_param_names, v1_item_clone_undecided_head, v1_item_field_type_exprs,
v1_map_key_required_type_names, v1_trait_derive_refuse, v1_with_map_key_requirement,
};
use crate::v1_rt;
use crate::v1_rt::{VecCompat, VecJoin};
Expand Down Expand Up @@ -14888,6 +14888,98 @@ pub fn v1_fn_body_derived_clone_param_names(
}
}

pub fn v1_fn_bounds_by_param(
clone_param_names: Rc<Vec<String>>,
eq_param_names: Rc<Vec<String>>,
) -> Rc<HashMap<String, Rc<Vec<String>>>> {
{
let with_clone = clone_param_names.clone().iter().cloned().fold(
v1_rt::rc_empty_map::<String, Rc<Vec<String>>>(),
|m: Rc<HashMap<String, Rc<Vec<String>>>>, n: String| {
v1_rt::rc_map_insert(m, n.clone(), Rc::new(vec!["Clone".to_string()]))
},
);
eq_param_names.clone().iter().cloned().fold(
with_clone.clone(),
|m: Rc<HashMap<String, Rc<Vec<String>>>>, n: String| match v1_rt::map_get(&m, n.clone())
{
Some(traits) => v1_rt::rc_map_insert(
m.clone(),
n.clone(),
v1_rt::concat(traits.clone(), Rc::new(vec!["PartialEq".to_string()])),
),
None => v1_rt::rc_map_insert(
m.clone(),
n.clone(),
Rc::new(vec!["PartialEq".to_string()]),
),
},
)
}
}

pub fn v1_fn_body_equality_bound_param_names(
body: Rc<Node>,
generic_param_names: Rc<Vec<String>>,
source_indices: Rc<HashMap<String, Rc<NewlineIndex>>>,
) -> Rc<Vec<String>> {
stacker::maybe_grow(512 * 1024, 2 * 1024 * 1024, || {
let here = match (*body.expr_data.clone()).clone() {
ExprData::ExprBinOp { op, .. } => {
if is_equality_comparison(op.clone()) {
v1_equality_bound_param_name(
v1_resolved_type_name_or_empty(
binop_left(body.clone()),
source_indices.clone(),
),
v1_resolved_type_name_or_empty(
binop_right(body.clone()),
source_indices.clone(),
),
generic_param_names.clone(),
)
} else {
Rc::new(vec![])
}
}
_ => Rc::new(vec![]),
};
body.children.clone().iter().cloned().fold(
here.clone(),
|acc: Rc<Vec<String>>, child: Rc<Node>| {
v1_union_clone_param_names(
acc,
v1_fn_body_equality_bound_param_names(
child.clone(),
generic_param_names.clone(),
source_indices.clone(),
),
)
},
)
})
}

pub fn is_equality_comparison(op: BinOp) -> bool {
match op.clone() {
BinOp::Eq => true,
BinOp::Ne => true,
_ => false,
}
}

pub fn v1_resolved_type_name_or_empty(
e: Rc<Node>,
source_indices: Rc<HashMap<String, Rc<NewlineIndex>>>,
) -> String {
match e.inferred.clone().as_deref().cloned() {
Some(InferredNode::Resolved { node: rt, .. }) => {
authored_name_at(source_indices.clone(), rt.clone())
}
_ => "".to_string(),
}
}

pub fn v1_call_forwarding_clone_bound_param_names(
generic_param_names: Rc<Vec<String>>,
body: Rc<Node>,
Expand Down Expand Up @@ -15074,11 +15166,19 @@ pub fn emit_fn_def(
} else {
derived_clone_param_names_with_rc_match.clone()
};
let needs_clone_bound = ((clone_param_names.clone().len() as i64) > 0);
let type_params_str = if needs_clone_bound.clone() {
v1_emit_type_params_with_clone_bounds(
let eq_param_names = v1_fn_body_equality_bound_param_names(
body.clone(),
generic_param_names.clone(),
si.clone(),
);
let bounds_by_param =
v1_fn_bounds_by_param(clone_param_names.clone(), eq_param_names.clone());
let needs_bound = (((clone_param_names.clone().len() as i64) > 0)
|| ((eq_param_names.clone().len() as i64) > 0));
let type_params_str = if needs_bound.clone() {
v1_emit_type_params_with_bounds(
type_params.clone(),
clone_param_names.clone(),
bounds_by_param.clone(),
si.clone(),
)
} else {
Expand Down
25 changes: 25 additions & 0 deletions src/v1/stage0/src/v1_compiler_trait_bound_witness.rs
Original file line number Diff line number Diff line change
Expand Up @@ -222,6 +222,31 @@ pub fn v1_call_forwarding_clone_bound_wrapper_param_names(
}
}

pub fn v1_equality_bound_param_name(
left_type_name: String,
right_type_name: String,
generic_param_names: Rc<Vec<String>>,
) -> Rc<Vec<String>> {
if ((left_type_name.clone() == "".to_string()) || (right_type_name.clone() == "".to_string())) {
Rc::new(vec![])
} else {
if ((left_type_name.clone() == right_type_name.clone()) && {
let mut __found = false;
for g in generic_param_names.clone().iter().cloned() {
if (g.clone() == left_type_name.clone()) {
__found = true;
break;
}
}
__found
}) {
Rc::new(vec![left_type_name.clone()])
} else {
Rc::new(vec![])
}
}
}

#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)]
pub struct BoundedToDirectTopLevelMatchBody;
#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)]
Expand Down
42 changes: 29 additions & 13 deletions src/v1/stage0/src/v1_compiler_trait_derive_emit.rs
Original file line number Diff line number Diff line change
Expand Up @@ -2693,9 +2693,9 @@ pub fn v1_item_clone_bounded_param_names(
}
}

pub fn v1_emit_type_params_with_clone_bounds(
pub fn v1_emit_type_params_with_bounds(
params: Rc<Vec<Rc<Node>>>,
clone_param_names: Rc<Vec<String>>,
bounds_by_param: Rc<HashMap<String, Rc<Vec<String>>>>,
source_indices: Rc<HashMap<String, Rc<NewlineIndex>>>,
) -> String {
if ((params.clone().len() as i64) == 0) {
Expand All @@ -2708,19 +2708,18 @@ pub fn v1_emit_type_params_with_clone_bounds(
__result.push({
let pname = generic_param_name_at(p.clone(), source_indices.clone());
let pascal = to_pascal(pname.clone());
if {
let mut __found = false;
for c in clone_param_names.clone().iter().cloned() {
if (c.clone() == pname.clone()) {
__found = true;
break;
match v1_rt::map_get(&bounds_by_param, pname.clone()) {
Some(traits) => {
if ((traits.clone().len() as i64) == 0) {
pascal.clone()
} else {
v1_rt::concat(
v1_rt::concat(pascal.clone(), ": ".to_string()),
traits.clone().join(&" + ".to_string()),
)
}
}
__found
} {
v1_rt::concat(pascal.clone(), ": Clone".to_string())
} else {
pascal.clone()
None => pascal.clone(),
}
});
}
Expand All @@ -2734,6 +2733,23 @@ pub fn v1_emit_type_params_with_clone_bounds(
}
}

pub fn v1_emit_type_params_with_clone_bounds(
params: Rc<Vec<Rc<Node>>>,
clone_param_names: Rc<Vec<String>>,
source_indices: Rc<HashMap<String, Rc<NewlineIndex>>>,
) -> String {
v1_emit_type_params_with_bounds(
params.clone(),
clone_param_names.clone().iter().cloned().fold(
v1_rt::rc_empty_map::<String, Rc<Vec<String>>>(),
|m: Rc<HashMap<String, Rc<Vec<String>>>>, n: String| {
v1_rt::rc_map_insert(m, n.clone(), Rc::new(vec!["Clone".to_string()]))
},
),
source_indices.clone(),
)
}

pub fn v1_emit_struct_from_capability_table(
module_path: String,
name: String,
Expand Down
Loading