Struct kontroli::Typing

pub struct Typing<T> {
    pub typ: T,
    pub term: Option<(T, Check)>,
    pub rewritable: bool,
}

Normalised, verified form of introduction commands.

An introduction command can have many shapes: x: A, x := t, x: A := t, ... A typing provides a uniform presentation of introduction commands with respect to type checking.

Fields

typ: T

term: Option<(T, Check)>

rewritable: bool

Implementations

impl<'s> Typing<RTerm<'s>>

pub fn declare(
    typ: RTerm<'s>,
    rewritable: bool,
    sig: &Signature<'s>
) -> Result<Self, Error>

pub fn define(
    oty: Option<RTerm<'s>>,
    term: RTerm<'s>,
    rewritable: bool,
    sig: &Signature<'s>
) -> Result<Self, Error>

pub fn check(self, sig: &Signature<'s>) -> Result<Self, Error>

Verify whether t: A if this was not previously checked.

Return a typing registering that t: A has been checked.

pub fn new(it: Intro<'s>, sig: &Signature<'s>) -> Result<Self, Error>

Construct a typing from an introduction command.

An introduction command can have many shapes, such as x: A, x := t, x: A := t, ... The type A of the newly introduced symbol is (a) inferred from its defining term t if not given and (b) verified to be of a proper sort. In case a defining term t is given, t is registered, along with the information whether the type A was inferred from it.

Constructing a typing from a command of the shape x: A := t does not check whether t: A. For this, the check function can be used. This allows us to postpone and parallelise type checking.

impl<'s> Typing<RTerm<'s>>

pub fn declare(
    typ: RTerm<'s>,
    rewritable: bool,
    sig: &Signature<'s>
) -> Result<Self, Error>

pub fn define(
    oty: Option<RTerm<'s>>,
    term: RTerm<'s>,
    rewritable: bool,
    sig: &Signature<'s>
) -> Result<Self, Error>

pub fn check(self, sig: &Signature<'s>) -> Result<Self, Error>

Verify whether t: A if this was not previously checked.

Return a typing registering that t: A has been checked.

pub fn new(it: Intro<'s>, sig: &Signature<'s>) -> Result<Self, Error>

Construct a typing from an introduction command.

An introduction command can have many shapes, such as x: A, x := t, x: A := t, ... The type A of the newly introduced symbol is (a) inferred from its defining term t if not given and (b) verified to be of a proper sort. In case a defining term t is given, t is registered, along with the information whether the type A was inferred from it.

Constructing a typing from a command of the shape x: A := t does not check whether t: A. For this, the check function can be used. This allows us to postpone and parallelise type checking.

Trait Implementations

impl<T: Clone> Clone for Typing<T>

fn clone(&self) -> Typing<T>

Returns a copy of the value.

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

Performs copy-assignment from source.