; scheme translator for COL terms
; this need to be used as a stub for scheme col participants

(define (iscic? x) (eq? (car x) 'cic))
(define (iscrc? x) (eq? (car x) 'crc))
(define (iscsc? x) (eq? (car x) 'csc))
(define (isid? x) (eq? (car x) 'id))
(define (isind? x) (eq? (car x) 'ind))
(define (isapp? x) (eq? (car x) 'capp))
(define (isabs? x) (eq? (car x) 'cabs))
(define (arg x) (cadr x))
(define (arg2 x) (caddr x))
(define (arity x) (length (cdr x)))


; sample local services:
;(define f (lambda (x) (+ x 1)))
;(define g (lambda (f) (lambda (x) (f (+ x 1)))))

; sample clause generated by meta-compiler:
;(define (invmatch x)
;  (cond ((= x 0) 'f)
;        ((= x 1) 'g)
;	(#t '())
;  )
;)

;(define (match c)
;  (cond ((eq? c 'f) '(id 0))
;  	((eq? c 'g) '(id 1))
;	(#t	'error)))

; lookup label in environment at level l for index x
(define (tolabel l m x)
  (if (null? m) 'notfound
      (if (= (- l x) (caar m)) (cadar m)
	  (tolabel l (cdr m) x))))

	
; col to scheme translation (including cabs)
; the mutable variable i is used to generate free var labels
; l is the embedding level (initially 0)
; m is an association list matching labels to de Bruijn indices

(define (maketau i)
(define (cstau x l m)
 ; generate new variable symbols based on mutable var (not generalized!)
 (define (fresh) (begin 
		   (set! i (+ 1 i)) 
	    	   (string->symbol (string-append "v" (string (+ 48 i))))))
  (cond ((iscic? x) (arg x))
	((iscrc? x) (arg x))
	((iscsc? x) (arg x))
	((isid? x) (invmatch (arg x)))
	((isind? x) (tolabel l m (arg x)))
	((isapp? x) (cons (cstau (arg x) l m) (list (cstau (arg2 x) l m))))
	((isabs? x) (let ((bv (fresh))) 
		       (let ((m2 (cons (cons l (list bv)) m)))
		          (let ((body (cstau (arg x) (+ l 1) m2)))
		            (cons 'lambda (cons (list bv) 
			      (list body)))))))
  )
) cstau)



; solution can't be formed for converting a scheme lambda term to col form
;(eval uu user-initial-environment)
;(define h (tau '(cabs (cabs (capp (ind 1) (ind 2)))) 0 '()))
;(define p (eval h user-initial-environment))
;((p 3) f)


(define (maketau2 i)
 ; generate new variable symbols based on mutable var (not generalized!)
 (define (fresh) (begin 
		   (set! i (+ 1 i)) 
	    	   (string->symbol (string-append "v" (string (+ 48 i))))))
(define (tau x l m)
  (cond ((eq? (car x) 'cic) (cadr x))
	((eq? (car x) 'crc) (cadr x))
	((eq? (car x) 'csc) (cadr x))
	((eq? (car x) 'id) (invmatch (cadr x)))
	((eq? (car x) 'ind) (tolabel l m (cadr x)))
	((eq? (car x) 'capp) (cons (tau (cadr x) l m) 
                                   (list (tau (caddr x) l m))))
	((eq? (car x) 'cabs) (let ((bv (fresh))) 
              (let ((m2 (cons (cons l (list bv)) m)))
                 (cons 'lambda (cons (list bv) 
                                     (list (tau (cadr x) (+ l 1) m2)))))))
  )
) tau)

; (define cstau (maketau2 0))


; other direction:

(define (verylast l)
  (if (null? (cdr l)) (car l)
	(verylast (cdr l))))

(define (prelast l)
 (define (prel l)
   (if (null? (cdr l)) '() (cons (car l) (prel (cdr l))))
 )
  (let ((pl (prel l)))
     (if (null? (cdr pl)) (car l) pl)))

(define (toind l m symbol)
  (if (null? m) 'error
      (if (eq? symbol (cadar m)) (list 'ind (- l (caar m)))
	  (toind l (cdr m) symbol))))

(define (mksclosure t e) (list 'sclosure t e))


; direction scheme -> col:
; s assumed to be in long normal form (for now)
; enviornment created explicitly by user - '(sclosure (lambda ...) env)
; l is embedding level while m is like (ol symbol)::...
; note: sctau works on both curried and uncurried forms!
(define (sctau s l m env)
  (cond ((null? s) s)
	((integer? s) (list 'cic s))
	((real? s) (list 'crc s))
	((string? s) (list 'csc s))
	((symbol? s) (if (not (eq? (match s) 'error))      
			  (match s)
			   (let ((ind (toind l m s)))
			      (if (not (eq? ind 'error)) ind
			        (sctau (eval s env) 0 '() env))))) ; diverge?
        ((eq? (car s) 'sclosure) (sctau (cadr s) l m (caddr s)))
	((eq? (car s) 'lambda)				     
		(let ((m2 (cons (list l (caadr s)) m)))
		   (list 'cabs (sctau (caddr s) (+ l 1) m2 env))))
	(#t  (list 'capp (sctau (prelast s) l m env) 
			 (sctau (verylast s) l m env)))
  ))

; (sctau '(f (f 3)) 0 '() (the-environment))
; (sctau '(lambda (x) (lambda (y) (y x))) 0 '() (the-environment))
; (sctau '(lambda (x) (f x)) 0 '() (the-environment))


; tcp server setup

(define (servecol)
  (define (siport i o u) i)
  (define (soport i o u) o)
  (define (ciport i o) i)  ; not used
  (define (coport i o) o)  ; not used
  (define sfd (open-tcp-server-socket 20027))
  (define (session)
     (let ((cfd (tcp-server-connection-accept sfd #t)))
       (let ((scin (cfd siport)) (scout (cfd soport)))
	(serverloop scin scout))))
  (define (serverloop scin scout)
    (define cstau (maketau2 0))
      (let ((interm (read scin)))
        (if (or (eof-object? interm) (eq? interm '$.))
				(begin (close-port scin) 
				   (close-port scout) (session))
	    (let ((sterm (eval (cstau interm 0 '()) 
				user-initial-environment)))
	      (begin
	        (write (sctau sterm 
	                      0 '() user-initial-environment) scout)
	        (write-string ".$" scout)
	        (flush-output scout)
	        (serverloop scin scout))))))
  (session))


; Use for latest MIT scheme:
(define (startserver)
  (define sfd (open-tcp-server-socket 20027))
  (define (session)
     (let ((cfd (tcp-server-connection-accept sfd #t #f)))
	(serverloop cfd)))
  (define (serverloop cfd)
    (define cstau (maketau2 0))
      (let ((interm (read cfd)))
        (if (or (eof-object? interm) (eq? interm '$.))
				(begin (close-port cfd) (session))
	    (let ((sterm (eval (cstau interm 0 '()) 
				user-initial-environment)))
	      (begin
	        (write (sctau sterm 
	                      0 '() user-initial-environment) cfd)
	        (write-string ".$" cfd)
	        (flush-output cfd)
	        (serverloop cfd))))))
  (session))

;      (let ((interms (string-append "(" 
;		      (read-string (char-set) scin) ")")))
;	(let ((sstream (string->input-port interms)))
;           (let ((interm (read scin)))
;            (if (or (eof-object? interm) (eq? interm '$.) (eq? interm '()))
;				(begin (close-port scin) 
;				   (close-port scout) (session))
;	     (let ((sterm (eval (cstau interm 0 '()) 
; (tcp-server-connection-accept sfd #t #f)
; (close-tcp-server-socket sfd)


; This procedure can be used to invoke a remote form of "eval" on scheme:
; It is not as transparent as implementing versions of functions that
; can do this automatically.

; should work on both new and old versions of mit scheme:
; return a list (inputport outputport)
(define (open_col_session hostname)
 (define (ciport i o) i)
 (define (coport i o) o)
  (let ((cfd (open-tcp-stream-socket hostname 20027)))
    (if (port? cfd) (list cfd cfd) (list (cfd ciport) (cfd coport)))))

(define (close_col_session Session)
   (if (output-port? (car Session)) (close-port (car Session))
      (begin (close-input-port (car Session))
	      (close-output-port (cadr Session)))))

(define (remote_eval Term Env Session)
 (let ((cstau (maketau2 0)))
   (begin
     (write (sctau Term 0 '() Env) (cadr Session))
     (flush-output (cadr Session))
     (let ((la (peek-char (car Session))))
        (if (not (char=? la #\())	 ; discard .$
	       (begin (read-char (car Session))
		      (read-char (car Session))
		      (read-char (car Session)))))
     (let ((interm (read (car Session))))
	(if (not (eof-object? interm))
	  (eval (cstau interm 0 '()) user-initial-environment))))))

; use as in:
; (load "circles.sch") ; load stub generated by meta-compiler
; (define s (open_col_session "localhost"))
; (remote_eval '(square 3) (the-environment) s)
; ...
; (close_col_session s)