Enum fungi_lang::decide::RelCtx

pub enum RelCtx {
    Empty,
    Ctx(Ctx),
    NVarEquiv(RelCtxRec, Var, Var, Sort),
    NVarApart(RelCtxRec, Var, Var, Sort),
    IVarEquiv(RelCtxRec, Var, Var, Sort),
    IVarApart(RelCtxRec, Var, Var, Sort),
    PropTrue(RelCtxRec, Prop),
    TVarRelated(RelCtxRec, Var, Var),
}

Relational typing context: Relates pairs of variables, terms, etc

Variants

Empty

Basecase 1: empty context

Ctx(Ctx)

Basecase 2: Non-relational typing context

NVarEquiv(RelCtxRec, Var, Var, Sort)

Assume a name variable equivalence, at a common sort

NVarApart(RelCtxRec, Var, Var, Sort)

Assume a name variable apartness, at a common sort

IVarEquiv(RelCtxRec, Var, Var, Sort)

Assume an index variable equivalence, at a common sort

IVarApart(RelCtxRec, Var, Var, Sort)

Assume an index variable apartness, at a common sort

PropTrue(RelCtxRec, Prop)

Assume a proposition is true

TVarRelated(RelCtxRec, Var, Var)

Type variables are related: TODO: Kinds?

Methods

impl RelCtx

pub fn prop_true(&self, p: Prop) -> Self

pub fn add_tvars(&self, a: Var, b: Var) -> Self

pub fn add_ivars(&self, a: Var, b: Var, g: Sort) -> Self

pub fn ivar(&self, a: Var, b: Var, g: Sort) -> Self

pub fn nt_eq(&self, n1: &Var, n2: &Var, g: &Sort) -> Self

pub fn lookup_type_def(&self, x: &Var) -> Option<Type>

pub fn rest(&self) -> Option<RelCtxRec>

pub fn lookup_tvars(&self, x1: &Var, x2: &Var) -> bool

pub fn lookup_nvareq(&self, x1: &Var, x2: &Var, g: &Sort) -> bool

pub fn lookup_ivareq(&self, x1: &Var, x2: &Var, g: &Sort) -> bool

pub fn lookup_nvarapart(&self, x1: &Var, x2: &Var, g: &Sort) -> bool

pub fn lookup_bitype_ctx(&self) -> Ctx

pub fn lookup_ivarapart(&self, x1: &Var, x2: &Var, g: &Sort) -> bool

Trait Implementations

impl Display for RelCtx

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

Formats the value using the given formatter.

impl Clone for RelCtx

fn clone(&self) -> RelCtx

Returns a copy of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for RelCtx

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

Formats the value using the given formatter.

impl Eq for RelCtx

impl PartialEq for RelCtx

fn eq(&self, other: &RelCtx) -> bool

This method tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &RelCtx) -> bool

This method tests for !=.

impl Hash for RelCtx

fn hash<__H: Hasher>(&self, state: &mut __H)

Feeds this value into the given [Hasher].

fn hash_slice<H>(data: &[Self], state: &mut H) where     H: Hasher,

Feeds a slice of this type into the given [Hasher].