Skip to content

Commit

Permalink
Refactor treatment of generic args of kind base (#622)
Browse files Browse the repository at this point in the history
  • Loading branch information
@nilehmann
nilehmann authored Feb 18, 2024
1 parent 8eac741 commit 15fe149
Show file tree
Hide file tree
Showing 38 changed files with 913 additions and 638 deletions.
2 changes: 1 addition & 1 deletion .github/workflows/ci.yml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,7 @@ jobs:
with:
enable-stack: true
stack-version: "latest"

- name: Install Z3
uses: cda-tum/[email protected]
with:
Expand Down
2 changes: 0 additions & 2 deletions .github/workflows/gh-pages.yml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,10 +3,8 @@ name: gh-pages
on:
push:
branches: [main]
paths: book/**
pull_request:
branches: [main]
paths: book/**

jobs:
build:
Expand Down
6 changes: 2 additions & 4 deletions crates/flux-desugar/src/desugar.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand All @@ -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 });
Expand Down
6 changes: 3 additions & 3 deletions crates/flux-fhir-analysis/locales/en-US.ftl
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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 =
Expand Down
201 changes: 106 additions & 95 deletions crates/flux-fhir-analysis/src/conv.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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,
}
}
Expand Down Expand Up @@ -426,7 +425,7 @@ impl<'a, 'genv, 'tcx> ConvCtxt<'a, 'genv, 'tcx> {
clauses: &mut Vec<rty::Clause>,
) -> 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 };
Expand All @@ -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!")
}
}
}

Expand Down Expand Up @@ -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);
Expand Down Expand Up @@ -738,50 +745,54 @@ impl<'a, 'genv, 'tcx> ConvCtxt<'a, 'genv, 'tcx> {
}

fn conv_base_ty(&self, env: &mut Env, bty: &fhir::BaseTy) -> QueryResult<rty::Ty> {
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 {
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)?;
let args = List::from_vec(args);

let refine_args = List::empty();
let alias_ty = rty::AliasTy { args, refine_args, def_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 {
Expand Down Expand Up @@ -850,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<rty::Ty> {
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<rty::Ty> {
fn conv_ty_ctor(&self, env: &mut Env, path: &fhir::Path) -> QueryResult<rty::TyCtor> {
let bty = match &path.res {
fhir::Res::PrimTy(PrimTy::Bool) => rty::BaseTy::Bool,
fhir::Res::PrimTy(PrimTy::Str) => rty::BaseTy::Str,
Expand All @@ -896,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)?;
Expand All @@ -909,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(
Expand All @@ -929,25 +912,43 @@ impl<'a, 'genv, 'tcx> ConvCtxt<'a, 'genv, 'tcx> {
args: &[fhir::GenericArg],
) -> QueryResult<Vec<rty::GenericArg>> {
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)
}

fn conv_generic_args_into(
&self,
env: &mut Env,
def_id: DefId,
args: &[fhir::GenericArg],
into: &mut Vec<rty::GenericArg>,
) -> 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, &param.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 { .. }) => {
into.push(rty::GenericArg::Ty(self.conv_ty(env, ty)?));
}
(fhir::GenericArg::Type(ty), rty::GenericParamDefKind::Base) => {
let ctor = self
.conv_ty(env, ty)?
.shallow_canonicalize()
.to_subset_ty_ctor()
.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);
}
}
}
Ok(())
Expand All @@ -957,7 +958,7 @@ impl<'a, 'genv, 'tcx> ConvCtxt<'a, 'genv, 'tcx> {
&self,
def_id: DefId,
into: &mut Vec<rty::GenericArg>,
) -> 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 {
Expand All @@ -966,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:?}");
Expand Down Expand Up @@ -1203,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<fhir::ParamId>, level: u32) -> Option<LookupResultKind> {
Some(LookupResultKind::LateBound {
level,
Expand Down Expand Up @@ -1478,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)]
Expand All @@ -1495,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 }
}
}
}
4 changes: 2 additions & 2 deletions crates/flux-fhir-analysis/src/lib.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -291,7 +291,7 @@ fn refinement_generics_of(
}
}

fn type_of(genv: GlobalEnv, def_id: LocalDefId) -> QueryResult<rty::EarlyBinder<rty::PolyTy>> {
fn type_of(genv: GlobalEnv, def_id: LocalDefId) -> QueryResult<rty::EarlyBinder<rty::TyCtor>> {
let ty = match genv.def_kind(def_id) {
DefKind::TyAlias { .. } => {
let alias = genv.map().expect_item(def_id).expect_type_alias();
Expand All @@ -310,7 +310,7 @@ fn type_of(genv: GlobalEnv, def_id: LocalDefId) -> QueryResult<rty::EarlyBinder<
DefKind::Impl { .. } | DefKind::Struct | DefKind::Enum | DefKind::AssocTy => {
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()))
Expand Down
Loading

0 comments on commit 15fe149

Please sign in to comment.