Mercurial > hg > Gears > GearsAgda

changeset 590:7c424dd0945d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 06 Dec 2019 17:39:37 +0900
parents 37f5826ca7d2
children 8ab2e2f9469f
files hoareBinaryTree.agda
diffstat 1 files changed, 24 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree.agda	Fri Dec 06 13:01:53 2019 +0900
+++ b/hoareBinaryTree.agda	Fri Dec 06 17:39:37 2019 +0900
@@ -62,6 +62,10 @@
   bt-node : ⦃ l l' u u' : ℕ ⦄ → (d : ℕ) →
              bt {n} {a}  → bt {n} {a} → l ≤ l' → u' ≤ u → bt 
 
+--
+--
+--  no children , having left node , having right node , having both
+--
 data bt' {n : Level} (A : Set n) : (key : ℕ) →  Set n where --  (a : Setn)
   bt'-leaf : (key : ℕ) → bt' A key
   bt'-node : { l r : ℕ } → (key : ℕ) → (value : A) →
@@ -70,7 +74,6 @@
 data bt'-path {n : Level} (A : Set n) : Set n where --  (a : Setn)
   bt'-left  : (key : ℕ) → {left-key : ℕ} → (bt' A left-key ) → (key < left-key) → bt'-path A
   bt'-right : (key : ℕ) → {right-key : ℕ} → (bt' A right-key ) → (right-key < key) → bt'-path A
-  bt'-null  : bt'-path A
 
 
 test = bt'-left {Z} {ℕ} 3 {5} (bt'-leaf 5) (s≤s (s≤s (s≤s (s≤s z≤n))))
@@ -85,9 +88,27 @@
 bt-find' key tr@(bt'-node key₁ value tree tree₁ x x₁) stack next | tri> ¬a ¬b c = 
          bt-find' key tree ( (bt'-right key {key₁} tr c )  ∷ stack)  next
 
+a<sa : { a : ℕ } → a < suc a
+a<sa {zero} = s≤s z≤n
+a<sa {suc a} = s≤s a<sa 
 
-bt-replace' : {n m : Level} {A : Set n} {t : Set m} {tn : ℕ} → (key : ℕ) → (tree : bt' ℕ tn ) → List (bt'-path A ) → ( {key1 : ℕ } → bt' A  key1 → List (bt'-path A ) → t ) → t
-bt-replace' = {!!}
+pa<a : { a : ℕ } → pred (suc a) < suc a
+pa<a {zero} = s≤s z≤n
+pa<a {suc a} = s≤s pa<a
+
+bt-replace' : {n m : Level} {A : Set n} {t : Set m} {tn : ℕ} → (key : ℕ) → (value : A ) → (tree : bt' A tn ) → List (bt'-path A )
+    → ( {key1 : ℕ } → bt' A  key1 → t ) → t
+bt-replace' {n} {m} {A} {t} {tn} key value node stack next = bt-replace1 tn node where
+         bt-replace0 : {tn : ℕ } (node : bt' A tn ) → List (bt'-path A ) → t
+         bt-replace0 node [] = next node 
+         bt-replace0 node (bt'-left key x x₁ ∷ stack) = {!!}
+         bt-replace0 node (bt'-right key x x₁ ∷ stack) = {!!}
+         bt-replace1 : (tn : ℕ ) (tree : bt' A tn ) → t
+         bt-replace1 zero (bt'-leaf key0) = bt-replace0 (bt'-node (suc zero) value
+              (bt'-leaf zero) (bt'-leaf (suc (suc zero))) {!!} {!!}) stack
+         bt-replace1 (suc tn) (bt'-leaf key0) = bt-replace0 (bt'-node (suc tn) value
+              (bt'-leaf tn) (bt'-leaf (suc (suc tn)) ){!!} {!!}) stack
+         bt-replace1 tn (bt'-node key value node node₁ x x₁) = bt-replace0 (bt'-node key value node node₁ x x₁) stack
 
 bt-find'-assert1 : {n m : Level} {A : Set n} {t : Set m} → Set n
 bt-find'-assert1 {n} {m} {A} {t} = (key : ℕ) →  (val : A) → bt-find' key {!!} {!!} (λ tree stack → {!!})