Struct gluon_check::substitution::Substitution

pub struct Substitution<T> where
    T: Substitutable,  { /* fields omitted */ }

Methods

impl<T> Substitution<T> where
    T: Substitutable, 

pub fn new(factory: T::Factory, interner: T::Interner) -> Substitution<T>

pub fn var_id(&self) -> u32

pub fn insert(&self, var: u32, t: T)

pub fn replace(&mut self, var: u32, t: T)

pub fn clear_from(&mut self, level: u32)

Assumes that no variables unified with anything (but variables < level may exist)

pub fn new_var(&self) -> T where
    T: Clone, 

Creates a new variable

pub fn new_var_fn<F>(&self, f: F) -> T where
    T: Clone,
    F: FnOnce(u32) -> T, 

pub fn real<'r>(&'r self, typ: &'r T) -> &'r T

If typ is a variable this returns the real unified value of that variable. Otherwise it just returns the type itself. Note that the returned type may contain terms which also need to have real called on them.

pub fn get_var(&self, var: u32) -> Option<&T>

pub fn find_type_for_var(&self, var: u32) -> Option<&T>

pub fn update_level(&self, var: u32, other: u32)

Updates the level of other to be the minimum level value of var and other

pub fn set_level(&self, var: u32, level: u32)

pub fn get_level(&self, var: u32) -> u32

pub fn replace_variable(&self, typ: &T) -> Option<T> where
    T: Clone, 

impl<T: Substitutable + Clone> Substitution<T>

pub fn make_real(&self, typ: &mut T)

impl<T: Substitutable + PartialEq + Clone> Substitution<T>

pub fn union(&self, id: &T::Variable, typ: &T) -> Result<Option<T>, Error<T>> where
    T::Variable: Clone,
    T: Display, 

Takes id and updates the substitution to say that it should have the same type as typ

impl Substitution<RcType>

pub fn new_skolem(&self, name: Symbol, kind: ArcKind) -> RcType

pub fn zonk(&self, typ: &RcType) -> RcType

pub fn bind_arc(&self, typ: &RcType) -> ArcType

Trait Implementations

impl<T> Default for Substitution<T> where
    T: Substitutable,
    T::Factory: Default,
    T::Interner: Default, 

fn default() -> Substitution<T>

Returns the "default value" for a type.

impl<T> Debug for Substitution<T> where
    T: Debug + Substitutable, 

fn fmt(&self, f: &mut Formatter) -> Result

Formats the value using the given formatter.

impl<T> TypeContext<Symbol, T> for Substitution<T> where
    T: Substitutable + From<Type<Symbol, T>>,
    &'a T::Interner: TypeContext<Symbol, T>, 

fn intern(&mut self, typ: Type<Symbol, T>) -> T

fn builtin(&mut self, typ: BuiltinType) -> T

fn forall(&mut self, params: Vec<Generic<Symbol>>, typ: T) -> T

fn with_forall(&mut self, typ: T, from: &T) -> T where
    Symbol: Clone + Eq + Hash,
    T: TypeExt<Id = Symbol> + Clone, 

fn array(&mut self, typ: T) -> T

fn app(&mut self, id: T, args: AppVec<T>) -> T

fn variant(&mut self, fields: Vec<Field<Symbol, T>>) -> T

fn poly_variant(&mut self, fields: Vec<Field<Symbol, T>>, rest: T) -> T

fn effect(&mut self, fields: Vec<Field<Symbol, T>>) -> T

fn poly_effect(&mut self, fields: Vec<Field<Symbol, T>>, rest: T) -> T

fn record(
    &mut self,
    types: Vec<Field<Symbol, Alias<Symbol, T>>>,
    fields: Vec<Field<Symbol, T>>
) -> T

fn poly_record(
    &mut self,
    types: Vec<Field<Symbol, Alias<Symbol, T>>>,
    fields: Vec<Field<Symbol, T>>,
    rest: T
) -> T

fn extend_row(
    &mut self,
    types: Vec<Field<Symbol, Alias<Symbol, T>>>,
    fields: Vec<Field<Symbol, T>>,
    rest: T
) -> T

fn generic(&mut self, typ: Generic<Symbol>) -> T

fn skolem(&mut self, typ: Skolem<Symbol>) -> T

fn variable(&mut self, typ: TypeVariable) -> T

fn alias(&mut self, name: Symbol, args: Vec<Generic<Symbol>>, typ: T) -> T

fn ident(&mut self, id: Symbol) -> T

fn projection(&mut self, id: AppVec<Symbol>) -> T

fn builtin_type(&mut self, typ: BuiltinType) -> T

fn new_alias(
    &mut self,
    name: Symbol,
    args: Vec<Generic<Symbol>>,
    typ: T
) -> Alias<Symbol, T>

fn new_data_alias(&mut self, data: AliasData<Symbol, T>) -> Alias<Symbol, T>

fn alias_group(
    &mut self,
    group: Vec<AliasData<Symbol, T>>
) -> Vec<Alias<Symbol, T>>

fn hole(&mut self) -> T

fn opaque(&mut self) -> T

fn error(&mut self) -> T

fn array_builtin(&mut self) -> T

fn empty_row(&mut self) -> T

fn function_builtin(&mut self) -> T

fn string(&mut self) -> T

fn char(&mut self) -> T

fn byte(&mut self) -> T

fn int(&mut self) -> T

fn float(&mut self) -> T

fn unit(&mut self) -> T

fn tuple<S, I>(&mut self, symbols: &mut S, elems: I) -> T where
    I: IntoIterator<Item = T>,
    S: IdentEnv<Ident = Id> + ?Sized, 

fn tuple_<S, I>(&mut self, symbols: &mut S, elems: I) -> Type<Id, T> where
    I: IntoIterator<Item = T>,
    S: IdentEnv<Ident = Id> + ?Sized, 

fn function<I>(&mut self, args: I, ret: T) -> T where
    I: IntoIterator<Item = T>,
    T: Clone,
    <I as IntoIterator>::IntoIter: DoubleEndedIterator,
    <<I as IntoIterator>::IntoIter as Iterator>::Item == T, 

fn function_implicit<I>(&mut self, args: I, ret: T) -> T where
    I: IntoIterator<Item = T>,
    <I as IntoIterator>::IntoIter: DoubleEndedIterator,
    <<I as IntoIterator>::IntoIter as Iterator>::Item == T, 

fn function_type<I>(&mut self, arg_type: ArgType, args: I, ret: T) -> T where
    I: IntoIterator<Item = T>,
    <I as IntoIterator>::IntoIter: DoubleEndedIterator,
    <<I as IntoIterator>::IntoIter as Iterator>::Item == T, 

impl<'a, T> TypeContext<Symbol, T> for &'a Substitution<T> where
    T: Substitutable + From<Type<Symbol, T>>,
    &'a T::Interner: TypeContext<Symbol, T>, 

fn intern(&mut self, typ: Type<Symbol, T>) -> T

fn builtin(&mut self, typ: BuiltinType) -> T

fn forall(&mut self, params: Vec<Generic<Symbol>>, typ: T) -> T

fn with_forall(&mut self, typ: T, from: &T) -> T where
    Symbol: Clone + Eq + Hash,
    T: TypeExt<Id = Symbol> + Clone, 

fn array(&mut self, typ: T) -> T

fn app(&mut self, id: T, args: AppVec<T>) -> T

fn variant(&mut self, fields: Vec<Field<Symbol, T>>) -> T

fn poly_variant(&mut self, fields: Vec<Field<Symbol, T>>, rest: T) -> T

fn effect(&mut self, fields: Vec<Field<Symbol, T>>) -> T

fn poly_effect(&mut self, fields: Vec<Field<Symbol, T>>, rest: T) -> T

fn record(
    &mut self,
    types: Vec<Field<Symbol, Alias<Symbol, T>>>,
    fields: Vec<Field<Symbol, T>>
) -> T

fn poly_record(
    &mut self,
    types: Vec<Field<Symbol, Alias<Symbol, T>>>,
    fields: Vec<Field<Symbol, T>>,
    rest: T
) -> T

fn extend_row(
    &mut self,
    types: Vec<Field<Symbol, Alias<Symbol, T>>>,
    fields: Vec<Field<Symbol, T>>,
    rest: T
) -> T

fn generic(&mut self, typ: Generic<Symbol>) -> T

fn skolem(&mut self, typ: Skolem<Symbol>) -> T

fn variable(&mut self, typ: TypeVariable) -> T

fn alias(&mut self, name: Symbol, args: Vec<Generic<Symbol>>, typ: T) -> T

fn ident(&mut self, id: Symbol) -> T

fn projection(&mut self, id: AppVec<Symbol>) -> T

fn builtin_type(&mut self, typ: BuiltinType) -> T

fn new_alias(
    &mut self,
    name: Symbol,
    args: Vec<Generic<Symbol>>,
    typ: T
) -> Alias<Symbol, T>

fn new_data_alias(&mut self, data: AliasData<Symbol, T>) -> Alias<Symbol, T>

fn alias_group(
    &mut self,
    group: Vec<AliasData<Symbol, T>>
) -> Vec<Alias<Symbol, T>>

fn hole(&mut self) -> T

fn opaque(&mut self) -> T

fn error(&mut self) -> T

fn array_builtin(&mut self) -> T

fn empty_row(&mut self) -> T

fn function_builtin(&mut self) -> T

fn string(&mut self) -> T

fn char(&mut self) -> T

fn byte(&mut self) -> T

fn int(&mut self) -> T

fn float(&mut self) -> T

fn unit(&mut self) -> T

fn tuple<S, I>(&mut self, symbols: &mut S, elems: I) -> T where
    I: IntoIterator<Item = T>,
    S: IdentEnv<Ident = Id> + ?Sized, 

fn tuple_<S, I>(&mut self, symbols: &mut S, elems: I) -> Type<Id, T> where
    I: IntoIterator<Item = T>,
    S: IdentEnv<Ident = Id> + ?Sized, 

fn function<I>(&mut self, args: I, ret: T) -> T where
    I: IntoIterator<Item = T>,
    T: Clone,
    <I as IntoIterator>::IntoIter: DoubleEndedIterator,
    <<I as IntoIterator>::IntoIter as Iterator>::Item == T, 

fn function_implicit<I>(&mut self, args: I, ret: T) -> T where
    I: IntoIterator<Item = T>,
    <I as IntoIterator>::IntoIter: DoubleEndedIterator,
    <<I as IntoIterator>::IntoIter as Iterator>::Item == T, 

fn function_type<I>(&mut self, arg_type: ArgType, args: I, ret: T) -> T where
    I: IntoIterator<Item = T>,
    <I as IntoIterator>::IntoIter: DoubleEndedIterator,
    <<I as IntoIterator>::IntoIter as Iterator>::Item == T, 

impl<'a> Substitution<Symbol, ArcType<Symbol>> for &'a Substitution<RcType>

fn new_var(&mut self) -> RcType

fn new_skolem(&mut self, name: Symbol, kind: ArcKind) -> RcType