Mercurial > hg > Gears > GearsAgda
changeset 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 | b78dc85d76d6 |
| files | hoareBinaryTree.agda |
| diffstat | 1 files changed, 20 insertions(+), 0 deletions(-) [+] |
line wrap: on
line diff
--- a/hoareBinaryTree.agda Wed Nov 03 15:58:10 2021 +0900 +++ b/hoareBinaryTree.agda Wed Nov 03 16:14:09 2021 +0900 @@ -33,6 +33,10 @@ node : (key : ℕ) → (value : A) → (left : bt A ) → (write : bt A ) → bt A +bt-length : {n : Level} {A : Set n} → (tree : bt A ) → ℕ +bt-length leaf = 0 +bt-length (node key value t t₁) = Data.Nat._⊔_ (bt-length t ) (bt-length t₁ ) + find : {n : Level} {A : Set n} {t : Set n} → (key : ℕ) → (tree : bt A ) → List (bt A) → (next : bt A → List (bt A) → t ) → (exit : bt A → List (bt A) → t ) → t find key leaf st _ exit = exit leaf st @@ -88,3 +92,19 @@ stackInvariant {_} {A} (x ∷ tail @ (node key value tree leaf ∷ _) ) = (tree ≡ x) ∧ stackInvariant tail stackInvariant {_} {A} (x ∷ tail @ (node key value left right ∷ _ )) = ( (left ≡ x) ∧ stackInvariant tail) ∨ ( (right ≡ x) ∧ stackInvariant tail) stackInvariant {_} {A} s = Lift _ ⊥ + +findP : {n : Level} {A : Set n} {t : Set n} → (key : ℕ) → (tree : bt A ) → (stack : List (bt A)) + → treeInvariant tree → stackInvariant stack + → (next : (tree1 : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant stack → bt-length tree1 < bt-length tree → t ) + → (exit : (tree1 : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant stack → t ) → t +findP = {!!} + +replaceP : {n : Level} {A : Set n} {t : Set n} + → (key : ℕ) → (value : A) → (tree : bt A) → (stack : List (bt A)) → treeInvariant tree ∧ stackInvariant stack + → (next : (tree1 : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant stack → bt-length tree1 < bt-length tree → t ) + → (exit : (tree1 : bt A) → treeInvariant tree1 → t) → t +replaceP = {!!} + + + +