Members/Moririn: hoareBinaryTree1.agda comparison

comparison hoareBinaryTree1.agda @ 766:bc9063c6fef3

...

author	Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date	Sat, 06 May 2023 21:33:42 +0900
parents	292aaf8e3b0f
children	9cdf272ca38c

comparison

equal deleted inserted replaced

-:292aaf8e3b0f
+:bc9063c6fef3
 → 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 : ℕ}
+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
 → RBtreeInvariant (node key₁ ⟪ Red , value₁ ⟫ (node key ⟪ Black , value ⟫ t₁ t₂) (node key₂ ⟪ Black , value₂ ⟫ t₃ t₄)) d
-rb-node-black  : {key key₁ key₂ : ℕ} → {value value₁ value₂ : A} → {t₁ t₂ t₃ t₄ : bt (Color ∧ A)} → key < key₁ → key₁ < key₂ → {d : ℕ}
+rb-node-black  : {key key₁ key₂ : ℕ} → {value value₁ value₂ : A} → {t₁ t₂ t₃ t₄ : bt (Color ∧ A)} → key < key₁ → key₁ < key₂ → (d : ℕ)
 → {c c₁ : Color}
 → RBtreeInvariant (node key  ⟪ c  , value  ⟫ t₁ t₂) d
 → 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)
 → (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
-→ {c : Color} → replacedTree key ⟪ c , value ⟫ (child-replaced key rot) repl
+→ 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
-→ {c : Color} → replacedTree key ⟪ c , value ⟫ (child-replaced key rot) rr
+→ replacedRBTree key value (child-replaced key rot) rr
 → length stack1 < length stack  → t )
 → (exit : {k1 d1 : ℕ} {c1 : Color} → (rot repl : bt (Color ∧ A) )
 →  {d : ℕ} → RBtreeInvariant repl d
-→ (ri : rotatedTree orig rot ) → {c : Color} → replacedTree key ⟪ c , value ⟫ rot repl → t ) → t
+→ (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
 rotateLeft1 : t
 rotateLeft1 with stackToPG tree orig stack si
 ... | case1 x = exit {!!} {!!} {!!} {!!} rr
 ... | case2 (case1 x) = {!!}
 → (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
-→ {c : Color} → replacedTree key ⟪ c , value ⟫ (child-replaced key rot) repl
+→ 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
-→ {c : Color} → replacedTree key ⟪ c , value ⟫ (child-replaced key rot) rr
+→ replacedRBTree key value  (child-replaced key rot) rr
 → length stack1 < length stack  → t )
 → (exit : {k1 d1 : ℕ} {c1 : Color} → (rot repl : bt (Color ∧ A) )
 →  {d : ℕ} → RBtreeInvariant repl d
-→ (ri : rotatedTree orig rot ) → {c : Color} → replacedTree key ⟪ c , value ⟫ rot repl → t ) → t
+→ (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
 rotateRight1 : t
 rotateRight1 with stackToPG tree orig stack si
 ... | case1 x = {!!}
 ... | case2 (case1 x) = {!!}
 → (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
-→ {c : Color} → replacedTree key ⟪ c , value ⟫ (child-replaced key rot) repl
+→ 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
-→ {c : Color} → replacedTree key ⟪ c , value ⟫ (child-replaced key rot) rr
+→ replacedRBTree key value  (child-replaced key rot) rr
 → length stack1 < length stack  → t )
 → (exit : {k1 d1 : ℕ} {c1 : Color} → (rot repl : bt (Color ∧ A) )
 →  {d : ℕ} → RBtreeInvariant repl d
-→ (ri : rotatedTree orig rot ) → {c : Color} → replacedTree key ⟪ c , value ⟫ rot repl → t ) → t
+→ (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
 insertCase51 : t
 insertCase51 with stackToPG tree orig stack si
 ... | case1 eq = {!!}
 ... | case2 (case1 eq ) = {!!}
 → (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
-→ {c : Color} → replacedTree key ⟪ c , value ⟫ (child-replaced key rot) rr
+→ 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
-→ {c : Color} → replacedTree key ⟪ c , value ⟫ (child-replaced key rot) rr
+→ 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 ) → {c : Color} → replacedTree key ⟪ c , value ⟫ (child-replaced key rot) repl → t ) → t
+→ (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 {c} 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
 insertCase2 tree leaf uncle grand stack si (s2-s1p2 () x₁)
 insertCase2 tree leaf uncle grand stack si (s2-1sp2 () x₁)
 insertCase12 : (to : bt (Color ∧ A)) → {d : ℕ} → RBtreeInvariant to d  → to ≡ orig
 → {stack : List (bt (Color ∧ A))} → (si : stackInvariant key tree to stack )
 → stack ≡ tree ∷ to ∷ [] → t
 insertCase12 (node k1 ⟪ Red , v1 ⟫ leaf (node k2 ⟪ Black , v2 ⟫ t1 t2)) (rb-right-red x₁ ro) eq (s-right x s-nil) refl = ?
 insertCase12 (node k1 ⟪ Red , v1 ⟫ (node k2 ⟪ Black , v2 ⟫ t1 t2) leaf) (rb-left-red x₁ ro) eq (s-right x s-nil) refl = ?
-insertCase12 (node k1 ⟪ Red , v1 ⟫ (node k2 ⟪ Black , v2 ⟫ t1 t2) (node k3 ⟪ Black , v3 ⟫ t3 t4)) (rb-node-red x₁ x₂ ro ro₁) refl (s-right x s-nil) refl = exit rot1 repl1 ? ins13 ins12 where
+insertCase12 (node k1 ⟪ Red , v1 ⟫ (node k2 ⟪ Black , v2 ⟫ t1 t2) (node k3 ⟪ Black , v3 ⟫ t3 t4)) (rb-node-red x₁ x₂ d ro ro₁) refl (s-right x s-nil) refl = exit rot1 repl1 rrb ins13 ins12 where
 rot1 : bt (Color ∧ A)
 rot1 = node k1 ⟪ Red , v1 ⟫ (node k2 ⟪ Black , v2 ⟫ t1 t2) (node k3 ⟪ Black , v3 ⟫ t3 t4)
 repl1 : bt (Color ∧ A)
-repl1 = ?
+repl1 = node k1 ⟪ Red , v1 ⟫ (node k2 ⟪ Black , v2 ⟫ t1 t2) repl
-ins12 : replacedTree key ⟪ ? , value ⟫ (child-replaced key rot1) repl1
+ins12 : replacedRBTree key value  (child-replaced key rot1) repl1
 ins12 = ?
 ins13 : rotatedTree (node k1 ⟪ Red , v1 ⟫ (node k2 ⟪ Black , v2 ⟫ t1 t2) (node k3 ⟪ Black , v3 ⟫ t3 t4)) rot1
 ins13 = rr-node
+rrb : RBtreeInvariant repl1 d
+rrb with repl | rbir
+... | r1 | r2 = ?
+-- -subst (λ k → RBtreeInvariant k d ) ? (rb-node-red ? ? d ro (subst₂ (λ j k → RBtreeInvariant j k) ? ? rbir ))
 -- exit (node k1 ⟪ Red , v1 ⟫ t1 rot) (node k1 ⟪ Black , v1 ⟫ ? ?) (rb-node-black ? ? ? ?)
 --   (subst₂ (λ j k → rotatedTree j k ) eq ? (rr-right ? rr-node rr-node roti))
---   (subst (λ k → replacedTree key ⟪ ? , value ⟫ ? ?) ? (r-right ? ri))
+--   (subst (λ k → replacedRBTree key value  ? ?) ? (r-right ? ri))
 -- k1 < key
 --     ⟪ red , k1 ⟫
 --   t1            tree → rot → repl
 insertCase12 (node k1 ⟪ Black , v1 ⟫ leaf leaf) (rb-single k1 v1) eq (s-right x s-nil) refl = ?
 insertCase12 (node k1 ⟪ Black , v1 ⟫ leaf (node _ ⟪ _ , _ ⟫ _ _)) (rb-right-black x₁ ro) eq (s-right x s-nil) refl = ?
 insertCase12 (node k1 ⟪ Black , v1 ⟫ (node _ ⟪ _ , _ ⟫ _ _) leaf) (rb-left-black x₁ ro) eq (s-right x s-nil) refl = ?
-insertCase12 (node k1 ⟪ Black , v1 ⟫ (node _ ⟪ _ , _ ⟫ _ _) (node _ ⟪ _ , _ ⟫ _ _)) (rb-node-black x₁ x₂ ro ro₁) eq (s-right x s-nil) refl = ?
+insertCase12 (node k1 ⟪ Black , v1 ⟫ (node _ ⟪ _ , _ ⟫ _ _) (node _ ⟪ _ , _ ⟫ _ _)) (rb-node-black x₁ x₂ d1 ro ro₁) eq (s-right x s-nil) refl = ?
 insertCase12 (node k1 ⟪ Red , v1 ⟫ leaf (node _ ⟪ Black , _ ⟫ _ _)) (rb-right-red x₁ ro) eq (s-left x s-nil) refl = ?
 insertCase12 (node k1 ⟪ Red , v1 ⟫ (node _ ⟪ Black , _ ⟫ _ _) leaf) (rb-left-red x₁ ro) eq (s-left x s-nil) refl = ?
-insertCase12 (node k1 ⟪ Red , v1 ⟫ (node _ ⟪ Black , _ ⟫ _ _) (node _ ⟪ Black , _ ⟫ _ _)) (rb-node-red x₁ x₂ ro ro₁) eq (s-left x s-nil) refl = ?
+insertCase12 (node k1 ⟪ Red , v1 ⟫ (node _ ⟪ Black , _ ⟫ _ _) (node _ ⟪ Black , _ ⟫ _ _)) (rb-node-red x₁ x₂ d1 ro ro₁) eq (s-left x s-nil) refl = ?
 insertCase12 (node k1 ⟪ Black , v1 ⟫ leaf leaf) (rb-single k1 v1) eq (s-left x s-nil) refl = ?
 insertCase12 (node k1 ⟪ Black , v1 ⟫ leaf (node _ ⟪ _ , _ ⟫ _ _)) (rb-right-black x₁ ro) eq (s-left x s-nil) refl = ?
 insertCase12 (node k1 ⟪ Black , v1 ⟫ (node _ ⟪ _ , _ ⟫ _ _) leaf) (rb-left-black x₁ ro) eq (s-left x s-nil) refl = ?
-insertCase12 (node k1 ⟪ Black , v1 ⟫ (node _ ⟪ _ , _ ⟫ _ _) (node _ ⟪ _ , _ ⟫ _ _)) (rb-node-black x₁ x₂ ro ro₁) eq (s-left x s-nil) refl = ?
+insertCase12 (node k1 ⟪ Black , v1 ⟫ (node _ ⟪ _ , _ ⟫ _ _) (node _ ⟪ _ , _ ⟫ _ _)) (rb-node-black x₁ x₂ d1 ro ro₁) eq (s-left x s-nil) refl = ?
 -- exit rot repl rbir ? ?
 ... | case2 (case2 pg) = insertCase2 tree (PG.parent pg) (PG.uncle pg) (PG.grand pg) stack si (PG.pg pg)

Mercurial > hg > Members > Moririn

comparison hoareBinaryTree1.agda @ 766:bc9063c6fef3