Skip to content

Commit

Permalink
phew, tests pass
Browse files Browse the repository at this point in the history
  • Loading branch information
Ranjit Jhala committed Oct 29, 2023
1 parent 4c718c6 commit 0b537d0
Show file tree
Hide file tree
Showing 26 changed files with 198 additions and 172 deletions.
5 changes: 4 additions & 1 deletion README.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -15,4 +15,7 @@ For an overview, take a look at the [`flux` website](https://flux-rs.github.io).
# Docs

Documentation, including installation and usage guides can be found on the
[website](https://flux-rs.github.io/flux).
[website](https://flux-rs.github.io/flux).


TRACE: insert_fn_sig DefId(0:14 ~ maps00[5caf]::rmap::{impl#0}::new) fn() -> {a0:RMap<sortof(K), sortof(V)>. RMap[K, V][a0] | true}
35 changes: 18 additions & 17 deletions crates/flux-desugar/src/desugar.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,10 +3,9 @@ use std::{borrow::Borrow, iter};
use flux_common::{bug, index::IndexGen, iter::IterExt, span_bug};
use flux_errors::FluxSession;
use flux_middle::{
fhir::{self, lift::LiftCtxt, ExprKind, FhirId, FluxOwnerId, Res},
fhir::{self, lift::LiftCtxt, ExprKind, FhirId, FluxOwnerId, GenericParamKind, Res},
global_env::GlobalEnv,
intern::List,
rty::GenericParamDefKind,
};
use flux_syntax::surface;
use hir::{def::DefKind, ItemKind, PrimTy};
Expand Down Expand Up @@ -234,6 +233,7 @@ impl<'a, 'tcx> DesugarCtxt<'a, 'tcx> {
let kind = match &param.kind {
surface::GenericParamKind::Type => fhir::GenericParamKind::Type { default: None },
surface::GenericParamKind::Base => fhir::GenericParamKind::BaseTy,
surface::GenericParamKind::Spl => fhir::GenericParamKind::SplTy,
surface::GenericParamKind::Refine { .. } => {
continue;
}
Expand Down Expand Up @@ -1633,7 +1633,7 @@ fn index_sort(
resolver_output: &ResolverOutput,
bty: &surface::BaseTy,
) -> Option<fhir::Sort> {
// CODESYNC(sort-of, 4) sorts should be given consistently
// CODESYNC(sort-of, 3) sorts should be given consistently
match &bty.kind {
surface::BaseTyKind::Path(path) => sort_of_surface_path(genv, resolver_output, path),
surface::BaseTyKind::Slice(_) => Some(fhir::Sort::Int),
Expand All @@ -1645,8 +1645,7 @@ fn sort_of_surface_path(
resolver_output: &ResolverOutput,
path: &surface::Path,
) -> Option<fhir::Sort> {
// CODESYNC(sort-of, 4) sorts should be given consistently

// CODESYNC(sort-of-path, 2) sorts should be given consistently
let res = resolver_output.path_res_map[&path.node_id];

match res {
Expand All @@ -1655,25 +1654,27 @@ fn sort_of_surface_path(
fhir::Res::PrimTy(PrimTy::Float(..) | PrimTy::Str | PrimTy::Char) => Some(fhir::Sort::Unit),
fhir::Res::Def(DefKind::TyAlias { .. } | DefKind::Enum | DefKind::Struct, def_id) => {
// TODO: duplication with sort_of_path
let Ok(generics) = genv.generics_of(def_id) else { return None };
let mut sort_args = vec![];
for (param, arg) in generics.params.iter().zip(&path.generics) {
if param.kind == GenericParamDefKind::BaseTy {
let surface::GenericArg::Type(ty) = arg else { return None };
let surface::BaseTyKind::Path(path) = &ty.as_bty()?.kind else {
return None;
};
let sort = sort_of_surface_path(genv, resolver_output, path)?;
sort_args.push(sort);
if let Some(generics) = genv.map().get_generics(def_id) {
for (param, arg) in generics.params.iter().zip(&path.generics) {
if let GenericParamKind::SplTy = param.kind {
let surface::GenericArg::Type(ty) = arg else { return None };
let surface::BaseTyKind::Path(path) = &ty.as_bty()?.kind else {
return None;
};
let sort = sort_of_surface_path(genv, resolver_output, path)?;
sort_args.push(sort);
}
}
}
println!("TRACE: sort_of_surface_path: {def_id:?} {sort_args:?}");
};
Some(fhir::Sort::Record(def_id, List::from_vec(sort_args)))
}
fhir::Res::Def(DefKind::TyParam, def_id) => {
let param = genv.get_generic_param(def_id.expect_local());
match &param.kind {
fhir::GenericParamKind::BaseTy => Some(fhir::Sort::Param(def_id)),
fhir::GenericParamKind::BaseTy | fhir::GenericParamKind::SplTy => {
Some(fhir::Sort::Param(def_id))
}
fhir::GenericParamKind::Type { .. } | fhir::GenericParamKind::Lifetime => None,
}
}
Expand Down
9 changes: 1 addition & 8 deletions crates/flux-desugar/src/lib.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -53,14 +53,7 @@ pub fn desugar_struct_def(
let mut cx = DesugarCtxt::new(genv, owner_id, resolver_output, None);

// Desugar and insert generics
let (generics, predicates) = if let Some(generics) = &struct_def.generics {
(cx.desugar_generics(generics)?, cx.as_lift_cx().lift_predicates()?)
} else {
cx.as_lift_cx().lift_generics_with_predicates()?
};
let refined_by = genv.map().refined_by(owner_id.def_id);
let generics = generics.with_refined_by(refined_by);
genv.map().insert_generics(def_id, generics);
let predicates = cx.as_lift_cx().lift_predicates()?;

// Desugar of struct_def needs to happen AFTER inserting generics. See #generics-and-desugaring
let struct_def = cx.desugar_struct_def(struct_def, &mut Binders::new())?;
Expand Down
4 changes: 3 additions & 1 deletion crates/flux-driver/src/callbacks.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -153,17 +153,19 @@ fn stage1_desugar(genv: &mut GlobalEnv, specs: &Specs) -> Result<(), ErrorGuaran
.err()
.or(err);

// Register RefinedBys
// Register RefinedBys (for structs and enums, which also registers their Generics)
err = specs
.refined_bys()
.try_for_each_exhaust(|(owner_id, refined_by)| {
let generics = lift::lift_generics(tcx, sess, owner_id)?;
let refined_by = if let Some(refined_by) = refined_by {
let def_id = owner_id.to_def_id();
let generics = tcx.generics_of(def_id);
desugar::desugar_refined_by(sess, map.sort_decls(), owner_id, generics, refined_by)?
} else {
lift::lift_refined_by(tcx, owner_id)
};
map.insert_generics(owner_id.def_id, generics.with_refined_by(&refined_by));
map.insert_refined_by(owner_id.def_id, refined_by);
Ok(())
})
Expand Down
9 changes: 7 additions & 2 deletions crates/flux-fhir-analysis/src/conv.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -162,6 +162,7 @@ pub(crate) fn conv_generics(
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::Lifetime => rty::GenericParamDefKind::Lifetime,
};
Expand Down Expand Up @@ -395,8 +396,9 @@ impl<'a, 'tcx> ConvCtxt<'a, 'tcx> {
let kind = rty::BoundRegionKind::BrNamed(def_id.to_def_id(), name);
Ok(rty::BoundVariableKind::Region(kind))
}
fhir::GenericParamKind::Type { default: _ } => bug!("unexpected!"),
fhir::GenericParamKind::BaseTy => bug!("unexpected!"),
fhir::GenericParamKind::Type { default: _ }
| fhir::GenericParamKind::BaseTy
| fhir::GenericParamKind::SplTy => bug!("unexpected!"),
}
}

Expand Down Expand Up @@ -635,6 +637,9 @@ impl<'a, 'tcx> ConvCtxt<'a, 'tcx> {

fn conv_base_ty(&self, env: &mut Env, bty: &fhir::BaseTy) -> QueryResult<rty::Ty> {
let sort = self.genv.sort_of_bty(bty);
// if sort.is_none() {
// println!("TRACE: conv_base_ty {bty:?} ==> None");
// }

if let fhir::BaseTyKind::Path(fhir::QPath::Resolved(self_ty, path)) = &bty.kind {
if let fhir::Res::Def(DefKind::AssocTy, def_id) = path.res {
Expand Down
2 changes: 1 addition & 1 deletion crates/flux-fhir-analysis/src/lib.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -160,7 +160,7 @@ fn generics_of(genv: &GlobalEnv, local_id: LocalDefId) -> QueryResult<rty::Gener
let is_trait = (def_kind == DefKind::Trait).then_some(local_id);
let generics = genv
.map()
.get_generics(local_id)
.get_generics(local_id.to_def_id())
.unwrap_or_else(|| bug!("no generics for {:?}", def_id));
let refine_params = genv
.map()
Expand Down
6 changes: 1 addition & 5 deletions crates/flux-fhir-analysis/src/wf/mod.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -411,13 +411,9 @@ impl<'a, 'tcx> Wf<'a, 'tcx> {
) -> Result<(), ErrorGuaranteed> {
if let Some(def_id) = adt_id &&
let Ok(generics) = self.genv.generics_of(def_id)
//&&
// let Some(local_def_id) = def_id.as_local()
{
// let refined_by = self.genv.map().refined_by(local_def_id);
for (arg, param) in args.iter().zip(generics.params.iter()) {
// if refined_by.is_base_generic(param.def_id) {
if param.kind == GenericParamDefKind::BaseTy {
if param.kind == GenericParamDefKind::SplTy {
if let fhir::GenericArg::Type(ty) = arg {
self.check_ty_is_base(ty)?
}
Expand Down
71 changes: 1 addition & 70 deletions crates/flux-fhir-analysis/src/wf/sortck.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -35,76 +35,6 @@ impl<'a, 'tcx> InferCtxt<'a, 'tcx> {
}
}

// CUT
// pub(super) fn check_refine_params(
// &mut self,
// owner_id: OwnerId,
// refine_params: &[fhir::RefineParam],
// ) -> Result<(), ErrorGuaranteed> {
// let allowed_generics: HashSet<DefId> = self
// .genv
// .generics_of(owner_id)
// .emit(self.genv.sess)?
// .params
// .iter()
// .filter_map(|param| {
// if let GenericParamDefKind::BaseTy = param.kind {
// Some(param.def_id)
// } else {
// None
// }
// })
// .collect();
// println!("TRACE: check_refine_params {owner_id:?} {allowed_generics:?} {refine_params:?}");
// for refine_param in refine_params {
// self.check_sort(&allowed_generics, &refine_param.sort)?
// }
// Ok(())
// }

// CUT
// fn check_sort(
// &self,
// allowed_generics: &HashSet<DefId>,
// sort: &fhir::Sort,
// ) -> Result<(), ErrorGuaranteed> {
// match sort {
// fhir::Sort::Int
// | fhir::Sort::Bool
// | fhir::Sort::Real
// | fhir::Sort::Loc
// | fhir::Sort::Unit
// | fhir::Sort::BitVec(_)
// | fhir::Sort::Var(_)
// | fhir::Sort::Infer(_)
// | fhir::Sort::Wildcard => Ok(()),
// fhir::Sort::App(_, sorts) => {
// for sort in sorts {
// self.check_sort(allowed_generics, sort)?;
// }
// Ok(())
// }
// fhir::Sort::Func(poly_func_sort) => {
// for sort in &poly_func_sort.skip_binders().inputs_and_output {
// self.check_sort(allowed_generics, sort)?;
// }
// Ok(())
// }
// fhir::Sort::Record(_, sorts) => {
// for sort in sorts {
// self.check_sort(allowed_generics, sort)?;
// }
// Ok(())
// }
// fhir::Sort::Param(def_id) => {
// if allowed_generics.contains(def_id) {
// Ok(())
// } else {
// Err(self.emit_err(errors::InvalidGenericSort::new(span, sort)))
// }
// }
// }
// }
pub(super) fn check_refine_arg(
&mut self,
arg: &fhir::RefineArg,
Expand Down Expand Up @@ -278,6 +208,7 @@ impl<'a, 'tcx> InferCtxt<'a, 'tcx> {
}
fhir::ExprKind::Dot(var, fld) => {
let sort = self[var.name].clone();
// println!("TRACE: synth_expr {:?} ==> {sort:?}", var.source_info.name);
match &sort {
fhir::Sort::Record(def_id, sort_args) => {
self.genv
Expand Down
9 changes: 5 additions & 4 deletions crates/flux-middle/src/fhir.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -65,6 +65,7 @@ pub struct GenericParam {
#[derive(Debug)]
pub enum GenericParamKind {
Type { default: Option<Ty> },
SplTy,
BaseTy,
Lifetime,
}
Expand Down Expand Up @@ -144,7 +145,7 @@ type Cache<K, V> = elsa::FrozenMap<K, V, std::hash::BuildHasherDefault<rustc_has
/// note: `Map` is a very generic name, so we typically use the type qualified as `fhir::Map`.
#[derive(Default)]
pub struct Map {
generics: Cache<LocalDefId, Box<Generics>>,
generics: Cache<DefId, Box<Generics>>,
predicates: ItemPredicates,
opaque_tys: UnordMap<LocalDefId, OpaqueTy>,
func_decls: FxHashMap<Symbol, FuncDecl>,
Expand Down Expand Up @@ -791,7 +792,7 @@ impl Generics {
let mut params = vec![];
for param in self.params {
let kind = if refined_by.is_base_generic(param.def_id.to_def_id()) {
GenericParamKind::BaseTy
GenericParamKind::SplTy
} else {
param.kind
};
Expand Down Expand Up @@ -1090,7 +1091,7 @@ impl Map {
}

pub fn insert_generics(&self, def_id: LocalDefId, generics: Generics) {
self.generics.insert(def_id, Box::new(generics));
self.generics.insert(def_id.to_def_id(), Box::new(generics));
}

pub fn insert_generic_predicates(&mut self, def_id: LocalDefId, predicates: GenericPredicates) {
Expand All @@ -1101,7 +1102,7 @@ impl Map {
self.opaque_tys.extend_unord(opaque_tys.into_items());
}

pub fn get_generics(&self, def_id: LocalDefId) -> Option<&Generics> {
pub fn get_generics(&self, def_id: DefId) -> Option<&Generics> {
self.generics.get(&def_id)
}

Expand Down
8 changes: 8 additions & 0 deletions crates/flux-middle/src/fhir/lift.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -33,6 +33,14 @@ pub fn lift_refined_by(tcx: TyCtxt, owner_id: OwnerId) -> fhir::RefinedBy {
}
}

pub fn lift_generics<'a, 'tcx>(
tcx: TyCtxt<'tcx>,
sess: &'a FluxSession,
owner_id: OwnerId,
) -> Result<fhir::Generics, ErrorGuaranteed> {
LiftCtxt::new(tcx, sess, owner_id, None).lift_generics()
}

pub fn lift_type_alias(
tcx: TyCtxt,
sess: &FluxSession,
Expand Down
28 changes: 18 additions & 10 deletions crates/flux-middle/src/global_env.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@ pub use rustc_span::{symbol::Ident, Symbol};

use crate::{
cstore::CrateStoreDyn,
fhir::{self, FluxLocalDefId, VariantIdx},
fhir::{self, FluxLocalDefId, GenericParamKind, VariantIdx},
intern::List,
queries::{Providers, Queries, QueryResult},
rty::{self, fold::TypeFoldable, normalize::Defns, refining::Refiner},
Expand Down Expand Up @@ -159,7 +159,10 @@ impl<'sess, 'tcx> GlobalEnv<'sess, 'tcx> {

pub fn get_generic_param(&self, def_id: LocalDefId) -> &fhir::GenericParam {
let owner = self.hir().ty_param_owner(def_id);
self.map().get_generics(owner).unwrap().get_param(def_id)
self.map()
.get_generics(owner.to_def_id())
.unwrap()
.get_param(def_id)
}

pub fn is_box(&self, res: fhir::Res) -> bool {
Expand Down Expand Up @@ -202,6 +205,7 @@ impl<'sess, 'tcx> GlobalEnv<'sess, 'tcx> {
}

pub fn sort_of_path(&self, path: &fhir::Path) -> Option<fhir::Sort> {
// CODESYNC(sort-of-path, 2) sorts should be given consistently
match path.res {
fhir::Res::PrimTy(PrimTy::Int(_) | PrimTy::Uint(_)) => Some(fhir::Sort::Int),
fhir::Res::PrimTy(PrimTy::Bool) => Some(fhir::Sort::Bool),
Expand All @@ -210,13 +214,15 @@ impl<'sess, 'tcx> GlobalEnv<'sess, 'tcx> {
}
fhir::Res::Def(DefKind::TyAlias { .. } | DefKind::Enum | DefKind::Struct, def_id) => {
let mut sort_args = vec![];
for arg in &path.args {
if let fhir::GenericArg::Type(ty) = arg &&
let Some(sort) = self.sort_of_ty(ty)
{
sort_args.push(sort);
if let Some(generics) = self.map().get_generics(def_id) {
for (param, arg) in generics.params.iter().zip(&path.args) {
if let GenericParamKind::SplTy = param.kind {
let fhir::GenericArg::Type(ty) = arg else { return None };
let sort = self.sort_of_ty(ty)?;
sort_args.push(sort);
}
}
}
};
Some(fhir::Sort::Record(def_id, List::from_vec(sort_args)))
}
fhir::Res::SelfTyAlias { alias_to, .. } => self.sort_of_self_ty_alias(alias_to),
Expand All @@ -235,7 +241,9 @@ impl<'sess, 'tcx> GlobalEnv<'sess, 'tcx> {
fn sort_of_generic_param(&self, def_id: DefId) -> Option<fhir::Sort> {
let param = self.get_generic_param(def_id.expect_local());
match &param.kind {
fhir::GenericParamKind::BaseTy => Some(fhir::Sort::Param(def_id)),
fhir::GenericParamKind::BaseTy | fhir::GenericParamKind::SplTy => {
Some(fhir::Sort::Param(def_id))
}
fhir::GenericParamKind::Type { .. } | fhir::GenericParamKind::Lifetime => None,
}
}
Expand All @@ -259,7 +267,7 @@ impl<'sess, 'tcx> GlobalEnv<'sess, 'tcx> {

fn sort_of_self_ty(&self, def_id: DefId, ty: rustc_middle::ty::Ty) -> Option<fhir::Sort> {
use rustc_middle::ty;
// CODESYNC(sort-of, 4) sorts should be given consistently
// CODESYNC(sort-of, 3) sorts should be given consistently
match ty.kind() {
ty::TyKind::Bool => Some(fhir::Sort::Bool),
ty::TyKind::Slice(_) | ty::TyKind::Int(_) | ty::TyKind::Uint(_) => {
Expand Down
Loading

0 comments on commit 0b537d0

Please sign in to comment.