From d7517e75b5589dc515b1a4af610be9ee29221e77 Mon Sep 17 00:00:00 2001 From: Nico Lehmann Date: Fri, 20 Dec 2024 21:25:04 -0300 Subject: [PATCH] Merge tys and fun_args (#958) --- crates/flux-infer/src/infer.rs | 121 ++++++++++++++++------------ crates/flux-refineck/src/checker.rs | 4 +- 2 files changed, 70 insertions(+), 55 deletions(-) diff --git a/crates/flux-infer/src/infer.rs b/crates/flux-infer/src/infer.rs index 8e3acfb65d..94b2ecae34 100644 --- a/crates/flux-infer/src/infer.rs +++ b/crates/flux-infer/src/infer.rs @@ -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>> { - 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) } @@ -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 { + bug!("call to `ptr_to_ref` on `DummyEnv`") + } + + fn unfold_strg_ref(&mut self, _: &mut InferCtxt, _: &Path, _: &Ty) -> InferResult { + 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 @@ -597,46 +626,53 @@ struct Sub { obligations: Vec>, } -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 @@ -644,8 +680,8 @@ impl Sub { // 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) } @@ -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); diff --git a/crates/flux-refineck/src/checker.rs b/crates/flux-refineck/src/checker.rs index f432e5b598..3bb0187545 100644 --- a/crates/flux-refineck/src/checker.rs +++ b/crates/flux-refineck/src/checker.rs @@ -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() { @@ -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