Mercurial > hg > Gears > GearsAgda

comparison redBlackTreeTest.agda @ 544:4f692df9b3db

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add reference
author ryokka
date Thu, 11 Jan 2018 18:54:56 +0900
parents 1595dd84fc3e
children b180dc78abcf
comparison
equal deleted inserted replaced
543:1595dd84fc3e 544:4f692df9b3db
39 test2 = refl 39 test2 = refl
40 40
41 test3 : putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero}) 1 1 41 test3 : putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero}) 1 1
42 $ \t -> putTree1 t 2 2 42 $ \t -> putTree1 t 2 2
43 $ \t -> putTree1 t 3 3 43 $ \t -> putTree1 t 3 3
44 $ \t -> putTree1 t 4 4 44 $ \t -> putTree1 t 4 4
45 $ \t -> getRedBlackTree t 4 45 $ \t -> getRedBlackTree t 4
46 $ \t x -> check1 x 4 ≡ True 46 $ \t x -> check1 x 4 ≡ True
47 test3 = refl 47 test3 = refl
48 48
49 test31 = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ ) 1 1 49 test31 = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ ) 1 1
50 $ \t -> putTree1 t 2 2 50 $ \t -> putTree1 t 2 2
51 $ \t -> putTree1 t 3 3 51 $ \t -> putTree1 t 3 3
52 $ \t -> putTree1 t 4 4 52 $ \t -> putTree1 t 4 4
53 $ \t -> root t 53 $ \t -> getRedBlackTree t 4
54 54 $ \t x -> x
55 -- test4 : putTree1 {_} {_} {ℕ} {ℕ} ( createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 $ \t -> putTree1 t 2 2 $ \t ->
56 -- root t ≡ Just (record { key = 1; value = 1; left = Just (record { key = 2 ; value = 2 } ); right = Nothing} )
57 -- test4 = refl
58
59 55
60 -- test5 : Maybe (Node ℕ ℕ) 56 -- test5 : Maybe (Node ℕ ℕ)
61 test5 = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ ) 4 4 57 test5 = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ ) 4 4
62 $ \t -> putTree1 t 6 6 58 $ \t -> putTree1 t 6 6
63 $ \t0 -> clearSingleLinkedStack (nodeStack t0) 59 $ \t0 -> clearSingleLinkedStack (nodeStack t0)
89 value1 = 1 85 value1 = 1
90 86
91 test8 : Maybe (Node ℕ ℕ) 87 test8 : Maybe (Node ℕ ℕ)
92 test8 = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ) 1 1 88 test8 = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ) 1 1
93 $ \t -> putTree1 t 2 2 (\ t -> root t) 89 $ \t -> putTree1 t 2 2 (\ t -> root t)
90
91
92 test9 : putRedBlackTree {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 ( \t -> getRedBlackTree t 1 ( \t x -> check1 x 1 ≡ True ))
93 test9 = refl
94
95 test10 : putRedBlackTree {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 (
96 \t -> putRedBlackTree t 2 2 (
97 \t -> getRedBlackTree t 1 (
98 \t x -> check1 x 1 ≡ True )))
99 test10 = refl
100
101 test11 = putRedBlackTree {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ) 1 1
102 $ \t -> putRedBlackTree t 2 2
103 $ \t -> putRedBlackTree t 3 3
104 $ \t -> getRedBlackTree t 2
105 $ \t x -> root t