;;; proof-netspace-client.lsp — query the proof netspace server.
;;;
;;; Three passes:
;;;
;;;   1. Verify each of five EML theorems per-proof (PROVEN / UNKNOWN).
;;;   2. Fetch the whole envelope — the server's full solution space
;;;      ships back in one round-trip as (envelope (h1 h2 ...)).
;;;   3. Merge our own envelope back + one synthetic hash. Server
;;;      reports (merged 1) proving the synthetic was the only new
;;;      entry and the rest were already known.
;;;
;;; Two nodes can chain (envelope) + (merge ...) in either direction
;;; until both hold the union of what either knew.
;;;
;;; Usage (start the server first):
;;;   python3 lumbda.py --fast examples/proof-netspace-client.lsp
;;;   ./c/lumbda examples/proof-netspace-client.lsp
;;;   ./asm/lumbda < examples/proof-netspace-client.lsp

(define *host* "127.0.0.1")
(define *port* 9086)

;;; ─── Canonical serializer (matches server) ─────────────────

(define (atom->string v)
  (cond
    ((number? v) (number->string v))
    ((symbol? v) (symbol->string v))
    ((null? v)   "()")
    ((pair? v)   (string-append "(" (list->str v) ")"))
    (else        "?")))

(define (list->str lst)
  (cond
    ((null? lst) "")
    ((null? (cdr lst)) (atom->string (car lst)))
    (else (string-append (atom->string (car lst)) " "
                         (list->str (cdr lst))))))

;;; ─── One-shot TCP round-trip ───────────────────────────────

(define (request str)
  (let ((sock (tcp-connect *host* *port*)))
    (if sock
        (begin
          (tcp-send sock str)
          (let ((resp (tcp-recv sock 65536)))
            (tcp-close sock)
            (if resp resp "NO-RESPONSE")))
        "NO-CONNECT")))

;;; ─── Per-proof verification ────────────────────────────────

(define (ask lhs rhs)
  (request (string-append "(" (atom->string lhs) " "
                              (atom->string rhs) ")")))

(define (probe name lhs rhs)
  (let ((t0 (current-time-ms)))
    (let ((resp (ask lhs rhs)))
      (let ((t1 (current-time-ms)))
        (display name) (display ": ")
        (display (- t1 t0)) (display " ms   ")
        (display resp)))))

;;; ─── Envelope teleport ─────────────────────────────────────

(define (count-items form n)
  ;; Return length of a list form; used to count hashes in envelope.
  (if (pair? form) (count-items (cdr form) (+ n 1)) n))

(define (parse-envelope resp)
  ;; resp = "(envelope (h1 h2 ...))\n" — return the inner list.
  (let ((form (read-from-string resp)))
    (if (and (pair? form) (eqv? (car form) 'envelope) (pair? (cdr form)))
        (car (cdr form))
        '())))

(define (hashes->string lst acc)
  (if (null? lst) acc
      (hashes->string (cdr lst)
                      (string-append acc (number->string (car lst)) " "))))

(define (fetch-envelope)
  (let ((t0 (current-time-ms)))
    (let ((resp (request "(envelope)")))
      (let ((t1 (current-time-ms)))
        (display "envelope     : ") (display (- t1 t0)) (display " ms   ")
        (let ((hashes (parse-envelope resp)))
          (display (count-items hashes 0))
          (display " hashes teleported") (newline)
          hashes)))))

(define (merge-envelope hashes synthetic)
  ;; Send the server its own envelope back plus one synthetic hash.
  ;; Expected reply: (merged 1) — only the synthetic was new.
  (let ((t0 (current-time-ms)))
    (let ((payload (string-append "(merge ("
                                  (hashes->string hashes "")
                                  (number->string synthetic) "))")))
      (let ((resp (request payload)))
        (let ((t1 (current-time-ms)))
          (display "merge        : ") (display (- t1 t0)) (display " ms   ")
          (display resp))))))

;;; ─── Run ───────────────────────────────────────────────────

(display "querying proof netspace at ") (display *host*) (display ":")
(display *port*) (newline)
(newline)

(probe "eml_is_exp   "  '(eml ?x 1)  '(exp ?x))
(probe "eml_is_e     "  '(eml 1 1)   '(exp 1))
(probe "eml_is_ln    "  '(eml 1 (eml (eml 1 ?x) 1))  '(ln ?x))
(probe "eml_is_zero  "  '(eml 1 (eml (eml 1 1) 1))   0)
(probe "eml_is_sub   "  '(eml (ln ?a) (exp ?b))      '(- ?a ?b))
(newline)

(define env (fetch-envelope))
(merge-envelope env 999999999)
(newline)

(display "done") (newline)