oxilean-parse

Parser for the OxiLean theorem prover

Converts OxiLean source text (.oxilean files) into an abstract syntax tree (AST). This crate is untrusted -- bugs here can cause parse failures but never soundness issues, because the kernel independently type-checks all elaborated terms.

62,293 SLOC -- fully implemented parser with lexer, AST, and error recovery (335 source files, 2,153 tests passing).

Architecture

Source text (.oxilean)
    |
    v
+----------------+
|    Lexer       |  -> Token stream with Span positions
|  (lexer.rs)    |
+-------+--------+
        v
+----------------+
|    Parser      |  -> Surface AST (SurfaceExpr, SurfaceDecl)
| (parser.rs)    |
+----------------+

Module Overview

Module	Status	Description
`token.rs`	Implemented	Token definitions (keywords, symbols, literals, identifiers)
`lexer.rs`	Implemented	Hand-written character-by-character lexer
`ast.rs`	Implemented	Surface syntax AST types
`parser.rs`	Implemented	Recursive descent / Pratt parser
`error.rs`	Implemented	Parse error type with `Display` and `Error`

Features

Lexer

UTF-8 identifier support (alpha, beta, Pi, lambda, arrow, turnstile, and other mathematical symbols)
Line comments (--) and nested block comments (/- ... -/)
Indentation tracking for where blocks
Source span (Span) for every token (enables precise error reporting)

Token System

Keywords: def, theorem, axiom, inductive, where, match, with, let, in, by, import, universe, namespace, end, if, then, else
Symbols: arrow, =>, :, ;, ,, ., |, (, ), {, }, [, ], :=, _, @, #
Literals: NatLit(u64), StrLit(String)
Identifiers: Ident(String)

Surface AST

// Expressions (what users write)
pub enum SurfaceExpr {
    Var(String),                    // unresolved name
    App(Box<SE>, Box<SE>),          // f a
    Lam(Vec<Binder>, Box<SE>),      // fun x => body
    Pi(Vec<Binder>, Box<SE>),       // (x : A) -> B
    Arrow(Box<SE>, Box<SE>),        // A -> B (non-dependent)
    Let(String, Option<Box<SE>>, Box<SE>, Box<SE>),
    Match(Box<SE>, Vec<MatchArm>),  // match e with | ...
    ByTactic(Vec<Tactic>),          // by { tac1; tac2; ... }
    Lit(Literal),                   // 42, "hello"
    Hole,                           // _
    Parens(Box<SE>),
    Proj(Box<SE>, String),          // e.field
}

// Declarations (top-level items)
pub enum SurfaceDecl {
    Def { name, params, ret_ty, body },
    Theorem { name, params, ty, proof },
    Axiom { name, params, ty },
    Inductive { name, params, ty, ctors },
    Import(String),
    Universe(Vec<String>),
}

Parser

Pratt parsing for expression operators (no external dependencies)
Operator precedence: arrows (right-assoc, prec 25), application (left-assoc, prec 1024)
Error recovery: synchronize on def, theorem, axiom, inductive, EOF
Multi-error reporting (continues parsing after an error)

Dependencies

oxilean-kernel -- for Name, Level, Literal types

Example (Target Syntax)

-- Natural number addition
def Nat.add (n m : Nat) : Nat :=
  match n with
  | Nat.zero   => m
  | Nat.succ k => Nat.succ (Nat.add k m)

-- Commutativity of addition (proof)
theorem Nat.add_comm (n m : Nat) : Nat.add n m = Nat.add m n := by
  induction n with
  | zero => simp [Nat.add]
  | succ k ih => simp [Nat.add, ih]

Testing

cargo test -p oxilean-parse

oxilean-parse 0.1.1