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 : 
  CC.t ->
  Textuallib.Textual.ProcDesc.t ->
  (CC.Atom.t * Equations.t, string) IStdlib.IStd.result

convert_proc cc proc converts a loop-free Textual procedure into e-graph terms in cc. Returns the root atom and the full equation trace, or Error msg for back-edges / unsupported constructs.