#lang racket/base
(require redex)
(require "network-calculus.rkt")
(require racket/list)
(require racket/set)
(require racket/match)
(require "redex-utils.rkt")

;; Plan:
;;
;; A chat user actor goes through several states.
;;  - waiting for the room to arrive
;;  - joining the room and waiting for the join to complete
;;  - greeting other actors as they arrive
;; The last two states can be collapsed into just one state; so there
;; are two states in total.
;;
;; The chat room itself is inert.
;;
;; The chat room has a boot process that accepts enrollees.
;;
;; The user-representing process simply relays quoted events/actions
;; to its counterparty.

;;---------------------------------------------------------------------------
;; User

(struct user-waiting-for-room (username) #:transparent)
(struct user-connected (username previous-peers event-log) #:transparent)

(define (subscriptions->peer-set peers)
  (list->set (filter-map (match-lambda
			  [`(pub (chat ,u *) ,*) u]
			  [_ #f]) peers)))

(define (user-beh e s)
  (match* (s e)
    [((user-waiting-for-room username) `(newtable ((sub (chatroom room1 *) 0))))
     (values (list (term (send (chatroom room1 ,(boot-relay username)))))
	     (user-connected username (set username) '()))]
    [((user-connected username previous-peers event-log) _)
     (define s1 (user-connected username previous-peers (append event-log (list e))))
     (match e
       [`(send (user ,_ (newtable ,subscriptions)))
	(define new-peers (subscriptions->peer-set subscriptions))
	(define arrived (set-subtract new-peers previous-peers))
	(values (map (lambda (u) (term (feedback
					(user ,username
					      (send (chat ,username ,(format "Hello, ~a" u)))))))
		     (set->list arrived))
		(struct-copy user-connected s1
		  [previous-peers (set-union arrived previous-peers)]))]
       [_
	(values (list) s1)])]
    ))

(define (boot-user username)
  (term (spawnA user ,(user-waiting-for-room username)
		(newtable ( (pub (chatroom room1 *) 1)
			    (sub (user ,username *) 0) )))))

;;---------------------------------------------------------------------------
;; Acceptor

(struct acceptor-state () #:transparent)

(define (acceptor-beh e s)
  (match* (s e)
    [((acceptor-state) `(meta (send (chatroom room1 ,action))))
     (values (list action)
	     s)]))

(define (boot-acceptor)
  (term (spawnA acceptor ,(acceptor-state)
		(newtable ( (meta (sub (chatroom room1 *) 0)) )))))

;;---------------------------------------------------------------------------
;; Relay

(struct relay-state (target-user) #:transparent)

(define (relay-beh e s)
  (match* (s e)
    [((relay-state target-user) `(meta (feedback (user ,_ ,action))))
     (values (list action)
	     s)]
    [((relay-state target-user) e)
     (values (list (term (meta (send (user ,target-user ,e)))))
	     s)]))

(define (boot-relay username)
  (term (spawnA relay ,(relay-state username)
		(newtable ( (meta (pub (user ,username *) 0))
			    (pub (chat ,username *) 0)
			    (sub (chat * *) 1) )))))

;;---------------------------------------------------------------------------
;; Main

(current-eval0 (lambda (f e u)
		 (write (list 'LEAFSTEP-I f u e))
		 (newline)
		 (define-values (actions u1)
		   (match* (f e u)
		     [('user e s) (user-beh e s)]
		     [('acceptor e s) (acceptor-beh e s)]
		     [('relay e s) (relay-beh e s)]
		     ))
		 (write (list 'LEAFSTEP-O f u1 actions))
		 (newline)
		 (values actions u1)))

(quasi-trace ==>
	     (term (bootSigma ,(boot-user 'A)
			      ,(boot-user 'B)
			      ,(boot-user 'C)
			      (spawnVM ,(boot-acceptor))
			      )))