Mercurial > hg > Members > soto > experimental

changeset 8:5b398e84eae3

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
refactoring
author soto
date Tue, 01 Dec 2020 19:04:17 +0900
parents 06d03fab2668
children a335a903f87d
files rbt_t.agda
diffstat 1 files changed, 76 insertions(+), 169 deletions(-) [+]
line wrap: on
line diff
--- a/rbt_t.agda	Tue Nov 24 19:28:52 2020 +0900
+++ b/rbt_t.agda	Tue Dec 01 19:04:17 2020 +0900
@@ -36,11 +36,8 @@
     varl : List rbt
 open Env
 
-whileTest_next : {l : Level} {t : Set l}  → (c10 : rbt) → (n : ℕ) → (list : List rbt) → (next : Env → t) → (exit : Env → t) → t
-whileTest_next c10 n list next exit = next (record {vart = c10 ; varn = n ; varl = list} )
-
---whileTest_exit : {l : Level} {t : Set l}  → (c10 : bst) → (n : ℕ) → (list : List bst) → (next : Env → t) → (exit : Env → t) → t
---whileTest_exit c10 n list next exit = exit (record {vart = c10 ; varn = n ; varl = list} )
+whileTest-next : {l : Level} {t : Set l}  → (c10 : rbt) → (n : ℕ) → (list : List rbt) → (next : Env → t) → (exit : Env → t) → t
+whileTest-next c10 n list next exit = next (record {vart = c10 ; varn = n ; varl = list} )
 
 merge-tree :  {le : Level} {t : Set le} → Env → (next : Env → t) → (exit : Env → t) → t
 
@@ -58,28 +55,13 @@
     ; rtree = (bt-node record { key = record { coler = black ; number = rn } ; ltree = rl ; rtree = rr }) })
     ; varn = varn ; varl = varl }
 
-{-
-split bt-empty n stack = bt-empty
-split node@(bt-node (record { key = record { coler = y ; number = x }; ltree = l; rtree = bt-empty }) ) n stack = node
-
-split node@(bt-node (record { key = record { coler = y ; number = x }; ltree = bt-empty; rtree = r }) ) n stack = node
-split node@(bt-node (record { key = record { coler = y ; number = x }
-  ; ltree = (bt-node (record { key = record { coler = ly ; number = lx }; ltree = ll; rtree = lr }) )
-  ; rtree = (bt-node (record { key = record { coler = ry ; number = rx }; ltree = rl; rtree = rr }) )}) ) n stack
-  = {!!}
--}
-{-
-merge-tree (bt-node (record { key = record { coler = red ; number = x }
-      ; ltree = (bt-node (record { key = record { coler = black ; number = lx }; ltree = ll; rtree = lr }) )
-      ; rtree = (bt-node (record { key = record { coler = black ; number = rx }; ltree = rl; rtree = rr }) )})) n stack
--}
 
 -- 右回転
 -- 実行時splitへ、それ以外はmerge-treeへ
-merge-rotate_right : {le : Level} {t : Set le} → Env → (next : Env → t) → (exit : Env → t) → t
-merge-rotate_right node@record { vart = bt-empty ; varn = varn ; varl = varl } next exit = exit node
-merge-rotate_right node@record { vart = bt-node record { key = record { coler = coler ; number = number } ; ltree = bt-empty ; rtree = r } ; varn = varn ; varl = varl } next exit = exit node
-merge-rotate_right record { vart = bt-node record { key = record { coler = y ; number = x }
+merge-rotate-right : {le : Level} {t : Set le} → Env → (next : Env → t) → (exit : Env → t) → t
+merge-rotate-right node@record { vart = bt-empty ; varn = varn ; varl = varl } next exit = exit node
+merge-rotate-right node@record { vart = bt-node record { key = record { coler = coler ; number = number } ; ltree = bt-empty ; rtree = r } ; varn = varn ; varl = varl } next exit = exit node
+merge-rotate-right record { vart = bt-node record { key = record { coler = y ; number = x }
   ; ltree = (bt-node record { key =  record { coler = ly ; number = lx } ; ltree = ll ; rtree = lr })
   ; rtree = r }
   ; varn = varn ; varl = varl } next exit
@@ -88,28 +70,15 @@
       ; rtree = (bt-node record { key = record { coler = red ; number = x } ; ltree = lr; rtree = r }) }
       ; varn = varn ; varl = varl }
 
-{-
-merge-rotate_right bt-empty n stack = bt-empty
-merge-rotate_right node@(bt-node (record { key = _; ltree = bt-empty; rtree = _ }) ) n stack = node
-merge-rotate_right (bt-node (record { key = record { coler = y ; number = x }
-  ; ltree = (bt-node (record { key = record { coler = ly ; number = lx }; ltree = ll; rtree = lr }) )
-  ; rtree = r }) ) n stack
-    = {!!}
--}
-{-
-split (bt-node (record { key = record { coler = y ; number = lx }
-      ; ltree = ll
-      ; rtree = (bt-node (record { key = record { coler = red ; number = x }; ltree = lr; rtree = r }) ) }) ) n stack
--}
 
 -- split
-split_branch : {le : Level} {t : Set le} → Env → (next : Env → t) → (exit : Env → t) → t
-split_branch node@record{ vart = bt-empty ; varn = varn ; varl = varl } next exit = exit node
-split_branch node@record{ vart = bt-node record { key = key ; ltree = bt-empty ; rtree = rtree } ; varn = varn ; varl = varl } next exit = exit node
-split_branch node@record{ vart = bt-node record { key = key₁ ; ltree = (bt-node record { key = record { coler = lc ; number = number } ; ltree = bt-empty ; rtree = lr }) ; rtree = rtree } ; varn = varn ; varl = varl } next exit = exit node
-split_branch node@record{ vart = bt-node record { key = key₁ ; ltree = (bt-node record { key = record { coler = black ; number = number } ; ltree = (bt-node node₁) ; rtree = lr }) ; rtree = rtree } ; varn = varn ; varl = varl } next exit = exit node
-split_branch node@record{ vart = bt-node record { key = key₁ ; ltree = (bt-node record { key = record { coler = red ; number = number₁ } ; ltree = (bt-node record { key = record { coler = black ; number = number } ; ltree = ltree ; rtree = rtree₁ }) ; rtree = lr }) ; rtree = rtree } ; varn = varn ; varl = varl } next exit = exit node
-split_branch node@record{ vart = bt-node record { key = key₁
+split-branch : {le : Level} {t : Set le} → Env → (next : Env → t) → (exit : Env → t) → t
+split-branch node@record{ vart = bt-empty ; varn = varn ; varl = varl } next exit = exit node
+split-branch node@record{ vart = bt-node record { key = key ; ltree = bt-empty ; rtree = rtree } ; varn = varn ; varl = varl } next exit = exit node
+split-branch node@record{ vart = bt-node record { key = key₁ ; ltree = (bt-node record { key = record { coler = lc ; number = number } ; ltree = bt-empty ; rtree = lr }) ; rtree = rtree } ; varn = varn ; varl = varl } next exit = exit node
+split-branch node@record{ vart = bt-node record { key = key₁ ; ltree = (bt-node record { key = record { coler = black ; number = number } ; ltree = (bt-node node₁) ; rtree = lr }) ; rtree = rtree } ; varn = varn ; varl = varl } next exit = exit node
+split-branch node@record{ vart = bt-node record { key = key₁ ; ltree = (bt-node record { key = record { coler = red ; number = number₁ } ; ltree = (bt-node record { key = record { coler = black ; number = number } ; ltree = ltree ; rtree = rtree₁ }) ; rtree = lr }) ; rtree = rtree } ; varn = varn ; varl = varl } next exit = exit node
+split-branch node@record{ vart = bt-node record { key = key₁
   ; ltree = (bt-node record { key = record { coler = red ; number = number₁ }
     ; ltree = (bt-node record { key = record { coler = red ; number = number } ; ltree = ltree ; rtree = rtree₁ })
     ; rtree = lr })
@@ -118,59 +87,16 @@
   = next node
 
 
-{-
-split_branch bt-empty n stack = bt-empty
-split_branch node@(bt-node (record { key = _; ltree = bt-empty; rtree = _}) ) n stack = node
-split_branch node@(bt-node (record { key = record { coler = y ; number = x }
-  ; ltree = (bt-node (record { key = record { coler = red ; number = rx }
-    ; ltree = (bt-node (record { key = record { coler = red ; number = rrx }; ltree = rrl; rtree = rrr }) )
-    ; rtree = lr }))
-  ; rtree = r }) ) n stack
-    = {!!}
-    --merge-rotate_right node n stack
-
-split_branch node@(bt-node (record { key = record { coler = y ; number = x }
-  ; ltree = (bt-node (record { key = record { coler = red ; number = rx }
-    ; ltree = (bt-node (record { key = record { coler = black ; number = rrx }; ltree = lll; rtree = rrr }))
-    ; rtree = lr  }) )
-  ; rtree = r }) ) n stack
-    = {!!}
-    --merge-tree node n stack
-
-split_branch node@(bt-node (record { key = record { coler = y ; number = x }
-  ; ltree = (bt-node (record { key = record { coler = red ; number = rx }
-    ; ltree =  bt-empty
-    ; rtree = rr }) )
-  ; rtree = r}) ) n stack
-    = {!!}
-    --merge-tree node n stack
-
-split_branch node@(bt-node (record { key = record { coler = y ; number = x }
-  ; ltree = (bt-node (record { key = record { coler = black ; number = rx }; ltree = rl; rtree = rr }) )
-  ; rtree = r }) ) n stack
-    = {!!}
-    --merge-tree node n stack
--}
 -- 左回転、exitはsplit_branchへ　nextもsplit_branchへ
-merge-rotate_left : {le : Level} {t : Set le} → Env → (next : Env → t) → (exit : Env → t) → t
-merge-rotate_left node@record { vart = bt-empty ; varn = varn ; varl = varl }  next exit = exit node
-merge-rotate_left node@record { vart = bt-node record { key = record { coler = coler ; number = number } ; ltree = ltree ; rtree = bt-empty } ; varn = varn ; varl = varl } next exit = exit node
-merge-rotate_left record { vart = bt-node record { key = record { coler = y ; number = x } ; ltree = l ; rtree = (bt-node record { key = record { coler = ry ; number = rx } ; ltree = rl ; rtree = rr }) } ; varn = varn ; varl = varl } next exit
+merge-rotate-left : {le : Level} {t : Set le} → Env → (next : Env → t) → (exit : Env → t) → t
+merge-rotate-left node@record { vart = bt-empty ; varn = varn ; varl = varl }  next exit = exit node
+merge-rotate-left node@record { vart = bt-node record { key = record { coler = coler ; number = number } ; ltree = ltree ; rtree = bt-empty } ; varn = varn ; varl = varl } next exit = exit node
+merge-rotate-left record { vart = bt-node record { key = record { coler = y ; number = x } ; ltree = l ; rtree = (bt-node record { key = record { coler = ry ; number = rx } ; ltree = rl ; rtree = rr }) } ; varn = varn ; varl = varl } next exit
   = next record { vart = bt-node record { key = record { coler = y ; number = rx }
   　　; ltree = (bt-node record { key = record { coler = red ; number = x } ; ltree = l ; rtree = rl })
   　　; rtree = rr}
   　　; varn = varn ; varl = varl }
 
-{-
-merge-rotate_left bt-empty n stack = bt-empty
-merge-rotate_left node@(bt-node (record { key = _; ltree = _; rtree = bt-empty }) ) n stack = node
-merge-rotate_left (bt-node (record { key = record { coler = y ; number = x }
-  ; ltree = l
-  ; rtree = (bt-node (record { key = record { coler = ry ; number = rx }; ltree = rl; rtree = rr }) ) }) ) n stack
-  = split_branch (bt-node (record { key = record { coler = y ; number = rx }
-    ; ltree = (bt-node (record { key = record { coler = red ; number = x }; ltree = l; rtree = rl }) )
-    ; rtree = rr }) ) n stack
--}
 
 -- skew exitがsplitへ　nextが左回転
 skew-bt : {le : Level} {t : Set le} → Env → (next : Env → t) → (exit : Env → t) → t
@@ -188,33 +114,17 @@
     = next node
 
 
-{-
-skew bt-empty n stack = bt-empty
-skew node@(bt-node (record { key = _; ltree = _ ; rtree = bt-empty }) ) n stack = node
-skew node@(bt-node (record { key = record { coler = y ; number = x }
-  ; ltree = l
-  ; rtree = r@(bt-node (record { key = record { coler = red ; number = lx }; ltree = ll; rtree = lr }) )}) ) n stack
-    = merge-rotate_left node n stack
-
-skew node@(bt-node (record { key = record { coler = y ; number = x }
-  ; ltree = l
-  ; rtree = (bt-node (record { key = record { coler = black ; number = lx }; ltree = ll; rtree = lr }) ) }) ) n stack
-    = split_branch node n stack
--}
-
-
--- test : {l : Level} {t : Set l} → (Code : Env → t) → t
--- test next = next (record {vart = bt-node (record { key = record { coler = red ; number = 0 }; ltree = bt-empty; rtree = bt-empty }); varn = 3; varl = []} )
-
-
-init_node_coler : Env → Env
-init_node_coler node@record { vart = bt-empty ; varn = varn ; varl = varl } = node
-init_node_coler record { vart = (bt-node record { key = record { coler = coler ; number = number } ; ltree = ltree ; rtree = rtree }) ; varn = varn ; varl = varl }
+set-node-coler : Env → Env
+set-node-coler node@record { vart = bt-empty ; varn = varn ; varl = varl } = node
+set-node-coler record { vart = (bt-node record { key = record { coler = coler ; number = number } ; ltree = ltree ; rtree = rtree }) ; varn = varn ; varl = varl }
   = record { vart = (bt-node record { key = record { coler = black ; number = number } ; ltree = ltree ; rtree = rtree }) ; varn = varn ; varl = varl }
 
-
+init-node-coler : {le : Level} {t : Set le} → Env → (next : Env → t) → (exit : Env → t) → t
+init-node-coler node@record { vart = bt-empty ; varn = varn ; varl = varl } next exit = exit node
+init-node-coler record { vart = (bt-node record { key = record { coler = coler ; number = number } ; ltree = ltree ; rtree = rtree }) ; varn = varn ; varl = varl } next exit
+  = exit record { vart = (bt-node record { key = record { coler = black ; number = number } ; ltree = ltree ; rtree = rtree }) ; varn = varn ; varl = varl }
 
-merge-tree node@record { vart = vart ; varn = varn ; varl = [] } next exit = exit (init_node_coler node)
+merge-tree node@record { vart = vart ; varn = varn ; varl = [] } next exit = exit node
 merge-tree node@record { vart = vart ; varn = varn ; varl = (bt-empty ∷ varl₁) } next exit = exit node
 merge-tree record { vart = vart ; varn = varn ; varl = (bt-node record { key = record { coler = coler ; number = number } ; ltree = ltree ; rtree = rtree } ∷ varl₁) } next exit with <-cmp varn number
 merge-tree record { vart = vart ; varn = varn ; varl = (bt-node record { key = record { coler = coler ; number = number } ; ltree = ltree ; rtree = rtree } ∷ varl₁) } next exit | tri≈ ¬a b ¬c
@@ -226,21 +136,6 @@
 merge-tree record { vart = vart ; varn = varn ; varl = (bt-node record { key = record { coler = coler ; number = number } ; ltree = ltree ; rtree = rtree } ∷ varl₁) } next exit | tri< a ¬b ¬c
   = next record { vart = (bt-node record { key = record { coler = coler ; number = number } ; ltree = vart ; rtree = rtree }) ; varn = number ; varl = varl₁ }
 
-{-
-merge-tree {le} {t} node n []  = node
-merge-tree node n (bt-empty ∷ xs) =  bt-empty
-merge-tree target n ( (bt-node (record { key = record { coler = y; number = x }; ltree = l; rtree = r }) ) ∷ xs) with <-cmp n x
-merge-tree {le} {t} target n ( (bt-node (record { key = record { coler = y; number = x }; ltree = l; rtree = r }) ) ∷ xs) | tri≈ ¬a b ¬c
-  = merge-tree {le} {t} (bt-node (record { key = record { coler = y; number = x }; ltree = l; rtree = r } ) ) x xs
-
-merge-tree {le} {t} target n ( (bt-node (record { key = record { coler = y; number = x }; ltree = l; rtree = r }) ) ∷ xs) | tri> ¬a ¬b c
-  = merge-tree {le} {t} (bt-node (record { key = record { coler = y; number = x }; ltree = l; rtree = target } ) ) x xs
-
-merge-tree {le} {t} target n ( (bt-node (record { key = record { coler = y; number = x }; ltree = l; rtree = r }) ) ∷ xs) | tri< a ¬b ¬c
-  = merge-tree {le} {t} (bt-node (record { key = record { coler = y; number = x }; ltree = target; rtree = r } ) ) x xs
--}
-
-
 
 -- insert
 bt-insert : {le : Level} {t : Set le} → Env → (next : Env → t) → (exit : Env → t) → t
@@ -264,6 +159,12 @@
 insert : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
 insert env exit = bt-insert env (λ env → insert env exit ) exit
 
+
+
+init-col : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
+init-col env exit = init-node-coler env exit exit
+
+{-
 {-# TERMINATING #-}
 merge : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
 
@@ -273,68 +174,74 @@
 
 {-# TERMINATING #-}
 rotate_right : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
-rotate_right env exit = merge-rotate_right env (λ env → split-p env (λ env → merge env exit ) ) exit
+rotate_right env exit = merge-rotate-right env (λ env → split-p env (λ env → merge env exit ) ) exit
 
 {-# TERMINATING #-}
 split-b : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
-split-b env exit = split_branch env (λ env → rotate_right env exit ) λ env → merge env exit
+split-b env exit = split-branch env (λ env → rotate_right env exit ) λ env → merge env exit
 
 {-# TERMINATING #-}
 rotate_left : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
-rotate_left env exit = merge-rotate_left env (λ env → split-b env exit ) exit
+rotate_left env exit = merge-rotate-left env (λ env → split-b env exit ) exit
 
 {-# TERMINATING #-}
 skew : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
 skew env exit = skew-bt env (λ env → rotate_left env (λ env → split-b env exit ) ) exit
 
 merge env exit = merge-tree env (λ env → skew env exit ) exit
+-}
+-- skewはnextがrotate-right。exitはsplitとなる
+-- skewの中にrotate-rightが内包され、実行後は必ずsplitに遷移する
+-- それはskewのexitと等しいので同時に記述してやる。
+skew' : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
+skew' env exit = skew-bt env (λ env → merge-rotate-left env exit exit ) exit
+
+split' : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
+split' env exit = split-branch env (λ env → merge-rotate-right env (λ env → split env exit exit ) (λ env → split env exit exit ) ) exit
 
 
--- equivalent of whileLoopP but it looks like an induction on varn
-
---whileTestP : {l : Level} {t : Set l} → (c10 : ℕ) → (c11 : ℕ) → (Code : Envc → t) → t
---whileTestP c10 n next = next (record {varn = c10 ; vari = 0 ; c10 = c10 } )
+{-
+merge' : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
+merge' node@record { vart = vart ; varn = varn ; varl = [] } exit = exit node
+merge' node@record { vart = vart ; varn = varn ; varl = (x ∷ varl₁) } exit = merge' (merge-tree node (λ env → skew' env (λ env → split' env (λ env → env) ) ) (λ env → env) ) exit
+-}
 
 whileTestP : {l : Level} {t : Set l} → (tree : rbt) → (n : ℕ) → (Code : Env → t) → t
 whileTestP tree n next = next (record {vart = tree ; varn = n ; varl = [] } )
 
-whileTestPCall : (tree : rbt) → (n : ℕ)  → Env
-whileTestPCall tree n = whileTestP {_} {_} tree n (λ env → insert env (λ env → merge env (λ env →  env)) )
+
 
-test1 = whileTestPCall bt-empty 0
-test2 = whileTestPCall (vart test1) 1
-test3 = whileTestPCall (vart test2) 2
-test4 = whileTestPCall (vart test3) 3
-test5 = whileTestPCall (vart test4) 4
-test6 = whileTestPCall (vart test5) 5
-test7 = whileTestPCall (vart test6) 6
+{-# TERMINATING #-}
+mergeP : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
+mergeP env exit = merge-tree env (λ env → skew' env (λ env → split' env (λ env → mergeP env exit)) ) exit
 
---whileTestPCall tree n = whileTestP {_} {_} tree n (λ env → merge env (λ env2 →  env2))
 {-
-bt-insert bt-empty n stack = merge-tree {le} {t} (bt-node (record { key = record { coler = red ; number = n }; ltree = bt-empty; rtree = bt-empty }) ) n stack
-bt-insert (bt-node (record { key = record { coler = y; number = x }; ltree = l; rtree = r }) ) n stack with <-cmp x n
-bt-insert (bt-node (record { key = record { coler = y; number = x }; ltree = l; rtree = r }) ) n stack | tri≈ ¬a b ¬c
-  = (bt-node (record { key = record { coler = y ; number = x }; ltree = l; rtree = r }) )
-bt-insert {le} {t} (bt-node (record { key = record { coler = y; number = x }; ltree = l; rtree = r }) ) n stack | tri> ¬a ¬b c
-  = bt-insert {le} {t} l n ( (bt-node (record { key = record { coler = y ; number = x }; ltree = bt-empty; rtree = r }) ) ∷ stack)
-bt-insert  {le} {t} (bt-node (record { key = record { coler = y; number = x }; ltree = l; rtree = r }) ) n stack | tri< a ¬b ¬c
-  = bt-insert {le} {t} r n ( (bt-node (record { key = record { coler = y ; number = x }; ltree = l; rtree = bt-empty }) ) ∷ stack )
+merge-tree env
+  (λ env → skew-bt env
+    (λ env → merge-rotate-left env
+      (λ env → split-branch env
+        (λ env →  merge-rotate-right env
+          (λ env → split env (λ env → mergeP env exit ) (λ env → mergeP env exit ) ) exit)
+      (λ env → mergeP env exit ) )
+    exit )
+  exit ) exit
 -}
 
---insert : bst → ℕ → bst
---insert node x = init_node_coler (bt-insert node x)
+--whileTestP : {l : Level} {t : Set l} → (c10 : ℕ) → (c11 : ℕ) → (Code : Envc → t) → t
+--whileTestP c10 n next = next (record {varn = c10 ; vari = 0 ; c10 = c10 } )
 
-{-
--- 以下test部分
-test-rbt1 : {le : Level} {t : Set le} → bst
-test-rbt1 {le} {t} = bt-insert {le} {t} bt-empty 0 []
+--whileTestPCall : (tree : rbt) → (n : ℕ)  → Env
+--whileTestPCall tree n = whileTestP {_} {_} tree n (λ env → insert env (λ env → merge env (λ env → init-col env (λ env → env ) ) ) )
+
+whileTestPCall' : (tree : rbt) → (n : ℕ)  → Env
+whileTestPCall' tree n = whileTestP {_} {_} tree n (λ env → insert env (λ env → mergeP env (λ env → init-col env (λ env → env ) ) ) )
 
-test-rbt2 : {le : Level} {t : Set le} → bst
-test-rbt2 {le} {t} = bt-insert {le} {t} test-rbt1 1 []
 
---test-rbt3 = bt-insert test-rbt2 2 []
---test-rbt4 = bt-insert test-rbt3 3 []
---test-rbt5 = bt-insert test-rbt4 4 []
---test-rbt6 = bt-insert test-rbt5 5 []
--}
-
+-- 以下test部分
+test1 = whileTestPCall' bt-empty 0
+test2 = whileTestPCall' (vart test1) 1
+test3 = whileTestPCall' (vart test2) 2
+test4 = whileTestPCall' (vart test3) 3
+test5 = whileTestPCall' (vart test4) 4
+test6 = whileTestPCall' (vart test5) 5
+test7 = whileTestPCall' (vart test6) 6