From 8c3f603495c2644e582f8a770dac2e0ce0e5d1dc Mon Sep 17 00:00:00 2001 From: Nico Lehmann Date: Wed, 14 Feb 2024 20:01:22 -0800 Subject: [PATCH 01/22] Add canonicalize module --- crates/flux-middle/src/rty/mod.rs | 1 + crates/flux-refineck/src/type_env.rs | 71 +++------------------------- 2 files changed, 8 insertions(+), 64 deletions(-) diff --git a/crates/flux-middle/src/rty/mod.rs b/crates/flux-middle/src/rty/mod.rs index 63d6ac4051..cb00c5afa7 100644 --- a/crates/flux-middle/src/rty/mod.rs +++ b/crates/flux-middle/src/rty/mod.rs @@ -4,6 +4,7 @@ //! //! * Types in this module use debruijn indices to represent local binders. //! * Data structures are interned so they can be cheaply cloned. +pub mod canonicalize; pub mod evars; mod expr; pub mod fold; diff --git a/crates/flux-refineck/src/type_env.rs b/crates/flux-refineck/src/type_env.rs index b38d61c38b..7bd787c985 100644 --- a/crates/flux-refineck/src/type_env.rs +++ b/crates/flux-refineck/src/type_env.rs @@ -7,12 +7,12 @@ use flux_middle::{ global_env::GlobalEnv, intern::List, rty::{ - box_args, + canonicalize::Hoister, evars::EVarSol, - fold::{FallibleTypeFolder, TypeFoldable, TypeFolder, TypeVisitable, TypeVisitor}, + fold::{FallibleTypeFolder, TypeFoldable, TypeVisitable, TypeVisitor}, subst::RegionSubst, - BaseTy, Binder, BoundVariableKind, Expr, ExprKind, GenericArg, HoleKind, Mutability, Path, - PtrKind, Region, SortCtor, Ty, TyKind, INNERMOST, + BaseTy, Binder, Expr, ExprKind, GenericArg, HoleKind, Mutability, Path, PtrKind, Region, + SortCtor, Ty, TyKind, INNERMOST, }, rustc::mir::{BasicBlock, Local, LocalDecls, Place, PlaceElem}, }; @@ -543,9 +543,9 @@ impl BasicBlockEnvShape { pub fn into_bb_env(self, kvar_store: &mut KVarStore) -> BasicBlockEnv { let mut bindings = self.bindings; - let mut generalizer = Generalizer::new(); - bindings.fmap_mut(|ty| generalizer.generalize(ty)); - let (vars, preds) = generalizer.into_parts(); + let mut hoister = Hoister::default(); + bindings.fmap_mut(|ty| hoister.hoist(ty)); + let (vars, preds) = hoister.into_parts(); // Replace all holes with a single fresh kvar on all parameters let mut constrs = preds @@ -574,63 +574,6 @@ impl BasicBlockEnvShape { } } -struct Generalizer { - vars: Vec, - preds: Vec, -} - -impl Generalizer { - fn new() -> Self { - Self { vars: vec![], preds: vec![] } - } - - fn into_parts(self) -> (List, Vec) { - (List::from_vec(self.vars), self.preds) - } - - fn generalize(&mut self, ty: &Ty) -> Ty { - ty.fold_with(self) - } -} - -impl TypeFolder for Generalizer { - fn fold_ty(&mut self, ty: &Ty) -> Ty { - match ty.kind() { - TyKind::Exists(ty) => { - ty.replace_bound_exprs_with(|sort, mode| { - let idx = self.vars.len(); - self.vars - .push(BoundVariableKind::Refine(sort.clone(), mode)); - Expr::late_bvar(INNERMOST, idx as u32) - }) - .fold_with(self) - } - TyKind::Constr(pred, ty) => { - self.preds.push(pred.clone()); - ty.fold_with(self) - } - _ => ty.clone(), - } - } - - fn fold_bty(&mut self, bty: &BaseTy) -> BaseTy { - match bty { - BaseTy::Adt(adt_def, args) if adt_def.is_box() => { - let (boxed, alloc) = box_args(args); - let args = List::from_arr([ - GenericArg::Ty(boxed.fold_with(self)), - GenericArg::Ty(alloc.clone()), - ]); - BaseTy::Adt(adt_def.clone(), args) - } - BaseTy::Ref(re, ty, Mutability::Not) => { - BaseTy::Ref(*re, ty.fold_with(self), Mutability::Not) - } - _ => bty.clone(), - } - } -} - impl TypeVisitable for BasicBlockEnvData { fn visit_with(&self, _visitor: &mut V) -> ControlFlow { unimplemented!() From cf4cb6eeb6f3d9358b3bcbb5f403643bc3c22211 Mon Sep 17 00:00:00 2001 From: Nico Lehmann Date: Wed, 14 Feb 2024 20:02:04 -0800 Subject: [PATCH 02/22] Add canonicalize module --- crates/flux-middle/src/rty/canonicalize.rs | 88 ++++++++++++++++++++++ 1 file changed, 88 insertions(+) create mode 100644 crates/flux-middle/src/rty/canonicalize.rs diff --git a/crates/flux-middle/src/rty/canonicalize.rs b/crates/flux-middle/src/rty/canonicalize.rs new file mode 100644 index 0000000000..efe9201b45 --- /dev/null +++ b/crates/flux-middle/src/rty/canonicalize.rs @@ -0,0 +1,88 @@ +use rustc_type_ir::{Mutability, INNERMOST}; + +use super::{ + box_args, + fold::{TypeFoldable, TypeFolder}, + BaseTy, Binder, BoundVariableKind, Expr, GenericArg, Ty, TyKind, +}; +use crate::intern::List; + +#[derive(Default)] +pub struct Hoister { + vars: Vec, + preds: Vec, +} + +impl Hoister { + pub fn into_parts(self) -> (List, Vec) { + (List::from_vec(self.vars), self.preds) + } + + pub fn hoist(&mut self, ty: &Ty) -> Ty { + ty.fold_with(self) + } +} + +impl TypeFolder for Hoister { + fn fold_ty(&mut self, ty: &Ty) -> Ty { + match ty.kind() { + TyKind::Exists(ty) => { + ty.replace_bound_exprs_with(|sort, mode| { + let idx = self.vars.len(); + self.vars + .push(BoundVariableKind::Refine(sort.clone(), mode)); + Expr::late_bvar(INNERMOST, idx as u32) + }) + .fold_with(self) + } + TyKind::Constr(pred, ty) => { + self.preds.push(pred.clone()); + ty.fold_with(self) + } + _ => ty.clone(), + } + } + + fn fold_bty(&mut self, bty: &BaseTy) -> BaseTy { + match bty { + BaseTy::Adt(adt_def, args) if adt_def.is_box() => { + let (boxed, alloc) = box_args(args); + let args = List::from_arr([ + GenericArg::Ty(boxed.fold_with(self)), + GenericArg::Ty(alloc.clone()), + ]); + BaseTy::Adt(adt_def.clone(), args) + } + BaseTy::Ref(re, ty, Mutability::Not) => { + BaseTy::Ref(*re, ty.fold_with(self), Mutability::Not) + } + BaseTy::Tuple(tys) => BaseTy::Tuple(tys.fold_with(self)), + _ => bty.clone(), + } + } +} + +impl Ty { + pub fn shallow_canonicalize(&self) -> CanonicalTy { + let mut hoister = Hoister::default(); + let ty = hoister.hoist(self); + let (vars, preds) = hoister.into_parts(); + let pred = Expr::and(preds); + let constr_ty = ConstrTy { ty, pred }; + if vars.is_empty() { + CanonicalTy::Constr(constr_ty) + } else { + CanonicalTy::Exists(Binder::new(constr_ty, vars)) + } + } +} + +pub enum CanonicalTy { + Exists(Binder), + Constr(ConstrTy), +} + +pub struct ConstrTy { + ty: Ty, + pred: Expr, +} From 33963c1f0473ec30ece7634498fb099f406f00f7 Mon Sep 17 00:00:00 2001 From: Nico Lehmann Date: Wed, 14 Feb 2024 20:19:16 -0800 Subject: [PATCH 03/22] canonicalty to bty_arg --- crates/flux-middle/src/rty/canonicalize.rs | 33 +++++++++++++++++++++- 1 file changed, 32 insertions(+), 1 deletion(-) diff --git a/crates/flux-middle/src/rty/canonicalize.rs b/crates/flux-middle/src/rty/canonicalize.rs index efe9201b45..35621710a9 100644 --- a/crates/flux-middle/src/rty/canonicalize.rs +++ b/crates/flux-middle/src/rty/canonicalize.rs @@ -3,7 +3,7 @@ use rustc_type_ir::{Mutability, INNERMOST}; use super::{ box_args, fold::{TypeFoldable, TypeFolder}, - BaseTy, Binder, BoundVariableKind, Expr, GenericArg, Ty, TyKind, + BaseTy, Binder, BoundVariableKind, Expr, ExprKind, GenericArg, Ty, TyKind, Var, }; use crate::intern::List; @@ -82,6 +82,37 @@ pub enum CanonicalTy { Constr(ConstrTy), } +impl CanonicalTy { + pub fn to_bty_arg(&self) -> Option { + match self { + CanonicalTy::Exists(poly_constr_ty) => { + let vars = poly_constr_ty.vars(); + let constr_ty = poly_constr_ty.as_ref().skip_binder(); + if let TyKind::Indexed(bty, idx) = constr_ty.ty.kind() + && vars.to_sort_list()[..] == [bty.sort()][..] + && let ExprKind::Var(Var::LateBound(INNERMOST, 0)) = idx.kind() + { + let ty = Ty::constr(constr_ty.pred.clone(), Ty::indexed(bty.clone(), idx)); + Some(GenericArg::BaseTy(Binder::new(ty, vars.clone()))) + } else { + None + } + } + CanonicalTy::Constr(constr_ty) => { + if let TyKind::Indexed(bty, idx) = constr_ty.ty.kind() { + let sort = bty.sort(); + let infer_mode = sort.default_infer_mode(); + let ty = Ty::constr(Expr::eq(Expr::nu(), idx), Ty::indexed(bty.clone(), idx)); + let vars = List::singleton(BoundVariableKind::Refine(sort, infer_mode)); + Some(GenericArg::BaseTy(Binder::new(ty, vars))) + } else { + None + } + } + } + } +} + pub struct ConstrTy { ty: Ty, pred: Expr, From a1aa7e73a0d4130d58ef5078cd47a7a4e8ecd89a Mon Sep 17 00:00:00 2001 From: Nico Lehmann Date: Wed, 14 Feb 2024 21:34:23 -0800 Subject: [PATCH 04/22] convert ty to bty arg ty --- crates/flux-fhir-analysis/src/conv.rs | 42 +++++++++++++++++++-------- crates/flux-middle/src/rty/expr.rs | 2 +- 2 files changed, 31 insertions(+), 13 deletions(-) diff --git a/crates/flux-fhir-analysis/src/conv.rs b/crates/flux-fhir-analysis/src/conv.rs index 03ca48cc57..8fee45ec90 100644 --- a/crates/flux-fhir-analysis/src/conv.rs +++ b/crates/flux-fhir-analysis/src/conv.rs @@ -424,7 +424,7 @@ impl<'a, 'genv, 'tcx> ConvCtxt<'a, 'genv, 'tcx> { clauses: &mut Vec, ) -> QueryResult { let mut into = vec![rty::GenericArg::Ty(bounded_ty.clone())]; - self.conv_generic_args_into(env, args, &mut into)?; + self.conv_generic_args_into(env, trait_id, args, &mut into)?; self.fill_generic_args_defaults(trait_id, &mut into)?; let trait_ref = rty::TraitRef { def_id: trait_id, args: into.into() }; let pred = rty::TraitPredicate { trait_ref }; @@ -736,18 +736,19 @@ impl<'a, 'genv, 'tcx> ConvCtxt<'a, 'genv, 'tcx> { let sort = self.genv.sort_of_bty(bty); if let fhir::BaseTyKind::Path(fhir::QPath::Resolved(self_ty, path)) = &bty.kind { - if let fhir::Res::Def(DefKind::AssocTy, def_id) = path.res { + if let fhir::Res::Def(DefKind::AssocTy, assoc_id) = path.res { + let trait_id = self.genv.tcx().trait_of_item(assoc_id).unwrap(); let self_ty = self.conv_ty(env, self_ty.as_deref().unwrap())?; let [.., trait_segment, assoc_segment] = path.segments else { span_bug!(bty.span, "expected at least two segments"); }; let mut args = vec![rty::GenericArg::Ty(self_ty)]; - self.conv_generic_args_into(env, trait_segment.args, &mut args)?; - self.conv_generic_args_into(env, assoc_segment.args, &mut args)?; + self.conv_generic_args_into(env, trait_id, trait_segment.args, &mut args)?; + self.conv_generic_args_into(env, assoc_id, assoc_segment.args, &mut args)?; let args = List::from_vec(args); let refine_args = List::empty(); - let alias_ty = rty::AliasTy { args, refine_args, def_id }; + let alias_ty = rty::AliasTy { args, refine_args, def_id: assoc_id }; return Ok(rty::Ty::alias(rty::AliasKind::Projection, alias_ty)); } // If it is a type parameter with no sort, it means it is of kind `Type` @@ -924,7 +925,7 @@ impl<'a, 'genv, 'tcx> ConvCtxt<'a, 'genv, 'tcx> { args: &[fhir::GenericArg], ) -> QueryResult> { let mut into = vec![]; - self.conv_generic_args_into(env, args, &mut into)?; + self.conv_generic_args_into(env, def_id, args, &mut into)?; self.fill_generic_args_defaults(def_id, &mut into)?; Ok(into) } @@ -932,17 +933,34 @@ impl<'a, 'genv, 'tcx> ConvCtxt<'a, 'genv, 'tcx> { fn conv_generic_args_into( &self, env: &mut Env, + def_id: DefId, args: &[fhir::GenericArg], into: &mut Vec, - ) -> QueryResult<()> { - for arg in args { - match arg { - fhir::GenericArg::Lifetime(lft) => { + ) -> QueryResult { + let generics = self.genv.generics_of(def_id)?; + for (idx, arg) in args.iter().enumerate() { + let param = generics.param_at(idx, self.genv)?; + match (arg, ¶m.kind) { + (fhir::GenericArg::Lifetime(lft), rty::GenericParamDefKind::Lifetime) => { into.push(rty::GenericArg::Lifetime(self.conv_lifetime(env, *lft))); } - fhir::GenericArg::Type(ty) => { + ( + fhir::GenericArg::Type(ty), + rty::GenericParamDefKind::Type { .. } | rty::GenericParamDefKind::SplTy, + ) => { into.push(rty::GenericArg::Ty(self.conv_ty(env, ty)?)); } + (fhir::GenericArg::Type(ty), rty::GenericParamDefKind::BaseTy) => { + let arg = self + .conv_ty(env, ty)? + .shallow_canonicalize() + .to_bty_arg() + .unwrap(); + into.push(arg); + } + _ => { + bug!("unexpected param `{:?}` for arg `{arg:?}`", param.kind); + } } } Ok(()) @@ -952,7 +970,7 @@ impl<'a, 'genv, 'tcx> ConvCtxt<'a, 'genv, 'tcx> { &self, def_id: DefId, into: &mut Vec, - ) -> QueryResult<()> { + ) -> QueryResult { let generics = self.genv.generics_of(def_id)?; for param in generics.params.iter().skip(into.len()) { if let rty::GenericParamDefKind::Type { has_default } = param.kind { diff --git a/crates/flux-middle/src/rty/expr.rs b/crates/flux-middle/src/rty/expr.rs index f788e57048..9b3c072b9d 100644 --- a/crates/flux-middle/src/rty/expr.rs +++ b/crates/flux-middle/src/rty/expr.rs @@ -938,7 +938,7 @@ mod pretty { impl Pretty for AliasReft { fn fmt(&self, cx: &PPrintCx, f: &mut fmt::Formatter<'_>) -> fmt::Result { define_scoped!(cx, f); - w!("<{:?} as {:?}", self.self_ty(), self.trait_id)?; + w!("<{:?} as {:?}", &self.args[0], self.trait_id)?; let args = &self.args[1..]; if !args.is_empty() { w!("<{:?}>", join!(", ", args))?; From 22f5063d5a5a9aa4dca6895627a002e425ea1930 Mon Sep 17 00:00:00 2001 From: Nico Lehmann Date: Thu, 15 Feb 2024 17:06:01 -0800 Subject: [PATCH 05/22] nit --- crates/flux-middle/src/rty/canonicalize.rs | 14 ++++++++++++-- 1 file changed, 12 insertions(+), 2 deletions(-) diff --git a/crates/flux-middle/src/rty/canonicalize.rs b/crates/flux-middle/src/rty/canonicalize.rs index 3ef95fde21..bff1ae48dd 100644 --- a/crates/flux-middle/src/rty/canonicalize.rs +++ b/crates/flux-middle/src/rty/canonicalize.rs @@ -88,10 +88,10 @@ impl CanonicalTy { CanonicalTy::Exists(poly_constr_ty) => { let vars = poly_constr_ty.vars(); let constr_ty = poly_constr_ty.as_ref().skip_binder(); - if let TyKind::Indexed(bty, idx) = constr_ty.ty.kind() + if let TyKind::Indexed(_, idx) = constr_ty.ty.kind() && idx.is_nu() { - let ty = Ty::constr(constr_ty.pred.clone(), Ty::indexed(bty.clone(), idx)); + let ty = constr_ty.to_ty(); Some(GenericArg::BaseTy(Binder::new(ty, vars.clone()))) } else { None @@ -120,3 +120,13 @@ pub struct ConstrTy { ty: Ty, pred: Expr, } + +impl ConstrTy { + pub fn to_ty(&self) -> Ty { + if self.pred.is_trivially_true() { + self.ty.clone() + } else { + Ty::constr(self.pred.clone(), self.ty.clone()) + } + } +} From ad46aa948a48cb2b9ec7899600b7719c3ed7f286 Mon Sep 17 00:00:00 2001 From: Nico Lehmann Date: Thu, 15 Feb 2024 17:47:59 -0800 Subject: [PATCH 06/22] save --- crates/flux-middle/src/rty/canonicalize.rs | 61 +++++++------- crates/flux-middle/src/rty/fold.rs | 28 ++++++- crates/flux-middle/src/rty/mod.rs | 96 +++++++++++++--------- crates/flux-middle/src/rty/projections.rs | 4 +- crates/flux-middle/src/rty/refining.rs | 2 +- crates/flux-middle/src/rty/subst.rs | 4 +- crates/flux-refineck/src/constraint_gen.rs | 2 +- crates/flux-refineck/src/type_env.rs | 6 +- 8 files changed, 122 insertions(+), 81 deletions(-) diff --git a/crates/flux-middle/src/rty/canonicalize.rs b/crates/flux-middle/src/rty/canonicalize.rs index bff1ae48dd..922e70cb53 100644 --- a/crates/flux-middle/src/rty/canonicalize.rs +++ b/crates/flux-middle/src/rty/canonicalize.rs @@ -3,7 +3,7 @@ use rustc_type_ir::{Mutability, INNERMOST}; use super::{ box_args, fold::{TypeFoldable, TypeFolder}, - BaseTy, Binder, BoundReftKind, BoundVariableKind, Expr, GenericArg, Ty, TyKind, + BaseTy, Binder, BoundVariableKind, Expr, GenericArg, Ty, TyKind, }; use crate::intern::List; @@ -84,35 +84,36 @@ pub enum CanonicalTy { impl CanonicalTy { pub fn to_bty_arg(&self) -> Option { - match self { - CanonicalTy::Exists(poly_constr_ty) => { - let vars = poly_constr_ty.vars(); - let constr_ty = poly_constr_ty.as_ref().skip_binder(); - if let TyKind::Indexed(_, idx) = constr_ty.ty.kind() - && idx.is_nu() - { - let ty = constr_ty.to_ty(); - Some(GenericArg::BaseTy(Binder::new(ty, vars.clone()))) - } else { - None - } - } - CanonicalTy::Constr(constr_ty) => { - if let TyKind::Indexed(bty, idx) = constr_ty.ty.kind() { - let sort = bty.sort(); - let infer_mode = sort.default_infer_mode(); - let ty = Ty::constr(Expr::eq(Expr::nu(), idx), Ty::indexed(bty.clone(), idx)); - let vars = List::singleton(BoundVariableKind::Refine( - sort, - infer_mode, - BoundReftKind::Annon, - )); - Some(GenericArg::BaseTy(Binder::new(ty, vars))) - } else { - None - } - } - } + todo!() + // match self { + // CanonicalTy::Exists(poly_constr_ty) => { + // let vars = poly_constr_ty.vars(); + // let constr_ty = poly_constr_ty.as_ref().skip_binder(); + // if let TyKind::Indexed(_, idx) = constr_ty.ty.kind() + // && idx.is_nu() + // { + // let ty = constr_ty.to_ty(); + // Some(GenericArg::Base(Binder::new(ty, vars.clone()))) + // } else { + // None + // } + // } + // CanonicalTy::Constr(constr_ty) => { + // if let TyKind::Indexed(bty, idx) = constr_ty.ty.kind() { + // let sort = bty.sort(); + // let infer_mode = sort.default_infer_mode(); + // let ty = Ty::constr(Expr::eq(Expr::nu(), idx), Ty::indexed(bty.clone(), idx)); + // let vars = List::singleton(BoundVariableKind::Refine( + // sort, + // infer_mode, + // BoundReftKind::Annon, + // )); + // Some(GenericArg::Base(Binder::new(ty, vars))) + // } else { + // None + // } + // } + // } } } diff --git a/crates/flux-middle/src/rty/fold.rs b/crates/flux-middle/src/rty/fold.rs index 0a1dbde83c..9a59edcd48 100644 --- a/crates/flux-middle/src/rty/fold.rs +++ b/crates/flux-middle/src/rty/fold.rs @@ -17,7 +17,7 @@ use super::{ AliasReft, AliasTy, BaseTy, BinOp, Binder, BoundVariableKind, Clause, ClauseKind, Constraint, CoroutineObligPredicate, Expr, ExprKind, FnOutput, FnSig, FnTraitPredicate, FuncSort, GenericArg, Invariant, KVar, Lambda, Name, OpaqueArgsMap, Opaqueness, OutlivesPredicate, - PolyFuncSort, ProjectionPredicate, PtrKind, Qualifier, ReLateBound, Region, Sort, + PolyFuncSort, ProjectionPredicate, PtrKind, Qualifier, ReLateBound, Region, SimpleTy, Sort, TraitPredicate, TraitRef, Ty, TyKind, }; use crate::{ @@ -967,11 +967,30 @@ impl TypeFoldable for AliasTy { } } +impl TypeVisitable for SimpleTy { + fn visit_with(&self, visitor: &mut V) -> ControlFlow { + self.bty.visit_with(visitor)?; + self.pred.visit_with(visitor) + } +} + +impl TypeFoldable for SimpleTy { + fn try_fold_with(&self, folder: &mut F) -> Result { + Ok(SimpleTy { + bty: self.bty.try_fold_with(folder)?, + pred: self.pred.try_fold_with(folder)?, + }) + } +} + impl TypeVisitable for GenericArg { fn visit_with(&self, visitor: &mut V) -> ControlFlow { match self { GenericArg::Ty(ty) => ty.visit_with(visitor), - GenericArg::BaseTy(ty) => ty.visit_with(visitor), + GenericArg::Base(ty) => { + todo!() + // ty.visit_with(visitor) + } GenericArg::Lifetime(_) => ControlFlow::Continue(()), GenericArg::Const(_) => ControlFlow::Continue(()), } @@ -982,7 +1001,10 @@ impl TypeFoldable for GenericArg { fn try_fold_with(&self, folder: &mut F) -> Result { let arg = match self { GenericArg::Ty(ty) => GenericArg::Ty(ty.try_fold_with(folder)?), - GenericArg::BaseTy(ty) => GenericArg::BaseTy(ty.try_fold_with(folder)?), + GenericArg::Base(ty) => { + todo!() + // GenericArg::Base(ty.try_fold_with(folder)?) + } GenericArg::Lifetime(re) => GenericArg::Lifetime(re.try_fold_with(folder)?), GenericArg::Const(c) => GenericArg::Const(c.clone()), }; diff --git a/crates/flux-middle/src/rty/mod.rs b/crates/flux-middle/src/rty/mod.rs index 3c595c9ea7..9b2d45cd90 100644 --- a/crates/flux-middle/src/rty/mod.rs +++ b/crates/flux-middle/src/rty/mod.rs @@ -608,7 +608,7 @@ pub enum BaseTy { Tuple(List), Array(Ty, Const), Never, - Closure(DefId, List), + Closure(DefId, /* upvar_tys */ List), Coroutine(DefId, /*resume_ty: */ Ty, /* upvar_tys: */ List), Param(ParamTy), } @@ -633,45 +633,30 @@ pub type GenericArgs = List; pub type OpaqueArgsMap = FxHashMap; #[derive(PartialEq, Clone, Eq, Hash, TyEncodable, TyDecodable)] -pub enum GenericArg { - Ty(Ty), - BaseTy(Binder), - Lifetime(Region), - Const(Const), +pub struct SimpleTy { + bty: BaseTy, + pred: Expr, } -impl GenericArgs { - pub fn identity_for_item(genv: GlobalEnv, def_id: impl Into) -> QueryResult { - let mut args = vec![]; - let generics = genv.generics_of(def_id)?; - Self::fill_item(genv, &mut args, &generics, &mut |param, _| { - GenericArg::from_param_def(genv, param) - })?; - Ok(List::from_vec(args)) +impl SimpleTy { + pub fn sort(&self) -> Sort { + self.bty.sort() } - fn fill_item( - genv: GlobalEnv, - args: &mut Vec, - generics: &Generics, - mk_kind: &mut F, - ) -> QueryResult<()> - where - F: FnMut(&GenericParamDef, &[GenericArg]) -> QueryResult, - { - if let Some(def_id) = generics.parent { - let parent_generics = genv.generics_of(def_id)?; - Self::fill_item(genv, args, &parent_generics, mk_kind)?; - } - for param in &generics.params { - let kind = mk_kind(param, args)?; - assert_eq!(param.index as usize, args.len(), "{args:#?}, {generics:#?}"); - args.push(kind); - } - Ok(()) + pub fn as_ty_ctor(&self) -> Binder { + let ty = Ty::constr(self.pred.clone(), Ty::indexed(self.bty.clone(), Expr::nu())); + Binder::with_sort(ty, self.sort()) } } +#[derive(PartialEq, Clone, Eq, Hash, TyEncodable, TyDecodable)] +pub enum GenericArg { + Ty(Ty), + Base(SimpleTy), + Lifetime(Region), + Const(Const), +} + impl GenericArg { pub fn expect_type(&self) -> &Ty { if let GenericArg::Ty(ty) = self { @@ -684,7 +669,7 @@ impl GenericArg { pub fn peel_out_sort(&self) -> Option { match self { GenericArg::Ty(ty) => ty.as_bty_skipping_existentials().map(BaseTy::sort), - GenericArg::BaseTy(abs) => Some(abs.vars()[0].expect_sort().clone()), + GenericArg::Base(ty) => Some(ty.sort()), GenericArg::Lifetime(_) | GenericArg::Const(_) => None, } } @@ -692,7 +677,7 @@ impl GenericArg { pub fn is_valid_base_arg(&self) -> bool { match self { GenericArg::Ty(ty) => ty.kind().is_valid_base_ty(), - GenericArg::BaseTy(bty) => bty.as_ref().skip_binder().kind().is_valid_base_ty(), + GenericArg::Base(ty) => true, _ => false, } } @@ -721,6 +706,38 @@ impl GenericArg { } } +impl GenericArgs { + pub fn identity_for_item(genv: GlobalEnv, def_id: impl Into) -> QueryResult { + let mut args = vec![]; + let generics = genv.generics_of(def_id)?; + Self::fill_item(genv, &mut args, &generics, &mut |param, _| { + GenericArg::from_param_def(genv, param) + })?; + Ok(List::from_vec(args)) + } + + fn fill_item( + genv: GlobalEnv, + args: &mut Vec, + generics: &Generics, + mk_kind: &mut F, + ) -> QueryResult<()> + where + F: FnMut(&GenericParamDef, &[GenericArg]) -> QueryResult, + { + if let Some(def_id) = generics.parent { + let parent_generics = genv.generics_of(def_id)?; + Self::fill_item(genv, args, &parent_generics, mk_kind)?; + } + for param in &generics.params { + let kind = mk_kind(param, args)?; + assert_eq!(param.index as usize, args.len(), "{args:#?}, {generics:#?}"); + args.push(kind); + } + Ok(()) + } +} + impl Clause { pub fn new(vars: impl Into>, kind: ClauseKind) -> Self { Clause { kind: Binder::new(kind, vars.into()) } @@ -2262,10 +2279,11 @@ mod pretty { define_scoped!(cx, f); match self { GenericArg::Ty(arg) => w!("{:?}", arg), - GenericArg::BaseTy(arg) => { - cx.with_bound_vars(arg.vars(), || { - cx.fmt_bound_vars("λ", arg.vars(), ". ", f)?; - w!("{:?}", arg.as_ref().skip_binder()) + GenericArg::Base(arg) => { + let ctor = arg.as_ty_ctor(); + cx.with_bound_vars(ctor.vars(), || { + cx.fmt_bound_vars("λ", ctor.vars(), ". ", f)?; + w!("{:?}", ctor.as_ref().skip_binder()) }) } GenericArg::Lifetime(re) => w!("{:?}", re), diff --git a/crates/flux-middle/src/rty/projections.rs b/crates/flux-middle/src/rty/projections.rs index f056a2dc0c..c63f27dcc2 100644 --- a/crates/flux-middle/src/rty/projections.rs +++ b/crates/flux-middle/src/rty/projections.rs @@ -280,7 +280,7 @@ fn into_rustc_generic_arg<'tcx>( use rustc_middle::ty; match arg { GenericArg::Ty(ty) => ty::GenericArg::from(into_rustc_ty(tcx, ty)), - GenericArg::BaseTy(bty) => { + GenericArg::Base(ty) => { ty::GenericArg::from(into_rustc_ty(tcx, &bty.clone().skip_binder())) } GenericArg::Lifetime(re) => ty::GenericArg::from(into_rustc_region(tcx, *re)), @@ -449,7 +449,7 @@ impl TVarSubst { self.infer_from_ty(&src.as_type().unwrap(), dst); } GenericArg::Lifetime(dst) => self.infer_from_region(&src.as_region().unwrap(), dst), - GenericArg::BaseTy(bty) => { + GenericArg::Base(bty) => { self.infer_from_ty(&src.as_type().unwrap(), &bty.clone().skip_binder()); } _ => (), diff --git a/crates/flux-middle/src/rty/refining.rs b/crates/flux-middle/src/rty/refining.rs index c584d383e0..46240c03a8 100644 --- a/crates/flux-middle/src/rty/refining.rs +++ b/crates/flux-middle/src/rty/refining.rs @@ -224,7 +224,7 @@ impl<'genv, 'tcx> Refiner<'genv, 'tcx> { Ok(rty::GenericArg::Ty(self.refine_ty(ty)?)) } (rty::GenericParamDefKind::BaseTy, rustc::ty::GenericArg::Ty(ty)) => { - Ok(rty::GenericArg::BaseTy(self.refine_poly_ty(ty)?)) + Ok(rty::GenericArg::Base(self.refine_poly_ty(ty)?)) } (rty::GenericParamDefKind::Lifetime, rustc::ty::GenericArg::Lifetime(re)) => { Ok(rty::GenericArg::Lifetime(*re)) diff --git a/crates/flux-middle/src/rty/subst.rs b/crates/flux-middle/src/rty/subst.rs index c7e6c280f7..2cb19fdf06 100644 --- a/crates/flux-middle/src/rty/subst.rs +++ b/crates/flux-middle/src/rty/subst.rs @@ -71,7 +71,7 @@ impl RegionSubst { debug_assert_eq!(args1.len(), args2.len()); for (arg1, arg2) in iter::zip(args1, args2) { match (arg1, arg2) { - (GenericArg::BaseTy(ty_con), ty::GenericArg::Ty(ty2)) => { + (GenericArg::Base(ty_con), ty::GenericArg::Ty(ty2)) => { self.infer_from_ty(ty_con.as_ref().skip_binder(), ty2); } (GenericArg::Ty(ty1), ty::GenericArg::Ty(ty2)) => { @@ -303,7 +303,7 @@ impl GenericsSubstDelegate for GenericArgsDelegate<'_> { fn bty_for_param(&mut self, param_ty: ParamTy, idx: &Expr) -> Ty { match self.0.get(param_ty.index as usize) { - Some(GenericArg::BaseTy(arg)) => arg.replace_bound_reft(idx), + Some(GenericArg::Base(arg)) => arg.replace_bound_reft(idx), Some(arg) => { bug!("expected base type for generic parameter, found `{:?}`", arg) } diff --git a/crates/flux-refineck/src/constraint_gen.rs b/crates/flux-refineck/src/constraint_gen.rs index 8263585924..7f39edf599 100644 --- a/crates/flux-refineck/src/constraint_gen.rs +++ b/crates/flux-refineck/src/constraint_gen.rs @@ -693,7 +693,7 @@ impl<'a, 'genv, 'tcx> InferCtxt<'a, 'genv, 'tcx> { Variance::Bivariant => Ok(()), } } - (GenericArg::BaseTy(_), GenericArg::BaseTy(_)) => { + (GenericArg::Base(_), GenericArg::Base(_)) => { tracked_span_bug!("generic argument subtyping for base types is not implemented"); } (GenericArg::Lifetime(_), GenericArg::Lifetime(_)) => Ok(()), diff --git a/crates/flux-refineck/src/type_env.rs b/crates/flux-refineck/src/type_env.rs index 48e6a61a5f..c660933ca7 100644 --- a/crates/flux-refineck/src/type_env.rs +++ b/crates/flux-refineck/src/type_env.rs @@ -373,8 +373,8 @@ impl BasicBlockEnvShape { fn pack_generic_arg(scope: &Scope, arg: &GenericArg) -> GenericArg { match arg { GenericArg::Ty(ty) => GenericArg::Ty(Self::pack_ty(scope, ty)), - GenericArg::BaseTy(arg) => { - GenericArg::BaseTy(arg.as_ref().map(|ty| Self::pack_ty(scope, ty))) + GenericArg::Base(arg) => { + GenericArg::Base(arg.as_ref().map(|ty| Self::pack_ty(scope, ty))) } GenericArg::Lifetime(re) => GenericArg::Lifetime(*re), GenericArg::Const(c) => GenericArg::Const(c.clone()), @@ -529,7 +529,7 @@ impl BasicBlockEnvShape { fn join_generic_arg(&self, arg1: &GenericArg, arg2: &GenericArg) -> GenericArg { match (arg1, arg2) { (GenericArg::Ty(ty1), GenericArg::Ty(ty2)) => GenericArg::Ty(self.join_ty(ty1, ty2)), - (GenericArg::BaseTy(_), GenericArg::BaseTy(_)) => { + (GenericArg::Base(_), GenericArg::Base(_)) => { tracked_span_bug!("generic argument join for base types is not implemented") } (GenericArg::Lifetime(re1), GenericArg::Lifetime(re2)) => { From 67b9736a24f42f4931bcd4b4583af1bcfa47e8db Mon Sep 17 00:00:00 2001 From: Nico Lehmann Date: Thu, 15 Feb 2024 20:29:10 -0800 Subject: [PATCH 07/22] ufff --- crates/flux-middle/src/rty/canonicalize.rs | 53 +++++++++------------- crates/flux-middle/src/rty/expr.rs | 27 +++++++++-- crates/flux-middle/src/rty/fold.rs | 7 ++- crates/flux-middle/src/rty/mod.rs | 43 ++++++------------ crates/flux-middle/src/rty/projections.rs | 2 +- 5 files changed, 63 insertions(+), 69 deletions(-) diff --git a/crates/flux-middle/src/rty/canonicalize.rs b/crates/flux-middle/src/rty/canonicalize.rs index 922e70cb53..c9816fdb51 100644 --- a/crates/flux-middle/src/rty/canonicalize.rs +++ b/crates/flux-middle/src/rty/canonicalize.rs @@ -3,7 +3,7 @@ use rustc_type_ir::{Mutability, INNERMOST}; use super::{ box_args, fold::{TypeFoldable, TypeFolder}, - BaseTy, Binder, BoundVariableKind, Expr, GenericArg, Ty, TyKind, + BaseTy, Binder, BoundVariableKind, Expr, GenericArg, SimpleTy, Ty, TyKind, }; use crate::intern::List; @@ -84,36 +84,27 @@ pub enum CanonicalTy { impl CanonicalTy { pub fn to_bty_arg(&self) -> Option { - todo!() - // match self { - // CanonicalTy::Exists(poly_constr_ty) => { - // let vars = poly_constr_ty.vars(); - // let constr_ty = poly_constr_ty.as_ref().skip_binder(); - // if let TyKind::Indexed(_, idx) = constr_ty.ty.kind() - // && idx.is_nu() - // { - // let ty = constr_ty.to_ty(); - // Some(GenericArg::Base(Binder::new(ty, vars.clone()))) - // } else { - // None - // } - // } - // CanonicalTy::Constr(constr_ty) => { - // if let TyKind::Indexed(bty, idx) = constr_ty.ty.kind() { - // let sort = bty.sort(); - // let infer_mode = sort.default_infer_mode(); - // let ty = Ty::constr(Expr::eq(Expr::nu(), idx), Ty::indexed(bty.clone(), idx)); - // let vars = List::singleton(BoundVariableKind::Refine( - // sort, - // infer_mode, - // BoundReftKind::Annon, - // )); - // Some(GenericArg::Base(Binder::new(ty, vars))) - // } else { - // None - // } - // } - // } + match self { + CanonicalTy::Exists(poly_constr_ty) => { + let constr_ty = poly_constr_ty.as_ref().skip_binder(); + if let TyKind::Indexed(bty, idx) = constr_ty.ty.kind() + && idx.is_nu() + { + let sty = SimpleTy::new(bty.clone(), &constr_ty.pred); + Some(GenericArg::Base(sty)) + } else { + None + } + } + CanonicalTy::Constr(constr_ty) => { + if let TyKind::Indexed(bty, idx) = constr_ty.ty.kind() { + let sty = SimpleTy::new(bty.clone(), Expr::eq(Expr::nu(), idx)); + Some(GenericArg::Base(sty)) + } else { + None + } + } + } } } diff --git a/crates/flux-middle/src/rty/expr.rs b/crates/flux-middle/src/rty/expr.rs index 933946cbf9..13062c8de0 100644 --- a/crates/flux-middle/src/rty/expr.rs +++ b/crates/flux-middle/src/rty/expr.rs @@ -6,13 +6,13 @@ use itertools::Itertools; use rustc_hir::def_id::DefId; use rustc_index::newtype_index; use rustc_macros::{Decodable, Encodable, TyDecodable, TyEncodable}; -use rustc_middle::mir::Local; +use rustc_middle::{mir::Local, ty::TyCtxt}; use rustc_span::{BytePos, Span, Symbol, SyntaxContext}; use rustc_target::abi::FieldIdx; use rustc_type_ir::{DebruijnIndex, INNERMOST}; use super::{ - evars::EVar, AliasReft, BaseTy, Binder, BoundReftKind, BoundVariableKind, FuncSort, IntTy, + evars::EVar, BaseTy, Binder, BoundReftKind, BoundVariableKind, FuncSort, GenericArgs, IntTy, Sort, UintTy, }; use crate::{ @@ -57,6 +57,24 @@ impl Lambda { } } +#[derive(Clone, PartialEq, Eq, Hash, TyEncodable, TyDecodable)] +pub struct AliasReft { + pub trait_id: DefId, + pub name: Symbol, + pub args: GenericArgs, +} + +impl AliasReft { + pub fn to_rustc_trait_ref<'tcx>(&self, tcx: TyCtxt<'tcx>) -> rustc_middle::ty::TraitRef<'tcx> { + let trait_def_id = self.trait_id; + let args = self + .args + .to_rustc(tcx) + .truncate_to(tcx, tcx.generics_of(trait_def_id)); + rustc_middle::ty::TraitRef::new(tcx, trait_def_id, args) + } +} + pub type Expr = Interned; #[derive(Clone, PartialEq, Eq, Hash, TyEncodable, TyDecodable)] @@ -558,8 +576,7 @@ impl Expr { } /// Simple syntactic check to see if the expression is a trivially true predicate. This is used - /// mostly for filtering predicates when pretty printing but also to simplify the constraint - /// before encoding it into fixpoint. + /// mostly for filtering predicates when pretty printing but also to simplify the types. pub fn is_trivially_true(&self) -> bool { self.is_true() || matches!(self.kind(), ExprKind::BinaryOp(BinOp::Eq | BinOp::Iff | BinOp::Imp, e1, e2) if e1 == e2) @@ -966,7 +983,7 @@ mod pretty { impl Pretty for AliasReft { fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result { define_scoped!(cx, f); - w!("<{:?} as {:?}", &self.args[0], self.trait_id)?; + w!("<({:?}) as {:?}", &self.args[0], self.trait_id)?; let args = &self.args[1..]; if !args.is_empty() { w!("<{:?}>", join!(", ", args))?; diff --git a/crates/flux-middle/src/rty/fold.rs b/crates/flux-middle/src/rty/fold.rs index ba5122a423..adeb8f4dc9 100644 --- a/crates/flux-middle/src/rty/fold.rs +++ b/crates/flux-middle/src/rty/fold.rs @@ -1010,7 +1010,7 @@ impl TypeFoldable for GenericArg { fn try_fold_with(&self, folder: &mut F) -> Result { let arg = match self { GenericArg::Ty(ty) => GenericArg::Ty(ty.try_fold_with(folder)?), - GenericArg::Base(ty) => GenericArg::Base(ty.try_fold_with(folder)?), + GenericArg::Base(sty) => GenericArg::Base(sty.try_fold_with(folder)?), GenericArg::Lifetime(re) => GenericArg::Lifetime(re.try_fold_with(folder)?), GenericArg::Const(c) => GenericArg::Const(c.clone()), }; @@ -1104,9 +1104,8 @@ impl TypeVisitable for Var { impl TypeFoldable for AliasReft { fn try_fold_with(&self, folder: &mut F) -> Result { let trait_id = self.trait_id; - let generic_args = self.args.try_fold_with(folder)?; - let alias_pred = AliasReft { trait_id, name: self.name, args: generic_args }; - Ok(alias_pred) + let args = self.args.try_fold_with(folder)?; + Ok(AliasReft { trait_id, name: self.name, args }) } } diff --git a/crates/flux-middle/src/rty/mod.rs b/crates/flux-middle/src/rty/mod.rs index 3621fe5634..de9b8412d6 100644 --- a/crates/flux-middle/src/rty/mod.rs +++ b/crates/flux-middle/src/rty/mod.rs @@ -17,8 +17,8 @@ use std::{borrow::Cow, fmt, hash::Hash, iter, slice, sync::LazyLock}; pub use evars::{EVar, EVarGen}; pub use expr::{ - AggregateKind, BinOp, BoundReft, Constant, ESpan, Expr, ExprKind, FieldProj, HoleKind, KVar, - KVid, Lambda, Loc, Name, Path, UnOp, Var, + AggregateKind, AliasReft, BinOp, BoundReft, Constant, ESpan, Expr, ExprKind, FieldProj, + HoleKind, KVar, KVid, Lambda, Loc, Name, Path, UnOp, Var, }; use flux_common::bug; use itertools::Itertools; @@ -718,24 +718,6 @@ pub struct TyS { kind: TyKind, } -#[derive(Clone, PartialEq, Eq, Hash, TyEncodable, TyDecodable)] -pub struct AliasReft { - pub trait_id: DefId, - pub name: Symbol, - pub args: GenericArgs, -} - -impl AliasReft { - pub fn to_rustc_trait_ref<'tcx>(&self, tcx: TyCtxt<'tcx>) -> rustc_middle::ty::TraitRef<'tcx> { - let trait_def_id = self.trait_id; - let args = self - .args - .to_rustc(tcx) - .truncate_to(tcx, tcx.generics_of(trait_def_id)); - rustc_middle::ty::TraitRef::new(tcx, trait_def_id, args) - } -} - #[derive(Clone, PartialEq, Eq, Hash, TyEncodable, TyDecodable, Debug)] pub enum TyKind { Indexed(BaseTy, Expr), @@ -814,16 +796,16 @@ pub type OpaqueArgsMap = FxHashMap; #[derive(PartialEq, Clone, Eq, Hash, TyEncodable, TyDecodable)] pub struct SimpleTy(Binder); -#[derive(PartialEq, Clone, Eq, Hash, TyEncodable, TyDecodable)] +#[derive(PartialEq, Clone, Eq, Hash, TyEncodable, TyDecodable, Debug)] struct SimpleTyInner { bty: BaseTy, pred: Expr, } impl SimpleTy { - pub fn new(bty: BaseTy, pred: Expr) -> Self { + pub fn new(bty: BaseTy, pred: impl Into) -> Self { let sort = bty.sort(); - SimpleTy(Binder::with_sort(SimpleTyInner { bty, pred }, sort)) + SimpleTy(Binder::with_sort(SimpleTyInner { bty, pred: pred.into() }, sort)) } pub fn sort(&self) -> Sort { @@ -835,9 +817,13 @@ impl SimpleTy { } pub fn as_ty_ctor(&self) -> Binder { - self.0 - .as_ref() - .map(|sty| Ty::constr(sty.pred.clone(), Ty::indexed(sty.bty.clone(), Expr::nu()))) + self.0.as_ref().map(|sty| { + if sty.pred.is_trivially_true() { + Ty::indexed(sty.bty.clone(), Expr::nu()) + } else { + Ty::constr(sty.pred.clone(), Ty::indexed(sty.bty.clone(), Expr::nu())) + } + }) } pub fn to_rustc<'tcx>(&self, tcx: TyCtxt<'tcx>) -> rustc_middle::ty::Ty<'tcx> { @@ -1594,11 +1580,12 @@ impl TyS { } } + #[track_caller] pub(crate) fn expect_tuple(&self) -> &[Ty] { if let TyKind::Indexed(BaseTy::Tuple(tys), _) = self.kind() { tys } else { - bug!("expected adt") + bug!("expected tuple found `{self:?}` (kind: `{:?}`)", self.kind()) } } @@ -2079,7 +2066,7 @@ mod pretty { let vars = &self.vars; cx.with_bound_vars(vars, || { if !vars.is_empty() { - cx.fmt_bound_vars("for<", vars, ">", f)?; + cx.fmt_bound_vars("for<", vars, "> ", f)?; } w!("{:?}", &self.value) }) diff --git a/crates/flux-middle/src/rty/projections.rs b/crates/flux-middle/src/rty/projections.rs index f66d7e51b7..d3c4d43290 100644 --- a/crates/flux-middle/src/rty/projections.rs +++ b/crates/flux-middle/src/rty/projections.rs @@ -311,7 +311,7 @@ impl TVarSubst { } GenericArg::Lifetime(dst) => self.infer_from_region(&src.as_region().unwrap(), dst), GenericArg::Base(ty) => { - todo!() + // todo!() // self.infer_from_ty(&src.as_type().unwrap(), ty.bty_skipping_binder()); } _ => (), From cbc20bd37528de7323c0c541c38a24ed40620265 Mon Sep 17 00:00:00 2001 From: Nico Lehmann Date: Thu, 15 Feb 2024 23:10:53 -0800 Subject: [PATCH 08/22] making progress --- crates/flux-fhir-analysis/src/conv.rs | 6 +- crates/flux-fhir-analysis/src/lib.rs | 4 +- crates/flux-metadata/src/lib.rs | 4 +- crates/flux-middle/src/cstore.rs | 2 +- crates/flux-middle/src/global_env.rs | 2 +- crates/flux-middle/src/queries.rs | 6 +- crates/flux-middle/src/rty/canonicalize.rs | 53 +++++------ crates/flux-middle/src/rty/fold.rs | 38 +++++--- crates/flux-middle/src/rty/mod.rs | 105 +++++++++++++++------ crates/flux-middle/src/rty/refining.rs | 81 ++++++++-------- crates/flux-middle/src/rty/subst.rs | 16 ++-- crates/flux-refineck/src/checker.rs | 10 +- 12 files changed, 193 insertions(+), 134 deletions(-) diff --git a/crates/flux-fhir-analysis/src/conv.rs b/crates/flux-fhir-analysis/src/conv.rs index 837bbd71cf..5157c4db9f 100644 --- a/crates/flux-fhir-analysis/src/conv.rs +++ b/crates/flux-fhir-analysis/src/conv.rs @@ -956,12 +956,12 @@ impl<'a, 'genv, 'tcx> ConvCtxt<'a, 'genv, 'tcx> { into.push(rty::GenericArg::Ty(self.conv_ty(env, ty)?)); } (fhir::GenericArg::Type(ty), rty::GenericParamDefKind::BaseTy) => { - let arg = self + let sty = self .conv_ty(env, ty)? .shallow_canonicalize() - .to_bty_arg() + .to_simple_ty() .unwrap(); - into.push(arg); + into.push(rty::GenericArg::Base(sty)); } _ => { bug!("unexpected param `{:?}` for arg `{arg:?}`", param.kind); diff --git a/crates/flux-fhir-analysis/src/lib.rs b/crates/flux-fhir-analysis/src/lib.rs index 38044cb22b..ebe95a4e32 100644 --- a/crates/flux-fhir-analysis/src/lib.rs +++ b/crates/flux-fhir-analysis/src/lib.rs @@ -291,7 +291,7 @@ fn refinement_generics_of( } } -fn type_of(genv: GlobalEnv, def_id: LocalDefId) -> QueryResult> { +fn type_of(genv: GlobalEnv, def_id: LocalDefId) -> QueryResult> { let ty = match genv.def_kind(def_id) { DefKind::TyAlias { .. } => { let alias = genv.map().expect_item(def_id).expect_type_alias(); @@ -310,7 +310,7 @@ fn type_of(genv: GlobalEnv, def_id: LocalDefId) -> QueryResult { let generics = genv.generics_of(def_id)?; let ty = genv.lower_type_of(def_id)?.skip_binder(); - Refiner::default(genv, &generics).refine_poly_ty(&ty)? + Refiner::default(genv, &generics).refine_ty_ctor(&ty)? } kind => { bug!("`{:?}` not supported", kind.descr(def_id.to_def_id())) diff --git a/crates/flux-metadata/src/lib.rs b/crates/flux-metadata/src/lib.rs index 101c0962a1..2a8dcf9095 100644 --- a/crates/flux-metadata/src/lib.rs +++ b/crates/flux-metadata/src/lib.rs @@ -49,7 +49,7 @@ pub struct CrateMetadata { fn_sigs: FxHashMap>, adts: FxHashMap, /// For now it only store type of aliases - type_of: FxHashMap>, + type_of: FxHashMap>, } #[derive(TyEncodable, TyDecodable)] @@ -98,7 +98,7 @@ impl CrateStore for CStore { .map(|adt| adt.variants.as_ref().map(rty::EarlyBinder::as_deref)) } - fn type_of(&self, def_id: DefId) -> Option<&rty::EarlyBinder> { + fn type_of(&self, def_id: DefId) -> Option<&rty::EarlyBinder> { self.meta.get(&def_id.krate)?.type_of.get(&def_id.index) } } diff --git a/crates/flux-middle/src/cstore.rs b/crates/flux-middle/src/cstore.rs index 5368d5d3f5..93b5d96c94 100644 --- a/crates/flux-middle/src/cstore.rs +++ b/crates/flux-middle/src/cstore.rs @@ -9,7 +9,7 @@ pub trait CrateStore { &self, def_id: DefId, ) -> Option>>; - fn type_of(&self, def_id: DefId) -> Option<&rty::EarlyBinder>; + fn type_of(&self, def_id: DefId) -> Option<&rty::EarlyBinder>; } pub type CrateStoreDyn = dyn CrateStore; diff --git a/crates/flux-middle/src/global_env.rs b/crates/flux-middle/src/global_env.rs index ab08971880..88015ce342 100644 --- a/crates/flux-middle/src/global_env.rs +++ b/crates/flux-middle/src/global_env.rs @@ -268,7 +268,7 @@ impl<'genv, 'tcx> GlobalEnv<'genv, 'tcx> { self.inner.queries.item_bounds(self, def_id) } - pub fn type_of(self, def_id: DefId) -> QueryResult> { + pub fn type_of(self, def_id: DefId) -> QueryResult> { self.inner.queries.type_of(self, def_id) } diff --git a/crates/flux-middle/src/queries.rs b/crates/flux-middle/src/queries.rs index efc7a4fed8..341cf8f882 100644 --- a/crates/flux-middle/src/queries.rs +++ b/crates/flux-middle/src/queries.rs @@ -56,7 +56,7 @@ pub struct Providers { FluxLocalDefId, ) -> QueryResult>>, pub adt_def: fn(GlobalEnv, LocalDefId) -> QueryResult, - pub type_of: fn(GlobalEnv, LocalDefId) -> QueryResult>, + pub type_of: fn(GlobalEnv, LocalDefId) -> QueryResult>, pub variants_of: fn( GlobalEnv, LocalDefId, @@ -129,7 +129,7 @@ pub struct Queries<'genv, 'tcx> { assoc_refinement_def: Cache<(DefId, Symbol), QueryResult>>, sort_of_assoc_reft: Cache<(DefId, Symbol), Option>>, item_bounds: Cache>>>, - type_of: Cache>>, + type_of: Cache>>, variants_of: Cache>>>, fn_sig: Cache>>, lower_late_bound_vars: Cache>>, @@ -443,7 +443,7 @@ impl<'genv, 'tcx> Queries<'genv, 'tcx> { &self, genv: GlobalEnv, def_id: DefId, - ) -> QueryResult> { + ) -> QueryResult> { run_with_cache(&self.type_of, def_id, || { if let Some(local_id) = def_id.as_local() { (self.providers.type_of)(genv, local_id) diff --git a/crates/flux-middle/src/rty/canonicalize.rs b/crates/flux-middle/src/rty/canonicalize.rs index c9816fdb51..12052136e7 100644 --- a/crates/flux-middle/src/rty/canonicalize.rs +++ b/crates/flux-middle/src/rty/canonicalize.rs @@ -3,7 +3,7 @@ use rustc_type_ir::{Mutability, INNERMOST}; use super::{ box_args, fold::{TypeFoldable, TypeFolder}, - BaseTy, Binder, BoundVariableKind, Expr, GenericArg, SimpleTy, Ty, TyKind, + BaseTy, Binder, BoundVariableKind, Expr, GenericArg, SimpleConstrTy, SimpleTy, Ty, TyKind, }; use crate::intern::List; @@ -68,7 +68,7 @@ impl Ty { let ty = hoister.hoist(self); let (vars, preds) = hoister.into_parts(); let pred = Expr::and(preds); - let constr_ty = ConstrTy { ty, pred }; + let constr_ty = CanonicalConstrTy { ty, pred }; if vars.is_empty() { CanonicalTy::Constr(constr_ty) } else { @@ -76,30 +76,36 @@ impl Ty { } } } +pub struct CanonicalConstrTy { + ty: Ty, + pred: Expr, +} pub enum CanonicalTy { - Exists(Binder), - Constr(ConstrTy), + Constr(CanonicalConstrTy), + Exists(Binder), } impl CanonicalTy { - pub fn to_bty_arg(&self) -> Option { + pub fn to_simple_ty(&self) -> Option { match self { - CanonicalTy::Exists(poly_constr_ty) => { - let constr_ty = poly_constr_ty.as_ref().skip_binder(); - if let TyKind::Indexed(bty, idx) = constr_ty.ty.kind() - && idx.is_nu() - { - let sty = SimpleTy::new(bty.clone(), &constr_ty.pred); - Some(GenericArg::Base(sty)) + CanonicalTy::Constr(constr) => { + if let TyKind::Indexed(bty, idx) = constr.ty.kind() { + let constr = SimpleConstrTy::new(bty.clone(), idx, &constr.pred); + Some(SimpleTy::Constr(constr)) } else { None } } - CanonicalTy::Constr(constr_ty) => { - if let TyKind::Indexed(bty, idx) = constr_ty.ty.kind() { - let sty = SimpleTy::new(bty.clone(), Expr::eq(Expr::nu(), idx)); - Some(GenericArg::Base(sty)) + CanonicalTy::Exists(poly_constr) => { + let constr = poly_constr.as_ref().skip_binder(); + if let TyKind::Indexed(bty, idx) = constr.ty.kind() + && idx.is_nu() + { + let poly_constr = poly_constr + .as_ref() + .map(|constr| SimpleConstrTy::new(bty.clone(), Expr::nu(), &constr.pred)); + Some(SimpleTy::Exists(poly_constr)) } else { None } @@ -107,18 +113,3 @@ impl CanonicalTy { } } } - -pub struct ConstrTy { - ty: Ty, - pred: Expr, -} - -impl ConstrTy { - pub fn to_ty(&self) -> Ty { - if self.pred.is_trivially_true() { - self.ty.clone() - } else { - Ty::constr(self.pred.clone(), self.ty.clone()) - } - } -} diff --git a/crates/flux-middle/src/rty/fold.rs b/crates/flux-middle/src/rty/fold.rs index adeb8f4dc9..8158e56b97 100644 --- a/crates/flux-middle/src/rty/fold.rs +++ b/crates/flux-middle/src/rty/fold.rs @@ -17,8 +17,8 @@ use super::{ AliasReft, AliasTy, BaseTy, BinOp, Binder, BoundVariableKind, Clause, ClauseKind, Constraint, CoroutineObligPredicate, Expr, ExprKind, FnOutput, FnSig, FnTraitPredicate, FuncSort, GenericArg, Invariant, KVar, Lambda, Name, OpaqueArgsMap, Opaqueness, OutlivesPredicate, - PolyFuncSort, ProjectionPredicate, PtrKind, Qualifier, ReLateBound, Region, SimpleTy, - SimpleTyInner, Sort, TraitPredicate, TraitRef, Ty, TyKind, + PolyFuncSort, ProjectionPredicate, PtrKind, Qualifier, ReLateBound, Region, SimpleConstrTy, + SimpleTy, Sort, TraitPredicate, TraitRef, Ty, TyKind, }; use crate::{ global_env::GlobalEnv, @@ -967,31 +967,41 @@ impl TypeFoldable for AliasTy { } } -impl TypeVisitable for SimpleTy { +impl TypeVisitable for SimpleConstrTy { fn visit_with(&self, visitor: &mut V) -> ControlFlow { - self.0.visit_with(visitor) + self.bty.visit_with(visitor)?; + self.idx.visit_with(visitor)?; + self.pred.visit_with(visitor) } } -impl TypeFoldable for SimpleTy { +impl TypeFoldable for SimpleConstrTy { fn try_fold_with(&self, folder: &mut F) -> Result { - Ok(SimpleTy(self.0.try_fold_with(folder)?)) + Ok(SimpleConstrTy { + bty: self.bty.try_fold_with(folder)?, + idx: self.idx.try_fold_with(folder)?, + pred: self.pred.try_fold_with(folder)?, + }) } } -impl TypeVisitable for SimpleTyInner { +impl TypeVisitable for SimpleTy { fn visit_with(&self, visitor: &mut V) -> ControlFlow { - self.bty.visit_with(visitor)?; - self.pred.visit_with(visitor) + match self { + SimpleTy::Constr(constr) => constr.visit_with(visitor), + SimpleTy::Exists(constr) => constr.visit_with(visitor), + } } } -impl TypeFoldable for SimpleTyInner { +impl TypeFoldable for SimpleTy { fn try_fold_with(&self, folder: &mut F) -> Result { - Ok(SimpleTyInner { - bty: self.bty.try_fold_with(folder)?, - pred: self.pred.try_fold_with(folder)?, - }) + match self { + SimpleTy::Constr(constr) => Ok(SimpleTy::Constr(constr.try_fold_with(folder)?)), + SimpleTy::Exists(poly_constr) => { + Ok(SimpleTy::Exists(poly_constr.try_fold_with(folder)?)) + } + } } } diff --git a/crates/flux-middle/src/rty/mod.rs b/crates/flux-middle/src/rty/mod.rs index de9b8412d6..79d1867d6d 100644 --- a/crates/flux-middle/src/rty/mod.rs +++ b/crates/flux-middle/src/rty/mod.rs @@ -554,7 +554,7 @@ pub struct ClosureOblig { pub oblig_sig: PolyFnSig, } -pub type PolyTy = Binder; +pub type TyCtor = Binder; pub type Ty = Interned; impl Ty { @@ -794,40 +794,97 @@ pub type RefineArgs = List; pub type OpaqueArgsMap = FxHashMap; #[derive(PartialEq, Clone, Eq, Hash, TyEncodable, TyDecodable)] -pub struct SimpleTy(Binder); - -#[derive(PartialEq, Clone, Eq, Hash, TyEncodable, TyDecodable, Debug)] -struct SimpleTyInner { +pub struct SimpleConstrTy { bty: BaseTy, + idx: Expr, pred: Expr, } +impl SimpleConstrTy { + pub fn new(bty: BaseTy, idx: impl Into, pred: impl Into) -> Self { + Self { bty, idx: idx.into(), pred: pred.into() } + } + + pub fn indexed(bty: BaseTy, idx: impl Into) -> Self { + Self::new(bty, idx, Expr::tt()) + } + + fn to_ty(&self) -> Ty { + let bty = self.bty.clone(); + if self.pred.is_trivially_true() { + Ty::indexed(bty, &self.idx) + } else { + Ty::constr(&self.pred, Ty::indexed(bty, &self.idx)) + } + } +} + +#[derive(PartialEq, Clone, Eq, Hash, TyEncodable, TyDecodable)] +pub enum SimpleTy { + Constr(SimpleConstrTy), + Exists(Binder), +} + impl SimpleTy { - pub fn new(bty: BaseTy, pred: impl Into) -> Self { - let sort = bty.sort(); - SimpleTy(Binder::with_sort(SimpleTyInner { bty, pred: pred.into() }, sort)) + fn indexed(bty: BaseTy, idx: impl Into) -> SimpleTy { + SimpleTy::Constr(SimpleConstrTy::indexed(bty, idx)) } - pub fn sort(&self) -> Sort { - self.0.vars().to_sort_list()[0].clone() + fn sort(&self) -> Sort { + self.bty_skipping_existential().sort() + } + + pub fn bty_skipping_existential(&self) -> &BaseTy { + match self { + SimpleTy::Exists(constr) => &constr.as_ref().skip_binder().bty, + SimpleTy::Constr(constr) => &constr.bty, + } } - pub fn bty_skipping_binder(&self) -> &BaseTy { - &self.0.as_ref().skip_binder().bty + pub fn to_ctor(&self) -> Binder { + match self { + SimpleTy::Constr(constr) => { + // given {b[e] | p} return λv. {b[v] | p ∧ v == e} + let sort = constr.bty.sort(); + let bty = constr.bty.shift_in_escaping(1); + let pred = constr.pred.shift_in_escaping(1); + let constr = SimpleConstrTy::new( + bty, + Expr::nu(), + Expr::and([pred, Expr::eq(Expr::nu(), &constr.idx)]), + ); + Binder::with_sort(constr, sort) + } + SimpleTy::Exists(poly_constr) => poly_constr.clone(), + } } - pub fn as_ty_ctor(&self) -> Binder { - self.0.as_ref().map(|sty| { - if sty.pred.is_trivially_true() { - Ty::indexed(sty.bty.clone(), Expr::nu()) - } else { - Ty::constr(sty.pred.clone(), Ty::indexed(sty.bty.clone(), Expr::nu())) + pub fn to_ty(&self) -> Ty { + match self { + SimpleTy::Constr(constr) => constr.to_ty(), + SimpleTy::Exists(poly_constr) => { + let sort = poly_constr.vars()[0].expect_sort(); + if sort.is_unit() { + poly_constr.replace_bound_reft(&Expr::unit()).to_ty() + } else if let Some(def_id) = sort.is_unit_adt() { + poly_constr + .replace_bound_reft(&Expr::unit_adt(def_id)) + .to_ty() + } else { + Ty::exists(poly_constr.as_ref().map(SimpleConstrTy::to_ty)) + } } - }) + } } pub fn to_rustc<'tcx>(&self, tcx: TyCtxt<'tcx>) -> rustc_middle::ty::Ty<'tcx> { - self.0.as_ref().skip_binder().bty.to_rustc(tcx) + self.bty_skipping_existential().to_rustc(tcx) + } +} + +impl From for SimpleTy { + fn from(v: SimpleConstrTy) -> Self { + Self::Constr(v) } } @@ -2386,13 +2443,7 @@ mod pretty { define_scoped!(cx, f); match self { GenericArg::Ty(arg) => w!("{:?}", arg), - GenericArg::Base(arg) => { - let ctor = arg.as_ty_ctor(); - cx.with_bound_vars(ctor.vars(), || { - cx.fmt_bound_vars("λ", ctor.vars(), ". ", f)?; - w!("{:?}", ctor.as_ref().skip_binder()) - }) - } + GenericArg::Base(arg) => w!("{:?}", arg.to_ty()), GenericArg::Lifetime(re) => w!("{:?}", re), GenericArg::Const(c) => w!("{:?}", c), } diff --git a/crates/flux-middle/src/rty/refining.rs b/crates/flux-middle/src/rty/refining.rs index a9b2b1686f..f86d7a7070 100644 --- a/crates/flux-middle/src/rty/refining.rs +++ b/crates/flux-middle/src/rty/refining.rs @@ -38,14 +38,14 @@ pub(crate) fn refine_generics(generics: &rustc::ty::Generics) -> QueryResult { genv: GlobalEnv<'genv, 'tcx>, generics: rty::Generics, - refine: fn(rty::BaseTy) -> rty::SimpleTy, + refine: fn(rty::BaseTy) -> rty::Binder, } impl<'genv, 'tcx> Refiner<'genv, 'tcx> { pub fn new( genv: GlobalEnv<'genv, 'tcx>, generics: &rty::Generics, - refine: fn(rty::BaseTy) -> rty::SimpleTy, + refine: fn(rty::BaseTy) -> rty::Binder, ) -> Self { Self { genv, generics: generics.clone(), refine } } @@ -59,7 +59,13 @@ impl<'genv, 'tcx> Refiner<'genv, 'tcx> { genv, generics: generics.clone(), refine: |bty| { - rty::SimpleTy::new(bty.shift_in_escaping(1), rty::Expr::hole(rty::HoleKind::Pred)) + let sort = bty.sort(); + let constr = rty::SimpleConstrTy::new( + bty.shift_in_escaping(1), + rty::Expr::nu(), + rty::Expr::hole(rty::HoleKind::Pred), + ); + rty::Binder::with_sort(constr, sort) }, } } @@ -221,10 +227,8 @@ impl<'genv, 'tcx> Refiner<'genv, 'tcx> { Ok(rty::GenericArg::Ty(self.refine_ty(ty)?)) } (rty::GenericParamDefKind::BaseTy, rustc::ty::GenericArg::Ty(ty)) => { - let TyOrSimple::Simple(ty) = self.refine_ty_inner(ty)? else { - bug!("unexpected ty") - }; - Ok(rty::GenericArg::Base(ty)) + let poly_constr = self.refine_ty_inner(ty)?.expect_simple(); + Ok(rty::GenericArg::Base(rty::SimpleTy::Exists(poly_constr))) } (rty::GenericParamDefKind::Lifetime, rustc::ty::GenericArg::Lifetime(re)) => { Ok(rty::GenericArg::Lifetime(*re)) @@ -263,22 +267,15 @@ impl<'genv, 'tcx> Refiner<'genv, 'tcx> { Ok(res) } - pub(crate) fn refine_ty(&self, ty: &rustc::ty::Ty) -> QueryResult { - let poly_ty = self.refine_poly_ty(ty)?; - let ty = match &poly_ty.vars()[..] { - [] => poly_ty.skip_binder().shift_out_escaping(1), - [rty::BoundVariableKind::Refine(s, ..)] => { - if s.is_unit() { - poly_ty.replace_bound_reft(&rty::Expr::unit()) - } else if let Some(def_id) = s.is_unit_adt() { - poly_ty.replace_bound_reft(&rty::Expr::unit_adt(def_id)) - } else { - rty::Ty::exists(poly_ty) - } - } - _ => rty::Ty::exists(poly_ty), - }; - Ok(ty) + pub fn refine_ty(&self, ty: &rustc::ty::Ty) -> QueryResult { + Ok(self.refine_ty_inner(ty)?.into_ty()) + } + + pub fn refine_ty_ctor(&self, ty: &rustc::ty::Ty) -> QueryResult { + Ok(self + .refine_ty_inner(ty)? + .expect_simple() + .map(|constr| constr.to_ty())) } fn refine_alias_kind(kind: &rustc::ty::AliasKind) -> rty::AliasKind { @@ -288,11 +285,7 @@ impl<'genv, 'tcx> Refiner<'genv, 'tcx> { } } - pub fn refine_poly_ty(&self, ty: &rustc::ty::Ty) -> QueryResult { - Ok(self.refine_ty_inner(ty)?.into_poly_ty()) - } - - fn refine_ty_inner(&self, ty: &rustc::ty::Ty) -> QueryResult { + fn refine_ty_inner(&self, ty: &rustc::ty::Ty) -> QueryResult { let bty = match ty.kind() { rustc::ty::TyKind::Closure(did, args) => { let args = args.as_closure(); @@ -330,7 +323,7 @@ impl<'genv, 'tcx> Refiner<'genv, 'tcx> { rustc::ty::TyKind::Param(param_ty) => { match self.param(*param_ty)?.kind { rty::GenericParamDefKind::Type { .. } | rty::GenericParamDefKind::SplTy => { - return Ok(TyOrSimple::Ty(rty::Ty::param(*param_ty))); + return Ok(RefineResult::Ty(rty::Ty::param(*param_ty))); } rty::GenericParamDefKind::BaseTy => rty::BaseTy::Param(*param_ty), rty::GenericParamDefKind::Lifetime | rty::GenericParamDefKind::Const { .. } => { @@ -348,7 +341,7 @@ impl<'genv, 'tcx> Refiner<'genv, 'tcx> { rustc::ty::TyKind::Alias(alias_kind, alias_ty) => { let kind = Self::refine_alias_kind(alias_kind); let alias_ty = self.refine_alias_ty(alias_kind, alias_ty)?; - return Ok(TyOrSimple::Ty(rty::Ty::alias(kind, alias_ty))); + return Ok(RefineResult::Ty(rty::Ty::alias(kind, alias_ty))); } rustc::ty::TyKind::Bool => rty::BaseTy::Bool, rustc::ty::TyKind::Int(int_ty) => rty::BaseTy::Int(*int_ty), @@ -361,7 +354,7 @@ impl<'genv, 'tcx> Refiner<'genv, 'tcx> { rty::BaseTy::RawPtr(self.as_default().refine_ty(ty)?, *mu) } }; - Ok(TyOrSimple::Simple((self.refine)(bty))) + Ok(RefineResult::Simple((self.refine)(bty))) } fn as_default(&self) -> Self { @@ -422,22 +415,32 @@ impl<'genv, 'tcx> Refiner<'genv, 'tcx> { } } -enum TyOrSimple { +enum RefineResult { Ty(rty::Ty), - Simple(rty::SimpleTy), + Simple(rty::Binder), } -impl TyOrSimple { - fn into_poly_ty(self) -> rty::PolyTy { +impl RefineResult { + fn into_ty(self) -> rty::Ty { match self { - TyOrSimple::Ty(ty) => rty::Binder::new(ty, List::empty()), - TyOrSimple::Simple(ty) => ty.as_ty_ctor(), + RefineResult::Ty(ty) => ty, + RefineResult::Simple(poly_constr) => rty::SimpleTy::Exists(poly_constr).to_ty(), + } + } + + fn expect_simple(self) -> rty::Binder { + if let RefineResult::Simple(poly_constr) = self { + poly_constr + } else { + bug!("unexpected ty") } } } -fn refine_default(bty: rty::BaseTy) -> rty::SimpleTy { - rty::SimpleTy::new(bty.shift_in_escaping(1), rty::Expr::tt()) +fn refine_default(bty: rty::BaseTy) -> rty::Binder { + let sort = bty.sort(); + let constr = rty::SimpleConstrTy::indexed(bty.shift_in_escaping(1), rty::Expr::nu()); + rty::Binder::with_sort(constr, sort) } pub fn refine_bound_variables( diff --git a/crates/flux-middle/src/rty/subst.rs b/crates/flux-middle/src/rty/subst.rs index 493e5ccb8b..4ec8a76327 100644 --- a/crates/flux-middle/src/rty/subst.rs +++ b/crates/flux-middle/src/rty/subst.rs @@ -72,7 +72,7 @@ impl RegionSubst { for (arg1, arg2) in iter::zip(args1, args2) { match (arg1, arg2) { (GenericArg::Base(ty1), ty::GenericArg::Ty(ty2)) => { - self.infer_from_bty(ty1.bty_skipping_binder(), ty2); + self.infer_from_bty(ty1.bty_skipping_existential(), ty2); } (GenericArg::Ty(ty1), ty::GenericArg::Ty(ty2)) => { self.infer_from_ty(ty1, ty2); @@ -253,7 +253,7 @@ pub(crate) struct GenericsSubstFolder<'a, D> { trait GenericsSubstDelegate { fn sort_for_param(&mut self, param_ty: ParamTy) -> Sort; fn ty_for_param(&mut self, param_ty: ParamTy) -> Ty; - fn bty_for_param(&mut self, param_ty: ParamTy, idx: &Expr) -> Ty; + fn bty_for_param(&mut self, param_ty: ParamTy, idx: &Expr) -> SimpleTy; fn region_for_param(&mut self, ebr: EarlyBoundRegion) -> Region; } @@ -273,8 +273,8 @@ impl GenericsSubstDelegate for IdentitySubstDelegate { Ty::param(param_ty) } - fn bty_for_param(&mut self, param_ty: ParamTy, idx: &Expr) -> Ty { - Ty::indexed(BaseTy::Param(param_ty), idx.clone()) + fn bty_for_param(&mut self, param_ty: ParamTy, idx: &Expr) -> SimpleTy { + SimpleTy::indexed(BaseTy::Param(param_ty), idx) } fn region_for_param(&mut self, ebr: EarlyBoundRegion) -> Region { @@ -301,9 +301,9 @@ impl GenericsSubstDelegate for GenericArgsDelegate<'_> { } } - fn bty_for_param(&mut self, param_ty: ParamTy, idx: &Expr) -> Ty { + fn bty_for_param(&mut self, param_ty: ParamTy, idx: &Expr) -> SimpleTy { match self.0.get(param_ty.index as usize) { - Some(GenericArg::Base(arg)) => arg.as_ty_ctor().replace_bound_reft(idx), + Some(GenericArg::Base(arg)) => arg.to_ctor().replace_bound_reft(idx).into(), Some(arg) => { bug!("expected base type for generic parameter, found `{:?}`", arg) } @@ -350,7 +350,7 @@ where bug!("unexpected type param {param_ty:?}"); } - fn bty_for_param(&mut self, param_ty: ParamTy, _idx: &Expr) -> Ty { + fn bty_for_param(&mut self, param_ty: ParamTy, _idx: &Expr) -> SimpleTy { bug!("unexpected base type param {param_ty:?}"); } @@ -386,7 +386,7 @@ impl TypeFolder for GenericsSubstFolder<'_, D> { TyKind::Param(param_ty) => self.delegate.ty_for_param(*param_ty), TyKind::Indexed(BaseTy::Param(param_ty), idx) => { let idx = idx.fold_with(self); - self.delegate.bty_for_param(*param_ty, &idx) + self.delegate.bty_for_param(*param_ty, &idx).to_ty() } _ => ty.super_fold_with(self), } diff --git a/crates/flux-refineck/src/checker.rs b/crates/flux-refineck/src/checker.rs index 4afd8a60be..94e9282380 100644 --- a/crates/flux-refineck/src/checker.rs +++ b/crates/flux-refineck/src/checker.rs @@ -1147,9 +1147,13 @@ fn instantiate_args_for_fun_call( let refiner = Refiner::new(genv, caller_generics, |bty| { let sort = bty.sort(); - let pred = - if !sort.is_unit() { rty::Expr::hole(rty::HoleKind::Pred) } else { rty::Expr::tt() }; - rty::SimpleTy::new(bty.shift_in_escaping(1), pred) + let bty = bty.shift_in_escaping(1); + let constr = if !sort.is_unit() { + rty::SimpleConstrTy::new(bty, Expr::nu(), Expr::hole(rty::HoleKind::Pred)) + } else { + rty::SimpleConstrTy::indexed(bty, Expr::nu()) + }; + Binder::with_sort(constr, sort) }); args.iter() From d9098af3003e25450a386862d4791e2bd4ee70a1 Mon Sep 17 00:00:00 2001 From: Nico Lehmann Date: Fri, 16 Feb 2024 08:32:29 -0800 Subject: [PATCH 09/22] Some fixes --- crates/flux-middle/src/pretty.rs | 4 +-- crates/flux-middle/src/rty/fold.rs | 24 +++++++++++++++++ crates/flux-middle/src/rty/mod.rs | 41 ++++++++++++++++++++++++----- crates/flux-middle/src/rty/subst.rs | 31 +++++++++++++++++----- 4 files changed, 84 insertions(+), 16 deletions(-) diff --git a/crates/flux-middle/src/pretty.rs b/crates/flux-middle/src/pretty.rs index f4fb892c2a..f43e773f71 100644 --- a/crates/flux-middle/src/pretty.rs +++ b/crates/flux-middle/src/pretty.rs @@ -175,7 +175,7 @@ struct Env { impl Env { fn lookup(&self, debruijn: DebruijnIndex, index: u32) -> Option { self.layers - .get(self.layers.len() - debruijn.as_usize() - 1)? + .get(self.layers.len().checked_sub(debruijn.as_usize() + 1)?)? .get(&index) .copied() } @@ -328,7 +328,7 @@ impl PrettyCx<'_> { if let Some(name) = self.env.borrow().lookup(debruijn, var.index) { w!("{name:?}") } else { - w!("(⭡{debruijn:?}.{})", ^var.index) + w!("⭡{}/#{}", ^debruijn.as_usize(), ^var.index) } } BoundReftKind::Named(name) => w!("{name}"), diff --git a/crates/flux-middle/src/rty/fold.rs b/crates/flux-middle/src/rty/fold.rs index 8158e56b97..2b19415f55 100644 --- a/crates/flux-middle/src/rty/fold.rs +++ b/crates/flux-middle/src/rty/fold.rs @@ -77,6 +77,13 @@ pub trait FallibleTypeFolder: Sized { bty.try_super_fold_with(self) } + fn try_fold_simple_constr_ty( + &mut self, + constr: &SimpleConstrTy, + ) -> Result { + constr.try_super_fold_with(self) + } + fn try_fold_region(&mut self, re: &Region) -> Result { Ok(*re) } @@ -103,6 +110,10 @@ pub trait TypeFolder: FallibleTypeFolder { bty.super_fold_with(self) } + fn fold_simple_constr_ty(&mut self, constr: &SimpleConstrTy) -> SimpleConstrTy { + constr.super_fold_with(self) + } + fn fold_region(&mut self, re: &Region) -> Region { *re } @@ -137,6 +148,13 @@ where Ok(self.fold_bty(bty)) } + fn try_fold_simple_constr_ty( + &mut self, + constr: &SimpleConstrTy, + ) -> Result { + Ok(self.fold_simple_constr_ty(constr)) + } + fn try_fold_region(&mut self, re: &Region) -> Result { Ok(self.fold_region(re)) } @@ -977,6 +995,12 @@ impl TypeVisitable for SimpleConstrTy { impl TypeFoldable for SimpleConstrTy { fn try_fold_with(&self, folder: &mut F) -> Result { + folder.try_fold_simple_constr_ty(self) + } +} + +impl TypeSuperFoldable for SimpleConstrTy { + fn try_super_fold_with(&self, folder: &mut F) -> Result { Ok(SimpleConstrTy { bty: self.bty.try_fold_with(folder)?, idx: self.idx.try_fold_with(folder)?, diff --git a/crates/flux-middle/src/rty/mod.rs b/crates/flux-middle/src/rty/mod.rs index 79d1867d6d..111b241fbe 100644 --- a/crates/flux-middle/src/rty/mod.rs +++ b/crates/flux-middle/src/rty/mod.rs @@ -795,9 +795,9 @@ pub type OpaqueArgsMap = FxHashMap; #[derive(PartialEq, Clone, Eq, Hash, TyEncodable, TyDecodable)] pub struct SimpleConstrTy { - bty: BaseTy, - idx: Expr, - pred: Expr, + pub bty: BaseTy, + pub idx: Expr, + pub pred: Expr, } impl SimpleConstrTy { @@ -809,6 +809,11 @@ impl SimpleConstrTy { Self::new(bty, idx, Expr::tt()) } + pub fn strengthen(&self, pred: impl Into) -> Self { + let this = self.clone(); + Self { bty: this.bty, idx: this.idx, pred: Expr::and([this.pred, pred.into()]) } + } + fn to_ty(&self) -> Ty { let bty = self.bty.clone(); if self.pred.is_trivially_true() { @@ -826,10 +831,6 @@ pub enum SimpleTy { } impl SimpleTy { - fn indexed(bty: BaseTy, idx: impl Into) -> SimpleTy { - SimpleTy::Constr(SimpleConstrTy::indexed(bty, idx)) - } - fn sort(&self) -> Sort { self.bty_skipping_existential().sort() } @@ -2259,6 +2260,30 @@ mod pretty { } } + impl Pretty for SimpleTy { + fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result { + define_scoped!(cx, f); + match self { + SimpleTy::Constr(constr) => { + w!("{:?}", constr) + } + SimpleTy::Exists(poly_constr) => { + cx.with_bound_vars(poly_constr.vars(), || { + cx.fmt_bound_vars("∃", poly_constr.vars(), ". ", f)?; + w!("{:?}", &poly_constr.value) + }) + } + } + } + } + + impl Pretty for SimpleConstrTy { + fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result { + define_scoped!(cx, f); + w!("{{ {:?}[{:?}] | {:?} }}", &self.bty, &self.idx, &self.pred) + } + } + impl Pretty for TyS { fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result { define_scoped!(cx, f); @@ -2482,5 +2507,7 @@ mod pretty { PtrKind, FuncSort, SortCtor, + SimpleTy, + SimpleConstrTy, ); } diff --git a/crates/flux-middle/src/rty/subst.rs b/crates/flux-middle/src/rty/subst.rs index 4ec8a76327..7bd2750c90 100644 --- a/crates/flux-middle/src/rty/subst.rs +++ b/crates/flux-middle/src/rty/subst.rs @@ -253,7 +253,7 @@ pub(crate) struct GenericsSubstFolder<'a, D> { trait GenericsSubstDelegate { fn sort_for_param(&mut self, param_ty: ParamTy) -> Sort; fn ty_for_param(&mut self, param_ty: ParamTy) -> Ty; - fn bty_for_param(&mut self, param_ty: ParamTy, idx: &Expr) -> SimpleTy; + fn ctor_for_param(&mut self, param_ty: ParamTy) -> Binder; fn region_for_param(&mut self, ebr: EarlyBoundRegion) -> Region; } @@ -273,8 +273,11 @@ impl GenericsSubstDelegate for IdentitySubstDelegate { Ty::param(param_ty) } - fn bty_for_param(&mut self, param_ty: ParamTy, idx: &Expr) -> SimpleTy { - SimpleTy::indexed(BaseTy::Param(param_ty), idx) + fn ctor_for_param(&mut self, param_ty: ParamTy) -> Binder { + Binder::with_sort( + SimpleConstrTy::indexed(BaseTy::Param(param_ty), Expr::nu()), + Sort::Param(param_ty), + ) } fn region_for_param(&mut self, ebr: EarlyBoundRegion) -> Region { @@ -301,9 +304,9 @@ impl GenericsSubstDelegate for GenericArgsDelegate<'_> { } } - fn bty_for_param(&mut self, param_ty: ParamTy, idx: &Expr) -> SimpleTy { + fn ctor_for_param(&mut self, param_ty: ParamTy) -> Binder { match self.0.get(param_ty.index as usize) { - Some(GenericArg::Base(arg)) => arg.to_ctor().replace_bound_reft(idx).into(), + Some(GenericArg::Base(arg)) => arg.to_ctor(), Some(arg) => { bug!("expected base type for generic parameter, found `{:?}`", arg) } @@ -350,7 +353,7 @@ where bug!("unexpected type param {param_ty:?}"); } - fn bty_for_param(&mut self, param_ty: ParamTy, _idx: &Expr) -> SimpleTy { + fn ctor_for_param(&mut self, param_ty: ParamTy) -> Binder { bug!("unexpected base type param {param_ty:?}"); } @@ -386,12 +389,26 @@ impl TypeFolder for GenericsSubstFolder<'_, D> { TyKind::Param(param_ty) => self.delegate.ty_for_param(*param_ty), TyKind::Indexed(BaseTy::Param(param_ty), idx) => { let idx = idx.fold_with(self); - self.delegate.bty_for_param(*param_ty, &idx).to_ty() + self.delegate + .ctor_for_param(*param_ty) + .replace_bound_reft(&idx) + .to_ty() } _ => ty.super_fold_with(self), } } + fn fold_simple_constr_ty(&mut self, constr: &SimpleConstrTy) -> SimpleConstrTy { + if let BaseTy::Param(param_ty) = &constr.bty { + self.delegate + .ctor_for_param(*param_ty) + .replace_bound_reft(&constr.idx) + .strengthen(&constr.pred) + } else { + constr.super_fold_with(self) + } + } + fn fold_region(&mut self, re: &Region) -> Region { if let ReEarlyBound(ebr) = *re { self.delegate.region_for_param(ebr) From d6df7dd8bb90191063287a283a9fa38cb0ba7a4b Mon Sep 17 00:00:00 2001 From: Nico Lehmann Date: Fri, 16 Feb 2024 10:03:41 -0800 Subject: [PATCH 10/22] Clean up refining of generic args --- crates/flux-middle/src/global_env.rs | 21 +----- crates/flux-middle/src/rty/refining.rs | 96 +++++++++--------------- crates/flux-middle/src/rustc/lowering.rs | 12 ++- 3 files changed, 46 insertions(+), 83 deletions(-) diff --git a/crates/flux-middle/src/global_env.rs b/crates/flux-middle/src/global_env.rs index 88015ce342..481abc0109 100644 --- a/crates/flux-middle/src/global_env.rs +++ b/crates/flux-middle/src/global_env.rs @@ -213,12 +213,10 @@ impl<'genv, 'tcx> GlobalEnv<'genv, 'tcx> { let Some(poly_trait_ref) = self.tcx().impl_trait_ref(impl_id) else { return Ok(None) }; - let impl_generics = self.generics_of(impl_id)?; - let trait_ref = poly_trait_ref.skip_binder(); - let args = lowering::lower_generic_args(self.tcx(), trait_ref.args) + let trait_ref = lowering::lower_trait_ref(self.tcx(), poly_trait_ref.skip_binder()) .map_err(|err| QueryErr::unsupported(self.tcx(), impl_id, err.into_err()))?; - let args = self.refine_default_generic_args(&impl_generics, &args)?; - let trait_ref = rty::TraitRef { def_id: trait_ref.def_id, args }; + let trait_generics = self.generics_of(trait_ref.def_id)?; + let trait_ref = Refiner::default(self, &trait_generics).refine_trait_ref(&trait_ref)?; Ok(Some(rty::EarlyBinder(trait_ref))) } @@ -322,19 +320,6 @@ impl<'genv, 'tcx> GlobalEnv<'genv, 'tcx> { generics.param_def_id_to_index[&def_id.to_def_id()] } - pub fn refine_default_generic_args( - self, - generics: &rty::Generics, - args: &ty::GenericArgs, - ) -> QueryResult { - let refiner = Refiner::default(self, generics); - let mut res = vec![]; - for arg in args { - res.push(refiner.refine_generic_arg_raw(arg)?); - } - Ok(res.into()) - } - pub fn refine_default( self, generics: &rty::Generics, diff --git a/crates/flux-middle/src/rty/refining.rs b/crates/flux-middle/src/rty/refining.rs index f86d7a7070..307ede7af1 100644 --- a/crates/flux-middle/src/rty/refining.rs +++ b/crates/flux-middle/src/rty/refining.rs @@ -116,12 +116,12 @@ impl<'genv, 'tcx> Refiner<'genv, 'tcx> { &rustc::ty::AliasKind::Projection, &proj_pred.projection_ty, )?, - term: self.as_default().refine_ty(&proj_pred.term)?, + term: self.refine_ty(&proj_pred.term)?, }; rty::ClauseKind::Projection(pred) } rustc::ty::ClauseKind::TypeOutlives(pred) => { - let pred = rty::OutlivesPredicate(self.as_default().refine_ty(&pred.0)?, pred.1); + let pred = rty::OutlivesPredicate(self.refine_ty(&pred.0)?, pred.1); rty::ClauseKind::TypeOutlives(pred) } }; @@ -156,14 +156,13 @@ impl<'genv, 'tcx> Refiner<'genv, 'tcx> { Ok(rty::ClauseKind::FnTrait(pred)) } - fn refine_trait_ref(&self, trait_ref: &rustc::ty::TraitRef) -> QueryResult { + pub(crate) fn refine_trait_ref( + &self, + trait_ref: &rustc::ty::TraitRef, + ) -> QueryResult { let trait_ref = rty::TraitRef { def_id: trait_ref.def_id, - args: trait_ref - .args - .iter() - .map(|arg| self.refine_generic_arg_raw(arg)) - .try_collect()?, + args: self.refine_generic_args(trait_ref.def_id, &trait_ref.args)?, }; Ok(trait_ref) } @@ -214,6 +213,20 @@ impl<'genv, 'tcx> Refiner<'genv, 'tcx> { }) } + fn refine_generic_args( + &self, + def_id: DefId, + args: &rustc::ty::GenericArgs, + ) -> QueryResult { + let generics = self.generics_of(def_id)?; + let mut result = vec![]; + for (idx, arg) in args.iter().enumerate() { + let param = generics.param_at(idx, self.genv)?; + result.push(self.refine_generic_arg(¶m, arg)?); + } + Ok(List::from_vec(result)) + } + pub fn refine_generic_arg( &self, param: &rty::GenericParamDef, @@ -240,26 +253,13 @@ impl<'genv, 'tcx> Refiner<'genv, 'tcx> { } } - pub(crate) fn refine_generic_arg_raw( - &self, - arg: &rustc::ty::GenericArg, - ) -> QueryResult { - match arg { - rustc::ty::GenericArg::Ty(ty) => Ok(rty::GenericArg::Ty(self.refine_ty(ty)?)), - rustc::ty::GenericArg::Lifetime(re) => Ok(rty::GenericArg::Lifetime(*re)), - rustc::ty::GenericArg::Const(c) => Ok(rty::GenericArg::Const(c.clone())), - } - } - - pub(crate) fn refine_alias_ty( + fn refine_alias_ty( &self, alias_kind: &rustc::ty::AliasKind, alias_ty: &rustc::ty::AliasTy, ) -> QueryResult { let def_id = alias_ty.def_id; - let args = self.iter_with_generics_of(def_id, &alias_ty.args, |param, arg| { - self.as_default().refine_generic_arg(param, arg) - })?; + let args = self.refine_generic_args(def_id, &alias_ty.args)?; let refine_args = self.refine_args_of(def_id, alias_kind)?; @@ -285,7 +285,7 @@ impl<'genv, 'tcx> Refiner<'genv, 'tcx> { } } - fn refine_ty_inner(&self, ty: &rustc::ty::Ty) -> QueryResult { + fn refine_ty_inner(&self, ty: &rustc::ty::Ty) -> QueryResult { let bty = match ty.kind() { rustc::ty::TyKind::Closure(did, args) => { let args = args.as_closure(); @@ -323,7 +323,7 @@ impl<'genv, 'tcx> Refiner<'genv, 'tcx> { rustc::ty::TyKind::Param(param_ty) => { match self.param(*param_ty)?.kind { rty::GenericParamDefKind::Type { .. } | rty::GenericParamDefKind::SplTy => { - return Ok(RefineResult::Ty(rty::Ty::param(*param_ty))); + return Ok(TyOrSimple::Ty(rty::Ty::param(*param_ty))); } rty::GenericParamDefKind::BaseTy => rty::BaseTy::Param(*param_ty), rty::GenericParamDefKind::Lifetime | rty::GenericParamDefKind::Const { .. } => { @@ -333,15 +333,13 @@ impl<'genv, 'tcx> Refiner<'genv, 'tcx> { } rustc::ty::TyKind::Adt(adt_def, args) => { let adt_def = self.genv.adt_def(adt_def.did())?; - let args = self.iter_with_generics_of(adt_def.did(), args, |param, arg| { - self.refine_generic_arg(param, arg) - })?; + let args = self.refine_generic_args(adt_def.did(), args)?; rty::BaseTy::adt(adt_def, args) } rustc::ty::TyKind::Alias(alias_kind, alias_ty) => { let kind = Self::refine_alias_kind(alias_kind); - let alias_ty = self.refine_alias_ty(alias_kind, alias_ty)?; - return Ok(RefineResult::Ty(rty::Ty::alias(kind, alias_ty))); + let alias_ty = self.as_default().refine_alias_ty(alias_kind, alias_ty)?; + return Ok(TyOrSimple::Ty(rty::Ty::alias(kind, alias_ty))); } rustc::ty::TyKind::Bool => rty::BaseTy::Bool, rustc::ty::TyKind::Int(int_ty) => rty::BaseTy::Int(*int_ty), @@ -354,7 +352,7 @@ impl<'genv, 'tcx> Refiner<'genv, 'tcx> { rty::BaseTy::RawPtr(self.as_default().refine_ty(ty)?, *mu) } }; - Ok(RefineResult::Simple((self.refine)(bty))) + Ok(TyOrSimple::Simple((self.refine)(bty))) } fn as_default(&self) -> Self { @@ -385,51 +383,27 @@ impl<'genv, 'tcx> Refiner<'genv, 'tcx> { } } - fn iter_with_generics_of( - &self, - def_id: DefId, - args: &[rustc::ty::GenericArg], - f: impl FnMut(&rty::GenericParamDef, &rustc::ty::GenericArg) -> QueryResult, - ) -> QueryResult { - let generics = self.generics_of(def_id)?; - self.iter_with_generic_params(&generics, args, f) - } - - fn iter_with_generic_params( - &self, - generics: &rty::Generics, - args: &[rustc::ty::GenericArg], - mut f: impl FnMut(&rty::GenericParamDef, &rustc::ty::GenericArg) -> QueryResult, - ) -> QueryResult { - args.iter() - .enumerate() - .map(|(idx, arg)| { - let param = generics.param_at(idx, self.genv)?; - f(¶m, arg) - }) - .try_collect() - } - fn param(&self, param_ty: ParamTy) -> QueryResult { self.generics.param_at(param_ty.index as usize, self.genv) } } -enum RefineResult { +enum TyOrSimple { Ty(rty::Ty), Simple(rty::Binder), } -impl RefineResult { +impl TyOrSimple { fn into_ty(self) -> rty::Ty { match self { - RefineResult::Ty(ty) => ty, - RefineResult::Simple(poly_constr) => rty::SimpleTy::Exists(poly_constr).to_ty(), + TyOrSimple::Ty(ty) => ty, + TyOrSimple::Simple(poly_constr) => rty::SimpleTy::Exists(poly_constr).to_ty(), } } + #[track_caller] fn expect_simple(self) -> rty::Binder { - if let RefineResult::Simple(poly_constr) = self { + if let TyOrSimple::Simple(poly_constr) = self { poly_constr } else { bug!("unexpected ty") diff --git a/crates/flux-middle/src/rustc/lowering.rs b/crates/flux-middle/src/rustc/lowering.rs index 373d40db1f..611a14811d 100644 --- a/crates/flux-middle/src/rustc/lowering.rs +++ b/crates/flux-middle/src/rustc/lowering.rs @@ -865,10 +865,7 @@ fn lower_clause<'tcx>( let kind = match kind { rustc_ty::ClauseKind::Trait(trait_pred) => { ClauseKind::Trait(TraitPredicate { - trait_ref: TraitRef { - def_id: trait_pred.trait_ref.def_id, - args: lower_generic_args(tcx, trait_pred.trait_ref.args)?, - }, + trait_ref: lower_trait_ref(tcx, trait_pred.trait_ref)?, }) } rustc_ty::ClauseKind::Projection(proj_pred) => { @@ -894,6 +891,13 @@ fn lower_clause<'tcx>( Ok(Clause::new(kind)) } +pub(crate) fn lower_trait_ref<'tcx>( + tcx: TyCtxt<'tcx>, + trait_ref: rustc_ty::TraitRef<'tcx>, +) -> Result { + Ok(TraitRef { def_id: trait_ref.def_id, args: lower_generic_args(tcx, trait_ref.args)? }) +} + fn lower_type_outlives<'tcx>( tcx: TyCtxt<'tcx>, pred: rustc_ty::TypeOutlivesPredicate<'tcx>, From e79091d2471c55881c4d931561a0b6970ed88ddb Mon Sep 17 00:00:00 2001 From: Nico Lehmann Date: Fri, 16 Feb 2024 10:45:31 -0800 Subject: [PATCH 11/22] Simplify SimpleTy --- crates/flux-fhir-analysis/src/conv.rs | 2 +- crates/flux-middle/src/rty/canonicalize.rs | 22 ++-- crates/flux-middle/src/rty/fold.rs | 48 ++------ crates/flux-middle/src/rty/mod.rs | 134 +++++++-------------- crates/flux-middle/src/rty/refining.rs | 34 +++--- crates/flux-middle/src/rty/subst.rs | 18 +-- crates/flux-refineck/src/checker.rs | 4 +- 7 files changed, 99 insertions(+), 163 deletions(-) diff --git a/crates/flux-fhir-analysis/src/conv.rs b/crates/flux-fhir-analysis/src/conv.rs index 5157c4db9f..5853359853 100644 --- a/crates/flux-fhir-analysis/src/conv.rs +++ b/crates/flux-fhir-analysis/src/conv.rs @@ -959,7 +959,7 @@ impl<'a, 'genv, 'tcx> ConvCtxt<'a, 'genv, 'tcx> { let sty = self .conv_ty(env, ty)? .shallow_canonicalize() - .to_simple_ty() + .to_simple_ty_ctor() .unwrap(); into.push(rty::GenericArg::Base(sty)); } diff --git a/crates/flux-middle/src/rty/canonicalize.rs b/crates/flux-middle/src/rty/canonicalize.rs index 12052136e7..fc28dbeb85 100644 --- a/crates/flux-middle/src/rty/canonicalize.rs +++ b/crates/flux-middle/src/rty/canonicalize.rs @@ -3,7 +3,7 @@ use rustc_type_ir::{Mutability, INNERMOST}; use super::{ box_args, fold::{TypeFoldable, TypeFolder}, - BaseTy, Binder, BoundVariableKind, Expr, GenericArg, SimpleConstrTy, SimpleTy, Ty, TyKind, + BaseTy, Binder, BoundVariableKind, Expr, GenericArg, SimpleTy, SimpleTyCtor, Ty, TyKind, }; use crate::intern::List; @@ -87,12 +87,20 @@ pub enum CanonicalTy { } impl CanonicalTy { - pub fn to_simple_ty(&self) -> Option { + pub fn to_simple_ty_ctor(&self) -> Option { match self { CanonicalTy::Constr(constr) => { if let TyKind::Indexed(bty, idx) = constr.ty.kind() { - let constr = SimpleConstrTy::new(bty.clone(), idx, &constr.pred); - Some(SimpleTy::Constr(constr)) + // given {b[e] | p} return λv. {b[v] | p ∧ v == e} + let sort = bty.sort(); + let bty = bty.shift_in_escaping(1); + let pred = constr.pred.shift_in_escaping(1); + let constr = SimpleTy::new( + bty, + Expr::nu(), + Expr::and([pred, Expr::eq(Expr::nu(), idx)]), + ); + Some(Binder::with_sort(constr, sort)) } else { None } @@ -102,10 +110,10 @@ impl CanonicalTy { if let TyKind::Indexed(bty, idx) = constr.ty.kind() && idx.is_nu() { - let poly_constr = poly_constr + let ctor = poly_constr .as_ref() - .map(|constr| SimpleConstrTy::new(bty.clone(), Expr::nu(), &constr.pred)); - Some(SimpleTy::Exists(poly_constr)) + .map(|constr| SimpleTy::new(bty.clone(), Expr::nu(), &constr.pred)); + Some(ctor) } else { None } diff --git a/crates/flux-middle/src/rty/fold.rs b/crates/flux-middle/src/rty/fold.rs index 2b19415f55..36a3f74596 100644 --- a/crates/flux-middle/src/rty/fold.rs +++ b/crates/flux-middle/src/rty/fold.rs @@ -17,8 +17,8 @@ use super::{ AliasReft, AliasTy, BaseTy, BinOp, Binder, BoundVariableKind, Clause, ClauseKind, Constraint, CoroutineObligPredicate, Expr, ExprKind, FnOutput, FnSig, FnTraitPredicate, FuncSort, GenericArg, Invariant, KVar, Lambda, Name, OpaqueArgsMap, Opaqueness, OutlivesPredicate, - PolyFuncSort, ProjectionPredicate, PtrKind, Qualifier, ReLateBound, Region, SimpleConstrTy, - SimpleTy, Sort, TraitPredicate, TraitRef, Ty, TyKind, + PolyFuncSort, ProjectionPredicate, PtrKind, Qualifier, ReLateBound, Region, SimpleTy, Sort, + TraitPredicate, TraitRef, Ty, TyKind, }; use crate::{ global_env::GlobalEnv, @@ -77,10 +77,7 @@ pub trait FallibleTypeFolder: Sized { bty.try_super_fold_with(self) } - fn try_fold_simple_constr_ty( - &mut self, - constr: &SimpleConstrTy, - ) -> Result { + fn try_fold_simple_ty(&mut self, constr: &SimpleTy) -> Result { constr.try_super_fold_with(self) } @@ -110,7 +107,7 @@ pub trait TypeFolder: FallibleTypeFolder { bty.super_fold_with(self) } - fn fold_simple_constr_ty(&mut self, constr: &SimpleConstrTy) -> SimpleConstrTy { + fn fold_simple_ty(&mut self, constr: &SimpleTy) -> SimpleTy { constr.super_fold_with(self) } @@ -148,11 +145,8 @@ where Ok(self.fold_bty(bty)) } - fn try_fold_simple_constr_ty( - &mut self, - constr: &SimpleConstrTy, - ) -> Result { - Ok(self.fold_simple_constr_ty(constr)) + fn try_fold_simple_ty(&mut self, constr: &SimpleTy) -> Result { + Ok(self.fold_simple_ty(constr)) } fn try_fold_region(&mut self, re: &Region) -> Result { @@ -985,7 +979,7 @@ impl TypeFoldable for AliasTy { } } -impl TypeVisitable for SimpleConstrTy { +impl TypeVisitable for SimpleTy { fn visit_with(&self, visitor: &mut V) -> ControlFlow { self.bty.visit_with(visitor)?; self.idx.visit_with(visitor)?; @@ -993,15 +987,15 @@ impl TypeVisitable for SimpleConstrTy { } } -impl TypeFoldable for SimpleConstrTy { +impl TypeFoldable for SimpleTy { fn try_fold_with(&self, folder: &mut F) -> Result { - folder.try_fold_simple_constr_ty(self) + folder.try_fold_simple_ty(self) } } -impl TypeSuperFoldable for SimpleConstrTy { +impl TypeSuperFoldable for SimpleTy { fn try_super_fold_with(&self, folder: &mut F) -> Result { - Ok(SimpleConstrTy { + Ok(SimpleTy { bty: self.bty.try_fold_with(folder)?, idx: self.idx.try_fold_with(folder)?, pred: self.pred.try_fold_with(folder)?, @@ -1009,26 +1003,6 @@ impl TypeSuperFoldable for SimpleConstrTy { } } -impl TypeVisitable for SimpleTy { - fn visit_with(&self, visitor: &mut V) -> ControlFlow { - match self { - SimpleTy::Constr(constr) => constr.visit_with(visitor), - SimpleTy::Exists(constr) => constr.visit_with(visitor), - } - } -} - -impl TypeFoldable for SimpleTy { - fn try_fold_with(&self, folder: &mut F) -> Result { - match self { - SimpleTy::Constr(constr) => Ok(SimpleTy::Constr(constr.try_fold_with(folder)?)), - SimpleTy::Exists(poly_constr) => { - Ok(SimpleTy::Exists(poly_constr.try_fold_with(folder)?)) - } - } - } -} - impl TypeVisitable for GenericArg { fn visit_with(&self, visitor: &mut V) -> ControlFlow { match self { diff --git a/crates/flux-middle/src/rty/mod.rs b/crates/flux-middle/src/rty/mod.rs index 111b241fbe..a5c95e20e8 100644 --- a/crates/flux-middle/src/rty/mod.rs +++ b/crates/flux-middle/src/rty/mod.rs @@ -793,14 +793,33 @@ pub type RefineArgs = List; pub type OpaqueArgsMap = FxHashMap; +type SimpleTyCtor = Binder; + +impl SimpleTyCtor { + pub fn as_bty_skipping_binder(&self) -> &BaseTy { + &self.as_ref().skip_binder().bty + } + + pub fn to_ty(&self) -> Ty { + let sort = self.sort(); + if sort.is_unit() { + self.replace_bound_reft(&Expr::unit()).to_ty() + } else if let Some(def_id) = sort.is_unit_adt() { + self.replace_bound_reft(&Expr::unit_adt(def_id)).to_ty() + } else { + Ty::exists(self.as_ref().map(SimpleTy::to_ty)) + } + } +} + #[derive(PartialEq, Clone, Eq, Hash, TyEncodable, TyDecodable)] -pub struct SimpleConstrTy { +pub struct SimpleTy { pub bty: BaseTy, pub idx: Expr, pub pred: Expr, } -impl SimpleConstrTy { +impl SimpleTy { pub fn new(bty: BaseTy, idx: impl Into, pred: impl Into) -> Self { Self { bty, idx: idx.into(), pred: pred.into() } } @@ -814,6 +833,10 @@ impl SimpleConstrTy { Self { bty: this.bty, idx: this.idx, pred: Expr::and([this.pred, pred.into()]) } } + fn to_rustc<'tcx>(&self, tcx: TyCtxt<'tcx>) -> rustc_middle::ty::Ty<'tcx> { + self.bty.to_rustc(tcx) + } + fn to_ty(&self) -> Ty { let bty = self.bty.clone(); if self.pred.is_trivially_true() { @@ -824,75 +847,10 @@ impl SimpleConstrTy { } } -#[derive(PartialEq, Clone, Eq, Hash, TyEncodable, TyDecodable)] -pub enum SimpleTy { - Constr(SimpleConstrTy), - Exists(Binder), -} - -impl SimpleTy { - fn sort(&self) -> Sort { - self.bty_skipping_existential().sort() - } - - pub fn bty_skipping_existential(&self) -> &BaseTy { - match self { - SimpleTy::Exists(constr) => &constr.as_ref().skip_binder().bty, - SimpleTy::Constr(constr) => &constr.bty, - } - } - - pub fn to_ctor(&self) -> Binder { - match self { - SimpleTy::Constr(constr) => { - // given {b[e] | p} return λv. {b[v] | p ∧ v == e} - let sort = constr.bty.sort(); - let bty = constr.bty.shift_in_escaping(1); - let pred = constr.pred.shift_in_escaping(1); - let constr = SimpleConstrTy::new( - bty, - Expr::nu(), - Expr::and([pred, Expr::eq(Expr::nu(), &constr.idx)]), - ); - Binder::with_sort(constr, sort) - } - SimpleTy::Exists(poly_constr) => poly_constr.clone(), - } - } - - pub fn to_ty(&self) -> Ty { - match self { - SimpleTy::Constr(constr) => constr.to_ty(), - SimpleTy::Exists(poly_constr) => { - let sort = poly_constr.vars()[0].expect_sort(); - if sort.is_unit() { - poly_constr.replace_bound_reft(&Expr::unit()).to_ty() - } else if let Some(def_id) = sort.is_unit_adt() { - poly_constr - .replace_bound_reft(&Expr::unit_adt(def_id)) - .to_ty() - } else { - Ty::exists(poly_constr.as_ref().map(SimpleConstrTy::to_ty)) - } - } - } - } - - pub fn to_rustc<'tcx>(&self, tcx: TyCtxt<'tcx>) -> rustc_middle::ty::Ty<'tcx> { - self.bty_skipping_existential().to_rustc(tcx) - } -} - -impl From for SimpleTy { - fn from(v: SimpleConstrTy) -> Self { - Self::Constr(v) - } -} - #[derive(PartialEq, Clone, Eq, Hash, TyEncodable, TyDecodable)] pub enum GenericArg { Ty(Ty), - Base(SimpleTy), + Base(SimpleTyCtor), Lifetime(Region), Const(Const), } @@ -909,7 +867,7 @@ impl GenericArg { pub fn peel_out_sort(&self) -> Option { match self { GenericArg::Ty(ty) => ty.as_bty_skipping_existentials().map(BaseTy::sort), - GenericArg::Base(ty) => Some(ty.sort()), + GenericArg::Base(ctor) => Some(ctor.sort()), GenericArg::Lifetime(_) | GenericArg::Const(_) => None, } } @@ -949,7 +907,9 @@ impl GenericArg { use rustc_middle::ty; match self { GenericArg::Ty(ty) => ty::GenericArg::from(ty.to_rustc(tcx)), - GenericArg::Base(ty) => ty::GenericArg::from(ty.to_rustc(tcx)), + GenericArg::Base(ctor) => { + ty::GenericArg::from(ctor.as_ref().skip_binder().to_rustc(tcx)) + } GenericArg::Lifetime(re) => ty::GenericArg::from(re.to_rustc(tcx)), GenericArg::Const(_) => todo!(), } @@ -1251,6 +1211,13 @@ impl Binder { pub fn try_map(self, f: impl FnOnce(T) -> Result) -> Result, E> { Ok(Binder { vars: self.vars, value: f(self.value)? }) } + + pub fn sort(&self) -> Sort { + match &self.vars[..] { + [BoundVariableKind::Refine(sort, ..)] => sort.clone(), + _ => bug!("expected single-sorted binder"), + } + } } impl List { @@ -2261,23 +2228,6 @@ mod pretty { } impl Pretty for SimpleTy { - fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result { - define_scoped!(cx, f); - match self { - SimpleTy::Constr(constr) => { - w!("{:?}", constr) - } - SimpleTy::Exists(poly_constr) => { - cx.with_bound_vars(poly_constr.vars(), || { - cx.fmt_bound_vars("∃", poly_constr.vars(), ". ", f)?; - w!("{:?}", &poly_constr.value) - }) - } - } - } - } - - impl Pretty for SimpleConstrTy { fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result { define_scoped!(cx, f); w!("{{ {:?}[{:?}] | {:?} }}", &self.bty, &self.idx, &self.pred) @@ -2467,8 +2417,13 @@ mod pretty { fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result { define_scoped!(cx, f); match self { - GenericArg::Ty(arg) => w!("{:?}", arg), - GenericArg::Base(arg) => w!("{:?}", arg.to_ty()), + GenericArg::Ty(ty) => w!("{:?}", ty), + GenericArg::Base(ctor) => { + cx.with_bound_vars(ctor.vars(), || { + cx.fmt_bound_vars("λ", ctor.vars(), ". ", f)?; + w!("{:?}", &ctor.value) + }) + } GenericArg::Lifetime(re) => w!("{:?}", re), GenericArg::Const(c) => w!("{:?}", c), } @@ -2508,6 +2463,5 @@ mod pretty { FuncSort, SortCtor, SimpleTy, - SimpleConstrTy, ); } diff --git a/crates/flux-middle/src/rty/refining.rs b/crates/flux-middle/src/rty/refining.rs index 307ede7af1..b4d6d1b79e 100644 --- a/crates/flux-middle/src/rty/refining.rs +++ b/crates/flux-middle/src/rty/refining.rs @@ -38,14 +38,14 @@ pub(crate) fn refine_generics(generics: &rustc::ty::Generics) -> QueryResult { genv: GlobalEnv<'genv, 'tcx>, generics: rty::Generics, - refine: fn(rty::BaseTy) -> rty::Binder, + refine: fn(rty::BaseTy) -> rty::Binder, } impl<'genv, 'tcx> Refiner<'genv, 'tcx> { pub fn new( genv: GlobalEnv<'genv, 'tcx>, generics: &rty::Generics, - refine: fn(rty::BaseTy) -> rty::Binder, + refine: fn(rty::BaseTy) -> rty::Binder, ) -> Self { Self { genv, generics: generics.clone(), refine } } @@ -60,7 +60,7 @@ impl<'genv, 'tcx> Refiner<'genv, 'tcx> { generics: generics.clone(), refine: |bty| { let sort = bty.sort(); - let constr = rty::SimpleConstrTy::new( + let constr = rty::SimpleTy::new( bty.shift_in_escaping(1), rty::Expr::nu(), rty::Expr::hole(rty::HoleKind::Pred), @@ -241,7 +241,7 @@ impl<'genv, 'tcx> Refiner<'genv, 'tcx> { } (rty::GenericParamDefKind::BaseTy, rustc::ty::GenericArg::Ty(ty)) => { let poly_constr = self.refine_ty_inner(ty)?.expect_simple(); - Ok(rty::GenericArg::Base(rty::SimpleTy::Exists(poly_constr))) + Ok(rty::GenericArg::Base(poly_constr)) } (rty::GenericParamDefKind::Lifetime, rustc::ty::GenericArg::Lifetime(re)) => { Ok(rty::GenericArg::Lifetime(*re)) @@ -285,7 +285,7 @@ impl<'genv, 'tcx> Refiner<'genv, 'tcx> { } } - fn refine_ty_inner(&self, ty: &rustc::ty::Ty) -> QueryResult { + fn refine_ty_inner(&self, ty: &rustc::ty::Ty) -> QueryResult { let bty = match ty.kind() { rustc::ty::TyKind::Closure(did, args) => { let args = args.as_closure(); @@ -323,7 +323,7 @@ impl<'genv, 'tcx> Refiner<'genv, 'tcx> { rustc::ty::TyKind::Param(param_ty) => { match self.param(*param_ty)?.kind { rty::GenericParamDefKind::Type { .. } | rty::GenericParamDefKind::SplTy => { - return Ok(TyOrSimple::Ty(rty::Ty::param(*param_ty))); + return Ok(TyOrBase::Ty(rty::Ty::param(*param_ty))); } rty::GenericParamDefKind::BaseTy => rty::BaseTy::Param(*param_ty), rty::GenericParamDefKind::Lifetime | rty::GenericParamDefKind::Const { .. } => { @@ -339,7 +339,7 @@ impl<'genv, 'tcx> Refiner<'genv, 'tcx> { rustc::ty::TyKind::Alias(alias_kind, alias_ty) => { let kind = Self::refine_alias_kind(alias_kind); let alias_ty = self.as_default().refine_alias_ty(alias_kind, alias_ty)?; - return Ok(TyOrSimple::Ty(rty::Ty::alias(kind, alias_ty))); + return Ok(TyOrBase::Ty(rty::Ty::alias(kind, alias_ty))); } rustc::ty::TyKind::Bool => rty::BaseTy::Bool, rustc::ty::TyKind::Int(int_ty) => rty::BaseTy::Int(*int_ty), @@ -352,7 +352,7 @@ impl<'genv, 'tcx> Refiner<'genv, 'tcx> { rty::BaseTy::RawPtr(self.as_default().refine_ty(ty)?, *mu) } }; - Ok(TyOrSimple::Simple((self.refine)(bty))) + Ok(TyOrBase::Base((self.refine)(bty))) } fn as_default(&self) -> Self { @@ -388,22 +388,22 @@ impl<'genv, 'tcx> Refiner<'genv, 'tcx> { } } -enum TyOrSimple { +enum TyOrBase { Ty(rty::Ty), - Simple(rty::Binder), + Base(rty::SimpleTyCtor), } -impl TyOrSimple { +impl TyOrBase { fn into_ty(self) -> rty::Ty { match self { - TyOrSimple::Ty(ty) => ty, - TyOrSimple::Simple(poly_constr) => rty::SimpleTy::Exists(poly_constr).to_ty(), + TyOrBase::Ty(ty) => ty, + TyOrBase::Base(ctor) => ctor.to_ty(), } } #[track_caller] - fn expect_simple(self) -> rty::Binder { - if let TyOrSimple::Simple(poly_constr) = self { + fn expect_simple(self) -> rty::Binder { + if let TyOrBase::Base(poly_constr) = self { poly_constr } else { bug!("unexpected ty") @@ -411,9 +411,9 @@ impl TyOrSimple { } } -fn refine_default(bty: rty::BaseTy) -> rty::Binder { +fn refine_default(bty: rty::BaseTy) -> rty::Binder { let sort = bty.sort(); - let constr = rty::SimpleConstrTy::indexed(bty.shift_in_escaping(1), rty::Expr::nu()); + let constr = rty::SimpleTy::indexed(bty.shift_in_escaping(1), rty::Expr::nu()); rty::Binder::with_sort(constr, sort) } diff --git a/crates/flux-middle/src/rty/subst.rs b/crates/flux-middle/src/rty/subst.rs index 7bd2750c90..476d36ae62 100644 --- a/crates/flux-middle/src/rty/subst.rs +++ b/crates/flux-middle/src/rty/subst.rs @@ -71,8 +71,8 @@ impl RegionSubst { debug_assert_eq!(args1.len(), args2.len()); for (arg1, arg2) in iter::zip(args1, args2) { match (arg1, arg2) { - (GenericArg::Base(ty1), ty::GenericArg::Ty(ty2)) => { - self.infer_from_bty(ty1.bty_skipping_existential(), ty2); + (GenericArg::Base(ctor1), ty::GenericArg::Ty(ty2)) => { + self.infer_from_bty(ctor1.as_bty_skipping_binder(), ty2); } (GenericArg::Ty(ty1), ty::GenericArg::Ty(ty2)) => { self.infer_from_ty(ty1, ty2); @@ -253,7 +253,7 @@ pub(crate) struct GenericsSubstFolder<'a, D> { trait GenericsSubstDelegate { fn sort_for_param(&mut self, param_ty: ParamTy) -> Sort; fn ty_for_param(&mut self, param_ty: ParamTy) -> Ty; - fn ctor_for_param(&mut self, param_ty: ParamTy) -> Binder; + fn ctor_for_param(&mut self, param_ty: ParamTy) -> SimpleTyCtor; fn region_for_param(&mut self, ebr: EarlyBoundRegion) -> Region; } @@ -273,9 +273,9 @@ impl GenericsSubstDelegate for IdentitySubstDelegate { Ty::param(param_ty) } - fn ctor_for_param(&mut self, param_ty: ParamTy) -> Binder { + fn ctor_for_param(&mut self, param_ty: ParamTy) -> SimpleTyCtor { Binder::with_sort( - SimpleConstrTy::indexed(BaseTy::Param(param_ty), Expr::nu()), + SimpleTy::indexed(BaseTy::Param(param_ty), Expr::nu()), Sort::Param(param_ty), ) } @@ -304,9 +304,9 @@ impl GenericsSubstDelegate for GenericArgsDelegate<'_> { } } - fn ctor_for_param(&mut self, param_ty: ParamTy) -> Binder { + fn ctor_for_param(&mut self, param_ty: ParamTy) -> SimpleTyCtor { match self.0.get(param_ty.index as usize) { - Some(GenericArg::Base(arg)) => arg.to_ctor(), + Some(GenericArg::Base(ctor)) => ctor.clone(), Some(arg) => { bug!("expected base type for generic parameter, found `{:?}`", arg) } @@ -353,7 +353,7 @@ where bug!("unexpected type param {param_ty:?}"); } - fn ctor_for_param(&mut self, param_ty: ParamTy) -> Binder { + fn ctor_for_param(&mut self, param_ty: ParamTy) -> SimpleTyCtor { bug!("unexpected base type param {param_ty:?}"); } @@ -398,7 +398,7 @@ impl TypeFolder for GenericsSubstFolder<'_, D> { } } - fn fold_simple_constr_ty(&mut self, constr: &SimpleConstrTy) -> SimpleConstrTy { + fn fold_simple_ty(&mut self, constr: &SimpleTy) -> SimpleTy { if let BaseTy::Param(param_ty) = &constr.bty { self.delegate .ctor_for_param(*param_ty) diff --git a/crates/flux-refineck/src/checker.rs b/crates/flux-refineck/src/checker.rs index 94e9282380..8825a17145 100644 --- a/crates/flux-refineck/src/checker.rs +++ b/crates/flux-refineck/src/checker.rs @@ -1149,9 +1149,9 @@ fn instantiate_args_for_fun_call( let sort = bty.sort(); let bty = bty.shift_in_escaping(1); let constr = if !sort.is_unit() { - rty::SimpleConstrTy::new(bty, Expr::nu(), Expr::hole(rty::HoleKind::Pred)) + rty::SimpleTy::new(bty, Expr::nu(), Expr::hole(rty::HoleKind::Pred)) } else { - rty::SimpleConstrTy::indexed(bty, Expr::nu()) + rty::SimpleTy::indexed(bty, Expr::nu()) }; Binder::with_sort(constr, sort) }); From 9382ebfd52dead3cc9ae04aa5a4cc56294168f89 Mon Sep 17 00:00:00 2001 From: Nico Lehmann Date: Fri, 16 Feb 2024 11:54:44 -0800 Subject: [PATCH 12/22] Remove SplTy --- crates/flux-desugar/src/desugar.rs | 6 +- crates/flux-fhir-analysis/locales/en-US.ftl | 6 +- crates/flux-fhir-analysis/src/conv.rs | 185 +++++++++--------- crates/flux-fhir-analysis/src/wf/errors.rs | 14 -- crates/flux-fhir-analysis/src/wf/mod.rs | 41 +--- crates/flux-middle/src/fhir.rs | 5 +- crates/flux-middle/src/rty/mod.rs | 39 ++-- crates/flux-middle/src/rty/projections.rs | 2 +- crates/flux-middle/src/rty/refining.rs | 9 +- crates/flux-middle/src/sort_of.rs | 10 +- crates/flux-refineck/src/constraint_gen.rs | 32 +-- crates/flux-refineck/src/type_env.rs | 18 +- crates/flux-syntax/src/grammar.lalrpop | 1 - crates/flux-syntax/src/surface.rs | 1 - crates/flux-syntax/src/surface/visit.rs | 2 +- .../tests/neg/error_messages/wf/kinds00.rs | 3 + .../tests/neg/error_messages/wf/kinds01.rs | 9 +- 17 files changed, 176 insertions(+), 207 deletions(-) diff --git a/crates/flux-desugar/src/desugar.rs b/crates/flux-desugar/src/desugar.rs index ff4b95f6e8..0372e83a55 100644 --- a/crates/flux-desugar/src/desugar.rs +++ b/crates/flux-desugar/src/desugar.rs @@ -212,8 +212,7 @@ impl<'a, 'genv, 'tcx: 'genv> RustItemCtxt<'a, 'genv, 'tcx> { surface::GenericParamKind::Type => { fhir::GenericParamKind::Type { default: None } } - surface::GenericParamKind::Spl => fhir::GenericParamKind::SplTy, - surface::GenericParamKind::Base => fhir::GenericParamKind::BaseTy, + surface::GenericParamKind::Base => fhir::GenericParamKind::Base, surface::GenericParamKind::Refine { .. } => unreachable!(), }; self_kind = Some(kind); @@ -230,8 +229,7 @@ impl<'a, 'genv, 'tcx: 'genv> RustItemCtxt<'a, 'genv, 'tcx> { .transpose()?, } } - surface::GenericParamKind::Base => fhir::GenericParamKind::BaseTy, - surface::GenericParamKind::Spl => fhir::GenericParamKind::SplTy, + surface::GenericParamKind::Base => fhir::GenericParamKind::Base, surface::GenericParamKind::Refine { .. } => unreachable!(), }; surface_params.insert(def_id, fhir::GenericParam { def_id, kind }); diff --git a/crates/flux-fhir-analysis/locales/en-US.ftl b/crates/flux-fhir-analysis/locales/en-US.ftl index b647bd688c..86567b4760 100644 --- a/crates/flux-fhir-analysis/locales/en-US.ftl +++ b/crates/flux-fhir-analysis/locales/en-US.ftl @@ -80,9 +80,6 @@ fhir_analysis_expected_numeric = fhir_analysis_no_equality = values of sort `{$sort}` cannot be compared for equality -fhir_analysis_invalid_base_instance = - values of this type cannot be used as base sorted instances - fhir_analysis_param_not_determined = parameter `{$name}` cannot be determined .label = undetermined parameter @@ -166,6 +163,9 @@ fhir_analysis_assoc_type_not_found = .label = cannot resolve this associated type .note = Flux cannot resolved associated types if they are defined in a super trait +fhir_analysis_invalid_base_instance = + values of this type cannot be used as base sorted instances + # Check impl against trait errors fhir_analysis_incompatible_sort = diff --git a/crates/flux-fhir-analysis/src/conv.rs b/crates/flux-fhir-analysis/src/conv.rs index 5853359853..fb59471d83 100644 --- a/crates/flux-fhir-analysis/src/conv.rs +++ b/crates/flux-fhir-analysis/src/conv.rs @@ -219,8 +219,7 @@ fn conv_generic_param_kind(kind: &fhir::GenericParamKind) -> rty::GenericParamDe fhir::GenericParamKind::Type { default } => { rty::GenericParamDefKind::Type { has_default: default.is_some() } } - fhir::GenericParamKind::SplTy => rty::GenericParamDefKind::SplTy, - fhir::GenericParamKind::BaseTy => rty::GenericParamDefKind::BaseTy, + fhir::GenericParamKind::Base => rty::GenericParamDefKind::Base, fhir::GenericParamKind::Lifetime => rty::GenericParamDefKind::Lifetime, } } @@ -453,9 +452,9 @@ impl<'a, 'genv, 'tcx> ConvCtxt<'a, 'genv, 'tcx> { let kind = rty::BoundRegionKind::BrNamed(def_id.to_def_id(), name); Ok(rty::BoundVariableKind::Region(kind)) } - fhir::GenericParamKind::Type { default: _ } - | fhir::GenericParamKind::BaseTy - | fhir::GenericParamKind::SplTy => bug!("unexpected!"), + fhir::GenericParamKind::Type { .. } | fhir::GenericParamKind::Base => { + bug!("unexpected!") + } } } @@ -673,7 +672,15 @@ impl<'a, 'genv, 'tcx> ConvCtxt<'a, 'genv, 'tcx> { fhir::TyKind::BaseTy(bty) => self.conv_base_ty(env, bty), fhir::TyKind::Indexed(bty, idx) => { let idx = self.conv_refine_arg(env, idx)?; - self.conv_indexed_type(env, bty, idx) + match &bty.kind { + fhir::BaseTyKind::Path(fhir::QPath::Resolved(_, path)) => { + Ok(self.conv_ty_ctor(env, path)?.replace_bound_reft(&idx)) + } + fhir::BaseTyKind::Slice(ty) => { + let bty = rty::BaseTy::Slice(self.conv_ty(env, ty)?); + Ok(rty::Ty::indexed(bty, idx)) + } + } } fhir::TyKind::Exists(params, ty) => { let layer = Layer::list(self, 0, params, false); @@ -738,51 +745,54 @@ impl<'a, 'genv, 'tcx> ConvCtxt<'a, 'genv, 'tcx> { } fn conv_base_ty(&self, env: &mut Env, bty: &fhir::BaseTy) -> QueryResult { - let sort = self.genv.sort_of_bty(bty); - - if let fhir::BaseTyKind::Path(fhir::QPath::Resolved(self_ty, path)) = &bty.kind { - if let fhir::Res::Def(DefKind::AssocTy, assoc_id) = path.res { - let trait_id = self.genv.tcx().trait_of_item(assoc_id).unwrap(); - let self_ty = self.conv_ty(env, self_ty.as_deref().unwrap())?; - let [.., trait_segment, assoc_segment] = path.segments else { - span_bug!(bty.span, "expected at least two segments"); - }; - let mut args = vec![rty::GenericArg::Ty(self_ty)]; - self.conv_generic_args_into(env, trait_id, trait_segment.args, &mut args)?; - self.conv_generic_args_into(env, assoc_id, assoc_segment.args, &mut args)?; - let args = List::from_vec(args); - - let refine_args = List::empty(); - let alias_ty = rty::AliasTy { args, refine_args, def_id: assoc_id }; - return Ok(rty::Ty::alias(rty::AliasKind::Projection, alias_ty)); - } - // If it is a type parameter with no sort, it means it is of kind `Type` - if let fhir::Res::SelfTyParam { .. } = path.res - && sort.is_none() - { - return Ok(rty::Ty::param(rty::SELF_PARAM_TY)); + match &bty.kind { + fhir::BaseTyKind::Path(fhir::QPath::Resolved(self_ty, path)) => { + match path.res { + fhir::Res::Def(DefKind::AssocTy, assoc_id) => { + let trait_id = self.genv.tcx().trait_of_item(assoc_id).unwrap(); + let self_ty = self.conv_ty(env, self_ty.as_deref().unwrap())?; + let [.., trait_segment, assoc_segment] = path.segments else { + span_bug!(bty.span, "expected at least two segments"); + }; + let mut args = vec![rty::GenericArg::Ty(self_ty)]; + self.conv_generic_args_into(env, trait_id, trait_segment.args, &mut args)?; + self.conv_generic_args_into(env, assoc_id, assoc_segment.args, &mut args)?; + let args = List::from_vec(args); + + let refine_args = List::empty(); + let alias_ty = rty::AliasTy { args, refine_args, def_id: assoc_id }; + return Ok(rty::Ty::alias(rty::AliasKind::Projection, alias_ty)); + } + fhir::Res::SelfTyParam { trait_ } => { + let param = self.genv.generics_of(trait_)?.param_at(0, self.genv)?; + if let rty::GenericParamDefKind::Type { .. } = param.kind { + return Ok(rty::Ty::param(rty::SELF_PARAM_TY)); + } + } + fhir::Res::Def(DefKind::TyParam, def_id) => { + let owner_id = self.genv.hir().ty_param_owner(def_id.expect_local()); + let param_ty = self.genv.def_id_to_param_ty(def_id.expect_local()); + let param = self + .genv + .generics_of(owner_id)? + .param_at(param_ty.index as usize, self.genv)?; + if let rty::GenericParamDefKind::Type { .. } = param.kind { + return Ok(rty::Ty::param(param_ty)); + } + } + _ => {} + } + Ok(self.conv_ty_ctor(env, path)?.to_ty()) } - if let fhir::Res::Def(DefKind::TyParam, def_id) = path.res - && sort.is_none() - { - let param_ty = self.genv.def_id_to_param_ty(def_id.expect_local()); - return Ok(rty::Ty::param(param_ty)); + fhir::BaseTyKind::Slice(ty) => { + let bty = rty::BaseTy::Slice(self.conv_ty(env, ty)?).shift_in_escaping(1); + let sort = bty.sort(); + Ok(rty::Ty::exists(rty::Binder::with_sort( + rty::Ty::indexed(bty, rty::Expr::nu()), + sort, + ))) } } - let sort = sort.unwrap(); - if sort.is_unit() { - let idx = rty::Expr::unit(); - self.conv_indexed_type(env, bty, idx) - } else if let Some(def_id) = sort.is_unit_adt() { - let idx = rty::Expr::unit_adt(def_id); - self.conv_indexed_type(env, bty, idx) - } else { - env.push_layer(Layer::empty()); - let idx = rty::Expr::nu(); - let ty = self.conv_indexed_type(env, bty, idx)?; - env.pop_layer(); - Ok(rty::Ty::exists(rty::Binder::with_sort(ty, sort))) - } } fn conv_lifetime(&self, env: &Env, lft: fhir::Lifetime) -> rty::Region { @@ -851,29 +861,7 @@ impl<'a, 'genv, 'tcx> ConvCtxt<'a, 'genv, 'tcx> { } } - fn conv_indexed_type( - &self, - env: &mut Env, - bty: &fhir::BaseTy, - idx: rty::Expr, - ) -> QueryResult { - match &bty.kind { - fhir::BaseTyKind::Path(fhir::QPath::Resolved(_, path)) => { - self.conv_indexed_path(env, path, idx) - } - fhir::BaseTyKind::Slice(ty) => { - let slice = rty::BaseTy::slice(self.conv_ty(env, ty)?); - Ok(rty::Ty::indexed(slice, idx)) - } - } - } - - fn conv_indexed_path( - &self, - env: &mut Env, - path: &fhir::Path, - idx: rty::Expr, - ) -> QueryResult { + fn conv_ty_ctor(&self, env: &mut Env, path: &fhir::Path) -> QueryResult { let bty = match &path.res { fhir::Res::PrimTy(PrimTy::Bool) => rty::BaseTy::Bool, fhir::Res::PrimTy(PrimTy::Str) => rty::BaseTy::Str, @@ -897,11 +885,7 @@ impl<'a, 'genv, 'tcx> ConvCtxt<'a, 'genv, 'tcx> { } fhir::Res::SelfTyParam { .. } => rty::BaseTy::Param(rty::SELF_PARAM_TY), fhir::Res::SelfTyAlias { alias_to, .. } => { - return Ok(self - .genv - .type_of(*alias_to)? - .instantiate_identity(&[]) - .replace_bound_reft(&idx)); + return Ok(self.genv.type_of(*alias_to)?.instantiate_identity(&[])); } fhir::Res::Def(DefKind::TyAlias { .. }, def_id) => { let generics = self.conv_generic_args(env, *def_id, path.last_segment().args)?; @@ -910,17 +894,15 @@ impl<'a, 'genv, 'tcx> ConvCtxt<'a, 'genv, 'tcx> { .iter() .map(|arg| self.conv_refine_arg(env, arg)) .try_collect_vec()?; - return Ok(self - .genv - .type_of(*def_id)? - .instantiate(&generics, &refine) - .replace_bound_reft(&idx)); + return Ok(self.genv.type_of(*def_id)?.instantiate(&generics, &refine)); } fhir::Res::Def(..) => { span_bug!(path.span, "unexpected resolution in conv_indexed_path: {:?}", path.res) } }; - Ok(rty::Ty::indexed(bty, idx)) + let sort = bty.sort(); + let bty = bty.shift_in_escaping(1); + Ok(rty::Binder::with_sort(rty::Ty::indexed(bty, rty::Expr::nu()), sort)) } pub fn conv_generic_args( @@ -949,19 +931,20 @@ impl<'a, 'genv, 'tcx> ConvCtxt<'a, 'genv, 'tcx> { (fhir::GenericArg::Lifetime(lft), rty::GenericParamDefKind::Lifetime) => { into.push(rty::GenericArg::Lifetime(self.conv_lifetime(env, *lft))); } - ( - fhir::GenericArg::Type(ty), - rty::GenericParamDefKind::Type { .. } | rty::GenericParamDefKind::SplTy, - ) => { + (fhir::GenericArg::Type(ty), rty::GenericParamDefKind::Type { .. }) => { into.push(rty::GenericArg::Ty(self.conv_ty(env, ty)?)); } - (fhir::GenericArg::Type(ty), rty::GenericParamDefKind::BaseTy) => { - let sty = self + (fhir::GenericArg::Type(ty), rty::GenericParamDefKind::Base) => { + let ctor = self .conv_ty(env, ty)? .shallow_canonicalize() .to_simple_ty_ctor() - .unwrap(); - into.push(rty::GenericArg::Base(sty)); + .ok_or_else(|| { + self.genv + .sess() + .emit_err(errors::InvalidBaseInstance::new(ty)) + })?; + into.push(rty::GenericArg::Base(ctor)); } _ => { bug!("unexpected param `{:?}` for arg `{arg:?}`", param.kind); @@ -984,7 +967,7 @@ impl<'a, 'genv, 'tcx> ConvCtxt<'a, 'genv, 'tcx> { .genv .type_of(param.def_id)? .instantiate(into, &[]) - .into_ty(); + .to_ty(); into.push(rty::GenericArg::Ty(ty)); } else { bug!("unexpected generic param: {param:?}"); @@ -1221,10 +1204,6 @@ impl Layer { Self::new(cx, 0, params, false, LayerKind::Record(def_id)) } - fn empty() -> Self { - Self { map: FxIndexMap::default(), filter_unit: false, kind: LayerKind::List } - } - fn get(&self, name: impl Borrow, level: u32) -> Option { Some(LookupResultKind::LateBound { level, @@ -1496,7 +1475,7 @@ fn conv_un_op(op: fhir::UnOp) -> rty::UnOp { mod errors { use flux_macros::Diagnostic; - use flux_middle::fhir::SurfaceIdent; + use flux_middle::fhir::{self, SurfaceIdent}; use rustc_span::Span; #[derive(Diagnostic)] @@ -1513,4 +1492,18 @@ mod errors { Self { span: ident.span } } } + + #[derive(Diagnostic)] + #[diag(fhir_analysis_invalid_base_instance, code = "FLUX")] + pub(super) struct InvalidBaseInstance<'fhir> { + #[primary_span] + span: Span, + ty: &'fhir fhir::Ty<'fhir>, + } + + impl<'fhir> InvalidBaseInstance<'fhir> { + pub(super) fn new(ty: &'fhir fhir::Ty<'fhir>) -> Self { + Self { ty, span: ty.span } + } + } } diff --git a/crates/flux-fhir-analysis/src/wf/errors.rs b/crates/flux-fhir-analysis/src/wf/errors.rs index e94639f48a..59adc3ee9d 100644 --- a/crates/flux-fhir-analysis/src/wf/errors.rs +++ b/crates/flux-fhir-analysis/src/wf/errors.rs @@ -184,20 +184,6 @@ impl<'a> InvalidPrimitiveDotAccess<'a> { } } -#[derive(Diagnostic)] -#[diag(fhir_analysis_invalid_base_instance, code = "FLUX")] -pub(super) struct InvalidBaseInstance<'fhir> { - #[primary_span] - span: Span, - ty: fhir::Ty<'fhir>, -} - -impl<'fhir> InvalidBaseInstance<'fhir> { - pub(super) fn new(ty: fhir::Ty<'fhir>) -> Self { - Self { ty, span: ty.span } - } -} - #[derive(Diagnostic)] #[diag(fhir_analysis_param_not_determined, code = "FLUX")] #[help] diff --git a/crates/flux-fhir-analysis/src/wf/mod.rs b/crates/flux-fhir-analysis/src/wf/mod.rs index 2ecc3bc698..d2b87d42ec 100644 --- a/crates/flux-fhir-analysis/src/wf/mod.rs +++ b/crates/flux-fhir-analysis/src/wf/mod.rs @@ -12,7 +12,7 @@ use flux_errors::{FluxSession, ResultExt}; use flux_middle::{ fhir::{self, ExprRes, FluxOwnerId, SurfaceIdent}, global_env::GlobalEnv, - rty::{self, GenericParamDefKind, WfckResults}, + rty::{self, WfckResults}, }; use rustc_data_structures::{ snapshot_map::{self, SnapshotMap}, @@ -20,7 +20,7 @@ use rustc_data_structures::{ }; use rustc_errors::{ErrorGuaranteed, IntoDiagnostic}; use rustc_hash::FxHashSet; -use rustc_hir::{def::DefKind, def_id::DefId, OwnerId}; +use rustc_hir::{def::DefKind, OwnerId}; use rustc_span::Symbol; use self::sortck::InferCtxt; @@ -255,9 +255,8 @@ impl<'genv, 'tcx> Wf<'genv, 'tcx> { fn check_generic_bound(&mut self, infcx: &mut InferCtxt, bound: &fhir::GenericBound) -> Result { match bound { fhir::GenericBound::Trait(trait_ref, _) => self.check_path(infcx, &trait_ref.trait_ref), - fhir::GenericBound::LangItemTrait(lang_item, args, bindings) => { - let def_id = self.genv.tcx().require_lang_item(*lang_item, None); - self.check_generic_args(infcx, def_id, args)?; + fhir::GenericBound::LangItemTrait(_, args, bindings) => { + self.check_generic_args(infcx, args)?; self.check_type_bindings(infcx, bindings)?; Ok(()) } @@ -385,10 +384,9 @@ impl<'genv, 'tcx> Wf<'genv, 'tcx> { self.check_type(infcx, ty)?; self.check_expr_as_pred(infcx, pred) } - fhir::TyKind::OpaqueDef(item_id, args, _refine_args, _) => { + fhir::TyKind::OpaqueDef(_item_id, args, _refine_args, _) => { // TODO sanity check the _refine_args (though they should never fail!) but we'd need their expected sorts - let def_id = item_id.owner_id.to_def_id(); - self.check_generic_args(infcx, def_id, args) + self.check_generic_args(infcx, args) } fhir::TyKind::RawPtr(ty, _) => self.check_type(infcx, ty), fhir::TyKind::Hole(_) | fhir::TyKind::Never => Ok(()), @@ -408,26 +406,7 @@ impl<'genv, 'tcx> Wf<'genv, 'tcx> { .try_collect_exhaust() } - fn check_generic_args_kinds(&self, def_id: DefId, args: &[fhir::GenericArg]) -> Result { - let generics = self.genv.generics_of(def_id).emit(self.genv.sess())?; - for (arg, param) in iter::zip(args, &generics.params) { - if param.kind == GenericParamDefKind::SplTy { - let ty = arg.expect_type(); - if self.genv.sort_of_ty(ty).is_none() { - return self.emit_err(errors::InvalidBaseInstance::new(*ty)); - } - } - } - Ok(()) - } - - fn check_generic_args( - &mut self, - infcx: &mut InferCtxt, - def_id: DefId, - args: &[fhir::GenericArg], - ) -> Result { - self.check_generic_args_kinds(def_id, args)?; + fn check_generic_args(&mut self, infcx: &mut InferCtxt, args: &[fhir::GenericArg]) -> Result { args.iter() .try_for_each_exhaust(|arg| self.check_generic_arg(infcx, arg)) } @@ -490,10 +469,8 @@ impl<'genv, 'tcx> Wf<'genv, 'tcx> { // TODO(nilehmann) we should check all segments let last_segment = path.last_segment(); - if let fhir::Res::Def(_kind, did) = &path.res - && !last_segment.args.is_empty() - { - self.check_generic_args(infcx, *did, last_segment.args)?; + if !last_segment.args.is_empty() { + self.check_generic_args(infcx, last_segment.args)?; } let bindings = self.check_type_bindings(infcx, last_segment.bindings); if !self.genv.is_box(path.res) { diff --git a/crates/flux-middle/src/fhir.rs b/crates/flux-middle/src/fhir.rs index 9db8d042b3..b2adb3b8e4 100644 --- a/crates/flux-middle/src/fhir.rs +++ b/crates/flux-middle/src/fhir.rs @@ -62,8 +62,7 @@ pub struct GenericParam<'fhir> { #[derive(Debug, Clone, Copy)] pub enum GenericParamKind<'fhir> { Type { default: Option> }, - SplTy, - BaseTy, + Base, Lifetime, } @@ -1004,7 +1003,7 @@ impl<'fhir> Generics<'fhir> { pub fn with_refined_by(self, genv: GlobalEnv<'fhir, '_>, refined_by: &RefinedBy) -> Self { let params = genv.alloc_slice_fill_iter(self.params.iter().map(|param| { let kind = if refined_by.is_base_generic(param.def_id.to_def_id()) { - GenericParamKind::SplTy + GenericParamKind::Base } else { param.kind }; diff --git a/crates/flux-middle/src/rty/mod.rs b/crates/flux-middle/src/rty/mod.rs index a5c95e20e8..bcb872afbc 100644 --- a/crates/flux-middle/src/rty/mod.rs +++ b/crates/flux-middle/src/rty/mod.rs @@ -152,8 +152,7 @@ pub struct GenericParamDef { #[derive(Debug, Clone, PartialEq, Eq, Hash)] pub enum GenericParamDefKind { Type { has_default: bool }, - SplTy, - BaseTy, + Base, Lifetime, Const { has_default: bool }, } @@ -555,6 +554,25 @@ pub struct ClosureOblig { } pub type TyCtor = Binder; + +impl TyCtor { + pub fn to_ty(&self) -> Ty { + match &self.vars[..] { + [] => return self.value.shift_out_escaping(1), + [BoundVariableKind::Refine(sort, ..)] => { + if sort.is_unit() { + return self.replace_bound_reft(&Expr::unit()); + } + if let Some(def_id) = sort.is_unit_adt() { + return self.replace_bound_reft(&Expr::unit_adt(def_id)); + } + } + _ => {} + } + Ty::exists(self.clone()) + } +} + pub type Ty = Interned; impl Ty { @@ -793,7 +811,7 @@ pub type RefineArgs = List; pub type OpaqueArgsMap = FxHashMap; -type SimpleTyCtor = Binder; +pub type SimpleTyCtor = Binder; impl SimpleTyCtor { pub fn as_bty_skipping_binder(&self) -> &BaseTy { @@ -882,7 +900,7 @@ impl GenericArg { fn from_param_def(genv: GlobalEnv, param: &GenericParamDef) -> QueryResult { match param.kind { - GenericParamDefKind::Type { .. } | GenericParamDefKind::SplTy => { + GenericParamDefKind::Type { .. } => { let param_ty = ParamTy { index: param.index, name: param.name }; Ok(GenericArg::Ty(Ty::param(param_ty))) } @@ -897,7 +915,7 @@ impl GenericArg { let ty = genv.lower_type_of(param.def_id)?.skip_binder(); Ok(GenericArg::Const(Const { kind, ty })) } - GenericParamDefKind::BaseTy => { + GenericParamDefKind::Base => { bug!("") } } @@ -1212,6 +1230,7 @@ impl Binder { Ok(Binder { vars: self.vars, value: f(self.value)? }) } + #[track_caller] pub fn sort(&self) -> Sort { match &self.vars[..] { [BoundVariableKind::Refine(sort, ..)] => sort.clone(), @@ -1319,16 +1338,6 @@ where } } -impl Binder { - pub fn into_ty(self) -> Ty { - if self.vars.is_empty() { - self.value - } else { - Ty::exists(self) - } - } -} - impl EarlyBinder { pub fn instantiate(self, args: &[GenericArg], refine_args: &[Expr]) -> T { self.0.fold_with(&mut subst::GenericsSubstFolder::new( diff --git a/crates/flux-middle/src/rty/projections.rs b/crates/flux-middle/src/rty/projections.rs index d3c4d43290..71a618183e 100644 --- a/crates/flux-middle/src/rty/projections.rs +++ b/crates/flux-middle/src/rty/projections.rs @@ -124,7 +124,7 @@ impl<'genv, 'tcx, 'cx> Normalizer<'genv, 'tcx, 'cx> { .genv .type_of(assoc_type_id)? .instantiate(&args, &[]) - .into_ty()) + .to_ty()) } } } diff --git a/crates/flux-middle/src/rty/refining.rs b/crates/flux-middle/src/rty/refining.rs index b4d6d1b79e..7722ed8c9d 100644 --- a/crates/flux-middle/src/rty/refining.rs +++ b/crates/flux-middle/src/rty/refining.rs @@ -236,10 +236,7 @@ impl<'genv, 'tcx> Refiner<'genv, 'tcx> { (rty::GenericParamDefKind::Type { .. }, rustc::ty::GenericArg::Ty(ty)) => { Ok(rty::GenericArg::Ty(self.refine_ty(ty)?)) } - (rty::GenericParamDefKind::SplTy, rustc::ty::GenericArg::Ty(ty)) => { - Ok(rty::GenericArg::Ty(self.refine_ty(ty)?)) - } - (rty::GenericParamDefKind::BaseTy, rustc::ty::GenericArg::Ty(ty)) => { + (rty::GenericParamDefKind::Base, rustc::ty::GenericArg::Ty(ty)) => { let poly_constr = self.refine_ty_inner(ty)?.expect_simple(); Ok(rty::GenericArg::Base(poly_constr)) } @@ -322,10 +319,10 @@ impl<'genv, 'tcx> Refiner<'genv, 'tcx> { } rustc::ty::TyKind::Param(param_ty) => { match self.param(*param_ty)?.kind { - rty::GenericParamDefKind::Type { .. } | rty::GenericParamDefKind::SplTy => { + rty::GenericParamDefKind::Type { .. } => { return Ok(TyOrBase::Ty(rty::Ty::param(*param_ty))); } - rty::GenericParamDefKind::BaseTy => rty::BaseTy::Param(*param_ty), + rty::GenericParamDefKind::Base => rty::BaseTy::Param(*param_ty), rty::GenericParamDefKind::Lifetime | rty::GenericParamDefKind::Const { .. } => { bug!() } diff --git a/crates/flux-middle/src/sort_of.rs b/crates/flux-middle/src/sort_of.rs index 03ef1cb6b0..280c098a38 100644 --- a/crates/flux-middle/src/sort_of.rs +++ b/crates/flux-middle/src/sort_of.rs @@ -57,9 +57,7 @@ impl<'sess, 'tcx> GlobalEnv<'sess, 'tcx> { fn sort_of_generic_param(self, def_id: LocalDefId) -> Option { let param = self.get_generic_param(def_id); match ¶m.kind { - fhir::GenericParamKind::BaseTy | fhir::GenericParamKind::SplTy => { - Some(rty::Sort::Param(self.def_id_to_param_ty(def_id))) - } + fhir::GenericParamKind::Base => Some(rty::Sort::Param(self.def_id_to_param_ty(def_id))), fhir::GenericParamKind::Type { .. } | fhir::GenericParamKind::Lifetime => None, } } @@ -68,9 +66,7 @@ impl<'sess, 'tcx> GlobalEnv<'sess, 'tcx> { let generics = self.map().get_generics(owner.expect_local()).unwrap(); let kind = generics.self_kind.as_ref()?; match kind { - fhir::GenericParamKind::BaseTy | fhir::GenericParamKind::SplTy => { - Some(rty::Sort::Param(rty::SELF_PARAM_TY)) - } + fhir::GenericParamKind::Base => Some(rty::Sort::Param(rty::SELF_PARAM_TY)), fhir::GenericParamKind::Type { .. } | fhir::GenericParamKind::Lifetime => None, } } @@ -82,7 +78,7 @@ impl<'sess, 'tcx> GlobalEnv<'sess, 'tcx> { } } - pub fn sort_of_ty(self, ty: &fhir::Ty) -> Option { + fn sort_of_ty(self, ty: &fhir::Ty) -> Option { match &ty.kind { fhir::TyKind::BaseTy(bty) | fhir::TyKind::Indexed(bty, _) => self.sort_of_bty(bty), fhir::TyKind::Exists(_, ty) | fhir::TyKind::Constr(_, ty) => self.sort_of_ty(ty), diff --git a/crates/flux-refineck/src/constraint_gen.rs b/crates/flux-refineck/src/constraint_gen.rs index 7f39edf599..31c4b216d9 100644 --- a/crates/flux-refineck/src/constraint_gen.rs +++ b/crates/flux-refineck/src/constraint_gen.rs @@ -150,7 +150,7 @@ impl<'a, 'genv, 'tcx> ConstrGen<'a, 'genv, 'tcx> { for (idx, arg) in generic_args.iter().enumerate() { let param = generics.param_at(idx, self.genv)?; match param.kind { - GenericParamDefKind::BaseTy => { + GenericParamDefKind::Base => { if !arg.is_valid_base_arg() { return Err(CheckerErrKind::InvalidGenericArg); } @@ -681,23 +681,23 @@ impl<'a, 'genv, 'tcx> InferCtxt<'a, 'genv, 'tcx> { arg1: &GenericArg, arg2: &GenericArg, ) -> Result { - match (arg1, arg2) { - (GenericArg::Ty(ty1), GenericArg::Ty(ty2)) => { - match variance { - Variance::Covariant => self.subtyping(rcx, ty1, ty2), - Variance::Invariant => { - self.subtyping(rcx, ty1, ty2)?; - self.subtyping(rcx, ty2, ty1) - } - Variance::Contravariant => self.subtyping(rcx, ty2, ty1), - Variance::Bivariant => Ok(()), - } - } - (GenericArg::Base(_), GenericArg::Base(_)) => { - tracked_span_bug!("generic argument subtyping for base types is not implemented"); + let (ty1, ty2) = match (arg1, arg2) { + (GenericArg::Ty(ty1), GenericArg::Ty(ty2)) => (ty1.clone(), ty2.clone()), + (GenericArg::Base(ctor1), GenericArg::Base(ctor2)) => { + debug_assert_eq!(ctor1.sort(), ctor2.sort()); + (ctor1.to_ty(), ctor2.to_ty()) } - (GenericArg::Lifetime(_), GenericArg::Lifetime(_)) => Ok(()), + (GenericArg::Lifetime(_), GenericArg::Lifetime(_)) => return Ok(()), _ => tracked_span_bug!("incompatible generic args: `{arg1:?}` `{arg2:?}"), + }; + match variance { + Variance::Covariant => self.subtyping(rcx, &ty1, &ty2), + Variance::Invariant => { + self.subtyping(rcx, &ty1, &ty2)?; + self.subtyping(rcx, &ty2, &ty1) + } + Variance::Contravariant => self.subtyping(rcx, &ty2, &ty1), + Variance::Bivariant => Ok(()), } } diff --git a/crates/flux-refineck/src/type_env.rs b/crates/flux-refineck/src/type_env.rs index d80d0851e4..ab2a47e75c 100644 --- a/crates/flux-refineck/src/type_env.rs +++ b/crates/flux-refineck/src/type_env.rs @@ -12,7 +12,7 @@ use flux_middle::{ fold::{FallibleTypeFolder, TypeFoldable, TypeVisitable, TypeVisitor}, subst::RegionSubst, BaseTy, Binder, BoundReftKind, Expr, ExprKind, GenericArg, HoleKind, Mutability, Path, - PtrKind, Region, SortCtor, Ty, TyKind, INNERMOST, + PtrKind, Region, SimpleTy, SortCtor, Ty, TyKind, INNERMOST, }, rustc::mir::{BasicBlock, Local, LocalDecls, Place, PlaceElem}, }; @@ -530,8 +530,20 @@ impl BasicBlockEnvShape { fn join_generic_arg(&self, arg1: &GenericArg, arg2: &GenericArg) -> GenericArg { match (arg1, arg2) { (GenericArg::Ty(ty1), GenericArg::Ty(ty2)) => GenericArg::Ty(self.join_ty(ty1, ty2)), - (GenericArg::Base(_), GenericArg::Base(_)) => { - tracked_span_bug!("generic argument join for base types is not implemented") + (GenericArg::Base(ctor1), GenericArg::Base(ctor2)) => { + let sty1 = ctor1.as_ref().skip_binder(); + let sty2 = ctor2.as_ref().skip_binder(); + debug_assert_eq3!(&sty1.idx, &sty2.idx, &Expr::nu()); + + let bty = self.join_bty(&sty1.bty, &sty2.bty); + let pred = if self.scope.has_free_vars(&sty2.pred) || sty1.pred != sty2.pred { + Expr::hole(HoleKind::Pred) + } else { + sty1.pred.clone() + }; + let sort = bty.sort(); + let ctor = Binder::with_sort(SimpleTy::new(bty, Expr::nu(), pred), sort); + GenericArg::Base(ctor) } (GenericArg::Lifetime(re1), GenericArg::Lifetime(re2)) => { debug_assert_eq!(re1, re2); diff --git a/crates/flux-syntax/src/grammar.lalrpop b/crates/flux-syntax/src/grammar.lalrpop index 5313494f6b..750434b1fc 100644 --- a/crates/flux-syntax/src/grammar.lalrpop +++ b/crates/flux-syntax/src/grammar.lalrpop @@ -41,7 +41,6 @@ GenericParam: surface::GenericParam = { let kind = match kind.as_str() { "type" => surface::GenericParamKind::Type, "base" => surface::GenericParamKind::Base, - "spl" => surface::GenericParamKind::Spl, _ => return Err(ParseError::User { error: UserParseError::UnexpectedToken(lo, hi) }) }; Ok(surface::GenericParam { name, kind, node_id: cx.next_node_id() }) diff --git a/crates/flux-syntax/src/surface.rs b/crates/flux-syntax/src/surface.rs index a9594f4d2a..c5676bed14 100644 --- a/crates/flux-syntax/src/surface.rs +++ b/crates/flux-syntax/src/surface.rs @@ -72,7 +72,6 @@ pub struct GenericParam { #[derive(Debug)] pub enum GenericParamKind { Type, - Spl, Base, Refine { sort: Sort }, } diff --git a/crates/flux-syntax/src/surface/visit.rs b/crates/flux-syntax/src/surface/visit.rs index 6ec98e0b84..9065a5975d 100644 --- a/crates/flux-syntax/src/surface/visit.rs +++ b/crates/flux-syntax/src/surface/visit.rs @@ -203,7 +203,7 @@ pub fn walk_generic_param(vis: &mut V, param: &GenericParam) { vis.visit_ident(param.name); match ¶m.kind { GenericParamKind::Refine { sort } => vis.visit_sort(sort), - GenericParamKind::Type | GenericParamKind::Spl | GenericParamKind::Base => {} + GenericParamKind::Type | GenericParamKind::Base => {} } } diff --git a/crates/flux-tests/tests/neg/error_messages/wf/kinds00.rs b/crates/flux-tests/tests/neg/error_messages/wf/kinds00.rs index 012a6e4b69..4cafecd3de 100644 --- a/crates/flux-tests/tests/neg/error_messages/wf/kinds00.rs +++ b/crates/flux-tests/tests/neg/error_messages/wf/kinds00.rs @@ -13,3 +13,6 @@ pub fn test00_bad() -> RSet { //~^ ERROR values of this type cannot be used as base sorted instances RSet::::new() } + +#[flux::sig(fn(soup:RSet))] //~ ERROR values of this type cannot be used as base sorted instances +pub fn test01(_s: RSet) {} diff --git a/crates/flux-tests/tests/neg/error_messages/wf/kinds01.rs b/crates/flux-tests/tests/neg/error_messages/wf/kinds01.rs index 5e01e1ce2a..e621454daa 100644 --- a/crates/flux-tests/tests/neg/error_messages/wf/kinds01.rs +++ b/crates/flux-tests/tests/neg/error_messages/wf/kinds01.rs @@ -5,11 +5,12 @@ use std::hash::Hash; use rset::RSet; -#[flux::sig(fn(soup:RSet))] //~ ERROR values of this type cannot be used as base sorted instances -pub fn test04(_s: RSet) {} - +// This error is confusing. The problem is that `RSet` cannot be instantiated with `T` because it is +// of kind `type`. But we don't know that until after we convert the argument to `rty` and we check if +// it is a valid simple type. The reason we only know that after conv is that we need to expand type +// aliases. #[flux::sig(fn(RSet[@salt]))] //~ ERROR type cannot be refined -pub fn test05(_s: RSet) +pub fn test01(_s: RSet) where T: Eq + Hash, { From 68a430ea5016959776795d333011cd8a321ea432 Mon Sep 17 00:00:00 2001 From: Nico Lehmann Date: Fri, 16 Feb 2024 16:34:08 -0800 Subject: [PATCH 13/22] Report invalid generic arg error --- crates/flux-middle/locales/en-US.ftl | 3 +++ crates/flux-middle/src/queries.rs | 9 ++++++++ crates/flux-middle/src/rty/mod.rs | 12 +++++++++-- crates/flux-middle/src/rty/refining.rs | 14 +++++++++--- crates/flux-refineck/locales/en-US.ftl | 3 --- crates/flux-refineck/src/checker.rs | 7 ------ crates/flux-refineck/src/constraint_gen.rs | 25 ++-------------------- 7 files changed, 35 insertions(+), 38 deletions(-) diff --git a/crates/flux-middle/locales/en-US.ftl b/crates/flux-middle/locales/en-US.ftl index d17d189902..1cd8fabcf2 100644 --- a/crates/flux-middle/locales/en-US.ftl +++ b/crates/flux-middle/locales/en-US.ftl @@ -24,3 +24,6 @@ middle_unsupported_generic_bound = middle_query_unsupported = unsupported signature .note = {$reason} + +middle_query_invalid_generic_arg = + cannot instantiate base generic with opaque type or a type parameter of kind type diff --git a/crates/flux-middle/src/queries.rs b/crates/flux-middle/src/queries.rs index 341cf8f882..306c51342f 100644 --- a/crates/flux-middle/src/queries.rs +++ b/crates/flux-middle/src/queries.rs @@ -40,6 +40,7 @@ pub type QueryResult = Result; #[derive(Debug, Clone)] pub enum QueryErr { Unsupported { def_id: DefId, def_span: Span, err: UnsupportedErr }, + InvalidGenericArg { def_id: DefId, def_span: Span }, Emitted(ErrorGuaranteed), } @@ -576,6 +577,14 @@ impl<'a> IntoDiagnostic<'a> for QueryErr { builder.downgrade_to_delayed_bug(); builder } + QueryErr::InvalidGenericArg { def_span, .. } => { + let builder = handler.struct_span_err_with_code( + def_span, + fluent::middle_query_invalid_generic_arg, + flux_errors::diagnostic_id(), + ); + builder + } } } } diff --git a/crates/flux-middle/src/rty/mod.rs b/crates/flux-middle/src/rty/mod.rs index bcb872afbc..7b8057ec79 100644 --- a/crates/flux-middle/src/rty/mod.rs +++ b/crates/flux-middle/src/rty/mod.rs @@ -1719,6 +1719,10 @@ impl BaseTy { matches!(self, BaseTy::Slice(..)) } + fn is_adt(&self) -> bool { + matches!(self, BaseTy::Adt(..)) + } + pub fn is_box(&self) -> bool { matches!(self, BaseTy::Adt(adt_def, _) if adt_def.is_box()) } @@ -2216,7 +2220,9 @@ mod pretty { define_scoped!(cx, f); let vars = &self.vars; cx.with_bound_vars(vars, || { - cx.fmt_bound_vars("exists<", vars, ">", f)?; + if !vars.is_empty() { + cx.fmt_bound_vars("exists<", vars, "> ", f)?; + } w!("{:?}", &self.value.ret)?; if !self.value.ensures.is_empty() { w!("; [{:?}]", join!(", ", &self.value.ensures))?; @@ -2253,7 +2259,9 @@ mod pretty { return Ok(()); } if idx.is_unit() { - w!("[]")?; + if bty.is_adt() { + w!("[]")?; + } } else { w!("[{:?}]", idx)?; } diff --git a/crates/flux-middle/src/rty/refining.rs b/crates/flux-middle/src/rty/refining.rs index 7722ed8c9d..8ef74676ad 100644 --- a/crates/flux-middle/src/rty/refining.rs +++ b/crates/flux-middle/src/rty/refining.rs @@ -7,7 +7,12 @@ use rustc_hir::def_id::DefId; use rustc_middle::ty::{ClosureKind, ParamTy}; use super::fold::TypeFoldable; -use crate::{global_env::GlobalEnv, intern::List, queries::QueryResult, rty, rustc}; +use crate::{ + global_env::GlobalEnv, + intern::List, + queries::{QueryErr, QueryResult}, + rty, rustc, +}; pub(crate) fn refine_generics(generics: &rustc::ty::Generics) -> QueryResult { let params = generics @@ -237,8 +242,11 @@ impl<'genv, 'tcx> Refiner<'genv, 'tcx> { Ok(rty::GenericArg::Ty(self.refine_ty(ty)?)) } (rty::GenericParamDefKind::Base, rustc::ty::GenericArg::Ty(ty)) => { - let poly_constr = self.refine_ty_inner(ty)?.expect_simple(); - Ok(rty::GenericArg::Base(poly_constr)) + let TyOrBase::Base(contr) = self.refine_ty_inner(ty)? else { + let def_span = self.genv.tcx().def_span(param.def_id); + return Err(QueryErr::InvalidGenericArg { def_id: param.def_id, def_span }); + }; + Ok(rty::GenericArg::Base(contr)) } (rty::GenericParamDefKind::Lifetime, rustc::ty::GenericArg::Lifetime(re)) => { Ok(rty::GenericArg::Lifetime(*re)) diff --git a/crates/flux-refineck/locales/en-US.ftl b/crates/flux-refineck/locales/en-US.ftl index 4909a54da7..35f93c1cc1 100644 --- a/crates/flux-refineck/locales/en-US.ftl +++ b/crates/flux-refineck/locales/en-US.ftl @@ -28,9 +28,6 @@ refineck_assert_error = refineck_param_inference_error = parameter inference error at function call -refineck_invalid_generic_arg = - cannot instantiate base or spl generic with opaque type - refineck_fold_error = type invariant may not hold (when place is folded) diff --git a/crates/flux-refineck/src/checker.rs b/crates/flux-refineck/src/checker.rs index 8825a17145..04b101e4cd 100644 --- a/crates/flux-refineck/src/checker.rs +++ b/crates/flux-refineck/src/checker.rs @@ -1425,7 +1425,6 @@ pub(crate) mod errors { Inference, OpaqueStruct(DefId), Query(QueryErr), - InvalidGenericArg, } impl CheckerError { @@ -1447,12 +1446,6 @@ pub(crate) mod errors { flux_errors::diagnostic_id(), ) } - CheckerErrKind::InvalidGenericArg => { - handler.struct_err_with_code( - fluent::refineck_invalid_generic_arg, - flux_errors::diagnostic_id(), - ) - } CheckerErrKind::OpaqueStruct(def_id) => { let mut builder = handler.struct_err_with_code( fluent::refineck_opaque_struct_error, diff --git a/crates/flux-refineck/src/constraint_gen.rs b/crates/flux-refineck/src/constraint_gen.rs index 31c4b216d9..4e62db02fd 100644 --- a/crates/flux-refineck/src/constraint_gen.rs +++ b/crates/flux-refineck/src/constraint_gen.rs @@ -9,9 +9,8 @@ use flux_middle::{ evars::{EVarCxId, EVarSol}, fold::TypeFoldable, AliasTy, BaseTy, BinOp, Binder, Constraint, CoroutineObligPredicate, ESpan, EVarGen, - EarlyBinder, Expr, ExprKind, FnOutput, GenericArg, GenericParamDefKind, HoleKind, - InferMode, Lambda, Mutability, Path, PolyFnSig, PolyVariant, PtrKind, Ref, Sort, Ty, - TyKind, Var, + EarlyBinder, Expr, ExprKind, FnOutput, GenericArg, HoleKind, InferMode, Lambda, Mutability, + Path, PolyFnSig, PolyVariant, PtrKind, Ref, Sort, Ty, TyKind, Var, }, rustc::mir::{BasicBlock, Place}, }; @@ -145,22 +144,6 @@ impl<'a, 'genv, 'tcx> ConstrGen<'a, 'genv, 'tcx> { .collect() } - fn check_generic_args(&self, did: DefId, generic_args: &[GenericArg]) -> Result { - let generics = self.genv.generics_of(did)?; - for (idx, arg) in generic_args.iter().enumerate() { - let param = generics.param_at(idx, self.genv)?; - match param.kind { - GenericParamDefKind::Base => { - if !arg.is_valid_base_arg() { - return Err(CheckerErrKind::InvalidGenericArg); - } - } - _ => continue, - } - } - Ok(()) - } - #[allow(clippy::too_many_arguments)] pub(crate) fn check_fn_call( &mut self, @@ -174,10 +157,6 @@ impl<'a, 'genv, 'tcx> ConstrGen<'a, 'genv, 'tcx> { let genv = self.genv; let span = self.span; - if let Some(did) = callee_def_id { - self.check_generic_args(did, generic_args)?; - } - let mut infcx = self.infcx(rcx, ConstrReason::Call); let snapshot = rcx.snapshot(); From c2b70c4ab2ca3d5ac0ccbe2b7701469a96cd2d88 Mon Sep 17 00:00:00 2001 From: Nico Lehmann Date: Fri, 16 Feb 2024 23:12:44 -0800 Subject: [PATCH 14/22] improve pprint a bit --- crates/flux-middle/src/rty/mod.rs | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/crates/flux-middle/src/rty/mod.rs b/crates/flux-middle/src/rty/mod.rs index 7b8057ec79..b596a1532f 100644 --- a/crates/flux-middle/src/rty/mod.rs +++ b/crates/flux-middle/src/rty/mod.rs @@ -2245,7 +2245,11 @@ mod pretty { impl Pretty for SimpleTy { fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result { define_scoped!(cx, f); - w!("{{ {:?}[{:?}] | {:?} }}", &self.bty, &self.idx, &self.pred) + if self.pred.is_trivially_true() { + w!("{:?}[{:?}]", &self.bty, &self.idx) + } else { + w!("{{ {:?}[{:?}] | {:?} }}", &self.bty, &self.idx, &self.pred) + } } } From 797993b5bb10ab941047338819689608663ab012 Mon Sep 17 00:00:00 2001 From: Nico Lehmann Date: Sat, 17 Feb 2024 16:27:19 -0800 Subject: [PATCH 15/22] minor improvements --- crates/flux-middle/src/rty/canonicalize.rs | 36 +++++++++++++++++++--- crates/flux-middle/src/rty/evars.rs | 2 +- crates/flux-middle/src/rty/expr.rs | 6 ++++ crates/flux-middle/src/rty/projections.rs | 9 ++++-- crates/flux-refineck/src/refine_tree.rs | 2 +- 5 files changed, 46 insertions(+), 9 deletions(-) diff --git a/crates/flux-middle/src/rty/canonicalize.rs b/crates/flux-middle/src/rty/canonicalize.rs index fc28dbeb85..1cff77c301 100644 --- a/crates/flux-middle/src/rty/canonicalize.rs +++ b/crates/flux-middle/src/rty/canonicalize.rs @@ -26,6 +26,7 @@ impl Hoister { impl TypeFolder for Hoister { fn fold_ty(&mut self, ty: &Ty) -> Ty { match ty.kind() { + TyKind::Indexed(bty, idx) => Ty::indexed(bty.fold_with(self), idx.clone()), TyKind::Exists(ty) => { ty.replace_bound_refts_with(|sort, mode, kind| { let idx = self.vars.len(); @@ -93,12 +94,10 @@ impl CanonicalTy { if let TyKind::Indexed(bty, idx) = constr.ty.kind() { // given {b[e] | p} return λv. {b[v] | p ∧ v == e} let sort = bty.sort(); - let bty = bty.shift_in_escaping(1); - let pred = constr.pred.shift_in_escaping(1); let constr = SimpleTy::new( - bty, + bty.clone(), Expr::nu(), - Expr::and([pred, Expr::eq(Expr::nu(), idx)]), + Expr::and([constr.pred.clone(), Expr::eq(Expr::nu(), idx)]), ); Some(Binder::with_sort(constr, sort)) } else { @@ -121,3 +120,32 @@ impl CanonicalTy { } } } + +mod pretty { + use super::*; + use crate::pretty::*; + + impl Pretty for CanonicalConstrTy { + fn fmt(&self, cx: &PrettyCx, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + define_scoped!(cx, f); + w!("{{ {:?} | {:?} }}", &self.ty, &self.pred) + } + } + + impl Pretty for CanonicalTy { + fn fmt(&self, cx: &PrettyCx, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + define_scoped!(cx, f); + match self { + CanonicalTy::Constr(constr) => w!("{:?}", constr), + CanonicalTy::Exists(poly_constr) => { + cx.with_bound_vars(poly_constr.vars(), || { + cx.fmt_bound_vars("∃", poly_constr.vars(), ". ", f)?; + w!("{:?}", poly_constr.as_ref().skip_binder()) + }) + } + } + } + } + + impl_debug_with_default_cx!(CanonicalTy); +} diff --git a/crates/flux-middle/src/rty/evars.rs b/crates/flux-middle/src/rty/evars.rs index 39ddb4175c..aa0b1973ff 100644 --- a/crates/flux-middle/src/rty/evars.rs +++ b/crates/flux-middle/src/rty/evars.rs @@ -149,7 +149,7 @@ mod pretty { impl Pretty for EVar { fn fmt(&self, _cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result { define_scoped!(cx, f); - w!("?e{}#{}", ^self.id.as_u32(), ^self.cx.0) + w!("?{}e#{}", ^self.id.as_u32(), ^self.cx.0) } } diff --git a/crates/flux-middle/src/rty/expr.rs b/crates/flux-middle/src/rty/expr.rs index 13062c8de0..ee0f579a28 100644 --- a/crates/flux-middle/src/rty/expr.rs +++ b/crates/flux-middle/src/rty/expr.rs @@ -824,6 +824,12 @@ impl From for Expr { } } +impl From for Expr { + fn from(var: Var) -> Self { + Expr::var(var, None) + } +} + impl From for Path { fn from(loc: Loc) -> Self { Path::new(loc, vec![]) diff --git a/crates/flux-middle/src/rty/projections.rs b/crates/flux-middle/src/rty/projections.rs index 71a618183e..4cdbcc3e7c 100644 --- a/crates/flux-middle/src/rty/projections.rs +++ b/crates/flux-middle/src/rty/projections.rs @@ -146,7 +146,7 @@ impl<'genv, 'tcx, 'cx> Normalizer<'genv, 'tcx, 'cx> { &self, obligation: &AliasTy, candidates: &mut Vec, - ) -> QueryResult<()> { + ) -> QueryResult { if let GenericArg::Ty(ty) = &obligation.args[0] && let TyKind::Alias(AliasKind::Opaque, alias_ty) = ty.kind() { @@ -321,11 +321,14 @@ impl TVarSubst { fn infer_from_ty(&mut self, src: &rustc_middle::ty::Ty, dst: &Ty) { use rustc_middle::ty; match src.kind() { - ty::TyKind::Param(pty) => self.insert_param_ty(*pty, dst), + ty::TyKind::Param(pty) => { + if !dst.has_escaping_bvars() { + self.insert_param_ty(*pty, dst); + } + } ty::TyKind::Adt(_, src_subst) => { // NOTE: see https://github.com/flux-rs/flux/pull/478#issuecomment-1650983695 if let Some(dst) = dst.as_bty_skipping_existentials() - && !dst.has_escaping_bvars() && let BaseTy::Adt(_, dst_subst) = dst { debug_assert_eq!(src_subst.len(), dst_subst.len()); diff --git a/crates/flux-refineck/src/refine_tree.rs b/crates/flux-refineck/src/refine_tree.rs index 8ef6df2ca2..44e583ca08 100644 --- a/crates/flux-refineck/src/refine_tree.rs +++ b/crates/flux-refineck/src/refine_tree.rs @@ -321,7 +321,7 @@ impl<'a, 'rcx> Unpacker<'a, 'rcx> { impl TypeFolder for Unpacker<'_, '_> { fn fold_ty(&mut self, ty: &Ty) -> Ty { match ty.kind() { - TyKind::Indexed(bty, idxs) => Ty::indexed(bty.fold_with(self), idxs.clone()), + TyKind::Indexed(bty, idx) => Ty::indexed(bty.fold_with(self), idx.clone()), TyKind::Exists(bound_ty) if self.unpack_exists => { // HACK(nilehmann) In general we shouldn't unpack through mutable references because // that makes referent type too specific. We only have this as a workaround to infer From 283a7b214f7af12cd006ddcd8803bfe8935e4b26 Mon Sep 17 00:00:00 2001 From: Nico Lehmann Date: Sat, 17 Feb 2024 19:11:14 -0800 Subject: [PATCH 16/22] All tests passing --- crates/flux-fhir-analysis/src/conv.rs | 2 +- crates/flux-middle/src/global_env.rs | 4 +- crates/flux-middle/src/rty/canonicalize.rs | 20 +- crates/flux-middle/src/rty/fold.rs | 20 +- crates/flux-middle/src/rty/mod.rs | 118 ++++----- crates/flux-middle/src/rty/projections.rs | 274 ++++++++++++++------- crates/flux-middle/src/rty/refining.rs | 14 +- crates/flux-middle/src/rty/subst.rs | 12 +- crates/flux-refineck/src/checker.rs | 4 +- crates/flux-refineck/src/type_env.rs | 4 +- 10 files changed, 291 insertions(+), 181 deletions(-) diff --git a/crates/flux-fhir-analysis/src/conv.rs b/crates/flux-fhir-analysis/src/conv.rs index fb59471d83..46e0c2781f 100644 --- a/crates/flux-fhir-analysis/src/conv.rs +++ b/crates/flux-fhir-analysis/src/conv.rs @@ -938,7 +938,7 @@ impl<'a, 'genv, 'tcx> ConvCtxt<'a, 'genv, 'tcx> { let ctor = self .conv_ty(env, ty)? .shallow_canonicalize() - .to_simple_ty_ctor() + .to_subset_ty_ctor() .ok_or_else(|| { self.genv .sess() diff --git a/crates/flux-middle/src/global_env.rs b/crates/flux-middle/src/global_env.rs index 481abc0109..db30b19dfe 100644 --- a/crates/flux-middle/src/global_env.rs +++ b/crates/flux-middle/src/global_env.rs @@ -215,8 +215,8 @@ impl<'genv, 'tcx> GlobalEnv<'genv, 'tcx> { let trait_ref = lowering::lower_trait_ref(self.tcx(), poly_trait_ref.skip_binder()) .map_err(|err| QueryErr::unsupported(self.tcx(), impl_id, err.into_err()))?; - let trait_generics = self.generics_of(trait_ref.def_id)?; - let trait_ref = Refiner::default(self, &trait_generics).refine_trait_ref(&trait_ref)?; + let impl_generics = self.generics_of(impl_id)?; + let trait_ref = Refiner::default(self, &impl_generics).refine_trait_ref(&trait_ref)?; Ok(Some(rty::EarlyBinder(trait_ref))) } diff --git a/crates/flux-middle/src/rty/canonicalize.rs b/crates/flux-middle/src/rty/canonicalize.rs index 1cff77c301..8c4c42a721 100644 --- a/crates/flux-middle/src/rty/canonicalize.rs +++ b/crates/flux-middle/src/rty/canonicalize.rs @@ -3,7 +3,7 @@ use rustc_type_ir::{Mutability, INNERMOST}; use super::{ box_args, fold::{TypeFoldable, TypeFolder}, - BaseTy, Binder, BoundVariableKind, Expr, GenericArg, SimpleTy, SimpleTyCtor, Ty, TyKind, + BaseTy, Binder, BoundVariableKind, Expr, GenericArg, SubsetTy, SubsetTyCtor, Ty, TyKind, }; use crate::intern::List; @@ -82,19 +82,29 @@ pub struct CanonicalConstrTy { pred: Expr, } +impl CanonicalConstrTy { + pub fn ty(&self) -> Ty { + self.ty.clone() + } + + pub fn pred(&self) -> Expr { + self.pred.clone() + } +} + pub enum CanonicalTy { Constr(CanonicalConstrTy), Exists(Binder), } impl CanonicalTy { - pub fn to_simple_ty_ctor(&self) -> Option { + pub fn to_subset_ty_ctor(&self) -> Option { match self { CanonicalTy::Constr(constr) => { if let TyKind::Indexed(bty, idx) = constr.ty.kind() { // given {b[e] | p} return λv. {b[v] | p ∧ v == e} let sort = bty.sort(); - let constr = SimpleTy::new( + let constr = SubsetTy::new( bty.clone(), Expr::nu(), Expr::and([constr.pred.clone(), Expr::eq(Expr::nu(), idx)]), @@ -111,7 +121,7 @@ impl CanonicalTy { { let ctor = poly_constr .as_ref() - .map(|constr| SimpleTy::new(bty.clone(), Expr::nu(), &constr.pred)); + .map(|constr| SubsetTy::new(bty.clone(), Expr::nu(), &constr.pred)); Some(ctor) } else { None @@ -147,5 +157,5 @@ mod pretty { } } - impl_debug_with_default_cx!(CanonicalTy); + impl_debug_with_default_cx!(CanonicalTy, CanonicalConstrTy); } diff --git a/crates/flux-middle/src/rty/fold.rs b/crates/flux-middle/src/rty/fold.rs index 36a3f74596..c031b4e4c5 100644 --- a/crates/flux-middle/src/rty/fold.rs +++ b/crates/flux-middle/src/rty/fold.rs @@ -17,7 +17,7 @@ use super::{ AliasReft, AliasTy, BaseTy, BinOp, Binder, BoundVariableKind, Clause, ClauseKind, Constraint, CoroutineObligPredicate, Expr, ExprKind, FnOutput, FnSig, FnTraitPredicate, FuncSort, GenericArg, Invariant, KVar, Lambda, Name, OpaqueArgsMap, Opaqueness, OutlivesPredicate, - PolyFuncSort, ProjectionPredicate, PtrKind, Qualifier, ReLateBound, Region, SimpleTy, Sort, + PolyFuncSort, ProjectionPredicate, PtrKind, Qualifier, ReLateBound, Region, Sort, SubsetTy, TraitPredicate, TraitRef, Ty, TyKind, }; use crate::{ @@ -77,7 +77,7 @@ pub trait FallibleTypeFolder: Sized { bty.try_super_fold_with(self) } - fn try_fold_simple_ty(&mut self, constr: &SimpleTy) -> Result { + fn try_fold_subset_ty(&mut self, constr: &SubsetTy) -> Result { constr.try_super_fold_with(self) } @@ -107,7 +107,7 @@ pub trait TypeFolder: FallibleTypeFolder { bty.super_fold_with(self) } - fn fold_simple_ty(&mut self, constr: &SimpleTy) -> SimpleTy { + fn fold_subset_ty(&mut self, constr: &SubsetTy) -> SubsetTy { constr.super_fold_with(self) } @@ -145,8 +145,8 @@ where Ok(self.fold_bty(bty)) } - fn try_fold_simple_ty(&mut self, constr: &SimpleTy) -> Result { - Ok(self.fold_simple_ty(constr)) + fn try_fold_subset_ty(&mut self, ty: &SubsetTy) -> Result { + Ok(self.fold_subset_ty(ty)) } fn try_fold_region(&mut self, re: &Region) -> Result { @@ -979,7 +979,7 @@ impl TypeFoldable for AliasTy { } } -impl TypeVisitable for SimpleTy { +impl TypeVisitable for SubsetTy { fn visit_with(&self, visitor: &mut V) -> ControlFlow { self.bty.visit_with(visitor)?; self.idx.visit_with(visitor)?; @@ -987,15 +987,15 @@ impl TypeVisitable for SimpleTy { } } -impl TypeFoldable for SimpleTy { +impl TypeFoldable for SubsetTy { fn try_fold_with(&self, folder: &mut F) -> Result { - folder.try_fold_simple_ty(self) + folder.try_fold_subset_ty(self) } } -impl TypeSuperFoldable for SimpleTy { +impl TypeSuperFoldable for SubsetTy { fn try_super_fold_with(&self, folder: &mut F) -> Result { - Ok(SimpleTy { + Ok(SubsetTy { bty: self.bty.try_fold_with(folder)?, idx: self.idx.try_fold_with(folder)?, pred: self.pred.try_fold_with(folder)?, diff --git a/crates/flux-middle/src/rty/mod.rs b/crates/flux-middle/src/rty/mod.rs index b596a1532f..22110acaa8 100644 --- a/crates/flux-middle/src/rty/mod.rs +++ b/crates/flux-middle/src/rty/mod.rs @@ -729,6 +729,57 @@ impl Ty { | TyKind::Blocked(_) => todo!(), } } + + /// Whether the type is an `int` or a `uint` + pub fn is_integral(&self) -> bool { + self.as_bty_skipping_existentials() + .map(BaseTy::is_integral) + .unwrap_or_default() + } + + /// Whether the type is a `bool` + pub fn is_bool(&self) -> bool { + self.as_bty_skipping_existentials() + .map(BaseTy::is_bool) + .unwrap_or_default() + } + + pub fn is_uninit(&self) -> bool { + matches!(self.kind(), TyKind::Uninit) + } + + pub fn is_box(&self) -> bool { + self.as_bty_skipping_existentials() + .map(BaseTy::is_box) + .unwrap_or_default() + } + + pub fn is_struct(&self) -> bool { + self.as_bty_skipping_existentials() + .map(BaseTy::is_struct) + .unwrap_or_default() + } + + pub fn is_array(&self) -> bool { + self.as_bty_skipping_existentials() + .map(BaseTy::is_array) + .unwrap_or_default() + } + + pub fn is_slice(&self) -> bool { + self.as_bty_skipping_existentials() + .map(BaseTy::is_slice) + .unwrap_or_default() + } + + pub fn as_bty_skipping_existentials(&self) -> Option<&BaseTy> { + match self.kind() { + TyKind::Indexed(bty, _) => Some(bty), + TyKind::Exists(ty) => Some(ty.as_ref().skip_binder().as_bty_skipping_existentials()?), + TyKind::Constr(_, ty) => ty.as_bty_skipping_existentials(), + _ => None, + } + } } #[derive(Clone, PartialEq, Eq, Hash, TyEncodable, TyDecodable)] @@ -811,9 +862,9 @@ pub type RefineArgs = List; pub type OpaqueArgsMap = FxHashMap; -pub type SimpleTyCtor = Binder; +pub type SubsetTyCtor = Binder; -impl SimpleTyCtor { +impl SubsetTyCtor { pub fn as_bty_skipping_binder(&self) -> &BaseTy { &self.as_ref().skip_binder().bty } @@ -825,19 +876,19 @@ impl SimpleTyCtor { } else if let Some(def_id) = sort.is_unit_adt() { self.replace_bound_reft(&Expr::unit_adt(def_id)).to_ty() } else { - Ty::exists(self.as_ref().map(SimpleTy::to_ty)) + Ty::exists(self.as_ref().map(SubsetTy::to_ty)) } } } #[derive(PartialEq, Clone, Eq, Hash, TyEncodable, TyDecodable)] -pub struct SimpleTy { +pub struct SubsetTy { pub bty: BaseTy, pub idx: Expr, pub pred: Expr, } -impl SimpleTy { +impl SubsetTy { pub fn new(bty: BaseTy, idx: impl Into, pred: impl Into) -> Self { Self { bty, idx: idx.into(), pred: pred.into() } } @@ -868,7 +919,7 @@ impl SimpleTy { #[derive(PartialEq, Clone, Eq, Hash, TyEncodable, TyDecodable)] pub enum GenericArg { Ty(Ty), - Base(SimpleTyCtor), + Base(SubsetTyCtor), Lifetime(Region), Const(Const), } @@ -1622,57 +1673,6 @@ impl TyS { bug!("expected tuple found `{self:?}` (kind: `{:?}`)", self.kind()) } } - - /// Whether the type is an `int` or a `uint` - pub fn is_integral(&self) -> bool { - self.as_bty_skipping_existentials() - .map(BaseTy::is_integral) - .unwrap_or_default() - } - - /// Whether the type is a `bool` - pub fn is_bool(&self) -> bool { - self.as_bty_skipping_existentials() - .map(BaseTy::is_bool) - .unwrap_or_default() - } - - pub fn is_uninit(&self) -> bool { - matches!(self.kind(), TyKind::Uninit) - } - - pub fn is_box(&self) -> bool { - self.as_bty_skipping_existentials() - .map(BaseTy::is_box) - .unwrap_or_default() - } - - pub fn is_struct(&self) -> bool { - self.as_bty_skipping_existentials() - .map(BaseTy::is_struct) - .unwrap_or_default() - } - - pub fn is_array(&self) -> bool { - self.as_bty_skipping_existentials() - .map(BaseTy::is_array) - .unwrap_or_default() - } - - pub fn is_slice(&self) -> bool { - self.as_bty_skipping_existentials() - .map(BaseTy::is_slice) - .unwrap_or_default() - } - - pub fn as_bty_skipping_existentials(&self) -> Option<&BaseTy> { - match self.kind() { - TyKind::Indexed(bty, _) => Some(bty), - TyKind::Exists(ty) => Some(ty.as_ref().skip_binder().as_bty_skipping_existentials()?), - TyKind::Constr(_, ty) => ty.as_bty_skipping_existentials(), - _ => None, - } - } } impl AliasTy { @@ -2242,7 +2242,7 @@ mod pretty { } } - impl Pretty for SimpleTy { + impl Pretty for SubsetTy { fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result { define_scoped!(cx, f); if self.pred.is_trivially_true() { @@ -2483,6 +2483,6 @@ mod pretty { PtrKind, FuncSort, SortCtor, - SimpleTy, + SubsetTy, ); } diff --git a/crates/flux-middle/src/rty/projections.rs b/crates/flux-middle/src/rty/projections.rs index 4cdbcc3e7c..5f3abfe451 100644 --- a/crates/flux-middle/src/rty/projections.rs +++ b/crates/flux-middle/src/rty/projections.rs @@ -11,9 +11,10 @@ use rustc_middle::{ use rustc_trait_selection::traits::SelectionContext; use super::{ + canonicalize::{CanonicalConstrTy, CanonicalTy}, fold::{FallibleTypeFolder, TypeSuperFoldable}, AliasKind, AliasReft, AliasTy, BaseTy, Clause, ClauseKind, Expr, ExprKind, GenericArg, - GenericArgs, ProjectionPredicate, RefineArgs, Region, Ty, TyKind, + GenericArgs, ProjectionPredicate, RefineArgs, Region, SubsetTy, Ty, TyKind, }; use crate::{ global_env::GlobalEnv, @@ -49,14 +50,16 @@ impl<'genv, 'tcx, 'cx> Normalizer<'genv, 'tcx, 'cx> { ) -> QueryResult { if let Some(impl_def_id) = self.impl_id_of_alias_reft(obligation)? { let impl_trait_ref = self - .tcx() - .impl_trait_ref(impl_def_id) + .genv + .impl_trait_ref(impl_def_id)? .unwrap() .skip_binder(); let generics = self.tcx().generics_of(impl_def_id); - let mut subst = TVarSubst::new(generics); - subst.infer_from_args(impl_trait_ref.args, &obligation.args); + let mut subst = Equate::new(generics); + for (a, b) in iter::zip(&impl_trait_ref.args, &obligation.args) { + subst.generic_args(a, b); + } let args = subst.finish(self.tcx(), generics); let pred = self @@ -100,15 +103,17 @@ impl<'genv, 'tcx, 'cx> Normalizer<'genv, 'tcx, 'cx> { // => {T -> {v. i32[v] | v > 0}, A -> Global} let impl_trait_ref = self - .tcx() - .impl_trait_ref(impl_def_id) + .genv + .impl_trait_ref(impl_def_id)? .unwrap() .skip_binder(); let generics = self.tcx().generics_of(impl_def_id); - let mut subst = TVarSubst::new(generics); - subst.infer_from_args(impl_trait_ref.args, &obligation.args); + let mut subst = Equate::new(generics); + for (a, b) in iter::zip(&impl_trait_ref.args, &obligation.args) { + subst.generic_args(a, b); + } let args = subst.finish(self.tcx(), generics); // 2. Get the associated type in the impl block and apply the substitution to it @@ -254,12 +259,139 @@ pub enum Candidate { TraitDef(ProjectionPredicate), } +// #[derive(Debug)] +// struct TVarSubst { +// args: Vec>, +// } + +// impl TVarSubst { +// fn new(generics: &rustc_middle::ty::Generics) -> Self { +// Self { args: vec![None; generics.count()] } +// } + +// fn finish<'tcx>( +// self, +// tcx: TyCtxt<'tcx>, +// generics: &'tcx rustc_middle::ty::Generics, +// ) -> Vec { +// self.args +// .into_iter() +// .enumerate() +// .map(|(idx, arg)| { +// if let Some(arg) = arg { +// arg +// } else { +// let param = generics.param_at(idx, tcx); +// bug!("cannot infer substitution for param {param:?}"); +// } +// }) +// .collect() +// } + +// fn insert_param_ty(&mut self, pty: ParamTy, ty: &Ty) { +// let arg = GenericArg::Ty(ty.clone()); +// if self.args[pty.index as usize].replace(arg).is_some() { +// bug!("duplicate insert"); +// } +// } + +// fn insert_early_bound_region(&mut self, ebr: EarlyBoundRegion, re: Region) { +// let arg = GenericArg::Lifetime(re); +// if self.args[ebr.index as usize].replace(arg).is_some() { +// bug!("duplicate insert"); +// } +// } + +// fn infer_from_args(&mut self, src: rustc_middle::ty::GenericArgsRef, dst: &GenericArgs) { +// debug_assert_eq!(src.len(), dst.len()); +// for (src, dst) in iter::zip(src, dst) { +// self.infer_from_arg(src, dst); +// } +// } + +// fn infer_from_arg(&mut self, src: rustc_middle::ty::GenericArg, dst: &GenericArg) { +// match dst { +// GenericArg::Ty(dst) => { +// self.infer_from_ty(&src.as_type().unwrap(), dst); +// } +// GenericArg::Lifetime(dst) => self.infer_from_region(&src.as_region().unwrap(), dst), +// GenericArg::Base(ty) => { +// // todo!() +// // self.infer_from_ty(&src.as_type().unwrap(), ty.bty_skipping_binder()); +// } +// _ => (), +// } +// } + +// fn infer_from_ty(&mut self, src: &rustc_middle::ty::Ty, dst: &Ty) { +// use rustc_middle::ty; +// match src.kind() { +// ty::TyKind::Param(pty) => { +// if !dst.has_escaping_bvars() { +// self.insert_param_ty(*pty, dst); +// } +// } +// ty::TyKind::Adt(_, src_subst) => { +// // NOTE: see https://github.com/flux-rs/flux/pull/478#issuecomment-1650983695 +// if let Some(dst) = dst.as_bty_skipping_existentials() +// && let BaseTy::Adt(_, dst_subst) = dst +// { +// debug_assert_eq!(src_subst.len(), dst_subst.len()); +// for (src_arg, dst_arg) in iter::zip(*src_subst, dst_subst) { +// self.infer_from_arg(src_arg, dst_arg); +// } +// } else { +// bug!("unexpected type {dst:?}"); +// } +// } +// ty::TyKind::Array(src, _) => { +// if let Some(BaseTy::Array(dst, _)) = dst.as_bty_skipping_existentials() { +// self.infer_from_ty(src, dst); +// } else { +// bug!("unexpected type {dst:?}"); +// } +// } +// ty::TyKind::Slice(src) => { +// if let Some(BaseTy::Slice(dst)) = dst.as_bty_skipping_existentials() { +// self.infer_from_ty(src, dst); +// } else { +// bug!("unexpected type {dst:?}"); +// } +// } +// ty::TyKind::Tuple(src_tys) => { +// if let Some(BaseTy::Tuple(dst_tys)) = dst.as_bty_skipping_existentials() { +// debug_assert_eq!(src_tys.len(), dst_tys.len()); +// iter::zip(src_tys.iter(), dst_tys.iter()) +// .for_each(|(src, dst)| self.infer_from_ty(&src, dst)); +// } else { +// bug!("unexpected type {dst:?}"); +// } +// } +// ty::TyKind::Ref(src_re, src_ty, _) => { +// if let Some(BaseTy::Ref(dst_re, dst_ty, _)) = dst.as_bty_skipping_existentials() { +// self.infer_from_region(src_re, dst_re); +// self.infer_from_ty(src_ty, dst_ty); +// } else { +// bug!("unexpected type {dst:?}"); +// } +// } +// _ => {} +// } +// } + +// fn infer_from_region(&mut self, src: &rustc_middle::ty::Region, dst: &Region) { +// if let rustc_middle::ty::RegionKind::ReEarlyBound(ebr) = src.kind() { +// self.insert_early_bound_region(ebr, *dst); +// } +// } +// } + #[derive(Debug)] -struct TVarSubst { +struct Equate { args: Vec>, } -impl TVarSubst { +impl Equate { fn new(generics: &rustc_middle::ty::Generics) -> Self { Self { args: vec![None; generics.count()] } } @@ -283,100 +415,68 @@ impl TVarSubst { .collect() } - fn insert_param_ty(&mut self, pty: ParamTy, ty: &Ty) { - let arg = GenericArg::Ty(ty.clone()); - if self.args[pty.index as usize].replace(arg).is_some() { - bug!("duplicate insert"); - } - } - - fn insert_early_bound_region(&mut self, ebr: EarlyBoundRegion, re: Region) { - let arg = GenericArg::Lifetime(re); - if self.args[ebr.index as usize].replace(arg).is_some() { - bug!("duplicate insert"); - } - } - - fn infer_from_args(&mut self, src: rustc_middle::ty::GenericArgsRef, dst: &GenericArgs) { - debug_assert_eq!(src.len(), dst.len()); - for (src, dst) in iter::zip(src, dst) { - self.infer_from_arg(src, dst); + fn generic_args(&mut self, a: &GenericArg, b: &GenericArg) { + match (a, b) { + (GenericArg::Ty(a), GenericArg::Ty(b)) => self.tys(a, b), + (GenericArg::Lifetime(a), GenericArg::Lifetime(b)) => self.regions(*a, *b), + (GenericArg::Base(a), GenericArg::Base(b)) => { + debug_assert_eq!(a.sort(), b.sort()); + self.btys(a.as_bty_skipping_binder(), b.as_bty_skipping_binder()); + } + _ => {} } } - fn infer_from_arg(&mut self, src: rustc_middle::ty::GenericArg, dst: &GenericArg) { - match dst { - GenericArg::Ty(dst) => { - self.infer_from_ty(&src.as_type().unwrap(), dst); + fn tys(&mut self, a: &Ty, b: &Ty) { + if let TyKind::Param(param_ty) = a.kind() { + if !b.has_escaping_bvars() { + self.insert_generic_arg(param_ty.index, GenericArg::Ty(b.clone())); } - GenericArg::Lifetime(dst) => self.infer_from_region(&src.as_region().unwrap(), dst), - GenericArg::Base(ty) => { - // todo!() - // self.infer_from_ty(&src.as_type().unwrap(), ty.bty_skipping_binder()); - } - _ => (), + return; } + let Some(a_bty) = a.as_bty_skipping_existentials() else { return }; + let Some(b_bty) = b.as_bty_skipping_existentials() else { return }; + self.btys(a_bty, b_bty); } - fn infer_from_ty(&mut self, src: &rustc_middle::ty::Ty, dst: &Ty) { - use rustc_middle::ty; - match src.kind() { - ty::TyKind::Param(pty) => { - if !dst.has_escaping_bvars() { - self.insert_param_ty(*pty, dst); + fn btys(&mut self, a: &BaseTy, b: &BaseTy) { + match (a, b) { + (BaseTy::Param(_), _) => todo!(), + (BaseTy::Adt(_, a_args), BaseTy::Adt(_, b_args)) => { + debug_assert_eq!(a_args.len(), b_args.len()); + for (a_arg, b_arg) in iter::zip(a_args, b_args) { + self.generic_args(a_arg, b_arg); } } - ty::TyKind::Adt(_, src_subst) => { - // NOTE: see https://github.com/flux-rs/flux/pull/478#issuecomment-1650983695 - if let Some(dst) = dst.as_bty_skipping_existentials() - && let BaseTy::Adt(_, dst_subst) = dst - { - debug_assert_eq!(src_subst.len(), dst_subst.len()); - for (src_arg, dst_arg) in iter::zip(*src_subst, dst_subst) { - self.infer_from_arg(src_arg, dst_arg); - } - } else { - bug!("unexpected type {dst:?}"); - } + (BaseTy::Array(a_ty, _), BaseTy::Array(b_ty, _)) => { + self.tys(a_ty, b_ty); } - ty::TyKind::Array(src, _) => { - if let Some(BaseTy::Array(dst, _)) = dst.as_bty_skipping_existentials() { - self.infer_from_ty(src, dst); - } else { - bug!("unexpected type {dst:?}"); + (BaseTy::Tuple(a_tys), BaseTy::Tuple(b_tys)) => { + debug_assert_eq!(a_tys.len(), b_tys.len()); + for (a_ty, b_ty) in iter::zip(a_tys, b_tys) { + self.tys(a_ty, b_ty); } } - ty::TyKind::Slice(src) => { - if let Some(BaseTy::Slice(dst)) = dst.as_bty_skipping_existentials() { - self.infer_from_ty(src, dst); - } else { - bug!("unexpected type {dst:?}"); - } + (BaseTy::Ref(a_re, a_ty, _), BaseTy::Ref(b_re, b_ty, _)) => { + self.regions(*a_re, *b_re); + self.tys(a_ty, b_ty); } - ty::TyKind::Tuple(src_tys) => { - if let Some(BaseTy::Tuple(dst_tys)) = dst.as_bty_skipping_existentials() { - debug_assert_eq!(src_tys.len(), dst_tys.len()); - iter::zip(src_tys.iter(), dst_tys.iter()) - .for_each(|(src, dst)| self.infer_from_ty(&src, dst)); - } else { - bug!("unexpected type {dst:?}"); - } - } - ty::TyKind::Ref(src_re, src_ty, _) => { - if let Some(BaseTy::Ref(dst_re, dst_ty, _)) = dst.as_bty_skipping_existentials() { - self.infer_from_region(src_re, dst_re); - self.infer_from_ty(src_ty, dst_ty); - } else { - bug!("unexpected type {dst:?}"); - } + (BaseTy::Slice(a_ty), BaseTy::Slice(b_ty)) => { + self.tys(a_ty, b_ty); } _ => {} } } - fn infer_from_region(&mut self, src: &rustc_middle::ty::Region, dst: &Region) { - if let rustc_middle::ty::RegionKind::ReEarlyBound(ebr) = src.kind() { - self.insert_early_bound_region(ebr, *dst); + fn regions(&mut self, a: Region, b: Region) { + if let Region::ReEarlyBound(ebr) = a { + self.insert_generic_arg(ebr.index, GenericArg::Lifetime(b)); + } + } + + fn insert_generic_arg(&mut self, idx: u32, arg: GenericArg) { + if self.args[idx as usize].replace(arg).is_some() { + bug!("duplicate insert"); } } } diff --git a/crates/flux-middle/src/rty/refining.rs b/crates/flux-middle/src/rty/refining.rs index 8ef74676ad..a287910674 100644 --- a/crates/flux-middle/src/rty/refining.rs +++ b/crates/flux-middle/src/rty/refining.rs @@ -43,14 +43,14 @@ pub(crate) fn refine_generics(generics: &rustc::ty::Generics) -> QueryResult { genv: GlobalEnv<'genv, 'tcx>, generics: rty::Generics, - refine: fn(rty::BaseTy) -> rty::Binder, + refine: fn(rty::BaseTy) -> rty::Binder, } impl<'genv, 'tcx> Refiner<'genv, 'tcx> { pub fn new( genv: GlobalEnv<'genv, 'tcx>, generics: &rty::Generics, - refine: fn(rty::BaseTy) -> rty::Binder, + refine: fn(rty::BaseTy) -> rty::Binder, ) -> Self { Self { genv, generics: generics.clone(), refine } } @@ -65,7 +65,7 @@ impl<'genv, 'tcx> Refiner<'genv, 'tcx> { generics: generics.clone(), refine: |bty| { let sort = bty.sort(); - let constr = rty::SimpleTy::new( + let constr = rty::SubsetTy::new( bty.shift_in_escaping(1), rty::Expr::nu(), rty::Expr::hole(rty::HoleKind::Pred), @@ -395,7 +395,7 @@ impl<'genv, 'tcx> Refiner<'genv, 'tcx> { enum TyOrBase { Ty(rty::Ty), - Base(rty::SimpleTyCtor), + Base(rty::SubsetTyCtor), } impl TyOrBase { @@ -407,7 +407,7 @@ impl TyOrBase { } #[track_caller] - fn expect_simple(self) -> rty::Binder { + fn expect_simple(self) -> rty::Binder { if let TyOrBase::Base(poly_constr) = self { poly_constr } else { @@ -416,9 +416,9 @@ impl TyOrBase { } } -fn refine_default(bty: rty::BaseTy) -> rty::Binder { +fn refine_default(bty: rty::BaseTy) -> rty::Binder { let sort = bty.sort(); - let constr = rty::SimpleTy::indexed(bty.shift_in_escaping(1), rty::Expr::nu()); + let constr = rty::SubsetTy::indexed(bty.shift_in_escaping(1), rty::Expr::nu()); rty::Binder::with_sort(constr, sort) } diff --git a/crates/flux-middle/src/rty/subst.rs b/crates/flux-middle/src/rty/subst.rs index 476d36ae62..86fa52dc09 100644 --- a/crates/flux-middle/src/rty/subst.rs +++ b/crates/flux-middle/src/rty/subst.rs @@ -253,7 +253,7 @@ pub(crate) struct GenericsSubstFolder<'a, D> { trait GenericsSubstDelegate { fn sort_for_param(&mut self, param_ty: ParamTy) -> Sort; fn ty_for_param(&mut self, param_ty: ParamTy) -> Ty; - fn ctor_for_param(&mut self, param_ty: ParamTy) -> SimpleTyCtor; + fn ctor_for_param(&mut self, param_ty: ParamTy) -> SubsetTyCtor; fn region_for_param(&mut self, ebr: EarlyBoundRegion) -> Region; } @@ -273,9 +273,9 @@ impl GenericsSubstDelegate for IdentitySubstDelegate { Ty::param(param_ty) } - fn ctor_for_param(&mut self, param_ty: ParamTy) -> SimpleTyCtor { + fn ctor_for_param(&mut self, param_ty: ParamTy) -> SubsetTyCtor { Binder::with_sort( - SimpleTy::indexed(BaseTy::Param(param_ty), Expr::nu()), + SubsetTy::indexed(BaseTy::Param(param_ty), Expr::nu()), Sort::Param(param_ty), ) } @@ -304,7 +304,7 @@ impl GenericsSubstDelegate for GenericArgsDelegate<'_> { } } - fn ctor_for_param(&mut self, param_ty: ParamTy) -> SimpleTyCtor { + fn ctor_for_param(&mut self, param_ty: ParamTy) -> SubsetTyCtor { match self.0.get(param_ty.index as usize) { Some(GenericArg::Base(ctor)) => ctor.clone(), Some(arg) => { @@ -353,7 +353,7 @@ where bug!("unexpected type param {param_ty:?}"); } - fn ctor_for_param(&mut self, param_ty: ParamTy) -> SimpleTyCtor { + fn ctor_for_param(&mut self, param_ty: ParamTy) -> SubsetTyCtor { bug!("unexpected base type param {param_ty:?}"); } @@ -398,7 +398,7 @@ impl TypeFolder for GenericsSubstFolder<'_, D> { } } - fn fold_simple_ty(&mut self, constr: &SimpleTy) -> SimpleTy { + fn fold_subset_ty(&mut self, constr: &SubsetTy) -> SubsetTy { if let BaseTy::Param(param_ty) = &constr.bty { self.delegate .ctor_for_param(*param_ty) diff --git a/crates/flux-refineck/src/checker.rs b/crates/flux-refineck/src/checker.rs index 04b101e4cd..aedbda588a 100644 --- a/crates/flux-refineck/src/checker.rs +++ b/crates/flux-refineck/src/checker.rs @@ -1149,9 +1149,9 @@ fn instantiate_args_for_fun_call( let sort = bty.sort(); let bty = bty.shift_in_escaping(1); let constr = if !sort.is_unit() { - rty::SimpleTy::new(bty, Expr::nu(), Expr::hole(rty::HoleKind::Pred)) + rty::SubsetTy::new(bty, Expr::nu(), Expr::hole(rty::HoleKind::Pred)) } else { - rty::SimpleTy::indexed(bty, Expr::nu()) + rty::SubsetTy::indexed(bty, Expr::nu()) }; Binder::with_sort(constr, sort) }); diff --git a/crates/flux-refineck/src/type_env.rs b/crates/flux-refineck/src/type_env.rs index ab2a47e75c..241034b8e7 100644 --- a/crates/flux-refineck/src/type_env.rs +++ b/crates/flux-refineck/src/type_env.rs @@ -12,7 +12,7 @@ use flux_middle::{ fold::{FallibleTypeFolder, TypeFoldable, TypeVisitable, TypeVisitor}, subst::RegionSubst, BaseTy, Binder, BoundReftKind, Expr, ExprKind, GenericArg, HoleKind, Mutability, Path, - PtrKind, Region, SimpleTy, SortCtor, Ty, TyKind, INNERMOST, + PtrKind, Region, SortCtor, SubsetTy, Ty, TyKind, INNERMOST, }, rustc::mir::{BasicBlock, Local, LocalDecls, Place, PlaceElem}, }; @@ -542,7 +542,7 @@ impl BasicBlockEnvShape { sty1.pred.clone() }; let sort = bty.sort(); - let ctor = Binder::with_sort(SimpleTy::new(bty, Expr::nu(), pred), sort); + let ctor = Binder::with_sort(SubsetTy::new(bty, Expr::nu(), pred), sort); GenericArg::Base(ctor) } (GenericArg::Lifetime(re1), GenericArg::Lifetime(re2)) => { From 5162b876d5e345e198a8efa5d6975170c16d7edf Mon Sep 17 00:00:00 2001 From: Nico Lehmann Date: Sat, 17 Feb 2024 19:33:32 -0800 Subject: [PATCH 17/22] Infer subst for base ty param tys --- crates/flux-middle/src/rty/mod.rs | 4 +- crates/flux-middle/src/rty/projections.rs | 151 ++-------------------- crates/flux-middle/src/rty/refining.rs | 2 +- crates/flux-middle/src/rty/subst.rs | 2 +- crates/flux-refineck/src/checker.rs | 2 +- 5 files changed, 19 insertions(+), 142 deletions(-) diff --git a/crates/flux-middle/src/rty/mod.rs b/crates/flux-middle/src/rty/mod.rs index 22110acaa8..bfc9513835 100644 --- a/crates/flux-middle/src/rty/mod.rs +++ b/crates/flux-middle/src/rty/mod.rs @@ -893,7 +893,7 @@ impl SubsetTy { Self { bty, idx: idx.into(), pred: pred.into() } } - pub fn indexed(bty: BaseTy, idx: impl Into) -> Self { + pub fn trivial(bty: BaseTy, idx: impl Into) -> Self { Self::new(bty, idx, Expr::tt()) } @@ -2086,7 +2086,7 @@ mod pretty { default fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result { define_scoped!(cx, f); cx.with_bound_vars(&self.vars, || { - cx.fmt_bound_vars("for<", &self.vars, ">", f)?; + cx.fmt_bound_vars("for<", &self.vars, "> ", f)?; w!("{:?}", &self.value) }) } diff --git a/crates/flux-middle/src/rty/projections.rs b/crates/flux-middle/src/rty/projections.rs index 5f3abfe451..df61e60a14 100644 --- a/crates/flux-middle/src/rty/projections.rs +++ b/crates/flux-middle/src/rty/projections.rs @@ -6,15 +6,14 @@ use rustc_hir::def_id::DefId; use rustc_infer::{infer::InferCtxt, traits::Obligation}; use rustc_middle::{ traits::{ImplSource, ObligationCause}, - ty::{EarlyBoundRegion, ParamTy, TyCtxt}, + ty::TyCtxt, }; use rustc_trait_selection::traits::SelectionContext; use super::{ - canonicalize::{CanonicalConstrTy, CanonicalTy}, fold::{FallibleTypeFolder, TypeSuperFoldable}, - AliasKind, AliasReft, AliasTy, BaseTy, Clause, ClauseKind, Expr, ExprKind, GenericArg, - GenericArgs, ProjectionPredicate, RefineArgs, Region, SubsetTy, Ty, TyKind, + AliasKind, AliasReft, AliasTy, BaseTy, Binder, Clause, ClauseKind, Expr, ExprKind, GenericArg, + ProjectionPredicate, RefineArgs, Region, SubsetTy, Ty, TyKind, }; use crate::{ global_env::GlobalEnv, @@ -56,7 +55,7 @@ impl<'genv, 'tcx, 'cx> Normalizer<'genv, 'tcx, 'cx> { .skip_binder(); let generics = self.tcx().generics_of(impl_def_id); - let mut subst = Equate::new(generics); + let mut subst = TVarSubst::new(generics); for (a, b) in iter::zip(&impl_trait_ref.args, &obligation.args) { subst.generic_args(a, b); } @@ -110,7 +109,7 @@ impl<'genv, 'tcx, 'cx> Normalizer<'genv, 'tcx, 'cx> { let generics = self.tcx().generics_of(impl_def_id); - let mut subst = Equate::new(generics); + let mut subst = TVarSubst::new(generics); for (a, b) in iter::zip(&impl_trait_ref.args, &obligation.args) { subst.generic_args(a, b); } @@ -259,139 +258,12 @@ pub enum Candidate { TraitDef(ProjectionPredicate), } -// #[derive(Debug)] -// struct TVarSubst { -// args: Vec>, -// } - -// impl TVarSubst { -// fn new(generics: &rustc_middle::ty::Generics) -> Self { -// Self { args: vec![None; generics.count()] } -// } - -// fn finish<'tcx>( -// self, -// tcx: TyCtxt<'tcx>, -// generics: &'tcx rustc_middle::ty::Generics, -// ) -> Vec { -// self.args -// .into_iter() -// .enumerate() -// .map(|(idx, arg)| { -// if let Some(arg) = arg { -// arg -// } else { -// let param = generics.param_at(idx, tcx); -// bug!("cannot infer substitution for param {param:?}"); -// } -// }) -// .collect() -// } - -// fn insert_param_ty(&mut self, pty: ParamTy, ty: &Ty) { -// let arg = GenericArg::Ty(ty.clone()); -// if self.args[pty.index as usize].replace(arg).is_some() { -// bug!("duplicate insert"); -// } -// } - -// fn insert_early_bound_region(&mut self, ebr: EarlyBoundRegion, re: Region) { -// let arg = GenericArg::Lifetime(re); -// if self.args[ebr.index as usize].replace(arg).is_some() { -// bug!("duplicate insert"); -// } -// } - -// fn infer_from_args(&mut self, src: rustc_middle::ty::GenericArgsRef, dst: &GenericArgs) { -// debug_assert_eq!(src.len(), dst.len()); -// for (src, dst) in iter::zip(src, dst) { -// self.infer_from_arg(src, dst); -// } -// } - -// fn infer_from_arg(&mut self, src: rustc_middle::ty::GenericArg, dst: &GenericArg) { -// match dst { -// GenericArg::Ty(dst) => { -// self.infer_from_ty(&src.as_type().unwrap(), dst); -// } -// GenericArg::Lifetime(dst) => self.infer_from_region(&src.as_region().unwrap(), dst), -// GenericArg::Base(ty) => { -// // todo!() -// // self.infer_from_ty(&src.as_type().unwrap(), ty.bty_skipping_binder()); -// } -// _ => (), -// } -// } - -// fn infer_from_ty(&mut self, src: &rustc_middle::ty::Ty, dst: &Ty) { -// use rustc_middle::ty; -// match src.kind() { -// ty::TyKind::Param(pty) => { -// if !dst.has_escaping_bvars() { -// self.insert_param_ty(*pty, dst); -// } -// } -// ty::TyKind::Adt(_, src_subst) => { -// // NOTE: see https://github.com/flux-rs/flux/pull/478#issuecomment-1650983695 -// if let Some(dst) = dst.as_bty_skipping_existentials() -// && let BaseTy::Adt(_, dst_subst) = dst -// { -// debug_assert_eq!(src_subst.len(), dst_subst.len()); -// for (src_arg, dst_arg) in iter::zip(*src_subst, dst_subst) { -// self.infer_from_arg(src_arg, dst_arg); -// } -// } else { -// bug!("unexpected type {dst:?}"); -// } -// } -// ty::TyKind::Array(src, _) => { -// if let Some(BaseTy::Array(dst, _)) = dst.as_bty_skipping_existentials() { -// self.infer_from_ty(src, dst); -// } else { -// bug!("unexpected type {dst:?}"); -// } -// } -// ty::TyKind::Slice(src) => { -// if let Some(BaseTy::Slice(dst)) = dst.as_bty_skipping_existentials() { -// self.infer_from_ty(src, dst); -// } else { -// bug!("unexpected type {dst:?}"); -// } -// } -// ty::TyKind::Tuple(src_tys) => { -// if let Some(BaseTy::Tuple(dst_tys)) = dst.as_bty_skipping_existentials() { -// debug_assert_eq!(src_tys.len(), dst_tys.len()); -// iter::zip(src_tys.iter(), dst_tys.iter()) -// .for_each(|(src, dst)| self.infer_from_ty(&src, dst)); -// } else { -// bug!("unexpected type {dst:?}"); -// } -// } -// ty::TyKind::Ref(src_re, src_ty, _) => { -// if let Some(BaseTy::Ref(dst_re, dst_ty, _)) = dst.as_bty_skipping_existentials() { -// self.infer_from_region(src_re, dst_re); -// self.infer_from_ty(src_ty, dst_ty); -// } else { -// bug!("unexpected type {dst:?}"); -// } -// } -// _ => {} -// } -// } - -// fn infer_from_region(&mut self, src: &rustc_middle::ty::Region, dst: &Region) { -// if let rustc_middle::ty::RegionKind::ReEarlyBound(ebr) = src.kind() { -// self.insert_early_bound_region(ebr, *dst); -// } -// } -// } - #[derive(Debug)] -struct Equate { +struct TVarSubst { args: Vec>, } -impl Equate { +impl TVarSubst { fn new(generics: &rustc_middle::ty::Generics) -> Self { Self { args: vec![None; generics.count()] } } @@ -420,7 +292,6 @@ impl Equate { (GenericArg::Ty(a), GenericArg::Ty(b)) => self.tys(a, b), (GenericArg::Lifetime(a), GenericArg::Lifetime(b)) => self.regions(*a, *b), (GenericArg::Base(a), GenericArg::Base(b)) => { - debug_assert_eq!(a.sort(), b.sort()); self.btys(a.as_bty_skipping_binder(), b.as_bty_skipping_binder()); } _ => {} @@ -441,7 +312,13 @@ impl Equate { fn btys(&mut self, a: &BaseTy, b: &BaseTy) { match (a, b) { - (BaseTy::Param(_), _) => todo!(), + (BaseTy::Param(param_ty), _) => { + if !b.has_escaping_bvars() { + let sort = b.sort(); + let ctor = Binder::with_sort(SubsetTy::trivial(b.clone(), Expr::nu()), sort); + self.insert_generic_arg(param_ty.index, GenericArg::Base(ctor)); + } + } (BaseTy::Adt(_, a_args), BaseTy::Adt(_, b_args)) => { debug_assert_eq!(a_args.len(), b_args.len()); for (a_arg, b_arg) in iter::zip(a_args, b_args) { diff --git a/crates/flux-middle/src/rty/refining.rs b/crates/flux-middle/src/rty/refining.rs index a287910674..1655b5f9af 100644 --- a/crates/flux-middle/src/rty/refining.rs +++ b/crates/flux-middle/src/rty/refining.rs @@ -418,7 +418,7 @@ impl TyOrBase { fn refine_default(bty: rty::BaseTy) -> rty::Binder { let sort = bty.sort(); - let constr = rty::SubsetTy::indexed(bty.shift_in_escaping(1), rty::Expr::nu()); + let constr = rty::SubsetTy::trivial(bty.shift_in_escaping(1), rty::Expr::nu()); rty::Binder::with_sort(constr, sort) } diff --git a/crates/flux-middle/src/rty/subst.rs b/crates/flux-middle/src/rty/subst.rs index 86fa52dc09..45781a9d12 100644 --- a/crates/flux-middle/src/rty/subst.rs +++ b/crates/flux-middle/src/rty/subst.rs @@ -275,7 +275,7 @@ impl GenericsSubstDelegate for IdentitySubstDelegate { fn ctor_for_param(&mut self, param_ty: ParamTy) -> SubsetTyCtor { Binder::with_sort( - SubsetTy::indexed(BaseTy::Param(param_ty), Expr::nu()), + SubsetTy::trivial(BaseTy::Param(param_ty), Expr::nu()), Sort::Param(param_ty), ) } diff --git a/crates/flux-refineck/src/checker.rs b/crates/flux-refineck/src/checker.rs index aedbda588a..2e68f23102 100644 --- a/crates/flux-refineck/src/checker.rs +++ b/crates/flux-refineck/src/checker.rs @@ -1151,7 +1151,7 @@ fn instantiate_args_for_fun_call( let constr = if !sort.is_unit() { rty::SubsetTy::new(bty, Expr::nu(), Expr::hole(rty::HoleKind::Pred)) } else { - rty::SubsetTy::indexed(bty, Expr::nu()) + rty::SubsetTy::trivial(bty, Expr::nu()) }; Binder::with_sort(constr, sort) }); From e3bba79b96aa92cf9bd61753b2d56fcdf3f9cbe1 Mon Sep 17 00:00:00 2001 From: Nico Lehmann Date: Sat, 17 Feb 2024 19:49:02 -0800 Subject: [PATCH 18/22] print --- crates/flux-middle/src/rty/mod.rs | 17 ++++++++++++----- 1 file changed, 12 insertions(+), 5 deletions(-) diff --git a/crates/flux-middle/src/rty/mod.rs b/crates/flux-middle/src/rty/mod.rs index bfc9513835..6e12bf9f93 100644 --- a/crates/flux-middle/src/rty/mod.rs +++ b/crates/flux-middle/src/rty/mod.rs @@ -2223,15 +2223,22 @@ mod pretty { if !vars.is_empty() { cx.fmt_bound_vars("exists<", vars, "> ", f)?; } - w!("{:?}", &self.value.ret)?; - if !self.value.ensures.is_empty() { - w!("; [{:?}]", join!(", ", &self.value.ensures))?; - } - Ok(()) + w!("{:?}", &self.value) }) } } + impl Pretty for FnOutput { + fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result { + define_scoped!(cx, f); + w!("{:?}", &self.ret)?; + if !self.ensures.is_empty() { + w!("; [{:?}]", join!(", ", &self.ensures))?; + } + Ok(()) + } + } + impl Pretty for Constraint { fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result { define_scoped!(cx, f); From 1235232ef669db0e722faeaacff88541de7a9835 Mon Sep 17 00:00:00 2001 From: Nico Lehmann Date: Sat, 17 Feb 2024 21:57:29 -0800 Subject: [PATCH 19/22] Documentation --- crates/flux-fhir-analysis/src/wf/mod.rs | 2 +- crates/flux-fhir-analysis/src/wf/sortck.rs | 6 +-- crates/flux-middle/src/fhir.rs | 5 +-- crates/flux-middle/src/rty/canonicalize.rs | 42 +++++++++++++++++-- crates/flux-middle/src/rty/mod.rs | 40 ++++++++++++++++++ crates/flux-refineck/src/fixpoint_encoding.rs | 2 +- crates/flux-refineck/src/refine_tree.rs | 11 ++--- crates/flux-refineck/src/type_env.rs | 4 +- crates/flux-refineck/src/type_env/place_ty.rs | 4 +- 9 files changed, 95 insertions(+), 21 deletions(-) diff --git a/crates/flux-fhir-analysis/src/wf/mod.rs b/crates/flux-fhir-analysis/src/wf/mod.rs index d2b87d42ec..b2bad18b56 100644 --- a/crates/flux-fhir-analysis/src/wf/mod.rs +++ b/crates/flux-fhir-analysis/src/wf/mod.rs @@ -37,7 +37,7 @@ struct Wf<'genv, 'tcx> { /// determined. The context is called Xi because in the paper [Focusing on Liquid Refinement Typing], /// the well-formedness judgment uses an uppercase Xi (Ξ) for a context that is similar in purpose. /// -/// This is basically a set of [`fhir::Name`] implemented with a snapshot map such that elements +/// This is basically a set of [`fhir::ParamId`] implemented with a snapshot map such that elements /// can be removed in batch when there's a change in polarity. /// /// [Focusing on Liquid Refinement Typing]: https://arxiv.org/pdf/2209.13000.pdf diff --git a/crates/flux-fhir-analysis/src/wf/sortck.rs b/crates/flux-fhir-analysis/src/wf/sortck.rs index ccc76e40d1..10ce73215a 100644 --- a/crates/flux-fhir-analysis/src/wf/sortck.rs +++ b/crates/flux-fhir-analysis/src/wf/sortck.rs @@ -352,9 +352,9 @@ impl<'genv> InferCtxt<'genv, '_> { } /// Whether a value of `sort1` can be automatically coerced to a value of `sort2`. A value of an - /// [`rty::Sort::Adt`] sort with a single field of sort `s` can be coerced to a value of sort `s` - /// and vice versa, i.e., we can automatically project the field out of the record or inject a - /// value into a record. + /// [`rty::SortCtor::Adt`] sort with a single field of sort `s` can be coerced to a value of sort + /// `s` and vice versa, i.e., we can automatically project the field out of the record or inject + /// a value into a record. fn is_coercible(&mut self, sort1: &rty::Sort, sort2: &rty::Sort, fhir_id: FhirId) -> bool { if self.try_equate(sort1, sort2).is_some() { return true; diff --git a/crates/flux-middle/src/fhir.rs b/crates/flux-middle/src/fhir.rs index b2adb3b8e4..26b2bdfae3 100644 --- a/crates/flux-middle/src/fhir.rs +++ b/crates/flux-middle/src/fhir.rs @@ -474,12 +474,11 @@ pub enum TyKind<'fhir> { /// A type that parses as a [`BaseTy`] but was written without refinements. Most types in /// this category are base types and will be converted into an [existential], e.g., `i32` is /// converted into `∃v:int. i32[v]`. However, this category also contains generic variables - /// of kind [type] or [*special*]. We cannot distinguish these syntactially so we resolve them - /// later in the analysis. + /// of kind [type]. We cannot distinguish these syntactially so we resolve them later in the + /// analysis. /// /// [existential]: crate::rty::TyKind::Exists /// [type]: GenericParamKind::Type - /// [*special*]: GenericParamKind::SplTy BaseTy(BaseTy<'fhir>), Indexed(BaseTy<'fhir>, RefineArg<'fhir>), Exists(&'fhir [RefineParam<'fhir>], &'fhir Ty<'fhir>), diff --git a/crates/flux-middle/src/rty/canonicalize.rs b/crates/flux-middle/src/rty/canonicalize.rs index 8c4c42a721..92b7c79f42 100644 --- a/crates/flux-middle/src/rty/canonicalize.rs +++ b/crates/flux-middle/src/rty/canonicalize.rs @@ -1,3 +1,23 @@ +//! A canonical type is a type where all [existentials] and [constraint predicates] are *hoisted* to +//! the top level. For example, the canonical version of `(∃a. i32[a], ∃b. { i32[b] | b > 0})` is +//! `∃a,b. { (i32[a], i32[b]) | b > 0}`. +//! +//! Canonicalization can be *shallow* or *deep*, by this we mean that some type constructors +//! introduce new "scopes" that limit the hoisting. For instance, we are not allowed (in general) to +//! hoist an existential type out of a generic argument, for example, in `Vec<∃v. i32[v]>` the +//! existential inside the `Vec` cannot be hoisted out. However, the type inside the generic argument +//! can be canonizalized locally inside the scope of the generic argument. Shallow canonicalization +//! stops when finding type constructors. In contrast, deep canonicalization also canonizalizes inside +//! type constructors. Note that some type constructors like shared references or boxes are transparent +//! to hoisting and do not introduce a new scope. +//! +//! It's also important to note that canonizalization doesn't imply any form of semantic equality +//! and it is just a best effort to facilitate syntactic manipulation. For example, the types +//! `∃a,b. (i32[a], i32[b])` and `∃a,b. (i32[b], i32[a])` are semantically equal but both are in +//! canonical form (in the current implementation). +//! +//! [existentials]: TyKind::Exists +//! [constraint predicates]: TyKind::Constr use rustc_type_ir::{Mutability, INNERMOST}; use super::{ @@ -8,12 +28,12 @@ use super::{ use crate::intern::List; #[derive(Default)] -pub struct Hoister { +pub struct ShallowHoister { vars: Vec, preds: Vec, } -impl Hoister { +impl ShallowHoister { pub fn into_parts(self) -> (List, Vec) { (List::from_vec(self.vars), self.preds) } @@ -23,7 +43,7 @@ impl Hoister { } } -impl TypeFolder for Hoister { +impl TypeFolder for ShallowHoister { fn fold_ty(&mut self, ty: &Ty) -> Ty { match ty.kind() { TyKind::Indexed(bty, idx) => Ty::indexed(bty.fold_with(self), idx.clone()), @@ -65,7 +85,7 @@ impl TypeFolder for Hoister { impl Ty { pub fn shallow_canonicalize(&self) -> CanonicalTy { - let mut hoister = Hoister::default(); + let mut hoister = ShallowHoister::default(); let ty = hoister.hoist(self); let (vars, preds) = hoister.into_parts(); let pred = Expr::and(preds); @@ -77,7 +97,12 @@ impl Ty { } } } + pub struct CanonicalConstrTy { + /// Guranteed to not have any (shallow) [existential] or [constraint] types + /// + /// [existential]: TyKind::Exists + /// [constraint]: TyKind::Constr ty: Ty, pred: Expr, } @@ -92,8 +117,17 @@ impl CanonicalConstrTy { } } +/// A (shallowly) canonicalized type. This can be either of the form `{T | p}` or `∃v0,…,vn. {T | p}`, +/// where `T` doesnt have any (shallow) [existential] or [constraint] types. +/// +/// When canonizalizing a type without a [constraint] type, `p` will be [`Expr::tt()`]. +/// +/// [existential]: TyKind::Exists +/// [constraint]: TyKind::Constr pub enum CanonicalTy { + /// A type of the form `{T | p}` Constr(CanonicalConstrTy), + /// A type of the form `∃v0,…,vn. {T | p}` Exists(Binder), } diff --git a/crates/flux-middle/src/rty/mod.rs b/crates/flux-middle/src/rty/mod.rs index 6e12bf9f93..9100be40fd 100644 --- a/crates/flux-middle/src/rty/mod.rs +++ b/crates/flux-middle/src/rty/mod.rs @@ -862,6 +862,8 @@ pub type RefineArgs = List; pub type OpaqueArgsMap = FxHashMap; +/// A type constructor meant to be used as generic arguments of type base. This is just an +/// alias to [`Binder`] pub type SubsetTyCtor = Binder; impl SubsetTyCtor { @@ -881,9 +883,47 @@ impl SubsetTyCtor { } } +/// A subset type is a simplified version of a type that has the form `{b[e] | p}` where `b` is a +/// [`BaseTy`], `e` a refinement index and `p` a predicate. These are mainly found under a [`Binder`] +/// with a single variable of the base type's sort. This can be interpreted as a type constructor or +/// an existial type. For example, under a binder with a variable `v` of sort `int`, we can interpret +/// `{i32[v] | v > 0}` as a lambda `λv:int. {i32[v] | v > 0}` that "constructs" types when applied to +/// ints or as an existential type `∃v:int. {i32[v] | v > 0}`. This second interpretation is the +/// reason we call this a subset type, i.e., the type `∃v. {b[v] | p}` corresponds to the subset of +/// values of (base) type `b` whose index satisfies `p`. In other words, these are the types supported +/// by liquid haskell, with the difference that we are explicit about separating refinements from +/// program values via an index. +/// +/// The main purpose for a [`SubsetTy`] is to be used as generic arguments of [kind base] when +/// interpreted as a type contructor. The key property of a [`SubsetTy`] is that it can be eagerly +/// +/// canonicalized via [*strengthening*] during substitution. For example, suppose we have a function +/// ```text +/// fn foo(x: T[@a], y: { T[@b] | b == a }) { } +/// ``` +/// If we instantiate `T` with `λv. { i32[v] | v > 0}`, after substituting an applying the lambda we +/// get: +/// ```text +/// fn foo(x: {i32[@a] | a > 0}, y: { { i32[@b] | b > 0 } | b == a }) { } +/// ``` +/// By the strengthening rule we can canonicalize this to +/// ```text +/// fn foo(x: {i32[@a] | a > 0}, y: { i32[@b] | b == a && b > 0 }) { } +/// ``` +/// As a result, we can guarantee a simple canonical form that makes it easier to manipulate types +/// syntactically. +/// +/// [kind base]: GenericParamDefKind::Base +/// [*strengthening*]: https://arxiv.org/pdf/2010.07763.pdf #[derive(PartialEq, Clone, Eq, Hash, TyEncodable, TyDecodable)] pub struct SubsetTy { + /// *NOTE*: This [`BaseTy`] is mainly going to be under a [`Binder`]. It is not yet clear whether + /// this [`BaseTy`] should be able to mention variables in the binder. In general, in a type + /// `∃v. {b[e] | p}` is fine to mention `v` inside `b`, but since [`SubsetTy`] is meant to + /// facilitate syntatic manipulation we may restrict this. pub bty: BaseTy, + /// This can be an arbitrary expression which makes the syntatic manipulation easier, but since + /// this is mostly going to be under a binder we expect it to be [`Expr::nu()`]. pub idx: Expr, pub pred: Expr, } diff --git a/crates/flux-refineck/src/fixpoint_encoding.rs b/crates/flux-refineck/src/fixpoint_encoding.rs index 8d4430af1a..1ec8e75a58 100644 --- a/crates/flux-refineck/src/fixpoint_encoding.rs +++ b/crates/flux-refineck/src/fixpoint_encoding.rs @@ -1093,7 +1093,7 @@ impl<'genv, 'tcx> ExprEncodingCtxt<'genv, 'tcx> { /// This function returns a very polymorphic sort for the UIF encoding the alias_pred; /// This is ok, as well-formedness in previous phases will ensure the function is always /// instantiated with the same sorts. However, the proper thing is to compute the *actual* -/// mono-sort at which this alias_pred is being used see [`GlobalEnv::sort_of_alias_pred`] but +/// mono-sort at which this alias_pred is being used see [`GlobalEnv::sort_of_alias_reft`] but /// that is a bit tedious as its done using the `fhir` (not `rty`). Alternatively, we might /// stash the computed mono-sort *in* the `rty::AliasPred` during `conv`? fn alias_reft_sort(arity: usize) -> rty::PolyFuncSort { diff --git a/crates/flux-refineck/src/refine_tree.rs b/crates/flux-refineck/src/refine_tree.rs index 44e583ca08..f5a5516c5f 100644 --- a/crates/flux-refineck/src/refine_tree.rs +++ b/crates/flux-refineck/src/refine_tree.rs @@ -193,16 +193,17 @@ impl<'rcx> RefineCtxt<'rcx> { fresh } - /// Given a [`sort`] that may contain aggregate sorts ([tuples] or [records]), it destructs the sort - /// recursively, generating multiple fresh variables and returning the "eta-expanded" tuple of fresh - /// variables. This is in contrast to generating a single fresh variable of tuple sort. + /// Given a [`sort`] that may contain aggregate sorts ([tuple] or [adt]), it destructs the sort + /// recursively, generating multiple fresh variables and returning an "eta-expanded" expression + /// of fresh variables. This is in contrast to generating a single fresh variable of aggregate + /// sort. /// /// For example, given the sort `(int, (bool, int))` it returns `(a0, (a1, a2))` for fresh variables /// `a0: int`, `a1: bool`, and `a2: int`. /// /// [`sort`]: Sort - /// [tuples]: Sort::Tuple - /// [records]: Sort::Adt + /// [tuple]: Sort::Tuple + /// [adt]: flux_middle::rty::SortCtor::Adt pub(crate) fn define_vars(&mut self, sort: &Sort) -> Expr { Expr::fold_sort(sort, |sort| Expr::fvar(self.define_var(sort))) } diff --git a/crates/flux-refineck/src/type_env.rs b/crates/flux-refineck/src/type_env.rs index 241034b8e7..db3eb41c46 100644 --- a/crates/flux-refineck/src/type_env.rs +++ b/crates/flux-refineck/src/type_env.rs @@ -7,7 +7,7 @@ use flux_middle::{ global_env::GlobalEnv, intern::List, rty::{ - canonicalize::Hoister, + canonicalize::ShallowHoister, evars::EVarSol, fold::{FallibleTypeFolder, TypeFoldable, TypeVisitable, TypeVisitor}, subst::RegionSubst, @@ -556,7 +556,7 @@ impl BasicBlockEnvShape { pub fn into_bb_env(self, kvar_store: &mut KVarStore) -> BasicBlockEnv { let mut bindings = self.bindings; - let mut hoister = Hoister::default(); + let mut hoister = ShallowHoister::default(); bindings.fmap_mut(|ty| hoister.hoist(ty)); let (vars, preds) = hoister.into_parts(); diff --git a/crates/flux-refineck/src/type_env/place_ty.rs b/crates/flux-refineck/src/type_env/place_ty.rs index b1319da208..51f3870f0d 100644 --- a/crates/flux-refineck/src/type_env/place_ty.rs +++ b/crates/flux-refineck/src/type_env/place_ty.rs @@ -847,7 +847,7 @@ fn fold( .map(|ty| fold(bindings, rcx, gen, ty, is_strg)) .try_collect_vec()?; - let partially_moved = fields.iter().any(|ty| ty.is_uninit()); + let partially_moved = fields.iter().any(Ty::is_uninit); let ty = if partially_moved { Ty::uninit() } else { @@ -868,7 +868,7 @@ fn fold( .map(|ty| fold(bindings, rcx, gen, ty, is_strg)) .try_collect_vec()?; - let partially_moved = fields.iter().any(|ty| ty.is_uninit()); + let partially_moved = fields.iter().any(Ty::is_uninit); let ty = if partially_moved { Ty::uninit() } else { Ty::tuple(fields) }; Ok(ty) } From 9392ab182b6242fa2608fb9cec3ca1581c4a251f Mon Sep 17 00:00:00 2001 From: Nico Lehmann Date: Sat, 17 Feb 2024 22:18:57 -0800 Subject: [PATCH 20/22] Tweak documentation --- crates/flux-middle/src/rty/expr.rs | 2 +- crates/flux-middle/src/rty/mod.rs | 14 ++++++++------ 2 files changed, 9 insertions(+), 7 deletions(-) diff --git a/crates/flux-middle/src/rty/expr.rs b/crates/flux-middle/src/rty/expr.rs index ee0f579a28..65dcec5ec9 100644 --- a/crates/flux-middle/src/rty/expr.rs +++ b/crates/flux-middle/src/rty/expr.rs @@ -576,7 +576,7 @@ impl Expr { } /// Simple syntactic check to see if the expression is a trivially true predicate. This is used - /// mostly for filtering predicates when pretty printing but also to simplify the types. + /// mostly for filtering predicates when pretty printing but also to simplify types in general. pub fn is_trivially_true(&self) -> bool { self.is_true() || matches!(self.kind(), ExprKind::BinaryOp(BinOp::Eq | BinOp::Iff | BinOp::Imp, e1, e2) if e1 == e2) diff --git a/crates/flux-middle/src/rty/mod.rs b/crates/flux-middle/src/rty/mod.rs index 9100be40fd..2cb1ba0aea 100644 --- a/crates/flux-middle/src/rty/mod.rs +++ b/crates/flux-middle/src/rty/mod.rs @@ -862,8 +862,11 @@ pub type RefineArgs = List; pub type OpaqueArgsMap = FxHashMap; -/// A type constructor meant to be used as generic arguments of type base. This is just an -/// alias to [`Binder`] +/// A type constructor meant to be used as generic arguments of [kind base]. This is just an alias to +/// [`Binder`], but we expect the binder to only have a single bound variable of the sort +/// of the underlying [`BaseTy`]. +/// +/// [kind base]: GenericParamDefKind::Base pub type SubsetTyCtor = Binder; impl SubsetTyCtor { @@ -896,13 +899,12 @@ impl SubsetTyCtor { /// /// The main purpose for a [`SubsetTy`] is to be used as generic arguments of [kind base] when /// interpreted as a type contructor. The key property of a [`SubsetTy`] is that it can be eagerly -/// -/// canonicalized via [*strengthening*] during substitution. For example, suppose we have a function +/// canonicalized via [*strengthening*] during substitution. For example, suppose we have a function: /// ```text /// fn foo(x: T[@a], y: { T[@b] | b == a }) { } /// ``` -/// If we instantiate `T` with `λv. { i32[v] | v > 0}`, after substituting an applying the lambda we -/// get: +/// If we instantiate `T` with `λv. { i32[v] | v > 0}`, after substitution and applying the lambda, +/// we get: /// ```text /// fn foo(x: {i32[@a] | a > 0}, y: { { i32[@b] | b > 0 } | b == a }) { } /// ``` From e67beb55e17440fb0f018aa8bb227c84985df912 Mon Sep 17 00:00:00 2001 From: Nico Lehmann Date: Sat, 17 Feb 2024 22:20:54 -0800 Subject: [PATCH 21/22] run mdbook on every pr --- .github/workflows/ci.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 5b906ddd47..801e137684 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -31,7 +31,7 @@ jobs: with: enable-stack: true stack-version: "latest" - + - name: Install Z3 uses: cda-tum/setup-z3@v1.0.9 with: From a875194f1ae60cdac9d8f6b67477d49c3800a315 Mon Sep 17 00:00:00 2001 From: Nico Lehmann Date: Sat, 17 Feb 2024 22:29:30 -0800 Subject: [PATCH 22/22] more docs --- .github/workflows/gh-pages.yml | 2 -- crates/flux-middle/src/rty/mod.rs | 18 +++++++++--------- 2 files changed, 9 insertions(+), 11 deletions(-) diff --git a/.github/workflows/gh-pages.yml b/.github/workflows/gh-pages.yml index 066e12d536..b543518d4a 100644 --- a/.github/workflows/gh-pages.yml +++ b/.github/workflows/gh-pages.yml @@ -3,10 +3,8 @@ name: gh-pages on: push: branches: [main] - paths: book/** pull_request: branches: [main] - paths: book/** jobs: build: diff --git a/crates/flux-middle/src/rty/mod.rs b/crates/flux-middle/src/rty/mod.rs index 2cb1ba0aea..688755cd62 100644 --- a/crates/flux-middle/src/rty/mod.rs +++ b/crates/flux-middle/src/rty/mod.rs @@ -862,9 +862,9 @@ pub type RefineArgs = List; pub type OpaqueArgsMap = FxHashMap; -/// A type constructor meant to be used as generic arguments of [kind base]. This is just an alias to -/// [`Binder`], but we expect the binder to only have a single bound variable of the sort -/// of the underlying [`BaseTy`]. +/// A type constructor meant to be used as generic a argument of [kind base]. This is just an alias +/// to [`Binder`], but we expect the binder to have a single bound variable of the sort of +/// the underlying [`BaseTy`]. /// /// [kind base]: GenericParamDefKind::Base pub type SubsetTyCtor = Binder; @@ -887,15 +887,15 @@ impl SubsetTyCtor { } /// A subset type is a simplified version of a type that has the form `{b[e] | p}` where `b` is a -/// [`BaseTy`], `e` a refinement index and `p` a predicate. These are mainly found under a [`Binder`] +/// [`BaseTy`], `e` a refinement index, and `p` a predicate. These are mainly found under a [`Binder`] /// with a single variable of the base type's sort. This can be interpreted as a type constructor or /// an existial type. For example, under a binder with a variable `v` of sort `int`, we can interpret /// `{i32[v] | v > 0}` as a lambda `λv:int. {i32[v] | v > 0}` that "constructs" types when applied to -/// ints or as an existential type `∃v:int. {i32[v] | v > 0}`. This second interpretation is the +/// ints, or as an existential type `∃v:int. {i32[v] | v > 0}`. This second interpretation is the /// reason we call this a subset type, i.e., the type `∃v. {b[v] | p}` corresponds to the subset of /// values of (base) type `b` whose index satisfies `p`. In other words, these are the types supported -/// by liquid haskell, with the difference that we are explicit about separating refinements from -/// program values via an index. +/// by liquid haskell (with the difference that we are explicit about separating refinements from +/// program values via an index). /// /// The main purpose for a [`SubsetTy`] is to be used as generic arguments of [kind base] when /// interpreted as a type contructor. The key property of a [`SubsetTy`] is that it can be eagerly @@ -919,9 +919,9 @@ impl SubsetTyCtor { /// [*strengthening*]: https://arxiv.org/pdf/2010.07763.pdf #[derive(PartialEq, Clone, Eq, Hash, TyEncodable, TyDecodable)] pub struct SubsetTy { - /// *NOTE*: This [`BaseTy`] is mainly going to be under a [`Binder`]. It is not yet clear whether + /// **NOTE:** This [`BaseTy`] is mainly going to be under a [`Binder`]. It is not yet clear whether /// this [`BaseTy`] should be able to mention variables in the binder. In general, in a type - /// `∃v. {b[e] | p}` is fine to mention `v` inside `b`, but since [`SubsetTy`] is meant to + /// `∃v. {b[e] | p}`, it's fine to mention `v` inside `b`, but since [`SubsetTy`] is meant to /// facilitate syntatic manipulation we may restrict this. pub bty: BaseTy, /// This can be an arbitrary expression which makes the syntatic manipulation easier, but since