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 point applies to dependent records.

Implementations

impl<'a> Evaluator<'a>

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

impl<'a> Evaluator<'a>

pub fn empty(toplevel: &'a Toplevel) -> Self

Constructs a new Evaluator with empty environment.

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

Return a new Evaluator with environment env.

pub fn eval_ty(&self, ty: &BaseTyS) -> BaseTyV

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: &BaseTmS) -> BaseTmV

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: &BaseTmV, field_name: FieldName, field_label: LabelSegment, ) -> BaseTmV

Compute the projection of a field from a term value.

pub fn field_ty( &self, ty: &BaseTyV, val: &BaseTmV, field_name: FieldName, ) -> BaseTyV

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

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

Bind a new neutral of type ty.

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

Bind a variable called “self” to ty.

pub fn quote_ty(&self, ty: &BaseTyV) -> BaseTyS

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 BaseTyV 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) -> BaseTmS

Produce term syntax from a neutral term.

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

pub fn quote_tm(&self, tm: &BaseTmV) -> BaseTmS

Produce term syntax from a term value.

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

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

Check if ty1 is a subtype of ty2.

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

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

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

Precondition: the type of tm must be convertible 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 convertible_ty<'b>( &self, ty1: &BaseTyV, ty2: &BaseTyV, ) -> Result<(), D<'b>>

Check if two types are convertible.

Ignores specializations: specializations are handled in Evaluator::subtype.

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

pub fn eta_neu(&self, n: &TmN, ty: &BaseTyV) -> BaseTmV

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

pub fn eta(&self, v: &BaseTmV, ty: Option<&BaseTyV>) -> BaseTmV

Performs eta-expansion of the term v at type ty.

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

Check if two terms are definitionally equal.

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

Assumes that the type of tm1 is convertible with the 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 path_ty( &self, ty: &BaseTyV, val: &BaseTmV, path: &[(FieldName, LabelSegment)], ) -> Result<BaseTyV, String>

Walk path from the value val of record type ty, returning the type of the field at the end of the path.

An empty path returns ty unchanged. Each segment requires the current type to be a record containing the named field.

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

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

Precondition: path is non-empty.

pub fn fiber_field_ty( &self, ty: &FiberTyV, field: FieldName, ) -> Option<FiberTyV>

The fiber type of field field of a fiber record type, if present.

Only Over generator fields are ever projected (as we.e); their types are closed, so this is a plain lookup with no environment.

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

Check that two fiber types are convertible.

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

Check that two fiber terms are equal. Fiber terms are all neutral, so this is structural.

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.