diff --git a/sx/sx/geography/cek.sx b/sx/sx/geography/cek.sx index de31b92..fb3c6d3 100644 --- a/sx/sx/geography/cek.sx +++ b/sx/sx/geography/cek.sx @@ -473,6 +473,150 @@ + +;; --------------------------------------------------------------------------- +;; CEK Freeze / Thaw — serializable computation +;; --------------------------------------------------------------------------- + +(defcomp ~geography/cek/cek-freeze-content () + (~docs/page :title "Freeze / Thaw" + + (p :class "text-stone-500 text-sm italic mb-8" + "A computation is a value. Freeze it to an s-expression. " + "Store it, transmit it, content-address it. Thaw and resume anywhere.") + + (~docs/section :title "The idea" :id "idea" + (p "The CEK machine makes evaluation explicit: every step is a pure function from state to state. " + "The state is a dict with four fields:") + (ul :class "list-disc pl-6 mb-4 space-y-1 text-stone-600" + (li (code "control") " \u2014 the expression being evaluated") + (li (code "env") " \u2014 the bindings in scope") + (li (code "kont") " \u2014 the continuation (what to do with the result)") + (li (code "phase") " \u2014 eval or continue")) + (p "Since the state is data, it can be serialized. " + (code "cek-freeze") " converts a live CEK state to pure s-expressions. " + (code "cek-thaw") " reconstructs a live state from frozen SX. " + (code "cek-run") " resumes from where it left off.")) + + (~docs/section :title "Freeze" :id "freeze" + (p "Take a computation mid-flight and freeze it:") + (~docs/code :code (highlight + "(let ((expr (sx-parse \"(+ 1 (* 2 3))\"))\n (state (make-cek-state (first expr) (make-env) (list))))\n ;; Step 4 times\n (set! state (cek-step (cek-step (cek-step (cek-step state)))))\n ;; Freeze to SX\n (cek-freeze state))" + "lisp")) + (p "The frozen state is pure SX:") + (~docs/code :code (highlight + "{:phase \"continue\"\n :control nil\n :value 1\n :env {}\n :kont ({:type \"arg\"\n :f (primitive \"+\")\n :evaled ()\n :remaining ((* 2 3))\n :env {}})}" + "lisp")) + (p "Everything is data. The continuation frame says: \u201cI was adding 1 to something, " + "and I still need to evaluate " (code "(* 2 3)") ".\u201d")) + + (~docs/section :title "Thaw and resume" :id "thaw" + (p "Parse the frozen SX back. Thaw it. Resume:") + (~docs/code :code (highlight + "(let ((frozen (sx-parse frozen-text))\n (state (cek-thaw (first frozen))))\n (cek-run state))\n;; => 7" + "lisp")) + (p "Native functions like " (code "+") " serialize as " (code "(primitive \"+\")") + " and are looked up in the primitive registry on thaw. " + "Lambdas serialize as their source AST \u2014 " (code "(lambda (x) (* x 2))") + " \u2014 and reconstruct as callable functions.")) + + (~docs/section :title "Live demo" :id "demo" + (p "Type an expression, step to any point, freeze the state. " + "The frozen SX appears below. Click Thaw to resume from the frozen state.") + (~geography/cek/freeze-demo)) + + (~docs/section :title "What this enables" :id "enables" + (ul :class "list-disc pl-6 mb-4 space-y-2 text-stone-600" + (li (strong "Persistence") " \u2014 save reactive island state to localStorage, " + "resume on page reload") + (li (strong "Migration") " \u2014 freeze a computation on one machine, " + "thaw on another. Same result, deterministically.") + (li (strong "Content addressing") " \u2014 hash the frozen SX \u2192 CID. " + "A pointer to a computation in progress, not just a value.") + (li (strong "Time travel") " \u2014 freeze at each step, store the history. " + "Jump to any point. Undo. Branch.") + (li (strong "Verification") " \u2014 re-run from a frozen state, " + "check the result matches. Reproducible computation.")) + (p "The Platonic argument made concrete: a computation IS a value. " + "The Form persists. The instance resumes.")))) + + +(defisland ~geography/cek/freeze-demo () + (let ((source (signal "(+ 1 (* 2 3))")) + (state-sig (signal nil)) + (step-count (signal 0)) + (frozen-sx (signal "")) + (thaw-result (signal ""))) + (letrec + ((do-parse (fn () + (reset! frozen-sx "") + (reset! thaw-result "") + (reset! step-count 0) + (let ((parsed (sx-parse (deref source)))) + (when (not (empty? parsed)) + (reset! state-sig (make-cek-state (first parsed) (make-env) (list))))))) + (do-step (fn () + (when (and (deref state-sig) (not (cek-terminal? (deref state-sig)))) + (reset! state-sig (cek-step (deref state-sig))) + (swap! step-count inc)))) + (do-freeze (fn () + (when (deref state-sig) + (let ((frozen (cek-freeze (deref state-sig)))) + (reset! frozen-sx (sx-serialize frozen)))))) + (do-thaw (fn () + (when (not (empty? (deref frozen-sx))) + (let ((parsed (sx-parse (deref frozen-sx)))) + (when (not (empty? parsed)) + (let ((thawed (cek-thaw (first parsed)))) + (reset! thaw-result + (str "Resumed from step " (deref step-count) ": " + (cek-run thawed))))))))) + (do-run (fn () + (when (deref state-sig) + (let run-loop () + (when (not (cek-terminal? (deref state-sig))) + (do-step) + (run-loop))))))) + ;; Auto-parse + (effect (fn () (do-parse))) + (div :class "space-y-4" + ;; Input + (div :class "flex gap-2 items-end" + (div :class "flex-1" + (label :class "text-xs text-stone-400 block mb-1" "Expression") + (input :type "text" :bind source + :class "w-full px-3 py-1.5 rounded border border-stone-300 font-mono text-sm focus:outline-none focus:border-violet-400" + :on-change (fn (e) (do-parse)))) + (div :class "flex gap-1" + (button :on-click (fn (e) (do-step)) + :class "px-3 py-1.5 rounded bg-violet-500 text-white text-sm hover:bg-violet-600" + "Step") + (button :on-click (fn (e) (do-run)) + :class "px-3 py-1.5 rounded bg-violet-700 text-white text-sm hover:bg-violet-800" + "Run"))) + ;; Step count + freeze button + (div :class "flex items-center gap-3" + (span :class "text-sm text-stone-500 font-mono" + "Step " (deref step-count)) + (when (deref state-sig) + (button :on-click (fn (e) (do-freeze)) + :class "px-3 py-1.5 rounded bg-amber-500 text-white text-sm hover:bg-amber-600" + "Freeze"))) + ;; Frozen SX output + (when (not (empty? (deref frozen-sx))) + (div :class "space-y-2" + (label :class "text-xs text-stone-400 block" "Frozen CEK state") + (pre :class "text-xs font-mono bg-stone-50 rounded p-3 overflow-x-auto whitespace-pre-wrap text-stone-700" + (deref frozen-sx)) + (button :on-click (fn (e) (do-thaw)) + :class "px-3 py-1.5 rounded bg-emerald-600 text-white text-sm hover:bg-emerald-700" + "Thaw \u2192 Resume"))) + ;; Thaw result + (when (not (empty? (deref thaw-result))) + (div :class "rounded bg-emerald-50 border border-emerald-200 p-3 text-emerald-800 font-mono text-sm" + (deref thaw-result))))))) + + ;; --------------------------------------------------------------------------- ;; Demo page content ;; --------------------------------------------------------------------------- diff --git a/sx/sx/nav-data.sx b/sx/sx/nav-data.sx index 2a15bf4..3d46dcb 100644 --- a/sx/sx/nav-data.sx +++ b/sx/sx/nav-data.sx @@ -174,7 +174,9 @@ (dict :label "Overview" :href "/sx/(geography.(cek))" :summary "The CEK machine — explicit evaluator with Control, Environment, Kontinuation. Three registers, pure step function.") (dict :label "Demo" :href "/sx/(geography.(cek.demo))" - :summary "Live islands evaluated by the CEK machine. Counter, computed chains, reactive attributes — all through explicit continuation frames."))) + :summary "Live islands evaluated by the CEK machine. Counter, computed chains, reactive attributes — all through explicit continuation frames.") + (dict :label "Freeze / Thaw" :href "/sx/(geography.(cek.freeze))" + :summary "Serialize a CEK state to s-expressions. Ship it, store it, content-address it. Thaw and resume anywhere."))) (define plans-nav-items (list (dict :label "Status" :href "/sx/(etc.(plan.status))" diff --git a/sx/sx/page-functions.sx b/sx/sx/page-functions.sx index 8572b6b..91794c1 100644 --- a/sx/sx/page-functions.sx +++ b/sx/sx/page-functions.sx @@ -66,6 +66,7 @@ '(~geography/cek/cek-content) (case slug "demo" '(~geography/cek/cek-demo-content) + "freeze" '(~geography/cek/cek-freeze-content) :else '(~geography/cek/cek-content))))) (define provide