\chapter{Red Black Tree の実装}

Left Learning Red Black Tree の実装において、
通常の言語であれば再起処理を用いて実装を行える部分を
継続にて実行可能なように変更する必要がある。
本節では、この課題に対して Gears Agda での
Left Learning Red Black Tree の実装方法について述べる。

\section{Gears Agda での Red Black Tree の 記述}
Gears Agda にて Red Black Tree を実装する際の手順を、
下\figref{rbt_imple}を参考に説明する。

\begin{figure}[H]
  \begin{center}
    \includegraphics[height=7.5cm]{pic/imple.pdf}
  \end{center}
  \caption{再起処理を回避する手順}
  \label{rbt_imple}
\end{figure}

41の値を Left Leaning Red Black Tree に insert もしくは delete する際の手順を説明する。
まず Root node である 59 と比較した際に、41はそれより小さい。
この際、left node に遷移するが、CbC では再起処理が行えないため、listに保持していく。
順々に辿っていき、対象の場所に到達すると insert / delete を行う。
その後はlistからnodeを取り出し、結合することで Left Leaning Red Black Tree の操作を行う。

\subsection{定義した Data Gear の記述}

Left Learning Red Black Tree の記述の際に、 Code Gear
に渡している Data Gear である Env の記述を \coderef{env_imple} に示す。

\lstinputlisting[label=env_imple, caption=insertにて目的の nodeまで辿るプログラム, firstline=13, lastline=39] {src/agda/rbt_t.agda}

箇条書きにてそれぞれについて解説を行う。


\begin{itemize}
\item col: 色のことで、red と black の data 型で記述し、パターンマッチを行う。
\item node: その名の通り node に格納されている値を保存する。 色と自然数が入る
\item tree: tree の構造 を保存する。ここで node と x / right tree を持つ
\item rbt: 上3つの要素を合わせて持つことで Left Learning Red Black Tree を定義する
\item Env: rbt 以外に追加や削除を行う対象となる値と、 rbtを保存できる List を持つ Data Gear
\end{itemize}

\subsection{目的の node まで辿る Gears Agda}
上記に示した手順通りにAgdaで記述すると下 \coderef{insert_imple}のようになる。
例は insert を行う場合の記述となる。

\lstinputlisting[label=insert_imple, caption=insertにて目的の nodeまで辿るプログラム, firstline=157, lastline=166] {src/agda/rbt_t.agda}

ソースコードの解説をする。上から3行はコメントで、この関数で行っていることを doに、
next / exit では4章で述べた次の関数遷移先を記載している。

5行目にて withを使用することで vart のパターンマッチを行っている。
vart が bt-empty である場合に 6行目が動作する。
bt-empty であれば node の一番下であるため、
varn を tree の値として insert して exit に遷移する。

7行目は vart が bt-empty ではないパターンの動作を記述している。
ここでは insertを行う値である varn と 現在いる位置の tree の値と比較を行い、
再度パターンマッチを行う。

8行目は比較した結果、同値だった場合であり、そのままexitに遷移している。

9行目は入力の値 varn の方が小さい場合を指している。
vart に left tree を入れ、varl には 現在の tree から left treeを除いた
treeを追加している。それを next に遷移させている。

10行目は入力の値 varn の方が大きい場合を指している。
9行目とは逆に、vart に right tree を入れ、varl には 現在の tree から right treeを除いた
treeを追加している。それをまたnext に遷移させている。

以上の手順により、目的の node まで辿っている。

\subsection{目的の node まで辿った後の Gears Agda}
目的の node にたどり着いた後、List に格納された tree と vart の結合を行う。
Gears Agda でそれを記述すると\coderef{mearge_imple}のようになる。

\lstinputlisting[label=mearge_imple, caption=insertにて目的の nodeまで辿るプログラム, firstline=145, lastline=155] {src/agda/rbt_t.agda}
ソースコードの解説をする。
5行目にて with を使用して varl についてパターンマッチを行っている。

6行目が varl に何も入っていない場合で、実行終了のため exitに遷移している。

7行目は varl に何か入っていた場合で、ここでは varl に入っているものが
何であるのか8行目と合わせてパターンマッチを行っている。
ここでは varl に入っていたものが bt-empty であった場合について記述されている。
bt-emptyが入ってくることは実装上ありえないので、exitに遷移することで強制終了している。

8行目では varl に入っていたものが bt-empty ではなかった場合で、
それをxtreeと命名している。
ここで vart に入っている値と xtree に入っている値を比較を行い、
さらにパターンマッチを行う。

9行目が入っている値と同じ値であった場合で、
特に操作する必要がないので vart に xtree を入れ、
varl を一つ進める。

10行目は vartが大きい場合で、
varnに xtree の値を入れ、
xtree の right tree に
現在のvart を入れたものを vartにして
varlを一つ進めている。

11行目は vartが小さい場合で、
10行目と逆のことをしている。
varnに xtree の値を入れ、
xtree の left tree に
現在のvart を入れたものを vartにして
varlを一つ進めている。

以上の組み合わせを行い、
Gears Agda にて 再起処理を使わず
に Left Learning Red Black Tree の insert / delete を
記述した。


% 以上のように Tree の基本操作である insert, find, delete の実装を行った。