Skip to content

Commit

Permalink
Rename RegionVarId to RegionId
Browse files Browse the repository at this point in the history
  • Loading branch information
@sonmarcho
sonmarcho committed Nov 10, 2023
1 parent d369bf4 commit 16ba3a9
Show file tree
Hide file tree
Showing 8 changed files with 90 additions and 90 deletions.
12 changes: 6 additions & 6 deletions charon/src/gast_utils.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -97,9 +97,9 @@ impl FunKind {
impl TraitDecl {
pub fn fmt_with_ctx<'a, C>(&'a self, ctx: &C) -> String
where
C: TypeFormatter<'a, Region<RegionVarId::Id>>
C: TypeFormatter<'a, Region<RegionId::Id>>
+ Formatter<&'a ErasedRegion>
+ Formatter<RegionVarId::Id>,
+ Formatter<RegionId::Id>,
{
let name = self.name.to_string();
let (generics, trait_clauses) = self.generics.fmt_with_ctx_with_trait_clauses(ctx);
Expand Down Expand Up @@ -172,9 +172,9 @@ impl TraitDecl {
impl TraitImpl {
pub fn fmt_with_ctx<'a, C>(&'a self, ctx: &C) -> String
where
C: TypeFormatter<'a, Region<RegionVarId::Id>>
C: TypeFormatter<'a, Region<RegionId::Id>>
+ Formatter<&'a ErasedRegion>
+ Formatter<RegionVarId::Id>,
+ Formatter<RegionId::Id>,
{
let name = self.name.to_string();
let (generics, trait_clauses) = self.generics.fmt_with_ctx_with_trait_clauses(ctx);
Expand Down Expand Up @@ -312,8 +312,8 @@ impl<T> GExprBody<T> {

pub trait GFunDeclFormatter<'a, Body: 'a> = ExprFormatter<'a>
+ Formatter<&'a Body>
+ Formatter<&'a Region<RegionVarId::Id>>
+ Formatter<RegionVarId::Id>;
+ Formatter<&'a Region<RegionId::Id>>
+ Formatter<RegionId::Id>;

impl<T> GFunDecl<T> {
/// This is an auxiliary function for printing definitions. One may wonder
Expand Down
48 changes: 24 additions & 24 deletions charon/src/regions_hierarchy.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -31,13 +31,13 @@ pub fn region_group_id_to_pretty_string(rid: RegionGroupId::Id) -> String {

#[derive(Copy, Clone)]
pub struct LifetimeConstraint {
region: Region<RegionVarId::Id>,
parent: Region<RegionVarId::Id>,
region: Region<RegionId::Id>,
parent: Region<RegionId::Id>,
}

/// An edge from r1 to r2 means:
/// r1 : r2 (i.e.: r1 lasts longer than r2)
type LifetimeConstraints = DiGraphMap<Region<RegionVarId::Id>, ()>;
type LifetimeConstraints = DiGraphMap<Region<RegionId::Id>, ()>;

/// A group of regions.
///
Expand All @@ -48,7 +48,7 @@ pub struct RegionGroup {
/// The region group identifier
pub id: RegionGroupId::Id,
/// The regions included in this group
pub regions: Vec<RegionVarId::Id>,
pub regions: Vec<RegionId::Id>,
/// The parent region groups
pub parents: Vec<RegionGroupId::Id>,
}
Expand All @@ -58,15 +58,15 @@ pub type RegionGroups = RegionGroupId::Vector<RegionGroup>;
/// Compute the region strongly connected components from a constraints graph.
fn compute_sccs_from_lifetime_constraints(
constraints_graph: &LifetimeConstraints,
region_params: &RegionVarId::Vector<RegionVar>,
) -> SCCs<Region<RegionVarId::Id>> {
region_params: &RegionId::Vector<RegionVar>,
) -> SCCs<Region<RegionId::Id>> {
// Apply Tarjan's algorithms to group the regions and the borrows which have
// the same lifetime. We then reorder those group of regions to be as close
// as possible to the original order.
let region_sccs = tarjan_scc(&constraints_graph);

// Reorder the SCCs
let get_region_parents = &|r: Region<RegionVarId::Id>| {
let get_region_parents = &|r: Region<RegionId::Id>| {
constraints_graph
.neighbors_directed(r, Direction::Outgoing)
.collect()
Expand All @@ -75,7 +75,7 @@ fn compute_sccs_from_lifetime_constraints(
// Option::iter is a trick to easily append a single region to the var regions
// Maybe there is a better way.
let all_var_regions = region_params.iter_indices().map(Region::Var);
let all_rids: Vec<Region<RegionVarId::Id>> = all_var_regions
let all_rids: Vec<Region<RegionId::Id>> = all_var_regions
.chain(Some(Region::Static).into_iter())
.collect();
trace!("all_rids: {:?}\nregion_sccs: {:?}", all_rids, region_sccs);
Expand All @@ -85,7 +85,7 @@ fn compute_sccs_from_lifetime_constraints(
trace!(
"{}",
vec_to_string(
&|scc: &Vec<Region<RegionVarId::Id>>| {
&|scc: &Vec<Region<RegionId::Id>>| {
let ids: Vec<String> = scc.iter().map(|r| r.to_string()).collect();
format!("[{}]", ids.join(", "))
},
Expand All @@ -102,7 +102,7 @@ fn compute_sccs_from_lifetime_constraints(
/// - then we compute the hierarchy from those accumulated constraints
/// This function performs the second step.
fn compute_regions_hierarchy_from_constraints(
mut constraints: SCCs<Region<RegionVarId::Id>>,
mut constraints: SCCs<Region<RegionId::Id>>,
) -> RegionGroups {
// The last SCC **MUST** contain the static region.
// For now, we don't handle cases where regions different from 'static
Expand All @@ -123,7 +123,7 @@ fn compute_regions_hierarchy_from_constraints(
let id = RegionGroupId::Id::new(i);

// Retrieve the set of regions in the group
let regions: Vec<RegionVarId::Id> = scc.into_iter().map(|r| *r.as_var()).collect();
let regions: Vec<RegionId::Id> = scc.into_iter().map(|r| *r.as_var()).collect();

// Compute the set of parent region groups
let parents: Vec<RegionGroupId::Id> = constraints
Expand All @@ -148,10 +148,10 @@ fn compute_regions_hierarchy_from_constraints(

/// See [TypesConstraintsMap]
pub type RegionVarsConstraintsMap =
LinkedHashMap<RegionVarId::Id, HashSet<Region<RegionVarId::Id>>>;
LinkedHashMap<RegionId::Id, HashSet<Region<RegionId::Id>>>;

/// See [TypesConstraintsMap]
pub type TypeVarsConstraintsMap = LinkedHashMap<TypeVarId::Id, HashSet<Region<RegionVarId::Id>>>;
pub type TypeVarsConstraintsMap = LinkedHashMap<TypeVarId::Id, HashSet<Region<RegionId::Id>>>;

/// See [TypesConstraintsMap]
#[derive(Debug, Clone)]
Expand Down Expand Up @@ -200,8 +200,8 @@ fn add_region_constraints(
updated: &mut bool,
acc_constraints: &mut LifetimeConstraints,
type_def_constraints: &mut Option<TypeDeclConstraintsMap>,
region: Region<RegionVarId::Id>,
parent_regions: &im::HashSet<Region<RegionVarId::Id>>,
region: Region<RegionId::Id>,
parent_regions: &im::HashSet<Region<RegionId::Id>>,
) {
// Check that the region is indeed in the nodes
if !acc_constraints.contains_node(region) {
Expand Down Expand Up @@ -250,7 +250,7 @@ fn compute_full_regions_constraints_for_ty(
constraints_map: &TypesConstraintsMap,
acc_constraints: &mut LifetimeConstraints,
type_def_constraints: &mut Option<TypeDeclConstraintsMap>, // TODO: rename
parent_regions: im::HashSet<Region<RegionVarId::Id>>,
parent_regions: im::HashSet<Region<RegionId::Id>>,
ty: &RTy,
) {
match ty {
Expand All @@ -268,8 +268,8 @@ fn compute_full_regions_constraints_for_ty(

// Compute the map from region param id to region instantation, for
// this ADT instantiation
let region_inst: RegionVarId::Vector<Region<RegionVarId::Id>> =
RegionVarId::Vector::from_iter(generics.regions.iter().copied());
let region_inst: RegionId::Vector<Region<RegionId::Id>> =
RegionId::Vector::from_iter(generics.regions.iter().copied());

// Lookup the constraints for this type definition
match type_id {
Expand Down Expand Up @@ -460,7 +460,7 @@ fn compute_regions_constraints_for_type_decl_group(
constraints_map: &mut TypesConstraintsMap,
types: &TypeDecls,
decl: &TypeDeclarationGroup,
) -> Vec<SCCs<Region<RegionVarId::Id>>> {
) -> Vec<SCCs<Region<RegionId::Id>>> {
// List the type ids in the type declaration group
let type_ids: HashSet<TypeDeclId::Id> = match decl {
TypeDeclarationGroup::NonRec(id) => {
Expand Down Expand Up @@ -603,7 +603,7 @@ fn compute_regions_constraints_for_type_decl_group(
}

// Compute the SCCs
let mut sccs_vec: Vec<SCCs<Region<RegionVarId::Id>>> = Vec::new();
let mut sccs_vec: Vec<SCCs<Region<RegionId::Id>>> = Vec::new();
for id in type_ids.iter() {
let type_def = types.get(*id).unwrap();
let sccs = compute_sccs_from_lifetime_constraints(
Expand Down Expand Up @@ -692,7 +692,7 @@ fn compute_regions_constraints_for_ty(
fn compute_regions_constraints_for_sig(
types_constraints: &TypesConstraintsMap,
sig: &FunSig,
) -> SCCs<Region<RegionVarId::Id>> {
) -> SCCs<Region<RegionId::Id>> {
trace!("sig: {sig:?}");

let mut constraints_graph = LifetimeConstraints::new();
Expand Down Expand Up @@ -742,7 +742,7 @@ pub fn compute_regions_hierarchies_for_functions(
impl RegionGroup {
pub fn fmt_with_ctx<T>(&self, ctx: &T) -> String
where
T: Formatter<RegionVarId::Id>,
T: Formatter<RegionId::Id>,
{
// The parent region groups
let parents: Vec<String> = self.parents.iter().map(|gid| gid.to_string()).collect();
Expand Down Expand Up @@ -773,8 +773,8 @@ fn types_def_constraints_map_fmt_with_ctx<'a, 'b, 'c, T>(
) -> String
where
T: Formatter<TypeVarId::Id>
+ Formatter<RegionVarId::Id>
+ Formatter<&'a Region<RegionVarId::Id>>,
+ Formatter<RegionId::Id>
+ Formatter<&'a Region<RegionId::Id>>,
{
let region_constraints = cs.region_vars_constraints.iter().map(|(rid, regions)| {
format!(
Expand Down
48 changes: 24 additions & 24 deletions charon/src/translate_ctx.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -157,9 +157,9 @@ pub(crate) struct BodyTransCtx<'tcx, 'ctx, 'ctx1> {
/// A hax state with an owner id
pub hax_state: hax::State<hax::Base<'tcx>, (), (), rustc_hir::def_id::DefId>,
/// The regions
pub region_vars: RegionVarId::Vector<RegionVar>,
pub region_vars: RegionId::Vector<RegionVar>,
/// The map from rust region to translated region indices
pub region_vars_map: RegionVarId::MapGenerator<hax::Region>,
pub region_vars_map: RegionId::MapGenerator<hax::Region>,
/// The type variables
pub type_vars: TypeVarId::Vector<TypeVar>,
/// The map from rust type variable indices to translated type variable
Expand Down Expand Up @@ -231,7 +231,7 @@ pub(crate) struct BodyTransCtx<'tcx, 'ctx, 'ctx1> {
/// ```
///
/// For this reason, we use a stack of vectors to store the bound variables.
pub bound_vars: im::Vector<im::Vector<RegionVarId::Id>>,
pub bound_vars: im::Vector<im::Vector<RegionId::Id>>,
}

/// A formatting context for type/global/function bodies.
Expand Down Expand Up @@ -484,8 +484,8 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
def_id,
t_ctx,
hax_state,
region_vars: RegionVarId::Vector::new(),
region_vars_map: RegionVarId::MapGenerator::new(),
region_vars: RegionId::Vector::new(),
region_vars_map: RegionId::MapGenerator::new(),
type_vars: TypeVarId::Vector::new(),
type_vars_map: TypeVarId::MapGenerator::new(),
vars: VarId::Vector::new(),
Expand Down Expand Up @@ -561,11 +561,11 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
self.t_ctx.translate_trait_impl_id(id)
}

pub(crate) fn get_region_from_rust(&self, r: hax::Region) -> Option<RegionVarId::Id> {
pub(crate) fn get_region_from_rust(&self, r: hax::Region) -> Option<RegionId::Id> {
self.region_vars_map.get(&r)
}

pub(crate) fn push_region(&mut self, r: hax::Region, name: Option<String>) -> RegionVarId::Id {
pub(crate) fn push_region(&mut self, r: hax::Region, name: Option<String>) -> RegionId::Id {
use crate::id_vector::ToUsize;
let rid = self.region_vars_map.insert(r);
assert!(rid.to_usize() == self.region_vars.len());
Expand All @@ -579,7 +579,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
use crate::id_vector::ToUsize;

// Register the variables
let var_ids: im::Vector<RegionVarId::Id> = names
let var_ids: im::Vector<RegionId::Id> = names
.into_iter()
.map(|name| {
// Note that we don't insert a binding in the region_vars_map
Expand Down Expand Up @@ -744,8 +744,8 @@ impl<'tcx, 'ctx> Formatter<GlobalDeclId::Id> for TransCtx<'tcx, 'ctx> {
}
}

impl<'tcx, 'ctx> Formatter<RegionVarId::Id> for TransCtx<'tcx, 'ctx> {
fn format_object(&self, id: RegionVarId::Id) -> String {
impl<'tcx, 'ctx> Formatter<RegionId::Id> for TransCtx<'tcx, 'ctx> {
fn format_object(&self, id: RegionId::Id) -> String {
id.to_pretty_string()
}
}
Expand All @@ -756,8 +756,8 @@ impl<'tcx, 'ctx> Formatter<TypeVarId::Id> for TransCtx<'tcx, 'ctx> {
}
}

impl<'tcx, 'ctx> Formatter<&Region<RegionVarId::Id>> for TransCtx<'tcx, 'ctx> {
fn format_object(&self, r: &Region<RegionVarId::Id>) -> String {
impl<'tcx, 'ctx> Formatter<&Region<RegionId::Id>> for TransCtx<'tcx, 'ctx> {
fn format_object(&self, r: &Region<RegionId::Id>) -> String {
r.fmt_with_ctx(self)
}
}
Expand Down Expand Up @@ -906,15 +906,15 @@ impl<'tcx, 'ctx, 'ctx1> Formatter<VarId::Id> for BodyTransCtx<'tcx, 'ctx, 'ctx1>
}
}

impl<'tcx, 'ctx, 'ctx1> Formatter<RegionVarId::Id> for BodyTransCtx<'tcx, 'ctx, 'ctx1> {
fn format_object(&self, id: RegionVarId::Id) -> String {
impl<'tcx, 'ctx, 'ctx1> Formatter<RegionId::Id> for BodyTransCtx<'tcx, 'ctx, 'ctx1> {
fn format_object(&self, id: RegionId::Id) -> String {
let v = self.region_vars.get(id).unwrap();
v.to_string()
}
}

impl<'tcx, 'ctx, 'ctx1> Formatter<&Region<RegionVarId::Id>> for BodyTransCtx<'tcx, 'ctx, 'ctx1> {
fn format_object(&self, r: &Region<RegionVarId::Id>) -> String {
impl<'tcx, 'ctx, 'ctx1> Formatter<&Region<RegionId::Id>> for BodyTransCtx<'tcx, 'ctx, 'ctx1> {
fn format_object(&self, r: &Region<RegionId::Id>) -> String {
r.fmt_with_ctx(self)
}
}
Expand All @@ -937,10 +937,10 @@ impl<'tcx, 'ctx, 'ctx1> Formatter<GlobalDeclId::Id> for BodyTransCtx<'tcx, 'ctx,
}
}

impl<'tcx, 'ctx, 'ctx1> Formatter<&Ty<Region<RegionVarId::Id>>>
impl<'tcx, 'ctx, 'ctx1> Formatter<&Ty<Region<RegionId::Id>>>
for BodyTransCtx<'tcx, 'ctx, 'ctx1>
{
fn format_object(&self, ty: &Ty<Region<RegionVarId::Id>>) -> String {
fn format_object(&self, ty: &Ty<Region<RegionId::Id>>) -> String {
ty.fmt_with_ctx(self)
}
}
Expand Down Expand Up @@ -1002,17 +1002,17 @@ impl<'tcx, 'ctx, 'ctx1> Formatter<VarId::Id> for BodyFormatCtx<'tcx, 'ctx, 'ctx1
}
}

impl<'tcx, 'ctx, 'ctx1> Formatter<RegionVarId::Id> for BodyFormatCtx<'tcx, 'ctx, 'ctx1> {
fn format_object(&self, id: RegionVarId::Id) -> String {
impl<'tcx, 'ctx, 'ctx1> Formatter<RegionId::Id> for BodyFormatCtx<'tcx, 'ctx, 'ctx1> {
fn format_object(&self, id: RegionId::Id) -> String {
match self.generics.regions.get(id) {
None => id.to_pretty_string(),
Some(v) => v.to_string(),
}
}
}

impl<'tcx, 'ctx, 'ctx1> Formatter<&Region<RegionVarId::Id>> for BodyFormatCtx<'tcx, 'ctx, 'ctx1> {
fn format_object(&self, r: &Region<RegionVarId::Id>) -> String {
impl<'tcx, 'ctx, 'ctx1> Formatter<&Region<RegionId::Id>> for BodyFormatCtx<'tcx, 'ctx, 'ctx1> {
fn format_object(&self, r: &Region<RegionId::Id>) -> String {
r.fmt_with_ctx(self)
}
}
Expand All @@ -1035,10 +1035,10 @@ impl<'tcx, 'ctx, 'ctx1> Formatter<GlobalDeclId::Id> for BodyFormatCtx<'tcx, 'ctx
}
}

impl<'tcx, 'ctx, 'ctx1> Formatter<&Ty<Region<RegionVarId::Id>>>
impl<'tcx, 'ctx, 'ctx1> Formatter<&Ty<Region<RegionId::Id>>>
for BodyFormatCtx<'tcx, 'ctx, 'ctx1>
{
fn format_object(&self, ty: &Ty<Region<RegionVarId::Id>>) -> String {
fn format_object(&self, ty: &Ty<Region<RegionId::Id>>) -> String {
ty.fmt_with_ctx(self)
}
}
Expand Down
2 changes: 1 addition & 1 deletion charon/src/translate_predicates.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -73,7 +73,7 @@ impl NonLocalTraitClause {

pub fn fmt_with_ctx<C>(&self, ctx: &C) -> String
where
C: for<'a> TypeFormatter<'a, Region<RegionVarId::Id>>
C: for<'a> TypeFormatter<'a, Region<RegionId::Id>>
+ for<'a> TypeFormatter<'a, ErasedRegion>,
{
let clause_id = self.clause_id.fmt_with_ctx(ctx);
Expand Down
4 changes: 2 additions & 2 deletions charon/src/translate_types.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -110,7 +110,7 @@ impl<'tcx, 'ctx, 'ctx1> TyTranslator<ErasedRegion> for BodyTransCtx<'tcx, 'ctx,
}
}

impl<'tcx, 'ctx, 'ctx1> TyTranslator<Region<RegionVarId::Id>> for BodyTransCtx<'tcx, 'ctx, 'ctx1> {
impl<'tcx, 'ctx, 'ctx1> TyTranslator<Region<RegionId::Id>> for BodyTransCtx<'tcx, 'ctx, 'ctx1> {
fn convert_rty(&self, ty: &RTy) -> RTy {
ty.clone()
}
Expand All @@ -123,7 +123,7 @@ impl<'tcx, 'ctx, 'ctx1> TyTranslator<Region<RegionVarId::Id>> for BodyTransCtx<'
t.clone()
}

fn translate_region(&self, region: &hax::Region) -> Region<RegionVarId::Id> {
fn translate_region(&self, region: &hax::Region) -> Region<RegionId::Id> {
match &region.kind {
hax::RegionKind::ReErased => unreachable!(),
hax::RegionKind::ReStatic => Region::Static,
Expand Down
Loading

0 comments on commit 16ba3a9

Please sign in to comment.