Struct Sem 

pub struct Sem<'a> {
    pub k: &'a mut Kernel,
    pub st: &'a mut State,
}

The engine: the kernel (environment, stores, well-known names) and the session state.

Fields

k: &'a mut Kernel

st: &'a mut State

Implementations

impl Sem<'_>

pub fn is_def_eq(&mut self, t: V, s: V) -> KResult<bool>

t ≡ s.

pub fn is_def_eq_within( &mut self, t: V, s: V, steps: u32, ) -> KResult<Option<bool>>

t ≡ s, if it is decided within steps conversion steps and the checker’s resources; None if not. An attempt is speculation: running out — of steps, or of recursion depth, which a step does not bound — leaves it undecided, never declined, and nothing is learned from it but what it proved along the way.

pub fn proof_positions(&mut self, ty: V) -> KResult<u64>

The positions of a Π telescope whose binder types are propositions.

impl Sem<'_>

pub fn const_type(&mut self, n: NameId, ls: LevelsId) -> KResult<V>

The type of constant n at universe levels ls.

pub fn eval(&mut self, env: EnvId, e: ExprId) -> KResult<V>

Evaluates e in env.

pub fn apply(&mut self, f: V, a: V) -> KResult<V>

f a.

pub fn instantiate(&mut self, clo: V, x: V) -> KResult<V>

The body of a closure applied to x: a lambda’s body, a Π’s codomain.

impl Sem<'_>

pub fn infer( &mut self, env: EnvId, ctx: CtxId, e: ExprId, check: bool, ) -> KResult<V>

The type of e, whose bound variables have the values env and the types ctx (an empty context means “the types of the values”).

impl Sem<'_>

pub fn type_of(&mut self, v: V) -> KResult<V>

The type of v.

pub fn is_prop(&mut self, ty: V) -> KResult<bool>

Whether the type ty lives in Prop.

pub fn signature( &mut self, c: NameId, ls: LevelsId, ) -> KResult<Option<Signature>>

The Signature of c.{ls}, computed once per settled constant and instantiation and shared by every later declaration; None for a constant only provisionally in the environment, or one given the wrong number of universes, whose applications’ types must be inferred.

impl Sem<'_>

pub fn whnf_core(&mut self, v: V, cheap_proj: bool) -> KResult<V>

Weak-head normal form without δ. With cheap_proj, a projection’s structure is only brought to whnf_core (not unfolded), as Lean’s whnfCore does inside conversion.

pub fn unfold(&mut self, v: V) -> KResult<Option<V>>

One δ-step: the definition at the head of v unfolded and applied to the arguments.

pub fn whnf(&mut self, v: V) -> KResult<V>

Full weak-head normal form.

impl<'a> Sem<'a>

pub fn new(k: &'a mut Kernel, st: &'a mut State) -> Sem<'a>

pub fn under<T>( &mut self, ty: V, f: impl FnOnce(&mut Self, V) -> KResult<T>, ) -> KResult<T>

Runs f under a fresh variable of type ty.

pub fn check_type(&mut self, ty: ExprId) -> KResult<LevelId>

Checks that the closed term ty is a type; its universe level.

pub fn check_value(&mut self, value: ExprId, ty: ExprId) -> KResult<()>

Checks the closed term value against the closed, already checked type ty.

pub fn show(&mut self, v: V) -> String

A one-line description of a value, for diagnostics.