Mercurial > hg > Gears > GearsAgda
changeset 829:2a19292edd88
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 05 Mar 2024 14:23:33 +0900 |
| parents | c9850c226195 |
| children | 1cce147edddb |
| files | hoareBinaryTree1.agda |
| diffstat | 1 files changed, 24 insertions(+), 24 deletions(-) [+] |
line wrap: on
line diff
--- a/hoareBinaryTree1.agda Thu Feb 29 17:35:40 2024 +0900 +++ b/hoareBinaryTree1.agda Tue Mar 05 14:23:33 2024 +0900 @@ -502,9 +502,9 @@ RTtoTI0 .(node key _ (node _ _ _ _) leaf) .(node key value (node _ _ _ _) leaf) key value (t-left x a b ti) r-node = t-left x a b ti RTtoTI0 .(node key _ (node _ _ _ _) (node _ _ _ _)) .(node key value (node _ _ _ _) (node _ _ _ _)) key value (t-node x x₁ a b c d ti ti₁) r-node = t-node x x₁ a b c d ti ti₁ -- r-right case -RTtoTI0 (node _ _ leaf leaf) (node _ _ leaf .(node key value leaf leaf)) key value (t-single _ _) (r-right x r-leaf) = t-right x ? ? (t-single key value) +RTtoTI0 (node _ _ leaf leaf) (node _ _ leaf .(node key value leaf leaf)) key value (t-single _ _) (r-right x r-leaf) = t-right x _ _ (t-single key value) RTtoTI0 (node _ _ leaf right@(node _ _ _ _)) (node key₁ value₁ leaf leaf) key value (t-right x₁ a b ti) (r-right x ri) = t-single key₁ value₁ -RTtoTI0 (node key₁ _ leaf right@(node key₂ _ _ _)) (node key₁ value₁ leaf right₁@(node key₃ _ _ _)) key value (t-right x₁ a b ti) (r-right x ri) = +RTtoTI0 (node key₁ _ leaf right@(node key₂ _ left₁ right₁)) (node key₁ value₁ leaf right₃@(node key₃ _ left₂ right₂)) key value (t-right x₁ a b ti) (r-right x ri) = t-right (subst (λ k → key₁ < k ) (rt-property-key ri) x₁) ? ? (RTtoTI0 _ _ key value ti ri) RTtoTI0 (node key₁ _ (node _ _ _ _) leaf) (node key₁ _ (node key₃ value left right) leaf) key value₁ (t-left x₁ a b ti) (r-right x ()) RTtoTI0 (node key₁ _ (node key₃ _ _ _) leaf) (node key₁ _ (node key₃ value₃ _ _) (node key value leaf leaf)) key value (t-left x₁ a b ti) (r-right x r-leaf) = @@ -518,27 +518,27 @@ t-left (subst (λ k → k < key₃ ) (rt-property-key ri) x₁) ? ? (RTtoTI0 _ _ key value ti ri) -- key₁ < key₃ RTtoTI0 (node key₁ _ (node key₂ _ _ _) (node _ _ _ _)) (node key₁ _ (node key₃ _ _ _) (node _ _ _ _)) key value (t-node x₁ x₂ a b c d ti ti₁) (r-left x ri) = t-node (subst (λ k → k < key₁ ) (rt-property-key ri) x₁) x₂ ? ? c d (RTtoTI0 _ _ key value ti ri) ti₁ -RTtoTI1 : {n : Level} {A : Set n} → (tree repl : bt A) → (key : ℕ) → (value : A) → treeInvariant repl - → replacedTree key value tree repl → treeInvariant tree -RTtoTI1 .leaf .(node key value leaf leaf) key value ti r-leaf = t-leaf -RTtoTI1 (node key value₁ leaf leaf) .(node key value leaf leaf) key value (t-single .key .value) r-node = t-single key value₁ -RTtoTI1 .(node key _ leaf (node _ _ _ _)) .(node key value leaf (node _ _ _ _)) key value (t-right x a b ti) r-node = t-right x a b ti -RTtoTI1 .(node key _ (node _ _ _ _) leaf) .(node key value (node _ _ _ _) leaf) key value (t-left x a b ti) r-node = t-left x a b ti -RTtoTI1 .(node key _ (node _ _ _ _) (node _ _ _ _)) .(node key value (node _ _ _ _) (node _ _ _ _)) key value (t-node x x₁ a b c d ti ti₁) r-node = t-node x x₁ a b c d ti ti₁ --- r-right case -RTtoTI1 (node key₁ value₁ leaf leaf) (node key₁ _ leaf (node _ _ _ _)) key value (t-right x₁ a b ti) (r-right x r-leaf) = t-single key₁ value₁ -RTtoTI1 (node key₁ value₁ leaf (node key₂ value₂ t2 t3)) (node key₁ _ leaf (node key₃ _ _ _)) key value (t-right x₁ a b ti) (r-right x ri) = - t-right (subst (λ k → key₁ < k ) (sym (rt-property-key ri)) x₁) ? ? (RTtoTI1 _ _ key value ti ri) -- key₁ < key₂ -RTtoTI1 (node _ _ (node _ _ _ _) leaf) (node _ _ (node _ _ _ _) (node key value _ _)) key value (t-node x₁ x₂ a b c d ti ti₁) (r-right x r-leaf) = - t-left x₁ ? ? ti -RTtoTI1 (node key₄ _ (node key₃ _ _ _) (node key₁ value₁ n n₁)) (node key₄ _ (node key₃ _ _ _) (node key₂ _ _ _)) key value (t-node x₁ x₂ a b c d ti ti₁) (r-right x ri) = t-node x₁ (subst (λ k → key₄ < k ) (sym (rt-property-key ri)) x₂) a b ? ? ti (RTtoTI1 _ _ key value ti₁ ri) -- key₄ < key₁ --- r-left case -RTtoTI1 (node key₁ value₁ leaf leaf) (node key₁ _ _ leaf) key value (t-left x₁ a b ti) (r-left x ri) = t-single key₁ value₁ -RTtoTI1 (node key₁ _ (node key₂ value₁ n n₁) leaf) (node key₁ _ (node key₃ _ _ _) leaf) key value (t-left x₁ a b ti) (r-left x ri) = - t-left (subst (λ k → k < key₁ ) (sym (rt-property-key ri)) x₁) ? ? (RTtoTI1 _ _ key value ti ri) -- key₂ < key₁ -RTtoTI1 (node key₁ value₁ leaf _) (node key₁ _ _ _) key value (t-node x₁ x₂ a b c d ti ti₁) (r-left x r-leaf) = t-right x₂ c d ti₁ -RTtoTI1 (node key₁ value₁ (node key₂ value₂ n n₁) _) (node key₁ _ _ _) key value (t-node x₁ x₂ a b c d ti ti₁) (r-left x ri) = - t-node (subst (λ k → k < key₁ ) (sym (rt-property-key ri)) x₁) x₂ ? ? c d (RTtoTI1 _ _ key value ti ri) ti₁ -- key₂ < key₁ +-- RTtoTI1 : {n : Level} {A : Set n} → (tree repl : bt A) → (key : ℕ) → (value : A) → treeInvariant repl +-- → replacedTree key value tree repl → treeInvariant tree +-- RTtoTI1 .leaf .(node key value leaf leaf) key value ti r-leaf = t-leaf +-- RTtoTI1 (node key value₁ leaf leaf) .(node key value leaf leaf) key value (t-single .key .value) r-node = t-single key value₁ +-- RTtoTI1 .(node key _ leaf (node _ _ _ _)) .(node key value leaf (node _ _ _ _)) key value (t-right x a b ti) r-node = t-right x a b ti +-- RTtoTI1 .(node key _ (node _ _ _ _) leaf) .(node key value (node _ _ _ _) leaf) key value (t-left x a b ti) r-node = t-left x a b ti +-- RTtoTI1 .(node key _ (node _ _ _ _) (node _ _ _ _)) .(node key value (node _ _ _ _) (node _ _ _ _)) key value (t-node x x₁ a b c d ti ti₁) r-node = t-node x x₁ a b c d ti ti₁ +-- -- r-right case +-- RTtoTI1 (node key₁ value₁ leaf leaf) (node key₁ _ leaf (node _ _ _ _)) key value (t-right x₁ a b ti) (r-right x r-leaf) = t-single key₁ value₁ +-- RTtoTI1 (node key₁ value₁ leaf (node key₂ value₂ t2 t3)) (node key₁ _ leaf (node key₃ _ _ _)) key value (t-right x₁ a b ti) (r-right x ri) = +-- t-right (subst (λ k → key₁ < k ) (sym (rt-property-key ri)) x₁) ? ? (RTtoTI1 _ _ key value ti ri) -- key₁ < key₂ +-- RTtoTI1 (node _ _ (node _ _ _ _) leaf) (node _ _ (node _ _ _ _) (node key value _ _)) key value (t-node x₁ x₂ a b c d ti ti₁) (r-right x r-leaf) = +-- t-left x₁ ? ? ti +-- RTtoTI1 (node key₄ _ (node key₃ _ _ _) (node key₁ value₁ n n₁)) (node key₄ _ (node key₃ _ _ _) (node key₂ _ _ _)) key value (t-node x₁ x₂ a b c d ti ti₁) (r-right x ri) = t-node x₁ (subst (λ k → key₄ < k ) (sym (rt-property-key ri)) x₂) a b ? ? ti (RTtoTI1 _ _ key value ti₁ ri) -- key₄ < key₁ +-- -- r-left case +-- RTtoTI1 (node key₁ value₁ leaf leaf) (node key₁ _ _ leaf) key value (t-left x₁ a b ti) (r-left x ri) = t-single key₁ value₁ +-- RTtoTI1 (node key₁ _ (node key₂ value₁ n n₁) leaf) (node key₁ _ (node key₃ _ _ _) leaf) key value (t-left x₁ a b ti) (r-left x ri) = +-- t-left (subst (λ k → k < key₁ ) (sym (rt-property-key ri)) x₁) ? ? (RTtoTI1 _ _ key value ti ri) -- key₂ < key₁ +-- RTtoTI1 (node key₁ value₁ leaf _) (node key₁ _ _ _) key value (t-node x₁ x₂ a b c d ti ti₁) (r-left x r-leaf) = t-right x₂ c d ti₁ +-- RTtoTI1 (node key₁ value₁ (node key₂ value₂ n n₁) _) (node key₁ _ _ _) key value (t-node x₁ x₂ a b c d ti ti₁) (r-left x ri) = +-- t-node (subst (λ k → k < key₁ ) (sym (rt-property-key ri)) x₁) x₂ ? ? c d (RTtoTI1 _ _ key value ti ri) ti₁ -- key₂ < key₁ insertTreeP : {n m : Level} {A : Set n} {t : Set m} → (tree : bt A) → (key : ℕ) → (value : A) → treeInvariant tree → (exit : (tree repl : bt A) → treeInvariant repl ∧ replacedTree key value tree repl → t ) → t @@ -551,7 +551,7 @@ (λ p → length (proj1 p)) ⟪ s , ⟪ t , t1 ⟫ ⟫ record { tree0 = tree ; ti = P0 ; si = proj2 P ; ri = R ; ci = lift tt } $ λ p P1 loop → replaceP key value (proj2 (proj2 p)) (proj1 p) P1 (λ key value {tree1} repl1 stack P2 lt → loop ⟪ stack , ⟪ tree1 , repl1 ⟫ ⟫ P2 lt ) - $ λ tree repl P → exit tree repl {!!} --exit tree repl ⟪ RTtoTI0 _ _ _ _ (proj1 P) (proj2 P) , proj2 P ⟫ + $ λ tree repl P → exit tree repl ⟪ RTtoTI0 _ _ _ _ (proj1 P) (proj2 P) , proj2 P ⟫ insertTestP1 = insertTreeP leaf 1 1 t-leaf $ λ _ x0 P0 → insertTreeP x0 2 1 (proj1 P0)