main.ss
#|               _                           _                        
     () |       | |  o              ()      | |                       
     /\/| __    | |      _  _       /\  __  | |     _   _  _  _    _  
    /   |/  \__ |/   |  / |/ |     /  \/    |/ \   |/  / |/ |/ |  |/  
   /(__/ \__/ \_/\/  |_/  |  |_/  /(__/\___/|   |_/|__/  |  |  |_/|__/

   Geometry of Interaction in Scheme.

   Copyright (c) 2009 David Van Horn
   Licensed under the Academic Free License version 3.0

   (at dvanhorn (dot ccs neu edu))

      That red horned, lousy, low life, underneath our boots...
      Praise the Lord.
      I don't know what it is.
      Two dollar - that demonmiester
      Three dollar - that prince devil
      Just see if you can come up with a figure that matches your faith.
                --- Tom Waits
|#

#lang scheme
(provide graph)
(require test-engine/scheme-tests)

;; This program compiles sharing graphs into a computational
;; representation of their geometry of interaction semantics.
;; The resulting object has named ports which you can interact
;; with, asking questions using contexts.

;; See Mairson, From Hilbert Space to Dilbert Space: Context
;; Semantics Made Simple, for reference.

;; The paper:  http://www.cs.brandeis.edu/~mairson/Papers/fsttcs02.pdf
;; The slides: http://www.cs.brandeis.edu/~mairson/dilbertslides.pdf

;; A graph G has a named interface to its ports.  Applying G
;; to the name of one of its ports produces the port value.
;; To interact with a port, apply it to a context and get back
;; a pair: the port where the result arrives and the resulting
;; context. 

;; For example, (G 'πi) => πi  and (πi c) => (cons πj c*).
;; By the reversibility of GoI (πj c*) => (cons πi c).

;; A Graph   is a Symbol -> Port
;; A Port    is a Context -> (Pair Port Context)
;; A Context is a Nat -> WireVal
;; A WireVal is one of
;;   - empty                    Empty stack
;;   - (cons Token WireVal)     Non-empty stack
;;   - (cons WireVal WireVal)   Pairing (bracket)
;;   - '?, v
;;   - Symbol                   Variable name (croissant)
;; A Token is one of '● '○ 'L 'R

;; Contexts are infinitely wide buses, reprented as functions
;; Nat -> WireVal, such that <<χ0,χ1,...>> = (λ (n) χn).
(define mt (λ (n)  empty))                 ;; <<,...,>>
(define (○^i i) (λ (n) (make-list i ')))  ;; <<o^i,o^i,...>>

;; Project out the first n elements of the context
;; Context Nat -> [Listof WireVal]
(define (proj c n) 
  (for/list ((i (in-range n))) (c i)))

(check-expect (proj mt 5) (make-list 5 empty))

;; Inject a finite list of wire values into the space of contexts.
;; [Listof WireVal] -> Context
(define (inj χs)
  (λ (n) (list-ref χs n)))

(check-expect (proj (inj '((x) (y) (z))) 3)
              '((x) (y) (z)))

;; Syntax: (graph <interface> <node-spec> ...)

;; <interface> ::= [(x-in x-out) (y-in y-out) ...]

;; The *-out names given will be named ports (all other ports
;; are not visible outside a graph and can be obtained only
;; through interaction).  The first link is assumed to be the
;; root link, which every graph has.  The remaining links
;; represent remaining named, open ports.

;; <node-spec> ::= (λ  i (p1 p2) (w1 w2) (b1 b2))  Lambda
;;              |  (@  i (p1 p2) (w1 w2) (b1 b2))  Apply
;;              |  (▵ i (p1 p2) (w1 w2) (b1 b2))  Share
;;              |  (x  i (p1 p2) (a1 a2))          Croissant
;;              |  (~  i (p1 p2) (a1 a2))          Bracket
;;              |  ('v i (p1 p2))                  Constant
;;              |  (δ  i (p1 p2) (a1 a2))          Primitive
;;              |  (⨀ i (p1 p2))                  Plug
;;              |  (⧻ f g (p1 p2) (p3 p4))        Chink

;; A node spec gives the level (i) of the node, its kind, and
;; a set of links for the node.  The number of links corresponds
;; to the arity of the node.  The order is always principal;
;; principal, auxillary; or principal, white, black.  Links are
;; directed from the outside into the node.

;; The ⧻-node is a "chink" in the graph.  It acts as an identity
;; but calls f with the context going left to right, and g with the
;; context going right to left, only for effect.  You can use IO
;; to observe a sub-interaction in the graph, like λs.λz.s(sz) vs succ.

;; A graph must have a balanced set of port names.  Every name appears
;; exactly once on the left hand side and once on the right hand
;; side of a link.

;; A graph compiles into a system of mutually tail recursive
;; functions.  Travelling along a wire is implemented as a goto
;; (tail call).  So compilation produces a single letrec of the form:

;; (letrec ((p1 (λ (c) (p2 (λ (n) ... context transformation ...))))
;;         ...)
;;   (λ (p-name) ... port with name p-name ...))

;; This represents a link from p1 to p2 that performs the given
;; transformation on the context.

;; The result is a function that consumes the name of a port and
;; returns the value of the port with that name.              
(define-syntax (graph stx)
  (syntax-case stx ()
    [(graph ([lr r] [lx x] ...) N ...)
     (let loop ((ns (syntax->list #'(N ...))) (bs null))
       (cond [(null? ns) #`(letrec ((r (λ (c) (cons lr c)))
                                    (x (λ (c) (cons lx c)))
                                    ...
                                    #,@bs)
                             (λ (π)
                               (case π
                                 [(r) lr]
                                 [(x) lx]
                                 ...
                                 [else (error "unknown port" π)])))]
             [else
              (syntax-case (car ns) (~   δ quote)
                ;; Ternary node
                [(kind i (l1 l2) (l3 l4) (l5 l6))
                 (with-syntax (((w b) (syntax-case #'kind (λ @ )
                                        [λ #'( )]
                                        [@ #'( )]
                                        [ #'(L R)])))
                   (loop (cdr ns)
                         (list* 
                          #'(l2 (λ (c) 
                                  ((if (eq? 'w (car (c i))) l3 l5)
                                   (λ (n) 
                                     (if (= n i)
                                         (cdr (c n))
                                         (c n))))))
                          #'(l4 (λ (c)
                                  (l1 (λ (n)
                                        (if (= n i)
                                            (cons 'w (c i))
                                            (c n))))))
                          #'(l6 (λ (c)
                                  (l1 (λ (n)
                                        (if (= n i)
                                            (cons 'b (c i))
                                            (c n))))))
                          bs)))]
                
                ;; Constant
                [('v i (l1 l2)) 
                 (loop (cdr ns) 
                       (list* 
                        #'(l2 (λ (c) 
                                (l1 (λ (n) (if (= i n)
                                               (if (eq? (c i) '?) v '?)
                                               (c n))))))
                        bs))]
                
                ;; Primop
                [(δ i f (l1 l2) (l3 l4))
                 (loop (cdr ns)
                       (list*
                        #'(l2 (λ (c) (l3 (λ (n)
                                           (if (= i n)
                                               (f (c i))
                                               (c n))))))
                        #'(l4 (λ (c) (l1 (λ (n)
                                           (if (= i n)
                                               '?
                                               (c n))))))
                        bs))]

                ;; Chink
                ;; a narrow opening or crack, typically one that admits light
                [( f g (l1 l2) (l3 l4))
                 (loop (cdr ns)
                       (list*
                        #'(l2 (λ (c) (f c) (l3 (λ (n) (c n)))))
                        #'(l4 (λ (c) (g c) (l1 (λ (n) (c n)))))
                        bs))]
                 
                ;; Bracket
                [(~ i (l1 l2) (l3 l4))
                 (loop (cdr ns)
                       (list* 
                        #'(l2 (λ (c) 
                                (l3 (λ (n)
                                      (cond [(< n i) (c n)]
                                            [(= n i) (car (c i))]
                                            [(= n (add1 i)) (cdr (c i))]
                                            [else (c (sub1 n))])))))
                        #'(l4 (λ (c) 
                                (l1 (λ (n)
                                      (cond [(< n i) (c n)]
                                            [(= n i) (cons (c i) (c (add1 i)))]
                                            [else (c (add1 n))])))))
                        bs))]
                
                ;; Variable
                [(x i (l1 l2) (l3 l4))
                 (loop (cdr ns)
                       (list* 
                        #'(l2 (λ (c) 
                                (l3 (λ (n)
                                      (cond [(< n i) (c n)]
                                            [else (c (add1 n))])))))
                        #'(l4 (λ (c) 
                                (l1 (λ (n)
                                      (cond [(< n i) (c n)]
                                            [(= n i) 'x]
                                            [else (c (sub1 n))])))))
                        bs))])]))]))

;; Nat Graph Symbol [Listof WireVal] -> [Pair Port [Listof WireVal]]
;; (inter n g p χs) injects the finite list χs into contexts, interacts
;; with g at port named p, and returns a list of the resulting port and
;; a projection of n values from resulting context.
;; Useful for examples and testing.
(define (inter n g p χs)
  (let ((r ((g p) (inj χs))))
    (list (car r)
          (proj (cdr r) n))))

(define NUMFIVE
  (graph [(π1 in)]
         ('5 0 (in π1))))

(check-expect (inter 2 NUMFIVE 'in '(? ...))
              (list (NUMFIVE 'in)  '(5 ...)))

(check-expect (inter 2 NUMFIVE 'in '(5 ...))
              (list (NUMFIVE 'in)  '(? ...)))

(define PLUS1
  (graph [(π1 in) (π2 out)]
         (δ 0 add1 (in π1) (out π2))))

(check-expect (inter 2 PLUS1 'in  '(3 ...))
              (list (PLUS1 'out)  '(4 ...)))
(check-expect (inter 2 PLUS1 'out '(? ...))
              (list (PLUS1 'in)   '(? ...)))

(define BRAC
  (graph [(π1 in) (π2 out)]
         (~ 0 (in π1) (out π2))))  
         
(check-expect (inter 4 BRAC 'in '((a . b) c d)) 
              (list (BRAC 'out) '(a b c d)))
(check-expect (inter 3 BRAC 'out '(a b c d)) 
              (list (BRAC 'in) '((a . b) c d)))

;; G(x)
(define VAR
  (graph [(π1 ) (π2 x)]
         (x 0 ( π1) (x π2))))
                 
(check-expect (inter 3 VAR ' '(x a b c))
              (list (VAR 'x) '(a b c)))          
(check-expect (inter 4 VAR 'x '(a b c))
              (list (VAR ') '(x a b c)))

;; G(λ)
(define LAM
  (graph [(π1 root) (π2 body) (π3 var)]
         (λ 0 (root π1) (body π2) (var π3))))

(check-expect (inter 2 LAM 'root '(() ...))
              (list (LAM 'body) '(() ...)))
(check-expect (inter 2 LAM 'body '(() ...))
              (list (LAM 'root) '(() ...)))
(check-expect (inter 2 LAM 'root '(() ...))
              (list (LAM 'var) '(() ...)))
(check-expect (inter 2 LAM 'var '(() ...))
              (list (LAM 'root) '(() ...)))

;; G(@)
(define APP
  (graph [(π1 cont) (π2 fun) (π3 arg)]
         (@ 0 (fun π2) (cont π1) (arg π3))))

(check-expect (inter 2 APP 'fun '(() ...))
              (list (APP 'cont) '(() ...)))
(check-expect (inter 2 APP 'cont '(() ...))
              (list (APP 'fun) '(() ...)))
(check-expect (inter 2 APP 'fun '(() ...))
              (list (APP 'arg) '(() ...)))
(check-expect (inter 2 APP 'arg '(() ...))
              (list (APP'fun) '(() ...)))

;; G(cross, bracket)
(define CBRAC
  (graph [(π1 ) (π2 out)]
         (x 1 (π3 π4) ( π1))
         (~ 0 (out π2) (π4 π3))))

(check-expect (inter 2 CBRAC ' '(a ...))
              (list (CBRAC 'out) '((a . x) ...)))
(check-expect (inter 2 CBRAC 'out '((a . x) ...))
              (list (CBRAC ') '(a ...)))

;; G(\x.x)
(define ID
  (graph [(π1 )]
         (λ 0 ( π1) (l4 l2) (l5 l3))
         (x 0 (l3 l5) (l2 l4))))

(check-expect (inter 3 ID ' '(() ...))
              (list (ID ') '(( . x) () ...)))
(check-expect (inter 2 ID ' '(( . x) () ...))
              (list (ID ') '(() ...)))

(define CHINK
  (graph [(π1 ) (π2 out)]
         ( (λ (c) (printf "in : ~a~n" (proj c 5)))
             (λ (c) (printf "out: ~a~n" (proj c 5)))
             ( π1)
             (out π2))))

(check-expect (inter 5 CHINK ' (proj (○^i 1) 5))
              (list (CHINK 'out) (proj (○^i 1) 5)))

(check-expect (inter 5 CHINK 'out (proj (○^i 1) 5))
              (list (CHINK ') (proj (○^i 1) 5)))


;; G_cbn((\f.((ff)(\y.y))(\x.x))
(define NNH
  (graph [(π1 )]
         (@  0 (π4  π2)  ( π1)  (π5  π3))
         (λ  0 (π2  π4)  (π7 π5)  (π22 π6))
         (@  0 (π15 π9)  (π5 π7)  (π10 π8))
         (@  0 (π18 π17) (π9 π15) (π21 π16))
         (f  0 (π20 π19) (π17 π18))
         ( 0 (π6  π22) (π19 π20) (π16 π21))
         (λ  1 (π8  π10) (π13 π11) (π14 π12))
         (y  1 (π12 π14) (π11 π13))
         (λ  1 (π3 π24) (π27 π25) (π23 π26))
         (x  1 (π26 π23) (π25 π27))))

;; G_cbn((\s.\z.s(sz)))
(define TWO
  (graph [(π1 )]
         (λ  0 ( π1)   (π4 π2)   (π13 π3))
         (λ  0 (π2 π4)   (π7 π5)   (π27 π6))
         (@  0 (π10 π9)  (π5 π7)   (π20 π8))
         (@  1 (π18 π19) (π8 π20)  (π22 π21))
         ( 0 (π3 π13)  (π11 π12) (π15 π14))
         (s  0 (π12 π11) (π9 π10))
         (s  1 (π16 π17) (π19 π18))
         (~  0 (π14 π15) (π17 π16))
         (~  0 (π6 π27)  (π25 π26))
         (~  1 (π26 π25) (π23 π24))
         (z  2 (π24 π23) (π21 π22))))

;; What's your head variable?
;; The left occurrence of s.
(check-expect (inter 2 TWO ' '(( )))           
              (list (TWO ')  '(( L . s) ())))  

;; What's the head variable of its first argument?
;; The right occurrence of s, in the box bound to α.
(check-expect (inter 2 TWO ' '(( L . s) ( . α) ())) 
              (list (TWO ')  '(( R α . s) ( ))))

;; And the head variable of its first argument?
;; z, in the box bound to β, in the box bound to α.
(check-expect (inter 2 TWO ' '(( R α . s) ( . β) ( )))
              (list (TWO ')  '((  α β . z) ( ))))


(define SUCC ;: !Int --o Int
  (graph [(π1 )]
         (λ 0 ( π1) (π4 π2) (π7 π3))
         (δ 0 add1 (π6 π5) (π2 π4))
         (α 0 (π3 π7) (π5 π6))))

;; What's the output?
;; What's the input?
(check-expect (inter 2 SUCC ' '(( ?) ( )))
              (list (SUCC ')  '(( . α) ?)))

;; The input is 5.
;; The output is 6.
(check-expect (inter 1 SUCC ' '(( . α) 5))
              (list (SUCC ')  '(( . 6))))

;; λf.f(f3) vs succ
(define EG
  (graph [(a0 )]
         (@ 0 (p1 a1) ( a0) (c1 a2))
         
         ;; The chink in the wall.
         ( (λ (c) (printf "C: ~a~n" (proj c 3)))
            (λ (c) (printf "S: ~a~n" (proj c 3)))
            (a2 c1)
            (s1 c2))
         
         ;; succ
         (λ 1 (c2 s1) (s4 s2) (s7 s3))
         (δ 1 add1 (s6 s5) (s2 s4))
         (α 1 (s3 s7) (s5 s6))
         
         ;; λf.f(f3)
         (λ  0 (a1 p1) (p4 p2) (p11 p3))
         (@  0 (p7 p6) (p2 p4) (p17 p5))
         (@  1 (p15 p16) (p5 p17) (p19 p18))
         ('3 2 (p18 p19))
         (f  0 (p9 p8) (p6 p7))
         (f  1 (p13 p14) (p16 p15))
         ( 0 (p3 p11) (p8 p9) (p12 p10))
         (~  0 (p10 p12) (p14 p13))))

(check-expect (inter 1 EG ' '(( ?) ()))
              (list (EG ')  '(5)))

(test)