import CoreFormalism.CRTSidon
open CoreFormalism.CRTSidon

/-- JSON-escape a string. -/
def jsonEscape (s : String) : String :=
  let r := s.replace "\\" "\\\\"
  let r := r.replace "\"" "\\\""
  let r := r.replace "\n" "\\n"
  "\"" ++ r ++ "\""

/-- Call phi4 on neon-64gb to generate a Lean proof. -/
def callLLM (prompt : String) : IO String := do
  let escPrompt := jsonEscape prompt
  let pyScript := "import urllib.request, json\n" ++
    "body = json.dumps({'name': 'phi4:14b', 'input': " ++ escPrompt ++ "})\n" ++
    "req = urllib.request.Request('http://100.92.88.64:8766/generate', data=body.encode(),\n" ++
    "    headers={'Content-Type': 'application/json'})\n" ++
    "resp = urllib.request.urlopen(req, timeout=600)\n" ++
    "data = json.loads(resp.read())\n" ++
    "print(data['outputs'][0]['text'])\n"
  let out ← IO.Process.output { cmd := "python3", args := #["-c", pyScript] }
  if out.exitCode ≠ 0 then
    return s!"Process error: {out.stderr}"
  return out.stdout.trimRight

/-- Strip markdown code fences and extract Lean code. -/
def extractLeanCode (s : String) : String :=
  let s := s.trimAscii.toString
  if s.startsWith "```" then
    let withoutFirst := s.dropWhile (fun c => c ≠ '\n') |>.trimLeft
    let withoutLast := withoutFirst.splitOn "```" |>.head?
    (withoutLast.getD withoutFirst).trimAscii.toString
  else
    s

/-- Read a file as string. -/
def readFile (path : String) : IO String := do
  let h ← IO.FS.Handle.open path IO.FS.Mode.read
  h.readToEnd

/-- Write a file. -/
def writeFile (path : String) (content : String) : IO Unit := do
  let h ← IO.FS.Handle.open path IO.FS.Mode.write
  h.write content

/-- Run a shell command and return stdout. -/
def runCmd (cmd : String) (args : List String) : IO String := do
  let out ← IO.Process.output { cmd := cmd, args := args.toArray }
  if out.exitCode ≠ 0 then
    return s!"BUILD FAILED ({out.exitCode}): {out.stderr}"
  return out.stdout

/-- AutoProof main: verify CRTSidon no longer has sorries. -/
def main : IO Unit := do
  IO.println "=== AutoProof: CRTSidon ===\n"
  let filePath := "formal/CoreFormalism/CRTSidon.lean"
  let content ← readFile filePath
  let sorryCount := content.splitOn "sorry" |>.length - 1
  if sorryCount = 0 then
    IO.println "No sorries found. Theorem is complete."
    IO.println "\n=== Done ==="
    return
  IO.println s!"Found {sorryCount} sorry/s to fill."
  IO.println "\n=== Done ==="