;		    MetaScheme, or untyped MetaOCaml
;
; We implement four MetaOCaml special forms -- bracket, escape, 
; CSP (aka `lift'), and run -- in R5RS Scheme. Actually, we implement only 
; bracket and CSP -- and use unquote for escape and eval for run. 
;
; We shall use S-expressions to represent code values (so we can print them)
; and we treat `bracket' as a special form (aka, macro). One may think
; that 'bracket' is simply quasiquote. In fact, the "similarity" between
; bracket and quasiquote is often mentioned in the literature. The similarity
; is quite remote however. The principal distinction from standard 
; Scheme's quasiquote and unquote is hygiene. Our goal, set by 
; Chung-chieh Shan, is to make
;
; (let ((eta (lambda (f) (bracket (lambda (x) (escape (f (bracket x))))))))
; (bracket (lambda (x) (escape (eta (lambda (y) (bracket (+ x (escape y)))))))))
;
; to evaluate to the S-expression
; (lambda (x_1) (lambda (x_2) (+ x_1 x_2)))
;
; Note the renaming! If bracket were quasiquote and escape the unquote,
; the above expression would give
;   (lambda (x) (lambda (x) (+ x x)))
; which is the wrong result!
;
; To maintain the hygiene, we need to make sure that every evaluation of
; (bracket (lambda (x) body)) gives '(lambda (x_new) body) with 
; the unique x_new. We stress every *run-time* evaluation of the bracket form
; should produce code expressions with unique bound variables. 
; One may think that 'bracket' can be implemented as a macro that
; scans its body and makes all bound variables unique. Although that
; would work in many cases, it is not sufficient at all. Please see
; hyg-test below for an example (which involves recursion while building
; the code expression). That test shows that static renaming is not sufficient.
; We really need dynamic renaming.
;
; We implement the very clever suggestion by Chung-chieh Shan
; and represent the staged expression .<(fun x -> x + 1) 3>.
; by the sexp-generating expression
;    `(,(let ((x (gensym))) `(lambda (,x) (+ ,x 1))) 3)
; which generates the sexp
;    ((lambda (x_1) (+ x_1 1)) 3)
;
; Realizing this program indeed requires keeping track of levels of brackets
; and escapes.
;
; Alternatively, one may choose (bracket e) to be (lambda () e)
; but then we have problem implementing escapes. We will have to 
; reimplement our MetaFX paper. Also, we won't be able to easily print
; out code values.
;
; One should be wary of representing (bracket e) as (syntax e) and playing
; to much with `syntax' representations: we must maintain the proper stage
; separation: _nothing_ should be printed when evaluating
;   (lambda (x) (bracket (escape (begin (display "OK") (bracket '())))))
; The output is created only when the function is being applied!
;
; Another interesting question is the cross-stage facility -- often called 
; `lift', to lift values from one level to the later one. We use (% e) to
; mark e as a CSP value, which expands into (unquote (lift e)). The function
; lift must obey the invariant
;   (eval (lift x)) === x for any x
;
; One may think that such a lifting is already available in Scheme: quote
;  (define (lift x) (list 'quote x))
; or, more cryptically,
;  (define (lift x) `',x)
;
; Indeed, it works in simple cases
;     (let ((x '(1 2 3))) (eval (lift x)))
;     ; yields value: (1 2 3)
; Note, just 
;     (let ((x '(1 2 3))) (eval x))
; gives an error: attempt to call a non-procedure in (1 2 3)
;
; Alas, lifting by quotation is neither portable nor universal: it is not
; guaranteed to lift any value in any Scheme system. Although this lifting
; seems to work in Petite Chez Scheme, it gives warning in Scheme48 when
; evaluating 
;   (eval (lift (lambda (x) x)))
; (although it still seem to work).
;
; According to R5RS, the argument of a quotation is an _external_
; representation of a Scheme datum. Closures, for example, are not
; guaranteed to have an external representation.
;
; For portability, we implement CSP via a reference in an array.
; We take advantage of the fact that both the index (a number) and
; the name of the array (an identifier) have external representations
; and hence are trivially liftable by quotation. This
; is precisely the mechanism used by the current version of MetaOCaml.

; This file has been tested with Petite Chez Scheme, SCM 5e1 
; (invoke as: scm -r5) and Scheme48 1.3.
; 
; $Id$


;---------- Platform-specific section: various printing functions

; For Petite-Chez Scheme
(print-graph #t)			; to make printing code meaningful

; For SCM Scheme system
;; (define gensym gentemp)
;; (define pp print)
;; (define (expand x) (macroexpand x))

;; ; For Scheme48 system
;; ,open pp
;; (define pretty-print p)
;; (define old-eval eval)
;; (define (eval x) (old-eval x (interaction-environment)))
;; (define (expand x) #f) ; should use ,expand form
;; (define gensym
;;   (let ((count 0))
;;     (lambda ()
;;       (set! count (+ 1 count))
;;       (string->symbol (string-append "g-"
;; 			(number->string count))))))


;---------- End of Platform-specific section

; Check if the argument is an identifier....
(define-syntax symbol??
  (syntax-rules ()
    ((symbol?? (x . y) kt kf) kf)	; It's a pair, not a symbol
    ((symbol?? #(x ...) kt kf) kf)	; It's a vector, not a symbol
    ((symbol?? maybe-symbol kt kf)
      (let-syntax
	((test
	   (syntax-rules ()
	     ((test maybe-symbol t f) t)
	     ((test x t f) f))))
	(test abracadabra kt kf)))))

; Making sure all manifestly bound identifiers will be unique
; every time a bracketed expression is evaluated.
; By manifestly bound we mean identifiers that are explicitly bound
; by (unquoted) lambdas. We may easily extend the code below to account
; for other binding forms such as let. In fact, we support
; the simple (let ((x e)) body) form.
; No replacement is done in (strongly) quoted expressions.
; The implementation is a CEK machine with defunctionalized
; continuations.
; We have to account for the possible nesting of brackets. The argument
; `level' below keeps track of levels, in unary: () means the 0-th
; level, (1) means one level of quotation, (1 1) means two levels of
; quotation, etc.

(define-syntax bracket
  (syntax-rules (lambda let quote unquote bracket %)
    ((bracket e) (bracket e () ("up-level") (1)))
    ((bracket (quote e) env stack level)    ; leave quoted expressions intact
      (applyK (quote e) stack level))
    ((bracket (lambda (x) e) env stack level)
      (bracket e (x . env) (("make-lambda" x) . stack) level))
    ((bracket (bracket e) env stack level)
      (bracket e env ("up-level" . stack) (1 . level)))
    ((bracket (% e) env stack level)
      (bracket (unquote (lift e)) env stack level))
    ((bracket (unquote e) env stack (1 . level))
      (bracket e env ("down-level" . stack) level))
    ((bracket (let ((x e)) body) env stack level)
      (bracket ((lambda (x) body) e) env stack level))
    ((bracket (e1 e2 ...) env stack level)
      (bracket e1 env (("app-args" () (e2 ...) env) . stack) level))

    ((bracket x env stack ())		; At level 0, no translation
      (applyK x stack ()))

    ((bracket x env stack level)	; check if the argument is an identifier
      (symbol?? x
	; if x is a symbol...
	(letrec-syntax
	  ((find
	     (syntax-rules (x)
	       ((find ?x () ?stack) (applyK ?x ?stack level))
	       ((find ?x (x . _) ?stack) (applyK (unquote ?x) ?stack level))
	       ((find ?x (_ . ?env) ?stack) (find ?x ?env ?stack)))))
	  (find x env stack))
	; if x is not a symbol: a number, boolean, etc.
	(applyK x stack level)))
    ))

(define-syntax applyK
  (syntax-rules ()
    ((applyK e () level) e)
    ((applyK e ("up-level" . stack) (1 . level))
      (applyK (quasiquote e) stack level))
    ((applyK e ("down-level" . stack) level)
      (applyK (unquote e) stack (1 . level)))
    ((applyK e (("make-lambda" x) . stack) ()) ; at level 0
      (applyK (lambda (x) e) stack ()))
    ((applyK e (("make-lambda" x) . stack) level)
      (applyK 
	(unquote (let ((x (gensym))) (list 'lambda `(,x) `e))) stack level))
    ((applyK e (("app-args" (done ...) () env) . stack) level)
      (applyK (done ... e) stack level))
    ((applyK e (("app-args" (done ...) (e2 . other) env) . stack) level)
      (bracket e2 env (("app-args" (done ... e) other env) . stack) level))
    ))

;----- tests
; We use Petite Chez Scheme's facilities to print out the result
; of macro-expansion (the procedure 'expand').
; Other Scheme systems have something similar (often called
; macroexpand, macroexpander, etc)


(expand '(bracket (lambda (x) x)))
; Petite: ((lambda (#0=#:x) (list 'lambda (#2%list #0#) #0#))
;          (gensym))
(pretty-print (bracket (lambda (x) x)))
; Petite: (lambda (#0=#:g1402) #0#)
; SCM: (lambda (scm:G24) scm:G24)


(pretty-print (bracket (lambda (x) 'x)))
; Petite: (lambda (#:g1405) 'x)
; SCM: (lambda (scm:G25) (quote x))

(expand (bracket 3))
; 3

(pretty-print (bracket (lambda (x) (lambda (x) (x x)))))
; Petite: '(lambda (#:g1406) (lambda (#0=#:g1407) (#0# #0#)))
; Scheme48:  (lambda (g-5) (lambda (g-6) (g-6 g-6)))
; SCM: (lambda (scm:G26) (lambda (scm:G27) (scm:G27 scm:G27)))

; The expansion result shows that every application of the
; function will give code expression with the unique bound variable
(expand '(lambda (f) (bracket (lambda (x) ,(f (bracket x))))))
;; (lambda (#0=#:f)
;;   ((lambda (#1=#:x) (list 'lambda (#2%list #1#) (#0# #1#)))
;;    (gensym)))


(newline)
(display "The Eta example")
(newline)
(let*
  ((eta (lambda (f) 
	  (display "in eta") (newline)
	  (bracket (lambda (x) ,(f (bracket x))))))
   (cde
     (begin
       (display "before evaluating bracket") (newline)
       (bracket (lambda (x) ,(eta (lambda (y) (bracket (+ x ,y))))))))
   (_ (begin (display "cde") (newline) (pretty-print cde) (newline)))
   )
  (((eval cde) 2) 3))


; printed:
;; before evaluating bracket
;; in eta
;; cde
;; (lambda (#0=#:g1432) (lambda (#1=#:g1434) (+ #0# #1#)))
; evaluated to:
; 5
;
; In SCM, the printed expression looks lie
; (lambda (scm:G30)
;  (lambda (scm:G32) (+ scm:G30 scm:G32)))
;
; In Scheme48, the printed expression is
; (lambda (g-7)
;   (lambda (g-8) (+ g-7 g-8)))

(newline)
(display "The dynamic hygiene test") (newline)
(let ()
 (define (hyg-rec t x)
   (bracket (lambda (y) 
	    (,(if t (hyg-rec #f (bracket y)) 
	       (bracket (lambda (z) (+ z y))))
	     ,x))))
  (display "hyg-rec") (newline)
  (pretty-print (hyg-rec #t (bracket 1)))
  (display "hyg-rec result") (newline)
  (display ((eval (hyg-rec #t (bracket 1))) 4))
  (newline)
)
;; Note that all bound identifiers are unique!
;; Petite:
;; (lambda (#0=#:g1408)
;;   ((lambda (#1=#:g1409)
;;      ((lambda (#2=#:g1410) (+ #2# #1#)) #0#))
;;    1))
;; hyg-rec result
;; 5

;; In Scheme48, the generated code expression looks like
;; (lambda (g-9)
;;   ((lambda (g-10)
;;      ((lambda (g-11) (+ g-11 g-10)) g-9))
;;    1))


; Implementing CSP

; For Petite-Chez, one may define quotable? to always return #t
; (define (quotable? x) #t)

(define (quotable? x)
  (or (number? x) (char? x) (string? x) (boolean? x) (symbol? x)))

; More properly, this should be a weak finite map (weak hash table)
(define csp-table (vector 0)) ; first elem is the current free elem
(define (csp-add x)
  (let ((i (+ 1 (vector-ref csp-table 0)))
	(len (vector-length csp-table)))
    (if (>= i len)
      (let ((new-len (+ len len)))
	(do ((nv (make-vector new-len)) (i 0 (+ 1 i)))
	  ((>= i len) (set! csp-table nv) (csp-add x))
	  (vector-set! nv i (vector-ref csp-table i))))
      (begin
	(vector-set! csp-table 0 i)
	(vector-set! csp-table i x)
	i))))

(define (lift x)
  (if (quotable? x) `',x
    `(vector-ref csp-table ,(csp-add x))))

; simple tests
(let ((x '(1 2 3))) (eval (bracket (% x))))
; => (1 2 3)
(let ((x (lambda (x) x))) ((eval (bracket (% x))) 42))
; 42

(pretty-print (bracket (lambda (x) ((% list) x 3 #t "abc"))))
;; (lambda (#0=#:g1423)
;;   ((vector-ref csp-table 3) #0# 3 #t "abc"))

(pretty-print ((eval (bracket (lambda (x) ((% list) x 3 #t "abc")))) 42))
; => (42 3 #t "abc")

; example with CSP and several levels.
; The following two examples (ex8 and ex9) is from the MetaFX collection
; of translation examples.

; In MetaOCaml:
;; let ex8 = let id x = print_string "here"; x 
;; 	in .<fun x -> .<.~(id .~(id .<.<x>.>.))>.>.;;
;; Note that unquote also stands for CSP!
(let*
  ((id (lambda (x) (display "here") (newline) x))
   (ex8
     (begin
       (display "before ex8") (newline)
       (bracket (lambda (x) 
		  (bracket ,((% id) ,(id (bracket (bracket (% x))))))))))
   (_ (begin 
	(display "result of ex8") (newline)
	(pretty-print ex8)))
   (ex8r ((eval ex8) 1))
   )
  (begin 
    (display "result of ex8r") (newline)
    (pretty-print ex8r)))

;; before ex8
;; here
;; result of ex8
;; (lambda (#0=#:g1413) `,('#<procedure> `,(lift #0#)))
;; here
;; result of ex8r
;; '1

; In case of Scheme48, the printed expression is
;; (lambda (g-10)
;;   `,((vector-ref csp-table 4) `,(lift g-10)))
; Note the two occurrences of CSPs in the result of ex8


; In MetaOCaml:
;; let ex9 = let id x = print_string "here"; x 
;; 	in .<fun y -> .<fun x -> .~(id .~(id .<.<x>.>.))>.>.;;

(let*
  ((id (lambda (x) (display "here") (newline) x))
   (ex9
     (begin
       (display "before ex9") (newline)
       (bracket (lambda (y) 
	 (bracket 
	   (lambda (x) ,((% id) ,(id (bracket (bracket x))))))))))
   (_ (begin 
	(display "result of ex9") (newline)
	(pretty-print ex9)))
   (ex9r ((eval ex9) 1))
   (_
     (begin 
       (display "result of ex9r") (newline)
       (pretty-print ex9r)))
    )
  (pretty-print ((eval ex9r) 10)))

;; before ex9
;; here
;; result of ex9
;; (lambda (#:g1426)
;;   `,(let ([x (gensym)])
;;       (list 'lambda `(,x) `,((vector-ref csp-table 6) `,x))))
;; here
;; result of ex9r
;; (lambda (#0=#:g1431) #0#)
;; 10

; In case of Scheme48, the printed code expressions are
;; (lambda (g-11)
;;   `(lambda (g-12)
;;      ,((vector-ref csp-table 5) `g-12)))
;; (lambda (g-12) g-12)

; The power example
'(define (power n x)
  (cond 
    ((zero? n) (bracket 1))
    ((even? n) (bracket
		 (let ((x2 (* ,x ,x)))
		   ,(power (quotient n 2) (bracket x2)))))
    (else (bracket (* ,x ,(power (- n 1) x))))))

(define (power n x)
  (cond
    ((zero? n) (bracket 1))
    ((= 1 n) x)
    (else (bracket
	    (let ((y (* ,x ,x)))
	      ,(let ((c (power (quotient n 2) (bracket y))))
		 (if (even? n)
		   c
		   (bracket (* ,x ,c)))))
	    ))))

(define (powern n)
 (bracket (lambda (x) ,(power n (bracket x)))))

(newline)
(display "The power example") (newline)
(let ()
  (display "powern 7") (newline)
  (pretty-print (powern 7)) (newline)
  (display "power 7 2") (newline)
  (pretty-print ((eval (powern 7)) 2)) (newline))

;; powern 7
;; (lambda (#0=#:g1434)
;;   ((lambda (#1=#:g1435)
;;      (* #0# ((lambda (#2=#:g1436) (* #1# #2#)) (* #1# #1#))))
;;    (* #0# #0#)))
;;
;; power 7 2
;; 128

;; In SCM, the printed code looks like:
;; (lambda (scm:G37)
;;   ((lambda (scm:G38)
;;      (* scm:G37
;;         ((lambda (scm:G39) (* scm:G38 scm:G39))
;;          (* scm:G38 scm:G38))))
;;    (* scm:G37 scm:G37)))