Crate kontroli

Type checking for the lambda-Pi calculus modulo rewriting.

This is the library underlying the Kontroli proof checker.

Usage

Users communicate with Kontroli using commands. A command either introduces of a new name (by declaration, definition, or theorem), or adds a rewrite rule. The state of a Kontroli typechecking session consists of a Symbols table, keeping track of all previously introduced names, and a Signature, recording types and rewrite rules attached to symbols.

How is a user command processed? A command is parsed from a string to yield a parse command. The scoping operation then refines the parse command to a scope command, verifying whether the names referenced in the parse command have been previously declared in the Symbols table. Once we have a scope command, we distinguish whether it introduces a name or adds a rewrite rule: In case of a rewrite rule, we add the rewrite rule to the signature. In case of a name introduction, we first update the Symbols table with the newly introduced name and verify that the given types and terms are valid, yielding a Typing. Once we have a typing, we add it to the signature.

This whole process is illustrated in the following image. The Symbols and Signature are boxed to indicate that they persist throughout the checking.

The following example parses a few commands and executes them on a signature. (By the way, this example, just as all other code examples in this library, can be executed by running cargo test.)

let cmds = [
    // declarations
    "prop : Type.\n",
    "imp : prop -> prop -> prop.\n",

    // definition with a rewrite rule
    "def proof : prop -> Type.\n",
    "[x, y] proof (imp x y) --> proof x -> proof y.\n",

    // theorem
    r"thm imp_refl (x : prop) : proof (imp x x) := p : proof x => p.\n",
];

let arena = Arena::new();
let mut syms = Symbols::new();
let mut sig = Signature::new();

for c in cmds.iter() {
    // parse and scope command in one go
    let cmd: Command<String> = Command::parse(c, &syms)?;
    match cmd {
        // introduction of a new name
        Command::Intro(id, it) => {
            let id: &str = arena.alloc(id);
            // add symbol to symbol table and fail if it is not new
            let sym = syms.insert(id)?;

            // typecheck and insert into signature
            let typing: Typing = Typing::new(Intro::from(it), &sig)?.check(&sig)?;
            sig.insert(sym, typing)?
        }
        // addition of rewrite rules
        Command::Rules(rules) => sig.add_rules(rules.into_iter().map(Rule::from))?
    }
}

Organisation

This library is divided into several modules:

• The parse module contains unshared, reference-free data structures,
• the scope module contains data structures with references, and
• the rc and arc modules contain data structures with references and shared pointers.

The rc and arc modules expose completely the same API, the difference being that the structures in rc cannot be used in multi-threaded scenarios. Due to the performance overhead incurred by the data structures in arc, it is advisable to use these only in multi-threaded scenarios, and to prefer rc whenever possible.

For many data structures, we have counterparts in the parse, scope, and rc/arc modules. We call types from the parse and scope modules "parse structures" and "scope structures", respectively. For example, we distinguish parse terms, scope terms, and terms (the latter being defined in the rc/arc modules). Parse structures are constructed by the parser and refined into their corresponding scope structures by the scoper. Parse and scope structures also implement the Send and Sync traits, meaning that they can be transferred and shared between threads. This allows parsing and checking to be performed in parallel.

Re-exports

pub use error::Error;

Modules

arc	Multi-threading kernel.
error	Common error type.
parse	Parsing to unshared, reference-free data structures.
rc	Single-threading kernel.
scope	Scoping of parse structures to data structures with references.

Structs

Application	Application of a list of arguments to a symbol.
Arg	Argument of a binder. For example, the x and A in the term \ x : A => t.
Rule	Rewrite rule.
Signature	Map from symbols to their associated types and rewrite rules.
Stack	A Vec that is iterated from the last to the first pushed element.
Typing	Normalised, verified form of introduction commands.

Enums

Command	Signature-changing command.
Intro	The way we introduce a new name.
Pattern	Rewrite pattern.
Term	Term for the lambda-Pi calculus.