Skip to content

Commit

Permalink
Merge tys and fun_args (#958)
Browse files Browse the repository at this point in the history
  • Loading branch information
@nilehmann
nilehmann authored Dec 21, 2024
1 parent e7b94cc commit d7517e7
Show file tree
Hide file tree
Showing 2 changed files with 70 additions and 55 deletions.
121 changes: 68 additions & 53 deletions crates/flux-infer/src/infer.rs
View file
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
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

0 comments on commit d7517e7

Please sign in to comment.