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