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

@[reducible, inline]

abbrev NN.Verification.PINN.PdeParse.State : Type

Parser state for the hand-written PDE expression parser.

@[inline]

def NN.Verification.PINN.PdeParse.eof (st : State) : Bool

Whether the PDE parser cursor has reached the end of its source text.

@[inline]

def NN.Verification.PINN.PdeParse.peek (st : State) : Option Char

Inspect the current PDE source character without advancing.

@[inline]

def NN.Verification.PINN.PdeParse.bump (st : State) : State

Advance the PDE parser cursor by one character.

@[inline]

def NN.Verification.PINN.PdeParse.fuelOf (st : State) : ℕ

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

def NN.Verification.PINN.PdeParse.isWs (c : Char) : Bool

Whitespace predicate used by the PDE expression parser.

def NN.Verification.PINN.PdeParse.skipWsFuel (fuel : ℕ) (st : State) : State

Skip whitespace with an explicit recursion budget.

def NN.Verification.PINN.PdeParse.skipWs (st : State) : State

Skip whitespace from the current parser state.

def NN.Verification.PINN.PdeParse.takeWhileFuel (fuel : ℕ) (p : Char → Bool) (acc : String) (st : State) : String × State

Consume characters satisfying p, accumulating into acc, with explicit fuel.

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

Consume characters satisfying p, accumulating into acc.

def NN.Verification.PINN.PdeParse.parseNumber (st : State) : Except String (Float × State)

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

def NN.Verification.PINN.PdeParse.parseNat (st : State) : Except String (ℕ × State)

Parse a natural number at the current parser state.

def NN.Verification.PINN.PdeParse.parseIdent (st : State) : Except String (String × State)

Parse an identifier used for environment lookup.

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

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

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

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

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

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

Parse a multiplicative term with an explicit recursion budget.

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

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

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

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

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

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

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

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

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

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.