Binary file paper/atton-master.pdf has changed

--- a/paper/cbc-type.tex	Mon Feb 06 10:15:16 2017 +0900
+++ b/paper/cbc-type.tex	Mon Feb 06 10:32:49 2017 +0900
@@ -140,8 +140,8 @@
 % }}}
 
 % {{{ メタレベル計算の実行
-
 \section{メタレベル計算の実行}
+\label{section:meta-level-exec}
 Meta DataSegment と Meta CodeSegment の定義を行なったので、残るは実行である。
 
 実行はノーマルレベルにおいては軽量継続 \verb/goto/ を定義することによって表せた。
@@ -181,11 +181,14 @@
 
 % TODO: メタの階層構造の図
 
+また、この節で取り扱ったソースコードは付録に付す。
+
 % }}}
 
 % {{{ Agda を用いた Continuation based C の検証
 
 \section{Agda を用いた Continuation based C の検証}
+\label{section:cbc-proof}
 Agda において CbC の CodeSegment と DataSegment を定義することができた。
 実際の CbC のコードを Agda に変換し、それらの性質を証明していく。
 
@@ -231,6 +234,7 @@
 \verb/popSingleLinkedStack/ は先頭が空でなければ先頭の値を \verb/top/ から取得し、\verb/element/を一つ進める。
 値が空であれば \verb/data/ を \verb/NULL/ にしたまま軽量継続を行なう。
 
+% TODO  null check を入れる
 \lstinputlisting[label=src:cbc-push-pop, caption= CbC における SingleLinkedStack を操作する Meta CodeSegment] {src/singleLinkedStack.c}
 
 次に Agda における定義をリスト~\ref{src:agda-push-pop}に示す。
@@ -261,6 +265,7 @@
 
 % {{{ スタックの実装の検証
 \section{スタックの実装の検証}
+\label{section:stack-proof}
 定義した SingleLinkedStack に対して証明を行なっていく。
 ここでの証明は SingleLinkedStack の処理が特定の性質を持つことを保証することである。
 
@@ -435,6 +440,6 @@
 このように、CbC で記述されたプログラムを Agda 上に記述することで、データ構造の性質を定理として証明することができた。
 これらの証明機構を CbC のコンパイラやランタイム、モデルチェッカなどに組み込むことにより CbC は CbC で記述されたコードを証明することができるようになる。
 なお、本論文で取り扱っている Agda のソースコードは視認性の向上のために暗黙的な引数を省略して記述している。
-動作する完全なコードは付録に付す。 % TODO: ふろく
+動作する完全なコードは付録に付す。
 
 % }}}

--- a/paper/sources.tex	Mon Feb 06 10:15:16 2017 +0900
+++ b/paper/sources.tex	Mon Feb 06 10:32:49 2017 +0900
@@ -1,9 +1,29 @@
-\chapter{chapter:sources}
+\chapter{ソースコード一覧}
+\label{chapter:sources}
 本論文中に取り上げた Agda の動作するソースコードを示す。
 
-\section{ノーマルレベル動作の実行}
-\label{appendix:normal-level-exec}
+\section{部分型の定義}
+リスト~\ref{src:agda-subtype} に Agda 上で定義した CbC の部分型の定義を示す。
+
+\lstinputlisting[label=src:agda-subtype, caption=Agda 上で定義した CbC の部分型の定義(subtype.agda)] {src/subtype.agda}
+
+\section{ノーマルレベル計算の実行}
 \ref{section:normal-level-exec}節で取り上げたソースコードをリスト~\ref{src:normal-level-exec}に示す。
 CbC のコードにより近づけるようにA gda 上の \verb/Data.Nat/ を \verb/Int/ という名前に変更している。
 
-\lstinputlisting[label=src:normal-level-exec, caption=ノーマルレベル実行の完全なソースコード] {src/atton-master-sample.agda}
+\lstinputlisting[label=src:normal-level-exec, caption=ノーマルレベル計算例の完全なソースコード(atton-master-sample.agda)] {src/atton-master-sample.agda.replaced}
+
+\section{メタレベル計算の実行}
+\ref{section:meta-level-exec}節で取り上げたソースコードをリスト~\ref{src:meta-level-exec}に示す。
+
+\lstinputlisting[label=src:meta-level-exec, caption=メタレベル計算例の完全なソースコード(atton-master-meta-sample.agda)] {src/atton-master-meta-sample.agda.replaced}
+
+\section{Agda を用いた Continuation based C の検証}
+\ref{section:cbc-proof}節で取り上げたソースコードを以下に示す。
+
+\lstinputlisting[label=src:cbc-proof-cbc, caption=Agda を用いた Continuation based C の検証コード(SingleLinkedStack.cbc)] {src/SingleLinkedStack.cbc}
+\lstinputlisting[label=src:cbc-proof-agda, caption=Agda を用いた Continuation based C の検証コード(stack-subtype.agda)] {src/stack-subtype.agda.replaced}
+
+\section{スタックの実装の検証}
+\ref{section:stack-proof}節で取り上げたソースコードをリスト~\ref{src:stack-proof}に示す。
+\lstinputlisting[label=src:stack-proof, caption=スタックの実装の検証コード(stack-subtype-sample.agda)] {src/stack-subtype-sample.agda.replaced}

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/src/SingleLinkedStack.cbc	Mon Feb 06 10:32:49 2017 +0900
@@ -0,0 +1,111 @@
+#include "../context.h"
+#include "../origin_cs.h"
+#include <stdio.h>
+
+// typedef 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;
+}
+
+void printStack1(union Data* data) {
+    struct Node* node = &data->Element.data->Node;
+    if (node == NULL) {
+        printf("NULL");
+    } else {
+        printf("key = %d ,", node->key);
+        printStack1((union Data*)data->Element.next);
+    }
+}
+
+void printStack(union Data* data) {
+    printStack1(data);
+    printf("\n");
+}
+
+__code clearSingleLinkedStack(struct SingleLinkedStack* stack,__code next(...)) {
+    stack->top = NULL;
+    goto next(...);
+}
+
+// TODO
+__code pushSingleLinkedStack(struct SingleLinkedStack* stack,union Data* data, __code next(...)) {
+    Element* element = new Element();
+    element->next = stack->top;
+    element->data = data;
+    stack->top = element;
+    goto next(...);
+}
+
+__code popSingleLinkedStack(struct SingleLinkedStack* stack, __code next(union Data* data, ...)) {
+    if (stack->top) {
+        data = stack->top->data;
+        stack->top = stack->top->next;
+    } else {
+        data = NULL;
+    }
+    goto next(data, ...);
+}
+
+__code pop2SingleLinkedStack(struct SingleLinkedStack* stack, __code next(union Data* data, union Data* data1, ...)) {
+    if (stack->top) {
+        data = stack->top->data;
+        stack->top = stack->top->next;
+    } else {
+        data = NULL;
+    }
+    if (stack->top) {
+        data1 = stack->top->data;
+        stack->top = stack->top->next;
+    } else {
+        data1 = NULL;
+    }
+    goto next(data, data1, ...);
+}
+
+
+__code getSingleLinkedStack(struct SingleLinkedStack* stack, __code next(union Data* data, ...)) {
+    if (stack->top)
+        data = stack->top->data;
+    else
+        data = NULL;
+    goto next(data, ...);
+}
+
+__code get2SingleLinkedStack(struct SingleLinkedStack* stack, __code next(union Data* data, union Data* data1, ...)) {
+    if (stack->top) {
+        data = stack->top->data;
+        if (stack->top->next) {
+            data1 = stack->top->next->data;
+        } else {
+            data1 = NULL;
+        }
+    } else {
+        data = NULL;
+        data1 = NULL;
+    }
+    goto next(data, data1, ...);
+}
+
+__code isEmptySingleLinkedStack(struct SingleLinkedStack* stack, __code next(...), __code whenEmpty(...)) {
+    if (stack->top)
+        goto next(...);
+    else
+        goto whenEmpty(...);
+}
+
+
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/src/stack-product.agda	Mon Feb 06 10:32:49 2017 +0900
@@ -0,0 +1,158 @@
+module stack-product where
+
+open import product
+open import Data.Product
+open import Data.Nat
+open import Function using (id)
+open import Relation.Binary.PropositionalEquality
+
+-- definition based from Gears(209:5708390a9d88) src/parallel_execution
+goto = executeCS
+
+data Bool : Set where
+  True  : Bool
+  False : Bool
+
+data Maybe (a : Set) : Set  where
+  Nothing : Maybe a
+  Just    : a -> Maybe a
+
+
+record Stack {a t : Set} (stackImpl : Set) : Set  where
+  field
+    stack : stackImpl
+    push : CodeSegment (stackImpl × a × (CodeSegment stackImpl t)) t
+    pop  : CodeSegment (stackImpl × (CodeSegment (stackImpl × Maybe a) t)) t
+
+
+data Element (a : Set) : Set where
+  cons : a -> Maybe (Element a) -> Element a
+
+datum : {a : Set} -> Element a -> a
+datum (cons a _) = a
+
+next : {a : Set} -> Element a -> Maybe (Element a)
+next (cons _ n) = n
+
+record SingleLinkedStack (a : Set) : Set where
+  field
+    top : Maybe (Element a)
+open SingleLinkedStack
+
+emptySingleLinkedStack : {a : Set} -> SingleLinkedStack a
+emptySingleLinkedStack = record {top = Nothing}
+
+
+
+
+pushSingleLinkedStack : {a t : Set} -> CodeSegment ((SingleLinkedStack a) × a × (CodeSegment (SingleLinkedStack a) t)) t
+pushSingleLinkedStack = cs push
+  where
+    push : {a t : Set} -> ((SingleLinkedStack a) × a × (CodeSegment (SingleLinkedStack a) t)) -> t
+    push (stack , datum , next) = goto next stack1
+      where
+        element = cons datum (top stack)
+        stack1  = record {top = Just element}
+
+popSingleLinkedStack : {a t : Set} -> CodeSegment (SingleLinkedStack a × (CodeSegment (SingleLinkedStack a × Maybe a) t))  t
+popSingleLinkedStack = cs pop
+  where
+    pop : {a t : Set} -> (SingleLinkedStack a × (CodeSegment (SingleLinkedStack a × Maybe a) t)) -> t
+    pop (record { top = Nothing } , nextCS) = goto nextCS (emptySingleLinkedStack , Nothing) 
+    pop (record { top = Just x } , nextCS)  = goto nextCS (stack1 , (Just datum1))
+      where
+        datum1 = datum x
+        stack1 = record { top = (next x) }
+
+
+
+
+
+createSingleLinkedStack : {a b : Set} -> Stack {a} {b} (SingleLinkedStack a)
+createSingleLinkedStack = record { stack = emptySingleLinkedStack
+                                 ; push = pushSingleLinkedStack
+                                 ; pop  = popSingleLinkedStack
+                                 }
+
+
+
+
+test01 : {a : Set} -> CodeSegment (SingleLinkedStack a × Maybe a) Bool
+test01 = cs test01'
+  where
+    test01' : {a : Set} -> (SingleLinkedStack a × Maybe a) -> Bool
+    test01' (record { top = Nothing } , _) = False
+    test01' (record { top = Just x } ,  _)  = True
+
+
+test02 : {a : Set} -> CodeSegment (SingleLinkedStack a) (SingleLinkedStack a × Maybe a)
+test02 = cs test02'
+  where
+    test02' : {a : Set} -> SingleLinkedStack a -> (SingleLinkedStack a × Maybe a)
+    test02' stack = goto popSingleLinkedStack (stack , (cs id))
+
+
+test03 : {a : Set} -> CodeSegment a (SingleLinkedStack a)
+test03  = cs test03'
+  where
+    test03' : {a : Set} -> a -> SingleLinkedStack a
+    test03' a = goto pushSingleLinkedStack (emptySingleLinkedStack , a , (cs id))
+
+
+lemma : {A : Set} {a : A} -> goto (test03 ◎ test02 ◎ test01) a ≡ False
+lemma = refl
+
+
+n-push : {A : Set} {a : A} -> CodeSegment (ℕ  × SingleLinkedStack A) (ℕ × SingleLinkedStack A)
+n-push {A} {a} = cs (push {A} {a})
+  where
+    push : {A : Set} {a : A} -> (ℕ × SingleLinkedStack A) -> (ℕ × SingleLinkedStack A)
+    push {A} {a} (zero  , s) = (zero , s)
+    push {A} {a} (suc n , s) = goto pushSingleLinkedStack (s , a , {!!} {- n-push -}) -- needs subtype
+
+
+{-
+
+n-push : {A : Set} {a : A} -> Nat -> SingleLinkedStack A -> SingleLinkedStack A
+n-push zero s            = s
+n-push {A} {a} (suc n) s = pushSingleLinkedStack (n-push {A} {a} n s) a (\s -> s)
+
+n-pop : {A : Set} {a : A} -> Nat -> SingleLinkedStack A -> SingleLinkedStack A
+n-pop zero    s         = s
+n-pop {A} {a} (suc n) s = popSingleLinkedStack (n-pop {A} {a} n s) (\s _ -> s)
+
+open ≡-Reasoning
+
+push-pop-equiv : {A : Set} {a : A} (s : SingleLinkedStack A) -> popSingleLinkedStack (pushSingleLinkedStack s a (\s -> s)) (\s _ -> s) ≡ s
+push-pop-equiv s = refl
+
+push-and-n-pop : {A : Set} {a : A} (n : Nat) (s : SingleLinkedStack A) -> n-pop {A} {a} (suc n) (pushSingleLinkedStack s a id) ≡ n-pop {A} {a} n s
+push-and-n-pop zero s            = refl
+push-and-n-pop {A} {a} (suc n) s = begin
+  n-pop (suc (suc n)) (pushSingleLinkedStack s a id)
+  ≡⟨ refl ⟩
+  popSingleLinkedStack (n-pop (suc n) (pushSingleLinkedStack s a id)) (\s _ -> s)
+  ≡⟨ cong (\s -> popSingleLinkedStack s (\s _ -> s)) (push-and-n-pop n s) ⟩
+  popSingleLinkedStack (n-pop n s) (\s _ -> s)
+  ≡⟨ refl ⟩
+  n-pop (suc n) s
+  ∎
+
+
+n-push-pop-equiv : {A : Set} {a : A} (n : Nat) (s : SingleLinkedStack A) -> (n-pop {A} {a} n (n-push {A} {a} n s)) ≡ s
+n-push-pop-equiv zero s            = refl
+n-push-pop-equiv {A} {a} (suc n) s = begin
+  n-pop (suc n) (n-push (suc n) s)
+  ≡⟨ refl ⟩
+  n-pop (suc n) (pushSingleLinkedStack (n-push n s) a (\s -> s))
+  ≡⟨ push-and-n-pop n (n-push n s)  ⟩
+  n-pop n (n-push n s)
+  ≡⟨ n-push-pop-equiv n s ⟩
+  s
+  ∎
+
+
+n-push-pop-equiv-empty : {A : Set} {a : A} -> (n : Nat) -> n-pop {A} {a} n (n-push {A} {a} n emptySingleLinkedStack)  ≡ emptySingleLinkedStack
+n-push-pop-equiv-empty n = n-push-pop-equiv n emptySingleLinkedStack
+-}
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/src/stack-subtype-sample.agda	Mon Feb 06 10:32:49 2017 +0900
@@ -0,0 +1,212 @@
+module stack-subtype-sample where
+
+open import Level renaming (suc to S ; zero to O)
+open import Function
+open import Data.Nat
+open import Data.Maybe
+open import Relation.Binary.PropositionalEquality
+
+open import stack-subtype ℕ 
+open import subtype Context  as N
+open import subtype Meta     as M
+
+
+record Num : Set where
+  field
+    num : ℕ
+
+instance
+  NumIsNormalDataSegment : N.DataSegment Num
+  NumIsNormalDataSegment = record { get = (\c -> record { num = Context.n c})
+                                  ; set = (\c n -> record c {n = Num.num n})}
+  NumIsMetaDataSegment : M.DataSegment Num
+  NumIsMetaDataSegment = record { get = (\m -> record {num = Context.n (Meta.context m)})
+                                ; set = (\m n -> record m {context = record (Meta.context m) {n = Num.num n}})}
+
+
+plus3 : Num -> Num
+plus3 record { num = n } = record {num = n + 3}
+
+plus3CS : N.CodeSegment Num Num
+plus3CS = N.cs plus3
+
+
+
+plus5AndPushWithPlus3 : {mc : Meta} {{_ : N.DataSegment Num}}
+               -> M.CodeSegment Num (Meta)
+plus5AndPushWithPlus3 {mc} {{nn}} = M.cs (\n -> record {context = con n ; nextCS = (liftContext {{nn}} {{nn}} plus3CS) ; stack = st} )
+  where
+    co    = Meta.context mc
+    con : Num -> Context
+    con record { num = num } = N.DataSegment.set nn co record {num = num + 5}
+    st    = Meta.stack mc
+
+
+
+
+push-sample : {{_ : N.DataSegment Num}} {{_ : M.DataSegment Num}} ->  Meta
+push-sample {{nd}} {{md}} = M.exec {{md}} (plus5AndPushWithPlus3 {mc} {{nd}}) mc
+  where
+    con  = record { n = 4 ; element = just 0}
+    code = N.cs (\c -> c)
+    mc   = record {context = con ; stack = emptySingleLinkedStack ; nextCS = code}
+
+
+push-sample-equiv : push-sample ≡ record { nextCS  = liftContext plus3CS
+                                          ; stack   = record { top = nothing}
+                                          ; context = record { n = 9} }
+push-sample-equiv = refl
+
+
+pushed-sample : {m : Meta} {{_ : N.DataSegment Num}} {{_ : M.DataSegment Num}} ->  Meta
+pushed-sample {m} {{nd}} {{md}} = M.exec {{md}} (M.csComp {m} {{md}} pushSingleLinkedStackCS (plus5AndPushWithPlus3 {mc} {{nd}})) mc
+  where
+    con  = record { n = 4 ; element = just 0}
+    code = N.cs (\c -> c)
+    mc   = record {context = con ; stack = emptySingleLinkedStack ; nextCS = code}
+
+
+
+pushed-sample-equiv : {m : Meta} ->
+                      pushed-sample {m} ≡ record { nextCS  = liftContext plus3CS
+                                                  ; stack   = record { top = just (cons 0 nothing) }
+                                                  ; context = record { n   = 12} }
+pushed-sample-equiv = refl
+
+
+
+pushNum : N.CodeSegment Context Context
+pushNum = N.cs pn
+  where
+    pn : Context -> Context
+    pn record { n = n } = record { n = pred n  ; element = just n}
+
+
+pushOnce : Meta -> Meta
+pushOnce m = M.exec pushSingleLinkedStackCS m
+
+n-push : {m : Meta} {{_ : M.DataSegment Meta}} (n : ℕ) -> M.CodeSegment Meta Meta
+n-push {{mm}} (zero)      = M.cs {{mm}} {{mm}} id
+n-push {m} {{mm}} (suc n) = M.cs {{mm}} {{mm}} (\m -> M.exec {{mm}} {{mm}} (n-push {m} {{mm}} n) (pushOnce m))
+
+popOnce : Meta -> Meta
+popOnce m = M.exec popSingleLinkedStackCS m
+
+n-pop : {m : Meta} {{_ : M.DataSegment Meta}} (n : ℕ) -> M.CodeSegment Meta Meta
+n-pop {{mm}} (zero)      = M.cs {{mm}} {{mm}} id
+n-pop {m} {{mm}} (suc n) = M.cs {{mm}} {{mm}} (\m -> M.exec {{mm}} {{mm}} (n-pop {m} {{mm}} n) (popOnce m))
+
+
+
+initMeta : ℕ  -> Maybe ℕ -> N.CodeSegment Context Context -> Meta
+initMeta n mn code = record { context = record { n = n ; element = mn}
+                         ; stack   = emptySingleLinkedStack
+                         ; nextCS  = code
+                         }
+
+n-push-cs-exec = M.exec (n-push {meta} 3) meta
+  where
+    meta = (initMeta 5 (just 9) pushNum)
+
+
+n-push-cs-exec-equiv : n-push-cs-exec ≡ record { nextCS  = pushNum
+                                                ; context = record {n = 2 ; element = just 3}
+                                                ; stack   = record {top = just (cons 4 (just (cons 5 (just (cons 9 nothing)))))}}
+n-push-cs-exec-equiv = refl
+
+
+n-pop-cs-exec = M.exec (n-pop {meta} 4) meta
+  where
+    meta = record { nextCS  = N.cs id
+                  ; context = record { n = 0 ; element = nothing}
+                  ; stack   = record {top = just (cons 9 (just (cons 8 (just (cons 7 (just (cons 6 (just (cons 5 nothing)))))))))}
+                  }
+
+n-pop-cs-exec-equiv : n-pop-cs-exec ≡ record { nextCS  = N.cs id
+                                              ; context = record { n = 0 ; element = just 6}
+                                              ; stack   = record { top = just (cons 5 nothing)}
+                                              }
+
+n-pop-cs-exec-equiv = refl
+
+
+open ≡-Reasoning
+
+id-meta : ℕ -> ℕ -> SingleLinkedStack ℕ -> Meta
+id-meta n e s = record { context = record {n = n ; element = just e}
+                       ; nextCS = (N.cs id) ; stack = s}
+
+exec-comp : (f g : M.CodeSegment Meta Meta) (m : Meta) -> M.exec (M.csComp {m} f g) m ≡ M.exec f (M.exec g m)
+exec-comp (M.cs x) (M.cs _) m = refl
+
+
+push-pop-type : ℕ -> ℕ  -> ℕ -> Element ℕ -> Set₁
+push-pop-type n e x s = M.exec (M.csComp {meta} (M.cs popOnce) (M.cs pushOnce)) meta ≡ meta
+  where
+    meta = id-meta n e record {top = just (cons x (just s))}
+
+push-pop : (n e x : ℕ) -> (s : Element ℕ) ->  push-pop-type n e x s
+push-pop n e x s = refl
+
+
+
+pop-n-push-type : ℕ -> ℕ -> ℕ -> SingleLinkedStack ℕ -> Set₁
+pop-n-push-type n cn ce s = M.exec (M.csComp {meta} (M.cs popOnce) (n-push {meta} (suc n))) meta
+                         ≡ M.exec (n-push {meta} n) meta
+  where
+    meta = id-meta cn ce s
+
+pop-n-push : (n cn ce : ℕ) -> (s : SingleLinkedStack ℕ) -> pop-n-push-type n cn ce s
+
+pop-n-push zero cn ce s    = refl
+pop-n-push (suc n) cn ce s = begin
+  M.exec (M.csComp {id-meta cn ce s} (M.cs popOnce) (n-push {id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})} (suc (suc n)))) (id-meta cn ce s)
+  ≡⟨ refl ⟩
+  M.exec (M.csComp {id-meta cn ce s} (M.cs popOnce) (M.csComp {id-meta cn ce s} (n-push {id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})} (suc n)) (M.cs pushOnce))) (id-meta cn ce s)
+  ≡⟨ exec-comp (M.cs popOnce) (M.csComp {id-meta cn ce s} (n-push {id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})} (suc n)) (M.cs pushOnce)) (id-meta cn ce s) ⟩                        
+  M.exec (M.cs popOnce) (M.exec (M.csComp {id-meta cn ce s} (n-push {id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})} (suc n)) (M.cs pushOnce)) (id-meta cn ce s))
+  ≡⟨ cong (\x -> M.exec (M.cs popOnce) x) (exec-comp (n-push {id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})} (suc n)) (M.cs pushOnce) (id-meta cn ce s)) ⟩
+  M.exec (M.cs popOnce) (M.exec (n-push {id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})} (suc n))(M.exec (M.cs pushOnce) (id-meta cn ce s)))
+  ≡⟨ refl ⟩                                                                                                          
+  M.exec (M.cs popOnce) (M.exec (n-push {id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})} (suc n)) (id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})))
+  ≡⟨ sym (exec-comp (M.cs popOnce) (n-push {id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})} (suc n)) (id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))}))) ⟩
+  M.exec (M.csComp {id-meta cn ce s} (M.cs popOnce) (n-push {id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})} (suc n))) (id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))}))
+  ≡⟨ pop-n-push n cn ce (record {top = just (cons ce (SingleLinkedStack.top s))}) ⟩
+  M.exec (n-push n) (id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))}))
+  ≡⟨ refl ⟩
+  M.exec (n-push n) (pushOnce (id-meta cn ce s))
+  ≡⟨ refl ⟩
+  M.exec (n-push n) (M.exec (M.cs pushOnce) (id-meta cn ce s))
+  ≡⟨ refl ⟩
+  M.exec (n-push {id-meta cn ce s} (suc n)) (id-meta cn ce s)
+  ∎
+
+
+
+n-push-pop-type : ℕ ->  ℕ  -> ℕ -> SingleLinkedStack ℕ -> Set₁
+n-push-pop-type n cn ce st = M.exec (M.csComp {meta} (n-pop {meta} n) (n-push {meta} n)) meta ≡ meta
+  where
+    meta = id-meta cn ce st
+
+n-push-pop : (n cn ce : ℕ) -> (s : SingleLinkedStack ℕ) -> n-push-pop-type n cn ce s
+n-push-pop zero    cn ce s = refl
+n-push-pop (suc n) cn ce s = begin
+  M.exec (M.csComp {id-meta cn ce s} (n-pop {id-meta cn ce s}  (suc n)) (n-push {id-meta cn ce s} (suc n))) (id-meta cn ce s)
+  ≡⟨ refl ⟩
+  M.exec (M.csComp  {id-meta cn ce s}  (M.cs (\m -> M.exec (n-pop {id-meta cn ce s} n) (popOnce m))) (n-push {id-meta cn ce s} (suc n))) (id-meta cn ce s)
+  ≡⟨ exec-comp (M.cs (\m -> M.exec (n-pop n) (popOnce m))) (n-push {id-meta cn ce s}  (suc n))  (id-meta cn ce s) ⟩
+  M.exec (M.cs (\m -> M.exec (n-pop  {id-meta cn ce s}  n) (popOnce m))) (M.exec (n-push {id-meta cn ce s} (suc n)) (id-meta cn ce s))
+  ≡⟨ refl ⟩
+  M.exec (n-pop n) (popOnce (M.exec (n-push {id-meta cn ce s} (suc n)) (id-meta cn ce s)))
+  ≡⟨ refl ⟩
+  M.exec (n-pop n) (M.exec (M.cs popOnce) (M.exec (n-push {id-meta cn ce s} (suc n)) (id-meta cn ce s)))
+  ≡⟨ cong (\x -> M.exec (n-pop  {id-meta cn ce s}  n) x) (sym (exec-comp (M.cs popOnce) (n-push {id-meta cn ce s}  (suc n)) (id-meta cn ce s))) ⟩
+  M.exec (n-pop n) (M.exec (M.csComp {id-meta cn ce s} (M.cs popOnce) (n-push {id-meta cn ce s} (suc n))) (id-meta cn ce s))
+  ≡⟨ cong (\x -> M.exec (n-pop {id-meta cn ce s}  n) x) (pop-n-push n cn ce s) ⟩
+  M.exec (n-pop n) (M.exec (n-push n) (id-meta cn ce s))
+  ≡⟨ sym (exec-comp (n-pop n) (n-push n) (id-meta cn ce s)) ⟩
+  M.exec (M.csComp (n-pop n) (n-push n)) (id-meta cn ce s)
+  ≡⟨ n-push-pop n cn ce s ⟩
+  id-meta cn ce s
+  ∎
+ 

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/src/stack-subtype.agda	Mon Feb 06 10:32:49 2017 +0900
@@ -0,0 +1,123 @@
+open import Level hiding (lift)
+open import Data.Maybe
+open import Data.Product
+open import Data.Nat hiding (suc)
+open import Function
+
+module stack-subtype (A : Set) where
+
+-- data definitions
+
+data Element (a : Set) : Set where
+  cons : a -> Maybe (Element a) -> Element a
+
+datum : {a : Set} -> Element a -> a
+datum (cons a _) = a
+
+next : {a : Set} -> Element a -> Maybe (Element a)
+next (cons _ n) = n
+
+record SingleLinkedStack (a : Set) : Set where
+  field
+    top : Maybe (Element a)
+open SingleLinkedStack
+
+record Context : Set where
+  field
+    -- fields for concrete data segments
+    n       : ℕ 
+    -- fields for stack
+    element : Maybe A
+
+
+
+
+
+open import subtype Context as N
+
+instance
+  ContextIsDataSegment : N.DataSegment Context
+  ContextIsDataSegment = record {get = (\c -> c) ; set = (\_ c -> c)}
+
+
+record Meta  : Set₁ where
+  field
+    -- context as set of data segments
+    context : Context
+    stack   : SingleLinkedStack A  
+    nextCS  : N.CodeSegment Context Context
+    
+
+    
+
+open import subtype Meta as M
+
+instance
+  MetaIncludeContext : M.DataSegment Context
+  MetaIncludeContext = record { get = Meta.context
+                              ; set = (\m c -> record m {context = c}) }
+
+  MetaIsMetaDataSegment : M.DataSegment Meta
+  MetaIsMetaDataSegment  = record { get = (\m -> m) ; set = (\_ m -> m) }
+
+
+liftMeta : {X Y : Set} {{_ : M.DataSegment X}} {{_ : M.DataSegment Y}} -> N.CodeSegment X Y -> M.CodeSegment X Y
+liftMeta (N.cs f) = M.cs f
+
+liftContext : {X Y : Set} {{_ : N.DataSegment X}} {{_ : N.DataSegment Y}} -> N.CodeSegment X Y -> N.CodeSegment Context Context
+liftContext {{x}} {{y}} (N.cs f) = N.cs (\c -> N.DataSegment.set y c (f (N.DataSegment.get x c)))
+ 
+-- definition based from Gears(209:5708390a9d88) src/parallel_execution
+
+emptySingleLinkedStack : SingleLinkedStack A
+emptySingleLinkedStack = record {top = nothing}
+
+
+pushSingleLinkedStack : Meta -> Meta
+pushSingleLinkedStack m = M.exec (liftMeta n) (record m {stack = (push s e) })
+  where
+    n = Meta.nextCS m
+    s = Meta.stack  m
+    e = Context.element (Meta.context m)
+    push : SingleLinkedStack A -> Maybe A -> SingleLinkedStack A
+    push s nothing  = s
+    push s (just x) = record {top = just (cons x (top s))}
+
+
+
+popSingleLinkedStack : Meta -> Meta
+popSingleLinkedStack m = M.exec (liftMeta n) (record m {stack = (st m) ; context = record con {element = (elem m)}})
+  where
+    n = Meta.nextCS m
+    con  = Meta.context m
+    elem : Meta -> Maybe A
+    elem record {stack = record { top = (just (cons x _)) }} = just x
+    elem record {stack = record { top = nothing           }} = nothing
+    st : Meta -> SingleLinkedStack A
+    st record {stack = record { top = (just (cons _ s)) }} = record {top = s}
+    st record {stack = record { top = nothing           }} = record {top = nothing}
+   
+
+
+
+pushSingleLinkedStackCS : M.CodeSegment Meta Meta
+pushSingleLinkedStackCS = M.cs pushSingleLinkedStack
+
+popSingleLinkedStackCS : M.CodeSegment Meta Meta
+popSingleLinkedStackCS = M.cs popSingleLinkedStack
+
+
+-- for sample
+
+firstContext : Context
+firstContext = record {element = nothing ; n = 0}
+
+
+firstMeta : Meta 
+firstMeta = record { context = firstContext
+                   ; stack = emptySingleLinkedStack
+                   ; nextCS = (N.cs (\m -> m))
+                   }
+
+
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/src/subtype.agda	Mon Feb 06 10:32:49 2017 +0900
@@ -0,0 +1,44 @@
+open import Level
+open import Relation.Binary.PropositionalEquality
+
+module subtype {l : Level} (Context : Set l) where
+
+
+record DataSegment {ll : Level} (A : Set ll) : Set (l ⊔ ll) where
+  field
+    get : Context -> A
+    set : Context -> A -> Context
+open DataSegment
+
+data CodeSegment {l1 l2 : Level} (A : Set l1) (B : Set l2) : Set (l ⊔ l1 ⊔ l2) where
+  cs : {{_ : DataSegment A}} {{_ : DataSegment B}} -> (A -> B) -> CodeSegment A B
+
+goto : {l1 l2 : Level} {I : Set l1} {O : Set l2} -> CodeSegment I O -> I -> O
+goto (cs b) i = b i
+
+exec : {l1 l2 : Level} {I : Set l1} {O : Set l2} {{_ : DataSegment I}} {{_ : DataSegment O}}
+     -> CodeSegment I O -> Context -> Context
+exec {l} {{i}} {{o}}  (cs b) c = set o c (b (get i c))
+
+
+comp : {con : Context} -> {l1 l2 l3 l4 : Level}
+       {A : Set l1} {B : Set l2} {C : Set l3} {D : Set l4}
+       {{_ : DataSegment A}} {{_ : DataSegment B}} {{_ : DataSegment C}} {{_ : DataSegment D}}
+       -> (C -> D) -> (A -> B) -> A -> D
+comp {con} {{i}} {{io}} {{oi}} {{o}} g f x = g (get oi (set io con (f x)))
+
+csComp : {con : Context} -> {l1 l2 l3 l4 : Level}
+        {A : Set l1} {B : Set l2} {C : Set l3} {D : Set l4}
+         {{_ : DataSegment A}} {{_ : DataSegment B}} {{_ : DataSegment C}} {{_ : DataSegment D}}
+       -> CodeSegment C D -> CodeSegment A B -> CodeSegment A D
+csComp {con} {A} {B} {C} {D} {{da}} {{db}} {{dc}} {{dd}} (cs g) (cs f)
+      = cs {{da}} {{dd}} (comp {con} {{da}} {{db}} {{dc}} {{dd}} g f)
+
+
+
+comp-associative : {A B C D E F : Set l} {con : Context}
+                   {{da : DataSegment A}} {{db : DataSegment B}} {{dc : DataSegment C}}
+                   {{dd : DataSegment D}} {{de : DataSegment E}} {{df : DataSegment F}}
+                   -> (a : CodeSegment A B) (b : CodeSegment C D) (c : CodeSegment E F)
+                   -> csComp {con} c (csComp {con} b a)  ≡ csComp {con} (csComp {con} c b) a
+comp-associative (cs _) (cs _) (cs _) = refl