--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc/Interface.mm	Fri Oct 06 14:42:32 2017 +0900
@@ -0,0 +1,77 @@
+Interfaceのtypedef はコールフレームを定義する
+Interfaceの呼び出しの時に使える引数はtypedefに定義されている必要がある
+... は呼び出し側のコールフレームを保存するのに使う
+
+
+typedef struct Stack<Type, Impl>{
+        Type* stack;
+        Type* data;
+        Type* data1;
+        __code whenEmpty(...);
+        __code clear(Impl* stack,__code next(...));
+        __code push(Impl* stack,Type* data, __code next(...));
+        __code pop(Impl* stack, __code next(Type* data, ...));
+        __code pop2(Impl* stack, __code next(Type* data, Type* data1, ...));
+        __code isEmpty(Impl* stack, __code next(...), __code whenEmpty(...));
+        __code get(Impl* stack, __code next(Type* data, ...));
+        __code get2(Impl* stack, __code next(Type* data, Type* data1, ...));
+        __code next(...);
+} Stack;
+
+呼び出し方の例
+    goto nodeStack->push(newNode, replaceNode1);
+newNode はdataに対応する replaceNode1はnextに対応する。
+replaceNode1のコールフレームは...に格納される。
+つまり、replaceNode1はCodeGearのクロージャに相当する。
+
+Interfaceから値を返す場合は継続経由で値を返す
+__code get2(Impl* stack, __code next(Type* data, Type* data1, ...));
+継続の型はInterfaceで定義されていて、この型に合うCodeGearを引数として渡す
+    goto nodeStack->get2(insertCase1,tree) //意味的にはtreeの後ろに...
+
+
+__code insertCase1(struct Node *parent, struct Node *grandparent, struct RedBlackTree* tree) { //こっちも後ろに...があるはず
+
+goto next(data, data1, ...);
+
+createはinterfaceの実装を定義する
+interfaceのメソッドの番号をここで指定する
+
+implimentation側のDataGearは格納される実装依存の状態を持つ
+
+
+    struct SingleLinkedStack {
+        struct Element* top;
+    } SingleLinkedStack;
+
+Stack* createSingleLinkedStack(struct Context* context) {
+    struct Stack* stack = new Stack();
+    struct SingleLinkedStack* singleLinkedStack = new SingleLinkedStack();
+    stack->stack = (union Data*)singleLinkedStack;
+    singleLinkedStack->top = NULL;
+    stack->push = C_pushSingleLinkedStack;
+    stack->pop  = C_popSingleLinkedStack;
+    stack->pop2  = C_pop2SingleLinkedStack;
+    stack->get  = C_getSingleLinkedStack;
+    stack->get2  = C_get2SingleLinkedStack;
+    stack->isEmpty = C_isEmptySingleLinkedStack;
+    stack->clear = C_clearSingleLinkedStack;
+    return stack;
+}
+
+
+実装内部で使うCodeGearの引数はコールフレームで決まる
+コールフレームに含まれない中間変数を使っても良いが、辻褄は合ってる必要はある
+一般的にはコールフレームに含まれている引数しか書けない
+実装側の引数を書いても良い（ようにするか？）
+
+実装の状態にアクセスする時にはコールフレーム内の実装を表すDataGearから取り出してくる
+
+
+__code replaceNode1(struct RedBlackTree* tree, struct Node* node, __code next(...)) {
+
+呼び出しの例
+    goto insertNode(tree, tree->nodeStack, node);
+
+
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/parallel_execution/RedBlackTree.agda	Fri Oct 06 14:42:32 2017 +0900
@@ -0,0 +1,30 @@
+module RedBlackTree where
+
+open import stack
+
+record Tree {a t : Set} (treeImpl : Set) : Set  where
+  field
+    tree : treeImpl
+    put : treeImpl -> a -> (treeImpl -> t) -> t
+    get  : treeImpl -> (treeImpl -> Maybe a -> t) -> t
+
+record RedBlackTree (a : Set) : Set where
+  field
+    top : Maybe (Element a)
+    stack : Stack
+open RedBlackTree
+
+putRedBlackTree : {Data t : Set} -> RedBlackTree Data -> Data -> (Code : RedBlackTree Data -> t) -> t
+putRedBlackTree stack datum next = next newtree
+  where
+    element = cons datum (top stack)
+    newtree  = record {top = Just element}
+
+getRedBlackTree : {a t : Set} -> RedBlackTree a -> (Code : RedBlackTree a -> (Maybe a) -> t) -> t
+getRedBlackTree tree cs with (top tree)
+...                                | Nothing = cs tree  Nothing
+...                                | Just d  = cs stack1 (Just data1)
+  where
+    data1  = datum d
+    stack1 = record { top = (next d) }
+