Mercurial > hg > Gears > GearsAgda

changeset 630:24bec7639079

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 09 Nov 2021 09:44:23 +0900
parents 7a19d4b43795
children 956ee8ae42b9
files hoareBinaryTree.agda
diffstat 1 files changed, 6 insertions(+), 6 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree.agda	Tue Nov 09 09:31:43 2021 +0900
+++ b/hoareBinaryTree.agda	Tue Nov 09 09:44:23 2021 +0900
@@ -101,9 +101,9 @@
 data stackInvariant {n : Level} {A : Set n} (key0 : ℕ) : (tree tree0 : bt A) → (stack  : List (bt A)) → Set n where
     s-nil : stackInvariant  key0 leaf leaf [] 
     s-single : (tree : bt A) → stackInvariant key0 tree tree (tree ∷ [] ) 
-    s-<      : (tree0 tree : bt A) → {key : ℕ } → {value : A } { left  : bt A} → {st : List (bt A)}
+    s-right      : (tree0 tree : bt A) → {key : ℕ } → {value : A } { left  : bt A} → {st : List (bt A)}
          → key < key0 → stackInvariant key0(node key value left tree ) tree0 (node key value left tree ∷ st )  → stackInvariant key0 tree tree0 (tree  ∷ node key value left tree ∷ st ) 
-    s->      : (tree0 tree : bt A) → {key : ℕ } → {value : A } { right  : bt A} → {st : List (bt A)}
+    s-left      : (tree0 tree : bt A) → {key : ℕ } → {value : A } { right  : bt A} → {st : List (bt A)}
          → key0 < key → stackInvariant key0(node key value tree right ) tree0 (node key value tree right ∷ st )  → stackInvariant key0 tree tree0 (tree  ∷ node key value tree right ∷ st ) 
 
 data replacedTree  {n : Level} {A : Set n} (key : ℕ) (value : A)  : (tree tree1 : bt A ) → Set n where
@@ -118,9 +118,9 @@
            →  treeInvariant tree ∧ stackInvariant key tree tree0 stack  
            → (next : (tree1 tree0 : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack → bt-depth tree1 < bt-depth tree   → t )
            → (exit : (tree1 tree0 : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack → t ) → t
-findP key leaf tree0 st Pre _ exit = exit leaf tree0 st {!!}
+findP key leaf tree0 st Pre _ exit = exit leaf tree0 st Pre
 findP key (node key₁ v tree tree₁) tree0 st Pre next exit with <-cmp key key₁
-findP key n tree0 st Pre _ exit | tri≈ ¬a b ¬c = exit n tree0 st {!!}
+findP key n tree0 st Pre _ exit | tri≈ ¬a b ¬c = exit n tree0 st Pre
 findP key n@(node key₁ v tree tree₁) tree0 st Pre next _ | tri< a ¬b ¬c = next tree tree0 (n ∷ st) {!!} {!!}
 findP key n@(node key₁ v tree tree₁) tree0 st Pre next _ | tri> ¬a ¬b c = next tree₁ tree0 (n ∷ st) {!!} {!!}
 
@@ -221,7 +221,7 @@
      → (exit : (tree repl : bt A) → treeInvariant tree ∧ replacedTree key value tree repl → t ) → t
 insertTreePP {n} {m} {A} {t} tree key value  P exit =
    TerminatingLoopS (bt A ∧ List (bt A) ) {λ p → findPR key (proj1 p) (proj2 p) (λ t s → Lift n ⊤) } (λ p → bt-depth (proj1 p)) ⟪ tree , [] ⟫  {!!}
-       $ λ p P loop → findPP key (proj1 p) (proj2 p) {!!} (λ t s P1 lt → loop ⟪ t ,  s  ⟫ {!!} lt )
+       $ λ p P loop → findPP key (proj1 p) (proj2 p) P (λ t s P1 lt → loop ⟪ t ,  s  ⟫ P1 lt )
        $ λ t s _ P → replaceNodeP key value t {!!}
        $ λ t1 P1 R → TerminatingLoopS (List (bt A) ∧ (bt A ∧ bt A ))
             {λ p → treeInvariant (proj1 (proj2 p)) ∧ stackInvariant key (proj1 (proj2 p)) tree (proj1 p)  ∧ replacedTree key value (proj1 (proj2 p)) (proj2 (proj2 p)) }
@@ -251,7 +251,7 @@
    TerminatingLoopS (bt A ∧ List (bt A) )
      {λ p → findPR key (proj1 p) (proj2 p) (findPC key value ) } (λ p → bt-depth (proj1 p))
               ⟪ tree1 , []  ⟫ {!!}
-       $ λ p P loop → findPPC key value (proj1 p) (proj2 p) {!!} (λ t s P1 lt → loop ⟪ t , s ⟫ {!!} lt )  
+       $ λ p P loop → findPPC key value (proj1 p) (proj2 p) P (λ t s P1 lt → loop ⟪ t , s ⟫ P1 lt )  
        $ λ t1 s1 found? P2 → insertTreeSpec0 t1 value (lemma6 t1 s1 found? P2) where
            lemma6 : (t1 : bt A) (s1 : List (bt A)) (found? : (t1 ≡ leaf) ∨ (node-key t1 ≡ just key)) (P2 : findPR key t1 s1 (findPC key value)) → top-value t1 ≡ just value
            lemma6 t1 s1 found? P2 = lemma7 t1 s1 (findPR.tree0 P2) ( findPC.tree1  (findPR.ci P2)) ( findPC.ci  (findPR.ci P2)) (findPR.si P2) found? where