Mercurial > hg > Gears > GearsAgda

changeset 539:39d465c20e5a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
print contant tree. C-c C-n test.
author ryokka
date Wed, 10 Jan 2018 18:10:03 +0900
parents 5c001e8ba0d5
children 6a4830c5a514
files redBlackTreeTest.agda
diffstat 1 files changed, 22 insertions(+), 7 deletions(-) [+]
line wrap: on
line diff
--- a/redBlackTreeTest.agda	Wed Jan 10 17:38:24 2018 +0900
+++ b/redBlackTreeTest.agda	Wed Jan 10 18:10:03 2018 +0900
@@ -49,14 +49,29 @@
 test4 = refl
 
 
-
--- test5 : Maybe (Node ℕ ℕ)
--- test5 = putTree1 {_} {_} {ℕ} {ℕ} {_} {Maybe (Node ℕ ℕ)} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 
---     $ \t -> putTree1 t 2 2
---     $ \t -> putTree1 t 3 3 
---     $ \t -> getRedBlackTree t 3
---     $ \t x -> root t 
+test5 : Maybe (Node ℕ ℕ)
+test5 = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ ) 1 1 
+    $ \t -> putTree1 t 2 2
+    $ \t -> putTree1 t 3 3 
+    $ \t -> getRedBlackTree t 3
+    $ \t x -> root t 
 
 -- test51 : putTree1 {_} {_} {ℕ} {ℕ} {_} {Maybe (Node ℕ ℕ)} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero} ) 1 1 $ \t ->
 --   putTree1 t 2 2 $ \t -> putTree1 t 3 3 $ \t -> root t ≡ Just (record { key = 1; value = 1; left = Just (record { key = 2 ; value = 2 } ); right = Nothing} )
 -- test51 = refl
+
+test6 : Maybe (Node ℕ ℕ)
+test6 = root (createEmptyRedBlackTreeℕ {_} ℕ {Maybe (Node ℕ ℕ)})
+
+
+test7 : Maybe (Node ℕ ℕ)
+test7 = clearStack (nodeStack tree2) (\ s -> replaceNode tree2 s n2 (\ t -> root t))
+  where
+    tree2 = createEmptyRedBlackTreeℕ {_} ℕ {Maybe (Node ℕ ℕ)}
+    k1 = 1
+    n2 = leafNode 0 0
+    value1 = 1
+
+test8 : Maybe (Node ℕ ℕ)
+test8 = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ) 1 1 
+    $ \t -> putTree1 t 2 2 (\ t -> root t)