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 #:binding-forms 36 (λ (x σ) M #:refers-to x) 37 ) 38 39(define-judgment-form stlc 40 #:mode (typeof I I O) 41 #:contract (typeof Γ M σ) 42 43 [--------------------------- 44 (typeof Γ c (const-type c))] 45 46 [(where τ (lookup Γ x)) 47 ---------------------- 48 (typeof Γ x τ)] 49 50 [(typeof (x σ Γ) M σ_2) 51 -------------------------------- 52 (typeof Γ (λ (x σ) M) (σ → σ_2))] 53 54 [(typeof Γ M (σ → σ_2)) 55 (typeof Γ M_2 σ) 56 ---------------------- 57 (typeof Γ (M M_2) σ_2)]) 58 59(define-metafunction stlc 60 const-type : c -> σ 61 [(const-type nil) 62 (list int)] 63 [(const-type cons) 64 (int → ((list int) → (list int)))] 65 [(const-type hd) 66 ((list int) → int)] 67 [(const-type tl) 68 ((list int) → (list int))] 69 [(const-type +) 70 (int → (int → int))] 71 [(const-type integer) 72 int]) 73 74(define-metafunction stlc 75 lookup : Γ x -> σ or #f 76 [(lookup (x σ Γ) x) 77 σ] 78 [(lookup (x σ Γ) x_2) 79 (lookup Γ x_2)] 80 [(lookup • x) 81 #f]) 82 83(define red 84 (reduction-relation 85 stlc 86 (--> (in-hole E ((λ (x τ) M) v)) 87 (in-hole E (substitute M x v)) 88 "βv") 89 (--> (in-hole E (hd ((cons v_1) v_2))) 90 (in-hole E v_1) 91 "hd") 92 (--> (in-hole E (tl ((cons v_1) v_2))) 93 (in-hole E v_2) 94 "tl") 95 (--> (in-hole E (hd nil)) 96 "error" 97 "hd-err") 98 (--> (in-hole E (tl nil)) 99 "error" 100 "tl-err") 101 (--> (in-hole E ((+ integer_1) integer_2)) 102 (in-hole E ,(+ (term integer_1) (term integer_2))) 103 "+"))) 104 105(define M? (redex-match stlc M)) 106(define/contract (Eval M) 107 (-> M? (or/c M? "error")) 108 (define M-t (judgment-holds (typeof • ,M τ) τ)) 109 (unless (pair? M-t) 110 (error 'Eval "doesn't typecheck: ~s" M)) 111 (define res (apply-reduction-relation* red M)) 112 (unless (= 1 (length res)) 113 (error 'Eval "internal error: not exactly 1 result ~s => ~s" M res)) 114 (define ans (car res)) 115 (if (equal? "error" ans) 116 "error" 117 (let ([ans-t (judgment-holds (typeof • ,ans τ) τ)]) 118 (unless (equal? M-t ans-t) 119 (error 'Eval "internal error: type soundness fails for ~s" M)) 120 ans))) 121 122(define x? (redex-match stlc x)) 123(define-metafunction stlc 124 subst : M x M -> M 125 [(subst M x N) 126 (substitute M x N)]) 127 128(define v? (redex-match? stlc v)) 129(define τ? (redex-match? stlc τ)) 130(define/contract (type-check M) 131 (-> M? (or/c τ? #f)) 132 (define M-t (judgment-holds (typeof • ,M τ) τ)) 133 (cond 134 [(empty? M-t) 135 #f] 136 [(null? (cdr M-t)) 137 (car M-t)] 138 [else 139 (error 'type-check "non-unique type: ~s : ~s" M M-t)])) 140 141(test-equal (type-check (term 5)) 142 (term int)) 143(test-equal (type-check (term (5 5))) 144 #f) 145 146(define (progress-holds? M) 147 (if (type-check M) 148 (or (v? M) 149 (not (null? (apply-reduction-relation red (term ,M))))) 150 #t)) 151 152(define (interesting-term? M) 153 (and (type-check M) 154 (term (uses-bound-var? () ,M)))) 155 156(define-metafunction stlc 157 [(uses-bound-var? (x_0 ... x_1 x_2 ...) x_1) 158 #t] 159 [(uses-bound-var? (x_0 ...) (λ (x τ) M)) 160 (uses-bound-var? (x x_0 ...) M)] 161 [(uses-bound-var? (x ...) (M N)) 162 ,(or (term (uses-bound-var? (x ...) M)) 163 (term (uses-bound-var? (x ...) N)))] 164 [(uses-bound-var? (x ...) (cons M)) 165 (uses-bound-var? (x ...) M)] 166 [(uses-bound-var? (x ...) any) 167 #f]) 168 169(define (really-interesting-term? M) 170 (and (interesting-term? M) 171 (term (applies-bv? () ,M)))) 172 173(define-metafunction stlc 174 [(applies-bv? (x_0 ... x_1 x_2 ...) (x_1 M)) 175 #t] 176 [(applies-bv? (x_0 ...) (λ (x τ) M)) 177 (applies-bv? (x x_0 ...) M)] 178 [(applies-bv? (x ...) (M N)) 179 ,(or (term (applies-bv? (x ...) M)) 180 (term (applies-bv? (x ...) N)))] 181 [(applies-bv? (x ...) (cons M)) 182 (applies-bv? (x ...) M)] 183 [(applies-bv? (x ...) any) 184 #f]) 185 186(define (reduction-step-count/func red v?) 187 (λ (term) 188 (let loop ([t term] 189 [n 0]) 190 (define res (apply-reduction-relation red t)) 191 (cond 192 [(and (empty? res) 193 (v? t)) 194 n] 195 [(and (empty? res) 196 (equal? t "error")) 197 n] 198 [(= (length res) 1) 199 (loop (car res) (add1 n))] 200 [else 201 (error 'reduction-step-count "failed reduction: ~s\n~s\n~s" term t res)])))) 202 203(define reduction-step-count 204 (reduction-step-count/func red v?)) 205 206 207(module+ test 208 209 (require redex/examples/stlc-tests-lib) 210 211 (parameterize ([default-language stlc]) 212 213 (stlc-tests uses-bound-var? 214 typeof 215 red 216 reduction-step-count 217 Eval 218 subst))) 219