#lang racket

(require redex/reduction-semantics
         redex/gui
         racket/syntax)

(define-language CCS
  ;; channels
  [a b c d e ::=
     (variable-prefix a) (variable-prefix b) (variable-prefix c) (variable-prefix d)
     (variable-prefix e) (variable-prefix f) (variable-prefix g) (variable-prefix s)
     (variable-prefix t) (variable-prefix q) (variable-prefix r)]
  ;; variables
  [x y z w ::=
     (variable-prefix x) (variable-prefix y) (variable-prefix z) (variable-prefix w)]
  [u v ::= a x]
  ;; processes
  [P Q ::=
     nil
     (‖ P ...)
     ((ν a) P)
     (! P)
     (u ⇐ v) ;; maybe use (▔ u ⟨ v ⟩) instead?
     (u (x) · P)]
  #:binding-forms
  ((ν a) P #:refers-to a)
  (u (x) · P #:refers-to x)
  )

(define-extended-language CCS+eval CCS
  [abstract-function
   (variable-prefix A) (variable-prefix B) (variable-prefix C) (variable-prefix D)
   (variable-prefix E) (variable-prefix F) (variable-prefix G) (variable-prefix H)
   (variable-prefix I) (variable-prefix J) (variable-prefix K) (variable-prefix L)
   (variable-prefix M) (variable-prefix N) (variable-prefix O) (variable-prefix P)
   (variable-prefix Q) (variable-prefix R) (variable-prefix S) (variable-prefix T)
   (variable-prefix U) (variable-prefix V) (variable-prefix W) (variable-prefix X)
   (variable-prefix Y) (variable-prefix Z)]
  [P ::= .... (abstract-function u v ...)]
  [E ::=
     hole
     (‖ P ... E Q ...)
     ((ν a) E)])

(define R
  (reduction-relation
   CCS+eval
   #:domain P

   ;; unfolding
   (--> (in-hole E (! P))
        (in-hole E (‖ P (! P)))
        "Rep")

   ;; congruence (2)
   (--> (in-hole E (par))
        (in-hole E nil)
        "Par Nil")
   (--> (in-hole E (‖ P ... 0 Q ...))
        (in-hole E (‖ P ... Q ...))
        "Zero")
   (--> (in-hole E (‖ P_1 ... (‖ Q ...) P_2 ...))
        (in-hole E (‖ P_1 ... Q ... P_2 ...))
        "Assoc")

   ;; congruence (3)
   (--> (in-hole E ((ν a) nil))
        (in-hole E nil)
        "Res Nil")
   #;
   (--> (in-hole E ((ν a) ((ν b) P)))
        (in-hole E ((ν b) ((ν a) P)))
        "Res Res")
   (--> (in-hole E (‖ P_1 ... ((ν a) Q) P_2 ...))
        (in-hole E ((ν a) (‖ P_1 ... Q P_2 ...)))
        "Res Par")

   ;; communication!
   (--> (in-hole E (‖ P_1 ... (a ⇐ v) P_2 ... (a (x) · P) P_3 ...))
        (in-hole E (‖ P_1 ... P_2 ... (substitute P x v) P_3 ...))
        "Comm1")
   (--> (in-hole E (‖ P_1 ... (a (x) · P) P_2 ... (a ⇐ v) P_3 ...))
        (in-hole E (‖ P_1 ... P_2 ... (substitute P x v) P_3 ...))
        "Comm2")
   ))

;; Some examples
(define communication-example
  (term (‖ (a (x) · (x ⇐ c))
           (a ⇐ b))))

(define scope-extrusion-example
  (term (‖ ((ν b) (a ⇐ b))
           (a (x) ·
              (c ⇐ x)))))

;; Small agents
(define-metafunction CCS
  FW : a b -> P
  [(FW a b) (a (z) · (b ⇐ z))])

(define-metafunction CCS
  D : a b c -> P
  [(D a b c) (a (z) ·
                (‖ (b ⇐ z)
                   (c ⇐ z)))])

(define-metafunction CCS
  K : a -> P
  [(K a) (a (z) · nil)])

(define-metafunction CCS
  NN : a -> P
  [(NN a) (! (a (x) ·
                ((ν b) (x ⇐ b))))])

;; Hacking!
(define-metafunction CCS
  [(SClient- integer)
   ((ν c) (‖ (a ⇐ c)
             (c (x) · (PClient c x))))
   (where abstract-function ,(format-symbol "PClient~a" (term integer)))])

(define-term SServer-a
  (! (a (y) ·
        ((ν s)
         (‖ (y ⇐ s)
            (PServer y s))))))

(define secure-client-server-example
  (term (‖ (SClient- 1) (SClient- 2) SServer-a)))

(define (lex-order rule-name)
  (cond [(equal? rule-name "Rep") 0]
        [(equal? rule-name "Res Par") -1]
        [else -2]))

(define (run-many! unfold-fuel t)
  (parameterize ([pretty-print-columns 50])
    (pretty-write t))
  (define next-steps
    (sort (apply-reduction-relation/tag-with-names R t)
          (λ (name1 name2)
            (define l1 (lex-order name1))
            (define l2 (lex-order name2))
            (or (< l1 l2)
                (and (= l1 l2) (string<? name1 name2))))
          #:key car))
  (cond
    [(< unfold-fuel 0)
     (printf "\nRun out of fuel.\n")
     t]
    [(null? next-steps) t]
    [else
     (match-define (cons (list rule-name t-next) _) next-steps)
     (printf "\n============ ~s ============\n" rule-name)
     (run-many! (cond [(member rule-name '("Rep" "Res Res")) (- unfold-fuel 1)]
                      [else unfold-fuel])
                t-next)]))