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