giles
3ca89ef765
- z3.sx: SX-to-SMT-LIB translator written in SX (359 lines), replaces Python translation logic - prove.sx: SMT-LIB satisfiability checker in SX — proves all 91 primitives sat by construction - Parser: support unicode characters (em-dash, accented letters) in symbols - Auto-resolve reader macros: #name finds name-translate in component env, no Python registration - Platform primitives: type-of, symbol-name, keyword-name, sx-parse registered in primitives.py - Cond heuristic: predicates ending in ? recognized as Clojure-style tests - Library loading: z3.sx loaded at startup with reload callbacks for hot-reload ordering - reader_z3.py: rewritten as thin shell delegating to z3.sx - Split monolithic .sx files: essays (22), plans (13), reactive-islands (6) into separate files Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
111 lines
9.5 KiB
Plaintext
111 lines
9.5 KiB
Plaintext
;; ---------------------------------------------------------------------------
|
|
;; Reader Macros
|
|
;; ---------------------------------------------------------------------------
|
|
|
|
(defcomp ~plan-reader-macros-content ()
|
|
(~doc-page :title "Reader Macros"
|
|
|
|
(~doc-section :title "Context" :id "context"
|
|
(p "SX has three hardcoded reader transformations: " (code "`") " → " (code "(quasiquote ...)") ", " (code ",") " → " (code "(unquote ...)") ", " (code ",@") " → " (code "(splice-unquote ...)") ". These are baked into the parser with no extensibility. The " (code "~") " prefix for components and " (code "&") " for param modifiers are just symbol characters, handled at eval time.")
|
|
(p "Reader macros add parse-time transformations triggered by a dispatch character. Motivating use case: a " (code "~md") " component that uses heredoc syntax for markdown source instead of string literals. More broadly: datum comments, raw strings, and custom literal syntax."))
|
|
|
|
(~doc-section :title "Design" :id "design"
|
|
|
|
(~doc-subsection :title "Dispatch Character: #"
|
|
(p "Lisp tradition. " (code "#") " is NOT in " (code "ident-start") " or " (code "ident-char") " — completely free. Pattern:")
|
|
(~doc-code :code (highlight "#;expr → (read and discard expr, return next)\n#|...| → raw string literal\n#'expr → (quote expr)" "lisp")))
|
|
|
|
(~doc-subsection :title "#; — Datum comment"
|
|
(p "Scheme/Racket standard. Reads and discards the next expression. Preserves balanced parens.")
|
|
(~doc-code :code (highlight "(list 1 #;(this is commented out) 2 3) → (list 1 2 3)" "lisp")))
|
|
|
|
(~doc-subsection :title "#|...| — Raw string"
|
|
(p "No escape processing. Everything between " (code "#|") " and " (code "|") " is literal. Enables inline markdown, regex patterns, code examples.")
|
|
(~doc-code :code (highlight "(~md #|## Title\n\nSome **bold** text with \"quotes\" and \\backslashes.|)" "lisp")))
|
|
|
|
(~doc-subsection :title "#' — Quote shorthand"
|
|
(p "Currently no single-char quote (" (code "`") " is quasiquote).")
|
|
(~doc-code :code (highlight "#'my-function → (quote my-function)" "lisp")))
|
|
|
|
(~doc-subsection :title "Extensible dispatch: #name"
|
|
(p "User-defined reader macros via " (code "#name expr") ". The parser reads an identifier after " (code "#") ", looks up a handler in the reader macro registry, and calls it with the next parsed expression. See the " (a :href "/plans/reader-macro-demo" :class "text-violet-600 hover:underline" "#z3 demo") " for a working example that translates SX spec declarations to SMT-LIB.")))
|
|
|
|
|
|
;; -----------------------------------------------------------------------
|
|
;; Implementation
|
|
;; -----------------------------------------------------------------------
|
|
|
|
(~doc-section :title "Implementation" :id "implementation"
|
|
|
|
(~doc-subsection :title "1. Spec: parser.sx"
|
|
(p "Add " (code "#") " dispatch to " (code "read-expr") " (after the " (code ",") "/" (code ",@") " case, before number). Add " (code "read-raw-string") " helper function.")
|
|
(~doc-code :code (highlight ";; Reader macro dispatch\n(= ch \"#\")\n (do (set! pos (inc pos))\n (if (>= pos len-src)\n (error \"Unexpected end of input after #\")\n (let ((dispatch-ch (nth source pos)))\n (cond\n ;; #; — datum comment: read and discard next expr\n (= dispatch-ch \";\")\n (do (set! pos (inc pos))\n (read-expr) ;; read and discard\n (read-expr)) ;; return the NEXT expr\n\n ;; #| — raw string\n (= dispatch-ch \"|\")\n (do (set! pos (inc pos))\n (read-raw-string))\n\n ;; #' — quote shorthand\n (= dispatch-ch \"'\")\n (do (set! pos (inc pos))\n (list (make-symbol \"quote\") (read-expr)))\n\n :else\n (error (str \"Unknown reader macro: #\" dispatch-ch))))))" "lisp"))
|
|
(p "The " (code "read-raw-string") " helper:")
|
|
(~doc-code :code (highlight "(define read-raw-string\n (fn ()\n (let ((buf \"\"))\n (define raw-loop\n (fn ()\n (if (>= pos len-src)\n (error \"Unterminated raw string\")\n (let ((ch (nth source pos)))\n (if (= ch \"|\")\n (do (set! pos (inc pos)) nil) ;; done\n (do (set! buf (str buf ch))\n (set! pos (inc pos))\n (raw-loop)))))))\n (raw-loop)\n buf)))" "lisp")))
|
|
|
|
(~doc-subsection :title "2. Python: parser.py"
|
|
(p "Add " (code "#") " dispatch to " (code "_parse_expr()") " (after " (code ",") "/" (code ",@") " handling ~line 252). Add " (code "_read_raw_string()") " method to Tokenizer.")
|
|
(~doc-code :code (highlight "# In _parse_expr(), after the comma/splice-unquote block:\nif raw == \"#\":\n tok._advance(1) # consume the #\n if tok.pos >= len(tok.text):\n raise ParseError(\"Unexpected end of input after #\",\n tok.pos, tok.line, tok.col)\n dispatch = tok.text[tok.pos]\n if dispatch == \";\":\n tok._advance(1)\n _parse_expr(tok) # read and discard\n return _parse_expr(tok) # return next\n if dispatch == \"|\":\n tok._advance(1)\n return tok._read_raw_string()\n if dispatch == \"'\":\n tok._advance(1)\n return [Symbol(\"quote\"), _parse_expr(tok)]\n raise ParseError(f\"Unknown reader macro: #{dispatch}\",\n tok.pos, tok.line, tok.col)" "python"))
|
|
(p "The " (code "_read_raw_string()") " method on Tokenizer:")
|
|
(~doc-code :code (highlight "def _read_raw_string(self) -> str:\n buf = []\n while self.pos < len(self.text):\n ch = self.text[self.pos]\n if ch == \"|\":\n self._advance(1)\n return \"\".join(buf)\n buf.append(ch)\n self._advance(1)\n raise ParseError(\"Unterminated raw string\",\n self.pos, self.line, self.col)" "python")))
|
|
|
|
(~doc-subsection :title "3. JS: auto-transpiled"
|
|
(p "JS parser comes from bootstrap of parser.sx — spec change handles it automatically."))
|
|
|
|
(~doc-subsection :title "4. Rebootstrap both targets"
|
|
(p "Run " (code "bootstrap_js.py") " and " (code "bootstrap_py.py") " to regenerate " (code "sx-ref.js") " and " (code "sx_ref.py") " from the updated parser.sx spec."))
|
|
|
|
(~doc-subsection :title "5. Grammar update"
|
|
(p "Add reader macro syntax to the grammar comment at the top of parser.sx:")
|
|
(~doc-code :code (highlight ";; reader → '#;' expr (datum comment)\n;; | '#|' raw-chars '|' (raw string)\n;; | \"#'\" expr (quote shorthand)" "lisp"))))
|
|
|
|
;; -----------------------------------------------------------------------
|
|
;; Files
|
|
;; -----------------------------------------------------------------------
|
|
|
|
(~doc-section :title "Files" :id "files"
|
|
(div :class "overflow-x-auto rounded border border-stone-200"
|
|
(table :class "w-full text-left text-sm"
|
|
(thead (tr :class "border-b border-stone-200 bg-stone-100"
|
|
(th :class "px-3 py-2 font-medium text-stone-600" "File")
|
|
(th :class "px-3 py-2 font-medium text-stone-600" "Change")))
|
|
(tbody
|
|
(tr :class "border-b border-stone-100"
|
|
(td :class "px-3 py-2 font-mono text-sm text-violet-700" "shared/sx/ref/parser.sx")
|
|
(td :class "px-3 py-2 text-stone-700" "# dispatch in read-expr, read-raw-string helper, grammar comment"))
|
|
(tr :class "border-b border-stone-100"
|
|
(td :class "px-3 py-2 font-mono text-sm text-violet-700" "shared/sx/parser.py")
|
|
(td :class "px-3 py-2 text-stone-700" "# dispatch in _parse_expr(), _read_raw_string()"))
|
|
(tr :class "border-b border-stone-100"
|
|
(td :class "px-3 py-2 font-mono text-sm text-violet-700" "shared/sx/ref/sx_ref.py")
|
|
(td :class "px-3 py-2 text-stone-700" "Rebootstrap"))
|
|
(tr :class "border-b border-stone-100"
|
|
(td :class "px-3 py-2 font-mono text-sm text-violet-700" "shared/static/scripts/sx-ref.js")
|
|
(td :class "px-3 py-2 text-stone-700" "Rebootstrap"))))))
|
|
|
|
;; -----------------------------------------------------------------------
|
|
;; Verification
|
|
;; -----------------------------------------------------------------------
|
|
|
|
(~doc-section :title "Verification" :id "verification"
|
|
|
|
(~doc-subsection :title "Parse tests"
|
|
(ul :class "list-disc pl-5 text-stone-700 space-y-1 font-mono text-sm"
|
|
(li "#;(ignored) 42 → 42")
|
|
(li "(list 1 #;2 3) → (list 1 3)")
|
|
(li "#|hello \"world\" \\n| → string: hello \"world\" \\n (literal, no escaping)")
|
|
(li "#|multi\\nline| → string with actual newline")
|
|
(li "#'foo → (quote foo)")
|
|
(li "# at EOF → error")
|
|
(li "#x unknown → error")))
|
|
|
|
(~doc-subsection :title "Regression"
|
|
(ul :class "list-disc pl-5 text-stone-700 space-y-1"
|
|
(li "All existing parser tests pass after changes")
|
|
(li "Rebootstrapped JS and Python pass their test suites")
|
|
(li "JS parity: SX.parse('#|hello|') returns [\"hello\"]"))))))
|
|
|
|
;; ---------------------------------------------------------------------------
|
|
;; Reader Macro Demo: #z3 — SX Spec to SMT-LIB
|
|
;; ---------------------------------------------------------------------------
|