1#lang racket/base 2 3(require redex/reduction-semantics 4 (only-in redex/private/generate-term pick-an-index) 5 racket/match 6 racket/list 7 racket/contract 8 racket/bool racket/set 9 (only-in redex/examples/stlc-tests-lib consistent-with?)) 10 11(provide (all-defined-out)) 12 13(define-language stlc 14 (M N ::= 15 (λ x M) 16 (M N) 17 x 18 c 19 (let ([x M]) N)) 20 (Γ (x σ Γ) 21 ·) 22 (σ τ ::= 23 int 24 (σ → τ) 25 (list τ) 26 (ref τ) 27 x) 28 (c d ::= c0 c1) 29 (c0 ::= + integer) 30 (c1 ::= cons nil hd tl new get set) 31 (x y r ::= variable-not-otherwise-mentioned) 32 33 (v (λ x M) 34 c 35 ((cons v) v) 36 (cons v) 37 (+ v) 38 (set v) 39 r) 40 (E hole 41 (E M) 42 (v E) 43 (let ([x E]) M)) 44 (Σ ::= · (r v Σ)) 45 46 (κ ::= 47 · 48 (λ τ κ) 49 (1 Γ M κ) 50 (2 τ κ)) 51 52 (G ::= · (τ σ G)) 53 (Gx ::= · (x σ Gx))) 54 55(define v? (redex-match? stlc v)) 56(define τ? (redex-match? stlc τ)) 57(define x? (redex-match? stlc x)) 58(define M? (redex-match? stlc M)) 59(define Σ-M? (redex-match? stlc (Σ M))) 60 61#| 62 63The typing judgment has no rule with multiple 64(self-referential) premises. Instead, it explicitly 65manipulates a continuation so that it can, when it 66discovers a type equality, simply do the substitution 67through the continuation. This also makes it possible 68to easily generate fresh variables by picking ones 69that aren't in the expression or the continuation. 70 71The 'tc-down' rules recur thru the term to find a type 72of the left-most subexpression and the 'tc-up' rules 73bring that type back, recurring on the continuation. 74 75|# 76 77(define-judgment-form stlc 78 #:mode (typeof I O) 79 #:contract (typeof M σ) 80 81 [(tc-down · M · σ) 82 ------------- 83 (typeof M σ)]) 84 85(define-judgment-form stlc 86 #:mode (tc-down I I I O) 87 #:contract (tc-down Γ M κ σ) 88 89 [(tc-up (const-type0 c0) κ σ_ans) 90 -------------------------------- "const0" 91 (tc-down Γ c0 κ σ_ans)] 92 93 [(where x ,(variable-not-in (term (Γ κ)) 'γ)) 94 (tc-up (const-type1 x c1) κ σ_ans) 95 -------------------------------------------- "const1" 96 (tc-down Γ c1 κ σ_ans)] 97 98 [(where τ (lookup-Γ Γ x)) 99 (tc-up τ κ σ_ans) 100 ------------------------ "var" 101 (tc-down Γ x κ σ_ans)] 102 103 [(where y ,(variable-not-in (term (x Γ M κ)) 'α2-)) 104 (tc-down (x y Γ) M (λ y κ) σ_ans) 105 -------------------------------------------------- "λ" 106 (tc-down Γ (λ x M) κ σ_ans)] 107 108 [(tc-down Γ M_1 (1 Γ M_2 κ) σ_2) 109 ------------------------------- "app" 110 (tc-down Γ (M_1 M_2) κ σ_2)] 111 112 [(where N_2 (subst N x v)) 113 (where y ,(variable-not-in (term N_2) 'l)) 114 (tc-down Γ ((λ y N_2) v) κ σ_2) 115 ------------------------------------------ "let poly" 116 (tc-down Γ (let ([x v]) N) κ σ_2)] 117 118 [(where #t (not-v? M)) 119 (tc-down Γ ((λ x N) M) κ σ_2) 120 --------------------------------- "let mono" 121 (tc-down Γ (let ([x M]) N) κ σ_2)]) 122 123(define-judgment-form stlc 124 #:mode (tc-up I I O) 125 #:contract (tc-up τ κ σ) 126 127 [--------------------- "done" 128 (tc-up σ_ans · σ_ans)] 129 130 [(tc-down Γ M (2 τ κ) σ_ans) 131 --------------------------- "app l" 132 (tc-up τ (1 Γ M κ) σ_ans)] 133 134 [(where x ,(variable-not-in (term (τ_1 τ_2 κ)) 'α1-)) 135 (unify τ_2 (τ_1 → x) Gx) 136 (tc-up (apply-subst-τ Gx x) 137 (apply-subst-κ Gx κ) 138 σ_ans) 139 --------------------------------------------------- "app r" 140 (tc-up τ_1 (2 τ_2 κ) σ_ans)] 141 142 [(tc-up (τ_1 → τ_2) κ σ_ans) 143 --------------------------- "λ" 144 (tc-up τ_2 (λ τ_1 κ) σ_ans)]) 145 146(define-metafunction stlc 147 const-type0 : c0 -> σ 148 [(const-type0 +) (int → (int → int))] 149 [(const-type0 integer) int]) 150 151(define-metafunction stlc 152 const-type1 : x c1 -> σ 153 [(const-type1 x nil) (list x)] 154 [(const-type1 x cons) (x → ((list x) → (list x)))] 155 [(const-type1 x hd) ((list x) → x)] 156 [(const-type1 x tl) ((list x) → (list x))] 157 [(const-type1 x new) (x → (ref x))] 158 [(const-type1 x get) ((ref x) → x)] 159 [(const-type1 x set) ((ref x) → (x → x))]) 160 161(define-metafunction stlc 162 lookup-Γ : Γ x -> σ or #f 163 [(lookup-Γ (x σ Γ) x) σ] 164 [(lookup-Γ (x σ Γ) y) (lookup-Γ Γ y)] 165 [(lookup-Γ · x) #f]) 166 167#| 168 169Algorithm copied from Chapter 8 in _Handbook of Automated Reasoning_: 170Unification Theory by Franz Baader and Wayne Synder 171http://www.cs.bu.edu/~snyder/publications/UnifChapter.pdf 172 173The 'uh' judgment form iterates over a set of equations applying the 174rules from the paper, building up the result substitution in Gx. 175 176|# 177 178(define-judgment-form stlc 179 #:mode (unify I I O) 180 181 [(uh (τ σ ·) Gx) 182 ---------------- 183 (unify τ σ Gx)]) 184 185(define-judgment-form stlc 186 #:mode (uh I O) 187 #:contract (uh G Gx) 188 189 [--------- "bottomed out" 190 (uh · ·)] 191 192 [(uh (x int G) Gx) 193 ------------------ "orient int" 194 (uh (int x G) Gx)] 195 196 [(uh (x (σ → τ) G) Gx) 197 ----------------------- "orient →" 198 (uh ((σ → τ) x G) Gx)] 199 200 [(uh (x (list τ) G) Gx) 201 ----------------------- "orient list" 202 (uh ((list τ) x G) Gx)] 203 204 [(uh (x (ref τ) G) Gx) 205 ----------------------- "orient ref" 206 (uh ((ref τ) x G) Gx)] 207 208 [(uh (τ_1 σ_1 (τ_2 σ_2 G)) Gx) 209 ------------------------------------ "decomposition →" 210 (uh ((τ_1 → τ_2) (σ_1 → σ_2) G) Gx)] 211 212 [(uh (τ σ G) Gx) 213 ------------------------------ "decomposition list" 214 (uh ((list τ) (list σ) G) Gx)] 215 216 [(uh (τ σ G) Gx) 217 ---------------------------- "decomposition ref" 218 (uh ((ref τ) (ref σ) G) Gx)] 219 220 [(uh G Gx) 221 -------------------- "decomposition int" 222 (uh (int int G) Gx)] 223 224 [(var-not-in-τ x τ) 225 (uh (eliminate-G x τ G) Gx) 226 (where Gx_eliminated (eliminate-Gx x τ Gx)) 227 (where τ_subst (apply-subst-τ Gx τ)) 228 ---------------------------------------------------- "variable elim" 229 (uh (x τ G) 230 (x τ_subst Gx_eliminated))]) 231 232(define-metafunction stlc 233 eliminate-G : x τ G -> G 234 [(eliminate-G x τ ·) ·] 235 [(eliminate-G x τ (σ_1 σ_2 G)) 236 ((eliminate-τ x τ σ_1) (eliminate-τ x τ σ_2) (eliminate-G x τ G))]) 237 238(define-metafunction stlc 239 eliminate-Gx : x τ Gx -> Gx 240 [(eliminate-Gx x τ ·) ·] 241 [(eliminate-Gx x τ (y σ Gx)) 242 ;; we can just put `y` in the result because the variable elim 243 ;; rule guarantees that `y` is never the same as `x` 244 (y (eliminate-τ x τ σ) (eliminate-Gx x τ Gx))]) 245 246(define-metafunction stlc 247 eliminate-τ : x τ σ -> σ 248 [(eliminate-τ x τ (σ_1 → σ_2)) ((eliminate-τ x τ σ_1) → (eliminate-τ x τ σ_2))] 249 [(eliminate-τ x τ (list σ)) (list (eliminate-τ x τ σ))] 250 [(eliminate-τ x τ (ref σ)) (ref (eliminate-τ x τ σ))] 251 [(eliminate-τ x τ int) int] 252 [(eliminate-τ x τ x) τ] 253 [(eliminate-τ x τ y) y]) 254 255(define-judgment-form stlc 256 #:mode (var-not-in-τ I I) 257 #:contract (var-not-in-τ x τ) 258 [(where #true (different x y)) 259 ----------------------------- 260 (var-not-in-τ x y)] 261 262 [-------------------- 263 (var-not-in-τ x int)] 264 265 [(var-not-in-τ x τ) 266 ------------------------ 267 (var-not-in-τ x (ref τ))] 268 269 [(var-not-in-τ x τ) 270 ------------------------- 271 (var-not-in-τ x (list τ))] 272 273 [(var-not-in-τ x τ) 274 (var-not-in-τ x σ) 275 ------------------------ 276 (var-not-in-τ x (τ → σ))]) 277 278(define-metafunction stlc 279 [(different x x) #false] 280 [(different x y) #true]) 281 282(define-metafunction stlc 283 apply-subst-τ : Gx τ -> τ 284 [(apply-subst-τ · τ) τ] 285 [(apply-subst-τ (x τ G) σ) 286 (apply-subst-τ G (eliminate-τ x τ σ))]) 287 288(define-metafunction stlc 289 apply-subst-κ : Gx κ -> κ 290 [(apply-subst-κ Gx ·) ·] 291 [(apply-subst-κ Gx (λ σ κ)) 292 (λ (apply-subst-τ Gx σ) (apply-subst-κ Gx κ))] 293 [(apply-subst-κ Gx (1 Γ M κ)) 294 (1 (apply-subst-Γ Gx Γ) M (apply-subst-κ Gx κ))] 295 [(apply-subst-κ Gx (2 σ κ)) 296 (2 (apply-subst-τ Gx σ) 297 (apply-subst-κ Gx κ))]) 298 299(define-metafunction stlc 300 apply-subst-Γ : Gx Γ -> Γ 301 [(apply-subst-Γ Gx (y σ Γ)) (y (apply-subst-τ Gx σ) (apply-subst-Γ Gx Γ))] 302 [(apply-subst-Γ Gx ·) ·]) 303 304(define-metafunction stlc 305 not-v? : M -> boolean 306 [(not-v? v) #f] 307 [(not-v? M) #t]) 308 309#| 310 311The reduction relation rewrites a pair of 312a store and an expression to a new store 313and a new expression or into the string 314 "error" (for hd and tl of the empty list) 315 316|# 317 318(define red 319 (reduction-relation 320 stlc 321 (--> (Σ (in-hole E ((λ x M) v))) 322 (Σ (in-hole E (subst M x v))) 323 "βv") 324 (--> (Σ (in-hole E (let ([x v]) M))) 325 (Σ (in-hole E (subst M x v))) 326 "let") 327 (--> (Σ (in-hole E (hd ((cons v_1) v_2)))) 328 (Σ (in-hole E v_1)) 329 "hd") 330 (--> (Σ (in-hole E (tl ((cons v_1) v_2)))) 331 (Σ (in-hole E v_2)) 332 "tl") 333 (--> (Σ (in-hole E (hd nil))) 334 "error" 335 "hd-err") 336 (--> (Σ (in-hole E (tl nil))) 337 "error" 338 "tl-err") 339 (--> (Σ (in-hole E ((+ integer_1) integer_2))) 340 (Σ (in-hole E ,(+ (term integer_1) (term integer_2)))) 341 "+") 342 (--> (Σ (in-hole E (new v))) 343 ((r v Σ) (in-hole E r)) 344 (fresh r) 345 "ref") 346 (--> (Σ (in-hole E ((set x) v))) 347 ((update-Σ Σ x v) (in-hole E (lookup-Σ Σ x))) 348 "set") 349 (--> (Σ (in-hole E (get x))) 350 (Σ (in-hole E (lookup-Σ Σ x))) 351 "get"))) 352 353#| 354 355Capture avoiding substitution 356 357|# 358 359 360(define-metafunction stlc 361 subst : M x M -> M 362 [(subst x x M_x) 363 M_x] 364 [(subst (λ x M) x M_x) 365 (λ x M)] 366 [(subst (let ([x M]) N) x M_x) 367 (let ([x (subst M x M_x)]) N)] 368 [(subst (λ y M) x M_x) 369 (λ x_new (subst (replace M y x_new) x M_x)) 370 (where x_new ,(variable-not-in (term (x y M)) 371 (term y)))] 372 [(subst (let ([y N]) M) x M_x) 373 (let ([x_new (subst N x M_x)]) (subst (replace M y x_new) x M_x)) 374 (where x_new ,(variable-not-in (term (x y M)) 375 (term y)))] 376 [(subst (M N) x M_x) 377 ((subst M x M_x) (subst N x M_x))] 378 [(subst M x M_z) 379 M]) 380 381(define-metafunction stlc 382 [(replace x x x_new) 383 x_new] 384 [(replace (λ x_0 M) x x_new) 385 (λ (replace x_0 x x_new) (replace M x x_new))] 386 [(replace (let ([x_0 M]) N) x x_new) 387 (let ([(replace x_0 x x_new) 388 (replace M x x_new)]) 389 (replace N x x_new))] 390 [(replace (M N) x x_new) 391 ((replace M x x_new) (replace N x x_new))] 392 [(replace M x x_new) 393 M]) 394 395(define-metafunction stlc 396 lookup-Σ : Σ x -> v 397 [(lookup-Σ (x v Σ) x) v] 398 [(lookup-Σ (x v Σ) y) (lookup-Σ Σ y)]) 399 400(define-metafunction stlc 401 update-Σ : Σ x v -> Σ 402 [(update-Σ (x v_1 Σ) x v_2) (x v_2 Σ)] 403 [(update-Σ (x v_1 Σ) y v_2) (x v_1 (update-Σ Σ y v_2))]) 404 405#| 406 407A top-level evaluator 408 409|# 410 411(define/contract (Eval M) 412 (-> M? (or/c "error" 'list 'λ 'ref number?)) 413 (define M-t (type-check M)) 414 (unless M-t 415 (error 'Eval "doesn't typecheck: ~s" M)) 416 (define res (apply-reduction-relation* red (term (· ,M)))) 417 (unless (= 1 (length res)) 418 (error 'Eval "internal error: not exactly 1 result ~s => ~s" M res)) 419 (define ans (car res)) 420 (match (car res) 421 ["error" "error"] 422 [`(,Σ ,N) 423 (define ans-t (type-check N Σ)) 424 (unless (equal? M-t ans-t) 425 (error 'Eval "internal error: type soundness fails for ~s" M)) 426 (match N 427 [(? x?) (cond 428 [(term (in-dom? ,Σ ,N)) 429 'ref] 430 [else 431 (error 'Eval "internal error: reduced to a free variable ~s" 432 M)])] 433 [(or `((cons ,_) ,_) `nil) 'list] 434 [(or `(λ ,_ ,_) `(cons ,_) `(set ,_) `(+ ,_)) 'λ] 435 [(? number?) N] 436 [_ (error 'Eval "internal error: didn't reduce to a value ~s" M)])])) 437 438#| 439 440A type checker; the optional argument is a store to use 441for type checking free variables in M. 442 443|# 444 445(define/contract (type-check M [Σ (term ·)]) 446 (->* (M?) (any/c) (or/c τ? #f)) 447 (define M-ts (judgment-holds (typeof ,(Σ+M->M Σ M) τ) τ)) 448 (cond 449 [(null? M-ts) 450 #f] 451 [(null? (cdr M-ts)) 452 (car M-ts)] 453 [else 454 (error 'type-check "non-unique type: ~s : ~s" M M-ts)])) 455 456;; building an expression out of a store can be done in this model 457;; with just topological sort because there are no recursive types, 458;; so the store will not contain any cycles 459(define (Σ+M->M Σ M) 460 ;; nodes : edges[r -o> v] 461 (define nodes (make-hash)) 462 (define edges (make-hash)) 463 (let loop ([Σ Σ]) 464 (match Σ 465 [`· (void)] 466 [`(,r ,v ,Σ) 467 (hash-set! nodes r v) 468 (loop Σ)])) 469 470 (for ([(n rhs) (in-hash nodes)]) (hash-set! edges n (set))) 471 (for ([(n-src rhs) (in-hash nodes)]) 472 (for ([(n-dest _) (in-hash nodes)]) 473 (when (mentions-node? n-dest rhs) 474 (hash-set! edges n-src (set-add (hash-ref edges n-src) n-dest))))) 475 (define rev-sorted (reverse-topo-sort (for/list ([(k v) (in-hash nodes)]) k) 476 edges)) 477 (let loop ([sorted rev-sorted]) 478 (cond 479 [(empty? sorted) M] 480 [else 481 (define r (car sorted)) 482 (term (let ([,r (new ,(hash-ref nodes r))]) 483 ,(loop (cdr sorted))))]))) 484 485(define (mentions-node? v r) 486 (let loop ([v v]) 487 (cond 488 [(symbol? v) (equal? r v)] 489 [(pair? v) (or (loop (car v)) (loop (cdr v)))] 490 [else #f]))) 491 492#| 493 494The first algorithm from this page: 495http://en.wikipedia.org/wiki/Topological_sorting#Algorithms 496 497|# 498(define/contract (reverse-topo-sort nodes edges) 499 (-> (listof any/c) (hash/c any/c (set/c any/c)) (listof any/c)) 500 501 (for ([node (in-list nodes)]) 502 (unless (hash-ref edges node #f) 503 (error 'topo-sort "no edge entry for ~s" node))) 504 505 (define incoming-counts (build-incoming-counts nodes edges)) 506 (define (remove-edge src dest) 507 (hash-set! edges src (set-remove (hash-ref edges src) dest)) 508 (hash-set! incoming-counts dest (- (hash-ref incoming-counts dest) 1))) 509 510 (define l '()) 511 (define s (for/set ([(n c) (in-hash incoming-counts)] 512 #:when (zero? c)) 513 n)) 514 (let loop () 515 (unless (set-empty? s) 516 (define n (set-first s)) 517 (set! s (set-remove s n)) 518 (set! l (cons n l)) 519 (for ([m (in-set (hash-ref edges n))]) 520 (remove-edge n m) 521 (when (zero? (hash-ref incoming-counts m)) 522 (set! s (set-add s m)))) 523 (loop))) 524 525 l) 526 527(define (build-incoming-counts nodes edges) 528 (define incoming-counts (make-hash)) 529 (for ([n (in-list nodes)]) (hash-set! incoming-counts n 0)) 530 (for ([(n neighbors) (in-hash edges)]) 531 (for ([neighbor (in-set neighbors)]) 532 (hash-set! incoming-counts neighbor (+ (hash-ref incoming-counts neighbor) 1)))) 533 incoming-counts) 534 535(module+ test 536 537 (test-equal (build-incoming-counts '(x y z) 538 (make-hash (list (cons 'x (set 'y 'z)) 539 (cons 'y (set 'z)) 540 (cons 'z (set))))) 541 (make-hash (list (cons 'x 0) 542 (cons 'y 1) 543 (cons 'z 2)))) 544 (test-equal (reverse-topo-sort '() (make-hash)) '()) 545 (test-equal (reverse-topo-sort '(x) 546 (make-hash (list (cons 'x (set))))) 547 '(x)) 548 (test-equal (reverse-topo-sort '(x y) 549 (make-hash (list (cons 'y (set)) 550 (cons 'x (set 'y))))) 551 '(y x)) 552 (test-equal (reverse-topo-sort '(y x) 553 (make-hash (list (cons 'y (set)) 554 (cons 'x (set 'y))))) 555 '(y x)) 556 (test-equal (reverse-topo-sort '(x y z) 557 (make-hash (list (cons 'x (set 'y)) 558 (cons 'y (set 'z)) 559 (cons 'z (set))))) 560 '(z y x)) 561 (test-equal (reverse-topo-sort '(x y z) 562 (make-hash (list (cons 'x (set 'y 'z)) 563 (cons 'y (set 'z)) 564 (cons 'z (set))))) 565 '(z y x)) 566 (define (one-of? a . bs) (for/or ([b (in-list bs)]) (equal? a b))) 567 (test-equal (one-of? (reverse-topo-sort '(x y z) 568 (make-hash (list (cons 'x (set 'z)) 569 (cons 'y (set 'z)) 570 (cons 'z (set))))) 571 '(z x y) 572 '(z y x)) 573 #t) 574 575 (test-equal (Σ+M->M (term (r1 r2 (r2 1 ·))) (term 2)) 576 (term (let ([r2 (new 1)]) (let ([r1 (new r2)]) 2)))) 577 (test-equal (Σ+M->M (term (r2 1 (r1 r2 ·))) (term 2)) 578 (term (let ([r2 (new 1)]) (let ([r1 (new r2)]) 2)))) 579 580 (test-equal (term (subst ((+ 1) 1) x 2)) 581 (term ((+ 1) 1))) 582 (test-equal (term (subst ((+ x) x) x 2)) 583 (term ((+ 2) 2))) 584 (test-equal (term (subst ((+ y) x) x 2)) 585 (term ((+ y) 2))) 586 (test-equal (term (subst ((+ y) z) x 2)) 587 (term ((+ y) z))) 588 (test-equal (term (subst ((λ x x) x) x 2)) 589 (term ((λ x x) 2))) 590 (test-equal (consistent-with? (term (subst ((λ y x) x) x 2)) 591 (term ((λ y 2) 2))) 592 #t) 593 (test-equal (consistent-with? (term (subst ((λ y x) x) x (λ q z))) 594 (term ((λ y (λ q z)) (λ q z)))) 595 #t) 596 (test-equal (consistent-with? (term (subst ((λ y x) x) x (λ q y))) 597 (term ((λ y2 (λ q y)) (λ q y)))) 598 #t) 599 (test-equal (consistent-with? (term (subst (λ z (λ z1 z)) q 1)) 600 (term (λ z (λ z1 z)))) 601 #t) 602 603 (test-equal (consistent-with? (term (subst (let ([y x]) x) x 2)) 604 (term (let ([y 2]) 2))) 605 #t) 606 (test-equal (consistent-with? (term (subst (let ([y x]) x) x (λ q z))) 607 (term (let ([y (λ q z)]) (λ q z)))) 608 #t) 609 (test-equal (consistent-with? (term (subst (let ([y x]) x) x (λ q y))) 610 (term (let ([y (λ q y)]) (λ q y)))) 611 #t) 612 (test-equal (consistent-with? (term (subst (let ([z 11]) (let ([z1 12]) z)) q 1)) 613 (term (let ([z 11]) (let ([z1 12]) z)))) 614 #t) 615 (test-equal (consistent-with? (term (subst (let ((|| +)) ||) |1| (λ x1 x1))) 616 (term (let ((|| +)) ||))) 617 #t) 618 619 (test-judgment-holds (unify x int (x int ·))) 620 (test-judgment-holds (unify int x (x int ·))) 621 (test-equal (judgment-holds (unify int (list int) Gx)) #f) 622 (test-judgment-holds (unify int int ·)) 623 (test-judgment-holds (unify (list int) (list int) ·)) 624 (test-judgment-holds (unify (int → x) 625 (y → (list int)) 626 (y int (x (list int) ·)))) 627 (test-equal (judgment-holds (unify (int → x) (x → (list int)) Gx)) #f) 628 (test-equal (judgment-holds (unify (x → (y → x)) 629 (int → ((list int) → y)) 630 Gx)) 631 #f) 632 (test-judgment-holds (unify (x → (y → x)) 633 (int → ((list int) → z)) 634 (x int (y (list int) (z int ·))))) 635 (test-judgment-holds (unify (x → (y → z)) 636 (int → ((list int) → x)) 637 (x int (y (list int) (z int ·))))) 638 (test-judgment-holds (unify (x → (y → z)) 639 (y → (z → int)) 640 (x int (y int (z int ·))))) 641 (test-equal (judgment-holds (unify x (x → y) Gx)) #f) 642 643 (test-equal (judgment-holds (typeof 5 τ) τ) 644 (list (term int))) 645 (test-equal (judgment-holds (typeof nil τ) τ) 646 (list (term (list γ)))) 647 (test-equal (judgment-holds (typeof (cons 1) τ) τ) 648 (list (term ((list int) → (list int))))) 649 (test-equal (judgment-holds (typeof ((cons 1) nil) τ) τ) 650 (list (term (list int)))) 651 (test-equal (consistent-with? (judgment-holds (typeof (λ x x) τ) τ) 652 (list (term (α → α)))) 653 #t) 654 (test-equal (consistent-with? (judgment-holds (typeof (λ x (λ y x)) τ) τ) 655 (list (term (α → (α1 → α))))) 656 #t) 657 (test-equal (consistent-with? (judgment-holds (typeof (λ f (λ x (f ((+ x) 1)))) τ) τ) 658 (list (term ((int → α) → (int → α))))) 659 #t) 660 (test-equal (judgment-holds (typeof (λ f (λ x ((+ (f ((+ x) 1))) 2))) τ) τ) 661 (list (term ((int → int) → (int → int))))) 662 (test-equal (judgment-holds (typeof (λ f (λ x ((+ x) (f 1)))) τ) τ) 663 (list (term ((int → int) → (int → int))))) 664 (test-equal (judgment-holds (typeof (λ x (x x)) τ) τ) 665 (list)) 666 (test-equal (judgment-holds (typeof ((+ ((+ 1) 2)) ((+ 3) 4)) τ) τ) 667 (list (term int))) 668 (test-equal (judgment-holds (typeof ((cons ((cons 1) nil)) nil) τ) τ) 669 (list (term (list (list int))))) 670 (test-equal (judgment-holds (typeof ((cons nil) nil) τ) τ) 671 (list (term (list (list γ1))))) 672 (test-equal (judgment-holds (typeof ((set (new 1)) 2) τ) τ) 673 (list (term int))) 674 (test-equal (judgment-holds (typeof (get (new 1)) τ) τ) 675 (list (term int))) 676 (test-equal (judgment-holds (typeof (let ([id (λ y y)]) 677 ((id id) 1)) 678 τ) 679 τ) 680 (list (term int))) 681 (test-equal (judgment-holds (typeof (let ([r (new nil)]) 682 (let ([n ((set r) ((cons 5) nil))]) 683 ((hd (get r)) 1))) 684 τ) 685 τ) 686 (list)) 687 688 (test-->> red (term (· ((λ x x) 7))) (term (· 7))) 689 (test-->> red (term (· (((λ x (λ x x)) 2) 1))) (term (· 1))) 690 (test-->> red (term (· (((λ x (λ y x)) 2) 1))) (term (· 2))) 691 (test-->> red 692 (term (· ((λ x ((cons x) nil)) 11))) 693 (term (· ((cons 11) nil)))) 694 (test-->> red 695 (term (· ((λ x ((cons x) nil)) 11))) 696 (term (· ((cons 11) nil)))) 697 (test-->> red 698 (term (· ((cons ((λ x x) 11)) nil))) 699 (term (· ((cons 11) nil)))) 700 (test-->> red 701 (term (· (cons ((λ x x) 1)))) 702 (term (· (cons 1)))) 703 (test-->> red 704 (term (· ((cons ((λ x x) 1)) nil))) 705 (term (· ((cons 1) nil)))) 706 (test-->> red 707 (term (· (hd ((λ x ((cons x) nil)) 11)))) 708 (term (· 11))) 709 (test-->> red 710 (term (· (tl ((λ x ((cons x) nil)) 11)))) 711 (term (· nil))) 712 (test-->> red 713 (term (· (tl nil))) 714 "error") 715 (test-->> red 716 (term (· (hd nil))) 717 "error") 718 (test-->> red 719 (term (· ((+ 1) (hd nil)))) 720 "error") 721 (test-->> red 722 (term (· ((+ ((+ 1) 2)) ((+ 3) 4)))) 723 (term (· 10))) 724 (test-->> red 725 (term (· ((λ f (f 3)) (cons 1)))) 726 (term (· ((cons 1) 3)))) 727 (test-->> red 728 (term (· ((λ f (f 3)) (+ 1)))) 729 (term (· 4))) 730 (test-->> red 731 (term (· (let ([f (+ 2)]) ((+ (f 3)) (f 4))))) 732 (term (· 11))) 733 (test-->> red 734 (term (· (get (new 1)))) 735 (term ((r 1 ·) 1))) 736 (test-->> red 737 (term (· ((set (new 1)) 2))) 738 (term ((r 2 ·) 1))) 739 (test-->> red 740 #:equiv consistent-with? 741 (term (· (let ([r (new 1)]) 742 (let ([o ((set r) 2)]) 743 (get r))))) 744 (term ((r 2 ·) 2))) 745 (test-->> red 746 #:equiv consistent-with? 747 (term (· (let ([r (new nil)]) 748 (let ([n ((set r) ((cons 5) nil))]) 749 ((hd (get r)) 1))))) 750 (term ((r ((cons 5) nil) ·) (5 1)))) 751 752 (test-equal (Eval (term ((λ x x) 3))) 753 3) 754 (test-equal (Eval (term ((cons 1) nil))) 755 'list) 756 (test-equal (Eval (term (cons 1))) 757 'λ) 758 (test-equal (Eval (term (λ x x))) 759 'λ) 760 (test-equal (type-check (term 5)) 761 (term int)) 762 (test-equal (type-check (term (5 5))) 763 #f) 764 (test-equal (type-check (term r1) (term (r1 r (r 1 ·)))) 765 (term (ref (ref int)))) 766 (test-equal (type-check (term r1) (term (r 1 (r1 r ·)))) 767 (term (ref (ref int))))) 768