pub enum Constraint<T: Types> {
Pred(Pred<T>, Option<T::Tag>),
Conj(Vec<Self>),
ForAll(Bind<T>, Box<Self>),
}
Variants§
Implementations§
Source§impl<T: Types> Constraint<T>
impl<T: Types> Constraint<T>
pub const TRUE: Self
pub fn foralls(bindings: Vec<Bind<T>>, c: Self) -> Self
pub fn conj(cstrs: Vec<Self>) -> Self
Sourcepub fn is_concrete(&self) -> bool
pub fn is_concrete(&self) -> bool
Returns true if the constraint has at least one concrete RHS (“head”) predicates.
If !c.is_concrete
then c
is trivially satisfiable and we can avoid calling fixpoint.
Source§impl<T: Types> Constraint<T>
impl<T: Types> Constraint<T>
pub fn depth_first_fragments(&self) -> ConstraintFragments<'_, T> ⓘ
pub fn kvar_deps(&self) -> Vec<T::KVar>
pub fn kvar_mappings( &self, ) -> (HashMap<T::KVar, Vec<Constraint<T>>>, HashMap<T::KVar, Vec<T::KVar>>)
pub fn topo_order_fragments(&self) -> Vec<Self>
pub fn fragment_kvar_head(&self) -> Option<T::KVar>
pub fn sub_all_kvars( &self, assignments: &HashMap<T::KVar, Vec<(&Qualifier<T>, Vec<usize>)>>, ) -> Self
pub fn sub_kvars_except_head( &self, assignments: &HashMap<T::KVar, Vec<(&Qualifier<T>, Vec<usize>)>>, ) -> Self
pub fn sub_head(&self, assignment: &(&Qualifier<T>, Vec<usize>)) -> Self
pub fn scope(&self, var: &T::KVar) -> Self
fn scope_help(&self, var: &T::KVar) -> Option<Constraint<T>>
Source§impl Constraint<ParsingTypes>
impl Constraint<ParsingTypes>
pub fn uniquify(&mut self)
fn uniquify_help(&mut self, used_names: &mut HashMap<String, u32>)
fn rename(&mut self, from: &String, to: &String)
pub fn is_satisfiable(&self) -> bool
pub fn sol1( &self, var: &String, ) -> Vec<(Vec<Bind<ParsingTypes>>, Vec<Expr<ParsingTypes>>)>
pub fn elim(&self, vars: &Vec<String>) -> Self
pub fn elim1(&self, var: &String) -> Self
fn do_elim( &self, var: &String, solution: &Vec<(Vec<Bind<ParsingTypes>>, Vec<Expr<ParsingTypes>>)>, ) -> Self
Trait Implementations§
Source§impl<T: Types> Clone for Constraint<T>
impl<T: Types> Clone for Constraint<T>
Source§impl<T: Types> Debug for Constraint<T>
impl<T: Types> Debug for Constraint<T>
Auto Trait Implementations§
impl<T> Freeze for Constraint<T>
impl<T> RefUnwindSafe for Constraint<T>where
<T as Types>::KVar: RefUnwindSafe,
<T as Types>::Tag: RefUnwindSafe,
<T as Types>::Var: RefUnwindSafe,
<T as Types>::Decimal: RefUnwindSafe,
<T as Types>::String: RefUnwindSafe,
<T as Types>::Sort: RefUnwindSafe,
impl<T> Send for Constraint<T>
impl<T> Sync for Constraint<T>
impl<T> Unpin for Constraint<T>
impl<T> UnwindSafe for Constraint<T>where
<T as Types>::KVar: UnwindSafe,
<T as Types>::Tag: UnwindSafe,
<T as Types>::Var: UnwindSafe,
<T as Types>::Decimal: UnwindSafe,
<T as Types>::String: UnwindSafe,
<T as Types>::Sort: UnwindSafe,
Blanket Implementations§
Source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
impl<T> BorrowMut<T> for Twhere
T: ?Sized,
Source§fn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more
Source§impl<T> CloneToUninit for Twhere
T: Clone,
impl<T> CloneToUninit for Twhere
T: Clone,
Source§impl<T> IntoEither for T
impl<T> IntoEither for T
Source§fn into_either(self, into_left: bool) -> Either<Self, Self>
fn into_either(self, into_left: bool) -> Either<Self, Self>
Converts
self
into a Left
variant of Either<Self, Self>
if into_left
is true
.
Converts self
into a Right
variant of Either<Self, Self>
otherwise. Read moreSource§fn into_either_with<F>(self, into_left: F) -> Either<Self, Self>
fn into_either_with<F>(self, into_left: F) -> Either<Self, Self>
Converts
self
into a Left
variant of Either<Self, Self>
if into_left(&self)
returns true
.
Converts self
into a Right
variant of Either<Self, Self>
otherwise. Read more