Created
December 7, 2012 21:03
-
-
Save ympbyc/4236507 to your computer and use it in GitHub Desktop.
Krivine's Machine
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
;;;; Krivine's Machine in Scheme ;;;; | |
;;; 2012 Minori Yamashita <[email protected]> ;;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))])) |
Author
ympbyc
commented
Dec 8, 2012
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment