Struct Evaluator

pub struct Evaluator<'a> { /* private fields */ }

The context used in evaluation, quoting, and conversion checking

We bundle this all together because conversion checking and quoting sometimes need to evaluate terms. For instance, quoting a lambda involves evaluating the body of the lambda in the context of a freshly introduced variable; even though we don’t have lambdas, a similar thing applies to dependent records.

Implementations

impl<'a> Evaluator<'a>

pub fn new(toplevel: &'a Toplevel, env: Env, scope_length: usize) -> Self

Constructor for Evaluator

pub fn with_env(&self, env: Env) -> Self

Return a new Evaluator with environment env

pub fn eval_ty(&self, ty: &TyS) -> TyV

Evaluate type syntax to produce a type value

Assumes that the type syntax is well-formed and well-scoped with respect to self.env

pub fn eval_tm(&self, tm: &TmS) -> TmV

Evaluate term syntax to produce a term value

Assumes that the term syntax is well-formed and well-scoped with respect to self.env

pub fn proj( &self, tm: &TmV, field_name: FieldName, field_label: LabelSegment, ) -> TmV

Compute the projection of a field from a term value

pub fn field_ty(&self, ty: &TyV, val: &TmV, field_name: FieldName) -> TyV

Evaluate the type of the field field_name of val : ty.

pub fn bind_neu( &self, name: VarName, label: LabelSegment, ty: TyV, ) -> (TmN, Self)

Bind a new neutral of type ty

pub fn bind_self(&self, ty: TyV) -> (TmN, Self)

Bind a variable called “self” to ty

pub fn quote_ty(&self, ty: &TyV) -> TyS

Produce type syntax from a type value.

This is a section of eval, in that self.eval_ty(self.quote_ty(ty_v)) == ty_v but it is not necessarily true that self.quote_ty(self.eval_ty(ty_s)) == ty_v.

This is used for displaying TyV to the user in type errors, and for creating syntax that can be re-evaluated in other contexts. In theory this could be used for conversion checking, but it’s more efficient to implement that directly, and it’s better to not do eta-expansion for user-facing messages or for syntax that is meant to be re-evaluated.

pub fn quote_neu(&self, n: &TmN) -> TmS

Produce term syntax from a term neutral.

The documentation for Evaluator::quote_ty is also applicable here.

pub fn quote_tm(&self, tm: &TmV) -> TmS

Produce term syntax from a term value.

The documentation for Evaluator::quote_ty is also applicable here.

pub fn subtype<'b>(&self, ty1: &TyV, ty2: &TyV) -> Result<(), D<'b>>

Check if ty1 is a subtype of ty2.

This is true iff ty1 is convertable with ty2, and an eta-expanded neutral of type ty1 is an element of ty2.

pub fn element_of<'b>(&self, tm: &TmV, ty: &TyV) -> Result<(), D<'b>>

Check if tm is an element of ty, accounting for specializations of ty.

Precondition: the type of tm must be convertable with ty, and tm is eta-expanded.

Example: if a : Entity and b : Entity are neutrals, then a is not an element of @sing b, but a is an element of @sing a.

pub fn convertable_ty<'b>(&self, ty1: &TyV, ty2: &TyV) -> Result<(), D<'b>>

Check if two types are convertable.

Ignores specializations: specializations are handled in Evaluator::subtype

On failure, returns a doc which describes the obstruction to convertability.

pub fn eta_neu(&self, n: &TmN, ty: &TyV) -> TmV

Performs eta-expansion of the neutral n at type ty.

pub fn eta(&self, v: &TmV, ty: &TyV) -> TmV

Performs eta-expansion of the term n at type ty

pub fn equal_tm<'b>(&self, tm1: &TmV, tm2: &TmV) -> Result<(), D<'b>>

Check if two terms are definitionally equal.

On failure, returns a doc which describes the obstruction to convertability.

Assumes that the base type of tm1 is convertable with the base type of tm2. First attempts to do conversion checking without eta-expansion (strict mode), and if that fails, does conversion checking with eta-expansion.

pub fn try_specialize( &self, ty: &TyV, path: &[(FieldName, LabelSegment)], field_ty: TyV, ) -> Result<TyV, String>

Try to specialize the record r with the subtype ty at path

Precondition: path is non-empty.

Trait Implementations

impl<'a> Clone for Evaluator<'a>

fn clone(&self) -> Evaluator<'a>

Returns a duplicate of the value.

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

Performs copy-assignment from source.