1#lang racket
2(require redex)
3
4(provide (all-defined-out))
5
6;; This semantics comes from the paper
7;; _A Natural Semantics for Lazy Evaluation_,
8;; by John Launchbury, POPL 1993
9;; extended with integers, +, and if0.
10
11(define-language L
12  (e ::=
13     v
14     (e x)
15     (let ([x e] ...) e)
16     x
17     (+ e e)        ;; add addition
18     (if0 e e e))   ;; add conditional
19  (v ::=            ;; don't use 'z' for values,
20     ;;                because that's confusing
21     i              ;; add integer constants
22     (λ (x) e))
23
24  (i ::= integer)
25  (x y z ::= variable-not-otherwise-mentioned)
26
27  (Γ Δ Θ ::= · (Γ x ↦ e))
28
29  #:binding-forms
30  (let ([x e] ...) e_body #:refers-to (shadow x ...))
31  (λ (x) e #:refers-to x))
32
33(define-judgment-form L
34  #:mode (⇓ I I O O)
35  #:contract (⇓ Γ e Δ v)
36
37
38  [----------- Value
39   (⇓ Γ v Γ v)]
40
41
42  [(⇓ Γ e Δ (λ (y) e_*))
43   (⇓ Δ (substitute e_* y x) Θ v)
44   ------------------------- Application
45   (⇓ Γ (e x) Θ v)]
46
47
48  [(where (Γ x ↦ e) (separate Γ_* x))
49   (⇓ Γ e Δ v)
50   (where Δ_* (Δ x ↦ v))
51   ---------------------------------- Variable
52   (⇓ Γ_* x Δ_* v)]
53
54
55  [(⇓ (extend Γ (x_i e_i) ...) e Δ v)
56   ---------------------------------- Let
57   (⇓ Γ (let ([x_i e_i] ...) e) Δ v)]
58
59
60  [(⇓ Γ e_1 Θ i_1)
61   (⇓ Θ e_2 Δ i_2)
62   ---------------------------------------------- Add
63   (⇓ Γ (+ e_1 e_2) Δ ,(+ (term i_1) (term i_2)))]
64
65
66  [(⇓ Γ e_1 Θ i)
67   (⇓ Θ (choose i e_2 e_3) Δ v)
68   ---------------------------- If
69   (⇓ Γ (if0 e_1 e_2 e_3) Δ v)])
70
71(define-metafunction L
72  choose : i e e -> e
73  [(choose 0 e_1 e_2) e_1]
74  [(choose i e_1 e_2) e_2])
75
76(define-metafunction L
77  separate : Γ x -> (Γ x ↦ e) or ⊥
78  [(separate · x) ⊥]
79  [(separate (Γ x ↦ e) x) (Γ x ↦ e)]
80  [(separate (Γ y ↦ e_*) x)
81   ((Γ_* y ↦ e_*) x ↦ e)
82   (where (Γ_* x ↦ e) (separate Γ x))]
83  [(separate (Γ y ↦ e_*) x) ⊥
84   (where ⊥ (separate Γ x))])
85
86(define-metafunction L
87  extend : Γ (x e) ... -> Γ
88  [(extend Γ) Γ]
89  [(extend Γ (x e) (x_* e_*) ...)
90   (extend (Γ x ↦ e) (x_* e_*) ...)])
91
92
93
94(define e? (redex-match? L e))
95(define v? (redex-match? L v))
96(define T-v? (redex-match? L (T v)))
97
98
99;; run a program to get it's result
100(define/contract (run p)
101  (-> e? (or/c v? #f))
102  (define vs (judgment-holds (⇓ · ,p Δ v) v))
103  (cond
104    [(pair? vs)
105     (unless (= 1 (length vs))
106       (error 'run "multiple results ~s" vs))
107     (car vs)]
108    [else #f]))
109
110;; opens a visualization of the derivation
111(define (show p)
112  (-> e? void?)
113  (show-derivations
114   (build-derivations
115    (⇓ · ,p Δ v))))
116
117(module+ test
118
119  (default-language L)
120
121  ;; replace-free, rename-bound, and subst tests omitted, since those metafunctions are gone
122
123  (test-equal (term (separate · x)) (term ⊥))
124  (test-equal (term (separate (· x ↦ 1) x)) (term (· x ↦ 1)))
125  (test-equal (term (separate ((· x ↦ 1) y ↦ 2) x))
126                (term ((· y ↦ 2) x ↦ 1)))
127  (test-equal (term (separate (· x ↦ 1) y)) (term ⊥))
128
129  ;; ^ tests omitted, since that metafunction is gone
130
131  (test-equal (judgment-holds (⇓ (· y ↦ 1) ((λ (x) x) y) Δ v) v)
132                (list (term 1)))
133
134  (test-equal (run (term 1)) 1)
135  (test-equal (run (term (let ([y 1])
136                             (let ([z ((λ (x) x) y)])
137                               2))))
138                2)
139  (test-equal (run (term (let ([y 1]) y))) 1)
140  (test-equal (run (term (let ([y (λ (x) x)]) y))) (term (λ (x1) x1)))
141  (test-equal (run (term (let ([y 1]) ((λ (x) x) y)))) 1)
142  (test-equal (run (term
143                      (let ([app (λ (f) (λ (x) (f x)))]
144                            [f (λ (x) (λ (y) x))]
145                            [o 1])
146                        (((app f) o) f))))
147                1)
148  (test-equal (run (term (if0 0 1 2))) 1)
149  (test-equal (run (term (if0 1 2 3))) 3)
150
151  ;; free variable errors return no derivation
152  (test-equal (run (term (let ([x y]) x))) #f)
153
154  ;; as do runtime errors
155  (test-equal (run (term (let ([two 2]) (1 two)))) #f)
156
157  (test-equal (run
158                 (term
159                  (let ([o 1]
160                        [t 2]
161                        [r 3]
162                        [f 4])
163                    (((((λ (x)
164                           (λ (y)
165                              (λ (z)
166                                 (λ (w)
167                                    (+ (+ x y)
168                                       (+ w z))))))
169                        o)
170                       t)
171                      r)
172                     f))))
173                10)
174
175  (test-equal (run (term
176                      (let ([me (λ (x) x)])
177                        (let ([tri
178                               (λ (x)
179                                  (let ([x1 (+ x -1)])
180                                    (+ (me x1) x)))]
181                              [five 5])
182                          (tri five)))))
183                9)
184
185  (test-equal (run (term (let ([tri
186                                  (λ (x)
187                                     (let ([x1 (+ x -1)])
188                                       x))]
189                                 [five 5])
190                             (tri five))))
191                5)
192
193  (test-equal (run (term
194                      (let ([Y (λ (f)
195                                  (let ([g (λ (x)
196                                              (let ([xx (x x)])
197                                                (f xx)))])
198                                    (g g)))]
199                            [tri
200                             (λ (me)
201                                (λ (x)
202                                   (if0 x
203                                        0
204                                        (let ([x1 (+ x -1)])
205                                          (+ (me x1) x)))))]
206                            [five 5])
207                        ((Y tri) five))))
208                (+ 5 4 3 2 1 0))
209
210
211  (test-equal (run (term (let ([one 1] [two 2])
212                             (((λ (x) (λ (x) (+ x one))) one) two))))
213                3)
214
215  (test-results))
216