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