Mercurial > hg > Members > Moririn
changeset 542:ee65e69c9b62
puttree1 act
| author | ryokka |
|---|---|
| date | Thu, 11 Jan 2018 17:38:13 +0900 |
| parents | 429ece770187 |
| children | 1595dd84fc3e |
| files | RedBlackTree.agda redBlackTreeTest.agda |
| diffstat | 2 files changed, 18 insertions(+), 11 deletions(-) [+] |
line wrap: on
line diff
--- a/RedBlackTree.agda Thu Jan 11 15:16:44 2018 +0900 +++ b/RedBlackTree.agda Thu Jan 11 17:38:13 2018 +0900 @@ -198,15 +198,14 @@ getRedBlackTree : {n m : Level } {a k si : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k si -> k -> (RedBlackTree {n} {m} {t} a k si -> (Maybe (Node a k)) -> t) -> t getRedBlackTree {_} {_} {a} {k} {_} {t} tree k1 cs = checkNode (root tree) where + search : Node a k -> t checkNode : Maybe (Node a k) -> t checkNode Nothing = cs tree Nothing checkNode (Just n) = search n - where - search : Node a k -> t - search n with compare tree (key n) k1 - search n | LT = checkNode (left n) - search n | GT = checkNode (right n) - search n | EQ = cs tree (Just n) + search n with compare tree k1 (key n) + search n | LT = checkNode (left n) + search n | GT = checkNode (right n) + search n | EQ = cs tree (Just n) open import Data.Nat hiding (compare)
--- a/redBlackTreeTest.agda Thu Jan 11 15:16:44 2018 +0900 +++ b/redBlackTreeTest.agda Thu Jan 11 17:38:13 2018 +0900 @@ -38,11 +38,19 @@ \t x -> check1 x 1 ≡ True ))) test2 = refl -test3 : putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 - $ \t -> putTree1 t 2 2 - $ \t -> getRedBlackTree t 2 - $ \t x -> check1 x 2 ≡ True -test3 = {!!} -- refl +test3 : putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero}) 1 1 + $ \t -> putTree1 t 2 2 + $ \t -> putTree1 t 3 3 + $ \t -> putTree1 t 4 4 + $ \t -> getRedBlackTree t 4 + $ \t x -> check1 x 4 ≡ True +test3 = refl + +test31 = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ ) 1 1 + $ \t -> putTree1 t 2 2 + $ \t -> putTree1 t 3 3 + $ \t -> putTree1 t 4 4 + $ \t -> root t -- test4 : putTree1 {_} {_} {ℕ} {ℕ} ( createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 $ \t -> putTree1 t 2 2 $ \t -> -- root t ≡ Just (record { key = 1; value = 1; left = Just (record { key = 2 ; value = 2 } ); right = Nothing} )