Mercurial > hg > Members > soto > experimental
changeset 10:ce192a384cb6
WIP add imple
| author | soto |
|---|---|
| date | Thu, 11 Feb 2021 15:35:48 +0900 |
| parents | a335a903f87d |
| children | e6a7215fb00c |
| files | .ipynb_checkpoints/Untitled-checkpoint.ipynb GearsRBTree.agdai Untitled.ipynb bt.agdai bt_t.agdai rbt_delete.agda rbt_delete.agdai rbt_imple.agda rbt_imple.agdai rbt_t.agdai test.agda test.agdai |
| diffstat | 12 files changed, 528 insertions(+), 0 deletions(-) [+] |
line wrap: on
line diff
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/.ipynb_checkpoints/Untitled-checkpoint.ipynb Thu Feb 11 15:35:48 2021 +0900 @@ -0,0 +1,6 @@ +{ + "cells": [], + "metadata": {}, + "nbformat": 4, + "nbformat_minor": 2 +}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Untitled.ipynb Thu Feb 11 15:35:48 2021 +0900 @@ -0,0 +1,251 @@ +{ + "cells": [ + { + "cell_type": "code", + "execution_count": 78, + "metadata": {}, + "outputs": [], + "source": [ + "# coding: utf-8\n", + "#\n", + "# llrbnode23.py : Left-Leaning Red Black Tree 用操作関数\n", + "# (2-3 木バージョン)\n", + "#\n", + "# Copyright (C) 2009 Makoto Hiroi\n", + "#\n", + "\n", + "# 終端\n", + "null = None\n", + "\n", + "# 色\n", + "BLACK = 0\n", + "RED = 1\n", + "\n", + "# 節\n", + "class Node:\n", + " def __init__(self, x, color = RED):\n", + " self.data = x\n", + " self.color = color\n", + " self.left = null\n", + " self.right = null\n", + "\n", + "# 終端の設定\n", + "def make_null():\n", + " global null\n", + " if null is None:\n", + " null = Node(None, BLACK)\n", + " null.left = None\n", + " null.right = None\n", + " return null\n", + "\n", + "# 右回転\n", + "def rotate_right(node):\n", + " lnode = node.left\n", + " node.left = lnode.right\n", + " lnode.right = node\n", + " lnode.color = node.color\n", + " node.color = RED\n", + " return lnode\n", + "\n", + "# 左回転\n", + "def rotate_left(node):\n", + " rnode = node.right\n", + " node.right = rnode.left\n", + " rnode.left = node\n", + " rnode.color = node.color\n", + " node.color = RED\n", + " return rnode\n", + "\n", + "\n", + "#\n", + "# データの挿入\n", + "#\n", + "\n", + "# 4 node の分割\n", + "def split(node):\n", + " node.color = RED\n", + " node.left.color = BLACK\n", + " node.right.color = BLACK\n", + "\n", + "# 挿入\n", + "def insert(node, x):\n", + " if node is null: return Node(x)\n", + " if x < node.data:\n", + " node.left = insert(node.left, x)\n", + " elif x > node.data:\n", + " node.right = insert(node.right, x)\n", + " # skew\n", + " if node.right.color == RED:\n", + " print(\"hoge\",node.right.data)\n", + " print_node(node, 0)\n", + " node = rotate_left(node)\n", + " # split\n", + " if node.left.color == RED and node.left.left.color == RED:\n", + " node = rotate_right(node)\n", + " split(node)\n", + " return node\n", + "\n", + "# 木の表示\n", + "def print_node(node, x):\n", + " if node is not null:\n", + " print_node(node.right, x + 1)\n", + " print(\" \" * x, node.color, node.data)\n", + " print_node(node.left, x + 1)\n", + "\n", + " \n" + ] + }, + { + "cell_type": "code", + "execution_count": 79, + "metadata": {}, + "outputs": [], + "source": [ + "root = make_null()" + ] + }, + { + "cell_type": "code", + "execution_count": 80, + "metadata": {}, + "outputs": [], + "source": [ + "root = insert(root, 0)\n", + "root.color = BLACK\n" + ] + }, + { + "cell_type": "code", + "execution_count": 81, + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + " 0 0\n" + ] + } + ], + "source": [ + "print_node(root, 2)\n" + ] + }, + { + "cell_type": "code", + "execution_count": 82, + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "hoge 1\n", + " 1 1\n", + " 0 0\n" + ] + } + ], + "source": [ + "root = insert(root, 1)" + ] + }, + { + "cell_type": "code", + "execution_count": 71, + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + " 0 0\n" + ] + } + ], + "source": [ + "print_node(root, 0)" + ] + }, + { + "cell_type": "code", + "execution_count": 52, + "metadata": {}, + "outputs": [ + { + "ename": "AttributeError", + "evalue": "type object 'Node' has no attribute 'make_null'", + "output_type": "error", + "traceback": [ + "\u001b[0;31m---------------------------------------------------------------------------\u001b[0m", + "\u001b[0;31mAttributeError\u001b[0m Traceback (most recent call last)", + "\u001b[0;32m<ipython-input-52-6016b722b985>\u001b[0m in \u001b[0;36m<module>\u001b[0;34m()\u001b[0m\n\u001b[0;32m----> 1\u001b[0;31m \u001b[0ma\u001b[0m\u001b[0;34m=\u001b[0m\u001b[0mNode\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mmake_null\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m", + "\u001b[0;31mAttributeError\u001b[0m: type object 'Node' has no attribute 'make_null'" + ] + } + ], + "source": [ + "a=Node.make_null()" + ] + }, + { + "cell_type": "code", + "execution_count": 43, + "metadata": {}, + "outputs": [], + "source": [ + "a = Node.insert(a, 0)" + ] + }, + { + "cell_type": "code", + "execution_count": 44, + "metadata": {}, + "outputs": [ + { + "ename": "NameError", + "evalue": "name 'print_node' is not defined", + "output_type": "error", + "traceback": [ + "\u001b[0;31m---------------------------------------------------------------------------\u001b[0m", + "\u001b[0;31mNameError\u001b[0m Traceback (most recent call last)", + "\u001b[0;32m<ipython-input-44-30dbdc80e254>\u001b[0m in \u001b[0;36m<module>\u001b[0;34m()\u001b[0m\n\u001b[0;32m----> 1\u001b[0;31m \u001b[0mNode\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mprint_node\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0ma\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0;36m0\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m", + "\u001b[0;32m<ipython-input-19-ffab890a4141>\u001b[0m in \u001b[0;36mprint_node\u001b[0;34m(node, x)\u001b[0m\n\u001b[1;32m 62\u001b[0m \u001b[0;32mdef\u001b[0m \u001b[0mprint_node\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mnode\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0mx\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 63\u001b[0m \u001b[0;32mif\u001b[0m \u001b[0mnode\u001b[0m \u001b[0;32mis\u001b[0m \u001b[0;32mnot\u001b[0m \u001b[0mnull\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m---> 64\u001b[0;31m \u001b[0mprint_node\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mnode\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mleft\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0mx\u001b[0m \u001b[0;34m+\u001b[0m \u001b[0;36m1\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m 65\u001b[0m \u001b[0mprint\u001b[0m \u001b[0;34m(\u001b[0m\u001b[0;34m\" \"\u001b[0m \u001b[0;34m*\u001b[0m \u001b[0mx\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0mnode\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mcolor\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0mnode\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mdata\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 66\u001b[0m \u001b[0mprint_node\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mnode\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mright\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0mx\u001b[0m \u001b[0;34m+\u001b[0m \u001b[0;36m1\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n", + "\u001b[0;31mNameError\u001b[0m: name 'print_node' is not defined" + ] + } + ], + "source": [ + "Node.print_node(a, 0)" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [] + } + ], + "metadata": { + "kernelspec": { + "display_name": "Python 3", + "language": "python", + "name": "python3" + }, + "language_info": { + "codemirror_mode": { + "name": "ipython", + "version": 3 + }, + "file_extension": ".py", + "mimetype": "text/x-python", + "name": "python", + "nbconvert_exporter": "python", + "pygments_lexer": "ipython3", + "version": "3.7.0" + } + }, + "nbformat": 4, + "nbformat_minor": 2 +}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/rbt_delete.agda Thu Feb 11 15:35:48 2021 +0900 @@ -0,0 +1,120 @@ +module rbt_delete where + +open import Level renaming ( suc to succ ; zero to Zero ) +open import Data.Nat hiding (compare) + +open import Data.List +open import Data.Bool + +open import Data.Nat.Properties as NatProp -- <-cmp +open import Relation.Binary -- need <-cmp relation + +open import rbt_t + +-- これあれか、またmergeする時にListにして今回はさらにbaranceも保持しないといけないのか +-- 再起処理側はmerge側に + +rbt-find : {le : Level} {t : Set le} → Env → (next : Env → t) → (exit : Env → t) → t +rbt-find env next exit with (Env.varn env) +... | n with (Env.vart env) +... | bt-empty = exit (record + { vart = bt-empty + ; varn = Env.varn env + ; varl = Env.varl env + }) +... | bt-node node with node.number (tree.key node) +... | x with <-cmp n x +... | tri≈ ¬a b ¬c = exit env +... | tri< a ¬b ¬c = next (record + { vart = tree.ltree node + ; varn = Env.varn env + ; varl = Env.varl env + }) +... | tri> ¬a ¬b c = next (record + { vart = tree.rtree node + ; varn = Env.varn env + ; varl = Env.varl env + }) + + + +-- serch min +-- exit時は終了 +-- next時は自己実行 +rbt-search-min : {le : Level} {t : Set le} → Env → (next : Env → t) → (exit : Env → t) → t +rbt-search-min env next exit with Env.vart env +... | bt-empty = exit env +... | bt-node node with tree.ltree node +... | bt-empty = exit env +... | bt-node lnode = next (record + { vart = bt-node lnode + ; varn = Env.varn env + ; varl = Env.varl env + }) + +-- find(分岐から) 分岐後、delete → balance → 終了 + +-- 右も左もenptyならreturn node をexit +-- numberが一致しているなら, next(自己実行)へ +bt-delete : {le : Level} {t : Set le} → Env → ℕ → (next : Env → t) → (exit : Env → t) → t +bt-delete env n next exit with Env.vart env +... | bt-empty = exit env +... | bt-node node with (node.number (tree.key node)) +... | num with <-cmp num n +... | tri< a ¬b ¬c = next {!!} -- listに左右どちらのbalanceなのか保持する。mergeする際にそれを参照する +... | tri> ¬a ¬b c = next {!!} -- 同上 +... | tri≈ ¬a b ¬c with node +... | record { key = key ; ltree = bt-empty ; rtree = bt-empty } = exit {!!} -- colerを赤にしてexit +... | record { key = key ; ltree = bt-node node₁ ; rtree = bt-empty } = {!!} -- leftのcolerを黒にしてexit +... | record { key = key ; ltree = ltree ; rtree = bt-node node₁ } = {!!} -- なんかやって右balance + +-- bt-delete record { vart = bt-empty ; varn = varn ; varl = varl } selfdo next exit = {!!} +-- bt-delete record { vart = (bt-node record { key = key ; ltree = ltree ; rtree = rtree }) ; varn = varn ; varl = varl } selfdo next exit = {!!} + + + +test'1 = whileTestPCall' bt-empty 0 +test'2 = whileTestPCall' (rbt_t.Env.vart test'1) 1 +test'3 = whileTestPCall' (rbt_t.Env.vart test'2) 2 +test'4 = whileTestPCall' (rbt_t.Env.vart test'3) 3 +test'5 = whileTestPCall' (rbt_t.Env.vart test'4) 4 +test'6 = whileTestPCall' (rbt_t.Env.vart test'5) 5 +test'7 = whileTestPCall' (rbt_t.Env.vart test'6) 6 +test'8 = whileTestPCall' (rbt_t.Env.vart test'7) 7 +test'9 = whileTestPCall' (rbt_t.Env.vart test'8) 8 +test'10 = whileTestPCall' (rbt_t.Env.vart test'9) 9 +test'11 = whileTestPCall' (rbt_t.Env.vart test'10) 10 +test'12 = whileTestPCall' (rbt_t.Env.vart test'11) 11 +test'13 = whileTestPCall' (rbt_t.Env.vart test'12) 12 +test'14 = whileTestPCall' (rbt_t.Env.vart test'13) 13 +test'15 = whileTestPCall' (rbt_t.Env.vart test'14) 14 + +{-# TERMINATING #-} +find-com : {l : Level} {t : Set l} → Env → (exit : Env → t) → t +find-com env exit = rbt-find env (λ env → find-com env exit ) exit + +--init +find : {l : Level} {t : Set l} → rbt → ℕ → (exit : Env → t) → t +find tree num exit = find-com (record{ vart = tree ; varn = num; varl = [] }) exit + +{-# TERMINATING #-} +search-min : {l : Level} {t : Set l} → Env → (exit : Env → t) → t +search-min env exit = rbt-search-min env (λ env → search-min env exit ) exit + +open import Agda.Builtin.Nat + +check-find : Env → ℕ → Bool +check-find tree num with Env.vart tree +... | bt-empty = false +... | bt-node node with node.number (tree.key node) +... | n = n == num + +a = search-min test'15 (λ env → env) + +b = find (Env.vart test'15) 123 (λ env → env) + + + +c = check-find (find (Env.vart test'15) 1 (λ env → env) ) 1 + +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/rbt_imple.agda Thu Feb 11 15:35:48 2021 +0900 @@ -0,0 +1,140 @@ +module rbt_imple where + +open import Level renaming ( suc to succ ; zero to Zero ) +open import Relation.Binary +open import Data.Nat hiding (_≤_ ; _≤?_) +open import Data.List hiding ([_]) +open import Data.Product +open import Data.Nat.Properties as NP + +open import rbt_t + +--このmutalの部分は別場所に書いてimportしたい。その方が綺麗に検証できそう +mutual + data right-List : Set where + [] : right-List + [_] : ℕ → right-List + _∷>_Cond_ : (x : ℕ) → (xs : right-List ) → (p : x Data.Nat.> top-r xs) → right-List + + top-r : right-List → ℕ + top-r [] = {!!} + top-r [ x ] = x + top-r (x ∷> l Cond x₁) = x + + insert-r : ℕ → right-List → right-List + insert-r x [] = [ x ] + insert-r x l@([ y ]) with <-cmp x y + ... | tri< a ¬b ¬c = l + ... | tri≈ ¬a b ¬c = l + ... | tri> ¬a ¬b c = x ∷> l Cond c + insert-r x l@(y ∷> ys Cond p) with <-cmp x y + ... | tri< a ¬b ¬c = l + ... | tri≈ ¬a b ¬c = l + ... | tri> ¬a ¬b c = x ∷> l Cond c + + data left-List : Set where + [] : left-List + [_] : ℕ -> left-List + _<∷_Cond_ : (x : ℕ) -> (xs : left-List ) -> (p : x Data.Nat.< top-l xs) -> left-List + + top-l : left-List → ℕ + top-l [] = {!!} + top-l [ x ] = x + top-l (x <∷ l Cond x₁) = x + + insert-l : ℕ -> left-List -> left-List + insert-l x [] = [ x ] + insert-l x l@([ y ]) with <-cmp x y + ... | tri< a ¬b ¬c = x <∷ l Cond a + ... | tri≈ ¬a b ¬c = l + ... | tri> ¬a ¬b c = l + insert-l x l@(y <∷ ys Cond p) with <-cmp x y + ... | tri< a ¬b ¬c = x <∷ l Cond a + ... | tri≈ ¬a b ¬c = l + ... | tri> ¬a ¬b c = l + + +record meta : Set where + field + deeps : ℕ + black-nodes : ℕ + l-list : left-List + r-list : right-List +open meta + +record tree-meta (A B C D : Set) : Set where + field + key : A + meta-data : B + ltree : C + rtree : D +open tree + +data rbt-meta : Set where + bt-empty : rbt-meta + bt-node : (node : tree-meta (node col ℕ ) meta rbt-meta rbt-meta ) → rbt-meta + +test'1 = whileTestPCall' bt-empty 0 +test'2 = whileTestPCall' (rbt_t.Env.vart test'1) 1 +test'3 = whileTestPCall' (rbt_t.Env.vart test'2) 2 +test'4 = whileTestPCall' (rbt_t.Env.vart test'3) 3 +test'5 = whileTestPCall' (rbt_t.Env.vart test'4) 4 +test'6 = whileTestPCall' (rbt_t.Env.vart test'5) 5 +test'7 = whileTestPCall' (rbt_t.Env.vart test'6) 6 +test'8 = whileTestPCall' (rbt_t.Env.vart test'7) 7 +test'9 = whileTestPCall' (rbt_t.Env.vart test'8) 8 +test'10 = whileTestPCall' (rbt_t.Env.vart test'9) 9 +test'11 = whileTestPCall' (rbt_t.Env.vart test'10) 10 +test'12 = whileTestPCall' (rbt_t.Env.vart test'11) 11 +test'13 = whileTestPCall' (rbt_t.Env.vart test'12) 12 +test'14 = whileTestPCall' (rbt_t.Env.vart test'13) 13 +test'15 = whileTestPCall' (rbt_t.Env.vart test'14) 14 + +testdata = rbt_t.Env.vart test'7 + +-- ここからmetaの作成 + +makemeta-comm : rbt_t.rbt → ℕ → meta → rbt-meta + +--make meta black nodes +makemeta-black-nodes : rbt_t.rbt → ℕ → meta → rbt-meta +makemeta-black-nodes = {!!} + +-- make meta deeps +set-black-nodes : rbt_t.rbt → meta → ℕ +set-black-nodes rbt fls with rbt +... | bt-empty = (suc (black-nodes fls) ) +... | bt-node node with (node.coler (key node)) +... | black = (suc (black-nodes fls) ) +... | red = (black-nodes fls) + +--make meta list +makemeta-comm rbt num fls with rbt +... | bt-empty = bt-empty +... | bt-node node = bt-node ( record { key = key node + ; meta-data = ( record {deeps = (deeps fls) + ; black-nodes = set-black-nodes rbt fls + ; l-list = insert-l (node.number (key node)) (l-list fls) + ; r-list = insert-r (node.number (key node)) (r-list fls) } ) + ; ltree = makemeta-comm (ltree node) (node.number (key node)) ( record { deeps = (suc (deeps fls)) + ; black-nodes = set-black-nodes rbt fls + ; l-list = insert-l (node.number (key node)) (l-list fls) + ; r-list = (r-list fls) } ) + ; rtree = makemeta-comm (rtree node) (node.number (key node)) ( record { deeps = (suc (deeps fls)) + ; black-nodes = set-black-nodes rbt fls + ; l-list = (l-list fls) + ; r-list = insert-r (node.number (key node)) (r-list fls) } ) }) + +-- init +makemeta : rbt → rbt-meta +makemeta rbt with rbt +... | bt-empty = bt-empty +... | bt-node node = bt-node ( record { key = key node + ; meta-data = ( record { deeps = 0 ; black-nodes = 1; l-list = [] ; r-list = [] } ) + ; ltree = makemeta-comm (ltree node) (node.number (key node)) + ( record { deeps = 1 ; black-nodes = 1 ; l-list = insert-l (node.number (key node)) [] ; r-list = [] } ) + ; rtree = makemeta-comm (rtree node) (node.number (key node)) + ( record { deeps = 1 ; black-nodes = 1 ; l-list = [] ; r-list = insert-r (node.number (key node)) [] } ) }) + +test11 = makemeta (rbt_t.Env.vart test'11) +