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