PdeParse

A compact hand-rolled parser from strings to PDE AST (Expr).

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

Derivative names accept both compact and subscript-style spellings: u, ux, uy, ut, uxx, uyy, utt, u_x, u_y, u_t, u_xx, u_yy, and u_tt. For 1D-in-time PINN examples, the parser treats t as the second axis, so u_t is the same primitive as u_y.

Numbers are parsed as Floats. Idents look up a value from env : String → Option Float. Unsupported tokens produce an error.

Natural powers use the usual identities ($x^0=1$), and powers bind more tightly than unary minus, so -u^2 means -(u^2). Power expansion creates a multiplication chain proportional to the exponent; recursive parser fuel does not cap that expansion.

Implementation note: The parser is total by threading a simple fuel : Nat through the recursive descent; fuel is initialized from the remaining bytes in the input and decreases on every recursive descent step.

References:

• PINNs (motivation for residual expressions): https://arxiv.org/abs/1711.10561

Scanning uses the same byte-position cursor as the ODE parser, with this grammar's fuel policy.

@[inline]

def NN.Verification.PINN.PdeParse.Internal.fuelOf (st : Util.TextCursor.Cursor) : ℕ

Recursion budget with additional headroom for the mutually recursive PDE grammar.

Even a one-character input like u traverses expr → term → unary → factor → primary, so the budget includes headroom beyond the remaining byte count.

def NN.Verification.PINN.PdeParse.Internal.skipWs (st : Util.TextCursor.Cursor) : Util.TextCursor.Cursor

Skip whitespace from the current parser state.

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

Consume characters satisfying p, accumulating into acc.

def NN.Verification.PINN.PdeParse.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.PINN.PdeParse.Internal.parseNat (st : Util.TextCursor.Cursor) : Except String (ℕ × Util.TextCursor.Cursor)

Parse a natural number at the current parser state.

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

Parse an identifier used for environment lookup.

def NN.Verification.PINN.PdeParse.Internal.builtinIdent? : String → Option PdeAst.Expr

Parse the built-in PDE primitive names before falling back to external constants.

def NN.Verification.PINN.PdeParse.Internal.parseExprCoreFuel (fuel : ℕ) (env : String → Option Float) (st : Util.TextCursor.Cursor) : Except String (PdeAst.Expr × Util.TextCursor.Cursor)

Parse an additive/subtractive expression with an explicit recursion budget.

def NN.Verification.PINN.PdeParse.Internal.parseExprCoreFuel.loop (env : String → Option Float) (fuel : ℕ) (acc : PdeAst.Expr) (st : Util.TextCursor.Cursor) : Except String (PdeAst.Expr × Util.TextCursor.Cursor)

def NN.Verification.PINN.PdeParse.Internal.parseTermFuel (fuel : ℕ) (env : String → Option Float) (st : Util.TextCursor.Cursor) : Except String (PdeAst.Expr × Util.TextCursor.Cursor)

Parse a multiplicative term with an explicit recursion budget.

def NN.Verification.PINN.PdeParse.Internal.parseTermFuel.loop (env : String → Option Float) (fuel : ℕ) (acc : PdeAst.Expr) (st : Util.TextCursor.Cursor) : Except String (PdeAst.Expr × Util.TextCursor.Cursor)

def NN.Verification.PINN.PdeParse.Internal.parseFactorFuel (fuel : ℕ) (env : String → Option Float) (st : Util.TextCursor.Cursor) : Except String (PdeAst.Expr × Util.TextCursor.Cursor)

Parse a primary expression plus an optional natural-number power, with $x^0=1$.

def NN.Verification.PINN.PdeParse.Internal.parseFactorFuel.powMul (base : PdeAst.Expr) (k : ℕ) (acc : PdeAst.Expr) : PdeAst.Expr

def NN.Verification.PINN.PdeParse.Internal.parseUnaryFuel (fuel : ℕ) (env : String → Option Float) (st : Util.TextCursor.Cursor) : Except String (PdeAst.Expr × Util.TextCursor.Cursor)

Parse leading negations. Exponentiation binds more tightly than unary minus.

def NN.Verification.PINN.PdeParse.Internal.parsePrimaryFuel (fuel : ℕ) (env : String → Option Float) (st : Util.TextCursor.Cursor) : Except String (PdeAst.Expr × Util.TextCursor.Cursor)

Parse atoms: parenthesized expressions, u/derivative names, numerals, or environment identifiers.

def NN.Verification.PINN.PdeParse.Internal.parseExprCore (env : String → Option Float) (st : Util.TextCursor.Cursor) : Except String (PdeAst.Expr × Util.TextCursor.Cursor)

Parse a full expression from the current parser state.

def NN.Verification.PINN.PdeParse.parseExpr (env : String → Option Float) (s : String) : Except String PdeAst.Expr

Entry point: parse a string to Expr using env for identifiers.