# HG changeset patch # User Shinji KONO # Date 1636507114 -32400 # Node ID 956ee8ae42b9d4aa6e83784b6fedbefe03ce0fb4 # Parent 24bec7639079b651165c9385ea74a3f6d1e276a2 ... diff -r 24bec7639079 -r 956ee8ae42b9 hoareBinaryTree.agda --- a/hoareBinaryTree.agda Tue Nov 09 09:44:23 2021 +0900 +++ b/hoareBinaryTree.agda Wed Nov 10 10:18:34 2021 +0900 @@ -196,7 +196,7 @@ tree0 : bt A ti : treeInvariant tree0 si : stackInvariant key tree tree0 stack - ci : C tree stack + ci : C tree stack -- data continuation findPP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree : bt A ) → (stack : List (bt A)) diff -r 24bec7639079 -r 956ee8ae42b9 hoareBinaryTree1.agda --- a/hoareBinaryTree1.agda Tue Nov 09 09:44:23 2021 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,117 +0,0 @@ -module hoareBinaryTree1 where - -open import Level renaming (zero to Z ; suc to succ) - -open import Data.Nat hiding (compare) -open import Data.Nat.Properties as NatProp -open import Data.Maybe --- open import Data.Maybe.Properties -open import Data.Empty -open import Data.List -open import Data.Product - -open import Function as F hiding (const) - -open import Relation.Binary -open import Relation.Binary.PropositionalEquality -open import Relation.Nullary hiding (proof) -open import logic - - -data bt {n : Level} (A : Set n) : Set n where - bt-empty : bt A - bt-node : (key : ℕ) → A → - (ltree : bt A) → (rtree : bt A) → bt A - -bt-find : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree : bt A ) → List (bt A) - → ( bt A → List (bt A) → t ) → t -bt-find {n} {m} {A} {t} key leaf@(bt-empty) stack exit = exit leaf stack -bt-find {n} {m} {A} {t} key (bt-node key₁ AA tree tree₁) stack next with <-cmp key key₁ -bt-find {n} {m} {A} {t} key node@(bt-node key₁ AA tree tree₁) stack exit | tri≈ ¬a b ¬c = exit node stack -bt-find {n} {m} {A} {t} key node@(bt-node key₁ AA ltree rtree) stack next | tri< a ¬b ¬c = bt-find key ltree (node ∷ stack) next -bt-find {n} {m} {A} {t} key node@(bt-node key₁ AA ltree rtree) stack next | tri> ¬a ¬b c = bt-find key rtree (node ∷ stack) next - -bt-replace : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → A → bt A → List (bt A) → (bt A → t ) → t -bt-replace {n} {m} {A} {t} ikey a otree stack next = bt-replace0 otree where - bt-replace1 : bt A → List (bt A) → t - bt-replace1 tree [] = next tree - bt-replace1 node ((bt-empty) ∷ stack) = bt-replace1 node stack - bt-replace1 node ((bt-node key₁ b x x₁) ∷ stack) = bt-replace1 (bt-node key₁ b node x₁) stack - bt-replace0 : (tree : bt A) → t - bt-replace0 tree@(bt-node key _ ltr rtr) = bt-replace1 (bt-node ikey a ltr rtr) stack -- find case - bt-replace0 bt-empty = bt-replace1 (bt-node ikey a bt-empty bt-empty) stack - - -bt-Empty : {n : Level} {A : Set n} → bt A -bt-Empty = bt-empty - -bt-insert : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → A → bt A → (bt A → t ) → t -bt-insert key a tree next = bt-find key tree [] (λ mtree stack → bt-replace key a mtree stack (λ tree → next tree) ) - -find-test : bt ℕ -find-test = bt-find 5 bt-empty [] (λ x y → x) - - -insert-test : bt ℕ -insert-test = bt-insert 5 7 bt-empty (λ x → x) - -insert-test1 : bt ℕ -insert-test1 = bt-insert 5 7 bt-empty (λ x → bt-insert 15 17 x (λ y → y)) - -insert-test2 : {n : Level} {t : Set n} → ( bt ℕ → t ) → t -insert-test2 next = bt-insert 15 17 bt-empty - $ λ x1 → bt-insert 5 7 x1 - $ λ x2 → bt-insert 1 3 x2 - $ λ x3 → bt-insert 4 2 x3 - $ λ x4 → bt-insert 1 4 x4 - $ λ y → next y - -insert-test3 : bt ℕ -insert-test3 = bt-insert 15 17 bt-empty - $ λ x1 → bt-insert 5 7 x1 - $ λ x2 → bt-insert 1 3 x2 - $ λ x3 → bt-insert 4 2 x3 - $ λ x4 → bt-insert 1 4 x4 - $ λ y → y - -insert-find0 : bt ℕ -insert-find0 = insert-test2 $ λ tree → bt-find 1 tree [] $ λ x y → x - -insert-find1 : List (bt ℕ) -insert-find1 = insert-test2 $ λ tree → bt-find 1 tree [] $ λ x y → y - --- --- 1 After insert, all node except inserted node is preserved --- 2 After insert, specified key node is inserted --- 3 tree node order is consistent --- --- 4 noes on stack + current node = original top node .... invriant bt-find --- 5 noes on stack + current node = original top node with replaced node .... invriant bt-replace - -tree+stack0 : {n : Level} {A : Set n} → (tree mtree : bt A) → (stack : List (bt A)) → Set n -tree+stack0 {n} {A} tree mtree [] = {!!} -tree+stack0 {n} {A} tree mtree (x ∷ stack) = {!!} - -tree+stack : {n : Level} {A : Set n} → (tree mtree : bt A) → (stack : List (bt A)) → Set n -tree+stack {n} {A} bt-empty mtree stack = (mtree ≡ bt-empty) ∧ (stack ≡ []) -tree+stack {n} {A} (bt-node key x tree tree₁) mtree stack = bt-replace key x mtree stack (λ ntree → ntree ≡ tree) - -data _implies_ (A B : Set ) : Set (succ Z) where - proof : ( A → B ) → A implies B - -implies2p : {A B : Set } → A implies B → A → B -implies2p (proof x) = x - - -bt-find-hoare1 : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree mtree : bt A ) → (stack : List (bt A)) - → (tree+stack tree mtree stack) - → ( (ntree : bt A) → (nstack : List (bt A)) → (tree+stack tree ntree nstack) → t ) → t -bt-find-hoare1 {n} {m} {A} {t} key leaf@(bt-empty) mtree stack t+s exit = exit leaf stack {!!} -bt-find-hoare1 {n} {m} {A} {t} key (bt-node key₁ AA tree tree₁) mtree stack t+s next with <-cmp key key₁ -bt-find-hoare1 {n} {m} {A} {t} key node@(bt-node key₁ AA tree tree₁) mtree stack t+s exit | tri≈ ¬a b ¬c = exit node stack {!!} -bt-find-hoare1 {n} {m} {A} {t} key node@(bt-node key₁ AA ltree rtree) mtree stack t+s next | tri< a ¬b ¬c = bt-find-hoare1 {n} {m} {A} {t} key ltree {!!} (node ∷ stack) {!!} {!!} -bt-find-hoare1 {n} {m} {A} {t} key node@(bt-node key₁ AA ltree rtree) mtree stack t+s next | tri> ¬a ¬b c = bt-find-hoare1 key rtree {!!} (node ∷ stack) {!!} {!!} - - -bt-find-hoare : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree : bt A ) → ( (ntree : bt A) → (nstack : List (bt A)) → (tree+stack tree ntree nstack) → t ) → t -bt-find-hoare {n} {m} {A} {t} key node exit = bt-find-hoare1 {n} {m} {A} {t} key node bt-empty [] ({!!}) exit