oxilean-elab

Elaborator for the OxiLean theorem prover

The elaborator translates surface syntax (from the parser) into kernel-checked terms. It handles type inference, implicit argument insertion, unification, pattern match compilation, and tactic execution. This crate is untrusted -- the kernel independently verifies all produced terms.

92,415 SLOC -- fully implemented elaboration pipeline (466 source files, 3,165 tests passing).

Architecture

Surface AST (from oxilean-parse)
    |
    v
+------------------------------------------+
|              Elaborator                   |
|                                           |
|  +---------------+    +---------------+   |
|  |  Meta-vars    |<---|  Unification  |   |
|  | (metavar.rs)  |    |  (unify.rs)   |   |
|  +------+--------+    +-------+-------+   |
|         |                     |           |
|  +------v---------------------v------+    |
|  |    Expression Elaboration         |    |
|  |      (elab_expr.rs)               |    |
|  +------+----------------------------+    |
|         |                                 |
|  +------v----------------------------+    |
|  |    Declaration Elaboration        |    |
|  |      (elab_decl.rs)               |    |
|  +------+----------------------------+    |
|         |                                 |
|  +------v----------------------------+    |
|  |       Tactic Engine               |    |
|  |     (tactic/mod.rs)               |    |
|  +-----------------------------------+    |
+------------------------------------------+
    |
    v
Kernel Expr terms -> sent to oxilean-kernel for verification

Module Overview

Key Concepts

Meta-variables

Meta-variables (?m) represent "holes" in partially-constructed terms. The elaborator creates metavariables for:

• Implicit arguments ({alpha : Type} -> insert ?alpha)
• User-written holes (_)
• Tactic goals

Metavariables are never sent to the kernel -- they must all be resolved during elaboration.

Unification

Given ?m x1 ... xn =? t, the unifier finds assignments for ?m. Strategies:

1. First-order: ?m =? t where ?m not in t -> assign ?m := t
2. Pattern (Miller): ?m x1 ... xn =? t where xi are distinct FVars -> ?m := fun x1...xn. t
3. Postponement: when unification cannot proceed, delay and retry later

Implicit Argument Insertion

When applying f : {alpha : Type} -> alpha -> alpha to an argument a:

1. Create metavariable ?alpha for the implicit parameter
2. Apply: f ?alpha a
3. Unification determines ?alpha from context

Tactic Engine

Tactics operate on a TacticState containing goals:

struct TacticState {
    goals: Vec<Goal>,
    env: Environment,
    assignments: MetaContext,
}

struct Goal {
    mvar: MetaVarId,       // the hole to fill
    lctx: Vec<LocalDecl>,  // local hypotheses
    target: Expr,          // what needs to be proved
}

Core Tactics

Dependencies

• oxilean-kernel -- for Expr, Name, Level, Environment types
• oxilean-parse -- for surface AST types

Testing

cargo test -p oxilean-elab

License

Copyright COOLJAPAN OU (Team Kitasan). Apache-2.0 -- See LICENSE for details.