# HG changeset patch # User Shinji KONO # Date 1575604913 -32400 # Node ID 37f5826ca7d2c984dc8521ddeace7a093391506d # Parent 8627d35d4bffa5a7ce3306b82bac6d15bbaf1b61 minor fix diff -r 8627d35d4bff -r 37f5826ca7d2 hoareBinaryTree.agda --- a/hoareBinaryTree.agda Thu Dec 05 20:38:54 2019 +0900 +++ b/hoareBinaryTree.agda Fri Dec 06 13:01:53 2019 +0900 @@ -75,13 +75,15 @@ 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' : {n m : Level} {A : Set n} {t : Set m} {tn : ℕ} → (key : ℕ) → (tree : bt' A tn ) → List (bt'-path A ) + → ( {key1 : ℕ } → bt' A key1 → List (bt'-path A ) → t ) → t +bt-find' key tr@(bt'-leaf key₁) stack next = next tr stack -- no key found 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-find' key tr@(bt'-node {l} {r} key₁ value tree tree₁ x x₁) stack next | tri< a ¬b ¬c = + bt-find' key tree ( (bt'-left key {key₁} tr a ) ∷ stack) next +bt-find' key found@(bt'-node key₁ value tree tree₁ x x₁) stack next | tri≈ ¬a b ¬c = next found stack +bt-find' key tr@(bt'-node key₁ value tree tree₁ x x₁) stack next | tri> ¬a ¬b c = + bt-find' key tree ( (bt'-right key {key₁} tr c ) ∷ stack) next 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 diff -r 8627d35d4bff -r 37f5826ca7d2 hoareRedBlackTree.agda --- a/hoareRedBlackTree.agda Thu Dec 05 20:38:54 2019 +0900 +++ b/hoareRedBlackTree.agda Fri Dec 06 13:01:53 2019 +0900 @@ -617,43 +617,27 @@ findNodeRight x [] = (left x ≡ nothing ) ∧ (right x ≡ nothing ) findNodeRight {n} x (h ∷ t) = Lift n ((key x) > (key h)) +data FindNodeInvariant {n : Level } {a : Set n} : (t : SingleLinkedStack (Node a)) (node : Maybe (Node a) ) → Set n where + fni-stackEmpty : (now : Maybe (Node a) ) → FindNodeInvariant [] now + fni-treeEmpty : (st : SingleLinkedStack (Node a)) → FindNodeInvariant st nothing + fni-Left : (x : Node a) (st : SingleLinkedStack (Node a)) (node : Maybe (Node a )) + → FindNodeInvariant ( x ∷ st ) node → findNodeLeft x st → FindNodeInvariant st node + fni-Right : (x : Node a) (st : SingleLinkedStack (Node a)) (node : Maybe (Node a )) + → FindNodeInvariant ( x ∷ st ) node → findNodeRight x st → FindNodeInvariant st node findNodeLoop : {n : Level } {a : Set n} (r : Node a ) (t : SingleLinkedStack (Node a)) → Set n findNodeLoop x st = ((findNodeRight x st) ∨ (findNodeLeft x st)) - - -data FindNodeInvariant {n : Level } {a : Set n} : (t : SingleLinkedStack (Node a)) (original : RedBlackTree {n} a ) → Set n where - fni-stackEmpty : (now : RedBlackTree {n} a ) → FindNodeInvariant [] now - fni-treeEmpty : (st : SingleLinkedStack (Node a)) → FindNodeInvariant st record { root = nothing ; nodeStack = st } - fni-Left : (x : Node a) (st : SingleLinkedStack (Node a)) (original : RedBlackTree {n} a ) - → FindNodeInvariant ( x ∷ st ) original → findNodeLeft x st → FindNodeInvariant st original - fni-Right : (x : Node a) (st : SingleLinkedStack (Node a)) (original : RedBlackTree {n} a ) - → FindNodeInvariant ( x ∷ st ) original → findNodeRight x st → FindNodeInvariant st original - -- fni-loop : (x : Node a) (st : SingleLinkedStack (Node a)) (original : RedBlackTree {n} a ) → FindNodeInvariant st original - - --- findNode1h : {n m : Level } {a : Set n} {t : Set m} → (tree : RedBlackTree {n} a ) → (Node a ) --- → ((new : RedBlackTree {n} a) → FindNodeInvariant (nodeStack new) tree → t ) --- → ( FindNodeInvariant (nodeStack tree) tree) → t --- findNode1h {n} {m} {a} {t} tree n0 next prev = findNode2h (root tree) (nodeStack tree) n0 prev --- module FindNodeH where --- findNode2h : (Maybe (Node a )) → (s : SingleLinkedStack (Node a )) → Node a → FindNodeInvariant s tree → t --- findNode2h nothing st n0 prev = next record { root = nothing ; nodeStack = st } prev --- findNode2h (just x) st n0 prev with <-cmp (key n0) (key x) --- ... | tri≈ ¬lt eq ¬gt = next (record {root = just x ; nodeStack = st }) prev -- ( fni-Last ? ) --- ... | tri< lt ¬eq ¬gt = pushSingleLinkedStack st x (λ s1 → findNode2h (left x) s1 n0 (fni-Left x s1 tree ({!!}) (lproof x s1 )) ) --- b where --- nextInvaliant : (t) --- nextInvaliant = next tree {!!} --- lproof : (x : Node a) → (s1 : SingleLinkedStack (Node a)) → findNodeLeft x s1 --→ (n0 : Node a) --- lproof ns [] with left ns | right ns --- lproof ns [] | just x | just x₁ = {!!} --- lproof ns [] | just x | nothing = {!!} --- lproof ns [] | nothing | just x = {!!} --- lproof ns [] | nothing | nothing = record { proj1 = refl ; proj2 = refl } --- lproof ns (x ∷ ss) = {!!} - --- ... | tri> ¬lt ¬eq gt = pushSingleLinkedStack st x (λ s1 → findNode2h (right x) s1 n0 (fni-Right x s1 tree ({!!}) {!!}) ) +findNode1h : {n m : Level } {a : Set n} {t : Set m} → (tree : RedBlackTree {n} a ) → (Node a ) + → ((new : RedBlackTree {n} a) → FindNodeInvariant (nodeStack new) (root new ) → t ) + → ( FindNodeInvariant (nodeStack tree) (root tree) ) → t +findNode1h {n} {m} {a} {t} tree n0 next prev = findNode2h (root tree) (nodeStack tree) prev + module FindNodeH where + findNode2h : (new : Maybe (Node a )) → (s : SingleLinkedStack (Node a )) → FindNodeInvariant s new → t + findNode2h nothing st prev = next record { root = nothing ; nodeStack = st } prev + findNode2h (just x) st prev with <-cmp (key n0) (key x) + ... | tri≈ ¬a b ¬c = next (record {root = just x ; nodeStack = st }) prev + ... | tri< a ¬b ¬c = pushSingleLinkedStack st x (λ s1 → findNode2h (right x) s1 (fni-Left x s1 {!!} {!!} {!!}) ) + ... | tri> ¬a ¬b c = pushSingleLinkedStack st x (λ s1 → findNode2h (left x) s1 (fni-Right x s1 {!!} {!!} {!!}) ) -- replaceNodeH : {n m : Level } {a : Set n} {t : Set m} → RedBlackTree {n} a → (Node a ) → (RedBlackTree {n} a → {!!} → t) → {!!} → t