-
Notifications
You must be signed in to change notification settings - Fork 0
/
mini-calc-test.rkt
60 lines (53 loc) · 2.84 KB
/
mini-calc-test.rkt
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
#lang racket
(require redex
"mini-calc.rkt")
;; mini-calc tests
(define s1 (term (σ ((rc 1 1) := (1 + 1)))))
(define s2 (term (σ ((rc 1 1) := (1 + 1)) ((rc 1 2) := (0 = 2)))))
(define s3 (term (σ ((rc 1 1) := (1 + 1)) ((rc 1 2) := (0 = 2)) ((rc 2 1) := (IF (1 = 2) 0 1)))))
(define s4 (term (σ ((rc 1 1) := ((1 + 1) + (rc 1 2))) ((rc 1 2) := 42))))
(define s5 (term (σ ((rc 1 1) := 42) ((rc 1 2) := (rc [0] [-1])))))
(define s6 (term (σ ((rc 1 1) := ((rc 1 2) + 1)) ((rc 1 2) := 42))))
(define s7 (term (σ ((rc 1 1) := ((rc 1 2) + 1)) ((rc 1 2) := (41 + 1)))))
(define s8 (term (σ ((rc 1 1) := ((rc [0] [1]) + 1)) ((rc 1 2) := (41 + 1)))))
(define s9 (term (σ ((rc 1 1) := 1) ((rc 1 2) := (1 + (rc 1 1)))
((rc 2 1) := (1 + (rc 1 1))))))
(define s10 (term (σ ((rc 1 1) := 1) ((rc 1 2) := (1 + (rc [0] [-1])))
((rc 2 1) := (1 + (rc [-1] [0]))))))
(define s11 (term (σ ((rc 1 1) := 1)
((rc 2 1) := (SUM ((rc [-1] [0]) : (rc [-1] [1])) 1))
((rc 1 2) := (1 + (rc [0] [-1]))))))
(test-equal (redex-match? mini-calc s s1) #t)
(test-equal (redex-match? mini-calc s s2) #t)
(test-equal (redex-match? mini-calc s s3) #t)
(test-equal (redex-match? mini-calc s s4) #t)
(test-equal (redex-match? mini-calc s s5) #t)
(test-equal (redex-match? mini-calc s s6) #t)
(test-equal (redex-match? mini-calc s s7) #t)
(test-equal (redex-match? mini-calc s s8) #t)
(test-equal (redex-match? mini-calc s s9) #t)
(test-equal (redex-match? mini-calc s s10) #t)
(test-equal (redex-match? mini-calc s s11) #t)
(test-equal (apply-reduction-relation* ->mini-calc s1)
'((σ ((rc 1 1) := 2))))
(test-equal (apply-reduction-relation* ->mini-calc s2)
'((σ ((rc 1 1) := 2) ((rc 1 2) := 0))))
(test-equal (apply-reduction-relation* ->mini-calc s3)
'((σ ((rc 1 1) := 2) ((rc 1 2) := 0) ((rc 2 1) := 1))))
(test-equal (apply-reduction-relation* ->mini-calc s4)
'((σ ((rc 1 2) := 42) ((rc 1 1) := 44))))
(test-equal (apply-reduction-relation* ->mini-calc s5)
'((σ ((rc 1 1) := 42) ((rc 1 2) := 42))))
(test-equal (apply-reduction-relation* ->mini-calc s6)
'((σ ((rc 1 2) := 42) ((rc 1 1) := 43))))
(test-equal (apply-reduction-relation* ->mini-calc s7)
'((σ ((rc 1 2) := 42) ((rc 1 1) := 43))))
(test-equal (apply-reduction-relation* ->mini-calc s8)
'((σ ((rc 1 2) := 42) ((rc 1 1) := 43))))
(test-equal (apply-reduction-relation* ->mini-calc s9)
'((σ ((rc 1 1) := 1) ((rc 1 2) := 2) ((rc 2 1) := 2))))
(test-equal (apply-reduction-relation* ->mini-calc s10)
'((σ ((rc 1 1) := 1) ((rc 1 2) := 2) ((rc 2 1) := 2))))
(test-equal (apply-reduction-relation* ->mini-calc s11)
'((σ ((rc 1 1) := 1) ((rc 1 2) := 2) ((rc 2 1) := 4))))
(traces ->mini-calc s11)