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)))