1#lang racket
2(require redex)
3
4#|
5
6A model of Racket's letrec
7
8|#
9
10(provide lang
11         surface-lang
12         result-and-output-of
13         result-of
14         run)
15
16(define-language surface-lang
17  (e (set! x e)
18     (let ((x_!_ e) ...) e)
19     (letrec ((x_!_ e) ...) e)
20     (if e e e)
21     (begin e e ...)
22     (e e ...)
23     (writeln e)
24     x
25     v)
26  (v fv sv)
27  (fv (λ (x_!_ ...) e) + - * =)
28  (sv number
29      (void)
30      #t
31      #f)
32  (x variable-not-otherwise-mentioned)
33
34  #:binding-forms
35  (λ (x ...) e #:refers-to (shadow x ...))
36  (let ([x e_x] ...) e_body #:refers-to (shadow x ...))
37  (letrec ([x e_x] ...) #:refers-to (shadow x ...) e_body #:refers-to (shadow x ...)))
38
39(define-extended-language lang surface-lang
40  (p ((store (x_!_ v-or-undefined) ...)
41      (output o ...)
42      e))
43  (e ::= ....
44     undefined
45     (lset! x e))
46  (o ::= procedure sv)
47  (P ((store (x v-or-undefined) ...) (output o ...) E))
48  (E (v ... E e ...)
49     (set! x E)
50     (lset! x E)
51     (let ((x v-or-undefined) ... (x E) (x e) ...) e)
52     (if E e e)
53     (begin E e e ...)
54     (writeln E)
55     hole)
56  (v-or-undefined v undefined))
57
58(define v? (redex-match? lang v))
59
60;; collect : term -> term
61;; performs a garbage collection on the term `p'
62(define (collect p)
63  (match p
64    [`((store (,vars ,vs) ...) ,o ,e)
65
66     (define (unused-var? var)
67       (and (not (in? var e))
68            (andmap (λ (rhs) (not (in? var rhs)))
69                    vs)))
70
71     (define unused
72       (for/list ([var (in-list vars)]
73                  #:when (unused-var? var))
74         var))
75
76     (cond
77       [(null? unused) p]
78       [else
79        (collect
80         (term ((store ,@(filter (λ (binding) (not (memq (car binding) unused)))
81                                 (cdar p)))
82                ,o
83                ,e)))])]))
84
85(define (in? var body)
86  (let loop ([body body])
87    (match body
88      [(cons a b) (or (loop a) (loop b))]
89      [(? symbol?) (equal? body var)]
90      [else #f])))
91
92(module+ test
93  (test-equal (collect (term ((store) (output) 1))) (term ((store) (output) 1)))
94  (test-equal (collect (term ((store (x 1)) (output) 1))) (term ((store) (output) 1)))
95  (test-equal (collect (term ((store (x 1)) (output) x))) (term ((store (x 1)) (output) x)))
96  (test-equal (collect (term ((store (x 1) (y x)) (output) 1))) (term ((store) (output) 1)))
97  (test-equal (collect (term ((store (x 1) (y x)) (output) y)))
98              (term ((store (x 1) (y x)) (output) y)))
99  ;; doesn't really do actually gc, so improving the collect
100  ;; function might break this test (which would be great)
101  (test-equal (collect (term ((store (x y) (y x)) (output) 1)))
102              (term ((store (x y) (y x)) (output) 1))))
103
104(define reductions
105  (reduction-relation
106   lang #:domain p
107   (==> (in-hole P_1 (begin v e_1 e_2 ...))
108        (in-hole P_1 (begin e_1 e_2 ...))
109        "begin many")
110
111   (==> (in-hole P_1 (begin e_1))
112        (in-hole P_1 e_1)
113        "begin one")
114
115   (==> ((store (x_before v-or-undefined_before) ...
116                (x_i v_i)
117                (x_after v-or-undefined_after) ...)
118         (output o ...)
119         (in-hole E_1 x_i))
120        ((store (x_before v-or-undefined_before) ...
121                (x_i v_i)
122                (x_after v-or-undefined_after) ...)
123         (output o ...)
124         (in-hole E_1 v_i))
125        "get")
126
127   (==> ((store (x_before v-or-undefined_before) ...
128                (x_i v_old)
129                (x_after v-or-undefined_after) ...)
130         (output o ...)
131         (in-hole E (set! x_i v_new)))
132        ((store (x_before v-or-undefined_before) ...
133                (x_i v_new)
134                (x_after v-or-undefined_after) ...)
135         (output o ...)
136         (in-hole E (void)))
137        "set!")
138   (==> ((store (x_before v-or-undefined_before) ...
139                (x_i v-or-undefined)
140                (x_after v-or-undefined_after) ...)
141         (output o ...)
142         (in-hole E (lset! x_i v_new)))
143        ((store (x_before v-or-undefined_before) ...
144                (x_i v_new)
145                (x_after v-or-undefined_after) ...)
146         (output o ...)
147         (in-hole E (void)))
148        "lset!")
149
150   (==> (in-hole P ((λ (x ..._1) e) v ..._1))
151        (in-hole P (let ([x v] ...) e))
152        "βv")
153
154   (==> (in-hole P (= number_1 number_2 ...))
155        (in-hole P ,(apply = (term (number_1 number_2 ...))))
156        "=")
157   (==> (in-hole P (- number_1 number_2 ...))
158        (in-hole P ,(apply - (term (number_1 number_2 ...))))
159        "-")
160   (==> (in-hole P (+ number ...))
161        (in-hole P ,(apply + (term (number ...))))
162        "+")
163   (==> (in-hole P (* number ...))
164        (in-hole P ,(apply * (term (number ...))))
165        "*")
166   (==> (in-hole P (zero? number))
167        (in-hole P (δ zero? number))
168        "zero")
169
170   (==> (in-hole P (if #f e_then e_else))
171        (in-hole P e_else)
172        "iff")
173   (==> (in-hole P (if v e_then e_else))
174        (in-hole P e_then)
175        (side-condition (not (equal? (term v) #f)))
176        "ift")
177
178   (==> ((store (x_old v-or-undefined_old) ...)
179         (output o ...)
180         (in-hole E (let ([x_1 v-or-undefined_1] [x_2 v-or-undefined_2] ...) e)))
181        ((store (x_old v-or-undefined_old) ... (x_new v-or-undefined_1))
182         (output o ...)
183         (in-hole E (let ([x_2 v-or-undefined_2] ...) (substitute e x_1 x_new))))
184        (fresh x_new)
185        "let1")
186   (==> (in-hole P (let () e))
187        (in-hole P e)
188        "let0")
189
190   (==> (in-hole P (letrec ((x e_1) ...) e_2))
191        (in-hole P (let ((x undefined) ...) (begin (lset! x e_1) ... e_2)))
192        "letrec")
193
194   (==> ((store (x v-or-undefined) ...)
195         (output o ...)
196         (in-hole E (writeln sv)))
197        ((store (x v-or-undefined) ...)
198         (output o ... sv)
199         (in-hole E (void)))
200        "write flat")
201   (==> ((store (x v-or-undefined) ...)
202         (output o ...)
203         (in-hole E (writeln fv)))
204        ((store (x v-or-undefined) ...)
205         (output o ... procedure)
206         (in-hole E (void)))
207        "write proc")
208
209   with
210   [(--> a ,(collect (term b))) (==> a b)]))
211
212(define (run e) (traces reductions (term ((store) (output) ,e))))
213
214(define (result-of prog #:steps [steps #f])
215  (define-values (result io) (result-and-output-of prog #:steps steps))
216  result)
217
218(define (io-of prog #:steps [steps #f])
219  (define-values (result io) (result-and-output-of prog #:steps steps))
220  io)
221
222(define (result-and-output-of e #:steps [steps #f])
223  (define cache (make-immutable-binding-hash lang))
224  (let loop ([prog (term ((store) (output) ,e))]
225             [steps-so-far 0])
226    (define cycle? (dict-ref cache prog #f))
227    (set! cache (dict-set cache prog #t))
228    (cond
229      [cycle?
230       (values 'infinite-loop '())]
231      [(or (not steps) (< steps-so-far steps))
232       (define nexts (apply-reduction-relation reductions prog))
233       (cond
234         [(null? nexts)
235          (match prog
236            [`((store . ,_) (output ,o ...) ,res)
237             (values res o)])]
238         [(null? (cdr nexts))
239          (loop (car nexts) (+ steps-so-far 1))]
240         [else
241          (error 'result-and-output-of
242                 (string-append
243                  "term reduced to multiple things\n"
244                  "  e: ~s\n"
245                  "  reduced to: ~s\n"
246                  "  which reduced to multiple things\n"
247                  "  ~s")
248                 e
249                 prog
250                 nexts)])]
251      [else (values 'ran-out-of-steps '())])))
252
253(module+ test
254  (test-equal
255   (result-of (term (let ((x 5))
256                      (begin
257                        (set! x 6)
258                        x))))
259   6)
260
261  (test-equal
262   (result-of
263    (term (letrec ((f (λ (x) (begin (set! f x) f))))
264            (begin (f 8)
265                   f))))
266   8)
267
268  (test-equal (result-of (term (+ 1 2 3 4))) 10)
269  (test-equal (result-of (term (- 1 2 3 4))) -8)
270  (test-equal (result-of (term (* 1 2 3 4))) 24)
271  (test-equal (result-of (term (= 1))) #t)
272  (test-equal (result-of (term (if (= 0 0) 1 2))) 1)
273  (test-equal (result-of (term (if (= 0 2) 1 2))) 2)
274  (test-equal (result-of (term (letrec ([x 1][y 2]) (+ x y)))) 3)
275  (test-equal (result-of (term (letrec ([x 1][y x][z 3]) y))) 1)
276
277  (test-equal (io-of (term (writeln (+ 1 2)))) (list 3))
278  (test-equal (io-of (term (writeln (writeln (+ 1 2))))) (term (3 (void))))
279
280  ;; test it gets stuck
281  (test-equal (redex-match lang
282                           v
283                           (result-of (term (letrec ((B (set! B #t))) 1))))
284              #f)
285
286  (test-equal
287   (result-of
288    (term (let ((x 9999))
289            (let ((x 5))
290              (let ((double (λ (x) (let ((xx x))
291                                     (begin (set! xx (+ xx xx)) xx)))))
292                (+ (double x)
293                   (+ (double (double x))
294                      x)
295                   (double x)))))))
296   45)
297
298  (test-equal
299   (result-of
300    (term (letrec ((fact
301                    (λ (x)
302                      (if (= x 0)
303                          1
304                          (* x (fact (- x 1)))))))
305            (fact 5))))
306   120)
307
308  (test-equal
309   (result-of
310    (term (let ((even? 0))
311            (let ((odd? 0))
312              (begin
313                (set! even?
314                      (λ (x)
315                        (if (= x 0)
316                            1
317                            (odd? (- x 1)))))
318                (set! odd?
319                      (λ (x)
320                        (if (= x 0)
321                            0
322                            (even? (- x 1)))))
323                (+ (+ (odd? 1)
324                      (* (odd? 2) 10))
325                   (* (odd? 3) 100)))))))
326   101)
327
328  (test-equal
329   (result-of
330    (term (let ([n 5]
331                [acc 1])
332            (letrec ([imperative-fact
333                      (λ ()
334                        (if (= n 0)
335                            acc
336                            (begin
337                              (set! acc (* acc n))
338                              (set! n (- n 1))
339                              (imperative-fact))))])
340              (imperative-fact)))))
341   120)
342
343  (test-equal
344   (result-of
345    (term (letrec ([loop (λ () (loop))])
346            (loop))))
347   'infinite-loop)
348
349  (test-equal
350   (result-of
351    (term (+ 1 (+ 1 (+ 1 (+ 1 (+ 1 (+ 1 2)))))))
352    #:steps 2)
353   'ran-out-of-steps))
354