Parse

Hand-rolled parser for ODE RHS expressions.

Grammar (informal): expr := term (('+' | '-') term)* term := unary (('' | '/') unary) unary := '-' unary | factor factor := primary ('^' nat)? 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; x^0 is one. Exponentiation binds more tightly than unary minus, so -u^2 means -(u^2). The expansion is proportional to n and is not capped by the recursive parser fuel.

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.Expr.

Parser state and low-level helpers

The cursor itself lives in NN.Verification.Util.TextCursor, shared with the PINN PDE parser, and so do the scanning primitives. What remains here is a thin layer whose only job is to supply this grammar's fuel budget to those primitives, so the rest of the file can call skipWs and friends without repeating fuelOf st at every site. The PDE parser keeps the same four names for the same reason; the budget behind them is what differs.

@[inline]

def NN.Verification.ODE.Parse.Internal.fuelOf (st : Util.TextCursor.Cursor) : ℕ

A fuel budget derived from the remaining input length, which is what guarantees termination.

Unlike the PDE parser this grammar bottoms out within the remaining bytes, so the raw remaining count is enough and no headroom factor is needed.

def NN.Verification.ODE.Parse.Internal.skipWs (st : Util.TextCursor.Cursor) : Util.TextCursor.Cursor

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

def NN.Verification.ODE.Parse.Internal.takeWhile (p : Char → Bool) (acc : String) (st : Util.TextCursor.Cursor) : String × Util.TextCursor.Cursor

Consume consecutive characters satisfying p, accumulating them into acc.

Returns the consumed text and the updated parser state.

def NN.Verification.ODE.Parse.Internal.parseNumber (st : Util.TextCursor.Cursor) : Except String (Float × Util.TextCursor.Cursor)

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

def NN.Verification.ODE.Parse.Internal.parseNat (st : Util.TextCursor.Cursor) : Except String (ℕ × Util.TextCursor.Cursor)

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

def NN.Verification.ODE.Parse.Internal.parseIdent (st : Util.TextCursor.Cursor) : Except String (String × Util.TextCursor.Cursor)

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

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 : Util.TextCursor.Cursor) : Except String (Expr × Util.TextCursor.Cursor)

Parse an addition/subtraction chain with an explicit fuel budget.

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

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

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

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

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

Parse a primary expression with optional natural-number exponentiation.

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

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

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

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

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.Expr).