Skip to content

Commit

Permalink
Prepare for non-top-level item binders
Browse files Browse the repository at this point in the history
  • Loading branch information
Nadrieril committed Dec 16, 2024
1 parent 3b50570 commit 009b068
Show file tree
Hide file tree
Showing 12 changed files with 420 additions and 190 deletions.
1 change: 1 addition & 0 deletions charon/src/ast/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -27,4 +27,5 @@ pub use krate::*;
pub use meta::*;
pub use names::*;
pub use types::*;
pub use types_utils::TyVisitable;
pub use values::*;
5 changes: 4 additions & 1 deletion charon/src/ast/names.rs
Original file line number Diff line number Diff line change
Expand Up @@ -29,10 +29,13 @@ pub enum PathElem {
#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize, Drive, DriveMut)]
#[charon::variants_prefix("ImplElem")]
pub enum ImplElem {
Ty(Binder<Ty>),
Ty(BoundTy),
Trait(TraitImplId),
}

/// Alias used for visitors.
pub type BoundTy = Binder<Ty>;

/// An item name/path
///
/// A name really is a list of strings. However, we sometimes need to
Expand Down
15 changes: 11 additions & 4 deletions charon/src/ast/types.rs
Original file line number Diff line number Diff line change
Expand Up @@ -234,6 +234,11 @@ pub struct RegionBinder<T> {
pub skip_binder: T,
}

// Renames useful for visitor derives
pub type BoundTypeOutlives = RegionBinder<TypeOutlives>;
pub type BoundRegionOutlives = RegionBinder<RegionOutlives>;
pub type BoundTraitTypeConstraint = RegionBinder<TraitTypeConstraint>;

/// A value of type `T` bound by generic parameters. Used in any context where we're adding generic
/// parameters that aren't on the top-level item, e.g. `for<'a>` clauses, trait methods (TODO),
/// GATs (TODO).
Expand Down Expand Up @@ -262,11 +267,11 @@ pub struct GenericParams {
// TODO: rename to match [GenericArgs]?
pub trait_clauses: Vector<TraitClauseId, TraitClause>,
/// The first region in the pair outlives the second region
pub regions_outlive: Vec<RegionBinder<RegionOutlives>>,
pub regions_outlive: Vec<BoundRegionOutlives>,
/// The type outlives the region
pub types_outlive: Vec<RegionBinder<TypeOutlives>>,
pub types_outlive: Vec<BoundTypeOutlives>,
/// Constraints over trait associated types
pub trait_type_constraints: Vec<RegionBinder<TraitTypeConstraint>>,
pub trait_type_constraints: Vec<BoundTraitTypeConstraint>,
}

/// A predicate of the form `exists<T> where T: Trait`.
Expand Down Expand Up @@ -657,9 +662,11 @@ pub enum TyKind {
/// This is essentially a "constrained" function signature:
/// arrow types can only contain generic lifetime parameters
/// (no generic types), no predicates, etc.
Arrow(RegionBinder<(Vec<Ty>, Ty)>),
Arrow(BoundArrowSig),
}

pub type BoundArrowSig = RegionBinder<(Vec<Ty>, Ty)>;

/// Builtin types identifiers.
///
/// WARNING: for now, all the built-in types are covariant in the generic
Expand Down
47 changes: 47 additions & 0 deletions charon/src/ast/types/vars.rs
Original file line number Diff line number Diff line change
Expand Up @@ -124,6 +124,10 @@ impl DeBruijnId {
DeBruijnId { index: 0 }
}

pub fn one() -> Self {
DeBruijnId { index: 1 }
}

pub fn new(index: usize) -> Self {
DeBruijnId { index }
}
Expand All @@ -143,6 +147,18 @@ impl DeBruijnId {
index: self.index - 1,
}
}

pub fn plus(&self, delta: Self) -> Self {
DeBruijnId {
index: self.index + delta.index,
}
}

pub fn sub(&self, delta: Self) -> Option<Self> {
Some(DeBruijnId {
index: self.index.checked_sub(delta.index)?,
})
}
}

impl<Id> DeBruijnVar<Id>
Expand All @@ -161,19 +177,44 @@ where
DeBruijnVar::Bound(index, id)
}

pub fn incr(&self) -> Self {
match *self {
DeBruijnVar::Bound(dbid, varid) => DeBruijnVar::Bound(dbid.incr(), varid),
DeBruijnVar::Free(varid) => DeBruijnVar::Free(varid),
}
}

pub fn decr(&self) -> Self {
match *self {
DeBruijnVar::Bound(dbid, varid) => DeBruijnVar::Bound(dbid.decr(), varid),
DeBruijnVar::Free(varid) => DeBruijnVar::Free(varid),
}
}

/// Returns the variable id if it is bound as the given depth.
pub fn bound_at_depth(&self, depth: DeBruijnId) -> Option<Id> {
match *self {
DeBruijnVar::Bound(dbid, varid) if dbid == depth => Some(varid),
_ => None,
}
}

/// Move the variable out of `depth` binders. Returns `None` if the variable is bound in one of
/// these `depth` binders.
pub fn move_out_from_depth(&self, depth: DeBruijnId) -> Option<Self> {
Some(match *self {
DeBruijnVar::Bound(dbid, varid) => DeBruijnVar::Bound(dbid.sub(depth)?, varid),
DeBruijnVar::Free(_) => *self,
})
}

/// Move under `depth` binders.
pub fn move_under_binders(&self, depth: DeBruijnId) -> Self {
match *self {
DeBruijnVar::Bound(dbid, varid) => DeBruijnVar::Bound(dbid.plus(depth), varid),
DeBruijnVar::Free(_) => *self,
}
}
}

impl TypeVar {
Expand All @@ -182,6 +223,12 @@ impl TypeVar {
}
}

impl Default for DeBruijnId {
fn default() -> Self {
Self::zero()
}
}

// The derive macro doesn't handle generics.
impl<Id: Drive> Drive for DeBruijnVar<Id> {
fn drive<V: Visitor>(&self, visitor: &mut V) {
Expand Down
149 changes: 125 additions & 24 deletions charon/src/ast/types_utils.rs
Original file line number Diff line number Diff line change
@@ -1,9 +1,10 @@
//! This file groups everything which is linked to implementations about [crate::types]
use crate::ast::BoundTy;
use crate::types::*;
use crate::{common::visitor_event::VisitEvent, ids::Vector};
use derive_visitor::{Drive, DriveMut, Event, Visitor, VisitorMut};
use derive_visitor::{visitor_enter_fn_mut, Drive, DriveMut, Event, Visitor, VisitorMut};
use std::collections::HashSet;
use std::{collections::HashMap, iter::Iterator};
use DeBruijnVar::Free;

impl GenericParams {
pub fn empty() -> Self {
Expand All @@ -21,6 +22,32 @@ impl GenericParams {
|| !self.trait_type_constraints.is_empty()
}

/// Run some sanity checks.
pub fn check_consistency(&self) {
// Sanity check: check the clause ids are consistent.
assert!(self
.trait_clauses
.iter()
.enumerate()
.all(|(i, c)| c.clause_id.index() == i));

// Sanity check: region names are pairwise distinct (this caused trouble when generating
// names for the backward functions in Aeneas): at some point, Rustc introduced names equal
// to `Some("'_")` for the anonymous regions, instead of using `None` (we now check in
// [translate_region_name] and ignore names equal to "'_").
let mut s = HashSet::new();
for r in &self.regions {
if let Some(name) = &r.name {
assert!(
!s.contains(name),
"Name \"{}\" reused for two different lifetimes",
name
);
s.insert(name);
}
}
}

pub fn len(&self) -> usize {
let GenericParams {
regions,
Expand Down Expand Up @@ -523,25 +550,32 @@ impl<V> std::ops::DerefMut for VisitInsideTy<V> {
}
}

type FnTys = (Vec<Ty>, Ty);

/// Visitor for the [Ty::substitute] function.
/// This substitutes only free variables; this does not work for non-top-level binders.
#[derive(VisitorMut)]
#[visitor(
PolyTraitDeclRef(enter, exit),
FnTys(enter, exit),
BoundArrowSig(enter, exit),
BoundRegionOutlives(enter, exit),
BoundTypeOutlives(enter, exit),
BoundTraitTypeConstraint(enter, exit),
BoundTy(enter, exit),
Region(exit),
Ty(exit),
ConstGeneric(exit),
TraitRef(exit)
)]
struct SubstVisitor<'a> {
pub(crate) struct SubstVisitor<'a> {
generics: &'a GenericArgs,
// Tracks the depth of binders we're inside of.
// Important: we must update it whenever we go inside a binder. Visitors are not generic so we
// must handle all the specific cases by hand. So far there's:
// - `PolyTraitDeclRef`
// - The contents of `TyKind::Arrow`
// - `TyKind::Arrow`
// - `BoundTypeOutlives`
// - `BoundRegionOutlives`
// - `BoundTraitTypeConstraint`
// - `BoundTy`
binder_depth: DeBruijnId,
}

Expand All @@ -553,27 +587,55 @@ impl<'a> SubstVisitor<'a> {
})
}

fn should_subst<Id: Copy>(&self, var: DeBruijnVar<Id>) -> Option<Id> {
match var {
DeBruijnVar::Free(id) => Some(id),
DeBruijnVar::Bound(..) => None,
}
}

fn enter_poly_trait_decl_ref(&mut self, _: &mut PolyTraitDeclRef) {
self.binder_depth = self.binder_depth.incr();
}

fn exit_poly_trait_decl_ref(&mut self, _: &mut PolyTraitDeclRef) {
self.binder_depth = self.binder_depth.decr();
}

fn enter_fn_tys(&mut self, _: &mut FnTys) {
fn enter_bound_arrow_sig(&mut self, _: &BoundArrowSig) {
self.binder_depth = self.binder_depth.incr();
}

fn exit_fn_tys(&mut self, _: &mut FnTys) {
fn exit_bound_arrow_sig(&mut self, _: &BoundArrowSig) {
self.binder_depth = self.binder_depth.decr();
}
fn enter_bound_ty(&mut self, _: &BoundTy) {
self.binder_depth = self.binder_depth.incr();
}
fn exit_bound_ty(&mut self, _: &BoundTy) {
self.binder_depth = self.binder_depth.decr();
}
fn enter_bound_type_outlives(&mut self, _: &BoundTypeOutlives) {
self.binder_depth = self.binder_depth.incr();
}
fn exit_bound_type_outlives(&mut self, _: &BoundTypeOutlives) {
self.binder_depth = self.binder_depth.decr();
}
fn enter_bound_region_outlives(&mut self, _: &BoundRegionOutlives) {
self.binder_depth = self.binder_depth.incr();
}
fn exit_bound_region_outlives(&mut self, _: &BoundRegionOutlives) {
self.binder_depth = self.binder_depth.decr();
}
fn enter_bound_trait_type_constraint(&mut self, _: &BoundTraitTypeConstraint) {
self.binder_depth = self.binder_depth.incr();
}
fn exit_bound_trait_type_constraint(&mut self, _: &BoundTraitTypeConstraint) {
self.binder_depth = self.binder_depth.decr();
}

fn exit_region(&mut self, r: &mut Region) {
match r {
Region::Var(var) => {
if let Some(varid) = var.bound_at_depth(self.binder_depth) {
*r = self.generics.regions.get(varid).unwrap().clone()
if let Some(varid) = self.should_subst(*var) {
*r = self.generics.regions[varid].move_under_binders(self.binder_depth)
}
}
_ => (),
Expand All @@ -582,39 +644,78 @@ impl<'a> SubstVisitor<'a> {

fn exit_ty(&mut self, ty: &mut Ty) {
match ty.kind() {
TyKind::TypeVar(Free(id)) => {
{}
*ty = self.generics.types.get(*id).unwrap().clone()
TyKind::TypeVar(var) => {
if let Some(id) = self.should_subst(*var) {
*ty = self.generics.types[id]
.clone()
.move_under_binders(self.binder_depth)
}
}
_ => (),
}
}

fn exit_const_generic(&mut self, cg: &mut ConstGeneric) {
match cg {
ConstGeneric::Var(Free(id)) => {
*cg = self.generics.const_generics.get(*id).unwrap().clone()
ConstGeneric::Var(var) => {
if let Some(id) = self.should_subst(*var) {
*cg = self.generics.const_generics[id]
.clone()
.move_under_binders(self.binder_depth)
}
}
_ => (),
}
}

fn exit_trait_ref(&mut self, tr: &mut TraitRef) {
match &mut tr.kind {
TraitRefKind::Clause(Free(id)) => {
*tr = self.generics.trait_refs.get(*id).unwrap().clone()
TraitRefKind::Clause(var) => {
if let Some(id) = self.should_subst(*var) {
*tr = self.generics.trait_refs[id]
.clone()
.move_under_binders(self.binder_depth)
}
}
_ => (),
}
}
}

impl Ty {
pub fn substitute(&mut self, generics: &GenericArgs) {
self.drive_inner_mut(&mut SubstVisitor::new(generics));
/// Types that are involved at the type-level and may be substituted around.
pub trait TyVisitable: Sized + Drive + DriveMut {
fn substitute(&mut self, generics: &GenericArgs) {
self.drive_mut(&mut SubstVisitor::new(generics));
}

/// Move under `depth` binders.
fn move_under_binders(mut self, depth: DeBruijnId) -> Self {
self.visit_db_id(|id| *id = id.plus(depth));
self
}

/// Move the region out of `depth` binders. Returns `None` if the variable is bound in one of
/// these `depth` binders.
fn move_from_under_binders(mut self, depth: DeBruijnId) -> Option<Self> {
let mut ok = true;
self.visit_db_id(|id| match id.sub(depth) {
Some(sub) => *id = sub,
None => ok = false,
});
ok.then_some(self)
}

/// Helper function.
fn visit_db_id(&mut self, f: impl FnMut(&mut DeBruijnId)) {
self.drive_mut(&mut Ty::visit_inside(visitor_enter_fn_mut(f)));
}
}

impl TyVisitable for ConstGeneric {}
impl TyVisitable for Region {}
impl TyVisitable for TraitRef {}
impl TyVisitable for Ty {}

impl PartialEq for TraitClause {
fn eq(&self, other: &Self) -> bool {
// Skip `span` and `origin`
Expand Down
Loading

0 comments on commit 009b068

Please sign in to comment.