Mercurial > hg > Gears > GearsAgda
changeset 609:79418701a283
add test and speciication
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 04 Nov 2021 16:35:11 +0900 |
| parents | 8df36383ced0 |
| children | 8239583dac0b |
| files | hoareBinaryTree.agda logic.agda |
| diffstat | 2 files changed, 77 insertions(+), 20 deletions(-) [+] |
line wrap: on
line diff
--- a/hoareBinaryTree.agda Wed Nov 03 18:28:31 2021 +0900 +++ b/hoareBinaryTree.agda Thu Nov 04 16:35:11 2021 +0900 @@ -33,11 +33,11 @@ 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₁ ) +bt-depth : {n : Level} {A : Set n} → (tree : bt A ) → ℕ +bt-depth leaf = 0 +bt-depth (node key value t t₁) = Data.Nat._⊔_ (bt-depth t ) (bt-depth t₁ ) -find : {n : Level} {A : Set n} {t : Set n} → (key : ℕ) → (tree : bt A ) → List (bt A) +find : {n m : Level} {A : Set n} {t : Set m} → (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 find key (node key₁ v tree tree₁) st next exit with <-cmp key key₁ @@ -46,12 +46,12 @@ find key n@(node key₁ v tree tree₁) st next _ | tri> ¬a ¬b c = next tree₁ (n ∷ st) {-# TERMINATING #-} -find-loop : {n : Level} {A : Set n} {t : Set n} → (key : ℕ) → bt A → List (bt A) → (exit : bt A → List (bt A) → t) → t -find-loop {_} {A} {t} key tree st exit = find-loop1 tree st where +find-loop : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → bt A → List (bt A) → (exit : bt A → List (bt A) → t) → t +find-loop {_} {_} {A} {t} key tree st exit = find-loop1 tree st where find-loop1 : bt A → List (bt A) → t find-loop1 tree st = find key tree st find-loop1 exit -replace : {n : Level} {A : Set n} {t : Set n} → (key : ℕ) → (value : A) → bt A → List (bt A) → (next : ℕ → A → bt A → List (bt A) → t ) → (exit : bt A → t) → t +replace : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (value : A) → bt A → List (bt A) → (next : ℕ → A → bt A → List (bt A) → t ) → (exit : bt A → t) → t replace key value tree [] next exit = exit tree replace key value tree (leaf ∷ st) next exit = next key value tree st replace key value tree (node key₁ value₁ left right ∷ st) next exit with <-cmp key key₁ @@ -60,12 +60,12 @@ ... | tri> ¬a ¬b c = next key value (node key₁ value₁ left tree ) st {-# TERMINATING #-} -replace-loop : {n : Level} {A : Set n} {t : Set n} → (key : ℕ) → (value : A) → bt A → List (bt A) → (exit : bt A → t) → t -replace-loop {_} {A} {t} key value tree st exit = replace-loop1 key value tree st where +replace-loop : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (value : A) → bt A → List (bt A) → (exit : bt A → t) → t +replace-loop {_} {_} {A} {t} key value tree st exit = replace-loop1 key value tree st where replace-loop1 : (key : ℕ) → (value : A) → bt A → List (bt A) → t replace-loop1 key value tree st = replace key value tree st replace-loop1 exit -insertTree : {n : Level} {A : Set n} {t : Set n} → (tree : bt A) → (key : ℕ) → (value : A) → (next : bt A → t ) → t +insertTree : {n m : Level} {A : Set n} {t : Set m} → (tree : bt A) → (key : ℕ) → (value : A) → (next : bt A → t ) → t insertTree tree key value exit = find-loop key tree [] ( λ t st → replace-loop key value t st exit ) insertTest1 = insertTree leaf 1 1 (λ x → x ) @@ -93,18 +93,74 @@ 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 ) +findP : {n m : Level} {A : Set n} {t : Set m} → (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-depth tree1 < bt-depth 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 = {!!} +findP key leaf st Pre _ exit = exit leaf st {!!} +findP key (node key₁ v tree tree₁) st Pre next exit with <-cmp key key₁ +findP key n st Pre _ exit | tri≈ ¬a b ¬c = exit n st {!!} +findP key n@(node key₁ v tree tree₁) st Pre next _ | tri< a ¬b ¬c = next tree (n ∷ st) {!!} {!!} +findP key n@(node key₁ v tree tree₁) st Pre next _ | tri> ¬a ¬b c = next tree₁ (n ∷ st) {!!} {!!} +replaceP : {n m : Level} {A : Set n} {t : Set m} + → (key : ℕ) → (value : A) → (tree : bt A) → (stack : List (bt A)) → treeInvariant tree ∧ stackInvariant stack + → (next : ℕ → A → (tree1 : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant stack → bt-depth tree1 < bt-depth tree → t ) + → (exit : (tree1 : bt A) → treeInvariant tree1 → t) → t +replaceP key value tree [] Pre next exit = exit tree {!!} +replaceP key value tree (leaf ∷ st) Pre next exit = next key value tree st {!!} {!!} +replaceP key value tree (node key₁ value₁ left right ∷ st) Pre next exit with <-cmp key key₁ +... | tri< a ¬b ¬c = next key value (node key₁ value₁ tree right ) st {!!} {!!} +... | tri≈ ¬a b ¬c = next key value (node key₁ value left right ) st {!!} {!!} +... | tri> ¬a ¬b c = next key value (node key₁ value₁ left tree ) st {!!} {!!} +open import Relation.Binary.Definitions +nat-≤> : { x y : ℕ } → x ≤ y → y < x → ⊥ +nat-≤> (s≤s x<y) (s≤s y<x) = nat-≤> x<y y<x +lemma3 : {i j : ℕ} → 0 ≡ i → j < i → ⊥ +lemma3 refl () +lemma5 : {i j : ℕ} → i < 1 → j < i → ⊥ +lemma5 (s≤s z≤n) () + +TerminatingLoopS : {l m : Level} {t : Set l} (Index : Set m ) → {Invraiant : Index → Set m } → ( reduce : Index → ℕ) + → (r : Index) → (p : Invraiant r) + → (loop : (r : Index) → Invraiant r → (next : (r1 : Index) → Invraiant r1 → reduce r1 < reduce r → t ) → t) → t +TerminatingLoopS {_} {_} {t} Index {Invraiant} reduce r p loop with <-cmp 0 (reduce r) +... | tri≈ ¬a b ¬c = loop r p (λ r1 p1 lt → ⊥-elim (lemma3 b lt) ) +... | tri< a ¬b ¬c = loop r p (λ r1 p1 lt1 → TerminatingLoop1 (reduce r) r r1 (≤-step lt1) p1 lt1 ) where + TerminatingLoop1 : (j : ℕ) → (r r1 : Index) → reduce r1 < suc j → Invraiant r1 → reduce r1 < reduce r → t + TerminatingLoop1 zero r r1 n≤j p1 lt = loop r1 p1 (λ r2 p1 lt1 → ⊥-elim (lemma5 n≤j lt1)) + TerminatingLoop1 (suc j) r r1 n≤j p1 lt with <-cmp (reduce r1) (suc j) + ... | tri< a ¬b ¬c = TerminatingLoop1 j r r1 a p1 lt + ... | tri≈ ¬a b ¬c = loop r1 p1 (λ r2 p2 lt1 → TerminatingLoop1 j r1 r2 (subst (λ k → reduce r2 < k ) b lt1 ) p2 lt1 ) + ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c n≤j ) + +open _∧_ + +insertTreeP : {n : Level} {A : Set n} {t : Set n} → (tree : bt A) → (key : ℕ) → (value : A) → treeInvariant tree → (exit : (tree : bt A) → treeInvariant tree → t ) → t +insertTreeP {n} {A} {t} tree key value P exit = + TerminatingLoopS (bt A ∧ List (bt A)) {λ p → treeInvariant (proj1 p) ∧ stackInvariant (proj2 p)} (λ p → bt-depth (proj1 p)) ⟪ tree , [] ⟫ ⟪ P , lift tt ⟫ + (λ p P loop → findP key (proj1 p) (proj2 p) P (λ t s P1 lt → loop ⟪ t , s ⟫ P1 lt ) + (λ t s P → TerminatingLoopS (bt A ∧ List (bt A)) {λ p → treeInvariant (proj1 p) ∧ stackInvariant (proj2 p)} (λ p → bt-depth (proj1 p)) ⟪ t , s ⟫ P + (λ p P1 loop → replaceP key value (proj1 p) (proj2 p) P1 (λ k v t s P2 lt → loop ⟪ t , s ⟫ P2 lt) exit) + ) ) + +top-value : {n : Level} {A : Set n} → (tree : bt A) → Maybe A +top-value leaf = nothing +top-value (node key value tree tree₁) = just value + +insertTreeSpec0 : {n : Level} {A : Set n} {t : Set n} → (tree : bt A) → (value : A) → top-value tree ≡ just value → ⊤ +insertTreeSpec0 _ _ _ = tt + +insertTreeSpec1 : {n : Level} {A : Set n} → (tree : bt A) → (key : ℕ) → (value : A) → treeInvariant tree → ⊤ +insertTreeSpec1 {n} {A} tree key value P = + TerminatingLoopS (bt A ∧ List (bt A)) {λ p → treeInvariant (proj1 p) ∧ stackInvariant (proj2 p)} (λ p → bt-depth (proj1 p)) ⟪ tree , [] ⟫ ⟪ P , lift tt ⟫ + $ λ p P loop → findP key (proj1 p) (proj2 p) P (λ t s P1 lt → loop ⟪ t , s ⟫ P1 lt ) + $ λ t s P → TerminatingLoopS (bt A ∧ List (bt A)) {λ p → treeInvariant (proj1 p) ∧ stackInvariant (proj2 p)} (λ p → bt-depth (proj1 p)) ⟪ t , s ⟫ P + $ λ p P1 loop → replaceP key value (proj1 p) (proj2 p) P1 (λ k v t s P2 lt → loop ⟪ t , s ⟫ P2 lt) + $ λ t1 P2 → TerminatingLoopS (bt A ∧ List (bt A)) {λ p → treeInvariant (proj1 p) ∧ stackInvariant (proj2 p)} (λ p → bt-depth (proj1 p)) ⟪ t1 , [] ⟫ ⟪ P2 , lift tt ⟫ + $ λ p P3 loop → findP key (proj1 p) (proj2 p) P3 (λ t s P3 lt → loop ⟪ t , s ⟫ P3 lt ) + $ λ t2 s1 P4 → insertTreeSpec0 t2 value {!!} +