From 8be8926155ae95b1892a69936c33525565d20c63 Mon Sep 17 00:00:00 2001 From: giles Date: Sun, 8 Mar 2026 20:39:41 +0000 Subject: [PATCH] Fix z3 demo code blocks: use (highlight ... "lisp") not :lang MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit ~doc-code only accepts :code — the :lang param was silently ignored. All code blocks now use (highlight "..." "lang") like the rest of the site. Co-Authored-By: Claude Opus 4.6 --- sx/sx/plans.sx | 39 +++++++++++++-------------------------- 1 file changed, 13 insertions(+), 26 deletions(-) diff --git a/sx/sx/plans.sx b/sx/sx/plans.sx index b91b69c..26c34f3 100644 --- a/sx/sx/plans.sx +++ b/sx/sx/plans.sx @@ -152,12 +152,10 @@ (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") - (~doc-code :lang "lisp" :code - "(define-primitive \"inc\"\n :params (n)\n :returns \"number\"\n :doc \"Increment by 1.\"\n :body (+ n 1))")) + (~doc-code :code (highlight "(define-primitive \"inc\"\n :params (n)\n :returns \"number\"\n :doc \"Increment by 1.\"\n :body (+ n 1))" "lisp"))) (div (p :class "text-xs text-stone-500 uppercase tracking-wider mb-1" "SMT-LIB Output") - (~doc-code :lang "lisp" :code - "; inc — Increment by 1.\n(declare-fun inc (Int) Int)\n(assert (forall (((n Int)))\n (= (inc n) (+ n 1))))\n(check-sat)")))) + (~doc-code :code (highlight "; inc — Increment by 1.\n(declare-fun inc (Int) Int)\n(assert (forall (((n Int)))\n (= (inc n) (+ n 1))))\n(check-sat)" "lisp")))) (~doc-subsection :title "clamp" (p :class "text-stone-600 mb-2" @@ -165,12 +163,10 @@ (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") - (~doc-code :lang "lisp" :code - "(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)))")) + (~doc-code :code (highlight "(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)))" "lisp"))) (div (p :class "text-xs text-stone-500 uppercase tracking-wider mb-1" "SMT-LIB Output") - (~doc-code :lang "lisp" :code - "; clamp — Clamp x to range [lo, hi].\n(declare-fun clamp (Int Int Int) Int)\n(assert (forall (((x Int) (lo Int) (hi Int)))\n (= (clamp x lo hi)\n (ite (>= lo (ite (<= hi x) hi x))\n lo\n (ite (<= hi x) hi x)))))\n(check-sat)"))))) + (~doc-code :code (highlight "; clamp — Clamp x to range [lo, hi].\n(declare-fun clamp (Int Int Int) Int)\n(assert (forall (((x Int) (lo Int) (hi Int)))\n (= (clamp x lo hi)\n (ite (>= lo (ite (<= hi x) hi x))\n lo\n (ite (<= hi x) hi x)))))\n(check-sat)" "lisp"))))) (~doc-section :title "Predicates" :id "predicates" (p :class "text-stone-600" @@ -180,23 +176,19 @@ (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") - (~doc-code :lang "lisp" :code - "(define-primitive \"odd?\"\n :params (n)\n :returns \"boolean\"\n :doc \"True if n is odd.\"\n :body (= (mod n 2) 1))")) + (~doc-code :code (highlight "(define-primitive \"odd?\"\n :params (n)\n :returns \"boolean\"\n :doc \"True if n is odd.\"\n :body (= (mod n 2) 1))" "lisp"))) (div (p :class "text-xs text-stone-500 uppercase tracking-wider mb-1" "SMT-LIB Output") - (~doc-code :lang "lisp" :code - "; odd? — True if n is odd.\n(declare-fun odd_p (Int) Bool)\n(assert (forall (((n Int)))\n (= (odd_p n) (= (mod n 2) 1))))\n(check-sat)")))) + (~doc-code :code (highlight "; odd? — True if n is odd.\n(declare-fun odd_p (Int) Bool)\n(assert (forall (((n Int)))\n (= (odd_p n) (= (mod n 2) 1))))\n(check-sat)" "lisp")))) (~doc-subsection :title "!= (inequality)" (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") - (~doc-code :lang "lisp" :code - "(define-primitive \"!=\"\n :params (a b)\n :returns \"boolean\"\n :doc \"Inequality.\"\n :body (not (= a b)))")) + (~doc-code :code (highlight "(define-primitive \"!=\"\n :params (a b)\n :returns \"boolean\"\n :doc \"Inequality.\"\n :body (not (= a b)))" "lisp"))) (div (p :class "text-xs text-stone-500 uppercase tracking-wider mb-1" "SMT-LIB Output") - (~doc-code :lang "lisp" :code - "; != — Inequality.\n(declare-fun neq (Int Int) Bool)\n(assert (forall (((a Int) (b Int)))\n (= (neq a b) (not (= a b)))))\n(check-sat)"))))) + (~doc-code :code (highlight "; != — Inequality.\n(declare-fun neq (Int Int) Bool)\n(assert (forall (((a Int) (b Int)))\n (= (neq a b) (not (= a b)))))\n(check-sat)" "lisp"))))) (~doc-section :title "Variadics and bodyless" :id "variadics" (p :class "text-stone-600" @@ -206,23 +198,19 @@ (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") - (~doc-code :lang "lisp" :code - "(define-primitive \"+\"\n :params (&rest args)\n :returns \"number\"\n :doc \"Sum all arguments.\")")) + (~doc-code :code (highlight "(define-primitive \"+\"\n :params (&rest args)\n :returns \"number\"\n :doc \"Sum all arguments.\")" "lisp"))) (div (p :class "text-xs text-stone-500 uppercase tracking-wider mb-1" "SMT-LIB Output") - (~doc-code :lang "lisp" :code - "; + — Sum all arguments.\n; (variadic — modeled as uninterpreted)\n(declare-fun + (Int Int) Int)\n(check-sat)")))) + (~doc-code :code (highlight "; + — Sum all arguments.\n; (variadic — modeled as uninterpreted)\n(declare-fun + (Int Int) Int)\n(check-sat)" "lisp"))))) (~doc-subsection :title "nil? (no body)" (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") - (~doc-code :lang "lisp" :code - "(define-primitive \"nil?\"\n :params (x)\n :returns \"boolean\"\n :doc \"True if x is nil/null/None.\")")) + (~doc-code :code (highlight "(define-primitive \"nil?\"\n :params (x)\n :returns \"boolean\"\n :doc \"True if x is nil/null/None.\")" "lisp"))) (div (p :class "text-xs text-stone-500 uppercase tracking-wider mb-1" "SMT-LIB Output") - (~doc-code :lang "lisp" :code - "; nil? — True if x is nil/null/None.\n(declare-fun nil_p (Int) Bool)\n(check-sat)"))))) + (~doc-code :code (highlight "; nil? — True if x is nil/null/None.\n(declare-fun nil_p (Int) Bool)\n(check-sat)" "lisp")))))) (~doc-section :title "How it works" :id "how-it-works" (p :class "text-stone-600" @@ -234,8 +222,7 @@ (li "Passes the AST to the handler function.") (li "The handler 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.")) - (~doc-code :lang "python" :code - "# Registration — one line\nfrom shared.sx.ref.reader_z3 import register_z3_macro\nregister_z3_macro()\n\n# Then #z3 works in any SX source:\nresult = parse('#z3(define-primitive \"inc\" ...)')\n# result is the SMT-LIB string") + (~doc-code :code (highlight "# Registration — one line\nfrom shared.sx.ref.reader_z3 import register_z3_macro\nregister_z3_macro()\n\n# Then #z3 works in any SX source:\nresult = parse('#z3(define-primitive \"inc\" ...)')\n# result is the SMT-LIB string" "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."))