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