Skip to content
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

Merge tys and fun_args in Sub #958

Merged
merged 1 commit into from
Dec 21, 2024
Merged

Merge tys and fun_args in Sub #958

Show file tree
Hide file tree
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
121 changes: 68 additions & 53 deletions crates/flux-infer/src/infer.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -462,27 +462,31 @@ impl InferCtxtAt<'_, '_, '_, '_> {
Ok(())
}

/// Relate types via subtyping for a function call. This is the same as [`InferCtxtAt::subtyping`]
/// except that we also consider strong references.
pub fn fun_arg_subtyping(
/// Relate types via subtyping. This is the same as [`InferCtxtAt::subtyping`] except that we
/// also require a [`LocEnv`] to handle pointers and strong references
pub fn subtyping_with_env(
&mut self,
env: &mut impl LocEnv,
a: &Ty,
b: &Ty,
reason: ConstrReason,
) -> InferResult {
let mut sub = Sub::new(reason, self.span);
sub.fun_args(self.infcx, env, a, b)
let mut sub = Sub::new(env, reason, self.span);
sub.tys(self.infcx, a, b)
}

/// Relate types via subtyping and returns coroutine obligations. See comment for [`Sub::obligations`].
/// Relate types via subtyping and returns coroutine obligations. This doesn't handle subtyping
/// when strong references are involved.
///
/// See comment for [`Sub::obligations`].
pub fn subtyping(
&mut self,
a: &Ty,
b: &Ty,
reason: ConstrReason,
) -> InferResult<Vec<Binder<rty::CoroutineObligPredicate>>> {
let mut sub = Sub::new(reason, self.span);
let mut env = DummyEnv;
let mut sub = Sub::new(&mut env, reason, self.span);
sub.tys(self.infcx, a, b)?;
Ok(sub.obligations)
}
Expand Down Expand Up @@ -587,8 +591,33 @@ pub trait LocEnv {
fn get(&self, path: &Path) -> Ty;
}

struct DummyEnv;

impl LocEnv for DummyEnv {
fn ptr_to_ref(
&mut self,
_: &mut InferCtxtAt,
_: ConstrReason,
_: Region,
_: &Path,
_: Ty,
) -> InferResult<Ty> {
bug!("call to `ptr_to_ref` on `DummyEnv`")
}

fn unfold_strg_ref(&mut self, _: &mut InferCtxt, _: &Path, _: &Ty) -> InferResult<Loc> {
bug!("call to `unfold_str_ref` on `DummyEnv`")
}

fn get(&self, _: &Path) -> Ty {
bug!("call to `get` on `DummyEnv`")
}
}

/// Context used to relate two types `a` and `b` via subtyping
struct Sub {
struct Sub<'a, E> {
/// The environment to lookup locations pointed to by [`TyKind::Ptr`].
env: &'a mut E,
reason: ConstrReason,
span: Span,
/// FIXME(nilehmann) This is used to store coroutine obligations generated during subtyping when
Expand All @@ -597,55 +626,62 @@ struct Sub {
obligations: Vec<Binder<rty::CoroutineObligPredicate>>,
}

impl Sub {
fn new(reason: ConstrReason, span: Span) -> Self {
Self { reason, span, obligations: vec![] }
impl<'a, E: LocEnv> Sub<'a, E> {
fn new(env: &'a mut E, reason: ConstrReason, span: Span) -> Self {
Self { env, reason, span, obligations: vec![] }
}

fn tag(&self) -> Tag {
Tag::new(self.reason, self.span)
}

fn fun_args(
&mut self,
infcx: &mut InferCtxt,
env: &mut impl LocEnv,
a: &Ty,
b: &Ty,
) -> InferResult {
fn tys(&mut self, infcx: &mut InferCtxt, a: &Ty, b: &Ty) -> InferResult {
let infcx = &mut infcx.branch();

// infcx.push_trace(TypeTrace::tys(a, b));

// We *fully* unpack the lhs before continuing to be able to prove goals like this
// ∃a. (i32[a], ∃b. {i32[b] | a > b})} <: ∃a,b. ({i32[a] | b < a}, i32[b])
// See S4.5 in https://arxiv.org/pdf/2209.13000v1.pdf
let a = infcx.unpack(a);
match (a.kind(), b.kind()) {
(TyKind::Exists(..), _) => {
bug!("existentials should be removed by the unpacking");
}
(TyKind::Constr(..), _) => {
bug!("constraint types should removed by the unpacking");
}

(_, TyKind::Exists(ctor_b)) => {
infcx.enter_exists(ctor_b, |infcx, ty_b| self.fun_args(infcx, env, a, &ty_b))
infcx.enter_exists(ctor_b, |infcx, ty_b| self.tys(infcx, &a, &ty_b))
}
(_, TyKind::Constr(pred_b, ty_b)) => {
infcx.check_pred(pred_b, self.tag());
self.fun_args(infcx, env, a, ty_b)
self.tys(infcx, &a, ty_b)
}

(TyKind::Ptr(PtrKind::Mut(_), path1), TyKind::StrgRef(_, path2, ty2)) => {
// We should technically remove `path1` from `env`, but we are assuming that functions
// always give back ownership of the location so `path1` is going to be overwritten
// after the call anyways.
let ty1 = env.get(path1);
let ty1 = self.env.get(path1);
infcx.unify_exprs(&path1.to_expr(), &path2.to_expr());
self.tys(infcx, &ty1, ty2)
}
(TyKind::StrgRef(_, path1, ty1), TyKind::StrgRef(_, path2, ty2)) => {
// We has to unfold strong references prior to a subtyping check. Normally, when
// We have to unfold strong references prior to a subtyping check. Normally, when
// checking a function body, a `StrgRef` is automatically unfolded i.e. `x:&strg T`
// is turned into a `x:ptr(l); l: T` where `l` is some fresh location. However, we
// need the below to do a similar unfolding in `check_fn_subtyping` where we just
// need the below to do a similar unfolding during function subtyping where we just
// have the super-type signature that needs to be unfolded. We also add the binding
// to the environment so that we can:
// (1) UPDATE the location after the call, and
// (2) CHECK the relevant `ensures` clauses of the super-sig.
// Same as the `Ptr` case above we should remove the location from the environment
// after unfolding to consume it, but we are assuming functions always give back
// ownership.
env.unfold_strg_ref(infcx, path1, ty1)?;
let ty1 = env.get(path1);
self.env.unfold_strg_ref(infcx, path1, ty1)?;
let ty1 = self.env.get(path1);
infcx.unify_exprs(&path1.to_expr(), &path2.to_expr());
self.tys(infcx, &ty1, ty2)
}
Expand All @@ -657,37 +693,16 @@ impl Sub {
// we solve them.
self.idxs_eq(infcx, &Expr::unit(), idx);

let mut at = infcx.at(self.span);
env.ptr_to_ref(&mut at, self.reason, *re, path, bound.clone())?;
self.env.ptr_to_ref(
&mut infcx.at(self.span),
self.reason,
*re,
path,
bound.clone(),
)?;
Ok(())
}
_ => self.tys(infcx, a, b),
}
}

fn tys(&mut self, infcx: &mut InferCtxt, a: &Ty, b: &Ty) -> InferResult {
let infcx = &mut infcx.branch();

// infcx.push_trace(TypeTrace::tys(a, b));

// We *fully* unpack the lhs before continuing to be able to prove goals like this
// ∃a. (i32[a], ∃b. {i32[b] | a > b})} <: ∃a,b. ({i32[a] | b < a}, i32[b])
// See S4.5 in https://arxiv.org/pdf/2209.13000v1.pdf
let a = infcx.unpack(a);
match (a.kind(), b.kind()) {
(TyKind::Exists(..), _) => {
bug!("existentials should be removed by the unpacking");
}
(TyKind::Constr(..), _) => {
bug!("constraint types should removed by the unpacking");
}
(_, TyKind::Exists(ctor_b)) => {
infcx.enter_exists(ctor_b, |infcx, ty_b| self.tys(infcx, &a, &ty_b))
}
(_, TyKind::Constr(pred_b, ty_b)) => {
infcx.check_pred(pred_b, self.tag());
self.tys(infcx, &a, ty_b)
}
(TyKind::Indexed(bty_a, idx_a), TyKind::Indexed(bty_b, idx_b)) => {
self.btys(infcx, bty_a, bty_b)?;
self.idxs_eq(infcx, idx_a, idx_b);
Expand Down
4 changes: 2 additions & 2 deletions crates/flux-refineck/src/checker.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -267,7 +267,7 @@ fn check_fn_subtyping(
}
for (actual, formal) in iter::zip(actuals, sub_sig.inputs()) {
let reason = ConstrReason::Subtype(SubtypeReason::Input);
infcx.fun_arg_subtyping(&mut env, &actual, formal, reason)?;
infcx.subtyping_with_env(&mut env, &actual, formal, reason)?;
}
// we check the requires AFTER the actual-formal subtyping as the above may unfold stuff in the actuals
for requires in sub_sig.requires() {
Expand Down Expand Up @@ -807,7 +807,7 @@ impl<'ck, 'genv, 'tcx, M: Mode> Checker<'ck, 'genv, 'tcx, M> {

// Check arguments
for (actual, formal) in iter::zip(actuals, fn_sig.inputs()) {
at.fun_arg_subtyping(env, &actual, formal, ConstrReason::Call)
at.subtyping_with_env(env, &actual, formal, ConstrReason::Call)
.with_span(span)?;
}
// Replace evars
Expand Down
Loading