;; ---------------------------------------------------------------------------
;; Reader Macro Demo: #z3 — SX Spec to SMT-LIB (live translation via z3.sx)
;; ---------------------------------------------------------------------------

(defcomp ~plans/reader-macro-demo/z3-example (&key (sx-source :as string) (smt-output :as string))
  (div :class "grid grid-cols-1 md:grid-cols-2 gap-4"
    (div
      (p :class "text-xs text-stone-500 uppercase tracking-wider mb-1" "SX Source")
      (~docs/code :src (highlight sx-source "lisp")))
    (div
      (p :class "text-xs text-stone-500 uppercase tracking-wider mb-1" "SMT-LIB Output (live from z3.sx)")
      (~docs/code :src (highlight smt-output "lisp")))))

(defcomp ~plans/reader-macro-demo/plan-reader-macro-demo-content ()
  (~docs/page :title "Reader Macro Demo: #z3"

    (~docs/section :title "The idea" :id "idea"
      (p :class "text-stone-600"
        "SX spec files (" (code "primitives.sx") ", " (code "eval.sx") ") are machine-readable declarations. Reader macros transform these at parse time. " (code "#z3") " reads a " (code "define-primitive") " declaration and emits " (a :href "https://smtlib.cs.uiowa.edu/" :class "text-violet-600 hover:underline" "SMT-LIB") " — the standard input language for " (a :href "https://github.com/Z3Prover/z3" :class "text-violet-600 hover:underline" "Z3") " and other theorem provers.")
      (p :class "text-stone-600"
        "Same source, two interpretations. The bootstrappers read " (code "define-primitive") " and emit executable code. " (code "#z3") " reads the same form and emits verification conditions. The specification is simultaneously a program and a proof obligation.")
      (div :class "rounded border border-violet-200 bg-violet-50 p-4 mt-4"
        (p :class "text-sm text-violet-800 font-semibold mb-2" "Self-hosted")
        (p :class "text-sm text-violet-700"
          "The translator is written in SX itself (" (code "z3.sx") "). The SX evaluator executes " (code "z3.sx") " against the spec to produce SMT-LIB. Same pattern as " (code "bootstrap_js.py") " and " (code "bootstrap_py.py") ", but the transformation logic is an s-expression program transforming other s-expressions. All examples on this page are " (em "live output") " — not hardcoded strings.")))

    (~docs/section :title "Arithmetic primitives" :id "arithmetic"
      (p :class "text-stone-600"
        "Primitives with " (code ":body") " generate " (code "forall") " assertions. Z3 can verify the definition is satisfiable.")

      (~docs/subsection :title "inc"
        (~plans/reader-macro-demo/z3-example
          :sx-source "(define-primitive \"inc\"\n  :params (n)\n  :returns \"number\"\n  :doc \"Increment by 1.\"\n  :body (+ n 1))"
          :smt-output #z3(define-primitive "inc" :params (n) :returns "number" :doc "Increment by 1." :body (+ n 1))))

      (~docs/subsection :title "clamp"
        (p :class "text-stone-600 mb-2"
          (code "max") " and " (code "min") " have no SMT-LIB equivalent — translated to " (code "ite") " (if-then-else).")
        (~plans/reader-macro-demo/z3-example
          :sx-source "(define-primitive \"clamp\"\n  :params (x lo hi)\n  :returns \"number\"\n  :doc \"Clamp x to range [lo, hi].\"\n  :body (max lo (min hi x)))"
          :smt-output #z3(define-primitive "clamp" :params (x lo hi) :returns "number" :doc "Clamp x to range [lo, hi]." :body (max lo (min hi x))))))

    (~docs/section :title "Predicates" :id "predicates"
      (p :class "text-stone-600"
        "Predicates return " (code "Bool") " in SMT-LIB. " (code "mod") " and " (code "=") " are identity translations — same syntax in both languages.")

      (~docs/subsection :title "odd?"
        (~plans/reader-macro-demo/z3-example
          :sx-source "(define-primitive \"odd?\"\n  :params (n)\n  :returns \"boolean\"\n  :doc \"True if n is odd.\"\n  :body (= (mod n 2) 1))"
          :smt-output #z3(define-primitive "odd?" :params (n) :returns "boolean" :doc "True if n is odd." :body (= (mod n 2) 1))))

      (~docs/subsection :title "!= (inequality)"
        (~plans/reader-macro-demo/z3-example
          :sx-source "(define-primitive \"!=\"\n  :params (a b)\n  :returns \"boolean\"\n  :doc \"Inequality.\"\n  :body (not (= a b)))"
          :smt-output #z3(define-primitive "!=" :params (a b) :returns "boolean" :doc "Inequality." :body (not (= a b))))))

    (~docs/section :title "Variadics and bodyless" :id "variadics"
      (p :class "text-stone-600"
        "Variadic primitives (" (code "&rest") ") are declared as uninterpreted functions — Z3 can reason about their properties but not their implementation. Primitives without " (code ":body") " get only a declaration.")

      (~docs/subsection :title "+ (variadic)"
        (~plans/reader-macro-demo/z3-example
          :sx-source "(define-primitive \"+\"\n  :params (&rest args)\n  :returns \"number\"\n  :doc \"Sum all arguments.\")"
          :smt-output #z3(define-primitive "+" :params (&rest args) :returns "number" :doc "Sum all arguments.")))

      (~docs/subsection :title "nil? (no body)"
        (~plans/reader-macro-demo/z3-example
          :sx-source "(define-primitive \"nil?\"\n  :params (x)\n  :returns \"boolean\"\n  :doc \"True if x is nil/null/None.\")"
          :smt-output #z3(define-primitive "nil?" :params (x) :returns "boolean" :doc "True if x is nil/null/None."))))

    (~docs/section :title "Translate entire spec files" :id "full-specs"
      (p :class "text-stone-600"
        "The translator can process entire spec files. " (code "z3-translate-file") " in " (code "z3.sx") " filters for " (code "define-primitive") ", " (code "define-io-primitive") ", and " (code "define-special-form") " declarations, translates each, and concatenates the output.")
      (p :class "text-stone-600"
        "Below is the live SMT-LIB output from translating the full " (code "primitives.sx") " — all 87 primitive declarations. The composition is pure SX: " (code "(z3-translate-file (sx-parse (read-spec-file \"primitives.sx\")))") " — read the file, parse it, translate it. No Python glue.")

      (~docs/subsection :title "primitives.sx (87 primitives)"
        (~docs/code :src (highlight (z3-translate-file (sx-parse (read-spec-file "primitives.sx"))) "lisp"))))

    (~docs/section :title "The translator: z3.sx" :id "z3-source"
      (p :class "text-stone-600"
        "The entire translator is a single SX file — s-expressions that walk other s-expressions and emit strings. No host language logic. The same file runs in Python (server) and could run in JavaScript (browser) via the bootstrapped evaluator.")
      (~docs/code :src (highlight (read-spec-file "z3.sx") "lisp"))
      (p :class "text-stone-600 mt-4"
        "359 lines. The key functions: " (code "z3-sort") " maps SX types to SMT-LIB sorts. " (code "z3-expr") " recursively translates expressions — identity ops pass through unchanged, " (code "max") "/" (code "min") " become " (code "ite") ", predicates get renamed. " (code "z3-translate") " dispatches on form type. " (code "z3-translate-file") " filters and batch-translates."))

    (~docs/section :title "The pattern: SX → anything" :id "sx-to-anything"
      (p :class "text-stone-600"
        "z3.sx proves the pattern: an SX program that transforms SX ASTs into a target language. The same pattern works for any target.")
      (div :class "rounded border border-stone-200 bg-stone-50 p-4 mt-2 mb-4"
        (table :class "w-full text-sm"
          (thead (tr :class "text-left text-stone-500"
            (th :class "pb-2 pr-4" "File")
            (th :class "pb-2 pr-4" "Defines")
            (th :class "pb-2 pr-4" "Reader macro")
            (th :class "pb-2" "Output")))
          (tbody
            (tr :class "text-stone-700 border-t border-stone-200"
              (td :class "py-2 pr-4 font-mono text-xs" "z3.sx")
              (td :class "py-2 pr-4 font-mono text-xs" "z3-translate")
              (td :class "py-2 pr-4 font-mono text-xs" "#z3")
              (td :class "py-2" "SMT-LIB (theorem prover)"))
            (tr :class "text-stone-400 border-t border-stone-200"
              (td :class "py-2 pr-4 font-mono text-xs" "py.sx")
              (td :class "py-2 pr-4 font-mono text-xs" "py-translate")
              (td :class "py-2 pr-4 font-mono text-xs" "#py")
              (td :class "py-2" "Python source"))
            (tr :class "text-stone-400 border-t border-stone-200"
              (td :class "py-2 pr-4 font-mono text-xs" "js.sx")
              (td :class "py-2 pr-4 font-mono text-xs" "js-translate")
              (td :class "py-2 pr-4 font-mono text-xs" "#js")
              (td :class "py-2" "JavaScript source"))
            (tr :class "text-stone-400 border-t border-stone-200"
              (td :class "py-2 pr-4 font-mono text-xs" "dot.sx")
              (td :class "py-2 pr-4 font-mono text-xs" "dot-translate")
              (td :class "py-2 pr-4 font-mono text-xs" "#dot")
              (td :class "py-2" "Graphviz dot (dependency graphs)")))))
      (p :class "text-stone-600"
        "Each translator is a pure SX function from AST to string. Drop the " (code ".sx") " file in the ref directory, define " (code "name-translate") ", and " (code "#name") " works everywhere — server and client. No Python. No registration. No glue.")
      (p :class "text-stone-600"
        "A " (code "py.sx") " wouldn't be limited to the spec. Any SX expression could be translated: " (code "#py(map (fn (x) (* x x)) items)") " → " (code "list(map(lambda x: x * x, items))") ". The bootstrappers (" (code "bootstrap_js.py") ", " (code "bootstrap_py.py") ") are Python programs that do this for the full spec. " (code "py.sx") " would be the same thing, written in SX — a self-hosting bootstrapper."))

    (~docs/section :title "How it works" :id "how-it-works"
      (p :class "text-stone-600"
        "The " (code "#z3") " reader macro is registered before parsing. When the parser hits " (code "#z3(define-primitive ...)") ", it:")
      (ol :class "list-decimal pl-6 space-y-2 text-stone-600"
        (li "Reads the identifier " (code "z3") " after " (code "#") ".")
        (li "Looks for " (code "z3-translate") " in the component environment — found, because " (code "z3.sx") " was loaded at startup.")
        (li "Reads the next expression — the full " (code "define-primitive") " form — into an AST node.")
        (li "Calls the " (code "z3-translate") " Lambda with the AST.")
        (li (code "z3.sx") " walks the AST, extracts " (code ":params") ", " (code ":returns") ", " (code ":body") ", and emits SMT-LIB.")
        (li "The resulting string replaces " (code "#z3(...)") " in the parse output."))
      (p :class "text-stone-600"
        "No Python glue. The parser auto-resolves " (code "#name") " by looking for " (code "name-translate") " in the component env. Any " (code ".sx") " file that defines a " (code "name-translate") " function becomes a reader macro. A future " (code "py.sx") " defining " (code "py-translate") " would make " (code "#py") " work the same way — SX to Python.")
      (p :class "text-stone-600"
        "The handler is a pure function from AST to value. No side effects. No mutation. Reader macros are " (em "syntax transformations") " — they happen before evaluation, before rendering, before anything else. They are the earliest possible extension point."))

    (~docs/section :title "The strange loop" :id "strange-loop"
      (p :class "text-stone-600"
        "The SX specification files are simultaneously:")
      (ul :class "list-disc pl-6 space-y-2 text-stone-600"
        (li (span :class "font-semibold" "Executable code") " — bootstrappers compile them to JavaScript and Python.")
        (li (span :class "font-semibold" "Documentation") " — this docs site renders them with syntax highlighting and prose.")
        (li (span :class "font-semibold" "Formal specifications") " — " (code "#z3") " extracts verification conditions that a theorem prover can check."))
      (p :class "text-stone-600"
        "One file. Three readings. No information lost. The " (code "define-primitive") " form in " (code "primitives.sx") " does not need to be translated, annotated, or re-expressed for any of these uses. The s-expression " (em "is") " the program, the documentation, and the proof obligation.")
      (p :class "text-stone-600"
        "And the reader macro that extracts proofs? It is itself written in SX — " (code "z3.sx") ", 359 lines of s-expressions that transform other s-expressions. The SX evaluator (bootstrapped from " (code "eval.sx") ") executes " (code "z3.sx") " against " (code "primitives.sx") " to produce SMT-LIB. The transformation tools are made of the same material as the things they transform.")
      (p :class "text-stone-600"
        "There is no " (code "reader_z3.py") ". No Python translation logic. The parser sees " (code "#z3") ", finds " (code "z3-translate") " in the component env (loaded from " (code "z3.sx") " at startup), and calls it. The full spec translation calls " (code "(z3-translate-file (sx-parse (read-spec-file ...)))") " — three SX functions composed together. Same evaluator. Same translator. Same source. Different reader."))))
