Mercurial > hg > Gears > GearsAgda

changeset 786:12e19644535e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
test
author Moririn < Moririn@cr.ie.u-ryukyu.ac.jp>
date Mon, 02 Oct 2023 18:44:21 +0900
parents c3cce455e4e7
children d0080588ccf4
files .git/COMMIT_EDITMSG .git/index .git/logs/HEAD .git/logs/refs/heads/master .git/logs/refs/remotes/origin/master .git/refs/heads/master .git/refs/remotes/origin/master hoareBinaryTree1.agda work.agda
diffstat 9 files changed, 41 insertions(+), 22 deletions(-) [+]
line wrap: on
line diff
--- a/.git/COMMIT_EDITMSG	Mon Aug 21 19:29:26 2023 +0900
+++ b/.git/COMMIT_EDITMSG	Mon Oct 02 18:44:21 2023 +0900
@@ -1,1 +1,1 @@
-8/17
+9/5
Binary file .git/index has changed
--- a/.git/logs/HEAD	Mon Aug 21 19:29:26 2023 +0900
+++ b/.git/logs/HEAD	Mon Oct 02 18:44:21 2023 +0900
@@ -9,3 +9,4 @@
 46c240f5b42cb03db61137e92d2f67892b410362 0487cd0857ea20b08f8080576621afa1ab1c17c0 e205718 <e205718@ie.u-ryukyu.ac.jp> 1688718982 +0900	commit: 7/7
 0487cd0857ea20b08f8080576621afa1ab1c17c0 0487cd0857ea20b08f8080576621afa1ab1c17c0 e205718 <e205718@ie.u-ryukyu.ac.jp> 1688719191 +0900	reset: moving to HEAD
 0487cd0857ea20b08f8080576621afa1ab1c17c0 2edd8b993212ee33e85ac9b10b3a413a8f4dced7 e205718 <e205718@ie.u-ryukyu.ac.jp> 1688719228 +0900	merge origin/master: Merge made by the 'ort' strategy.
+2edd8b993212ee33e85ac9b10b3a413a8f4dced7 fecc8adcfeb1c0743aead365974dd4df0a754916 e205718 <e205718@ie.u-ryukyu.ac.jp> 1693708090 +0900	commit: 9/3
--- a/.git/logs/refs/heads/master	Mon Aug 21 19:29:26 2023 +0900
+++ b/.git/logs/refs/heads/master	Mon Oct 02 18:44:21 2023 +0900
@@ -8,3 +8,4 @@
 69d6285765c99fd5afe14cafd957ccbccc7d348e 46c240f5b42cb03db61137e92d2f67892b410362 e205718 <e205718@ie.u-ryukyu.ac.jp> 1687779007 +0900	commit: d
 46c240f5b42cb03db61137e92d2f67892b410362 0487cd0857ea20b08f8080576621afa1ab1c17c0 e205718 <e205718@ie.u-ryukyu.ac.jp> 1688718982 +0900	commit: 7/7
 0487cd0857ea20b08f8080576621afa1ab1c17c0 2edd8b993212ee33e85ac9b10b3a413a8f4dced7 e205718 <e205718@ie.u-ryukyu.ac.jp> 1688719228 +0900	merge origin/master: Merge made by the 'ort' strategy.
+2edd8b993212ee33e85ac9b10b3a413a8f4dced7 fecc8adcfeb1c0743aead365974dd4df0a754916 e205718 <e205718@ie.u-ryukyu.ac.jp> 1693708090 +0900	commit: 9/3
--- a/.git/logs/refs/remotes/origin/master	Mon Aug 21 19:29:26 2023 +0900
+++ b/.git/logs/refs/remotes/origin/master	Mon Oct 02 18:44:21 2023 +0900
@@ -7,3 +7,4 @@
 69d6285765c99fd5afe14cafd957ccbccc7d348e 46c240f5b42cb03db61137e92d2f67892b410362 e205718 <e205718@ie.u-ryukyu.ac.jp> 1687779013 +0900	update by push
 46c240f5b42cb03db61137e92d2f67892b410362 baeb8f1be6e05a9a3a38e619a9c9e0496e8da3e1 e205718 <e205718@ie.u-ryukyu.ac.jp> 1688719065 +0900	fetch: fast-forward
 baeb8f1be6e05a9a3a38e619a9c9e0496e8da3e1 2edd8b993212ee33e85ac9b10b3a413a8f4dced7 e205718 <e205718@ie.u-ryukyu.ac.jp> 1688719257 +0900	update by push
+2edd8b993212ee33e85ac9b10b3a413a8f4dced7 fecc8adcfeb1c0743aead365974dd4df0a754916 e205718 <e205718@ie.u-ryukyu.ac.jp> 1693708101 +0900	update by push
--- a/.git/refs/heads/master	Mon Aug 21 19:29:26 2023 +0900
+++ b/.git/refs/heads/master	Mon Oct 02 18:44:21 2023 +0900
@@ -1,1 +1,1 @@
-2edd8b993212ee33e85ac9b10b3a413a8f4dced7
+fecc8adcfeb1c0743aead365974dd4df0a754916
--- a/.git/refs/remotes/origin/master	Mon Aug 21 19:29:26 2023 +0900
+++ b/.git/refs/remotes/origin/master	Mon Oct 02 18:44:21 2023 +0900
@@ -1,1 +1,1 @@
-2edd8b993212ee33e85ac9b10b3a413a8f4dced7
+fecc8adcfeb1c0743aead365974dd4df0a754916
--- a/hoareBinaryTree1.agda	Mon Aug 21 19:29:26 2023 +0900
+++ b/hoareBinaryTree1.agda	Mon Oct 02 18:44:21 2023 +0900
@@ -301,7 +301,8 @@
         ... |  tri≈ ¬a b ¬c = ⊥-elim (¬a x)
         ... |  tri> ¬a ¬b c = ⊥-elim (¬a x)
         repl12 : replacedTree key value (child-replaced key  tree1  ) repl
-        repl12 = subst₂ (λ j k → replacedTree key value j k ) (sym (subst (λ k → child-replaced key k ≡ leaf) (sym repl09) repl07 ) ) (sym (rt-property-leaf (replacePR.ri Pre))) r-leaf
+        repl12 = subst₂ {!!} {!!} {!!} {!!}
+       -- repl12 = subst₂ (λ j k → replacedTree key value j k ) (sym (subst (λ k → child-replaced key k ≡ leaf) (sym repl09) repl07 ) ) (sym (rt-property-leaf (replacePR.ri Pre))) r-leaf
 replaceP {n} {_} {A} key value {tree}  repl (node key₁ value₁ left right ∷ st@(tree1 ∷ st1)) Pre next exit  with <-cmp key key₁ 
 ... | tri< a ¬b ¬c = next key value (node key₁ value₁ repl right ) st Post ≤-refl where
     Post : replacePR key value tree1 (node key₁ value₁ repl right ) st (λ _ _ _ → Lift n ⊤) 
@@ -927,23 +928,36 @@
       -- grand ≡ node kg vg (node ku ⟪ Black , proj4 ⟫ left₁ right₁) (node kp ⟪ Black , proj3 ⟫ left right)
     insertCase1 : t
     insertCase1 with stackToPG (RBI.tree r) orig stack (RBI.si r)
-    ... | case1 eq = exit repl stack eq record {  -- exit rot repl rbir (subst (λ k → rotatedTree k rot) (stackCase1 si eq) roti) ri 
-       od = {!!} ; d = {!!} ; rd = {!!}
-       ; tree = RBI.tree r ; rot = {!!}
-       ; origti = {!!}
-       ; origrb = {!!}
-       ; treerb = {!!}
-       ; replrb = {!!}
-       ; d=rd = {!!}
-       ; si = {!!}
-       ; rotated = {!!}
-       ; ri = {!!} }
-    ... | case2 (case1 eq ) = {!!} where
-        insertCase12 : (to : bt (Color ∧ A)) → {d : ℕ} → RBtreeInvariant orig   → to ≡ orig
-          → (rr : bt (Color ∧ A)) → {dr : ℕ} → RBtreeInvariant {!!}   → rr ≡ {!!}
-          → {stack : List (bt (Color ∧ A))} → (si : stackInvariant key {!!} to stack ) 
-          → stack ≡ {!!} ∷ to ∷ [] → t
-        insertCase12 = {!!}
+    ... | case1 eq = exit repl stack eq  record {  -- exit rot repl rbir (subst (λ k → rotatedTree k rot) (stackCase1 si eq) roti) ri 
+        od = RBI.od r ; d = RBI.d r  ; rd = RBI.rd r ; --r
+        tree = RBI.tree r ; rot = RBI.rot r
+       ; origti = RBI.origti r
+       ; origrb = RBI.origrb r 
+       ; treerb = RBI.treerb r
+       ; replrb = RBI.replrb r
+       ; d=rd = RBI.d=rd r
+       ; si = RBI.si r
+       ; rotated = RBI.rotated r
+       ; ri = RBI.ri r } 
+    ... | case2 (case1 eq) = {!!} where -- insertCase12
+        insertCase12 : (to : bt (Color ∧ A)) → RBtreeInvariant orig   → to ≡ orig
+          → (rr : bt (Color ∧ A)) → RBtreeInvariant repl → rr ≡ repl
+          → {stack : List (bt (Color ∧ A))} → (si : stackInvariant key rr to stack ) 
+          → stack ≡ rr  ∷ to ∷ [] → t
+        insertCase12 to origrb to≡orig rr rrrb rr≡repl si s≡  = next rr stack 
+{-         record {
+         od = RBI.od r ; d = RBI.d r  ; rd = RBI.rd r ; --r
+         tree = rr ; rot = RBI.rot r
+         ; origti = RBI.origti r
+         ; origrb = RBI.origrb r
+         ; treerb = rrrb
+         ; replrb = rrrb
+         ; d=rd = RBI.d=rd r
+         ; si = si
+         ; rotated = RBI.rotated r
+         ; ri = {!!} }
+         -}
+         ? {!!}
     -- exit rot repl rbir ? ? 
     ... | case2 (case2 pg) = {!!} -- insertCase2 tree (PG.parent pg) (PG.uncle pg) (PG.grand pg) stack si (PG.pg pg) 
 
--- a/work.agda	Mon Aug 21 19:29:26 2023 +0900
+++ b/work.agda	Mon Oct 02 18:44:21 2023 +0900
@@ -163,7 +163,7 @@
 black-depth (node key ⟪ Black , value ⟫  t t₁) = suc (black-depth t  ⊔ black-depth t₁ )
 
 data RBtreeInvariant {n : Level} {A : Set n} : (tree : bt (Color ∧ A)) → Set n where
-    rb-leaf : RBtreeInvariant leaf
+    rb-leaf :  RBtreeInvariant leaf
     rb-single : (key : ℕ) → (value : A) →  RBtreeInvariant (node key ⟪ Black , value ⟫ leaf leaf)
     rb-right-red : {key key₁ : ℕ} → {value value₁ : A} → {t t₁ : bt (Color ∧ A)} → key < key₁
        → black-depth t ≡ black-depth t₁ 
@@ -354,3 +354,5 @@
            
 rbi-case1 {n} {A} {key} (node key1 ⟪ Black , value1 ⟫ l r) leaf rbip rbir (node key3 ⟪ Red , val3 ⟫ la ra) (node key4-- ⟪ Red , val4 ⟫ lb rb) pa li ri = {!!}
 -}
+
+