spw.rkt

#lang racket
(require redex)

;; ═══════════════════════════════════════════════════════════════════
;; SPW.CORE — Formal Semantics in PLT Redex
;; 
;; 5 Operators, 3 Clusters:
;;   FLOW:      ~ (chain)    -> (lower)
;;   QUERY:     ? (probe)    ! (force)
;;   STRUCTURE: ^ (annotate)
;; ═══════════════════════════════════════════════════════════════════


;; ═══════════════════════════════════════════════════════════════════
;; § 1. SURFACE SYNTAX
;; ═══════════════════════════════════════════════════════════════════

(define-language Spw-Surface
  
  ;; Surface expressions (what you type)
  (surf ::= x
            lit
            (surf)                    ; grouping
            
            ;; Prefix position
            (op-pre op surf)          ; !x  ~x  ?x  ^x
            
            ;; Postfix position  
            (op-post surf op)         ; x!  x~  x?  x^
            
            ;; Infix position
            (op-in surf op surf)      ; x ~ y   x -> y   x ^ tag
            
            ;; Bracket coupling (surface)
            (couple surf surf ())     ; x <> y ()
            (couple surf surf [])     ; x <> y []
            (couple surf surf {}))    ; x <> y {}
  
  ;; The 5 core operators
  (op ::= ~ -> ? ! ^)
  
  ;; Atoms
  (x ::= variable-not-otherwise-mentioned)
  (lit ::= number string boolean))


;; ═══════════════════════════════════════════════════════════════════
;; § 2. CORE AST (desugared/lowered)
;; ═══════════════════════════════════════════════════════════════════

(define-language Spw-AST
  
  ;; AST nodes
  (ast ::= x
           lit
           
           ;; === SEMANTIC nodes (affect evaluation) ===
           (Unary op ast dir)              ; op applied to ast
           (Binary op ast ast)             ; infix application
           (Query mode ast)                ; ? forms
           (Flow ast ast)                  ; ~ chaining
           (Lower ast ast)                 ; -> boundary cross
           (Force ast)                     ; ! forcing
           (Coupled phase ast ast)         ; bracket coupling result
           
           ;; === HINT nodes (metadata only, no eval effect) ===
           (Hint ast meta))
  
  ;; Direction for unary
  (dir ::= pre post)
  
  ;; Query modes
  (mode ::= probe     ; prefix ?  — execute/introspect
            flag)     ; postfix ? — mark for review
  
  ;; Coupling phases (bracket-determined)
  (phase ::= transient   ; ()
             cycle       ; []
             frozen)     ; {}
  
  ;; Hint metadata
  (meta ::= (pin)
            (label x)
            (tag x)
            (relax)
            (accumulate))
  
  ;; Atoms (same as surface)
  (op ::= ~ -> ? ! ^)
  (x ::= variable-not-otherwise-mentioned)
  (lit ::= number string boolean))


;; ═══════════════════════════════════════════════════════════════════
;; § 3. LOWERING: Surface → AST
;; ═══════════════════════════════════════════════════════════════════

(define-metafunction Spw-Surface
  lower : surf -> any  ;; produces Spw-AST term
  
  ;; Atoms pass through
  [(lower x) x]
  [(lower lit) lit]
  
  ;; Grouping
  [(lower (surf)) (lower surf)]
  
  ;; ─── CLUSTER 1: FLOW (~, ->) ─────────────────────────────────────
  
  ;; ~ prefix: soften (semantic)
  [(lower (op-pre ~ surf))
   (Unary ~ (lower surf) pre)]
  
  ;; ~ postfix: relax hint (non-semantic)
  [(lower (op-post surf ~))
   (Hint (lower surf) (relax))]
  
  ;; ~ infix: FLOW (semantic — context threads)
  [(lower (op-in surf_1 ~ surf_2))
   (Flow (lower surf_1) (lower surf_2))]
  
  ;; -> infix only: LOWER (semantic — boundary cross)
  [(lower (op-in surf_1 -> surf_2))
   (Lower (lower surf_1) (lower surf_2))]
  
  ;; -> prefix/postfix: ERROR (-> only valid at boundaries)
  [(lower (op-pre -> surf))
   ,(error 'lower "-> invalid in prefix position")]
  [(lower (op-post surf ->))
   ,(error 'lower "-> invalid in postfix position")]
  
  ;; ─── CLUSTER 2: QUERY/FORCE (?, !) ───────────────────────────────
  
  ;; ? prefix: PROBE (semantic — executes)
  [(lower (op-pre ? surf))
   (Query probe (lower surf))]
  
  ;; ? postfix: FLAG (semantic but non-mutating)
  [(lower (op-post surf ?))
   (Query flag (lower surf))]
  
  ;; ? infix: guard/conditional (semantic)
  [(lower (op-in surf_1 ? surf_2))
   (Binary ? (lower surf_1) (lower surf_2))]
  
  ;; ! prefix: FORCE (semantic — surge)
  [(lower (op-pre ! surf))
   (Force (lower surf))]
  
  ;; ! postfix: assert-flag hint (non-semantic)
  [(lower (op-post surf !))
   (Hint (lower surf) (pin))]
  
  ;; ! infix: assert against (semantic)
  [(lower (op-in surf_1 ! surf_2))
   (Binary ! (lower surf_1) (lower surf_2))]
  
  ;; ─── CLUSTER 3: STRUCTURE (^) ────────────────────────────────────
  
  ;; ^ prefix: label hint (non-semantic)
  [(lower (op-pre ^ surf))
   (Hint (lower surf) (label anon))]
  
  ;; ^ postfix: pin hint (non-semantic)
  [(lower (op-post surf ^))
   (Hint (lower surf) (pin))]
  
  ;; ^ infix: named label hint (non-semantic)
  [(lower (op-in surf_1 ^ x))
   (Hint (lower surf_1) (label x))]
  
  ;; ─── COUPLING ────────────────────────────────────────────────────
  
  [(lower (couple surf_1 surf_2 ()))
   (Coupled transient (lower surf_1) (lower surf_2))]
  
  [(lower (couple surf_1 surf_2 []))
   (Coupled cycle (lower surf_1) (lower surf_2))]
  
  [(lower (couple surf_1 surf_2 {}))
   (Coupled frozen (lower surf_1) (lower surf_2))])


;; ═══════════════════════════════════════════════════════════════════
;; § 4. REPL STATE
;; ═══════════════════════════════════════════════════════════════════

(define-extended-language Spw-REPL Spw-AST
  
  ;; REPL state configuration
  (state ::= (repl-state ctx result pinned canon))
  
  ;; Context (what ~ threads through)
  (ctx ::= (context focus lhs result-set))
  
  (focus ::= ast none)           ; current focus
  (lhs ::= ast none)             ; left-hand side of chain
  (result-set ::= (ast ...))     ; accumulated results
  
  ;; Result of last evaluation
  (result ::= ast none)
  
  ;; Pinned values (from ^)
  (pinned ::= ((x ast) ...))
  
  ;; Canon (lowered/committed values from ->)
  (canon ::= (ast ...))
  
  ;; Values
  (v ::= lit x (forced v) (flagged v) (soft v) (lowered v)))


;; Initial REPL state
(define init-state
  (term (repl-state 
         (context none none ())
         none
         ()
         ())))


;; ═══════════════════════════════════════════════════════════════════
;; § 5. REPL STEP SEMANTICS
;; ═══════════════════════════════════════════════════════════════════

(define repl-step
  (reduction-relation
   Spw-REPL
   #:domain (ast state)
   
   ;; ─── VALUES (no reduction) ──────────────────────────────────────
   ;; Literals and variables are values; update result
   (--> (lit (repl-state ctx result pinned canon))
        (lit (repl-state ctx lit pinned canon))
        "lit-val")
   
   (--> (x (repl-state ctx result pinned canon))
        (x (repl-state ctx x pinned canon))
        "var-val")
   
   
   ;; ═══ CLUSTER 1: FLOW ════════════════════════════════════════════
   
   ;; ~ prefix: wrap in soft (deferred)
   (--> ((Unary ~ ast pre) 
         (repl-state ctx result pinned canon))
        ((soft ast) 
         (repl-state ctx (soft ast) pinned canon))
        "~-pre-soften")
   
   ;; ~ infix (Flow): chain with context threading
   ;; Key: lhs becomes available in context, focus shifts to rhs
   (--> ((Flow v ast_2)
         (repl-state (context focus_old lhs_old result-set) result pinned canon))
        (ast_2
         (repl-state (context ast_2 v (v ... result-set)) result pinned canon))
        (where (v ...) result-set)
        "~-flow-chain")
   
   ;; soft realizes when inner is value
   (--> ((soft v)
         (repl-state ctx result pinned canon))
        (v
         (repl-state ctx v pinned canon))
        "soft-realize")
   
   ;; -> infix (Lower): commit, add to canon, CLEAR context
   (--> ((Lower v_1 v_2)
         (repl-state ctx result pinned canon))
        ((lowered v_2)
         (repl-state (context none none ()) (lowered v_2) pinned (v_2 ... canon)))
        (where (v_2 ...) canon)
        "->-lower-commit")
   
   
   ;; ═══ CLUSTER 2: QUERY/FORCE ═════════════════════════════════════
   
   ;; ? prefix (probe): execute and return
   (--> ((Query probe v)
         (repl-state ctx result pinned canon))
        (v
         (repl-state ctx v pinned canon))
        "?-probe")
   
   ;; ? postfix (flag): mark but DON'T mutate context
   ;; This is the "postfix ? non-mutation" law
   (--> ((Query flag v)
         (repl-state ctx result pinned canon))
        ((flagged v)
         (repl-state ctx result pinned canon))  ; result unchanged!
        "?-flag-no-mutate")
   
   ;; ! prefix (force): surge, make it happen
   (--> ((Force v)
         (repl-state ctx result pinned canon))
        ((forced v)
         (repl-state ctx (forced v) pinned canon))
        "!-force")
   
   ;; ? infix (guard): check condition
   (--> ((Binary ? v_1 v_2)
         (repl-state ctx result pinned canon))
        (v_1  ; simplified: return guarded value
         (repl-state ctx v_1 pinned canon))
        "?-guard")
   
   ;; ! infix (assert): force with check
   (--> ((Binary ! v_1 v_2)
         (repl-state ctx result pinned canon))
        ((forced v_1)
         (repl-state ctx (forced v_1) pinned canon))
        "!-assert")
   
   
   ;; ═══ CLUSTER 3: STRUCTURE ═══════════════════════════════════════
   
   ;; Hints pass through (non-semantic!)
   ;; They may update pinned but don't affect evaluation
   (--> ((Hint v (label x))
         (repl-state ctx result pinned canon))
        (v
         (repl-state ctx result ((x v) ... pinned) canon))
        (where ((x v) ...) pinned)
        "^-label-hint")
   
   (--> ((Hint v (pin))
         (repl-state ctx result pinned canon))
        (v
         (repl-state ctx result pinned canon))
        "^-pin-hint")
   
   (--> ((Hint v (relax))
         (repl-state ctx result pinned canon))
        (v
         (repl-state ctx result pinned canon))
        "~-relax-hint")
   
   
   ;; ═══ COUPLING ═══════════════════════════════════════════════════
   
   (--> ((Coupled phase v_1 v_2)
         (repl-state ctx result pinned canon))
        ((Coupled phase v_1 v_2)
         (repl-state ctx (Coupled phase v_1 v_2) pinned canon))
        "coupled-val")))


;; ═══════════════════════════════════════════════════════════════════
;; § 6. PROPERTIES & LAWS
;; ═══════════════════════════════════════════════════════════════════

;; LAW 1: "postfix ? non-mutation"
;; Flagging should not change the result in context
(define (law:postfix-?-no-mutate)
  (redex-check 
   Spw-REPL
   v
   (let* ([before-result (term (repl-state (context none none ()) some-result () ()))]
          [flagged-term (term (Query flag v))]
          [stepped (apply-reduction-relation repl-step (term (,flagged-term ,before-result)))])
     (for/and ([s stepped])
       (match s
         [`(,_ (repl-state ,_ some-result ,_ ,_)) #t]
         [_ #f])))
   #:attempts 100))

;; LAW 2: "-> only at boundaries (syntactic)"
;; Lower should not appear in prefix/postfix in well-formed surface
(define (law:lower-boundary-only)
  (redex-check
   Spw-Surface
   surf
   (not (redex-match? Spw-Surface (op-pre -> surf_1) (term surf)))
   #:attempts 100))

;; LAW 3: "hints don't change evaluation result"
(define (law:hints-transparent)
  (redex-check
   Spw-REPL
   v
   (let* ([state (term (repl-state (context none none ()) none () ()))]
          [direct (apply-reduction-relation* repl-step (term (v ,state)))]
          [hinted (apply-reduction-relation* repl-step 
                    (term ((Hint v (pin)) ,state)))])
     ;; Both should reach same value (ignoring state)
     (equal? (map car direct) (map car hinted)))
   #:attempts 100))

;; LAW 4: "~ preserves context, -> clears it"
(define (law:flow-vs-lower-context)
  (redex-check
   Spw-REPL
   (v_1 v_2)
   (let* ([state (term (repl-state (context none none ()) none () ()))]
          ;; Flow should have v_1 in result-set after
          [flow-result (apply-reduction-relation repl-step 
                         (term ((Flow v_1 v_2) ,state)))]
          ;; Lower should have empty context after
          [lower-result (apply-reduction-relation repl-step
                          (term ((Lower v_1 v_2) ,state)))])
     (and 
      ;; Flow: v_1 appears in result-set
      (for/or ([r flow-result])
        (match r
          [`(,_ (repl-state (context ,_ ,_ (,v_1 . ,_)) ,_ ,_ ,_)) #t]
          [_ #f]))
      ;; Lower: context is cleared
      (for/or ([r lower-result])
        (match r
          [`(,_ (repl-state (context none none ()) ,_ ,_ ,_)) #t]
          [_ #f]))))
   #:attempts 50))


;; ═══════════════════════════════════════════════════════════════════
;; § 7. TESTS & EXAMPLES
;; ═══════════════════════════════════════════════════════════════════

(module+ test
  (require rackunit)
  
  ;; ─── Lowering tests ──────────────────────────────────────────────
  
  ;; ~ prefix → semantic Unary
  (check-equal?
   (term (lower (op-pre ~ x)))
   (term (Unary ~ x pre)))
  
  ;; ~ postfix → Hint (non-semantic)
  (check-equal?
   (term (lower (op-post x ~)))
   (term (Hint x (relax))))
  
  ;; ~ infix → Flow
  (check-equal?
   (term (lower (op-in a ~ b)))
   (term (Flow a b)))
  
  ;; -> infix → Lower
  (check-equal?
   (term (lower (op-in draft -> final)))
   (term (Lower draft final)))
  
  ;; ? prefix → Query probe
  (check-equal?
   (term (lower (op-pre ? x)))
   (term (Query probe x)))
  
  ;; ? postfix → Query flag
  (check-equal?
   (term (lower (op-post x ?)))
   (term (Query flag x)))
  
  ;; ^ infix → Hint with label
  (check-equal?
   (term (lower (op-in x ^ mytag)))
   (term (Hint x (label mytag))))
  
  ;; ─── REPL step tests ─────────────────────────────────────────────
  
  (define test-state
    (term (repl-state (context none none ()) none () ())))
  
  ;; Force produces forced
  (check-not-empty
   (filter
    (λ (r) (match r [`((forced x) ,_) #t] [_ #f]))
    (apply-reduction-relation repl-step (term ((Force x) ,test-state)))))
  
  ;; Flow threads context
  (check-not-empty
   (filter
    (λ (r) (match r 
             [`(y (repl-state (context y x (x)) ,_ ,_ ,_)) #t]
             [_ #f]))
    (apply-reduction-relation repl-step (term ((Flow x y) ,test-state)))))
  
  ;; Lower clears context
  (check-not-empty
   (filter
    (λ (r) (match r
             [`((lowered y) (repl-state (context none none ()) ,_ ,_ (y))) #t]
             [_ #f]))
    (apply-reduction-relation repl-step (term ((Lower x y) ,test-state))))))


;; ═══════════════════════════════════════════════════════════════════
;; § 8. VISUALIZATION & EXPLORATION
;; ═══════════════════════════════════════════════════════════════════

;; Trace a reduction
;; (traces repl-step (term ((Flow (Force x) (Query probe y)) ,init-state)))

;; Run to completion
(define (run-spw ast)
  (apply-reduction-relation* repl-step (term (,ast ,init-state))))

;; Lower surface and run
(define (eval-surface surf)
  (run-spw (term (lower ,surf))))

;; Example: ?{ x } ~ ?y ~ !z
;; (eval-surface (term (op-in (op-in (op-pre ? x) ~ (op-pre ? y)) ~ (op-pre ! z))))


;; ═══════════════════════════════════════════════════════════════════
;; § SUMMARY: Operator Classification
;; ═══════════════════════════════════════════════════════════════════
;;
;; ┌─────────┬──────────────────┬──────────────────┬──────────────────┐
;; │ Op      │ Prefix           │ Postfix          │ Infix            │
;; ├─────────┼──────────────────┼──────────────────┼──────────────────┤
;; │ ~       │ SEMANTIC(soft)   │ HINT(relax)      │ SEMANTIC(Flow)   │
;; │ ->      │ ERROR            │ ERROR            │ SEMANTIC(Lower)  │
;; │ ?       │ SEMANTIC(probe)  │ SEMANTIC(flag)*  │ SEMANTIC(guard)  │
;; │ !       │ SEMANTIC(force)  │ HINT(pin)        │ SEMANTIC(assert) │
;; │ ^       │ HINT(label)      │ HINT(pin)        │ HINT(label x)    │
;; └─────────┴──────────────────┴──────────────────┴──────────────────┘
;;
;; * flag is semantic but non-mutating (doesn't change ctx.result)
;; ═══════════════════════════════════════════════════════════════════