From 4415027f7b98b170a9d0329248cb9580c253407c Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 1 Sep 2026 11:40:45 +0000 Subject: [PATCH] Traverse types once when relating them invariantly Relating two types invariantly was expressed as subtyping in both directions, which walks the whole type structure twice. Each owning or mutable pointer nested inside relates its referent invariantly again, so the number of clauses emitted for a refinement doubled per pointer layer above it: the eight identical clauses per basic block edge in a `&mut self` method over `Option` come from three such layers. The two directions do not derive different constraints. Relating types invariantly is symmetric, and every position below an owning or mutable pointer is related invariantly again, so the second direction re-derives the constraints of the first. Relate types in a single traversal carrying the relation to derive, emitting both implications where the refinements must agree. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01PEtrgExrszb8aBUEGASPeE --- src/rty/subtyping.rs | 203 +++++++++++++++++++++++-------------------- 1 file changed, 110 insertions(+), 93 deletions(-) diff --git a/src/rty/subtyping.rs b/src/rty/subtyping.rs index 03477f02..6c713e0e 100644 --- a/src/rty/subtyping.rs +++ b/src/rty/subtyping.rs @@ -48,13 +48,6 @@ pub trait Subtyping { got: &RefinedType, expected: &RefinedType, ) -> Vec; - - #[must_use] - fn relate_equal_refined_type( - &self, - got: &RefinedType, - expected: &RefinedType, - ) -> Vec; } impl Subtyping for C @@ -66,70 +59,7 @@ where T: chc::Var, U: chc::Var, { - tracing::debug!(got = %got.display(), expected = %expected.display(), "sub_type"); - - let mut clauses = Vec::new(); - match (got, expected) { - (Type::Int, Type::Int) - | (Type::Bool, Type::Bool) - | (Type::String, Type::String) - | (Type::Never, Type::Never) => {} - (Type::Enum(got), Type::Enum(expected)) if got.symbol() == expected.symbol() => { - for (got_ty, expected_ty) in got.args.iter().zip(expected.args.iter()) { - let cs = self.relate_sub_refined_type(got_ty, expected_ty); - clauses.extend(cs); - } - } - (Type::Tuple(got), Type::Tuple(expected)) - if got.elems.len() == expected.elems.len() => - { - for (got_ty, expected_ty) in got.elems.iter().zip(expected.elems.iter()) { - let cs = self.relate_sub_refined_type(got_ty, expected_ty); - clauses.extend(cs); - } - } - (Type::Pointer(got), Type::Pointer(expected)) if got.kind == expected.kind => { - match got.kind { - PointerKind::Ref(RefKind::Immut) => { - let cs = self.relate_sub_refined_type(&got.elem, &expected.elem); - clauses.extend(cs); - } - PointerKind::Own | PointerKind::Ref(RefKind::Mut) => { - let cs = self.relate_equal_refined_type(&got.elem, &expected.elem); - clauses.extend(cs); - } - } - } - (Type::Function(got), Type::Function(expected)) - if got.params.len() == expected.params.len() => - { - let mut builder = chc::ClauseBuilder::default(); - for (param_idx, param_rty) in got.params.iter_enumerated() { - let param_sort = param_rty.ty.to_sort(); - if !param_sort.is_singleton() { - builder.add_mapped_var(param_idx, param_sort); - } - } - for (got_ty, expected_ty) in got.params.iter().zip(expected.params.iter()) { - let cs = builder.relate_sub_refined_type(expected_ty, got_ty); - clauses.extend(cs); - } - let cs = builder.relate_sub_refined_type(&got.ret, &expected.ret); - clauses.extend(cs); - } - (Type::Array(got), Type::Array(expected)) => { - let cs1 = self.relate_sub_refined_type(&got.index, &expected.index); - clauses.extend(cs1); - let cs2 = self.relate_sub_refined_type(&got.elem, &expected.elem); - clauses.extend(cs2); - } - _ => panic!( - "inconsistent types: got={}, expected={}", - got.display(), - expected.display() - ), - } - clauses + relate_type(self, got, expected, Relation::Sub) } fn relate_sub_refined_type( @@ -141,34 +71,121 @@ where T: chc::Var, U: chc::Var, { - tracing::debug!(got = %got.display(), expected = %expected.display(), "sub_refined_type"); + relate_refined_type(self, got, expected, Relation::Sub) + } +} - let mut clauses = self.relate_sub_type(&got.ty, &expected.ty); +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +enum Relation { + Sub, + Equal, +} - let cs = self - .build_clause() - .with_value_var(&got.ty) - .add_body(got.refinement.clone()) - .head(expected.refinement.clone()); - clauses.extend(cs); - clauses +#[must_use] +fn relate_type( + scope: &C, + got: &Type, + expected: &Type, + relation: Relation, +) -> Vec +where + C: ClauseScope, + T: chc::Var, + U: chc::Var, +{ + tracing::debug!(got = %got.display(), expected = %expected.display(), ?relation, "relate_type"); + + let mut clauses = Vec::new(); + match (got, expected) { + (Type::Int, Type::Int) + | (Type::Bool, Type::Bool) + | (Type::String, Type::String) + | (Type::Never, Type::Never) => {} + (Type::Enum(got), Type::Enum(expected)) if got.symbol() == expected.symbol() => { + for (got_ty, expected_ty) in got.args.iter().zip(expected.args.iter()) { + let cs = relate_refined_type(scope, got_ty, expected_ty, relation); + clauses.extend(cs); + } + } + (Type::Tuple(got), Type::Tuple(expected)) if got.elems.len() == expected.elems.len() => { + for (got_ty, expected_ty) in got.elems.iter().zip(expected.elems.iter()) { + let cs = relate_refined_type(scope, got_ty, expected_ty, relation); + clauses.extend(cs); + } + } + (Type::Pointer(got), Type::Pointer(expected)) if got.kind == expected.kind => { + let elem_relation = match got.kind { + PointerKind::Ref(RefKind::Immut) => relation, + PointerKind::Own | PointerKind::Ref(RefKind::Mut) => Relation::Equal, + }; + let cs = relate_refined_type(scope, &got.elem, &expected.elem, elem_relation); + clauses.extend(cs); + } + (Type::Function(got), Type::Function(expected)) + if got.params.len() == expected.params.len() => + { + let mut builder = chc::ClauseBuilder::default(); + for (param_idx, param_rty) in got.params.iter_enumerated() { + let param_sort = param_rty.ty.to_sort(); + if !param_sort.is_singleton() { + builder.add_mapped_var(param_idx, param_sort); + } + } + for (got_ty, expected_ty) in got.params.iter().zip(expected.params.iter()) { + let cs = relate_refined_type(&builder, expected_ty, got_ty, relation); + clauses.extend(cs); + } + let cs = relate_refined_type(&builder, &got.ret, &expected.ret, relation); + clauses.extend(cs); + } + (Type::Array(got), Type::Array(expected)) => { + let cs1 = relate_refined_type(scope, &got.index, &expected.index, relation); + clauses.extend(cs1); + let cs2 = relate_refined_type(scope, &got.elem, &expected.elem, relation); + clauses.extend(cs2); + } + _ => panic!( + "inconsistent types: got={}, expected={}", + got.display(), + expected.display() + ), } + clauses +} - fn relate_equal_refined_type( - &self, - got: &RefinedType, - expected: &RefinedType, - ) -> Vec - where - T: chc::Var, - U: chc::Var, - { - tracing::debug!(got = %got.display(), expected = %expected.display(), "equal_refined_type"); +#[must_use] +fn relate_refined_type( + scope: &C, + got: &RefinedType, + expected: &RefinedType, + relation: Relation, +) -> Vec +where + C: ClauseScope, + T: chc::Var, + U: chc::Var, +{ + tracing::debug!(got = %got.display(), expected = %expected.display(), ?relation, "relate_refined_type"); + + let mut clauses = relate_type(scope, &got.ty, &expected.ty, relation); - let mut clauses = self.relate_sub_refined_type(got, expected); - clauses.extend(self.relate_sub_refined_type(expected, got)); - clauses + let cs = scope + .build_clause() + .with_value_var(&got.ty) + .add_body(got.refinement.clone()) + .head(expected.refinement.clone()); + clauses.extend(cs); + + if relation == Relation::Equal { + let cs = scope + .build_clause() + .with_value_var(&expected.ty) + .add_body(expected.refinement.clone()) + .head(got.refinement.clone()); + clauses.extend(cs); } + + clauses } #[must_use]