1#lang racket/base
2(require redex/reduction-semantics)
3(provide stlc-tests
4         consistent-with?)
5
6(define (consistent-with? t1 t2)
7  (define table (make-hash))
8  (let loop ([t1 t1]
9             [t2 t2])
10    (cond
11      [(and (pair? t1) (pair? t2))
12       (and (loop (car t1) (car t2))
13            (loop (cdr t1) (cdr t2)))]
14      [(and (symbol? t1)
15            (symbol? t2)
16            (not (equal? t1 t2))
17            (same-first-char-or-empty-and-numbers? t1 t2))
18       (cond
19         [(equal? t1 t2) #t]
20         [else
21          (define bound (hash-ref table t1 #f))
22          (cond
23            [bound (equal? bound t2)]
24            [else
25             (hash-set! table t1 t2)
26             #t])])]
27      [else (equal? t1 t2)])))
28
29(define (same-first-char-or-empty-and-numbers? t1 t2)
30  (define (first-char s) (string-ref (symbol->string s) 0))
31  (cond
32    [(equal? t1 '||)
33     (regexp-match #rx"[^[0-9]*$" (symbol->string t2))]
34    [(equal? t2 '||)
35     (regexp-match #rx"[^[0-9]*$" (symbol->string t1))]
36    [else
37     (equal? (first-char t1)
38             (first-char t2))]))
39
40(define-syntax-rule
41  (stlc-tests uses-bound-var?
42              typeof
43              red
44              reduction-step-count
45              Eval
46              subst)
47  (begin
48
49    (test-equal (term (uses-bound-var? () 5))
50                #f)
51    (test-equal (term (uses-bound-var? () nil))
52                #f)
53    (test-equal (term (uses-bound-var? () (λ (x int) x)))
54                #t)
55    (test-equal (term (uses-bound-var? () (λ (x int) y)))
56                #f)
57    (test-equal (term (uses-bound-var? () ((λ (x int) x) 5)))
58                #t)
59    (test-equal (term (uses-bound-var? () ((λ (x int) xy) 5)))
60                #f)
61
62    (test-equal (consistent-with? '(λ (z1 int) (λ (z2 int) z2))
63                                  '(λ (z int) (λ (z1 int) z)))
64                #f)
65    (test-equal (consistent-with? '(λ (z1 int) (λ (z2 int) z2))
66                                  '(λ (z int) (λ (z1 int) z1)))
67                #t)
68
69    (test-equal (term (subst ((+ 1) 1) x 2))
70                (term ((+ 1) 1)))
71    (test-equal (term (subst ((+ x) x) x 2))
72                (term ((+ 2) 2)))
73    (test-equal (term (subst ((+ y) x) x 2))
74                (term ((+ y) 2)))
75    (test-equal (term (subst ((+ y) z) x 2))
76                (term ((+ y) z)))
77    (test-equal (term (subst ((λ (x int) x) x) x 2))
78                (term ((λ (x int) x) 2)))
79    (test-equal (consistent-with? (term (subst ((λ (y int) x) x) x 2))
80                                  (term ((λ (y int) 2) 2)))
81                #t)
82    (test-equal (consistent-with? (term (subst ((λ (y int) x) x) x (λ (q int) z)))
83                                  (term ((λ (y int) (λ (q int) z)) (λ (q int) z))))
84                #t)
85    (test-equal (consistent-with? (term (subst ((λ (y int) x) x) x (λ (q int) y)))
86                                  (term ((λ (y2 int) (λ (q int) y)) (λ (q int) y))))
87                #t)
88    (test-equal (consistent-with? (term (subst (λ (z int) (λ (z1 int) z)) q 1))
89                                  (term (λ (z int) (λ (z1 int) z))))
90                #t)
91
92    (test-equal (judgment-holds (typeof • 5 τ) τ)
93                (list (term int)))
94    (test-equal (judgment-holds (typeof • nil τ) τ)
95                (list (term (list int))))
96    (test-equal (judgment-holds (typeof • (cons 1) τ) τ)
97                (list (term ((list int) → (list int)))))
98    (test-equal (judgment-holds (typeof • ((cons 1) nil) τ) τ)
99                (list (term (list int))))
100    (test-equal (judgment-holds (typeof • (λ (x int) x) τ) τ)
101                (list (term (int → int))))
102    (test-equal (judgment-holds (typeof • (λ (x (int → int)) (λ (y int) x)) τ) τ)
103                (list (term ((int → int) → (int → (int → int))))))
104    (test-equal (judgment-holds (typeof • ((+ ((+ 1) 2)) ((+ 3) 4)) τ) τ)
105                (list (term int)))
106
107    (test-->> red (term ((λ (x int) x) 7)) (term 7))
108    (test-->> red (term (((λ (x int) (λ (x int) x)) 2) 1)) (term 1))
109    (test-->> red (term (((λ (x int) (λ (y int) x)) 2) 1)) (term 2))
110    (test-->> red
111              (term ((λ (x int) ((cons x) nil)) 11))
112              (term ((cons 11) nil)))
113    (test-->> red
114              (term ((λ (x int) ((cons x) nil)) 11))
115              (term ((cons 11) nil)))
116    (test-->> red
117              (term ((cons ((λ (x int) x) 11)) nil))
118              (term ((cons 11) nil)))
119    (test-->> red
120              (term (cons ((λ (x int) x) 1)))
121              (term (cons 1)))
122    (test-->> red
123              (term ((cons ((λ (x int) x) 1)) nil))
124              (term ((cons 1) nil)))
125    (test-->> red
126              (term (hd ((λ (x int) ((cons x) nil)) 11)))
127              (term 11))
128    (test-->> red
129              (term (tl ((λ (x int) ((cons x) nil)) 11)))
130              (term nil))
131    (test-->> red
132              (term (tl nil))
133              "error")
134    (test-->> red
135              (term (hd nil))
136              "error")
137    (test-->> red
138              (term ((+ 1) (hd nil)))
139              "error")
140    (test-->> red
141              (term ((+ ((+ 1) 2)) ((+ 3) 4)))
142              (term 10))
143    (test-->> red
144              (term ((λ (f (int → (list int))) (f 3)) (cons 1)))
145              (term ((cons 1) 3)))
146    (test-->> red
147              (term ((λ (f (int → int)) (f 3)) (+ 1)))
148              (term 4))
149
150    (test-equal (Eval (term ((λ (x int) x) 3)))
151                (term 3))
152
153    (test-equal (reduction-step-count (term (λ (x int) x)))
154                0)
155    (test-equal (reduction-step-count (term ((λ (x int) x) 1)))
156                1)
157    (test-equal (reduction-step-count (term ((λ (x int) x) 1)))
158                1)
159    (test-equal (reduction-step-count (term ((cons 1) nil)))
160                0)
161    (test-equal (reduction-step-count (term (hd ((cons 1) nil))))
162                1)
163    (test-equal (reduction-step-count (term (hd nil)))
164                1)
165    (test-equal (reduction-step-count (term ((λ (x int) x) (hd ((cons 1) nil)))))
166                2)
167
168    (test-results)))