Mercurial > hg > Members > soto > experimental
view rbt_t.agda @ 7:06d03fab2668
add continuatioin rbt-insert
author | soto |
---|---|
date | Tue, 24 Nov 2020 19:28:52 +0900 |
parents | |
children | 5b398e84eae3 |
line wrap: on
line source
module rbt_t where open import Data.Nat hiding (compare) open import Data.Nat.Properties as NatProp -- <-cmp open import Relation.Binary open import Data.List -- → t を適用するために必要だった open import Level renaming ( suc to succ ; zero to Zero ) open import Level data col : Set where black : col red : col record node (A B : Set) : Set where field coler : A number : B record tree (A B C : Set) : Set where field key : A ltree : B rtree : C data rbt : Set where bt-empty : rbt bt-node : (node : tree (node col ℕ) rbt rbt ) → rbt record Env : Set (succ Zero) where field vart : rbt varn : ℕ 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} ) merge-tree : {le : Level} {t : Set le} → Env → (next : Env → t) → (exit : Env → t) → t -- 全てmerge-treeへ split : {le : Level} {t : Set le} → Env → (next : Env → t) → (exit : Env → t) → t split node@record { vart = bt-empty ; varn = varn ; varl = varl } next exit = exit node split node@record { vart = (bt-node record { key = key ; ltree = bt-empty ; rtree = rtree }) ; varn = varn ; varl = varl } next exit = exit node split node@record { vart = (bt-node record { key = key ; ltree = (bt-node node₁) ; rtree = bt-empty }) ; varn = varn ; varl = varl } next exit = exit node split record { vart = (bt-node record { key = record { coler = coler₁ ; number = number₁ } ; ltree = (bt-node record { key = record { coler = ly ; number = ln } ; ltree = ll ; rtree = lr }) ; rtree = (bt-node record { key = record { coler = ry ; number = rn } ; ltree = rl ; rtree = rr }) }) ; varn = varn ; varl = varl } next exit = next record { vart = (bt-node record { key = record { coler = red ; number = number₁ } ; ltree = (bt-node record { key = record { coler = black ; number = ln } ; ltree = ll ; rtree = lr }) ; 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 } ; ltree = (bt-node record { key = record { coler = ly ; number = lx } ; ltree = ll ; rtree = lr }) ; rtree = r } ; varn = varn ; varl = varl } next exit = next record { vart = 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 }) } ; 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₁ ; 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 }) ; rtree = rtree } ; varn = varn ; varl = varl } next exit = 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 = 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 skew-bt node@record { vart = bt-empty ; varn = varn ; varl = varl } next exit = exit node skew-bt node@record { vart = (bt-node record { key = key ; ltree = ltree ; rtree = bt-empty }) ; varn = varn ; varl = varl } next exit = exit node skew-bt node@record { vart = (bt-node record { key = key₁ ; ltree = ltree₁ ; rtree = (bt-node record { key = record { coler = black ; number = number } ; ltree = ltree ; rtree = rtree }) }) ; varn = varn ; varl = varl } next exit = exit node skew-bt node@record { vart = (bt-node record { key = key₁ ; ltree = ltree₁ ; rtree = (bt-node record { key = record { coler = red ; number = number } ; ltree = ltree ; rtree = rtree }) }) ; varn = varn ; varl = varl } next exit = 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 } = 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 = (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 = next record { vart = (bt-node record { key = record { coler = coler ; number = number } ; ltree = ltree ; rtree = rtree }) ; varn = number ; varl = varl₁ } 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 = ltree ; rtree = vart }) ; varn = number ; varl = varl₁ } 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 -- mergeへ遷移する bt-insert (record { vart = bt-empty ; varn = varn ; varl = varl }) next exit = exit (record { vart = (bt-node (record { key = record { coler = red ; number = varn }; ltree = bt-empty; rtree = bt-empty })) ; varn = varn ; varl = varl }) -- 場合分けを行う bt-insert record {vart = (bt-node record { key = record { coler = y; number = x } ; ltree = ltree ; rtree = rtree }) ; varn = n ; varl = varl } next exit with <-cmp x n bt-insert node@(record { vart = (bt-node record { key = key ; ltree = ltree ; rtree = rtree }) ; varn = varn ; varl = varl } ) next exit | tri≈ ¬a b ¬c = exit node bt-insert record {vart = (bt-node record { key = key ; ltree = ltree ; rtree = rtree }) ; varn = varn ; varl = varl } next exit | tri> ¬a ¬b c = next (record {vart = ltree ; varn = varn ; varl = (bt-node record { key = key ; ltree = bt-empty ; rtree = rtree }) ∷ varl }) bt-insert record {vart = (bt-node record { key = key ; ltree = ltree ; rtree = rtree }) ; varn = varn ; varl = varl } next exit | tri< a ¬b ¬c = next (record {vart = rtree ; varn = varn ; varl = (bt-node record { key = key ; ltree = ltree ; rtree = bt-empty }) ∷ varl }) -- normal loop without termination {-# TERMINATING #-} insert : {l : Level} {t : Set l} → Env → (exit : Env → t) → t insert env exit = bt-insert env (λ env → insert env exit ) exit {-# TERMINATING #-} merge : {l : Level} {t : Set l} → Env → (exit : Env → t) → t {-# TERMINATING #-} split-p : {l : Level} {t : Set l} → Env → (exit : Env → t) → t split-p env exit = split env (λ env → merge env (λ env → merge env exit ) ) exit {-# 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 {-# 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 {-# 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 {-# 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 -- 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 } ) 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 --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 ) -} --insert : bst → ℕ → bst --insert node x = init_node_coler (bt-insert node x) {- -- 以下test部分 test-rbt1 : {le : Level} {t : Set le} → bst test-rbt1 {le} {t} = bt-insert {le} {t} bt-empty 0 [] 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 [] -}