Documentation

LeanMlir.Proofs.Codegen.StableHLO.Parse

StableHLOParse — the token skeleton of an SHlo term round-trips #

StableHLO.Basic states what each SHlo graph denotes: its *_faithful theorems equate den of a node or graph with a named ℝ function (fwdGraph_faithful : den (fwdGraph W b x) = mnistLinear W b x, …). This file is about the other side, the encoding the printer works from:

Scope: the round trip is a statement about toToks, not about the text. Which operands each op's emitted line reads, in what order, with what types, is decided by emitTok (in StableHLO/Pretty.lean) and is trusted, together with the per-op lexical syntax, the per-op StableHLO semantics, the lowering, and float32 ≈ ℝ.

source
def Proofs.StableHLO.parseStack :
List Tok → List Raw → Option (List Raw)

Stack reconstructor: fold the token stream, pushing operands and applying each opcode to the top of the stack (popping its arity).

Instances For
    source
    def Proofs.StableHLO.parse (ts : List Tok) :
    Option Raw

    Parse a full token stream back to a single graph.

    Equations
    Instances For
      source
      theorem Proofs.StableHLO.parseStack_toToks (r : Raw) (ts : List Tok) (st : List Raw) :
      parseStack (toToks r ++ ts) st = parseStack ts (r :: st)

      Stack invariant. Serializing r and folding it onto a stack st pushes exactly r. The generalized statement that drives the round-trip.

      source
      theorem Proofs.StableHLO.parse_toToks (r : Raw) :
      parse (toToks r) = some r

      Serialization round-trip. parse recovers any skeleton from its postorder token stream.

      source
      theorem Proofs.StableHLO.roundtrip {k : ℕ} (a : SHlo k) :
      parse (toToks (skel a)) = some (skel a)

      Skeleton round trip. The postorder token encoding of the skeleton of any SHlo term is invertible: parse (toToks (skel a)) = some (skel a). It is a statement about toToks, not about the text: which operands each op's emitted line reads, in what order, and with what types is decided by emitTok and remains trusted along with the lexical syntax.