# HG changeset patch # User soto # Date 1606203408 -32400 # Node ID d1d11fe2e1041f1ad591d52307936949fc80544c # Parent 5b56077a18621386bf9c6c1cb513c1ccb9cd1bed add continuation bt-insert diff -r 5b56077a1862 -r d1d11fe2e104 GearsRBTree.agda --- a/GearsRBTree.agda Mon Nov 23 15:42:10 2020 +0900 +++ b/GearsRBTree.agda Tue Nov 24 16:36:48 2020 +0900 @@ -101,6 +101,7 @@ ; ltree = (bt-node (record { key = record { coler = red ; number = x }; ltree = l; rtree = rl }) ) ; rtree = rr }) ) n stack + -- skew skew : rbt → ℕ → List rbt → rbt skew bt-empty n stack = bt-empty @@ -117,26 +118,21 @@ --treeをmerge - merge-tree node n [] = init_node_coler 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 target n ( (bt-node (record { key = record { coler = y; number = x }; ltree = l; rtree = r }) ) ∷ xs) | tri≈ ¬a b ¬c = skew (bt-node (record { key = record { coler = y; number = x }; ltree = l; rtree = r } ) ) x xs - -- merge-tree (bt-node (record { key = record { coler = y; number = x }; ltree = l; rtree = r } ) ) xs merge-tree target n ( (bt-node (record { key = record { coler = y; number = x }; ltree = l; rtree = r }) ) ∷ xs) | tri> ¬a ¬b c = skew (bt-node (record { key = record { coler = y; number = x }; ltree = l; rtree = target } ) ) x xs - -- merge-tree (bt-node (record { key = record { coler = y; number = x }; ltree = l; rtree = target } ) ) xs merge-tree target n ( (bt-node (record { key = record { coler = y; number = x }; ltree = l; rtree = r }) ) ∷ xs) | tri< a ¬b ¬c = skew (bt-node (record { key = record { coler = y; number = x }; ltree = target; rtree = r } ) ) x xs - -- merge-tree (bt-node (record { key = record { coler = y; number = x }; ltree = target; rtree = r } ) ) xs rbt-insert : rbt → ℕ → List rbt → rbt rbt-insert bt-empty n stack = merge-tree (bt-node (record { key = record { coler = red ; number = n }; ltree = bt-empty; rtree = bt-empty }) ) n stack --- ( bt-node (record { key = record { coler = red ; nu mber = n }; ltree = bt-empty; rtree = bt-empty }) ) -- mergeに遷移する rbt-insert (bt-node (record { key = record { coler = y; number = x }; ltree = l; rtree = r }) ) n stack with <-cmp x n rbt-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 }) ) diff -r 5b56077a1862 -r d1d11fe2e104 bt_t.agda --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/bt_t.agda Tue Nov 24 16:36:48 2020 +0900 @@ -0,0 +1,162 @@ +module bt_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 bst : Set where + bt-empty : bst + bt-node : (node : tree (node col ℕ) bst bst ) → bst + +record Env : Set (succ Zero) where + field + vart : bst + varn : ℕ + varl : List bst +open Env + +data Cond : Set (succ Zero) where + nextcond : Env → Cond → Cond + exitcond : Env → Cond +open Cond + + +whileTest_next : {l : Level} {t : Set l} → (c10 : bst) → (n : ℕ) → (list : List bst) → (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 + +whileTest_next1 : {l : Level} {t : Set l} → (c10 : bst) → (n : ℕ) → (list : List bst) → Cond → Cond +whileTest c10 next1 n list (nextcond x next) = {!!} +whileTest c10 next1 n list (exitcond x) = {!!} + + + +-- 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 = []} ) + +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 + = next record { vart = (bt-node record { key = record { coler = coler ; number = number } ; ltree = ltree ; rtree = rtree }) ; varn = varn ; 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 = varn ; 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 = varn ; 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 +merge env exit = merge-tree env (λ env → merge 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 : bst) → (n : ℕ) → (Code : Env → t) → t +whileTestP tree n next = next (record {vart = tree ; varn = n ; varl = [] } ) + +whileTestPCall : (tree : bst) → (n : ℕ) → Env +whileTestPCall tree n = whileTestP {_} {_} tree n (λ env → insert env (λ env → merge env (λ env → env)) ) + +test1 = whileTestPCall bt-empty 1 +test2 = whileTestPCall (vart test1) 2 + +--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 ) +-} + +init_node_coler : bst → bst +init_node_coler bt-empty = bt-empty +init_node_coler (bt-node (record { key = record { coler = y; number = x }; ltree = l; rtree = r }) ) = (bt-node (record { key = record { coler = black; number = x }; ltree = l; rtree = r }) ) + + +--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 [] +-} +