popl-2012-ryr-talk/amb-test.rkt at master · rfindler/popl-2012-ryr-talk · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
#lang racket
(require redex "amb.rkt")

(test-->> red
          (term ((+ 1 2 3)))
          (term (6)))
(test-->> red
          (term ((+ 1 (+ 2 3))))
          (term (6)))
(test-->> red
          (term ((+ (+ 1 2) 3)))
          (term (6)))
(test-->> red
          (term ((amb (+ 1 2) 4)))
          (term (3 4)))
(test-->> red
          (term ((+ 1 (amb 1 2))))
          (term (2 3)))
(test-->> red
          (term ((((λ ((x num)) (λ ((y num)) x)) 1) 2)))
          (term (1)))
(test-->> red
          (term ((((λ ((x num)) (λ ((y num)) (amb x y))) 1) 2)))
          (term (1 2)))
(test-->> red
          (term ((+ (amb (+ 1 2) (+ 3 4.5))
                    (amb (+ 5 6) (+ 7 8)))))
          (term (14 18 18.5 22.5)))

(test-equal (judgment-holds (types (x : num ·) y t_1) t_1)
            (term ()))
(test-equal (judgment-holds (types (x : num ·) x t_1) t_1)
            (term (num)))
(test-equal (judgment-holds (types (x : num (y : (→ num num) ·)) x t_1) t_1)
            (term (num)))
(test-equal (judgment-holds (types (x : num (y : (→ num num) ·)) y t_1) t_1)
            (term ((→ num num))))
(test-equal (judgment-holds (types (x : num (x : (→ num num) ·)) y t_1) t_1)
            (term ()))
(test-equal (judgment-holds (types · (+ 1 2 3) t_1) t_1)
            (term (num)))
(test-equal (judgment-holds (types · (λ ((y num)) y) t_1) t_1)
            (term ((→ num num))))
(test-equal (judgment-holds (types · (λ ((y num) (z num)) y) t_1) t_1)
            (term ((→ num num num))))
(test-equal (judgment-holds (types · (λ ((y num)) (λ ((z num)) y)) t_1) t_1)
            (term ((→ num (→ num num)))))
(test-equal (judgment-holds (types · (((λ ((x num)) (λ ((y num)) x)) 1) 2) t_1) t_1)
            (term (num)))
(test-equal (judgment-holds (types · (amb) t_1) t_1)
            (term (num)))
(test-equal (judgment-holds (types · (amb 1) t_1) t_1)
            (term (num)))
(test-equal (judgment-holds (types · (amb 1 2) t_1) t_1)
            (term (num)))
(test-equal (judgment-holds (types · (+ (amb (+ 1 2) (+ 3 4.5))
                                        (amb (+ 5 6) (+ 7 8)))
                                   t_1)
                            t_1)
            (term (num)))

(test-results)