Mercurial > hg > Gears > GearsAgda

changeset 588:8627d35d4bff

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add data bt', and some function
author ryokka
date Thu, 05 Dec 2019 20:38:54 +0900
parents f103f07c0552
children 37f5826ca7d2
files hoareBinaryTree.agda hoareRedBlackTree.agda
diffstat 2 files changed, 63 insertions(+), 13 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree.agda	Thu Dec 05 18:11:22 2019 +0900
+++ b/hoareBinaryTree.agda	Thu Dec 05 20:38:54 2019 +0900
@@ -5,7 +5,7 @@
 open import Data.Nat hiding (compare)
 open import Data.Nat.Properties as NatProp
 open import Data.Maybe
-open import Data.Maybe.Properties
+-- open import Data.Maybe.Properties
 open import Data.Empty
 open import Data.List
 open import Data.Product
@@ -45,20 +45,79 @@
 
 tt = pushSigmaStack 3 (true ∷ []) (λ st → st)
 
+_iso_ : {n : Level} {a : Set n} → ℕ → ℕ → Set
+d iso d' = (¬ (suc d ≤ d')) ∧ (¬ (suc d' ≤ d))
+
+iso-intro : {n : Level} {a : Set n} {x y : ℕ} → ¬ (suc x ≤ y) → ¬ (suc y ≤ x) → _iso_ {n} {a} x y
+iso-intro = λ z z₁ → record { proj1 = z ; proj2 = z₁ }
+
+
 {--
   data A B : C → D → Set where の A B と C → D の差は？
   
  --}
-data bt {n : Level} {a : Set n} : Set n where
+
+data bt {n : Level} {a : Set n} : Set n where --  (a : Setn)
   bt-leaf : ⦃ l u : ℕ ⦄ → l ≤ u → bt
   bt-node : ⦃ l l' u u' : ℕ ⦄ → (d : ℕ) →
              bt {n} {a}  → bt {n} {a} → l ≤ l' → u' ≤ u → bt 
 
+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) →
+             bt' {n} A l  → bt' {n} A r → l < key → key < r → bt' A key
+
+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))))
+
+bt-find' : {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-find' key (bt'-leaf key₁) stack next = {!!}
+bt-find' key (bt'-node key₁ value tree tree₁ x x₁) stack next with <-cmp key key₁
+bt-find' {n} {m} {A} {t} key tr@(bt'-node {l} {r} key₁ value tree tree₁ x x₁) stack next | tri< a ¬b ¬c =
+         bt-find' {n} {m} {A} {t} key tree ( (bt'-left {n} {A} key {key₁} {!!} {!!}  )  ∷ stack)  next
+bt-find' key found@(bt'-node key₁ value tree tree₁ x x₁) stack next | tri≈ ¬a b ¬c = next {!!} stack
+bt-find' key (bt'-node key₁ value tree tree₁ x x₁) stack next | tri> ¬a ¬b c = {!!}
+
+
+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' = {!!}
+
+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 → {!!})
+
+
+-- find'-support : {n m : Level} {a : Set n} {t : Set m}  ⦃ l u : ℕ  ⦄ → (d : ℕ) → (tree : bt' {n} {a} ) → SingleLinkedStack (bt' {n} {a} ) → ( (bt' {n} {a} ) → SingleLinkedStack (bt' {n} {a} ) → Maybe (Σ ℕ (λ d' → _iso_  {n} {a} d d')) → t ) → t
+
+-- find'-support {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key leaf@(bt'-leaf x) st cg = cg leaf st nothing
+-- find'-support {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (bt'-node d tree₁ tree₂ x x₁) st cg with <-cmp key d
+-- find'-support {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key node@(bt'-node d tree₁ tree₂ x x₁) st cg | tri≈ ¬a b ¬c = cg node st (just (d , iso-intro {n} {a} ¬a ¬c))
+
+-- find'-support {n} {m} {a} {t}  key node@(bt'-node ⦃ nl ⦄ ⦃ l' ⦄ ⦃ nu ⦄ ⦃ u' ⦄ d L R x x₁) st cg | tri< a₁ ¬b ¬c =
+--                          pushSingleLinkedStack st node
+--                          (λ st2 → find'-support {n} {m} {a} {t} {{l'}} {{d}} key L st2 cg)
+
+-- find'-support {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key node@(bt'-node ⦃ ll ⦄ ⦃ ll' ⦄ ⦃ lr ⦄ ⦃ lr' ⦄ d L R x x₁) st cg | tri> ¬a ¬b c = pushSingleLinkedStack st node
+--                          (λ st2 → find'-support {n} {m} {a} {t} {{d}} {{lr'}} key R st2 cg)
+
+
+
 lleaf : {n : Level} {a : Set n} → bt {n} {a} 
 lleaf = (bt-leaf ⦃ 0 ⦄ ⦃ 3 ⦄ z≤n)
 
+lleaf1 : {n : Level} {A : Set n} → (0 < 3)  → (a : A) → (d : ℕ ) → bt' {n} A d
+lleaf1 0<3 a d = bt'-leaf d
+
+test-node1 : bt' ℕ 3
+test-node1 = bt'-node (3) 3 (bt'-leaf 2) (bt'-leaf 4) (s≤s (s≤s (s≤s z≤n))) (s≤s (s≤s (s≤s (s≤s z≤n))))
+
+
 rleaf : {n : Level} {a : Set n} → bt {n} {a} 
-rleaf = (bt-leaf ⦃ 3 ⦄ ⦃ 4 ⦄ (n≤1+n 3))
+rleaf = (bt-leaf ⦃ 3 ⦄ ⦃ 3 ⦄ (s≤s (s≤s (s≤s z≤n))))
 
 test-node : {n : Level} {a : Set n} → bt {n} {a} 
 test-node {n} {a} = (bt-node ⦃ 0 ⦄ ⦃ 0 ⦄ ⦃ 4 ⦄ ⦃ 4 ⦄ 3 lleaf rleaf z≤n ≤-refl )
@@ -68,12 +127,6 @@
 
 
 
-_iso_ : {n : Level} {a : Set n} → ℕ → ℕ → Set
-d iso d' = (¬ (suc d ≤ d')) ∧ (¬ (suc d' ≤ d))
-
-iso-intro : {n : Level} {a : Set n} {x y : ℕ} → ¬ (suc x ≤ y) → ¬ (suc y ≤ x) → _iso_ {n} {a} x y
-iso-intro = λ z z₁ → record { proj1 = z ; proj2 = z₁ }
-
 -- search の {{ l }} {{ u }} はその時みている node の 大小。 l が小さく u が大きい
 -- ここでは d が現在の node のkey値なので比較後のsearch では値が変わる
 bt-search : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (d : ℕ) → bt {n} {a} → (Maybe (Σ ℕ (λ d' → _iso_  {n} {a} d d')) → t ) → t
@@ -161,16 +214,13 @@
 replace-helper {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ subt@(bt-node d tree tree₁ x₁ x₂) (bt-node d₁ x x₃ x₄ x₅ ∷ st) cg | tri< a₁ ¬b ¬c = replace-helper ⦃ l ⦄ ⦃ u ⦄ (bt-node d₁ subt x₃ x₄ x₅) st cg
 replace-helper {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ subt@(bt-node d tree tree₁ x₁ x₂) (bt-node d₁ x x₃ x₄ x₅ ∷ st) cg | tri≈ ¬a b ¬c = replace-helper ⦃ l ⦄ ⦃ u ⦄ (bt-node d₁ subt x₃ x₄ x₅) st cg
 replace-helper {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ subt@(bt-node d tree tree₁ x₁ x₂) (bt-node d₁ x x₃ x₄ x₅ ∷ st) cg | tri> ¬a ¬b c = replace-helper ⦃ l ⦄ ⦃ u ⦄ (bt-node d₁ x₃ subt x₄ x₅) st cg
-
 replace-helper {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ tree (x ∷ st) cg = replace-helper ⦃ l ⦄ ⦃ u ⦄ tree st cg  -- Unknown Case
 
 
 
-
 bt-replace : {n m : Level} {a : Set n} {t : Set m}  ⦃ l u : ℕ  ⦄
            → (d : ℕ) → (bt {n} {a} ) → SingleLinkedStack (bt {n} {a} )
            → Maybe (Σ ℕ (λ d' → _iso_  {n} {a} d d')) → ( (bt {n} {a} ) → t ) → t
-
 bt-replace {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ d tree st eqP cg = replace-helper {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ ((bt-node ⦃ 0 ⦄ ⦃ 0 ⦄ ⦃ d ⦄ ⦃ d ⦄ d (bt-leaf ⦃ 0 ⦄ ⦃ d ⦄ z≤n ) (bt-leaf  ⦃ d ⦄  ⦃ d ⦄ ≤-refl) z≤n ≤-refl)) st cg
 
 
--- a/hoareRedBlackTree.agda	Thu Dec 05 18:11:22 2019 +0900
+++ b/hoareRedBlackTree.agda	Thu Dec 05 20:38:54 2019 +0900
@@ -7,7 +7,7 @@
 open import Data.Nat hiding (compare)
 open import Data.Nat.Properties as NatProp
 open import Data.Maybe
-open import Data.Maybe.Properties
+-- open import Data.Maybe.Properties
 open import Data.Empty
 open import Data.List
 open import Data.Product