Mercurial > hg > Papers > 2021 > soto-prosym
view rbt/rbt.agda @ 14:393c839f987b default tip
DONE
author | soto <soto@cr.ie.u-ryukyu.ac.jp> |
---|---|
date | Sat, 08 Jan 2022 12:41:39 +0900 |
parents | 7ba9fa08ffb4 |
children |
line wrap: on
line source
module rbt where open import Data.Nat open import Level renaming (zero to Z ; suc to succ) open import Data.List open import Data.Nat.Properties as NatProp -- <-cmp open import Relation.Binary open import Relation.Binary.PropositionalEquality open import Relation.Nullary open import Data.Product open import Function as F hiding (const) open import Level renaming (zero to Z ; suc to succ) open import Data.Nat hiding (compare) open import Data.Nat.Properties as NatProp open import Data.Maybe -- open import Data.Maybe.Properties open import Data.Empty open import Data.List open import Data.Product open import Function as F hiding (const) open import Relation.Binary open import Relation.Binary.PropositionalEquality open import Relation.Nullary data coler : Set where red : coler black : coler data bool : Set where true : bool false : bool data rbt {n : Level} (A : Set n) : Set n where leaf : rbt A node : (key-t : ℕ) → (col : coler) → (value : A) → (ltree : rbt A ) → (rtree : rbt A ) → rbt A record Env {n : Level} (A : Set n) : Set n where field varn : ℕ varv : A vart : rbt A varl : List (rbt A) flag : bool open Env find : {n m : Level} {A : Set n} {t : Set m} → (env : Env A ) → (next : (env : Env A ) → t ) → (exit : (env : Env A ) → t ) → t find env next exit = find-c (vart env) env next exit where find-c : {n m : Level} {A : Set n} {t : Set m} → (tree : rbt A) → (env : Env A ) → (next : (env : Env A ) → t ) → (exit : (env : Env A ) → t ) → t find-c leaf env next exit = exit env find-c n@(node key-t col value ltree rtree) env next exit with <-cmp (varn env) key-t ... | tri< a ¬b ¬c = find-c ltree record env {vart = ltree ; varl = (n ∷ (varl env))} next exit ... | tri≈ ¬a b ¬c = exit record env {vart = n} ... | tri> ¬a ¬b c = find-c rtree record env {vart = rtree ; varl = (n ∷ (varl env))} next exit replaceNode1 : {n m : Level} {A : Set n} {t : Set m} → (env : Env A ) → (next : Env A → t) → t replaceNode1 env next with vart env ... | leaf = next record env {vart = (node (varn env) red (varv env) leaf leaf) } ... | node key-t col value ltree rtree = next record env {vart = (node (varn env) col (varv env) ltree rtree) } replace : {n m : Level} {A : Set n} {t : Set m} → (env : Env A ) → (next : Env A → t ) → (exit : Env A → t) → t replace env next exit = replace-c (varl env) env exit where split-c : {n m : Level} {A : Set n} {t : Set m} → Env A → (exit : Env A → t) → t split-c env exit with (vart env) ... | leaf = {!!} -- replace-c ... | node key-t col value leaf leaf = {!!} ... | node key-t col value leaf (node key-t₁ col₁ value₁ rtree rtree₁) = {!!} ... | node key-t col value (node key-t₁ col₁ value₁ ltree ltree₁) leaf = {!!} ... | node key-t col value (node key-t₁ col₁ value₁ ltree ltree₁) (node key-t₂ col₂ value₂ rtree rtree₁) = {!!} marge-left-tree : {n m : Level} {A : Set n} {t : Set m} → Env A → (exit : Env A → t) → t marge-left-tree env exit with (varl env) ... | [] = {!!} -- split ... | tree ∷ st with (vart env) ... | leaf = {!!} -- split ... | node key-t col value x x₁ = {!!} -- split rotate-left : {n m : Level} {A : Set n} {t : Set m} → (rbt A) → Env A → (next : Env A → t) → (exit : Env A → t) → t rotate-left tree env next exit with varl env ... | [] = {!!} -- split ... | tree ∷ st with vart env ... | leaf = {!!} -- split ... | node nkey-t ncol nvalue nltree nrtree with tree ... | leaf = {!!} -- split ... | node key-t col value ltree leaf = exit env ... | node key-t col value ltree rtree@(node rkey-t rcol rvalue rltree rrtree) = next record env { vart = node nkey-t ncol nvalue (node rkey-t col rvalue (node key-t red value ltree rltree) rrtree) -- ltree nrtree ; varn = varn env; varl = varl env } replace-c : {n m : Level} {A : Set n} {t : Set m} → List (rbt A) → (env : Env A) → (exit : Env A → t) → t balance_insert_left : {n m : Level} {A : Set n} {t : Set m} → List (rbt A) → (rbt A) → (env : Env A) → (exit : Env A → t ) → t balance_insert_left st tree env exit with flag env ... | true = replace-c st env exit ... | false with tree ... | leaf = {!!} -- split ... | node key-t col value leaf rtree = {!!} --split ... | node key-t col value ltree@(node lkey-t lcol lvalue lltree lrtree) rtree with lrtree ... | leaf = {!!} --split ... | (node lrkey-t black lrvalue lrltree lrrtree) = {!!} -- split ... | (node lrkey-t red lrvalue lrltree lrrtree) = rotate-left ltree env (λ env → replace-c st env exit) (λ env → {!!}) -- rotate left replace-c st env exit with st ... | [] = exit env ... | leaf ∷ st1 = replace-c st1 env exit ... | n@(node key-t col value ltree rtree) ∷ st1 with <-cmp (varn env) (key-t) ... | tri< a ¬b ¬c = balance_insert_left st1 (node key-t col value (vart env) rtree) record env{vart = (node key-t col value (vart env) rtree); varl = st1} exit -- balance left ... | tri≈ ¬a b ¬c = replace-c st1 record env{vart = (node key-t col (varv env) ltree rtree); varl = st1} exit -- そのままloop ... | tri> ¬a ¬b c = replace-c st1 record env{vart = (node key-t col value ltree (vart env)); varl = st1} exit -- balance right -- 左回転、exitはsplit_branchへ nextもsplit_branchへ rotate-left : {n m : Level} {A : Set n} {t : Set m} → Env A → (next : Env A → t) → (exit : Env A → t) → t rotate-left env next exit with vart env ... | leaf = exit env ... | node key-t col value ltree leaf = exit env ... | node key-t col value ltree rtree@(node rkey-t rcol rvalue rltree rrtree) = next record env { vart = (node rkey-t col rvalue (node key-t red value ltree rltree) rrtree) ; varn = varn env; varl = varl env } -- 右回転、実行時splitへ、それ以外はmerge-treeへ rotate-right : {n m : Level} {A : Set n} {t : Set m} → Env A → (next : Env A → t) → (exit : Env A → t) → t rotate-right env next exit with vart env ... | leaf = exit env ... | node key-t col value leaf rtree = exit env ... | node key-t col value (node lkey-t lcol lvalue lltree lrtree) rtree = next record env { vart = (node lkey-t col lvalue lltree (node key-t red value lrtree rtree) ) ; varn = varn env; varl = varl env }