Mercurial > hg > Gears > GearsAgda

changeset 770:a4bc901bba36

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
RBI record
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 08 May 2023 12:59:13 +0900
parents ce0d41a84c2b
children feb3553ef88c
files hoareBinaryTree1.agda
diffstat 1 files changed, 24 insertions(+), 6 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Sun May 07 20:19:18 2023 +0900
+++ b/hoareBinaryTree1.agda	Mon May 08 12:59:13 2023 +0900
@@ -611,18 +611,22 @@
        rest : List (bt A)
        stack=gp : stack ≡ ( self ∷ parent ∷ grand ∷ rest )
 
-record RBI {n : Level} {A : Set n} (key : ℕ) (value : A) (tree repl : bt (Color ∧ A) ) (stack : List (bt (Color ∧ A))) (C : bt (Color ∧ A) → bt (Color ∧ A) → List (bt (Color ∧ A)) → Set n) : Set n where
+record RBI {n : Level} {A : Set n} (key : ℕ) (value : A) (orig : bt (Color ∧ A) ) (stack : List (bt (Color ∧ A)))  : Set n where
    field
      d rd : ℕ
-     tree0 rot : bt (Color ∧ A)
-     tree0rb : RBtreeInvariant tree0 d
+     tree rot repl : bt (Color ∧ A)
+     treerb : RBtreeInvariant tree d
      replrb : RBtreeInvariant repl rd
      d=rd : ( d ≡ rd ) ∨ ( suc d ≡ rd )
+     si : stackInvariant key tree orig stack
      rotated : rotatedTree tree rot
-     si : stackInvariant key tree tree0 stack
      ri : replacedRBTree key value (child-replaced key rot ) repl
-     ci : C tree repl stack     -- data continuation
    
+rbi-case1 : {n : Level} {A : Set n} → {key : ℕ} → {value : A} → (tree orig : bt (Color ∧ A) )
+           →  (stack : List (bt (Color ∧ A))) 
+           →  stack ≡ tree ∷ orig ∷ [] → RBI key value orig stack → RBI key value orig (orig ∷ [])
+rbi-case1 {n} {A} {key} {value} tree orig stack eq rbi = ?
+
 stackToPG : {n : Level} {A : Set n} → {key : ℕ } → (tree orig : bt A )
            →  (stack : List (bt A)) → stackInvariant key tree orig stack
            → ( stack ≡ orig ∷ [] ) ∨ ( stack ≡ tree ∷ orig ∷ [] ) ∨ PG A tree stack
@@ -763,6 +767,20 @@
 
 replaceRBP : {n m : Level} {A : Set n} {t : Set m}
      → (key : ℕ) → (value : A) 
+     → (orig : bt (Color ∧ A)) 
+     → (stack : List (bt (Color ∧ A))) 
+     → (r : RBI key value orig stack )
+     → (next : (stack1 : List (bt (Color ∧ A))) 
+        → (r : RBI key value orig stack1 ) 
+        → length stack1 < length stack  → t )
+     → (exit : (repl : bt (Color ∧ A) ) → (stack1 : List (bt (Color ∧ A)))
+        →  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 
@@ -780,7 +798,7 @@
      → (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 tree rot repl rbio rbit rbir stack si roti ri 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