PdeParse

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

Grammar (informal): expr := term (('+' | '-') term)* term := factor ('' factor) factor := primary ('^' int)? primary:= 'u' | 'ux' | 'uy' | 'uxx' | 'uyy' | number | ident | '(' expr ')'

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

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

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

Parser state for the hand-written PDE expression parser.

• s : String

  Input string being parsed.

• i : String.Pos.Raw

  Current raw byte position in s.

@[inline]

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

@[inline]

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

@[inline]

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

@[inline]

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

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

Whitespace predicate used by the PDE expression parser.

def NN.Verification.PINN.PdeParse.skipWsFuel : ℕ → 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.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 integer power.

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

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.