#!/usr/bin/env julia
include(joinpath(@__DIR__,"..","src","OmegaNaughtProofs.jl"))
using .OmegaNaughtProofs
using TOML
root=normpath(joinpath(@__DIR__,".."))
open(joinpath(root,"PROOFS.md"),"w") do io
    println(io,"# Complete mathematical proof companion\n")
    println(io,"Generated verbatim from the literate proof strings in `src/ProofGuide.jl` by `scripts/export_guides.jl`.\n")
    println(io,"These are mathematical arguments with exact Julia certificates at the stated interfaces. Julia does not kernel-check the universal logical, real, or calculus inferences. `THEOREM_GUIDE.md` maps all 147 original declarations individually.\n")
    for key in sort(collect(keys(PROOFS)))
        lines=split(strip(PROOFS[key]),'\n';limit=2)
        println(io,"## ",key," — ",lines[1],"\n")
        println(io,lines[2],"\n")
    end
end
entries=TOML.parsefile(joinpath(root,"THEOREMS.toml"))["theorem"]
open(joinpath(root,"THEOREM_GUIDE.md"),"w") do io
    println(io,"# All 147 source theorems: declarations and proof steps\n")
    println(io,"Every declaration below is copied verbatim from its supplied Lean module. Section variables and module definitions remain applicable; the source file is the authority for elaborated domains. The new mathematical proof is in `PROOFS.md` and the Julia string `PROOFS[chapter]`. Computational evidence does not replace the analytic argument.\n")
    for e in entries
        println(io,"## ",e["name"],"\n")
        println(io,"Source: [",e["source"],"](",e["source"],"), line ",e["line"],". Proof chapter: **",e["chapter"],"**.\n")
        println(io,"```lean\n",e["statement"],"\n```\n")
        println(io,"Section context: `",replace(e["section_context"],"\n"=>"; "),"`\n")
        println(io,"Proof step: ",e["proof_step"],"\n")
        println(io,"Evidence: ",e["evidence"],"\n")
    end
end
println("Exported PROOFS.md and THEOREM_GUIDE.md (",length(entries)," theorems).")