Mercurial > hg > Document > Growi
changeset 27:459b9fa6f047
backup 2021-01-20
| author | autobackup |
|---|---|
| date | Wed, 20 Jan 2021 00:10:03 +0900 |
| parents | f0d19eb29616 |
| children | 36c9c8f982f0 |
| files | Christie/for.NET.md user/Okud/メモ/2021/01/19.md user/anatofuz/note/2021/01/19.md user/jogo/memo/2021/01/19/jogo.md user/matac42/note/2021/01/19.md user/pine/メモ/2021/01/19.md user/soto/log/untitled.md |
| diffstat | 7 files changed, 757 insertions(+), 4 deletions(-) [+] |
line wrap: on
line diff
--- a/Christie/for.NET.md Tue Jan 19 00:10:03 2021 +0900 +++ b/Christie/for.NET.md Wed Jan 20 00:10:03 2021 +0900 @@ -320,6 +320,29 @@ https://stackoverflow.com/questions/35734051/c-sharp-task-thread-pool-running-100-tasks-across-only-10-threads --- +lockのwaitとnotifyについて +Javaでは排他制御として`synchronized(lock)`(lockはobject型)を使用することで排他制御ができる。 +解除にはlock.notifyなどを使う +https://docs.oracle.com/en/java/javase/11/docs/api/java.base/java/lang/Object.html#notify() + +C#ではMoniterクラスの中にwaitやpulse関数があり、同じように使えるっぽい +https://docs.microsoft.com/en-us/dotnet/api/system.threading.monitor.pulse?view=net-5.0 + +```java +Object lock = new Object; +synchronized(lock) { + lock.notify(); // lockの解除 +} +``` + +```c# +objecy lockObj = new object; +lock(lockObj) { + Moniter.Pulse(lock); +} +``` + +--- ## TODO * annotation → fin * daemon @@ -328,14 +351,14 @@ * AcceptThread → cgm要実装 * IncomingTcpConnection → CodeGearManager要実装 * OutboundTcpConnection → fin + * ThreadPoolExecutors 実装 * codegear * CodeGear → InputDataGear要実装 * InputDataGear * cgm要実装 * CodeGearManager - * IncomingTcpConnection要実装 - * ChristieDeamon要実装 - * ThreadPoolExecutorとは + * cg要実装 + * ThreadPoolExcuter要実装 * CodeGearExecutor * cgm要実装 * cg要実装 @@ -351,7 +374,7 @@ * DataGears → fin * WaitList → fin * LocalDataGearManager → fin - * RemoteDataGearManager → cgm要実装 + * RemoteDataGearManager → fin
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/user/Okud/メモ/2021/01/19.md Wed Jan 20 00:10:03 2021 +0900 @@ -0,0 +1,24 @@ +# Gears OS Device Driver 作成 +## 研究理由 +- OSには信頼性の保証が求められている。 +- 当研究室では、継続を基本とする言語Continuation Based Cを用いて、OSの実装を行っている。 +- Gears OSをRaspberry Piに搭載することができれば、他のハードウェアにも載せることができる。 +- Gears OSを載せたRaspberry Piはシリアル通信を用いて他のハードから入力しなければならない。 +- 直接キーボードをつないで入力できれば便利になる。 +- そこで、Gears OSのDevice Driverを作成する。 + +## やること +- UEFIからxv6をbootさせる + - qemuで再現する + - v86用の64bitUEFIでxv6をbootさせるbootloaderを参考に(https://pibvt.hateblo.jp/entry/2018/09/15/010757) + +- UEFIからUSBの値などを持ってくる + + +## 進捗 +- qemuでraspberrypiのUEFIは動いた + +## 小ネタ +- プリンタの設定をした +- 200GのSDカードが割れた +- 教科書や本をpdfにしようとしている
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/user/anatofuz/note/2021/01/19.md Wed Jan 20 00:10:03 2021 +0900 @@ -0,0 +1,509 @@ + + +# 研究目的 +- アプリケーションの信頼性を保証するには土台となるOSの信頼性を高く保証する必要がある + - しかしOSの機能をテストですべて検証するのは不可能である。 +- 定理証明やモデル検査を利用して、テストに頼らずに保証したい + - 証明しやすい形、かつ実際に動くソースコードが必要 + - 継続ベースの状態遷移系で再実装することで表現しやすくしたい +- プログラムは二つの計算に分離される + - プログラムは入力と出力の関係を決める計算(ノーマルレベル) + - その計算に必要なメタな計算(メタレベル) +- プログラムの信頼性の保証を動作しつつ行うには、メタレベルの計算を活用したい +- そのためにはメタレベルの計算を柔軟に扱うAPIや, メタレベルを保証しつつCbCを拡張した実装方法が必要 +- 本研究ではノーマル/メタレベルでの実装に適した、継続を基本とする言語Continuation Based Cを用いて、OSの実装を行い、メタ計算APIについて考察する。 + + +# 今週 +- genericsの実装あとすこし +- DPPの例題をちょいちょい修正 +- 学位審査願いを提出する必要があるらしい +- シス管とか... + +# generics +- 型と`.cbc`の書き換えを行う方針 + - どの型を生成したか覚える必要があるので、`generete_context`でまとめて変換 + +# genericsの使い方 +- 型変数として使っているケース +- 型変数に具体的な値をいれているところ(型インスタンス) +- interfaceの実装にgenericsが伝搬するケース + - しないケース + +## 型変数として使っているケース + +- この場合は`T`は型変数 + +```c +typedef struct AtomicT <T>{ + __code checkAndSet(Impl* atomic_t,T* ptr ,T init, T newData, __code next(...), __code fail(...)); + __code set(Impl* atomic_t,T* ptr ,T newData, __code next(...)); + __code next(...); + __code fail(...); +} AtomicT; +``` + +## 型インスタンス + +- Tに具体的な値`int`を埋め込んでいる + +```c +typedef struct PhilsImpl <> impl Phils { + int self; + AtomicT<int> Leftfork; + AtomicT<int> Rightfork; + __code next(...); +} PhilsImpl; +``` + +## interfaceの実装にgenericsが伝搬するケース + +- 型変数Tが共通 + - implが決まればinterfaceも決まる + +```c +typedef struct AtomicT <T>{ + __code checkAndSet(Impl* atomic_t,T* ptr ,T init, T newData, __code next(...), __code fail(...)); + __code set(Impl* atomic_t,T* ptr ,T newData, __code next(...)); + __code next(...); + __code fail(...); +} AtomicT; +``` + +```c +typedef struct AtomicTImpl <T> impl AtomicT { + T atomic; + T init; + __code next(...); +} AtomicTImpl; +``` + +## interfaceの実装にgenericsが伝搬しないケース + +- inputDataGearとしてはTはくる + - stack_generics_impl自体はTは持たない(stack_generics_impl.cbcはもつ + +```c +typedef struct StackGenerics <T> { + __code clear(Impl* stack,__code next(...)); + __code push(Impl* stack,T* data, __code next(...)); + __code pop(Impl* stack, __code next(T* data, ...)); + __code pop2(Impl* stack, __code next(T* data, T* data1, ...)); + __code isEmpty(Impl* stack, __code next(...), __code whenEmpty(...)); + __code get(Impl* stack, __code next(T* data, ...)); + __code get2(Impl* stack, __code next(T* data, T* data1, ...)); + __code next(...); + __code whenEmpty(...); +} StackGenerics; +``` + +``` +typedef struct StackGenericsImpl <T> impl StackGenerics { + __code next(...); +} StackGenericsImpl; +``` + +# .cbcに関する話 +- `AtomicT<int>`みたいに使っている場所はわかりやすく置換 +- `AtomicT<T>`を作るimplなCbCファイルはgenericsで使われている値が決まったら、その分だけ作る + - `AtomicT<int>, AtomicT<foo>` -> `AtomicT_int`, `AtomicT_foo`をつくる + - `.cbc`の中身を一度よむ -> 書き換えをする必要がある + + +# 現状 + +- 誰がどこでgenericsを使っているかは特定 +- 型インスタンス的に使っているとこの書き換えが完了 +- implのcbcの書き換えを今実装中 +- ヘッダはcontextを作る前に差し替える + +```perl +[ + [0] { + AtomicT { + _caller { + /home/anatofuz/src/firefly/hg/Gears/Gears/src/parallel_execution/../parallel_execution/AtomicT.h 1 + }, + T [ + [0] "ptr", + [1] "init", + [2] "newData" + ] + }, + AtomicTImpl { + _caller { + /home/anatofuz/src/firefly/hg/Gears/Gears/src/parallel_execution/c/AtomicTImpl.c 1, + /home/anatofuz/src/firefly/hg/Gears/Gears/src/parallel_execution/../parallel_execution/AtomicTImpl.h 1 + }, + _interface "AtomicT", + T [ + [0] "atomic", + [1] "init", + [2] "AtomicT" + ] + } + }, + [1] { + AtomicT { + int [ + [0] { + caller "/home/anatofuz/src/firefly/hg/Gears/Gears/src/parallel_execution/../parallel_execution/examples/DPP/PhilsImpl.h", + impl "PhilsImpl", + inCbC 0, + interface "Phils", + in_type_name "PhilsImpl", + vname "Leftfork" + }, + [1] { + caller "/home/anatofuz/src/firefly/hg/Gears/Gears/src/parallel_execution/../parallel_execution/examples/DPP/PhilsImpl.h", + impl "PhilsImpl", + inCbC 0, + interface "Phils", + in_type_name "PhilsImpl", + vname "Rightfork" + }, + [2] { + caller "/home/anatofuz/src/firefly/hg/Gears/Gears/src/parallel_execution/c/examples/DPP/PhilsImpl.c", + impl "PhilsImpl", + inCbC 1, + interface "Phils", + in_type_name "AtomicT", + vname "right" + }, + [3] { + caller "/home/anatofuz/src/firefly/hg/Gears/Gears/src/parallel_execution/c/examples/DPP/PhilsImpl.c", + impl "PhilsImpl", + inCbC 1, + interface "Phils", + in_type_name "AtomicT", + vname "left" + }, + [4] { + caller "/home/anatofuz/src/firefly/hg/Gears/Gears/src/parallel_execution/c/examples/DPP/main.c", + impl "AtomicTImpl", + inCbC 1, + interface "AtomicT", + in_type_name "AtomicT", + vname "AtomicT" + }, + [5] { + caller "/home/anatofuz/src/firefly/hg/Gears/Gears/src/parallel_execution/c/examples/DPP/main.c", + impl "AtomicTImpl", + inCbC 1, + interface "AtomicT", + in_type_name "AtomicT", + vname "AtomicT" + }, + [6] { + caller "/home/anatofuz/src/firefly/hg/Gears/Gears/src/parallel_execution/c/examples/DPP/main.c", + impl "AtomicTImpl", + inCbC 1, + interface "AtomicT", + in_type_name "AtomicT", + vname "AtomicT" + }, + [7] { + caller "/home/anatofuz/src/firefly/hg/Gears/Gears/src/parallel_execution/c/examples/DPP/main.c", + impl "AtomicTImpl", + inCbC 1, + interface "AtomicT", + in_type_name "AtomicT", + vname "AtomicT" + }, + [8] { + caller "/home/anatofuz/src/firefly/hg/Gears/Gears/src/parallel_execution/c/examples/DPP/main.c", + impl "AtomicTImpl", + inCbC 1, + interface "AtomicT", + in_type_name "AtomicT", + vname "AtomicT" + } + ] + } + } +] +``` + +# ここから下は作業メモ + +```perl +\ { + AtomicT { + file_path "/home/anatofuz/src/firefly/hg/Gears/Gears/src/parallel_execution/../parallel_execution/AtomicT.h", + name "AtomicT", + typed_variable [ + [0] { + type "T", + vname "ptr" + }, + [1] { + type "T", + vname "init" + }, + [2] { + type "T", + vname "newData" + } + ], + typed_variable_types { + T [ + [0] "ptr", + [1] "init", + [2] "newData" + ] + } + }, + AtomicTImpl { + file_path "/home/anatofuz/src/firefly/hg/Gears/Gears/src/parallel_execution/../parallel_execution/AtomicTImpl.h", + interface "AtomicT", + name "AtomicTImpl", + typed_variable [ + [0] { + type "T", + vname "atomic" + }, + [1] { + type "T", + vname "init" + } + ], + typed_variable_types { + T [ + [0] "atomic", + [1] "init" + ] + } + } +} +\ { + AtomicT { + caller "/home/anatofuz/src/firefly/hg/Gears/Gears/src/parallel_execution/c/examples/DPP/PhilsImpl.c", + defined_type "int", + line_number 14, + name "AtomicT" + }, + PhilsImpl { + field_defined_type [ + [0] { + generics "int", + type "AtomicT", + vname "Leftfork" + }, + [1] { + generics "int", + type "AtomicT", + vname "Rightfork" + } + ], + file_path "/home/anatofuz/src/firefly/hg/Gears/Gears/src/parallel_execution/../parallel_execution/examples/DPP/PhilsImpl.h", + interface "Phils", + name "PhilsImpl" + } +} +``` + + +```perl +\ { + StackGenerics { + file_path "/home/anatofuz/src/firefly/hg/Gears/Gears/src/parallel_execution/../parallel_execution/interface/StackGenerics.h", + name "StackGenerics", + typed_variable [ + [0] { + type "T", + vname "data" + }, + [1] { + type "T", + vname "data1" + } + ], + typed_variable_types { + T [ + [0] "data", + [1] "data1" + ] + } + } +} +\ { + StackGenerics { + caller "/home/anatofuz/src/firefly/hg/Gears/Gears/src/parallel_execution/c/examples/generics_test/main.c", + defined_type "Integer", + line_number 49, + name "StackGenerics" + } +} +``` + + + +# フロー +- `AtomicT<int>`している箇所を特定 + - `.h`と`.cbc` + - それぞれ置換していく(rename) +- `AtomicT<T>`を使っている箇所を特定 + - `.h`と`.cbc` + - この場合は本体を削除して置き換える + - 具体的なinstanceの数分作成する +- 知らないと行けないのは? + - 置換すべきファイル名 + - InterfaceかImplか + - implだったらinterfaceも書き換え? + - 同じファイルかチェックする必要がありそう + - 置換する対象 + - フィールド + - 型名 + - CodeGearの名前 + + +# 処理自体は + +```shell +$cat c/AtomicTImpl.c | perl -nle 's/<.*>//g; s/AtomicT/AtomicTInt/g; s/(AtomicT\w+)Impl/$1ImplInt/g;print' +``` + + +```perl +\ { + StackGenerics { + Integer [ + [0] { + caller "/home/anatofuz/src/firefly/hg/Gears/Gears/src/parallel_execution/c/examples/generics_test/main.c", + impl "StackGenericsImpl", + inCbC 1, + interface "StackGenerics", + in_type_name "StackGenerics", + vname "StackGenerics" + } + ] + } +} +\ { + StackGenerics { + _caller { + /home/anatofuz/src/firefly/hg/Gears/Gears/src/parallel_execution/../parallel_execution/interface/StackGenerics.h 1 + }, + T [ + [0] "data", + [1] "data1" + ] + } +} +``` + + +``` +[ + [0] { + StackGenerics { + _caller { + /home/anatofuz/src/firefly/hg/Gears/Gears/src/parallel_execution/../parallel_execution/interface/StackGenerics.h 1 + }, + T [ + [0] "data", + [1] "data1" + ] + } + }, + [1] { + StackGenerics { + Integer [ + [0] { + caller "/home/anatofuz/src/firefly/hg/Gears/Gears/src/parallel_execution/c/examples/generics_test/main.c", + impl "StackGenericsImpl", + inCbC 1, + interface "StackGenerics", + in_type_name "StackGenerics", + vname "StackGenerics" + } + ] + } + } +] +``` + + +``` ++kajika+anatofuz$ ./dpp_create_context.sh > /dev/null +\ { + /home/anatofuz/src/firefly/hg/Gears/Gears/src/parallel_execution/c/examples/DPP/main.c [ + [0] { + caller "/home/anatofuz/src/firefly/hg/Gears/Gears/src/parallel_execution/c/examples/DPP/main.c", + impl "AtomicTimpl", + inCbC 1, + interface "AtomicT", + in_type_name "AtomicT", + vname "AtomicT" + }, + [1] { + caller "/home/anatofuz/src/firefly/hg/Gears/Gears/src/parallel_execution/c/examples/DPP/main.c", + impl "AtomicTimpl", + inCbC 1, + interface "AtomicT", + in_type_name "AtomicT", + vname "AtomicT" + }, + [2] { + caller "/home/anatofuz/src/firefly/hg/Gears/Gears/src/parallel_execution/c/examples/DPP/main.c", + impl "AtomicTimpl", + inCbC 1, + interface "AtomicT", + in_type_name "AtomicT", + vname "AtomicT" + }, + [3] { + caller "/home/anatofuz/src/firefly/hg/Gears/Gears/src/parallel_execution/c/examples/DPP/main.c", + impl "AtomicTimpl", + inCbC 1, + interface "AtomicT", + in_type_name "AtomicT", + vname "AtomicT" + }, + [4] { + caller "/home/anatofuz/src/firefly/hg/Gears/Gears/src/parallel_execution/c/examples/DPP/main.c", + impl "AtomicTimpl", + inCbC 1, + interface "AtomicT", + in_type_name "AtomicT", + vname "AtomicT" + } + ], + /home/anatofuz/src/firefly/hg/Gears/Gears/src/parallel_execution/c/examples/DPP/PhilsImpl.c [ + [0] { + caller "/home/anatofuz/src/firefly/hg/Gears/Gears/src/parallel_execution/c/examples/DPP/PhilsImpl.c", + impl "PhilsImpl", + inCbC 1, + interface "Phils", + in_type_name "AtomicT", + vname "right" + }, + [1] { + caller "/home/anatofuz/src/firefly/hg/Gears/Gears/src/parallel_execution/c/examples/DPP/PhilsImpl.c", + impl "PhilsImpl", + inCbC 1, + interface "Phils", + in_type_name "AtomicT", + vname "left" + } + ], + /home/anatofuz/src/firefly/hg/Gears/Gears/src/parallel_execution/../parallel_execution/examples/DPP/PhilsImpl.h [ + [0] { + caller "/home/anatofuz/src/firefly/hg/Gears/Gears/src/parallel_execution/../parallel_execution/examples/DPP/PhilsImpl.h", + impl "PhilsImpl", + inCbC 0, + interface "Phils", + in_type_name "PhilsImpl", + vname "Leftfork" + }, + [1] { + caller "/home/anatofuz/src/firefly/hg/Gears/Gears/src/parallel_execution/../parallel_execution/examples/DPP/PhilsImpl.h", + impl "PhilsImpl", + inCbC 0, + interface "Phils", + in_type_name "PhilsImpl", + vname "Rightfork" + } + ] +} +```
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/user/jogo/memo/2021/01/19/jogo.md Wed Jan 20 00:10:03 2021 +0900 @@ -0,0 +1,17 @@ +# 研究目的 + +多段 ssh 接続を管理する sshr の改良 + +## 研究内容 + +目的のサーバにアクセスするために外部からサーバへのアクセスへは踏み台サーバからのアクセスが必要である．踏み台サーバでは外部から第三者に乗っ取られることや不特定多数の攻撃の中継地点を防止するためのものである．しかし，利用している踏み台サーバが停止すると学内での復旧作業が必要になってしまうそこで，新規踏み台サーバとしてsshrを提案する.sshrは鶴田博文氏が作成したものである．sshrはシステム管理者が組み込み可能なフック関数を用いてシステム変化に追従できるsshプロキシサーバである．本稿ではsshrを改良し弊学へ利用できるように実装をした． + +# sshrのを改良した +- openssh7.8以上の秘密鍵で認証できるように対応した． +- 本家のx/ssh/cryptoで議論されてたissueをコピペして直せた +- PR出そうとしている + + +# 不動産関連 +- 新居周りの書類，入金などが終わった. +- 気が楽になった \ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/user/matac42/note/2021/01/19.md Wed Jan 20 00:10:03 2021 +0900 @@ -0,0 +1,31 @@ +# +## 研究目的 +* 今の興味 + * 今はtokenizeとかparserとか + * vmやcontainer + * 文字列操作 + * ubuntu desktop + + * 計算とメタコンピューテーションの二つがある + * メタ計算としてプログラムの正しさをもとめる + * バージョン管理やモデル検査 + +## 調べること +* Gearsのフロントエンド +* CbCのインターフェースをサポートするperlスクリプトがある +* goto meta +* メタコンピューテーション +* GearsOSでメタ +* agdaのreflection +* agdaからCbCの生成 +* haskell to C にするやつがある +* set jumpを排除したい +* llvm builtin set jump +* setjump.hを外したいが... +* builtin setjumpを使って， +* gccとllvmのバージョンについていくお仕事 + * この作業でgccとllvmに慣れるかも +* CbCでいろいろ書くとか + * grep + * その他のライブラリ +* 上地先輩のやhokama先輩の卒論 \ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/user/pine/メモ/2021/01/19.md Wed Jan 20 00:10:03 2021 +0900 @@ -0,0 +1,27 @@ +# Gears OS +## 研究目的 +- なんとなくOSやりたい +- ファイルシステム +- x.v6のファイルシステムの書き換え + + +## 調べること +- ceph +- x.v6のファイルシステム +- docker +- vhat +- aufs +- singularity +- コンテナの強調して動くファイルシステム +- GearsOSのファイルシステムもそうであるべき +- メタコンピューテーション +- java reflection +- 圏論のモナド +- 単一モナド +- x.v6のファイルシステムのcbcで書き直す +- cephは分散ファイルシステム +- クラスター化されたファイルシステム +- christie +- jungle +- 上記2つを +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/user/soto/log/untitled.md Wed Jan 20 00:10:03 2021 +0900 @@ -0,0 +1,122 @@ +# 研究目的 + +- OSやアプリケーションの信頼性を高めることは重要な課題である。 + +- 研究室でCbCという言語を開発している。その信頼性を証明したい。 + - CbCとは、Cからループ制御構造とサブルーチンコールを取り除き、継続を導入したCの下位言語である。継続呼び出しは引数付き goto 文で表現される。 + +- cbcはサブルーチンとループ制御をcから取り除いている。その為、それを実装した際のプログラムを検証をする必要がある。 + +- プログラムの検証手法のひとつに、Hoare Logic がある。 + - これを説明すると、「プログラムの事前条件(P)が成立しているとき、コマンド(C)実行して停止すると事後条件(Q)が成り立つ」というものである。 + + - つまり、関数が任意の値が引数として実行された際に、任意の値が帰ってきた場合を「関数は正常に実行される」といえる。 + + - CbC では実行を継続するため、ある関数の実行結果は事後条件になるが、その実行結果が遷移する次の関数の事前条件になる。それを繋げていくため、個々の関数の正当性を証明することと接続の健全性について証明するだけでプログラム全体の検証を行うことができる。 + + +- cbcの実行を継続するという性質に Hoare Logicを連続して用いると、個々の関数の正当性の証明と接続の健全性について証明する事でプログラム全体の検証を行う事ができる。 + +- これらのことから、Hoare Logicを用いてCbCを検証する。 + + +- 先行研究ではCbCにおけるWhileLoopの検証を行なった。 + +- agdaが変数への再代入を許していない為、ループが存在し、かつ再代入がプログラムに含まれるデータ構造である赤黒木の検証を行う + +# 今週やった事 +- meta-dataの作成 + - 木の深さカウント(途中) + - black-nodeの数え上げ + +- 関数の実装 + - find-min(最小値を返す) + - find(値を検索する) + - delete(途中) + +## meta-dataの作成 +前回と同じく再起処理を使ってなんとかした + +## 関数の実装 + +### find-min +左ノードをみていく感じにして実装 +```Agda +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 +こちらも普通に実装 +見つかった場合とemptyに行った場合にexitしている。 +上に当てはまらない場合に大小関係によって探索する部分を切り替えている。 + +```Agda +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 + }) +``` + +見つかった場合にTrue, 存在しない場合にFalseを返すようにした。 + +### delete +実装途中。 +若干面倒ではあるができそうではある。 + +## 余談 +- 来週院試なのでスライドを作成したい。 + +# 作業ログ + +## 赤黒木のノード数を数える関数を作成する +- 深さをひとつづつ数えて、l-node,r-nodeがenptyになるまで繰り返す +- 終わったら、r-nodeとl-nodeで深さを比較、大きい方を上に上げる +- すると最終的に最大のdeepが取ってこれる。 + +deepのカウントまではできた +get-deepで深さを簡単に取れるようにできたらいいな + +## 上から数えた際の黒ノードの数え上げ +- そのノードが黒ならsucするようにする + +## metadetaの作成をどうしようか +方法としては以下が挙げられる +- 全て同時にやる方法 + - コードが冗長になる… +- ひとつづつやる方法 + - ひとつづつやるには、作らない部分のフィールドにNanを入れてやらないといけない + +~~同時にやる方を採用してみる~~\ +最初にフィールド変数として持っておいて、 +ひとつづつ編集していく方式の方が綺麗そう + +## node数の数え上げ +加えてlog_2 nする関数を作成しないといけない +