Struct Kernel 

pub struct Kernel {
    pub s: Store,
    pub env: Env,
    pub wk: WellKnown,
    pub engine: Engine,
    pub probe_steps: u32,
    pub theory: Theory,
    /* private fields */
}

A kernel is plain data (its only shared cells are immutable: interned strings and admitted constants), so a clone is an independent kernel; mirror keeps one as a snapshot to branch from.

Fields

s: Store

env: Env

wk: WellKnown

engine: Engine

Which judgment admits definitions, theorems, opaques and axioms.

probe_steps: u32

The steps the value engine lets one argument pair of a same-head comparison take before it unfolds the definitions instead (see sem::conv): conversion steps and δ-unfolding steps both spend it. It changes what conversion costs, never what it answers.

theory: Theory

The type theory this kernel checks.

Implementations

impl Kernel

pub fn check_name(&self, n: NameId, allow_primitive: bool) -> KResult<()>

pub fn check_duplicate_lparams(&self, ps: &[NameId]) -> KResult<()>

pub fn with_decl<T>( &mut self, lparams: Rc<[NameId]>, safety: Safety, f: impl FnOnce(&mut Kernel) -> KResult<T>, ) -> KResult<T>

Runs f as one declaration’s check: fresh caches and local context, scratch memory released afterwards whatever the outcome.

pub fn may_trust(&self, d: &Decl) -> bool

Whether d may be admitted unchecked in a trusted-prefix run (see super::export::Observe::trust_before): anything but a primitive or the quotient.

pub fn may_trust_block(&self, claimed: &[Const]) -> bool

Whether an inductive block declaring claimed may be admitted unchecked: none of its constants is a primitive.

pub fn admit_trusted(&mut self, d: Decl)

Admits d as the export states it, without checking it (trusted-prefix runs only).

pub fn admit_trusted_block(&mut self, claimed: Vec<Const>)

Admits an inductive block’s constants as the export states them, without checking them (trusted-prefix runs only).

pub fn add_decl(&mut self, decl: Decl) -> KResult<()>

pub fn const_levels_of(&mut self, ps: &[NameId]) -> LevelsId

pub fn is_sort(&self, e: ExprId) -> bool

impl Kernel

pub fn add_inductive( &mut self, decl: InductiveDecl, claimed: Vec<Const>, ) -> KResult<()>

Admits an inductive family whose declarations an export claims are claimed.

impl Kernel

pub fn logos(ctx: &Context) -> Kernel

A kernel for LOGOS’s theory over the declarations of ctx.

impl Kernel

pub fn check_primitive_def(&mut self, d: &DefnDecl) -> KResult<bool>

Returns whether d may take a primitive name (Lean’s checkPrimitiveDef), and records a primitive whose equations check as computed natively (validated_primitives).

In LOGOS’s theory a primitive’s name refuses nothing: a definition that does not check as the primitive is an ordinary one, computed by unfolding, and its literal rules read Zero and Succ only while they are Nat’s constructors (Kernel::reads_nat_literal). So a definition named Succ is admitted, and an impostor Nat.div is not computed natively.

impl Kernel

pub fn ignorable_args(&mut self, c: NameId, ls: LevelsId) -> KResult<u64>

The argument positions of c.{ls} whose arguments need not be compared (see the module documentation). Zero for anything that is not a settled, unfoldable definition.

pub fn absent_mask(&mut self, c: NameId, ls: LevelsId) -> Option<u64>

The positions c’s value never mentions, or None when c.{ls} is not a settled, unfoldable definition (whose arguments must then all be compared).

impl Kernel

pub fn with_sem<T>( &mut self, f: impl FnOnce(&mut Sem<'_>) -> KResult<T>, ) -> KResult<T>

Runs the value engine on this kernel with its session state.

pub fn sem_epoch(&self) -> u64

Changes whenever something already evaluated may now mean something else: the quotient reductions were switched on, or a primitive was validated (its literal extension switched on). The value engine’s session never spans two epochs.

A withdrawn declaration needs no epoch: only a provisional declaration is ever withdrawn, and a session that touches one is marked (scratch_seen) and ends with its declaration.

impl Kernel

pub fn new() -> Kernel

pub fn begin_decl(&mut self, lparams: Rc<[NameId]>, safety: Safety)

Starts checking one declaration: fresh local context, caches, and scratch region.

pub fn end_decl(&mut self)

pub fn memory_report(&self) -> Vec<(&'static str, usize)>

The store’s memory, plus the kernel’s own caches and environment.

pub fn set_safety(&mut self, safety: Safety)

pub fn push_local(&mut self, ty: ExprId, val: Option<ExprId>) -> ExprId

pub fn fvar_index(&self, e: ExprId) -> u32

pub fn mk_binding(&mut self, pi: bool, fvars: &[ExprId], body: ExprId) -> ExprId

mkForall/mkLambda over local declarations (lets become let).

pub fn mk_pi(&mut self, fvars: &[ExprId], body: ExprId) -> ExprId

pub fn mk_lambda(&mut self, fvars: &[ExprId], body: ExprId) -> ExprId

pub fn get_const(&self, n: NameId) -> KResult<Rc<Const>>

pub fn instantiate_type_lparams(&mut self, c: &Const, ls: LevelsId) -> ExprId

c’s type at universe arguments ls.

pub fn infer(&mut self, e: ExprId, infer_only: bool) -> KResult<ExprId>

pub fn sort_level(&self, s: ExprId) -> LevelId

pub fn ensure_sort(&mut self, e: ExprId) -> KResult<ExprId>

pub fn ensure_pi(&mut self, e: ExprId) -> KResult<ExprId>

pub fn get_sort_level(&mut self, e: ExprId) -> KResult<LevelId>

pub fn is_prop(&mut self, e: ExprId) -> KResult<bool>

e’s type is Prop.

pub fn check(&mut self, e: ExprId) -> KResult<ExprId>

Infers e’s type with full checking.

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

pub fn is_app_of_arity(&self, e: ExprId, n: NameId, arity: usize) -> bool

pub fn nat_lit_to_ctor(&mut self, n: &Nat) -> ExprId

pub fn str_lit_to_ctor(&mut self, sid: StrId) -> ExprId

pub fn unfold_definition(&mut self, e: ExprId) -> Option<ExprId>

pub fn reduce_nat(&mut self, e: ExprId) -> KResult<Option<ExprId>>

Lean’s reduceNat: Nat.succ and the GMP-accelerated binary operations on literals.

pub fn whnf(&mut self, e: ExprId) -> KResult<ExprId>

pub fn conforms(&mut self, actual: ExprId, expected: ExprId) -> KResult<bool>

Whether a term of type actual may stand where expected is required: definitional equality in Lean’s theory, cumulative subtyping in LOGOS’s.

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

pub fn unfold_steps(&self) -> u64

The δ-unfoldings this kernel’s weak-head reduction has taken: a primitive at literals computed natively takes none.

pub fn conversion_steps(&self) -> u64

The definitional-equality steps this kernel has taken (see conv_steps).

pub fn show(&self, e: ExprId) -> String

pub fn level_node(&self, l: LevelId) -> LevelNode

pub fn quot_kind(&self, n: NameId) -> Option<QuotKind>

Trait Implementations

impl Clone for Kernel

fn clone(&self) -> Kernel

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Default for Kernel

fn default() -> Self

Returns the “default value” for a type.