import MaxLeafFormal.RSCCert
import MaxLeafFormal.RSCParams
import MaxLeafFormal.RSCTrials
import MaxLeafFormal.RSCRec
import MaxLeafFormal.RSCTreeModel
import MaxLeafFormal.RSCGraph
import MaxLeafFormal.RSCCompose

/-! Statement dump for refactoring the RSC modules: the elaborated type of
every public constant defined in an RSC module, sorted by name. Run with `lake env lean` before and
after the pass and diff the outputs; not imported by the library. -/

open Lean Elab Command Meta

/-- The RSC modules: everything under `MaxLeafFormal.RSC.` plus the top-level RSC files. -/
def rscModule (m : Name) : Bool :=
  (`MaxLeafFormal.RSC).isPrefixOf m && m != `MaxLeafFormal.RSC ||
  [`MaxLeafFormal.RSCCert, `MaxLeafFormal.RSCParams, `MaxLeafFormal.RSCTrials,
   `MaxLeafFormal.RSCRec, `MaxLeafFormal.RSCTreeModel, `MaxLeafFormal.RSCTreeGen,
   `MaxLeafFormal.RSCTreeDefs, `MaxLeafFormal.RSCGraph, `MaxLeafFormal.RSCGraphDefs,
   `MaxLeafFormal.RSCCompose].contains m

#eval show CommandElabM Unit from do
  let env ← getEnv
  let mods := env.header.moduleNames
  let mut out : Array (String × String) := #[]
  for (n, ci) in env.constants.map₁.toList do
    let some idx := env.getModuleIdxFor? n | continue
    let some m := mods[idx.toNat]? | continue
    unless rscModule m do continue
    if isPrivateName n || n.isInternalDetail then continue
    let s ← liftTermElabM do
      let t ← ppExpr ci.type
      pure s!"{n} : {t}"
    out := out.push (n.toString, s)
  for (_, s) in out.qsort (fun a b => a.1 < b.1) do
    IO.println s