Skip to content

Commit

Permalink
Rename the code that replaces unbound variables to "freshen" rather t…
Browse files Browse the repository at this point in the history
…han "skolemize" -- strictly speaking, this is not skolemization, because it is not discharging quantifiers. Also, the trait selection code will still be doing true skolemization, so it would be a confusing overlap of names.
  • Loading branch information
nikomatsakis committed Dec 19, 2014
1 parent 3cf0fbe commit 416e629
Show file tree
Hide file tree
Showing 6 changed files with 104 additions and 100 deletions.
Expand Up @@ -8,21 +8,21 @@
// option. This file may not be copied, modified, or distributed
// except according to those terms.

//! Skolemization is the process of replacing unknown variables with fresh types. The idea is that
//! the type, after skolemization, contains no inference variables but instead contains either a
//! Freshening is the process of replacing unknown variables with fresh types. The idea is that
//! the type, after freshening, contains no inference variables but instead contains either a
//! value for each variable or fresh "arbitrary" types wherever a variable would have been.
//!
//! Skolemization is used primarily to get a good type for inserting into a cache. The result
//! Freshening is used primarily to get a good type for inserting into a cache. The result
//! summarizes what the type inferencer knows "so far". The primary place it is used right now is
//! in the trait matching algorithm, which needs to be able to cache whether an `impl` self type
//! matches some other type X -- *without* affecting `X`. That means if that if the type `X` is in
//! fact an unbound type variable, we want the match to be regarded as ambiguous, because depending
//! on what type that type variable is ultimately assigned, the match may or may not succeed.
//!
//! Note that you should be careful not to allow the output of skolemization to leak to the user in
//! error messages or in any other form. Skolemization is only really useful as an internal detail.
//! Note that you should be careful not to allow the output of freshening to leak to the user in
//! error messages or in any other form. Freshening is only really useful as an internal detail.
//!
//! __An important detail concerning regions.__ The skolemizer also replaces *all* regions with
//! __An important detail concerning regions.__ The freshener also replaces *all* regions with
//! 'static. The reason behind this is that, in general, we do not take region relationships into
//! account when making type-overloaded decisions. This is important because of the design of the
//! region inferencer, which is not based on unification but rather on accumulating and then
Expand All @@ -39,47 +39,47 @@ use std::collections::hash_map;
use super::InferCtxt;
use super::unify::InferCtxtMethodsForSimplyUnifiableTypes;

pub struct TypeSkolemizer<'a, 'tcx:'a> {
pub struct TypeFreshener<'a, 'tcx:'a> {
infcx: &'a InferCtxt<'a, 'tcx>,
skolemization_count: uint,
skolemization_map: hash_map::HashMap<ty::InferTy, Ty<'tcx>>,
freshen_count: uint,
freshen_map: hash_map::HashMap<ty::InferTy, Ty<'tcx>>,
}

impl<'a, 'tcx> TypeSkolemizer<'a, 'tcx> {
pub fn new(infcx: &'a InferCtxt<'a, 'tcx>) -> TypeSkolemizer<'a, 'tcx> {
TypeSkolemizer {
impl<'a, 'tcx> TypeFreshener<'a, 'tcx> {
pub fn new(infcx: &'a InferCtxt<'a, 'tcx>) -> TypeFreshener<'a, 'tcx> {
TypeFreshener {
infcx: infcx,
skolemization_count: 0,
skolemization_map: hash_map::HashMap::new(),
freshen_count: 0,
freshen_map: hash_map::HashMap::new(),
}
}

fn skolemize<F>(&mut self,
opt_ty: Option<Ty<'tcx>>,
key: ty::InferTy,
skolemizer: F)
-> Ty<'tcx> where
fn freshen<F>(&mut self,
opt_ty: Option<Ty<'tcx>>,
key: ty::InferTy,
freshener: F)
-> Ty<'tcx> where
F: FnOnce(uint) -> ty::InferTy,
{
match opt_ty {
Some(ty) => { return ty.fold_with(self); }
None => { }
}

match self.skolemization_map.entry(key) {
match self.freshen_map.entry(key) {
hash_map::Occupied(entry) => *entry.get(),
hash_map::Vacant(entry) => {
let index = self.skolemization_count;
self.skolemization_count += 1;
let t = ty::mk_infer(self.infcx.tcx, skolemizer(index));
let index = self.freshen_count;
self.freshen_count += 1;
let t = ty::mk_infer(self.infcx.tcx, freshener(index));
entry.set(t);
t
}
}
}
}

impl<'a, 'tcx> TypeFolder<'tcx> for TypeSkolemizer<'a, 'tcx> {
impl<'a, 'tcx> TypeFolder<'tcx> for TypeFreshener<'a, 'tcx> {
fn tcx<'b>(&'b self) -> &'b ty::ctxt<'tcx> {
self.infcx.tcx
}
Expand All @@ -106,37 +106,37 @@ impl<'a, 'tcx> TypeFolder<'tcx> for TypeSkolemizer<'a, 'tcx> {
fn fold_ty(&mut self, t: Ty<'tcx>) -> Ty<'tcx> {
match t.sty {
ty::ty_infer(ty::TyVar(v)) => {
self.skolemize(self.infcx.type_variables.borrow().probe(v),
self.freshen(self.infcx.type_variables.borrow().probe(v),
ty::TyVar(v),
ty::SkolemizedTy)
ty::FreshTy)
}

ty::ty_infer(ty::IntVar(v)) => {
self.skolemize(self.infcx.probe_var(v),
ty::IntVar(v),
ty::SkolemizedIntTy)
self.freshen(self.infcx.probe_var(v),
ty::IntVar(v),
ty::FreshIntTy)
}

ty::ty_infer(ty::FloatVar(v)) => {
self.skolemize(self.infcx.probe_var(v),
ty::FloatVar(v),
ty::SkolemizedIntTy)
self.freshen(self.infcx.probe_var(v),
ty::FloatVar(v),
ty::FreshIntTy)
}

ty::ty_infer(ty::SkolemizedTy(c)) |
ty::ty_infer(ty::SkolemizedIntTy(c)) => {
if c >= self.skolemization_count {
ty::ty_infer(ty::FreshTy(c)) |
ty::ty_infer(ty::FreshIntTy(c)) => {
if c >= self.freshen_count {
self.tcx().sess.bug(
format!("Encountered a skolemized type with id {} \
format!("Encountered a freshend type with id {} \
but our counter is only at {}",
c,
self.skolemization_count).as_slice());
self.freshen_count).as_slice());
}
t
}

ty::ty_open(..) => {
self.tcx().sess.bug("Cannot skolemize an open existential type");
self.tcx().sess.bug("Cannot freshen an open existential type");
}

ty::ty_bool |
Expand Down
12 changes: 6 additions & 6 deletions src/librustc/middle/infer/mod.rs
Expand Up @@ -19,7 +19,7 @@ pub use self::TypeOrigin::*;
pub use self::ValuePairs::*;
pub use self::fixup_err::*;
pub use middle::ty::IntVarValue;
pub use self::skolemize::TypeSkolemizer;
pub use self::freshen::TypeFreshener;

use middle::subst;
use middle::subst::Substs;
Expand Down Expand Up @@ -57,7 +57,7 @@ pub mod lattice;
pub mod lub;
pub mod region_inference;
pub mod resolve;
mod skolemize;
mod freshen;
pub mod sub;
pub mod type_variable;
pub mod unify;
Expand Down Expand Up @@ -505,8 +505,8 @@ pub struct CombinedSnapshot {
}

impl<'a, 'tcx> InferCtxt<'a, 'tcx> {
pub fn skolemize<T:TypeFoldable<'tcx>>(&self, t: T) -> T {
t.fold_with(&mut self.skolemizer())
pub fn freshen<T:TypeFoldable<'tcx>>(&self, t: T) -> T {
t.fold_with(&mut self.freshener())
}

pub fn type_var_diverges(&'a self, ty: Ty) -> bool {
Expand All @@ -516,8 +516,8 @@ impl<'a, 'tcx> InferCtxt<'a, 'tcx> {
}
}

pub fn skolemizer<'b>(&'b self) -> TypeSkolemizer<'b, 'tcx> {
skolemize::TypeSkolemizer::new(self)
pub fn freshener<'b>(&'b self) -> TypeFreshener<'b, 'tcx> {
freshen::TypeFreshener::new(self)
}

pub fn combine_fields<'b>(&'b self, a_is_expected: bool, trace: TypeTrace<'tcx>)
Expand Down

0 comments on commit 416e629

Please sign in to comment.