# HG changeset patch # User soto # Date 1606817057 -32400 # Node ID 5b398e84eae3ad37df5b66e223aac3ad59984e71 # Parent 06d03fab26684ff8686669e195ec019be6924537 refactoring diff -r 06d03fab2668 -r 5b398e84eae3 rbt_t.agda --- 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