Mercurial > hg > Members > Moririn
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 |