Rename the code that replaces unbound variables to "freshen" rather than "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.

This commit is contained in:
Niko Matsakis 2014-12-12 06:13:42 -05:00
parent 3cf0fbeee9
commit 416e62924e
6 changed files with 104 additions and 100 deletions

View File

@ -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
@ -39,26 +39,26 @@ 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 {
@ -66,12 +66,12 @@ impl<'a, 'tcx> TypeSkolemizer<'a, 'tcx> {
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
}
@ -79,7 +79,7 @@ impl<'a, 'tcx> TypeSkolemizer<'a, 'tcx> {
}
}
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
}
@ -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 |

View File

@ -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;
@ -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;
@ -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 {
@ -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>)

View File

@ -30,7 +30,7 @@ use middle::mem_categorization::Typer;
use middle::subst::{Subst, Substs, VecPerParamSpace};
use middle::ty::{mod, Ty, RegionEscape};
use middle::infer;
use middle::infer::{InferCtxt, TypeSkolemizer};
use middle::infer::{InferCtxt, TypeFreshener};
use middle::ty_fold::TypeFoldable;
use std::cell::RefCell;
use std::collections::hash_map::HashMap;
@ -44,12 +44,12 @@ pub struct SelectionContext<'cx, 'tcx:'cx> {
param_env: &'cx ty::ParameterEnvironment<'tcx>,
typer: &'cx (Typer<'tcx>+'cx),
/// Skolemizer used specifically for skolemizing entries on the
/// Freshener used specifically for skolemizing entries on the
/// obligation stack. This ensures that all entries on the stack
/// at one time will have the same set of skolemized entries,
/// which is important for checking for trait bounds that
/// recursively require themselves.
skolemizer: TypeSkolemizer<'cx, 'tcx>,
freshener: TypeFreshener<'cx, 'tcx>,
/// If true, indicates that the evaluation should be conservative
/// and consider the possibility of types outside this crate.
@ -73,8 +73,8 @@ struct TraitObligationStack<'prev, 'tcx: 'prev> {
obligation: &'prev TraitObligation<'tcx>,
/// Trait ref from `obligation` but skolemized with the
/// selection-context's skolemizer. Used to check for recursion.
skol_trait_ref: Rc<ty::PolyTraitRef<'tcx>>,
/// selection-context's freshener. Used to check for recursion.
fresh_trait_ref: Rc<ty::PolyTraitRef<'tcx>>,
previous: Option<&'prev TraitObligationStack<'prev, 'tcx>>
}
@ -172,7 +172,7 @@ impl<'cx, 'tcx> SelectionContext<'cx, 'tcx> {
infcx: infcx,
param_env: param_env,
typer: typer,
skolemizer: infcx.skolemizer(),
freshener: infcx.freshener(),
intercrate: false,
}
}
@ -185,7 +185,7 @@ impl<'cx, 'tcx> SelectionContext<'cx, 'tcx> {
infcx: infcx,
param_env: param_env,
typer: typer,
skolemizer: infcx.skolemizer(),
freshener: infcx.freshener(),
intercrate: true,
}
}
@ -347,16 +347,16 @@ impl<'cx, 'tcx> SelectionContext<'cx, 'tcx> {
// This suffices to allow chains like `FnMut` implemented in
// terms of `Fn` etc, but we could probably make this more
// precise still.
let input_types = stack.skol_trait_ref.value.input_types();
let unbound_input_types = input_types.iter().any(|&t| ty::type_is_skolemized(t));
let input_types = stack.fresh_trait_ref.value.input_types();
let unbound_input_types = input_types.iter().any(|&t| ty::type_is_fresh(t));
if
unbound_input_types &&
(self.intercrate ||
stack.iter().skip(1).any(
|prev| stack.skol_trait_ref.value.def_id == prev.skol_trait_ref.value.def_id))
|prev| stack.fresh_trait_ref.value.def_id == prev.fresh_trait_ref.value.def_id))
{
debug!("evaluate_stack({}) --> unbound argument, recursion --> ambiguous",
stack.skol_trait_ref.repr(self.tcx()));
stack.fresh_trait_ref.repr(self.tcx()));
return EvaluatedToAmbig;
}
@ -373,19 +373,19 @@ impl<'cx, 'tcx> SelectionContext<'cx, 'tcx> {
// `Option<Box<List<T>>>` is `Send` if `Box<List<T>>` is
// `Send`.
//
// Note that we do this comparison using the `skol_trait_ref`
// Note that we do this comparison using the `fresh_trait_ref`
// fields. Because these have all been skolemized using
// `self.skolemizer`, we can be sure that (a) this will not
// `self.freshener`, we can be sure that (a) this will not
// affect the inferencer state and (b) that if we see two
// skolemized types with the same index, they refer to the
// same unbound type variable.
if
stack.iter()
.skip(1) // skip top-most frame
.any(|prev| stack.skol_trait_ref == prev.skol_trait_ref)
.any(|prev| stack.fresh_trait_ref == prev.fresh_trait_ref)
{
debug!("evaluate_stack({}) --> recursive",
stack.skol_trait_ref.repr(self.tcx()));
stack.fresh_trait_ref.repr(self.tcx()));
return EvaluatedToOk;
}
@ -445,20 +445,20 @@ impl<'cx, 'tcx> SelectionContext<'cx, 'tcx> {
}
// Check the cache. Note that we skolemize the trait-ref
// separately rather than using `stack.skol_trait_ref` -- this
// separately rather than using `stack.fresh_trait_ref` -- this
// is because we want the unbound variables to be replaced
// with fresh skolemized types starting from index 0.
let cache_skol_trait_ref =
self.infcx.skolemize(stack.obligation.trait_ref.clone());
debug!("candidate_from_obligation(cache_skol_trait_ref={}, obligation={})",
cache_skol_trait_ref.repr(self.tcx()),
let cache_fresh_trait_ref =
self.infcx.freshen(stack.obligation.trait_ref.clone());
debug!("candidate_from_obligation(cache_fresh_trait_ref={}, obligation={})",
cache_fresh_trait_ref.repr(self.tcx()),
stack.repr(self.tcx()));
assert!(!stack.obligation.trait_ref.has_escaping_regions());
match self.check_candidate_cache(cache_skol_trait_ref.clone()) {
match self.check_candidate_cache(cache_fresh_trait_ref.clone()) {
Some(c) => {
debug!("CACHE HIT: cache_skol_trait_ref={}, candidate={}",
cache_skol_trait_ref.repr(self.tcx()),
debug!("CACHE HIT: cache_fresh_trait_ref={}, candidate={}",
cache_fresh_trait_ref.repr(self.tcx()),
c.repr(self.tcx()));
return c;
}
@ -467,9 +467,9 @@ impl<'cx, 'tcx> SelectionContext<'cx, 'tcx> {
// If no match, compute result and insert into cache.
let candidate = self.candidate_from_obligation_no_cache(stack);
debug!("CACHE MISS: cache_skol_trait_ref={}, candidate={}",
cache_skol_trait_ref.repr(self.tcx()), candidate.repr(self.tcx()));
self.insert_candidate_cache(cache_skol_trait_ref, candidate.clone());
debug!("CACHE MISS: cache_fresh_trait_ref={}, candidate={}",
cache_fresh_trait_ref.repr(self.tcx()), candidate.repr(self.tcx()));
self.insert_candidate_cache(cache_fresh_trait_ref, candidate.clone());
candidate
}
@ -569,7 +569,7 @@ impl<'cx, 'tcx> SelectionContext<'cx, 'tcx> {
}
fn pick_candidate_cache(&self,
cache_skol_trait_ref: &Rc<ty::PolyTraitRef<'tcx>>)
cache_fresh_trait_ref: &Rc<ty::PolyTraitRef<'tcx>>)
-> &SelectionCache<'tcx>
{
// High-level idea: we have to decide whether to consult the
@ -591,7 +591,7 @@ impl<'cx, 'tcx> SelectionContext<'cx, 'tcx> {
// If the trait refers to any parameters in scope, then use
// the cache of the param-environment.
if
cache_skol_trait_ref.value.input_types().iter().any(
cache_fresh_trait_ref.value.input_types().iter().any(
|&t| ty::type_has_self(t) || ty::type_has_params(t))
{
return &self.param_env.selection_cache;
@ -604,7 +604,7 @@ impl<'cx, 'tcx> SelectionContext<'cx, 'tcx> {
// See the discussion in doc.rs for more details.
if
!self.param_env.caller_bounds.is_empty() &&
cache_skol_trait_ref.value.input_types().iter().any(
cache_fresh_trait_ref.value.input_types().iter().any(
|&t| ty::type_has_ty_infer(t))
{
return &self.param_env.selection_cache;
@ -615,21 +615,21 @@ impl<'cx, 'tcx> SelectionContext<'cx, 'tcx> {
}
fn check_candidate_cache(&mut self,
cache_skol_trait_ref: Rc<ty::PolyTraitRef<'tcx>>)
cache_fresh_trait_ref: Rc<ty::PolyTraitRef<'tcx>>)
-> Option<SelectionResult<'tcx, Candidate<'tcx>>>
{
let cache = self.pick_candidate_cache(&cache_skol_trait_ref);
let cache = self.pick_candidate_cache(&cache_fresh_trait_ref);
let hashmap = cache.hashmap.borrow();
hashmap.get(&cache_skol_trait_ref).map(|c| (*c).clone())
hashmap.get(&cache_fresh_trait_ref).map(|c| (*c).clone())
}
fn insert_candidate_cache(&mut self,
cache_skol_trait_ref: Rc<ty::PolyTraitRef<'tcx>>,
cache_fresh_trait_ref: Rc<ty::PolyTraitRef<'tcx>>,
candidate: SelectionResult<'tcx, Candidate<'tcx>>)
{
let cache = self.pick_candidate_cache(&cache_skol_trait_ref);
let cache = self.pick_candidate_cache(&cache_fresh_trait_ref);
let mut hashmap = cache.hashmap.borrow_mut();
hashmap.insert(cache_skol_trait_ref, candidate);
hashmap.insert(cache_fresh_trait_ref, candidate);
}
fn assemble_candidates<'o>(&mut self,
@ -1269,8 +1269,8 @@ impl<'cx, 'tcx> SelectionContext<'cx, 'tcx> {
}
ty::ty_open(_) |
ty::ty_infer(ty::SkolemizedTy(_)) |
ty::ty_infer(ty::SkolemizedIntTy(_)) => {
ty::ty_infer(ty::FreshTy(_)) |
ty::ty_infer(ty::FreshIntTy(_)) => {
self.tcx().sess.bug(
format!(
"asked to assemble builtin bounds of unexpected type: {}",
@ -1831,11 +1831,11 @@ impl<'cx, 'tcx> SelectionContext<'cx, 'tcx> {
obligation: &'o TraitObligation<'tcx>)
-> TraitObligationStack<'o, 'tcx>
{
let skol_trait_ref = obligation.trait_ref.fold_with(&mut self.skolemizer);
let fresh_trait_ref = obligation.trait_ref.fold_with(&mut self.freshener);
TraitObligationStack {
obligation: obligation,
skol_trait_ref: skol_trait_ref,
fresh_trait_ref: fresh_trait_ref,
previous: previous_stack.map(|p| p), // FIXME variance
}
}

View File

@ -1538,12 +1538,16 @@ pub enum InferTy {
TyVar(TyVid),
IntVar(IntVid),
FloatVar(FloatVid),
SkolemizedTy(uint),
/// A `FreshTy` is one that is generated as a replacement for an
/// unbound type variable. This is convenient for caching etc. See
/// `middle::infer::freshen` for more details.
FreshTy(uint),
// FIXME -- once integral fallback is impl'd, we should remove
// this type. It's only needed to prevent spurious errors for
// integers whose type winds up never being constrained.
SkolemizedIntTy(uint),
FreshIntTy(uint),
}
impl Copy for InferTy {}
@ -1610,8 +1614,8 @@ impl fmt::Show for InferTy {
TyVar(ref v) => v.fmt(f),
IntVar(ref v) => v.fmt(f),
FloatVar(ref v) => v.fmt(f),
SkolemizedTy(v) => write!(f, "SkolemizedTy({})", v),
SkolemizedIntTy(v) => write!(f, "SkolemizedIntTy({})", v),
FreshTy(v) => write!(f, "FreshTy({})", v),
FreshIntTy(v) => write!(f, "FreshIntTy({})", v),
}
}
}
@ -2986,7 +2990,7 @@ pub fn type_contents<'tcx>(cx: &ctxt<'tcx>, ty: Ty<'tcx>) -> TypeContents {
}
// Scalar and unique types are sendable, and durable
ty_infer(ty::SkolemizedIntTy(_)) |
ty_infer(ty::FreshIntTy(_)) |
ty_bool | ty_int(_) | ty_uint(_) | ty_float(_) |
ty_bare_fn(_) | ty::ty_char => {
TC::None
@ -3592,10 +3596,10 @@ pub fn type_is_integral(ty: Ty) -> bool {
}
}
pub fn type_is_skolemized(ty: Ty) -> bool {
pub fn type_is_fresh(ty: Ty) -> bool {
match ty.sty {
ty_infer(SkolemizedTy(_)) => true,
ty_infer(SkolemizedIntTy(_)) => true,
ty_infer(FreshTy(_)) => true,
ty_infer(FreshIntTy(_)) => true,
_ => false
}
}
@ -4428,8 +4432,8 @@ pub fn ty_sort_string<'tcx>(cx: &ctxt<'tcx>, ty: Ty<'tcx>) -> String {
ty_infer(TyVar(_)) => "inferred type".to_string(),
ty_infer(IntVar(_)) => "integral variable".to_string(),
ty_infer(FloatVar(_)) => "floating-point variable".to_string(),
ty_infer(SkolemizedTy(_)) => "skolemized type".to_string(),
ty_infer(SkolemizedIntTy(_)) => "skolemized integral type".to_string(),
ty_infer(FreshTy(_)) => "skolemized type".to_string(),
ty_infer(FreshIntTy(_)) => "skolemized integral type".to_string(),
ty_param(ref p) => {
if p.space == subst::SelfSpace {
"Self".to_string()
@ -5594,7 +5598,7 @@ pub fn object_region_bounds<'tcx>(tcx: &ctxt<'tcx>,
// Since we don't actually *know* the self type for an object,
// this "open(err)" serves as a kind of dummy standin -- basically
// a skolemized type.
let open_ty = ty::mk_infer(tcx, SkolemizedTy(0));
let open_ty = ty::mk_infer(tcx, FreshTy(0));
let opt_trait_ref = opt_principal.map_or(Vec::new(), |principal| {
let substs = principal.substs().with_self_ty(open_ty);

View File

@ -374,8 +374,8 @@ pub fn ty_to_string<'tcx>(cx: &ctxt<'tcx>, typ: &ty::TyS<'tcx>) -> String {
ty::IntVar(ref vid) if print_var_ids => vid.repr(cx),
ty::FloatVar(ref vid) if print_var_ids => vid.repr(cx),
ty::TyVar(_) | ty::IntVar(_) | ty::FloatVar(_) => format!("_"),
ty::SkolemizedTy(v) => format!("SkolemizedTy({})", v),
ty::SkolemizedIntTy(v) => format!("SkolemizedIntTy({})", v)
ty::FreshTy(v) => format!("FreshTy({})", v),
ty::FreshIntTy(v) => format!("FreshIntTy({})", v)
}
}

View File

@ -848,12 +848,12 @@ pub fn fulfill_obligation<'a, 'tcx>(ccx: &CrateContext<'a, 'tcx>,
}
}
// Use skolemize to simultaneously replace all type variables with
// Use freshen to simultaneously replace all type variables with
// their bindings and replace all regions with 'static. This is
// sort of overkill because we do not expect there to be any
// unbound type variables, hence no skolemized types should ever
// be inserted.
let vtable = vtable.fold_with(&mut infcx.skolemizer());
// unbound type variables, hence no `TyFresh` types should ever be
// inserted.
let vtable = vtable.fold_with(&mut infcx.freshener());
info!("Cache miss: {}", trait_ref.repr(ccx.tcx()));
ccx.trait_cache().borrow_mut().insert(trait_ref,