#lang scheme

(require redex/reduction-semantics 
         (planet schematics/schemeunit))

(define-language pi-calculus
  (pi (pi pi)
      zero
      (nu a pi)
      (out a a pi)
      (in a a pi)
      (bang pi))
  (a variable)
  ;; evaluation contexts:
  (E hole
     (E pi)
     (pi E)
     (nu a E)
     (bang E)))


(define red
  (reduction-relation 
   pi-calculus

   (--> (in-hole E_1 ((in-hole E_in (in a_chan a_var pi_inner-in)) (in-hole E_out (out a_chan a_sent pi_inner-out))))
        (in-hole E_1 (maybe-lift sent E_in (in a_chan a_var pi_inner-in) E_out (out a_chan a_sent pi_inner-out)))
                
        (fresh sent)
        ;; the name of the channel must be free on both sides:
        (side-condition (and (not (member (term a_chan) (term (bound-by E_in))))
                             (not (member (term a_chan) (term (bound-by E_out)))))))
   
   
   ;; EXACTLY THE SAME except in & out are reversed in the input:
   (--> (in-hole E_1 ((in-hole E_out (out a_chan a_sent pi_inner-out)) (in-hole E_in (in a_chan a_var pi_inner-in))))
        (in-hole E_1 (maybe-lift sent E_in (in a_chan a_var pi_inner-in) E_out (out a_chan a_sent pi_inner-out)))
        
        (fresh sent)
        ;; the name of the channel must be free on both sides:
        (side-condition (and (not (member (term a_chan) (term (bound-by E_in))))
                             (not (member (term a_chan) (term (bound-by E_out)))))))))


;; maybe-lift : given a fresh identifier and two context/pi pairs, perform replication
;; on each pair if necessary and then lift the nu-binding of the a_sent name if necessary
;; (renaming it a_lifted)
(define-metafunction pi-calculus
  maybe-lift : a E pi E pi -> pi
  
  ;; the name being sent needs lifting, so that it includes the recipient:
  [(maybe-lift a_lifted E_in (in a_chan a_var pi_inner-in) E_out (out a_chan a_sent pi_inner-out))
   (nu a_lifted ((in-hole E_unbanged-in (subst a_var a_lifted pi_inner-in))
                 (in-hole (rename-innermost a_sent a_lifted E_unbanged-out)
                          (subst a_sent a_lifted pi_inner-out))))
   
   (where E_unbanged-in  (replicate-as-needed E_in  (in a_chan a_var pi_inner-in)))
   (where E_unbanged-out (replicate-as-needed E_out (out a_chan a_sent pi_inner-out)))
   
   (side-condition (member (term a_sent) (term (bound-by E_out))))]

  ;; otherwise, no need to lift nu:
  [(maybe-lift a_lifted E_in (in a_chan a_var pi_inner-in) E_out (out a_chan a_sent pi_inner-out))
   ((in-hole E_unbanged-in (subst a_var a_sent pi_inner-in))
    (in-hole E_unbanged-out pi_inner-out))
   
   (where E_unbanged-in  (replicate-as-needed E_in  (in a_chan a_var pi_inner-in)))
   (where E_unbanged-out (replicate-as-needed E_out (out a_chan a_sent pi_inner-out)))])



;; replicate-as-needed : performs replication to uncover the desired
;; expression
(define-metafunction pi-calculus
  replicate-as-needed : E pi -> E
  [(replicate-as-needed hole pi_orig)     hole]  
  [(replicate-as-needed (E pi) pi_orig)   ((replicate-as-needed E pi_orig) pi)]
  [(replicate-as-needed (pi E) pi_orig)   (pi (replicate-as-needed E pi_orig))]
  [(replicate-as-needed (nu a E) pi_orig) (nu a (replicate-as-needed E pi_orig))]
  [(replicate-as-needed (bang E) pi_orig) ((replicate-as-needed E pi_orig)
                                           (in-hole (bang E) pi_orig))])

;; rename-innermost : rename the *innermost* binding of a given name along
;; an evaluation context, using another given name. At this point,
;; there should be no bangs along the context. Also, a_from should 
;; be fresh, so there's no need to worry about those collisions.
(define-metafunction pi-calculus
  rename-innermost : a_from a_to E -> E
  ;; no hole case; the base case is no more bindings of a_from
  [(rename-innermost a_from a_to (E pi))         ((rename-innermost a_from a_to E) pi)]
  [(rename-innermost a_from a_to (pi E))         (pi (rename-innermost a_from a_to E))]
  
  ;; this is the last! substitute from here on out:
  [(rename-innermost a_from a_to (nu a_from E))  (subst/E a_from a_to E)
   (side-condition (not (member (term a_from) (term (bound-by E)))))]
  
  [(rename-innermost a_from a_to (nu a_other E)) (nu a_other (rename-innermost a_from a_to E))]
  ;; no case for bang.  
  )

;; THE REST OF THIS IS BOILERPLATE... (subst, free-vars, etc.)


;; BOUND-BY : compute the variables bound along the spine of a context
(define-metafunction pi-calculus
  bound-by : E -> (a ...)
  [(bound-by hole)     ()]
  [(bound-by (E pi))   (bound-by E)]
  [(bound-by (pi E))   (bound-by E)]
  [(bound-by (nu a E)) (a a_rest ...)
                       (where (a_rest ...) (bound-by E))]
  [(bound-by (bang E)) (bound-by E)])




;; SUBST

;; substitute a_to for a_from in pi.  Note that renaming may be necessary, 
;; when looking inside a binder for a_to.
(define-metafunction pi-calculus
  subst : a a pi -> pi
  [(subst a_from a_to zero) zero]
  [(subst a_from a_to (pi_1 pi_2)) ((subst a_from a_to pi_1)
                                    (subst a_from a_to pi_2))]
  ;; shadowing of a_from: stop substitution
  [(subst a_from a_to (nu a_from pi)) (nu a_from pi)]
  ;; shadowing of a_to: rename if a_from occurs free.
  [(subst a_from a_to (nu a_to pi))
   (nu a_new (subst a_from a_to (subst a_to a_new pi)))
   (where a_new (fresh-in (nu a_to pi) a_to))
   (side-condition (member (term a_from) (term (free-vars pi))))]
  ;; otherwise, proceed:
  [(subst a_from a_to (nu a pi))
   (nu a (subst a_from a_to pi))]
  
  [(subst a_from a_to (out a_1 a_2 pi))
   (out (subst-name a_from a_to a_1)
        (subst-name a_from a_to a_2) 
        (subst a_from a_to pi))]
   ;; shadowing of a_from: stop substitution
  [(subst a_from a_to (in a_chan a_from pi))
   (in (subst-name a_from a_to a_chan) a_from pi)]
  ;; shadowing of a_to: rename if a_from occurs free
  [(subst a_from a_to (in a_chan a_to pi))
   (in (subst-name a_from a_to a_chan) 
       a_new
       (subst a_from a_to (subst a_to a_new pi)))
   (where a_new (fresh-in (in a_chan a_to pi) a_to))
   (side-condition (member (term a_from) (term (free-vars pi))))]
  ;; otherwise, proceed:
  [(subst a_from a_to (in a_chan a_var pi))
   (in (subst-name a_from a_to a_chan) a_var (subst a_from a_to pi))]
  
  [(subst a_from a_to (bang pi))
   (bang (subst a_from a_to pi))])

;; SUBST/E : substitute a_to for a_from in pi; assumes 
;; there are no more bindings for a_from along the context spine,
;; and that a_to is fresh (enough).
(define-metafunction pi-calculus
  subst/E : a_from a_to E -> E

  [(subst/E a_from a_to hole)      hole]
  [(subst/E a_from a_to (pi E))    ((subst a_from a_to pi) (subst/E a_from a_to E))]
  [(subst/E a_from a_to (E pi))    ((subst/E a_from a_to E) (subst a_from a_to pi))]
  [(subst/E a_from a_to (nu a E))  (nu a (subst/E a_from a_to E))]
  [(subst/E a_from a_to (bang E))  (bang (subst/E a_from a_to))])


;; SUBST-NAME: replace a_from with a_to, leave other names alone.
(define-metafunction pi-calculus
  subst-name : a a a -> a
  [(subst-name a_src a_tgt a_src)   a_tgt]
  [(subst-name a_src a_tgt a)       a])

;; FREE-VARS : return a list of the variables that occur free in the term
;; WARNING: MAY INCLUDE DUPLICATES...
(define-metafunction pi-calculus
  free-vars : pi -> (a ...)
  [(free-vars zero) ()]
  [(free-vars (pi_1 pi_2)) (a_1 ... a_2 ...)
                           (where (a_1 ...) (free-vars pi_1))
                           (where (a_2 ...) (free-vars pi_2))]
  [(free-vars (nu a pi)) (set-minus (free-vars pi) a)]
  [(free-vars (out a_chan a_sent pi)) (a_chan a_sent a ...)
                                      (where (a ...) (free-vars pi))]
  [(free-vars (in a_chan a_var pi)) (a_chan a ...)
                                    (where (a ...) (set-minus (free-vars pi) a_var))])

;; remove *all* instances of a_kilt from (a ...)
(define-metafunction pi-calculus
  set-minus : (a ...) a -> (a ...)
  [(set-minus (a_1 ... a_kilt a_2 ...) a_kilt) (set-minus (a_1 ... a_2 ...) a_kilt)]
  [(set-minus (a ...) a_kilt) (a ...)])


;; provide variable-not-in as a metafunction:
(define-metafunction pi-calculus
  fresh-in : pi a -> a
  [(fresh-in pi a) ,(variable-not-in (term pi) (term a))])


;; TEST CASES

(check-equal? (apply-reduction-relation red (term zero))
              '())
;; simplest communication:
(check-equal? (apply-reduction-relation 
               red
               (term ((in a b zero) (out a c zero))))
              `((zero zero)))
;; check simplest substitution
(check-equal? (apply-reduction-relation 
               red
               (term ((out a c zero) (in a b (out b b zero)))))
              `(((out c c zero) zero)))
;; check simple nesting
(check-equal? (apply-reduction-relation 
               red
               (term (((out z y zero) (out a c zero)) ((in a b (out b b zero)) (out x w zero)))))
              `((((out c c zero) (out x w zero)) ((out z y zero) zero))))
;; outer context:
(check-equal? (apply-reduction-relation 
               red
               (term (zero (nu a (((out z y zero) (out a c zero)) ((in a b (out b b zero)) (out x w zero)))))))
              `((zero (nu a (((out c c zero) (out x w zero)) ((out z y zero) zero))))))
;; with bang replication:
(check-equal? (apply-reduction-relation 
               red
               (term (zero (nu a (((out z y zero) (out a c zero)) ((bang (in a b (out b b zero))) (out x w zero)))))))
              `((zero (nu a ((((out c c zero)
                               (bang (in a b (out b b zero))))
                              (out x w zero)) 
                             ((out z y zero) zero))))))
;; with lifting (depends on fresh name):
(check-equal? (apply-reduction-relation 
               red
               (term (zero (nu a (((out z y zero) (nu c (out a c (in c c zero)))) ((bang (in a b (out b b zero))) (out x w zero)))))))
              `((zero (nu a (nu sent
                                ((((out sent sent zero)
                                   (bang (in a b (out b b zero))))
                                  (out x w zero))
                                 ((out z y zero) (in sent c zero))))))))

;; need longer examples...

;; this on taken from wikipedia:
(check-equal? (apply-reduction-relation
               red
               (term ((nu x ((out x z zero)
                             (in x y (out y x (in x y zero)))))
                      (in z v (out v v zero)))))
              (list (term ((nu x ((out z x (in x y zero))
                                  zero))
                           (in z v (out v v zero))))))
(check-equal? (apply-reduction-relation
               red
               (term ((nu x ((out z x (in x y zero))
                             zero))
                      (in z v (out v v zero)))))
              (list (term (nu sent ((out sent sent zero)
                                    ((in sent y zero) zero))))))

(check-equal? (apply-reduction-relation
               red
               (term (nu sent ((out sent sent zero)
                               ((in sent y zero) zero)))))
              (list (term (nu sent ((zero zero)
                                    zero)))))



(check-equal? (term (rename-innermost a1 a2 
                                      ((out a1 a1 zero)
                                       (nu a1 ((nu a1 (hole (out a1 a1 zero)))
                                               (out a1 a1 zero))))))
              (term ((out a1 a1 zero)
                     (nu a1 ((hole (out a2 a2 zero))
                             (out a1 a1 zero))))))

(check-equal? (term (replicate-as-needed ((out a b zero)
                                          (bang ((nu e (bang hole))
                                                 (out c d zero))))
                                         (out e f zero)))
              (term ((out a b zero)
                     (((nu e (hole
                              (bang (out e f zero))))
                             (out c d zero))
                      (bang ((nu e (bang (out e f zero)))
                             (out c d zero)))))))

(begin (check-equal? (term (bound-by hole))
                     '())
       (check-equal? (term (bound-by (nu x hole)))
                     '(x))
       (check-equal? (term (bound-by (nu x (nu y hole))))
                     '(x y))
       (check-equal? (term (bound-by (zero (nu x hole))))
                     '(x))
       (check-equal? (term (bound-by (bang (nu x hole))))
                     '(x)))


(check-equal? (term (set-minus (w x y x z) x))
              `(w y z))

(begin 
  (check-equal? (term (free-vars zero)) `())
  (check-equal? (term (free-vars (out a b zero))) `(a b))
  (check-equal? (term (free-vars (out a b (out c d zero)))) `(a b c d))
  (check-equal? (term (free-vars ((out a b zero) (out c d zero)))) `(a b c d))
  (check-equal? (term (free-vars (nu a (out a a (out b a zero)))))  '(b))
  (check-equal? (term (free-vars (in a b (out b b zero)))) `(a)))


(begin 
  (check-equal? (term (subst a1 a2 zero)) 'zero)
  (check-equal? (term (subst a1 a2 (out a b zero))) `(out a b zero))
  (check-equal? (term (subst a1 a2 (out a b (out a1 c (out d a1 zero))))) `(out a b (out a2 c (out d a2 zero))))
  (check-equal? (term (subst a1 a2 ((out a1 a zero)
                                    (out b a1 zero))))
                `((out a2 a zero) (out b a2 zero)))
  (check-equal? (term (subst a1 a2 (nu a1 (out a1 a1 zero))))
                (term (nu a1 (out a1 a1 zero))))
  
  ;; note : this test case depends on redex's choice of a fresh name for a2:
  (check-equal? (term (subst a1 a2 (nu a2 (out a1 a1 (out a2 a2 zero)))))
                (term (nu a3 (out a2 a2 (out a3 a3 zero)))))
  ;; no name change should happen, because a_from doesn't occur free under the binder:
  (check-equal? (term (subst a1 a2 (nu a2 (out a2 a2 zero))))
                (term (nu a2 (out a2 a2 zero))))
  
  (check-equal? (term (subst a1 a2 (nu a3 (out a1 a1 zero))))
                (term (nu a3 (out a2 a2 zero))))
  
  (check-equal? (term (subst a1 a2 (in a1 a1 (out a1 a1 zero))))
                (term (in a2 a1 (out a1 a1 zero))))
  (check-equal? (term (subst a1 a2 (in a1 a2 (out a1 a1 (out a2 a2 zero)))))
                (term (in a2 a3 (out a2 a2 (out a3 a3 zero)))))
  (check-equal? (term (subst a1 a2 (in a1 a3 (out a3 a1 zero))))
                (term (in a2 a3 (out a3 a2 zero))))
  
  (check-equal? (term (subst a1 a2 (bang (out a1 a1 zero))))
                (term (bang (out a2 a2 zero))))
  
  
  )

;; milner's encoding of the cbn lambda-calculus
;; (in progress)
(define (encode M u)
  (match M
    [`(lam ,(? symbol? x) ,M)
     (term (in ,u ,x (in ,u v ,(encode M u))))]
    [(? symbol x)
     (out ,x ,u)]
    [`(,M ,N)
     (nu v (,(encode M v)
            ;; where x is fresh.  Yes, I should do this in redex.
            (nu x (out v x (out v u ,(encode-binding x N))))))]))