Krivine's Machine

Krivine.scm

;;;; Krivine's Machine in Scheme ;;;;
;;; 2012 Minori Yamashita <ympbyc@gmail.com> ;;add your name here
;;;
;;; reference:
;;;   http://pauillac.inria.fr/~xleroy/talks/zam-kazam05.pdf
;;;   http://pop-art.inrialpes.fr/~fradet/PDFs/HOSC07.pdf

;;; Notes ;;;
;; CLOSURE creates thunks that packs the continuation and environment together. 
;; To create closures(function objects), CLOSURE the GRAB and expression followed by CONTINUE.
;;

(use srfi-1)

;;; Helpers ;;;

;;get the value associated with the key symbol
(define (assoc-ref env key)
  (let ((binding (assq key env)))
    (if binding (cdr binding) 'lookup-fail)))


;;; Krivine's Machine ;;;
(define (Krivine code env stack g-env) 
  (print (format "code : ~S" code))
  (print (format "env  : ~S" env))
  (print (format "stack: ~S" stack))
  (print (format "g-env: ~S" g-env))
  (newline)

  ;inst        inst-arg    code-rest  env stack global
  ((caar code) (cdar code) (cdr code) env stack g-env))

;; returns what's on the top of the stack
(define (STOP args code env stack g-env)
  (car stack))

;; cons a self-evaluating value on to the stack
(define (CONSTANT args code env stack g-env)
  (Krivine
    code
    env
    (cons (car args) stack)
    g-env))

;; refer a value associated with the character from either local-env or global-env
(define (ACCESS args code env stack g-env)
  (let ([val (assoc-ref env (car args))])
    (Krivine
      code
      env
      (if (eq? val 'lookup-fail) 
        (cons (assoc-ref g-env (car args)) stack)
        (cons val stack))
      g-env)))

;; retrieves a thunk from the stack and replace the state with its.
;; thunks carry all the continuation therefore no need to worry about the "frame" or "return"
(define (CONTINUE args code env stack g-env)
  (let* ([closure (car stack)]
         [c-code  (assoc-ref closure 'code)]
         [c-env   (assoc-ref closure 'env)])
  (Krivine
    c-code
    c-env
    (cdr stack)
    g-env)))

;; associate a stack-top value with the character and cons the pair onto the local-env
(define (GRAB args code env stack g-env)
  (Krivine
    code
    (cons `(,(car args) . ,(car stack)) env)
    (cdr stack)
    g-env))

;; creates a thunk that is a data carrying continuation + environment
(define (CLOSURE args code env stack g-env)
  (Krivine
    code
    env
    (cons `((code . ,(car args)) (env . ,env)) stack)
    g-env))

;; creates a global binding
(define (DEFINE args code env stack g-env)
  (Krivine
    code
    env
    (cdr stack)
    (cons `(,(car args) . ,(car stack)) g-env)))

;;;
;; N[n] = ACCESS(n); CONTINUE
;; N[λa] = GRAB; N[a]
;; N[b a] = CLOSURE(N[a]); N[b]
;;
;; M := x | M_1 M_2 | λx.M
;; (M N, S, E)     -> (M, (S,(N,E)), E)
;; (λM, (S,N), E)  -> (M, S, (E,N))
;; (i+1, S, (E,N)) -> (i, S, E)
;; (0, S, (E_1 (M, E_2))) -> (M, S, E_2)
;;To evaluate an application M N, the K-machine builds a closure made of the argument N
;;and the current environment E in the stack and proceeds with the reduction of the function
;;M. This is the first characteristic of the K-machine: a closure is built in constant time and includes the complete current environment.
;;The evaluation of a λ-abstraction places the argument (the stack’s top element) in the environment and proceeds with the body of the function. This is the second and more important characteristic of the K-machine: it strives not to build closures for functions. Other
;;abstract machines return functions as closures before applying them.
;;The evaluation of a variable i amounts to following i links to find the corresponding closure in the environment. The closure’s components become the current code and environment.
;;;

;;; experiment ;;;
;; (((λx.λy.y) 5) 6)   CLOSURE
;;                6      CONSTANT 6; STOP
;;  ((λx.λy.y) 5)      CLOSURE
;;             5         CONSTANT 5; STOP
;;   (λx.λy.y)         GRAB x
;;       λy.y          GRAB y
;;          y          ACCESS y; CONTINUE

;;Normal function application
;(print (Krivine `(
;  (,CLOSURE (
;    (,CONSTANT 6)
;    (,STOP)))
;  (,CLOSURE (
;    (,CONSTANT 5)
;    (,STOP)))
;  (,GRAB x)
;  (,GRAB y)
;  (,ACCESS y)
;  (,CONTINUE)
;) '() '() '()))

;;Closures
;(print (Krivine `(
;  (,CLOSURE (
;    (,GRAB x)
;    (,ACCESS x)
;    (,CONTINUE))) ;;普通の意味のクロージャ
;  (,DEFINE my-closure)
;  (,CLOSURE (
;    (,CONSTANT 5)
;    (,STOP))) ;;Thunk
;  (,ACCESS my-closure)
;  (,CONTINUE)
;) '() '() '()))


;;; Compiler ;;;

;;Helper
(define (atom? x)
  (cond
    [(string?  x) #t]
    [(number?  x) #t]
    [(boolean? x) #t]
    [(char?    x) #t]
    [else #f]))

;;compile :: Nadeko -> Krivine
(define (compile program)
  (fold-right compile- `((,STOP)) program))

;;compile- :: Nadeko -> code -> code
(define (compile- exp code)
  (print (format "exp : ~S" exp))
  (print (format "code: ~S" code))
  (newline)
  (cond
    [(atom? exp)
     (cons `(,CONSTANT ,exp) code)]

    [(symbol? exp)
     `((,ACCESS ,exp) (,CONTINUE))]

    [(eq? (car exp) 'quote)
     (cons `(,CONSTANT (cadr exp)) code)]

    [(eq? (car exp) ':=)
     (cons `(,CLOSURE ,(compile- (caddr exp) code))
       `((,DEFINE ,(cadr exp))))]

    [(eq? (car exp) '->)
     (cons `(,GRAB ,(caadr exp)) (compile- (caddr exp) code))]

    [else
     (cons `(,CLOSURE ,(compile- (cadr exp) code))
      (compile- (car exp) code))]))

Thunk+継続
つまり式+環境+継続

(print (Krivine `(
(,CLOSURE (
(,GRAB x)
(,ACCESS x)
(,TAILAPPLY))) ;;普通の意味のクロージャ
(,DEFINE my-closure)
(,CLOSURE (
(,CONSTANT 5)
(,STOP))) ;;プロミス(thunk)
(,ACCESS my-closure)
(,TAILAPPLY)
) '() '() '()))

`(
  (,CLOSURE (
    (,GRAB x)
    (,ACCESS x)
    (,TAILAPPLY))) ;;普通の意味のクロージャ
  (,DEFINE my-closure)
  (,CLOSURE (
    (,CONSTANT 5)
    (,STOP))) ;;Thunk
  (,ACCESS my-closure)
  (,TAILAPPLY)
)