Mercurial > hg > Members > Moririn

changeset 775:fb74ba4fa38e

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 Thu, 11 May 2023 17:52:58 +0900
parents ebd8a73543dd
children 576b35b1d2d7
files hoareBinaryTree1.agda
diffstat 1 files changed, 67 insertions(+), 110 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Tue May 09 23:17:54 2023 +0900
+++ b/hoareBinaryTree1.agda	Thu May 11 17:52:58 2023 +0900
@@ -615,10 +615,10 @@
        rest : List (bt A)
        stack=gp : stack ≡ ( self ∷ parent ∷ grand ∷ rest )
 
-record RBI {n : Level} {A : Set n} (key : ℕ) (value : A) (orig : bt (Color ∧ A) ) (stack : List (bt (Color ∧ A)))  : Set n where
+record RBI {n : Level} {A : Set n} (key : ℕ) (value : A) (orig repl : bt (Color ∧ A) ) (stack : List (bt (Color ∧ A)))  : Set n where
    field
        od d rd : ℕ
-       tree rot repl : bt (Color ∧ A)
+       tree rot : bt (Color ∧ A)
        origti : treeInvariant orig 
        origrb : RBtreeInvariant orig od
        treerb : RBtreeInvariant tree d
@@ -731,97 +731,74 @@
            →  RBtreeInvariant tree ds ∧  RBtreeInvariant (PG.parent pg) dp ∧  RBtreeInvariant (PG.grand pg) dg 
 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 
-           →  RBtreeInvariant tree d ∧ stackInvariant key tree tree0 stack  
-           → (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 : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree : bt (Color ∧ A) ) 
+           → {d : ℕ} →  RBtreeInvariant tree d 
+           → (exit : (current : bt (Color ∧ A)) → (stack : List (bt (Color ∧ A))) 
+               → RBI key value tree current stack → t ) → t
 findRBT = {!!}
 
 rotateLeft : {n m : Level} {A : Set n} {t : Set m}
-     → (key : ℕ) → (value : A) → {d0 : ℕ} 
-     → (orig tree rot repl : bt (Color ∧ A)) {d0 : ℕ}
-     →  RBtreeInvariant orig d0 
-     →  {d : ℕ} → RBtreeInvariant tree d →  {dr : ℕ} → RBtreeInvariant repl dr 
-     → (stack : List (bt (Color ∧ A))) → (si : stackInvariant key tree orig stack ) 
-     → rotatedTree tree rot
-     → replacedRBTree key value  (child-replaced key rot) repl
-     → (next : {key2 d2 : ℕ} {c2 : Color} 
-        → (to tr rot rr : bt (Color ∧ A)) 
-        →  RBtreeInvariant orig d0 
-        →  {d : ℕ} → RBtreeInvariant tree d →  {dr : ℕ} → RBtreeInvariant rr dr 
-        → (stack1 : List (bt (Color ∧ A))) → stackInvariant key tr to stack1 
-        → rotatedTree tr rot
-        → replacedRBTree key value (child-replaced key rot) rr
+     → (key : ℕ) → (value : A) 
+     → (orig tree : bt (Color ∧ A)) 
+     → (stack : List (bt (Color ∧ A))) 
+     → (r : RBI key value orig tree stack )
+     → (next : (tree1 (bt (Color ∧ A))) → (stack1 : List (bt (Color ∧ A))) 
+        → (r : RBI key value orig current stack1 ) 
         → length stack1 < length stack  → t )
-     → (exit : {k1 d1 : ℕ} {c1 : Color} → (rot repl : bt (Color ∧ A) )
-        →  {d : ℕ} → RBtreeInvariant repl d 
-        → (ri : rotatedTree orig rot ) → replacedRBTree key  value rot repl → t ) → t
-rotateLeft {n} {m} {A} {t} key value orig tree rot repl rbo rbt rbr stack si ri rr next exit = rotateLeft1 where
+     → (exit : (repl : bt (Color ∧ A) ) → (stack1 : List (bt (Color ∧ A)))
+        →  stack1 ≡ (orig ∷ [])
+        →  RBI key value orig repl stack1
+        → t ) → t
+rotateLeft {n} {m} {A} {t} key value = ? where
     rotateLeft1 : t
-    rotateLeft1 with stackToPG tree orig stack si
+    rotateLeft1 with stackToPG ? orig stack si
     ... | case1 x = exit {!!} {!!} {!!} {!!} rr
     ... | case2 (case1 x) = {!!}
     ... | case2 (case2 pg) = {!!}
 
 rotateRight : {n m : Level} {A : Set n} {t : Set m}
-     → (key : ℕ) → (value : A) → {d0 : ℕ} 
-     → (orig tree rot repl : bt (Color ∧ A)) {d0 : ℕ}
-     →  RBtreeInvariant orig d0 
-     →  {d : ℕ} → RBtreeInvariant tree d →  {dr : ℕ} → RBtreeInvariant repl dr 
-     → (stack : List (bt (Color ∧ A))) → (si : stackInvariant key tree orig stack ) 
-     → rotatedTree tree rot
-     → replacedRBTree key value  (child-replaced key rot) repl
-     → (next : {key2 d2 : ℕ} {c2 : Color}  
-        → (to tr rot rr : bt (Color ∧ A)) 
-        →  RBtreeInvariant orig d0 
-        →  {d : ℕ} → RBtreeInvariant tree d →  {dr : ℕ} → RBtreeInvariant rr dr 
-        → (stack1 : List (bt (Color ∧ A))) → stackInvariant key tr to stack1 
-        → rotatedTree tr rot
-        → replacedRBTree key value  (child-replaced key rot) rr
+     → (key : ℕ) → (value : A) 
+     → (orig tree : bt (Color ∧ A)) 
+     → (stack : List (bt (Color ∧ A))) 
+     → (r : RBI key value orig tree stack )
+     → (next : (stack1 : List (bt (Color ∧ A))) 
+        → (r : RBI key value orig stack1 ) 
         → length stack1 < length stack  → t )
-     → (exit : {k1 d1 : ℕ} {c1 : Color} → (rot repl : bt (Color ∧ A) )
-        →  {d : ℕ} → RBtreeInvariant repl d 
-        → (ri : rotatedTree orig rot ) → replacedRBTree key value  rot repl → t ) → t
-rotateRight {n} {m} {A} {t} key value orig tree rot repl rbo rbt rbr stack si ri rr next exit = rotateRight1 where
+     → (exit : (repl : bt (Color ∧ A) ) → (stack1 : List (bt (Color ∧ A)))
+        →  stack1 ≡ (orig ∷ [])
+        →  RBI key value orig repl stack1
+        → t ) → t
+rotateRight {n} {m} {A} {t} key value = ? where
     rotateRight1 : t
-    rotateRight1 with stackToPG tree orig stack si
+    rotateRight1 with stackToPG ? ? ? ?
     ... | case1 x = {!!}
     ... | case2 (case1 x) = {!!}
     ... | case2 (case2 pg) = {!!}
 
 insertCase5 : {n m : Level} {A : Set n} {t : Set m}
-     → (key : ℕ) → (value : A) → {d0 : ℕ} 
-     → (orig tree rot repl : bt (Color ∧ A)) {d0 : ℕ}
-     →  RBtreeInvariant orig d0 
-     →  {d : ℕ} → RBtreeInvariant tree d →  {dr : ℕ} → RBtreeInvariant repl dr 
-     → (stack : List (bt (Color ∧ A))) → (si : stackInvariant key tree orig stack ) 
-     → rotatedTree tree rot
-     → replacedRBTree key value  (child-replaced key rot) repl
-     → (next : {key2 d2 : ℕ} {c2 : Color}   
-        → (to tr rot rr : bt (Color ∧ A)) 
-        →  RBtreeInvariant orig d0 
-        →  {d : ℕ} → RBtreeInvariant tree d →  {dr : ℕ} → RBtreeInvariant rr dr 
-        → (stack1 : List (bt (Color ∧ A))) → stackInvariant key tr to stack1 
-        → rotatedTree tr rot
-        → replacedRBTree key value  (child-replaced key rot) rr
+     → (key : ℕ) → (value : A) 
+     → (orig tree : bt (Color ∧ A)) 
+     → (stack : List (bt (Color ∧ A))) 
+     → (r : RBI key value orig tree stack )
+     → (next : (tree1 (bt (Color ∧ A)))  (stack1 : List (bt (Color ∧ A))) 
+        → (r : RBI key value orig tree1 stack1 ) 
         → length stack1 < length stack  → t )
-     → (exit : {k1 d1 : ℕ} {c1 : Color} → (rot repl : bt (Color ∧ A) )
-        →  {d : ℕ} → RBtreeInvariant repl d 
-        → (ri : rotatedTree orig rot ) → replacedRBTree key value  rot repl → t ) → t
-insertCase5 {n} {m} {A} {t} key value orig tree rot repl rbo rbt rbr stack si ri rr next exit = insertCase51 where
+     → (exit : (repl : bt (Color ∧ A) ) → (stack1 : List (bt (Color ∧ A)))
+        →  stack1 ≡ (orig ∷ [])
+        →  RBI key value orig repl stack1
+        → t ) → t
+insertCase5 {n} {m} {A} {t} key value = ? where
     insertCase51 : t
-    insertCase51 with stackToPG tree orig stack si
+    insertCase51 with stackToPG ? orig stack ?
     ... | 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) 
 
 
@@ -829,7 +806,7 @@
 
 replaceRBP : {n m : Level} {A : Set n} {t : Set m}
      → (key : ℕ) → (value : A) 
-     → (orig : bt (Color ∧ A)) 
+     → (orig repl : bt (Color ∧ A)) 
      → (stack : List (bt (Color ∧ A))) 
      → (r : RBI key value orig stack )
      → (next : (stack1 : List (bt (Color ∧ A))) 
@@ -839,28 +816,7 @@
         →  stack1 ≡ (orig ∷ [])
         →  RBI key value orig stack1
         → t ) → t
-replaceRBP = ?
-
-replaceRBP' : {n m : Level} {A : Set n} {t : Set m}
-     → (key : ℕ) → (value : A) 
-     → (to tr rot rr : bt (Color ∧ A)) 
-     →  {d0 : ℕ} → RBtreeInvariant to d0 
-     →  {d  : ℕ} → RBtreeInvariant tr d →  {dr : ℕ} → RBtreeInvariant rr dr 
-     → (stack : List (bt (Color ∧ A))) → stackInvariant key tr to stack
-     → rotatedTree tr rot
-     → replacedRBTree key value  (child-replaced key rot) rr
-     → (next : {key2 d2 : ℕ} {c2 : Color}   
-        → (to tr rot rr : bt (Color ∧ A)) 
-        →  RBtreeInvariant to d0 
-        →  {d : ℕ} → RBtreeInvariant tr d →  {dr : ℕ} → RBtreeInvariant rr dr 
-        → (stack1 : List (bt (Color ∧ A))) → stackInvariant key tr to stack1 
-        → rotatedTree tr rot
-        → replacedRBTree key  value  (child-replaced key rot) rr
-        → length stack1 < length stack  → t )
-     → (exit : (rot repl : bt (Color ∧ A) )
-        →  {d : ℕ} → RBtreeInvariant repl d 
-        → (ri : rotatedTree to rot ) → replacedRBTree key  value  (child-replaced key rot) repl → t ) → t
-replaceRBP' {n} {m} {A} {t} key value orig tree rot repl rbio rbit rbir stack si roti ri next exit = ? where
+replaceRBP {n} {m} {A} {t} key value orig stack r next exit = ? where
     insertCase2 : (tree parent uncle grand : bt (Color ∧ A)) 
       → (stack : List (bt (Color ∧ A))) → (si : stackInvariant key tree orig stack ) 
       → (pg : ParentGrand tree parent uncle grand ) → t
@@ -868,41 +824,42 @@
     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 ⟪ 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
+    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 {!!} 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
+    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
       -- 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
+    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
       -- 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
+    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
       -- 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 = exit rot repl rbir (subst (λ k → rotatedTree k rot) (stackCase1 si eq) roti) ri 
+    insertCase1 with stackToPG ? orig stack ?
+    ... | case1 eq = ? -- exit rot repl rbir (subst (λ k → rotatedTree k rot) (stackCase1 si eq) roti) ri 
     ... | case2 (case1 eq ) = ? where
         insertCase12 : (to : bt (Color ∧ A)) → {d : ℕ} → RBtreeInvariant orig d  → to ≡ orig
-          → (rr : bt (Color ∧ A)) → {dr : ℕ} → RBtreeInvariant repl dr  → rr ≡ repl
-          → {stack : List (bt (Color ∧ A))} → (si : stackInvariant key tree to stack ) 
-          → stack ≡ tree ∷ to ∷ [] → t
+          → (rr : bt (Color ∧ A)) → {dr : ℕ} → RBtreeInvariant ? dr  → rr ≡ ?
+          → {stack : List (bt (Color ∧ A))} → (si : stackInvariant key ? to stack ) 
+          → stack ≡ ? ∷ to ∷ [] → t
         insertCase12 = ?
     -- exit rot repl rbir ? ? 
-    ... | case2 (case2 pg) = insertCase2 tree (PG.parent pg) (PG.uncle pg) (PG.grand pg) stack si (PG.pg pg) 
+    ... | case2 (case2 pg) = ? -- insertCase2 tree (PG.parent pg) (PG.uncle pg) (PG.grand pg) stack si (PG.pg pg) 
 
 
+