;; ---------------------------------------------------------------------------
;; Self-Hosting Bootstrapper — py.sx (COMPLETE)
;; ---------------------------------------------------------------------------
;; @css bg-green-100 text-green-800 bg-green-50 border-green-200 text-green-700 text-green-600

(defcomp ()
  (~docs/page :title "Self-Hosting Bootstrapper"

    ;; -----------------------------------------------------------------------
    ;; Status banner
    ;; -----------------------------------------------------------------------

    (div (~tw :tokens "rounded-lg bg-green-50 border border-green-200 p-4 mb-8")
      (div (~tw :tokens "flex items-center gap-3")
        (span (~tw :tokens "inline-flex items-center rounded-full bg-green-100 px-3 py-1 text-sm font-semibold text-green-800")
          "Complete")
        (p (~tw :tokens "text-green-700 text-sm")
          (code "py.sx") " is implemented and verified. G0 == G1: 128/128 defines match, "
          "1490 lines, 88,955 bytes — byte-for-byte identical. "
          (a :href "/sx/(language.(bootstrapper.self-hosting))" (~tw :tokens "underline text-green-600 font-medium")
             "See live verification."))))

    ;; -----------------------------------------------------------------------
    ;; The Idea
    ;; -----------------------------------------------------------------------

    (~docs/section :title "The Idea" :id "idea"
      (p "We have " (code "bootstrap_py.py") " — a Python program that reads "
         (code ".sx") " spec files and emits " (code "sx_ref.py")
         ", a standalone Python evaluator. It's a compiler written in the host language.")
      (p "We also have " (code "z3.sx") " — a translator written in SX itself that "
         "converts SX spec declarations into SMT-LIB for Z3. It's proof that "
         "SX can generate code in another language.")
      (p (strong "py.sx") " — an SX-to-Python translator written in SX. "
         "Feed it through the existing Python evaluator against the spec files and it produces "
         (code "sx_ref.py") ". The bootstrapper bootstraps itself.")
      (p (code "py.sx") " produces output identical to " (code "bootstrap_py.py")
         ". The Python bootstrapper is redundant. "
         "The spec defines itself."))

    ;; -----------------------------------------------------------------------
    ;; Results
    ;; -----------------------------------------------------------------------

    (~docs/section :title "Results" :id "results"
      (div (~tw :tokens "overflow-x-auto rounded border border-stone-200 my-4")
        (table (~tw :tokens "w-full text-sm")
          (thead (~tw :tokens "bg-stone-50")
            (tr
              (th (~tw :tokens "px-4 py-2 text-left font-semibold text-stone-700") "Metric")
              (th (~tw :tokens "px-4 py-2 text-left font-semibold text-stone-700") "Value")))
          (tbody
            (tr (~tw :tokens "border-t border-stone-100")
              (td (~tw :tokens "px-4 py-2 text-stone-600") "py.sx size")
              (td (~tw :tokens "px-4 py-2 font-mono") "1,182 lines"))
            (tr (~tw :tokens "border-t border-stone-100")
              (td (~tw :tokens "px-4 py-2 text-stone-600") "bootstrap_py.py size (replaced)")
              (td (~tw :tokens "px-4 py-2 font-mono") "902 lines (PyEmitter class)"))
            (tr (~tw :tokens "border-t border-stone-100")
              (td (~tw :tokens "px-4 py-2 text-stone-600") "Defines translated")
              (td (~tw :tokens "px-4 py-2 font-mono") "128/128 exact match"))
            (tr (~tw :tokens "border-t border-stone-100")
              (td (~tw :tokens "px-4 py-2 text-stone-600") "Spec files processed")
              (td (~tw :tokens "px-4 py-2 font-mono") "7 (eval, forms, render, adapter-html, adapter-sx, deps, signals)"))
            (tr (~tw :tokens "border-t border-stone-100")
              (td (~tw :tokens "px-4 py-2 text-stone-600") "Output size")
              (td (~tw :tokens "px-4 py-2 font-mono") "1,490 lines / 88,955 bytes"))
            (tr (~tw :tokens "border-t border-stone-100 bg-green-50")
              (td (~tw :tokens "px-4 py-2 font-semibold text-green-700") "G0 == G1")
              (td (~tw :tokens "px-4 py-2 font-semibold text-green-700") "Identical (diff is empty)"))))))

    ;; -----------------------------------------------------------------------
    ;; Architecture
    ;; -----------------------------------------------------------------------

    (~docs/section :title "Architecture" :id "architecture"
      (p "Three bootstrapper generations:")
      (div (~tw :tokens "overflow-x-auto rounded border border-stone-200 my-4")
        (table (~tw :tokens "w-full text-sm")
          (thead (~tw :tokens "bg-stone-50")
            (tr
              (th (~tw :tokens "px-4 py-2 text-left font-semibold text-stone-700") "Gen")
              (th (~tw :tokens "px-4 py-2 text-left font-semibold text-stone-700") "Source")
              (th (~tw :tokens "px-4 py-2 text-left font-semibold text-stone-700") "Runs on")
              (th (~tw :tokens "px-4 py-2 text-left font-semibold text-stone-700") "Reads")
              (th (~tw :tokens "px-4 py-2 text-left font-semibold text-stone-700") "Produces")))
          (tbody
            (tr (~tw :tokens "border-t border-stone-100")
              (td (~tw :tokens "px-4 py-2 font-mono text-stone-600") "G0")
              (td (~tw :tokens "px-4 py-2") (code "bootstrap_py.py"))
              (td (~tw :tokens "px-4 py-2") "Python (manual)")
              (td (~tw :tokens "px-4 py-2") (code "eval.sx") ", " (code "render.sx") ", ...")
              (td (~tw :tokens "px-4 py-2") (code "sx_ref.py")))
            (tr (~tw :tokens "border-t border-stone-100 bg-green-50")
              (td (~tw :tokens "px-4 py-2 font-mono text-green-700") "G1")
              (td (~tw :tokens "px-4 py-2") (code "py.sx"))
              (td (~tw :tokens "px-4 py-2") "Python evaluator + SX")
              (td (~tw :tokens "px-4 py-2") (code "eval.sx") ", " (code "render.sx") ", ...")
              (td (~tw :tokens "px-4 py-2 font-semibold text-green-700") (code "sx_ref.py") " (identical)"))
            (tr (~tw :tokens "border-t border-stone-100")
              (td (~tw :tokens "px-4 py-2 font-mono text-stone-600") "G2")
              (td (~tw :tokens "px-4 py-2") (code "py.sx"))
              (td (~tw :tokens "px-4 py-2") (code "sx_ref.py") " from G1 + SX")
              (td (~tw :tokens "px-4 py-2") (code "eval.sx") ", " (code "render.sx") ", ...")
              (td (~tw :tokens "px-4 py-2") (code "sx_ref.py") " (fixed-point)")))))

      (p "G0 is the hand-written compiler. G1 replaces it with SX. "
         "G2 proves the fixed-point: " (code "py.sx") " compiled by its own output "
         "produces the same output. That's the definition of self-hosting."))

    ;; -----------------------------------------------------------------------
    ;; Translation Rules
    ;; -----------------------------------------------------------------------

    (~docs/section :title "Translation Rules" :id "translation"

      (~docs/subsection :title "Name Mangling"
        (p "SX identifiers become valid Python identifiers. "
           "The RENAMES dict (200+ entries) handles explicit mappings; "
           "general rules handle the rest:")
        (div (~tw :tokens "overflow-x-auto rounded border border-stone-200 my-4")
          (table (~tw :tokens "w-full text-sm")
            (thead (~tw :tokens "bg-stone-50")
              (tr
                (th (~tw :tokens "px-4 py-2 text-left font-semibold text-stone-700") "SX")
                (th (~tw :tokens "px-4 py-2 text-left font-semibold text-stone-700") "Python")
                (th (~tw :tokens "px-4 py-2 text-left font-semibold text-stone-700") "Rule")))
            (tbody
              (tr (~tw :tokens "border-t border-stone-100")
                (td (~tw :tokens "px-4 py-2 font-mono") "eval-expr")
                (td (~tw :tokens "px-4 py-2 font-mono") "eval_expr")
                (td (~tw :tokens "px-4 py-2") "kebab → snake"))
              (tr (~tw :tokens "border-t border-stone-100")
                (td (~tw :tokens "px-4 py-2 font-mono") "nil?")
                (td (~tw :tokens "px-4 py-2 font-mono") "is_nil")
                (td (~tw :tokens "px-4 py-2") "predicate rename"))
              (tr (~tw :tokens "border-t border-stone-100")
                (td (~tw :tokens "px-4 py-2 font-mono") "empty?")
                (td (~tw :tokens "px-4 py-2 font-mono") "empty_p")
                (td (~tw :tokens "px-4 py-2") "? → _p (general)"))
              (tr (~tw :tokens "border-t border-stone-100")
                (td (~tw :tokens "px-4 py-2 font-mono") "set!")
                (td (~tw :tokens "px-4 py-2 font-mono") "set_b")
                (td (~tw :tokens "px-4 py-2") "! → _b"))
              (tr (~tw :tokens "border-t border-stone-100")
                (td (~tw :tokens "px-4 py-2 font-mono") "type")
                (td (~tw :tokens "px-4 py-2 font-mono") "type_")
                (td (~tw :tokens "px-4 py-2") "Python reserved word escape"))))))

      (~docs/subsection :title "Special Forms"
        (p "Each SX special form maps to a Python expression pattern:")
        (div (~tw :tokens "overflow-x-auto rounded border border-stone-200 my-4")
          (table (~tw :tokens "w-full text-sm")
            (thead (~tw :tokens "bg-stone-50")
              (tr
                (th (~tw :tokens "px-4 py-2 text-left font-semibold text-stone-700") "SX")
                (th (~tw :tokens "px-4 py-2 text-left font-semibold text-stone-700") "Python")))
            (tbody
              (tr (~tw :tokens "border-t border-stone-100")
                (td (~tw :tokens "px-4 py-2 font-mono") "(if c t e)")
                (td (~tw :tokens "px-4 py-2 font-mono") "(t if sx_truthy(c) else e)"))
              (tr (~tw :tokens "border-t border-stone-100")
                (td (~tw :tokens "px-4 py-2 font-mono") "(let ((a 1)) body)")
                (td (~tw :tokens "px-4 py-2 font-mono") "(lambda a: body)(1)"))
              (tr (~tw :tokens "border-t border-stone-100")
                (td (~tw :tokens "px-4 py-2 font-mono") "(fn (x) body)")
                (td (~tw :tokens "px-4 py-2 font-mono") "lambda x: body"))
              (tr (~tw :tokens "border-t border-stone-100")
                (td (~tw :tokens "px-4 py-2 font-mono") "(and a b c)")
                (td (~tw :tokens "px-4 py-2 font-mono") "(a if not sx_truthy(a) else ...)"))
              (tr (~tw :tokens "border-t border-stone-100")
                (td (~tw :tokens "px-4 py-2 font-mono") "(case x \"a\" 1)")
                (td (~tw :tokens "px-4 py-2 font-mono") "_sx_case(x, [(\"a\", lambda: 1)])"))))))

      (~docs/subsection :title "Mutation: set! and Cell Variables"
        (p "Python closures can read but not rebind outer variables. "
           (code "py.sx") " detects " (code "set!") " targets that cross lambda boundaries "
           "and routes them through a " (code "_cells") " dict:")
        (~docs/code :src (highlight ";; SX                              ;; Python
(define counter                    def counter():
  (fn ()                               _cells = {}
    (let ((n 0))                       _cells['n'] = 0
      (fn ()                           return lambda: _sx_begin(
        (set! n (+ n 1))                   _sx_cell_set(_cells, 'n', ...),
        n))))                              _cells['n'])" "python"))
        (p "This is the hardest translation rule. " (code "py-find-nested-set-vars")
           " scans the AST for " (code "set!") " inside nested " (code "fn") " bodies. "
           (code "py-emit-define-as-def") " emits a " (code "def") " with " (code "_cells")
           " dict instead of a lambda.")))

    ;; -----------------------------------------------------------------------
    ;; Scope
    ;; -----------------------------------------------------------------------

    (~docs/section :title "Scope" :id "scope"
      (p (code "py.sx") " is a general-purpose SX-to-Python translator. "
         "The translation rules are mechanical and apply to " (em "all") " SX, "
         "not just the spec subset.")
      (p "The spec files are the " (em "first test case") " — because we can verify correctness "
         "by diffing G0 and G1 output. But the translator itself is target-agnostic: "
         "it translates SX syntax, not SX semantics. Every SX form has a "
         "straightforward Python equivalent.")
      (p "The roadmap:")
      (ul (~tw :tokens "list-disc pl-6 space-y-1 text-stone-700")
        (li (code "py.sx") " → Python — " (strong "done"))
        (li (code "js.sx") " → JavaScript (replaces " (code "bootstrap_js.py") ")")
        (li (code "go.sx") " → Go (new host)")
        (li (code "rs.sx") " → Rust (new host)")
        (li (code "hs.sx") " → Haskell (new host)"))
      (p "Each new host only needs: (1) a minimal evaluator to run "
         (code "{host}.sx") " once, and (2) the platform interface in the target language."))

    ;; -----------------------------------------------------------------------
    ;; Implications
    ;; -----------------------------------------------------------------------

    (~docs/section :title "Implications" :id "implications"
      (~docs/subsection :title "Practical"
        (p "One less Python file to maintain. Changes to the transpilation logic "
           "are written in SX and tested with the SX test harness. The spec and its "
           "compiler live in the same language."))

      (~docs/subsection :title "Architectural"
        (p "With " (code "z3.sx") " (SMT-LIB) and " (code "py.sx") " (Python), "
           "the pattern is clear: SX translators are SX programs. "
           "Adding a new target language means writing one " (code ".sx") " file, "
           "not a new Python compiler."))

      (~docs/subsection :title "Philosophical"
        (p "A self-hosting bootstrapper is a fixed point. The spec defines behavior. "
           "The translator is itself defined in terms of that behavior. Running the "
           "translator on the spec produces a program that can run the translator on "
           "the spec and get the same program.")
        (p "Gödel showed that any sufficiently powerful formal system can encode statements "
           "about itself. A self-hosting bootstrapper is the constructive version: "
           "the system doesn't just " (em "talk") " about itself, it " (em "builds") " itself.")))))
