Crate oxilean_elab

Expand description

§OxiLean Elaborator — From Surface Syntax to Typed Kernel Terms

The elaborator bridges the gap between user-written OxiLean code (surface syntax) and kernel-verified terms. It performs type inference, implicit argument resolution, unification, and tactic execution.

§Quick Start

§Elaborating an Expression

use oxilean_elab::{ElabContext, elaborate_expr};
use oxilean_kernel::Environment;

let env = Environment::new();
let ctx = ElabContext::new(&env);
let surface_expr = /* parsed from source */;
let (kernel_expr, ty) = elaborate_expr(&ctx, surface_expr)?;

§Elaborating a Declaration

use oxilean_elab::elaborate_decl;

let decl = /* parsed surface declaration */;
let elaborator = DeclElaborator::new(&ctx);
elaborator.elaborate(decl)?;

§Architecture Overview

The elaborator is a multi-stage system:

Surface Syntax AST (from parser)
    │
    ▼
┌───────────────────────────┐
│  Name Resolution          │  → Resolve names to definitions
│  (context.rs, elab_decl)  │  → Build local contexts
└───────────────────────────┘
    │
    ▼
┌───────────────────────────┐
│  Type Inference           │  → Synthesize types for unknowns
│  (infer.rs)               │  → Generate metavariables (?m)
└───────────────────────────┘
    │
    ▼
┌───────────────────────────┐
│  Implicit Arg Resolution  │  → Resolve {x} and [x]
│  (implicit.rs)            │  → Unify with inferred types
└───────────────────────────┘
    │
    ▼
┌───────────────────────────┐
│  Unification & Solving    │  → Solve metavariable constraints
│  (unify.rs, solver.rs)    │  → Higher-order unification
└───────────────────────────┘
    │
    ▼
┌───────────────────────────┐
│  Elaboration Passes       │  → Coercions, macros, tactics
│  (elaborate.rs)           │  → Build kernel terms
└───────────────────────────┘
    │
    ▼
Kernel Expressions (fully elaborated)
    │
    └─→ Kernel Type Checker (kernel TCB validates)
    └─→ Environment (if type-check passes)

§Key Concepts & Terminology

§Metavariables

Metavariables (?m, ?t, ?P) represent unknown terms during elaboration:

?m : τ = metavariable with type τ
Initially unsolved
Solved via unification constraints
Must be fully solved before kernel validation

Example:

User writes: let x := _ in x + 1
Elaborator creates: let x := ?m in x + 1
Constraint: ?m : Nat (inferred from context)
Solution: ?m = 5 (if inferrable from usage)
Final: let x := 5 in x + 1

§Type Inference

Bidirectional type checking:

Synthesis (↑): Infer type of expression expr ↑ τ
Checking (↓): Check expression against type expr ↓ τ

Example:

Synth: f x ↑ ?τ
  ├─ Synth: f ↑ (α → β)
  ├─ Check: x ↓ α
  └─ Result: β

Check: fun x => x + 1 ↓ Nat → Nat
  ├─ Expect x : Nat
  └─ Check: x + 1 ↓ Nat

§Implicit Arguments

Arguments can be:

Explicit (x : T): Must be provided by user
Implicit {x : T}: Inferred from context
Instance [C x]: Filled by typeclass resolution

The elaborator inserts placeholder metavariables for implicit args, then solves them via unification.

§Unification

Solves constraints of the form ?m =?= expr:

First-order: ?m = f x
Higher-order: ?f = λ x. ?body
Occurs check: Prevents infinite types like ?m = f ?m

§Elaboration Context

Manages state during elaboration:

Local variables: x : T in scope
Metavariables: Mapping from MetaVarId to assignment
Configuration: Options for tactics, coercions, etc.
Environment: Global definitions and axioms

§Module Organization

§Core Elaboration Modules

Module	Purpose
`context`	Elaboration context and local variable management
`metavar`	Metavariable creation and tracking
`infer`	Type synthesis and checking
`unify`	Higher-order unification algorithm

§Expression & Declaration Elaboration

Module	Purpose
`elaborate`	Main expression elaboration pipeline
`elab_decl`	Declaration (def, theorem, etc.) elaboration
`binder`	Binder (`fun`, `forall`) elaboration

§Argument Resolution

Module	Purpose
`implicit`	Implicit argument resolution and synthesis
`instance`	Typeclass instance resolution

§Advanced Features

Module	Purpose
`unify`	Higher-order unification
`solver`	Constraint solver
`coercion`	Type coercion insertion
`pattern_match`	Pattern matching elaboration
`mutual`	Mutual recursion validation
`equation`	Equation compiler (pattern matching)

§Tactics

Module	Purpose
`tactic`	Tactic engine and core tactics
`tactic::intro`	`intro` tactic (introduce binders)
`tactic::apply`	`apply` tactic (apply theorem)
`tactic::exact`	`exact` tactic (provide term directly)
`tactic::rw`	`rw` tactic (rewrite by equality)

§Utilities

Module	Purpose
`error_msg`	Error message formatting
`notation`	Notation expansion
`macro_expand`	Macro expansion
`attribute`	Attribute processing (e.g., `@[simp]`)
`derive`	Deriving instances (e.g., `Eq`, `Show`)
`trace`	Debug tracing

§Elaboration Pipeline Details

§Phase 1: Name Resolution

Converts surface names to qualified names:

Local variables: x → local index
Global constants: Nat.add → fully qualified path
Scoped opens: Apply namespace resolution
Shadowing: Inner scopes shadow outer

§Phase 2: Type Inference

Generates type constraints:

For each subexpression, create metavariable for unknown type
Collect unification constraints
Maintain bidirectional flow (synthesis ↑, checking ↓)

§Phase 3: Implicit Argument Synthesis

Fill in implicit arguments:

For each implicit parameter, create metavariable\
Pass to unification solver
Fails if multiple solutions or no solution\

§Phase 4: Unification & Solving

Solve all metavariable constraints:

Higher-order unification algorithm
Occurs check to prevent infinite terms
Backtracking for multiple solutions

§Phase 5: Term Construction

Build final kernel Expr:

Substitute metavars with solutions
Insert coercions where needed
Expand macros
Validate termination

§Phase 6: Tactic Execution (for proofs)

If proof is by <tactic>:

Execute tactic to transform goal
May generate new subgoals
Recursively elaborate subgoals\

§Phase 7: Kernel Validation

Pass to kernel type checker:

Independent verification
All metavars must be solved
Type check must succeed

§Usage Examples

§Example 1: Simple Expression

use oxilean_elab::{ElabContext, elaborate_expr};

let ctx = ElabContext::new(&env);
let expr = SurfaceExpr::app(
    SurfaceExpr::const_("Nat.add"),
    vec![SurfaceExpr::lit(5), SurfaceExpr::lit(3)],
);
let (kernel_expr, ty) = elaborate_expr(&ctx, expr)?;
// kernel_expr is now fully elaborated and type-checked

§Example 2: Function with Implicit Arguments

// User writes: myFunc x (where myFunc has implicit args)
// Elaborator infers and fills implicit args from context
let elaborate = elaborate_expr(&ctx, surface_expr)?;

§Example 3: Tactic-Based Proof

// User writes: theorem my_thm : P := by intro h; exact h
// Elaborator:
//   1. Creates goal: ⊢ P
//   2. Runs tactic: intro h
//   3. New goal: h : ⊢ P (with h in context)
//   4. Runs tactic: exact h
//   5. Constructs proof term

§Error Handling

Elaboration errors include:

Type mismatch: Expected type τ, got σ
Unification failure: Cannot unify terms
Unsolved metavariables: ?m remains after elaboration
Unknown identifier: Name not in scope
Ambiguous instance: Multiple typeclass instances match
Tactic error: Tactic failed or invalid in context\

All errors carry source location and helpful context messages.

§Tactic System

Tactics are proof-building procedures:

Interactive: In REPL or IDE
Automated: Called during elaboration

Core tactics:

intro: Introduce binders from goal type
apply: Apply theorem to goal
exact: Provide exact proof term
rw: Rewrite using equality
simp: Simplify using lemmas
cases: Case analysis on inductive type
induction: Inductive reasoning\

§Integration with Other Crates

§With oxilean-kernel

Uses kernel Expr, Environment, TypeChecker
Passes elaborated terms to kernel for validation
Kernel is never bypassed

§With oxilean-parse

Consumes SurfaceExpr, SurfaceDecl from parser
Converts to kernel types

§With oxilean-meta

Meta layer provides metavariable-aware operations
Extends kernel WHNF, DefEq, TypeInfer with metavar support

§Performance Considerations

Metavar allocation: O(1) arena insertion
Unification: O(expr_size) per constraint
Memoization: Avoid re-elaborating same subexpressions
Lazy evaluation: Defer expensive operations (normalization)\

§Further Reading

ARCHITECTURE.md — System architecture
Module documentation for specific subcomponents

Re-exports§

pub use attribute::apply_attributes;
pub use attribute::process_attributes;
pub use attribute::AttrEntry;
pub use attribute::AttrError;
pub use attribute::AttrHandler;
pub use attribute::AttributeManager;
pub use attribute::ProcessedAttrs;
pub use binder::BinderElabResult;
pub use binder::BinderTypeResult;
pub use coercion::Coercion;
pub use coercion::CoercionRegistry;
pub use context::ElabContext;
pub use context::LocalEntry;
pub use derive::DerivableClass;
pub use derive::DeriveRegistry;
pub use derive::Deriver;
pub use elab_decl::elaborate_decl;
pub use elab_decl::DeclElabError;
pub use elab_decl::DeclElaborator;
pub use elab_decl::PendingDecl;
pub use elaborate::elaborate_expr;
pub use equation::DecisionTree;
pub use equation::Equation;
pub use equation::EquationCompiler;
pub use equation::Pattern;
pub use implicit::resolve_implicits;
pub use implicit::resolve_instance;
pub use implicit::ImplicitArg;
pub use infer::Constraint;
pub use infer::InferResult;
pub use infer::TypeInferencer;
pub use instance::InstanceDecl;
pub use instance::InstanceResolver;
pub use macro_expand::MacroDef;
pub use macro_expand::MacroExpander;
pub use metavar::MetaVar;
pub use metavar::MetaVarContext;
pub use mutual::CallGraph;
pub use mutual::MutualBlock;
pub use mutual::MutualChecker;
pub use mutual::MutualElabError;
pub use mutual::StructuralRecursion;
pub use mutual::TerminationKind;
pub use mutual::WellFoundedRecursion;
pub use notation::expand_do_notation;
pub use notation::expand_list_literal;
pub use notation::Notation;
pub use notation::NotationRegistry;
pub use pattern_match::check_exhaustive;
pub use pattern_match::check_redundant;
pub use pattern_match::elaborate_match;
pub use pattern_match::ElabPattern;
pub use pattern_match::ExhaustivenessResult;
pub use pattern_match::MatchEquation;
pub use pattern_match::PatternCompiler;
pub use quote::quote;
pub use quote::unquote;
pub use quote::QuoteContext;
pub use solver::is_unifiable;
pub use solver::ConstraintSolver;
pub use structure::FieldInfo;
pub use structure::ProjectionDecl;
pub use structure::StructElabError;
pub use structure::StructureElaborator;
pub use structure::StructureInfo;
pub use tactic::eval_tactic_block;
pub use tactic::tactic_apply;
pub use tactic::tactic_by_contra;
pub use tactic::tactic_cases;
pub use tactic::tactic_contrapose;
pub use tactic::tactic_exact;
pub use tactic::tactic_induction;
pub use tactic::tactic_intro;
pub use tactic::tactic_push_neg;
pub use tactic::tactic_split;
pub use tactic::Goal;
pub use tactic::Tactic;
pub use tactic::TacticError;
pub use tactic::TacticRegistry;
pub use tactic::TacticResult;
pub use tactic::TacticState;
pub use typeclass::Instance;
pub use typeclass::Method;
pub use typeclass::TypeClass;
pub use typeclass::TypeClassRegistry;
pub use unify::unify;

Modules§

attr_names: Well-known attribute names used in elaboration.
attribute: Auto-generated module structure
bench_support: Auto-generated module structure
binder: Auto-generated module structure
coercion: Auto-generated module structure
command_elab: Auto-generated module structure
completion_provider: Auto-generated module structure
context: Auto-generated module structure
delaborator: Delaborator: convert kernel Expr to surface syntax. Auto-generated module structure
derive: Auto-generated module structure
derive_adv: Auto-generated module structure
differential_test: Differential testing framework: compare OxiLean elaboration against expected outputs. Auto-generated module structure
do_notation: Full do-notation elaboration (bind, pure, for, try-catch, return). Auto-generated module structure
elab_decl: Auto-generated module structure
elab_expr: Auto-generated module structure
elaborate: Auto-generated module structure
elaboration_profiler: Auto-generated module structure
equation: Auto-generated module structure
error_msg: Error message formatting and reporting infrastructure. Auto-generated module structure
hover_info: Auto-generated module structure
implicit: Auto-generated module structure
infer: Auto-generated module structure
info_tree: Info tree for IDE integration (hover, go-to-def, type-on-hover). Auto-generated module structure
instance: Auto-generated module structure
lean4_compat: Auto-generated module structure
macro_expand: Auto-generated module structure
metaprog: Auto-generated module structure
metavar: Auto-generated module structure
module_import: Auto-generated module structure
mutual: Auto-generated module structure
notation: Auto-generated module structure
parallel: Auto-generated module structure
pattern_match: Auto-generated module structure
predef: Pre-definition analysis: well-foundedness, structural recursion, termination. Auto-generated module structure
quote: Auto-generated module structure
solver: Auto-generated module structure
structure: Auto-generated module structure
tactic: Auto-generated module structure
tactic_auto: Auto-generated module structure
tactic_names: Names of all well-known tactics supported by the elaborator.
tactic_names_ext: Extended tactic name constants.
trace: Auto-generated module structure
typeclass: Auto-generated module structure
unify: Auto-generated module structure

Macros§

trace_elab: Macro for elaboration tracing
trace_infer: Macro for type inference tracing
trace_instance: Macro for instance synthesis tracing
trace_tactic: Macro for tactic tracing
trace_unify: Macro for unification tracing

Structs§

AttributeRegistry: A registry for declaration attributes.
ClassInstance: A type class instance record.
CoercionExt: A coercion rule: how to convert from type A to type B.
CoercionRegistryExt: A registry of coercions.
DeclAttribute: An attribute that can be attached to declarations.
ElabConfig: Global configuration for the elaboration pipeline.
ElabConfigExt: Configuration for the elaborator.
ElabMetrics: Metrics collected during elaboration.
ElabNoteSet: A collection of elaboration notes for a single declaration.
ElabPipeline: A pipeline of elaboration passes applied in sequence.
ElabPipelineRegistry: Pipeline configuration registry.
ElabStats: Statistics collected during an elaboration run.
EnvSnapshot: A snapshot of the elaboration environment at a point in time.
EnvSnapshotManager: A manager for environment snapshots (for module-level rollback).
InstanceRegistry: A registry for type class instances.
NamespaceEntry: A namespace entry.
NamespaceManager: A namespace manager tracking open namespaces.
ProofHistory: A history of proof state snapshots for undo support.
ProofStateSnapshot: A snapshot of a tactic proof state (for undo/redo).

Enums§

DeclKind: The kind of a top-level declaration.
ElabErrorCode: Structured error codes for elaboration failures.
ElabNote: A structured note (hint, warning, or info) attached to an elaborated item.
ElabStage: Represents a named stage in the elaboration pipeline.
Reducibility: Reducibility annotation for a definition.
UniverseCheckMode: Universe checking mode.

Traits§

ElabPass: A named elaboration pass that transforms an expression.

Functions§

is_known_tactic: Check whether a string is a known tactic name.
is_mathlib_tactic: Check if a tactic name is a Mathlib-style extended tactic.
might_be_recursive: Check if a declaration name looks like a recursive definition.
pretty_expr: Format a kernel expression as a human-readable string.
pretty_expr_list: Format a list of expressions as a comma-separated string.
tactic_category: Return the category of a tactic (proof-search, rewriting, etc.).