1#lang racket
2
3#|
4
5A core contract calculus, including blame,
6with function contracts, (eager) pair contracts,
7and a few numeric predicates
8
9|#
10
11(require redex/reduction-semantics
12         redex/examples/subst)
13
14(define-language lang
15  (e (e e ...)
16     x
17     number
18     (λ (x ...) e)
19
20     (if e e e)
21     #t #f
22
23     cons car cdr
24
25     -> or/c
26     ac
27     pred?
28     (blame l)
29     l)
30  (pred? number?
31         odd?
32         positive?)
33  (E (v ... E e ...)
34     (if E e e)
35     hole)
36  (v number
37     (λ (x ...) e)
38     cons car cdr
39     (cons v v)
40     pred?
41     -> or/c ac
42     (-> v ...)
43     (or/c v ...)
44     #t #f
45     l)
46
47  (l + -) ;; blame labels
48
49  (x variable-not-otherwise-mentioned))
50
51(define reds
52  (reduction-relation
53   lang
54   (--> (in-hole E ((λ (x ...) e) v ...))
55        (in-hole E (subst-n ((x v) ... e)))
56        (side-condition (= (length (term (x ...)))
57                           (length (term (v ...)))))
58        βv)
59
60   (--> (in-hole E (if #t e_1 e_2)) (in-hole E e_1) ift)
61   (--> (in-hole E (if #f e_1 e_2)) (in-hole E e_2) iff)
62
63   (--> (in-hole E (number? number)) (in-hole E #t))
64   (--> (in-hole E (number? v))
65        (in-hole E #f)
66        (side-condition (not (number? (term v)))))
67
68   (--> (in-hole E (car (cons v_1 v_2)))
69        (in-hole E v_1))
70   (--> (in-hole E (cdr (cons v_1 v_2)))
71        (in-hole E v_2))
72
73   (--> (in-hole E (odd? number))
74        (in-hole E #t)
75        (side-condition (odd? (term number))))
76   (--> (in-hole E (odd? v))
77        (in-hole E #f)
78        (side-condition (or (not (number? (term v)))
79                            (not (odd? (term v))))))
80
81   (--> (in-hole E (positive? number))
82        (in-hole E #t)
83        (side-condition (positive? (term number))))
84   (--> (in-hole E (positive? v))
85        (in-hole E #f)
86        (side-condition (or (not (number? (term v)))
87                            (not (positive? (term v))))))
88
89
90   (--> (in-hole E (blame l))
91        (blame l)
92        (side-condition (not (equal? (term E) (term hole)))))
93
94   (--> (in-hole E (ac pred? v l))
95        (in-hole E (if (pred? v) v (blame l))))
96   (--> (in-hole E (ac (-> v_dom ... v_rng) (λ (x ...) e) l))
97        (in-hole E (λ (x ...) (ac v_rng ((λ (x ...) e) (ac v_dom x l_2) ...) l)))
98        (where l_2 (¬ l)))
99
100   (--> (in-hole E (ac (cons v_1 v_2) (cons v_3 v_4) l))
101        (in-hole E (cons (ac v_1 v_3 l) (ac v_2 v_4 l))))
102
103   (--> (in-hole E (ac (or/c pred? v_1 v_2 ...) v_3 l))
104        (in-hole E (if (pred? v_3)
105                       v_3
106                       (ac (or/c v_1 v_2 ...) v_3 l))))
107   (--> (in-hole E (ac (or/c v_1) v_2 l))
108        (in-hole E (ac v_1 v_2 l)))
109   ))
110
111(define-metafunction lang
112  [(¬ +) -]
113  [(¬ -) +])
114
115(test-->> reds (term ((λ (x y) x) 1 2)) 1)
116(test-->> reds (term ((λ (x y) y) 1 2)) 2)
117(test-->> reds (term (if (if #t #f #t) #f #t)) (term #t))
118(test-->> reds (term (positive? 1)) #t)
119(test-->> reds (term (positive? -1)) #f)
120(test-->> reds (term (positive? (λ (x) x))) #f)
121(test-->> reds (term (odd? 1)) #t)
122(test-->> reds (term (odd? 2)) #f)
123(test-->> reds (term (odd? (λ (x) x))) #f)
124(test-->> reds (term (car (cdr (cdr (cons 1 (cons 2 (cons 3 #f))))))) 3)
125
126(test-->> reds (term ((λ (x) x) (blame -))) (term (blame -)))
127(test-->> reds (term (ac number? 1 +)) 1)
128(test-->> reds (term (ac number? (λ (x) x) +)) (term (blame +)))
129(test-->> reds (term ((ac (-> number? number?) (λ (x) x) +) 1)) 1)
130(test-->> reds
131         (term ((ac (-> number? number?) (λ (x) x) +) #f))
132         (term (blame -)))
133(test-->> reds
134         (term ((ac (-> number? number?) (λ (x) #f) +) 1))
135         (term (blame +)))
136(test-->> reds
137         (term (ac (or/c odd? positive?) 1 +))
138         1)
139(test-->> reds
140         (term (ac (or/c odd? positive?) -1 +))
141         -1)
142(test-->> reds
143         (term (ac (or/c odd? positive?) 2 +))
144         2)
145(test-->> reds
146         (term (ac (or/c odd? positive?) -2 +))
147         (term (blame +)))
148
149(test-->> reds
150         (term (ac (cons odd? positive?) (cons 3 1) +))
151         (term (cons 3 1)))
152
153(test-results)
154