TextualPeg (infer.SemDiffLib.TextualPeg)

Module SemDiffLib.TextualPeg

Program Equivalence Graph (PEG) built from Textual IR.

A PEG is a pure functional representation of an imperative program where control flow is encoded as data: branches become @phi(cond, then, else) nodes, side effects are ordered by state tokens @seq(state, effect), and the procedure result is @ret(final_state, return_value). Two programs are semantically equivalent when their PEG roots belong to the same e-class after equality saturation. See Tate et al., "Equality Saturation: a New Approach to Optimization", POPL 2009.

This module converts a Textual procedure into PEG terms inside a CongruenceClosureSolver e-graph. Python-specific: interprets py_store_fast / py_load_fast to build proper SSA with @phi nodes at control-flow join points rather than treating the mutable *PyLocals frame as opaque.

Phase 1 handles loop-free procedures only (no back-edges).

module CC = CongruenceClosureSolver

Equations trace

Records every binding produced during PEG construction. Useful for debugging and for understanding the translation.

module Equations : sig ... end

Construction

val convert_proc : 
  ?theta_counter:int IStdlib.IStd.ref ->
  CC.t ->
  Textuallib.Textual.ProcDesc.t ->
  (CC.Atom.t * Equations.t * int, string) IStdlib.IStd.result

convert_proc cc proc converts a Textual procedure into e-graph terms in cc. Returns the root atom, the full equation trace, and the number of loops, or Error msg for unsupported constructs. theta_counter provides fresh names for recursive variables across procedures sharing the same cc.

Pretty-printing

val pp_tree : 
  ?depth:int ->
  CC.t ->
  Stdlib.Format.formatter ->
  CC.Atom.t ->
  unit

pp_tree cc fmt atom prints the PEG rooted at atom as an ASCII tree.