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) 9 10(provide (all-defined-out)) 11 12(define-language stlc 13 (M N ::= 14 (λ (x σ) M) 15 (M N) 16 x 17 c) 18 (Γ (x σ Γ) 19 •) 20 (σ τ ::= 21 int 22 (list int) 23 (σ → τ)) 24 (c d ::= cons nil hd tl + integer) 25 ((x y) variable-not-otherwise-mentioned) 26 27 (v (λ (x τ) M) 28 c 29 (cons v) 30 ((cons v) v) 31 (+ v)) 32 (E hole 33 (E M) 34 (v E))) 35 36(define-judgment-form stlc 37 #:mode (typeof I I O) 38 #:contract (typeof Γ M σ) 39 40 [--------------------------- 41 (typeof Γ c (const-type c))] 42 43 [(where τ (lookup Γ x)) 44 ---------------------- 45 (typeof Γ x τ)] 46 47 [(typeof (x σ Γ) M σ_2) 48 -------------------------------- 49 (typeof Γ (λ (x σ) M) (σ → σ_2))] 50 51 [(typeof Γ M (σ → σ_2)) 52 (typeof Γ M_2 σ) 53 ---------------------- 54 (typeof Γ (M M_2) σ_2)]) 55 56(define-metafunction stlc 57 const-type : c -> σ 58 [(const-type nil) 59 (list int)] 60 [(const-type cons) 61 (int → ((list int) → (list int)))] 62 [(const-type hd) 63 ((list int) → int)] 64 [(const-type tl) 65 ((list int) → (list int))] 66 [(const-type +) 67 (int → (int → int))] 68 [(const-type integer) 69 int]) 70 71(define-metafunction stlc 72 lookup : Γ x -> σ or #f 73 [(lookup (x σ Γ) x) 74 σ] 75 [(lookup (x σ Γ) x_2) 76 (lookup Γ x_2)] 77 [(lookup • x) 78 #f]) 79 80(define red 81 (reduction-relation 82 stlc 83 (--> (in-hole E ((λ (x τ) M) v)) 84 (in-hole E (subst M x v)) 85 "βv") 86 (--> (in-hole E (hd ((cons v_1) v_2))) 87 (in-hole E v_1) 88 "hd") 89 (--> (in-hole E (tl ((cons v_1) v_2))) 90 (in-hole E v_2) 91 "tl") 92 (--> (in-hole E (hd nil)) 93 "error" 94 "hd-err") 95 (--> (in-hole E (tl nil)) 96 "error" 97 "tl-err") 98 (--> (in-hole E ((+ integer_1) integer_2)) 99 (in-hole E ,(+ (term integer_1) (term integer_2))) 100 "+"))) 101 102(define-metafunction stlc 103 subst : M x M -> M 104 [(subst x x M_x) 105 M_x] 106 [(subst (λ (x τ) M) x M_x) 107 (λ (x τ) M)] 108 [(subst (λ (y τ) M) x M_x) 109 (λ (x_new τ) (subst (replace M y x_new) x M_x)) 110 (where x_new ,(variable-not-in (term (x y M)) 111 (term y)))] 112 [(subst (M N) x M_x) 113 ((subst M x M_x) (subst N x M_x))] 114 [(subst M x M_z) 115 M]) 116 117(define-metafunction stlc 118 [(replace (any_1 ...) x_1 x_new) 119 ((replace any_1 x_1 x_new) ...)] 120 [(replace x_1 x_1 x_new) 121 x_new] 122 [(replace any_1 x_1 x_new) 123 any_1]) 124 125(define M? (redex-match stlc M)) 126(define/contract (Eval M) 127 (-> M? (or/c M? string? 'error)) 128 (define M-t (judgment-holds (typeof • ,M τ) τ)) 129 (cond 130 [(pair? M-t) 131 (define res (apply-reduction-relation* red M)) 132 (cond 133 [(= 1 (length res)) 134 (define ans (car res)) 135 (if (equal? "error" ans) 136 'error 137 (let ([ans-t (judgment-holds (typeof • ,ans τ) τ)]) 138 (cond 139 [(equal? M-t ans-t) ans] 140 [else (format "internal error: type soundness fails for ~s" M)])))] 141 [else 142 (format "internal error: not exactly 1 result ~s => ~s" M res)])] 143 [else 144 (error 'Eval "argument doesn't typecheck: ~s" M)])) 145 146(define-metafunction stlc 147 answer : any -> any 148 [(answer (λ (x τ) M)) λ] 149 [(answer c) c] 150 [(answer (cons v)) λ] 151 [(answer ((cons v_1) v_2)) cons] 152 [(answer (+ v)) λ] 153 [(answer error) error]) 154 155(define x? (redex-match stlc x)) 156 157(define v? (redex-match? stlc v)) 158(define τ? (redex-match? stlc τ)) 159(define/contract (type-check M) 160 (-> M? (or/c τ? #f)) 161 (define M-t (judgment-holds (typeof • ,M τ) τ)) 162 (cond 163 [(empty? M-t) 164 #f] 165 [(null? (cdr M-t)) 166 (car M-t)] 167 [else 168 (error 'type-check "non-unique type: ~s : ~s" M M-t)])) 169 170(define (progress-holds? M) 171 (if (type-check M) 172 (or (v? M) 173 (not (null? (apply-reduction-relation red (term ,M))))) 174 #t)) 175 176(define (interesting-term? M) 177 (and (type-check M) 178 (term (uses-bound-var? () ,M)))) 179 180(define-metafunction stlc 181 [(uses-bound-var? (x_0 ... x_1 x_2 ...) x_1) 182 #t] 183 [(uses-bound-var? (x_0 ...) (λ (x τ) M)) 184 (uses-bound-var? (x x_0 ...) M)] 185 [(uses-bound-var? (x ...) (M N)) 186 ,(or (term (uses-bound-var? (x ...) M)) 187 (term (uses-bound-var? (x ...) N)))] 188 [(uses-bound-var? (x ...) (cons M)) 189 (uses-bound-var? (x ...) M)] 190 [(uses-bound-var? (x ...) any) 191 #f]) 192 193(define (really-interesting-term? M) 194 (and (interesting-term? M) 195 (term (applies-bv? () ,M)))) 196 197(define-metafunction stlc 198 [(applies-bv? (x_0 ... x_1 x_2 ...) (x_1 M)) 199 #t] 200 [(applies-bv? (x_0 ...) (λ (x τ) M)) 201 (applies-bv? (x x_0 ...) M)] 202 [(applies-bv? (x ...) (M N)) 203 ,(or (term (applies-bv? (x ...) M)) 204 (term (applies-bv? (x ...) N)))] 205 [(applies-bv? (x ...) (cons M)) 206 (applies-bv? (x ...) M)] 207 [(applies-bv? (x ...) any) 208 #f]) 209 210(define (reduction-step-count/func red v?) 211 (λ (term) 212 (let loop ([t term] 213 [n 0]) 214 (define res (apply-reduction-relation red t)) 215 (cond 216 [(and (empty? res) 217 (v? t)) 218 n] 219 [(and (empty? res) 220 (equal? t "error")) 221 n] 222 [(= (length res) 1) 223 (loop (car res) (add1 n))] 224 [else 225 (error 'reduction-step-count "failed reduction: ~s\n~s\n~s" term t res)])))) 226 227(define reduction-step-count 228 (reduction-step-count/func red v?)) 229 230;; rewrite all βv redexes already in the term 231;; (but not any new ones that might appear) 232(define-metafunction stlc 233 βv-> : M -> M 234 [(βv-> ((λ (x τ) M) v)) (subst (βv-> M) x (βv-> v))] 235 [(βv-> ((λ (x τ) M) y)) (subst (βv-> M) x y)] 236 [(βv-> (λ (x τ) M)) (λ (x τ) (βv-> M))] 237 [(βv-> (M N)) ((βv-> M) (βv-> N))] 238 [(βv-> M) M]) 239 240;; check : (or/c #f M) -> boolean[#f = counterexample found!] 241(define (subst-check M) 242 (or (not M) 243 (let ([M-type (type-check M)]) 244 (implies M-type 245 (let* ([N (term (βv-> ,M))][N-type (type-check N)]) 246 (and (equal? N-type M-type) 247 (let ([a1 (Eval M)] [a2 (Eval N)]) 248 (and (not (string? a1)) (not (string? a2)) 249 (equal? (term (answer ,a1)) (term (answer ,a2))) 250 (or (equal? a1 'error) 251 (and (equal? (type-check a1) M-type) 252 (equal? (type-check a2) M-type))))))))))) 253 254(module+ test 255 256 (require redex/examples/stlc-tests-lib) 257 258 (stlc-tests uses-bound-var? 259 typeof 260 red 261 reduction-step-count 262 Eval 263 subst) 264 265 (test-equal (term (βv-> ((λ (x int) x) 1))) 266 (term 1)) 267 (test-equal (term (βv-> (((λ (x (int → int)) x) (λ (x int) x)) 1))) 268 (term ((λ (x int) x) 1))) 269 (test-equal (term (βv-> ((+ ((λ (x int) x) 1)) ((λ (y int) y) 2)))) 270 (term ((+ 1) 2))) 271 (test-equal (term (βv-> (λ (y int) ((λ (x int) x) y)))) 272 (term (λ (y int) y))) 273 (test-equal (subst-check (term ((λ (x int) x) 1))) #t) 274 (test-equal (subst-check (term (hd ((cons 1) 2)))) #t) 275 276 (test-results))