Mercurial > hg > Gears > GearsAgda

changeset 758:2488a3402c19

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 Tue, 02 May 2023 07:42:19 +0900
parents edfeedb45595
children 8435718138d1
files hoareBinaryTree1.agda
diffstat 1 files changed, 46 insertions(+), 38 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Mon May 01 09:08:01 2023 +0900
+++ b/hoareBinaryTree1.agda	Tue May 02 07:42:19 2023 +0900
@@ -524,19 +524,19 @@
 
 data RBtreeInvariant {n : Level} {A : Set n} : (tree : bt (Color ∧ A)) → (bd : ℕ) → Set n where
     rb-leaf     : RBtreeInvariant leaf 0
-    rb-single : (key : ℕ) → (value : A) → (c : Color) →  RBtreeInvariant (node key ⟪ c , value ⟫ leaf leaf) 1
-    rb-right-red : {key key₁ : ℕ} → {value value₁ : A} → {t t₁ : bt (Color ∧ A)} → key < key₁ → {d : ℕ }
-       → RBtreeInvariant (node key₁ ⟪ Black , value₁ ⟫ t t₁) d
-       → RBtreeInvariant (node key  ⟪ Red ,   value  ⟫ leaf (node key₁ ⟪ Black , value₁ ⟫ t t₁)) d
-    rb-right-black : {key key₁ : ℕ} → {value value₁ : A} → {t t₁ : bt (Color ∧ A)} → key < key₁ → {d : ℕ } {c : Color}
-       → RBtreeInvariant (node key₁ ⟪ c     , value₁ ⟫ t t₁) d
-       → RBtreeInvariant (node key  ⟪ Black , value  ⟫ leaf (node key₁ ⟪ c , value₁ ⟫ t t₁)) (suc d)
-    rb-left-red : {key key₁ : ℕ} → {value value₁ : A} → {t t₁ : bt (Color ∧ A)} → key < key₁ → {d : ℕ }
-       → RBtreeInvariant (node key₁ ⟪ Black , value₁ ⟫ t t₁) d
-       → RBtreeInvariant (node key₁  ⟪ Red ,   value  ⟫ (node key ⟪ Black , value₁ ⟫ t t₁) leaf ) d
-    rb-left-black : {key key₁ : ℕ} → {value value₁ : A} → {t t₁ : bt (Color ∧ A)} → key < key₁ → {d : ℕ } {c : Color}
-       → RBtreeInvariant (node key₁ ⟪ c     , value₁ ⟫ t t₁) d
-       → RBtreeInvariant (node key₁  ⟪ Black , value  ⟫ (node key ⟪ c , value₁ ⟫ t t₁) leaf) (suc d)
+    rb-single : (key : ℕ) → (value : A) →  RBtreeInvariant (node key ⟪ Black , value ⟫ leaf leaf) 1
+    rb-right-red : {key key₁ : ℕ} → {value value₁ : A} → {t t₁ : bt (Color ∧ A)} → key < key₁ 
+       → RBtreeInvariant (node key₁ ⟪ Black , value₁ ⟫ t t₁) 1
+       → RBtreeInvariant (node key  ⟪ Red ,   value  ⟫ leaf (node key₁ ⟪ Black , value₁ ⟫ t t₁)) 1
+    rb-right-black : {key key₁ : ℕ} → {value value₁ : A} → {t t₁ : bt (Color ∧ A)} → key < key₁ →  {c : Color}
+       → RBtreeInvariant (node key₁ ⟪ c     , value₁ ⟫ t t₁) 1
+       → RBtreeInvariant (node key  ⟪ Black , value  ⟫ leaf (node key₁ ⟪ c , value₁ ⟫ t t₁)) 1
+    rb-left-red : {key key₁ : ℕ} → {value value₁ : A} → {t t₁ : bt (Color ∧ A)} → key < key₁ 
+       → RBtreeInvariant (node key₁ ⟪ Black , value₁ ⟫ t t₁) 1
+       → RBtreeInvariant (node key₁  ⟪ Red ,   value  ⟫ (node key ⟪ Black , value₁ ⟫ t t₁) leaf ) 1
+    rb-left-black : {key key₁ : ℕ} → {value value₁ : A} → {t t₁ : bt (Color ∧ A)} → key < key₁ →  {c : Color}
+       → RBtreeInvariant (node key₁ ⟪ c     , value₁ ⟫ t t₁) 1
+       → RBtreeInvariant (node key₁  ⟪ Black , value  ⟫ (node key ⟪ c , value₁ ⟫ t t₁) leaf) 1
     rb-node-red  : {key key₁ key₂ : ℕ} → {value value₁ value₂ : A} → {t₁ t₂ t₃ t₄ : bt (Color ∧ A)} → key < key₁ → key₁ < key₂ → {d : ℕ}
        → RBtreeInvariant (node key ⟪ Black , value ⟫ t₁ t₂) d
        → RBtreeInvariant (node key₂ ⟪ Black , value₂ ⟫ t₃ t₄) d
@@ -547,6 +547,14 @@
        → RBtreeInvariant (node key₂ ⟪ c₁ , value₂ ⟫ t₃ t₄) d
        → RBtreeInvariant (node key₁ ⟪ Black , value₁ ⟫ (node key ⟪ c , value ⟫ t₁ t₂) (node key₂ ⟪ c₁ , value₂ ⟫ t₃ t₄)) (suc d)
 
+tesr-rb-0 : RBtreeInvariant {_} {ℕ} leaf 0
+tesr-rb-0 = rb-leaf
+
+tesr-rb-1 : RBtreeInvariant {_} {ℕ} (node 10 ⟪ Black , 10 ⟫ leaf leaf) 1
+tesr-rb-1 = rb-single 10 10
+
+tesr-rb-2 : RBtreeInvariant {_} {ℕ} (node 10 ⟪ Red , 10 ⟫ (node 5 ⟪ Black , 5 ⟫ leaf leaf)  leaf) 1
+tesr-rb-2 = rb-left-red (add< _) ( rb-single 10 5)
 
 -- This one can be very difficult
 -- data replacedRBTree  {n : Level} {A : Set n} (key : ℕ) (value : A)  : (before after : bt (Color ∧ A) ) → Set n where
@@ -631,7 +639,7 @@
            →  RBtreeInvariant orig d0 
            →  (stack : List (bt (Color ∧ A)))  → (pg : PG (Color ∧ A) tree stack )
            →  RBtreeInvariant tree ds ∧  RBtreeInvariant (PG.parent pg) dp ∧  RBtreeInvariant (PG.grand pg) dg 
-PGtoRBinvariant = ?
+PGtoRBinvariant = {!!}
 
 findRBT : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree tree0 : bt (Color ∧ A) ) → (stack : List (bt (Color ∧ A))) → {d d0 : ℕ}
            →  RBtreeInvariant tree0 d0 
@@ -639,7 +647,7 @@
            → (next : (tree1 : bt (Color ∧ A)) → (stack : List (bt (Color ∧ A))) → {d1 : ℕ} → RBtreeInvariant tree1 d1 ∧ stackInvariant key tree1 tree0 stack → bt-depth tree1 < bt-depth tree   → t )
            → (exit : (tree1 : bt (Color ∧ A)) → (stack : List (bt (Color ∧ A))) → {d1 : ℕ} → RBtreeInvariant tree1 d1 ∧ stackInvariant key tree1 tree0 stack
                  → (tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key )  → t ) → t
-findRBT = ?
+findRBT = {!!}
 
 rotateLeft : {n m : Level} {A : Set n} {t : Set m}
      → (key : ℕ) → (value : A) → {d0 : ℕ} 
@@ -663,9 +671,9 @@
 rotateLeft {n} {m} {A} {t} key value orig tree rot repl rbo rbt rbr stack si ri rr next exit = rotateLeft1 where
     rotateLeft1 : t
     rotateLeft1 with stackToPG tree orig stack si
-    ... | case1 x = ?
-    ... | case2 (case1 x) = ?
-    ... | case2 (case2 pg) = ?
+    ... | case1 x = exit {!!} {!!} {!!} {!!} rr
+    ... | case2 (case1 x) = {!!}
+    ... | case2 (case2 pg) = {!!}
 
 rotateRight : {n m : Level} {A : Set n} {t : Set m}
      → (key : ℕ) → (value : A) → {d0 : ℕ} 
@@ -689,9 +697,9 @@
 rotateRight {n} {m} {A} {t} key value orig tree rot repl rbo rbt rbr stack si ri rr next exit = rotateRight1 where
     rotateRight1 : t
     rotateRight1 with stackToPG tree orig stack si
-    ... | case1 x = ?
-    ... | case2 (case1 x) = ?
-    ... | case2 (case2 pg) = ?
+    ... | case1 x = {!!}
+    ... | case2 (case1 x) = {!!}
+    ... | case2 (case2 pg) = {!!}
 
 insertCase5 : {n m : Level} {A : Set n} {t : Set m}
      → (key : ℕ) → (value : A) → {d0 : ℕ} 
@@ -715,15 +723,15 @@
 insertCase5 {n} {m} {A} {t} key value orig tree rot repl rbo rbt rbr stack si ri rr next exit = insertCase51 where
     insertCase51 : t
     insertCase51 with stackToPG tree orig stack si
-    ... | case1 eq = ?
-    ... | case2 (case1 eq ) = ?
+    ... | case1 eq = {!!}
+    ... | case2 (case1 eq ) = {!!}
     ... | case2 (case2 pg) with PG.pg pg
-    ... | s2-s1p2 x x₁ = rotateRight ? ? ? ? ? ? ? ? ? ? ? ? ? next exit
+    ... | s2-s1p2 x x₁ = rotateRight {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} next exit
        -- x     : PG.parent pg ≡ node kp vp tree n1
        -- x₁    : PG.grand pg ≡ node kg vg (PG.parent pg) (PG.uncle pg)
-    ... | s2-1sp2 x x₁ = rotateLeft ? ? ? ? ? ? ? ? ? ? ? ? ? next exit
-    ... | s2-s12p x x₁ = rotateLeft ? ? ? ? ? ? ? ? ? ? ? ? ? next exit
-    ... | s2-1s2p x x₁ = rotateLeft ? ? ? ? ? ? ? ? ? ? ? ? ? next exit
+    ... | s2-1sp2 x x₁ = rotateLeft {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} next exit
+    ... | s2-s12p x x₁ = rotateLeft {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} next exit
+    ... | s2-1s2p x x₁ = rotateLeft {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} next exit
     -- = insertCase2 tree (PG.parent pg) (PG.uncle pg) (PG.grand pg) stack si (PG.pg pg) 
 
 
@@ -755,35 +763,35 @@
     insertCase2 tree leaf uncle grand stack si (s2-1sp2 () x₁) 
     insertCase2 tree leaf uncle grand stack si (s2-s12p () x₁) 
     insertCase2 tree leaf uncle grand stack si (s2-1s2p () x₁) 
-    insertCase2 tree parent@(node kp ⟪ Red , _ ⟫ _ _) uncle grand stack si pg = next ? ? ? ? ? ? ? ? ? ? ? ?
-    insertCase2 tree parent@(node kp ⟪ Black , _ ⟫ _ _) leaf grand stack si pg = ?
-    insertCase2 tree parent@(node kp ⟪ Black , _ ⟫ _ _) (node ku ⟪ Red , _ ⟫ _ _ ) grand stack si pg = next ? ? ? ? ? ? ? ? ? ? ? ?
+    insertCase2 tree parent@(node kp ⟪ Red , _ ⟫ _ _) uncle grand stack si pg = next {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!}
+    insertCase2 tree parent@(node kp ⟪ Black , _ ⟫ _ _) leaf grand stack si pg = {!!}
+    insertCase2 tree parent@(node kp ⟪ Black , _ ⟫ _ _) (node ku ⟪ Red , _ ⟫ _ _ ) grand stack si pg = next {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!}
     insertCase2 tree parent@(node kp ⟪ Black , _ ⟫ _ _) (node ku ⟪ Black , _ ⟫ _ _) grand stack si (s2-s1p2 x x₁) = 
-          insertCase5 key value orig tree ? repl rbio ? ? stack si ? ri ? ? next exit
+          insertCase5 key value orig tree {!!} repl rbio {!!} {!!} stack si {!!} ri {!!} {!!} next exit
       -- tree is left of parent, parent is left of grand
       --  node kp ⟪ Black , proj3 ⟫ left right ≡ node kp₁ vp tree n1
       --  grand ≡ node kg vg (node kp ⟪ Black , proj3 ⟫ left right) (node ku ⟪ Black , proj4 ⟫ left₁ right₁)
     insertCase2 tree parent@(node kp ⟪ Black , _ ⟫ _ _) (node ku ⟪ Black , _ ⟫ _ _) grand stack si (s2-1sp2 x x₁) = 
-          rotateLeft key value orig tree ? repl rbio ? ? stack si ? ri ? ? 
-             (λ a b c d e f h i j k l m  → insertCase5 key value a b c d ? ? h i j k l ? ? next exit ) exit
+          rotateLeft key value orig tree {!!} repl rbio {!!} {!!} stack si {!!} ri {!!} {!!} 
+             (λ a b c d e f h i j k l m  → insertCase5 key value a b c d {!!} {!!} h i j k l {!!} {!!} next exit ) exit
       -- tree is right of parent, parent is left of grand  rotateLeft
       --  node kp ⟪ Black , proj3 ⟫ left right ≡ node kp₁ vp n1 tree
       --  grand ≡ node kg vg (node kp ⟪ Black , proj3 ⟫ left right) (node ku ⟪ Black , proj4 ⟫ left₁ right₁)
     insertCase2 tree parent@(node kp ⟪ Black , _ ⟫ _ _) (node ku ⟪ Black , _ ⟫ _ _) grand stack si (s2-s12p x x₁) = 
-          rotateRight key value orig tree ? repl rbio ? ? stack si ? ri ? ? 
-             (λ a b c d e f h i j k l m  → insertCase5 key value a b c d ? ? h i j k l ? ? next exit ) exit
+          rotateRight key value orig tree {!!} repl rbio {!!} {!!} stack si {!!} ri {!!} {!!} 
+             (λ a b c d e f h i j k l m  → insertCase5 key value a b c d {!!} {!!} h i j k l {!!} {!!} next exit ) exit
       -- tree is left of parent, parent is right of grand, rotateRight
       -- node kp ⟪ Black , proj3 ⟫ left right ≡ node kp₁ vp tree n1
       --  grand ≡ node kg vg (node ku ⟪ Black , proj4 ⟫ left₁ right₁) (node kp ⟪ Black , proj3 ⟫ left right)
     insertCase2 tree parent@(node kp ⟪ Black , _ ⟫ _ _) (node ku ⟪ Black , _ ⟫ _ _) grand stack si (s2-1s2p x x₁) = 
-          insertCase5 key value orig tree ? repl rbio ? ? stack si ? ri ? ? next exit
+          insertCase5 key value orig tree {!!} repl rbio {!!} {!!} stack si {!!} ri {!!} {!!} next exit
       -- tree is right of parent, parent is right of grand
       -- node kp ⟪ Black , proj3 ⟫ left right ≡ node kp₁ vp n1 tree
       -- grand ≡ node kg vg (node ku ⟪ Black , proj4 ⟫ left₁ right₁) (node kp ⟪ Black , proj3 ⟫ left right)
     insertCase1 : t
     insertCase1 with stackToPG tree orig stack si
-    ... | case1 eq = ?
-    ... | case2 (case1 eq ) = ?
+    ... | case1 eq = exit repl repl rbir {!!} (subst₂ (λ j k → replacedTree key ⟪ {!!} , value ⟫ j k ) {!!} {!!} r-node )
+    ... | case2 (case1 eq ) = {!!}
     ... | case2 (case2 pg) = insertCase2 tree (PG.parent pg) (PG.uncle pg) (PG.grand pg) stack si (PG.pg pg)