1#lang racket
2(require redex
3         "subst.rkt")
4
5(reduction-steps-cutoff 10)
6
7(define-language lang
8  (e (e e)
9     x
10     number
11     (lambda (x t) e)
12     (if e e e)
13     (= e e)
14     (-> e e)
15     num
16     bool)
17  (c (t c)
18     (c e)
19     (-> t c)
20     (-> c e)
21     (= t c)
22     (= c e)
23     (if c e e)
24     (if t c e)
25     (if t t c)
26     hole)
27  (x (variable-except lambda -> if =))
28  (t num bool (-> t t)))
29
30(define reductions
31  (reduction-relation
32   lang
33   (r--> number num)
34
35   (r--> (lambda (x_1 t_1) e_body)
36         (-> t_1 (subst (x_1 t_1 e_body))))
37
38   (r--> ((-> t_1 t_2) t_1) t_2)
39
40   (e--> (side-condition ((-> t_1 t) t_2)
41                         (not (equal? (term t_1) (term t_2))))
42         ,(format "app: domain error ~s and ~s" (term t_1) (term t_2)))
43
44   (e--> (num t_1)
45         ,(format "app: non function error ~s" (term t_1)))
46
47   (r--> (if bool t_1 t_1) t_1)
48   (e--> (side-condition (if bool t_1 t_2)
49                         (not (equal? (term t_1) (term t_2))))
50         ,(format "if: then and else clause mismatch ~s and ~s" (term t_1) (term t_2)))
51   (e--> (side-condition (if t_1 t t)
52                         (not (equal? (term t_1) 'bool)))
53         ,(format "if: test not boolean ~s" (term t_1)))
54
55   (r--> (= num num) bool)
56   (e--> (side-condition (= t_1 t_2)
57                         (or (not (equal? (term t_1) 'num))
58                             (not (equal? (term t_2) 'num))))
59         ,(format "=: not comparing numbers ~s and ~s" (term t_1) (term t_2)))
60
61   with
62
63   [(--> (in-hole c_1 a) (in-hole c_1 b)) (r--> a b)]
64   [(--> (in-hole c a) b) (e--> a b)]))
65
66(traces reductions
67        '((lambda (x num) (lambda (y num) (if (= x y) 0 x))) 1))
68(traces reductions
69        '((lambda (x num) (lambda (y num) (if (= x y) 0 (lambda (x num) x)))) 1))
70