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

;; Plan:
;;
;; This is a limited protocol that probably only works for cycle-free
;; routing trees. It could well fail horribly when cycles in the
;; routing graph exist.
;;
;; A sender waits for the receiver to become visible, and then sends a
;; message. A receiver simply advertises its presence and collects
;; messages.
;;
;; A relay is bidirectional (but doesn't have to be). A relay is
;; composed of two peers communicating. Each peer mirrors routes on
;; its side at the side of its peer, and delivers messages it receives
;; via its peer. It is careful to subtract its peer's routes from
;; advertisements it receives from its environment to help avoid
;; routing loops.

;; Notes.
;;
;; The sender and receiver can now interoperate without knowing that
;; there's a bridge connecting them. They feel that they are part of
;; the same network.
;;
;; We have the machinery necessary to explore the consequences of
;; various routing protocols in a formal setting.
;;
;; As expected, routing loops are extremely easy to set up. For
;; example, try uncommenting the "loop" example below. For a start,
;; there are duplicate packets because more than one route from a
;; sender to a receiver exists. Furthermore, the relays don't have
;; deduplication machinery built-in, so B and C exchange 'hello and
;; 'world packets for ever.
;;
;; However, multi-hop (loop-free) routing works fine! See the
;; "multi-hop" example below.

;;---------------------------------------------------------------------------
;; Sender

(define (sender-beh e s)
  (match e
    [`(newtable ,subscriptions)
     (if (ormap (match-lambda [`(sub (receiver *) 0) #t] [_ #f]) subscriptions)
	 (values (list (term (send (receiver hello)))
		       (term (send (receiver world)))
		       (term (newtable ())))
		 s)
	 (values (list)
		 s))]
    [_ (values (list) s)]))

(define (boot-sender)
  (term (spawnA sender ()
		(newtable ( (pub (receiver *) 1) )))))

;;---------------------------------------------------------------------------
;; Receiver

(define (receiver-beh e s)
  (match e
    [`(send (receiver ,m)) (values (list) (append s (list m)))]
    [_ (values (list) s)]))

(define (boot-receiver)
  (term (spawnA receiver ()
		(newtable ( (sub (receiver *) 0) )))))

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

(struct relay-state (my-subnet my-subs peer-subnet peer-subs) #:transparent)

(define (nonmeta-participant-route? r)
  (match r
    [`(meta ,_) #f]
    [`(,_ ,_ 0) #t]
    [_ #f]))

(define (subs-diff a b)
  (set->list (set-subtract (list->set (filter nonmeta-participant-route? a))
			   (list->set (filter nonmeta-participant-route? b)))))

(define (core-relay-subscriptions my-subnet peer-subnet)
  (term ( (sub * 1)
	  (pub * 1)
	  (meta (sub (,peer-subnet ,my-subnet *) 0))
	  (meta (pub (,my-subnet ,peer-subnet *) 0)) )))

(define (relay-beh e s)
  (match-define (relay-state my-subnet my-subs peer-subnet peer-subs) s)
  (match e
    [`(newtable ,new-my-subs)
     (if (equal? new-my-subs my-subs)
	 (values (list) s)
	 (let ((new-out (subs-diff new-my-subs peer-subs)))
	   (values (list (term (meta (send (,my-subnet ,peer-subnet (newtable ,new-out))))))
		   (relay-state my-subnet new-my-subs peer-subnet peer-subs))))]
    [(or `(send ,_) `(feedback ,_))
     (if (term (filter-event ,e ,(filter nonmeta-participant-route? peer-subs)))
	 (values (list (term (meta (send (,my-subnet ,peer-subnet ,e))))) s)
	 (values (list) s))]
    [`(meta (send (,(== peer-subnet) ,(== my-subnet) ,quoted-event)))
     (match quoted-event
       [`(newtable ,new-peer-subs)
	(if (equal? new-peer-subs peer-subs)
	    (values (list) s)
	    (let ((new-in (subs-diff new-peer-subs my-subs)))
	      (values (list (term (newtable
				   ,(append (core-relay-subscriptions my-subnet peer-subnet)
					    new-in))))
		      (relay-state my-subnet my-subs peer-subnet new-peer-subs))))]
       [(or `(send ,_) `(feedback ,_)) (values (list (term ,quoted-event)) s)]
       [_ (values (list) s)])]
    [_ (values (list) s)]))

(define (boot-relay my-subnet peer-subnet)
  (term (spawnA relay ,(relay-state my-subnet '() peer-subnet '())
		(newtable ,(core-relay-subscriptions my-subnet peer-subnet)))))

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

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

;; "Single-hop" example
(quasi-trace ==>
	     (term (bootSigma (spawnVM ,(boot-sender)
				       ,(boot-relay 'A 'B))
			      (spawnVM ,(boot-receiver)
				       ,(boot-relay 'B 'A))
			      )))

;; ;; "Multi-hop" example
;; (quasi-trace ==>
;; 	     (term (bootSigma (spawnVM ,(boot-sender)
;; 				       ,(boot-relay 'A 'B))
;; 			      (spawnVM ,(boot-relay 'B 'A)
;; 				       ,(boot-relay 'B 'C))
;; 			      (spawnVM ,(boot-receiver)
;; 				       ,(boot-relay 'C 'B))
;; 			      )))

;; ;; "Loop" example
;; (quasi-trace ==>
;; 	     (term (bootSigma (spawnVM ,(boot-sender)
;; 				       ,(boot-relay 'A 'B)
;; 				       ,(boot-relay 'A 'C))
;; 			      (spawnVM ,(boot-receiver)
;; 				       ,(boot-relay 'B 'A)
;; 				       ,(boot-relay 'B 'C))
;; 			      (spawnVM ,(boot-receiver)
;; 			      	       ,(boot-relay 'C 'A)
;; 			      	       ,(boot-relay 'C 'B))
;; 			      )))