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

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

NN.Verification.Util.TextCursor is the shared byte-position cursor, and this parser and the ODE parser both scan with it. The four forwarders below read exactly like the ODE parser's, but each one closes over fuelOf, and the fuel policy is where the two grammars part company. Binding it once here is what keeps the recursive descent underneath free of budget arithmetic.

@[inline]

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

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

This is the one place where the two hand-written parsers genuinely differ, so it is worth stating why. fuel is a recursion budget, not a token count. Even a one-character input like u walks expr → term → unary → factor → primary, so a budget equal to the remaining bytes would run out before the grammar bottoms out. Scaling by 8 and adding 16 covers the deepest descent that any accepted input can force.

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.