#lang racket

(require redex/reduction-semantics) ;; to avoid needing to load the GUI stuff, for headless use
(require (only-in "redex-iswim.rkt" ISWIM))

(define-extended-language ISWIM+Actors ISWIM
  (expr ....
        (send expr expr)   ;; sends the second arg to the first arg, a PID
        (receive)          ;; blocks, waiting for the next message
        (self)             ;; evaluates to the PID of the calling actor
        (spawn expr ...))  ;; spawns a new actor which performs the exprs.

  (value ....
         pid)

  (pid variable-not-otherwise-mentioned)

  (context ....
           (send context expr)
           (send pid context))

  (configuration (actor ...))
  (actor (pid : mailbox expr))
  (mailbox (value ...)))

(define ISWIM+Actors-inner-red
  (reduction-relation ISWIM+Actors
    (==> ((lambda (x ...) expr ...) value ...)
         (begin (subst-all expr (x ...) (value ...)) ...)
         beta)

    (==> (prim value ...)
         (delta prim (value ...))
         delta)

    (==> (begin expr)
         expr
         begin-one)

    (==> (begin value expr_0 expr ...)
         (begin expr_0 expr ...)
         begin-many)

    (==> (if #t expr_0 expr_1)
         expr_0
         if-true)

    (==> (if #f expr_0 expr_1)
         expr_1
         if-false)

    (==> (rec x expr)
         (substitute expr x (rec x expr))
         unfold)

    with
    [(--> (in-hole context A) (in-hole context B))
     (==> A B)]))

(define-metafunction ISWIM+Actors
  reduce-inner : expr -> expr
  [(reduce-inner expr) ,(first (apply-reduction-relation* ISWIM+Actors-inner-red (term expr)
                                                          #:error-on-multiple? #t))])

(define ISWIM+Actors-red
 (reduction-relation ISWIM+Actors

  (--> (actor_0 ...
        (pid_1 : mailbox (in-hole context (send pid value_0)))
        actor_1 ...)

       ((deliver pid value_0 actor_0) ...
        (deliver pid value_0 (pid_1 : mailbox (reduce-inner (in-hole context #t))))
        (deliver pid value_0 actor_1) ...)

       send)

  (--> (actor_0 ... (pid :
                         (value_0 value_1 ...)
                         (in-hole context (receive)))
        actor_1 ...)

       (actor_0 ... (pid :
                         (        value_1 ...)
                         (reduce-inner (in-hole context value_0  )))
        actor_1 ...)

       receive)

  (--> (actor_0 ... (pid : mailbox (in-hole context (self))) actor_1 ...)
       (actor_0 ... (pid : mailbox (reduce-inner (in-hole context pid))) actor_1 ...)
       self)

  (--> (actor_0 ... (pid_1 : mailbox (in-hole context (spawn expr ...)))
        actor_1 ...)

       (actor_0 ... (pid_1 : mailbox (reduce-inner (in-hole context pid_new)))
        actor_1 ... (pid_new : () (reduce-inner (begin expr ...))))

       (fresh pid_new)
       spawn)

  ))

(define-metafunction ISWIM+Actors
  delta : prim (value ...) -> value
  [(delta + (number_0 number_1)) ,(+ (term number_0) (term number_1))]
  [(delta - (number_0 number_1)) ,(- (term number_0) (term number_1))]
  [(delta = (value_0 value_1)) ,(equal? (term value_0) (term value_1))]
  [(delta car ((cons value_0 value_1))) value_0]
  [(delta cdr ((cons value_0 value_1))) value_1]
  [(delta pair? ((cons value_0 value_1))) #t]
  [(delta pair? (value)) #f (side-condition (or (not (pair? (term value)))
                                                (not (eq? (car (term value)) 'cons))))]
  [(delta null? (nil)) #t]
  [(delta null? (value)) #f (side-condition (not (eq? (term value) 'nil)))])

(define-metafunction ISWIM+Actors
  subst-all : expr (x ...) (value ...) -> expr
  [(subst-all expr () ()) expr]
  [(subst-all expr (x x_0 ...) (value value_0 ...))
   (subst-all (substitute expr x value) (x_0 ...) (value_0 ...))])

(define-metafunction ISWIM+Actors
  let : ((x expr) ...) expr ... -> expr
  [(let ((x_0 expr_0) ...) expr_1 ...)
   ((lambda (x_0 ...) expr_1 ...) expr_0 ...)])

(define-metafunction ISWIM+Actors
  boot-actor : expr ... -> configuration
  [(boot-actor expr ...) ((boot : () (reduce-inner (begin expr ...))))])

(define-metafunction ISWIM+Actors
  deliver : pid value actor -> actor
  [(deliver pid value (pid : (value_0 ...) expr)) (pid : (value_0 ... value) expr)]
  [(deliver pid value actor) actor])

(module+ test

  (test-->> ISWIM+Actors-red
            (term (boot-actor ((lambda (x) (+ x 1)) 123)))
            (term ((boot : () 124))))

  (test-->> ISWIM+Actors-red
            (term (boot-actor (send (self) 123) (+ (receive) 1)))
            (term ((boot : () 124))))

  (test-->> ISWIM+Actors-red
            (term (boot-actor (let ((w (self))) w)))
            (term ((boot : () boot))))

  (test-->> ISWIM+Actors-red
            (term (boot-actor (spawn 1) (spawn 2)))
            (term ((boot : () pid_new1) (pid_new : () 1) (pid_new1 : () 2))))

  (test-->> ISWIM+Actors-red
            (term (boot-actor (let ((w (self))) (spawn (send w 123)) (receive))))
            (term ((boot : () 123) (pid_new : () #t))))

  (test-->> ISWIM+Actors-red
            (term (boot-actor (let ((w (self))) (spawn (send w (self))) (receive))))
            (term ((boot : () pid_new) (pid_new : () #t))))

  (test-->> ISWIM+Actors-red
            (term (boot-actor
                   ((rec loop (lambda (count) (if (= count 0)
                                                  0
                                                  (begin (send (self) count)
                                                         (loop (- count 1)))))) 3)))
            (term ((boot : (3 2 1) 0))))

  (test-->> ISWIM+Actors-red

            (term (boot-actor
                   (spawn (send (self) 0))
                   (spawn (send (self) 0))))

            (term ((boot : () pid_new1)
                   (pid_new : (0) #t)
                   (pid_new1 : (0) #t))))

  (void
   (time
    (apply-reduction-relation* ISWIM+Actors-red
                               (term (boot-actor
                                      (let ((w (self)))
                                        (spawn (send w 1))
                                        (spawn (send w 2))
                                        (receive)))))))

  )