\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 の実装を行った．