Parse

Hand-rolled parser for ODE RHS expressions.

Grammar (informal): expr := term (('+' | '-') term)* term := factor (('' | '/') factor) factor := unary ('^' nat)? unary := '-' unary | primary primary:= number | 't' | 'u' | ident '(' expr ')' | ident | '(' expr ')'

Supported unary functions: sin, cos, exp, log. Supported identifiers: pi.

Exponentiation is expanded into repeated multiplication when ^ n is given.

This parser is part of the executable ODE verifier. We keep the grammar direct and hand-written so that the accepted certificate syntax is visible in one file, with predictable errors and no hidden parser-combinator behavior.

The output AST is NN.Verification.ODE.Ast.Expr.

Parser state and low-level helpers

structure NN.Verification.ODE.Parse.State : Type

Parser state for scanning a String by byte-position.

We track the source string s and the current raw byte index i.

• s : String

  Source text being parsed.

• i : String.Pos.Raw

  Current raw byte offset in s.

@[inline]

def NN.Verification.ODE.Parse.peek (st : State) : Option Char

Peek at the current character, if any, without advancing.

@[inline]

def NN.Verification.ODE.Parse.bump (st : State) : State

Advance the current position by one character.

@[inline]

def NN.Verification.ODE.Parse.fuelOf (st : State) : ℕ

A fuel budget derived from the remaining input length (used to guarantee termination).

def NN.Verification.ODE.Parse.Internal.isWs (c : Char) : Bool

Internal: ASCII whitespace predicate used by skipWs.

def NN.Verification.ODE.Parse.Internal.skipWsFuel : ℕ → State → State

Fuel-bounded whitespace skipping (implementation of skipWs).

def NN.Verification.ODE.Parse.skipWs (st : State) : State

Skip ASCII whitespace (' ', '\t', '\n').

def NN.Verification.ODE.Parse.Internal.takeWhileFuel (fuel : ℕ) (p : Char → Bool) (acc : String) (st : State) : String × State

Internal: fuel-bounded implementation of takeWhile.

def NN.Verification.ODE.Parse.takeWhile (p : Char → Bool) (acc : String) (st : State) : String × State

Consume consecutive characters satisfying p, accumulating them into acc.

Returns the consumed text and the updated parser state.

def NN.Verification.ODE.Parse.parseNumber (st : State) : Except String (Float × State)

Parse a signed decimal number without exponent, e.g. -12.34.

def NN.Verification.ODE.Parse.parseNat (st : State) : Except String (ℕ × State)

Parse a natural number (decimal digits) used for exponents ^ n.

def NN.Verification.ODE.Parse.parseIdent (st : State) : Except String (String × State)

Parse an identifier consisting of letters/digits/underscore.

Built-in constants and unary functions

def NN.Verification.ODE.Parse.Internal.constOfIdent? (id : String) : Option Float

Internal: interpret built-in constants like pi / π.

def NN.Verification.ODE.Parse.Internal.applyFunc? (id : String) (arg : Expr) : Option Expr

Interpret supported unary function names (e.g. sin, cos, exp, log).

Recursive descent: expression/term/factor/unary/primary

def NN.Verification.ODE.Parse.Internal.parseExprFuel (fuel : ℕ) (st : State) : Except String (Expr × State)

Internal: parse an expr (addition/subtraction chain), with an explicit fuel budget.

This is a plain def (not private) because the module is in a public section for export/doc tooling, and Lean 4.29 disallows referring to private declarations from public ones.

def NN.Verification.ODE.Parse.Internal.parseExprFuel.loop (fuel : ℕ) (acc : Expr) (st : State) : Except String (Expr × State)

def NN.Verification.ODE.Parse.Internal.parseTermFuel (fuel : ℕ) (st : State) : Except String (Expr × State)

Parse a term (multiplication/division chain), with an explicit fuel budget.

def NN.Verification.ODE.Parse.Internal.parseTermFuel.loop (fuel : ℕ) (acc : Expr) (st : State) : Except String (Expr × State)

def NN.Verification.ODE.Parse.Internal.parseFactorFuel (fuel : ℕ) (st : State) : Except String (Expr × State)

Parse a factor (unary with optional exponentiation), with an explicit fuel budget.

def NN.Verification.ODE.Parse.Internal.parseFactorFuel.powMul (base : Expr) (k : ℕ) (acc : Expr) : Expr

def NN.Verification.ODE.Parse.Internal.parseUnaryFuel (fuel : ℕ) (st : State) : Except String (Expr × State)

Parse a unary (leading negations), with an explicit fuel budget.

def NN.Verification.ODE.Parse.Internal.parsePrimaryFuel (fuel : ℕ) (st : State) : Except String (Expr × State)

Parse a primary atom (number/variable/function-call/parentheses), with an explicit fuel budget.

def NN.Verification.ODE.Parse.parseExpr (s : String) : Except String Expr

Parse an ODE RHS expression string into an AST.

This is the user-facing entrypoint for the ODE verifier: it parses a string like "sin(t) + u^2" into an Expr (NN.Verification.ODE.Ast.Expr).