256 lines
7.2 KiB
Scheme
256 lines
7.2 KiB
Scheme
(module iswim mzscheme
|
|
(require (lib "reduction-semantics.ss" "reduction-semantics")
|
|
(lib "subst.ss" "reduction-semantics")
|
|
(lib "contract.ss"))
|
|
|
|
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
|
;; Expression grammar:
|
|
|
|
(define iswim-grammar
|
|
(language (M (M M)
|
|
(o1 M)
|
|
(o2 M M)
|
|
V
|
|
("letcc" X M)
|
|
("cc" M M))
|
|
(V X
|
|
("lam" variable M)
|
|
b
|
|
("[" M "]"))
|
|
(X variable)
|
|
(b number)
|
|
(o1 "add1" "sub1" "iszero")
|
|
(o2 "+" "-" "*" "^")
|
|
(on o1 o2)
|
|
|
|
;; Evaluation contexts:
|
|
(E hole
|
|
(E M)
|
|
(V E)
|
|
(o1 E)
|
|
(o2 E M)
|
|
(o2 V E)
|
|
("cc" E M)
|
|
("cc" V E))
|
|
|
|
;; Continuations (CK machine):
|
|
(k "mt"
|
|
("fun" V k)
|
|
("arg" M k)
|
|
("narg" (V ... on) (M ...) k))
|
|
|
|
;; Environments and closures (CEK):
|
|
(env ((X = vcl) ...))
|
|
(cl (M : env))
|
|
(vcl (V- : env))
|
|
|
|
;; Values that are not variables:
|
|
(V- ("lam" variable M)
|
|
b)
|
|
|
|
;; Continuations with closures (CEK):
|
|
(k- "mt"
|
|
("fun" vcl k-)
|
|
("arg" cl k-)
|
|
("narg" (vcl ... on) (cl ...) k-))))
|
|
|
|
(define M? (language->predicate iswim-grammar 'M))
|
|
(define V? (language->predicate iswim-grammar 'V))
|
|
(define o1? (language->predicate iswim-grammar 'o1))
|
|
(define o2? (language->predicate iswim-grammar 'o2))
|
|
(define on? (language->predicate iswim-grammar 'on))
|
|
(define k? (language->predicate iswim-grammar 'k))
|
|
|
|
(define env? (language->predicate iswim-grammar 'env))
|
|
(define cl? (language->predicate iswim-grammar 'cl))
|
|
(define vcl? (language->predicate iswim-grammar 'vcl))
|
|
(define k-? (language->predicate iswim-grammar 'k-))
|
|
|
|
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
|
;; Substitution:
|
|
|
|
;; The subst form makes implemention of capture-avoiding
|
|
;; easier. We just have to describe how variables bind
|
|
;; in our language's forms.
|
|
|
|
(define iswim-subst/backwards
|
|
(subst
|
|
[(? symbol?) (variable)]
|
|
[(? number?) (constant)]
|
|
[`("lam" ,X ,M)
|
|
(all-vars (list X))
|
|
(build (lambda (X-list M) `("lam" ,(car X-list) ,M)))
|
|
(subterm (list X) M)]
|
|
[`(,(and o (or "add1" "sub1" "iszero")) ,M1)
|
|
(all-vars '())
|
|
(build (lambda (vars M1) `(,o ,M1)))
|
|
(subterm '() M1)]
|
|
[`(,(and o (or "+" "-" "*" "^")) ,M1 ,M2)
|
|
(all-vars '())
|
|
(build (lambda (vars M1 M2) `(,o ,M1 ,M2)))
|
|
(subterm '() M1)
|
|
(subterm '() M2)]
|
|
[`(,M1 ,M2)
|
|
(all-vars '())
|
|
(build (lambda (empty-list M1 M2) `(,M1 ,M2)))
|
|
(subterm '() M1)
|
|
(subterm '() M2)]
|
|
[`("letcc" ,X ,M)
|
|
(all-vars (list X))
|
|
(build (lambda (X-list M) `("letcc" ,(car X-list) ,M)))
|
|
(subterm (list X) M)]
|
|
[`("cc" ,M1 ,M2)
|
|
(all-vars '())
|
|
(build (lambda (vars M1 M2) `("cc" ,M1 ,M2)))
|
|
(subterm '() M1)
|
|
(subterm '() M2)]
|
|
[`("[" ,E "]")
|
|
(all-vars '())
|
|
(build (lambda (vars) `("[" ,E "]")))]))
|
|
|
|
|
|
;; the argument order for the subst-generated function
|
|
;; doesn't match the order in the notes:
|
|
(define (iswim-subst M Xr Mr)
|
|
(iswim-subst/backwards Xr Mr M))
|
|
|
|
(define empty-env '())
|
|
|
|
;; Environment lookup
|
|
(define (env-lookup env X)
|
|
(let ([m (assq X env)])
|
|
(and m (caddr m))))
|
|
|
|
;; Environment extension
|
|
(define (env-extend env X vcl)
|
|
(cons (list X '= vcl) env))
|
|
|
|
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
|
;; Reductions:
|
|
|
|
;; beta_v reduction
|
|
(define beta_v
|
|
(reduction iswim-grammar
|
|
(("lam" X_1 M_1) V_1)
|
|
(iswim-subst (term M_1) (term X_1) (term V_1))))
|
|
|
|
|
|
(define delta
|
|
(list
|
|
(reduction iswim-grammar ("add1" b_1) (add1 (term b_1)))
|
|
(reduction iswim-grammar ("sub1" b_1) (sub1 (term b_1)))
|
|
(reduction iswim-grammar ("iszero" b_1)
|
|
(if (zero? (term b_1))
|
|
'("lam" x ("lam" y x))
|
|
'("lam" x ("lam" y y))))
|
|
(reduction iswim-grammar ("+" b_1 b_2) (+ (term b_1) (term b_2)))
|
|
(reduction iswim-grammar ("-" b_1 b_2) (- (term b_1) (term b_2)))
|
|
(reduction iswim-grammar ("*" b_1 b_2) (* (term b_1) (term b_2)))
|
|
(reduction iswim-grammar ("^" b_1 b_2) (expt (term b_1) (term b_2)))))
|
|
|
|
;; ->v
|
|
(define ->v (map (lambda (red)
|
|
(compatible-closure red iswim-grammar 'M))
|
|
(cons beta_v delta)))
|
|
|
|
;; :->v
|
|
(define :->v (map (lambda (red)
|
|
(context-closure red iswim-grammar 'E))
|
|
(cons beta_v delta)))
|
|
|
|
;; :->v+letcc
|
|
(define :->v+letcc (append
|
|
:->v
|
|
(list
|
|
|
|
;; letcc rule:
|
|
(reduction
|
|
iswim-grammar
|
|
(in-hole E_1 ("letcc" X_1 M_1))
|
|
(plug (term E_1)
|
|
(iswim-subst (term M_1) (term X_1) `("["
|
|
,(plug (term E_1) '||)
|
|
"]"))))
|
|
|
|
;; cc rule:
|
|
(reduction
|
|
iswim-grammar
|
|
(in-hole E ("cc" ("[" (in-hole E_2 ||) "]") V_1))
|
|
(plug (term E_2) (term V_1))))))
|
|
|
|
|
|
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
|
;; Helpers:
|
|
|
|
(define (delta*n on Vs)
|
|
(let ([l (reduce delta `(,on ,@Vs))])
|
|
(if (null? l)
|
|
#f
|
|
(car l))))
|
|
|
|
(define (delta*1 o1 V)
|
|
(delta*n o1 (list V)))
|
|
|
|
(define (delta*2 o2 V1 V2)
|
|
(delta*n o2 (list V1 V2)))
|
|
|
|
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
|
;; Abbreviations:
|
|
|
|
(define (if0 test then else)
|
|
(let ([X (variable-not-in `(,then ,else) 'X)])
|
|
`(((("iszero" ,test) ("lam" ,X ,then)) ("lam" ,X ,else)) 77)))
|
|
|
|
(define true '("lam" x ("lam" y x)))
|
|
(define false '("lam" x ("lam" y y)))
|
|
(define boolean-not `("lam" x ((x ,false) ,true)))
|
|
|
|
(define mkpair '("lam" x ("lam" y ("lam" s ((s x) y)))))
|
|
(define fst '("lam" p (p ("lam" x ("lam" y x)))))
|
|
(define snd '("lam" p (p ("lam" x ("lam" y y)))))
|
|
|
|
(define Y_v '("lam" f ("lam" x
|
|
((("lam" g (f ("lam" x ((g g) x))))
|
|
("lam" g (f ("lam" x ((g g) x)))))
|
|
x))))
|
|
|
|
(define mksum `("lam" s
|
|
("lam" x
|
|
,(if0 'x 0 '("+" x (s ("sub1" x)))))))
|
|
(define sum `(,Y_v ,mksum))
|
|
|
|
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
|
;; Exports:
|
|
|
|
(provide/contract (iswim-grammar compiled-lang?)
|
|
(M? (any/c . -> . boolean?))
|
|
(V? (any/c . -> . boolean?))
|
|
(o1? (any/c . -> . boolean?))
|
|
(o2? (any/c . -> . boolean?))
|
|
(on? (any/c . -> . boolean?))
|
|
(k? (any/c . -> . boolean?))
|
|
(env? (any/c . -> . boolean?))
|
|
(cl? (any/c . -> . boolean?))
|
|
(vcl? (any/c . -> . boolean?))
|
|
(iswim-subst (M? symbol? M? . -> . M?))
|
|
(env-lookup (env? symbol? . -> . (union false/c vcl?)))
|
|
(env-extend (env? symbol? vcl? . -> . env?))
|
|
(empty-env env?)
|
|
(beta_v red?)
|
|
(delta (listof red?))
|
|
(delta*1 (o1? V? . -> . (union false/c V?)))
|
|
(delta*2 (o2? V? V? . -> . (union false/c V?)))
|
|
(delta*n (on? (listof V?) . -> . (union false/c V?)))
|
|
(->v (listof red?))
|
|
(:->v (listof red?))
|
|
(:->v+letcc (listof red?))
|
|
(if0 (M? M? M? . -> . M?))
|
|
(true M?)
|
|
(false M?)
|
|
(boolean-not M?)
|
|
(mkpair M?)
|
|
(fst M?)
|
|
(snd M?)
|
|
(Y_v M?)
|
|
(sum M?)))
|