comparison hoareBinaryTree.agda @ 606:61a0491a627b

with Hoare condition
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 03 Nov 2021 16:14:09 +0900
parents f8cc98fcc34b
children 79418701a283
comparison
equal deleted inserted replaced
605:f8cc98fcc34b 606:61a0491a627b
30 -- 30 --
31 data bt {n : Level} (A : Set n) : Set n where 31 data bt {n : Level} (A : Set n) : Set n where
32 leaf : bt A 32 leaf : bt A
33 node : (key : ℕ) → (value : A) → 33 node : (key : ℕ) → (value : A) →
34 (left : bt A ) → (write : bt A ) → bt A 34 (left : bt A ) → (write : bt A ) → bt A
35
36 bt-length : {n : Level} {A : Set n} → (tree : bt A ) → ℕ
37 bt-length leaf = 0
38 bt-length (node key value t t₁) = Data.Nat._⊔_ (bt-length t ) (bt-length t₁ )
35 39
36 find : {n : Level} {A : Set n} {t : Set n} → (key : ℕ) → (tree : bt A ) → List (bt A) 40 find : {n : Level} {A : Set n} {t : Set n} → (key : ℕ) → (tree : bt A ) → List (bt A)
37 → (next : bt A → List (bt A) → t ) → (exit : bt A → List (bt A) → t ) → t 41 → (next : bt A → List (bt A) → t ) → (exit : bt A → List (bt A) → t ) → t
38 find key leaf st _ exit = exit leaf st 42 find key leaf st _ exit = exit leaf st
39 find key (node key₁ v tree tree₁) st next exit with <-cmp key key₁ 43 find key (node key₁ v tree tree₁) st next exit with <-cmp key key₁
86 stackInvariant {_} {A} (x ∷ node key value leaf leaf ∷ tail ) = Lift _ ⊥ 90 stackInvariant {_} {A} (x ∷ node key value leaf leaf ∷ tail ) = Lift _ ⊥
87 stackInvariant {_} {A} (x ∷ tail @ (node key value leaf tree ∷ _) ) = (tree ≡ x) ∧ stackInvariant tail 91 stackInvariant {_} {A} (x ∷ tail @ (node key value leaf tree ∷ _) ) = (tree ≡ x) ∧ stackInvariant tail
88 stackInvariant {_} {A} (x ∷ tail @ (node key value tree leaf ∷ _) ) = (tree ≡ x) ∧ stackInvariant tail 92 stackInvariant {_} {A} (x ∷ tail @ (node key value tree leaf ∷ _) ) = (tree ≡ x) ∧ stackInvariant tail
89 stackInvariant {_} {A} (x ∷ tail @ (node key value left right ∷ _ )) = ( (left ≡ x) ∧ stackInvariant tail) ∨ ( (right ≡ x) ∧ stackInvariant tail) 93 stackInvariant {_} {A} (x ∷ tail @ (node key value left right ∷ _ )) = ( (left ≡ x) ∧ stackInvariant tail) ∨ ( (right ≡ x) ∧ stackInvariant tail)
90 stackInvariant {_} {A} s = Lift _ ⊥ 94 stackInvariant {_} {A} s = Lift _ ⊥
95
96 findP : {n : Level} {A : Set n} {t : Set n} → (key : ℕ) → (tree : bt A ) → (stack : List (bt A))
97 → treeInvariant tree → stackInvariant stack
98 → (next : (tree1 : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant stack → bt-length tree1 < bt-length tree → t )
99 → (exit : (tree1 : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant stack → t ) → t
100 findP = {!!}
101
102 replaceP : {n : Level} {A : Set n} {t : Set n}
103 → (key : ℕ) → (value : A) → (tree : bt A) → (stack : List (bt A)) → treeInvariant tree ∧ stackInvariant stack
104 → (next : (tree1 : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant stack → bt-length tree1 < bt-length tree → t )
105 → (exit : (tree1 : bt A) → treeInvariant tree1 → t) → t
106 replaceP = {!!}
107
108
109
110