;		    MetaScheme, or untyped MetaOCaml
;
; We implement four MetaOCaml special forms -- bracket, escape, 
; CSP (aka `lift'), and run -- in 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).
; The biggest surprise of this project is that given the very `natural'
; representation choices above, we have to use syntax-case at least once, 
; to generate globally-unique identifiers. Alternatively, we can use
; lower-level facilities (such as defmacro, renaming-macros) if available.
; We give the example of both below.
;
; We could use 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)
; Alas, realizing this program makes us reimplement quasiquote, maintain
; syntactic environment, etc. We end up with essentially the implementation
; of syntax-case. We could just as well have used the R5RS portable
; macroexpander by Dybvig et al or by Petrofsky. If we use syntax-case or
; lower-level macros, the whole implementation becomes quite compact, see
; below.
;
; This shows that often mentioned `similarity' between bracket and
; quasiquote is deeply flawed. 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!
;
; The major difficulty is to decide what should be the representation
; of code values.
; One can 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 the code values.
;
; A better choice for code values appears to be S-expressions.
; But then we need to make identifiers bound by lambda in code expressions
; to be globally unique. By that we mean the symbol of the identifier
; must be globally unique rather than just its `color' (or timestamp),
; because the color of an identifier is disregarded in (quoted) S-expressions.
; Although syntax-rules can produce identifiers with globally-unique
; colors, they can't produce globally-unique symbols. We must use syntax-case!
; 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

; For a syntax-case system:

; The only (and necessary) appearance of syntax-case, to generate
; globally-unique identifier _symbols_
;    (mgensym op arg ...) expands into (op unique-id arg ...)
(define-syntax mgensym
  (lambda (x)
    (syntax-case x ()
      ((_ op arg ...)
	(with-syntax (((newid) (generate-temporaries '(1))))
	  (syntax (op newid arg ...)))))))

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

; For SCM Scheme system
(define (expand x) (display (eval x)))
(defmacro mgensym (op . args)
  (let ((newid (gentemp)))
    `(,op ,newid ,@args)))

; 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-syntax mgensym
  (let ((gensym
	  (let ((count 0))
	    (lambda ()
	      (set! count (+ 1 count))
	      (string->symbol (string-append "g-"
				(number->string count)))))))
  (lambda (form ren comp)
    (let ((op (cadr form))
	  (args (cddr form))
	  (newid (gensym))) 
      `(,op ,newid . ,args)))))

; For a Scheme system that provides define-macro
(define pp print)
(define (expand x) (macroexpand x))
(define-macro (mgensym op . args)
  (let ((newid (gensym)))
    `(,op ,newid ,@args)))

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

(define-syntax bracket
  (syntax-rules ()
    ((bracket x) (ALPHA `x))))

; Alpha-renaming of all manifestly bound identifiers.
; By manifestly bound we mean identifiers that are explicitly bound
; by (unquoted) lambdas. We may easily extend the ALPHA below to account
; for other binding forms such as let.
; No replacement is done in (strongly) quoted expressions.
; The implementation of ALPHA is a CEK machine with defunctionalized
; continuations.

(define-syntax ALPHA
  (syntax-rules (lambda quote bracket %)
    ((ALPHA t) (ALPHA t () ()))
    ((ALPHA (quote e) env stack)	; leave quoted expressions intact
      (applyK (quote e) stack))
    ((ALPHA (lambda (x) e) env stack)
     (let-syntax ((ren (syntax-rules ()
            ((ren ?newx ?x ?e ?env ?st) 
	      (ALPHA ?e ((?x ?newx) . ?env) (("make-lambda" ?newx) . ?st))))))
       (mgensym ren x e env stack)))
;; The following generates a uniquely colored identifier x (but not
;; a unique symbol. In quotes and quasiquotes, the color is disregarded
;;     ((ALPHA (lambda (x) e) env stack)
;;      (let-syntax ((ren (syntax-rules ()
;;             ((ren ?x ?e ?env ?st) 
;; 	      (ALPHA ?e ((?x x) . ?env) (("make-lambda" x) . ?st))))))
;;        (ren x e env stack)))
    ((ALPHA (bracket e) env stack)
      (ALPHA (quasiquote e) env stack))
    ((ALPHA (% e) env stack)
      (ALPHA (unquote (lift e)) env stack))
    ((ALPHA (e1 e2 ...) env stack)
      (ALPHA e1 env (("app-args" () (e2 ...) env) . stack)))

    ((ALPHA x env stack)		; apply the substitution env to x
      (letrec-syntax
	((find
	   (syntax-rules (x)
	     ((find ?x () ?stack) (applyK ?x ?stack))
	     ((find ?x ((x ?xnew) . _) ?stack) (applyK ?xnew ?stack))
	     ((find ?x (_ . ?env) ?stack) (find ?x ?env ?stack)))))
	(find x env stack)))
    ))

(define-syntax applyK
  (syntax-rules ()
    ((applyK e ()) e)
    ((applyK e (("make-lambda" x) . stack))
      (applyK (lambda (x) e) stack))
    ((applyK e (("app-args" (done ...) () env) . stack))
      (applyK (done ... e) stack))
    ((applyK e (("app-args" (done ...) (e2 . other) env) . stack))
      (ALPHA e2 env (("app-args" (done ... e) other env) . stack)))
    ))

;----- 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=#:g1404) #0#)
; SCM: (lambda (scm:G24) scm:G24)

(expand '(bracket (lambda (x) 'x)))
; Petite: '(lambda (#:g1405) 'x)
; SCM: (lambda (scm:G25) (quote x))

(expand '(bracket (lambda (x) (lambda (x) (x x)))))
; Petite: '(lambda (#:g1406) (lambda (#0=#:g1407) (#0# #0#)))
; SCM: (lambda (scm:G26) (lambda (scm:G27) (scm:G27 scm:G27)))

(expand '(lambda (f) (bracket (lambda (x) ,(f (bracket x))))))
; (lambda (#0=#:f) (#2%list 'lambda '(#1=#:g1408) (#0# '#1#)))


; The following shows result nicely only for Petite Chez
'(expand
  '(bracket (lambda (x) ,(eta (lambda (y) (bracket (+ x ,y)))))))
;; (#2%list
;;   'lambda
;;   '(#0=#:g1418)
;;   (eta (lambda (#1=#:g1419) (#2%list '+ '#0# #1#))))

(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-6)
;  (lambda (g-8) (+ g-6 g-8)))


; 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


; 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 (#:g1430)
;;   `(lambda (#0=#:g1431) ,(#<procedure> `#0#)))
;; 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)