Skip to content

Dedup add_lower_bound/add_upper_bound into add_var_bound #4408

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
nitishagar wants to merge 1 commit into
base: main
Choose a base branch
from
+72 −69
Open

Dedup add_lower_bound/add_upper_bound into add_var_bound #4408

Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
141 changes: 72 additions & 69 deletions pyrefly/lib/solver/solver.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2088,24 +2088,59 @@ impl Solver {
Ok(())
}

pub fn add_lower_bound(
/// Shared core of [`Self::add_lower_bound`] (`is_upper == false`) and
/// [`Self::add_upper_bound`] (`is_upper == true`).
///
/// The two public functions are near-perfect mirrors: every divergence is
/// mechanically derivable from `is_upper` — which `Bounds` field is the
/// bound-side vs the opposite-side, the `is_subset` argument order, and the
/// `is_upper` bool threaded through `get_new_bound` (the same idiom
/// [`Self::get_new_bound`] already uses).
///
/// Preserves the two-phase lock pattern of the originals: read under the
/// lock, drop the guard, validate without the lock (the `is_subset` callback
/// recurses into `is_subset_eq` which re-locks `variables`), then re-lock to
/// write. Holding the lock across `is_subset` would deadlock.
fn add_var_bound(
&self,
v: Var,
bound: Type,
is_upper: bool,
is_subset: &mut dyn FnMut(&Type, &Type) -> Result<(), SubsetError>,
) -> Result<(), SubsetError> {
let lock = self.variables.lock();
let e = lock.get(v);
let (first_bound, upper_bound, res, quantified_kind) = match &*e {
// The bound-side field holds bounds on the same side being added; the
// opposite-side field (`bounds.upper` for a lower bound, `bounds.lower`
// for an upper bound) is what the new bound must be consistent with.
let (first_bound, opp_bound, res, quantified_kind) = match &*e {
Variable::Quantified {
quantified: _,
bounds,
}
| Variable::Unwrap(bounds) => (
bounds.lower.first().cloned(),
self.get_current_bound(bounds.upper.clone()),
(if is_upper {
&bounds.upper
} else {
&bounds.lower
})
.first()
.cloned(),
self.get_current_bound(if is_upper {
bounds.lower.clone()
} else {
bounds.upper.clone()
}),
if let Variable::Quantified { quantified, .. } = &*e {
self.validate_bound_consistency(&bound, &bounds.lower, quantified.kind())
self.validate_bound_consistency(
&bound,
if is_upper {
&bounds.upper
} else {
&bounds.lower
},
quantified.kind(),
)
} else {
Ok(())
},
Expand All @@ -2120,7 +2155,17 @@ impl Solver {
drop(e);
drop(lock);
let res = res.and_then(|_| {
upper_bound.map_or(Ok(()), |upper_bound| is_subset(&bound, &upper_bound))
// For a lower bound we check `bound <: opp_bound` (the existing upper
// bound); for an upper bound we check `opp_bound <: bound` (the
// existing lower bound). Either way the new bound must be consistent
// with the opposite-side bound via transitivity.
opp_bound.map_or(Ok(()), |opp_bound| {
if is_upper {
is_subset(&opp_bound, &bound)
} else {
is_subset(&bound, &opp_bound)
}
})
});
let new_bound = match (res.is_ok(), quantified_kind) {
(true, Some(QuantifiedKind::IntVar)) => Some(
Expand All @@ -2129,12 +2174,12 @@ impl Solver {
// `validate_bound_consistency` accepted this bound, so the
// same IntVar normalization must succeed before storing it.
type_as_intvar_solution(&bound)
.expect("successful IntVar lower-bound check must normalize"),
false,
.expect("successful IntVar bound check must normalize"),
is_upper,
is_subset,
),
),
(true, _) => Some(self.get_new_bound(first_bound, bound, false, is_subset)),
(true, _) => Some(self.get_new_bound(first_bound, bound, is_upper, is_subset)),
(false, Some(QuantifiedKind::IntVar)) => None,
(false, _) => {
// TODO(https://github.com/facebook/pyrefly/issues/105): don't throw away the bound.
Expand All @@ -2148,78 +2193,36 @@ impl Solver {
quantified: _,
bounds,
}
| Variable::Unwrap(bounds) => self.add_bound(&mut bounds.lower, new_bound),
| Variable::Unwrap(bounds) => self.add_bound(
if is_upper {
&mut bounds.upper
} else {
&mut bounds.lower
},
new_bound,
),
_ => {}
}
}
res
}

pub fn add_lower_bound(
&self,
v: Var,
bound: Type,
is_subset: &mut dyn FnMut(&Type, &Type) -> Result<(), SubsetError>,
) -> Result<(), SubsetError> {
self.add_var_bound(v, bound, false, is_subset)
}

pub fn add_upper_bound(
&self,
v: Var,
bound: Type,
is_subset: &mut dyn FnMut(&Type, &Type) -> Result<(), SubsetError>,
) -> Result<(), SubsetError> {
let lock = self.variables.lock();
let e = lock.get(v);
let (first_bound, lower_bound, res, quantified_kind) = match &*e {
Variable::Quantified {
quantified: _,
bounds,
}
| Variable::Unwrap(bounds) => (
bounds.upper.first().cloned(),
self.get_current_bound(bounds.lower.clone()),
if let Variable::Quantified { quantified, .. } = &*e {
self.validate_bound_consistency(&bound, &bounds.upper, quantified.kind())
} else {
Ok(())
},
if let Variable::Quantified { quantified, .. } = &*e {
Some(quantified.kind())
} else {
None
},
),
_ => return Ok(()),
};
drop(e);
drop(lock);
let res = res.and_then(|_| {
lower_bound.map_or(Ok(()), |lower_bound| is_subset(&lower_bound, &bound))
});
let new_bound = match (res.is_ok(), quantified_kind) {
(true, Some(QuantifiedKind::IntVar)) => Some(
self.get_new_bound(
first_bound,
// `validate_bound_consistency` accepted this bound, so the
// same IntVar normalization must succeed before storing it.
type_as_intvar_solution(&bound)
.expect("successful IntVar upper-bound check must normalize"),
true,
is_subset,
),
),
(true, _) => Some(self.get_new_bound(first_bound, bound, true, is_subset)),
(false, Some(QuantifiedKind::IntVar)) => None,
(false, _) => {
// TODO(https://github.com/facebook/pyrefly/issues/105): don't throw away the bound.
Some(NewBound::AddBound(Type::any_error()))
}
};
let lock = self.variables.lock();
if let Some(new_bound) = new_bound {
match &mut *lock.get_mut(v) {
Variable::Quantified {
quantified: _,
bounds,
}
| Variable::Unwrap(bounds) => self.add_bound(&mut bounds.upper, new_bound),
_ => {}
}
}
res
self.add_var_bound(v, bound, true, is_subset)
}

/// Get current bound from a set of bounds of an unfinished variable.
Expand Down
Loading