1#lang racket 2(require redex) 3 4(provide (all-defined-out)) 5 6;; This semantics comes from the paper 7;; _A Natural Semantics for Lazy Evaluation_, 8;; by John Launchbury, POPL 1993 9;; extended with integers, +, and if0. 10 11(define-language L 12 (e ::= 13 v 14 (e x) 15 (let ([x e] ...) e) 16 x 17 (+ e e) ;; add addition 18 (if0 e e e)) ;; add conditional 19 (v ::= ;; don't use 'z' for values, 20 ;; because that's confusing 21 i ;; add integer constants 22 (λ (x) e)) 23 24 (i ::= integer) 25 (x y z ::= variable-not-otherwise-mentioned) 26 27 (Γ Δ Θ ::= · (Γ x ↦ e)) 28 29 #:binding-forms 30 (let ([x e] ...) e_body #:refers-to (shadow x ...)) 31 (λ (x) e #:refers-to x)) 32 33(define-judgment-form L 34 #:mode (⇓ I I O O) 35 #:contract (⇓ Γ e Δ v) 36 37 38 [----------- Value 39 (⇓ Γ v Γ v)] 40 41 42 [(⇓ Γ e Δ (λ (y) e_*)) 43 (⇓ Δ (substitute e_* y x) Θ v) 44 ------------------------- Application 45 (⇓ Γ (e x) Θ v)] 46 47 48 [(where (Γ x ↦ e) (separate Γ_* x)) 49 (⇓ Γ e Δ v) 50 (where Δ_* (Δ x ↦ v)) 51 ---------------------------------- Variable 52 (⇓ Γ_* x Δ_* v)] 53 54 55 [(⇓ (extend Γ (x_i e_i) ...) e Δ v) 56 ---------------------------------- Let 57 (⇓ Γ (let ([x_i e_i] ...) e) Δ v)] 58 59 60 [(⇓ Γ e_1 Θ i_1) 61 (⇓ Θ e_2 Δ i_2) 62 ---------------------------------------------- Add 63 (⇓ Γ (+ e_1 e_2) Δ ,(+ (term i_1) (term i_2)))] 64 65 66 [(⇓ Γ e_1 Θ i) 67 (⇓ Θ (choose i e_2 e_3) Δ v) 68 ---------------------------- If 69 (⇓ Γ (if0 e_1 e_2 e_3) Δ v)]) 70 71(define-metafunction L 72 choose : i e e -> e 73 [(choose 0 e_1 e_2) e_1] 74 [(choose i e_1 e_2) e_2]) 75 76(define-metafunction L 77 separate : Γ x -> (Γ x ↦ e) or ⊥ 78 [(separate · x) ⊥] 79 [(separate (Γ x ↦ e) x) (Γ x ↦ e)] 80 [(separate (Γ y ↦ e_*) x) 81 ((Γ_* y ↦ e_*) x ↦ e) 82 (where (Γ_* x ↦ e) (separate Γ x))] 83 [(separate (Γ y ↦ e_*) x) ⊥ 84 (where ⊥ (separate Γ x))]) 85 86(define-metafunction L 87 extend : Γ (x e) ... -> Γ 88 [(extend Γ) Γ] 89 [(extend Γ (x e) (x_* e_*) ...) 90 (extend (Γ x ↦ e) (x_* e_*) ...)]) 91 92 93 94(define e? (redex-match? L e)) 95(define v? (redex-match? L v)) 96(define T-v? (redex-match? L (T v))) 97 98 99;; run a program to get it's result 100(define/contract (run p) 101 (-> e? (or/c v? #f)) 102 (define vs (judgment-holds (⇓ · ,p Δ v) v)) 103 (cond 104 [(pair? vs) 105 (unless (= 1 (length vs)) 106 (error 'run "multiple results ~s" vs)) 107 (car vs)] 108 [else #f])) 109 110;; opens a visualization of the derivation 111(define (show p) 112 (-> e? void?) 113 (show-derivations 114 (build-derivations 115 (⇓ · ,p Δ v)))) 116 117(module+ test 118 119 (default-language L) 120 121 ;; replace-free, rename-bound, and subst tests omitted, since those metafunctions are gone 122 123 (test-equal (term (separate · x)) (term ⊥)) 124 (test-equal (term (separate (· x ↦ 1) x)) (term (· x ↦ 1))) 125 (test-equal (term (separate ((· x ↦ 1) y ↦ 2) x)) 126 (term ((· y ↦ 2) x ↦ 1))) 127 (test-equal (term (separate (· x ↦ 1) y)) (term ⊥)) 128 129 ;; ^ tests omitted, since that metafunction is gone 130 131 (test-equal (judgment-holds (⇓ (· y ↦ 1) ((λ (x) x) y) Δ v) v) 132 (list (term 1))) 133 134 (test-equal (run (term 1)) 1) 135 (test-equal (run (term (let ([y 1]) 136 (let ([z ((λ (x) x) y)]) 137 2)))) 138 2) 139 (test-equal (run (term (let ([y 1]) y))) 1) 140 (test-equal (run (term (let ([y (λ (x) x)]) y))) (term (λ (x1) x1))) 141 (test-equal (run (term (let ([y 1]) ((λ (x) x) y)))) 1) 142 (test-equal (run (term 143 (let ([app (λ (f) (λ (x) (f x)))] 144 [f (λ (x) (λ (y) x))] 145 [o 1]) 146 (((app f) o) f)))) 147 1) 148 (test-equal (run (term (if0 0 1 2))) 1) 149 (test-equal (run (term (if0 1 2 3))) 3) 150 151 ;; free variable errors return no derivation 152 (test-equal (run (term (let ([x y]) x))) #f) 153 154 ;; as do runtime errors 155 (test-equal (run (term (let ([two 2]) (1 two)))) #f) 156 157 (test-equal (run 158 (term 159 (let ([o 1] 160 [t 2] 161 [r 3] 162 [f 4]) 163 (((((λ (x) 164 (λ (y) 165 (λ (z) 166 (λ (w) 167 (+ (+ x y) 168 (+ w z)))))) 169 o) 170 t) 171 r) 172 f)))) 173 10) 174 175 (test-equal (run (term 176 (let ([me (λ (x) x)]) 177 (let ([tri 178 (λ (x) 179 (let ([x1 (+ x -1)]) 180 (+ (me x1) x)))] 181 [five 5]) 182 (tri five))))) 183 9) 184 185 (test-equal (run (term (let ([tri 186 (λ (x) 187 (let ([x1 (+ x -1)]) 188 x))] 189 [five 5]) 190 (tri five)))) 191 5) 192 193 (test-equal (run (term 194 (let ([Y (λ (f) 195 (let ([g (λ (x) 196 (let ([xx (x x)]) 197 (f xx)))]) 198 (g g)))] 199 [tri 200 (λ (me) 201 (λ (x) 202 (if0 x 203 0 204 (let ([x1 (+ x -1)]) 205 (+ (me x1) x)))))] 206 [five 5]) 207 ((Y tri) five)))) 208 (+ 5 4 3 2 1 0)) 209 210 211 (test-equal (run (term (let ([one 1] [two 2]) 212 (((λ (x) (λ (x) (+ x one))) one) two)))) 213 3) 214 215 (test-results)) 216