Mercurial > hg > Papers > 2018 > ryokka-sigos

changeset 5:341b4c04597f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
modify section3
author ryokka
date Sun, 22 Apr 2018 20:53:49 +0900
parents d273fa70e9f6
children 4312a27022d1
files Paper/auto/sigos.el Paper/sigos.bib Paper/sigos.pdf Paper/sigos.tex Paper/src/AgdaStackSomeState.agda Paper/src/stackTest.agda
diffstat 6 files changed, 125 insertions(+), 148 deletions(-) [+]
line wrap: on
line diff
--- a/Paper/auto/sigos.el	Sun Apr 22 18:42:34 2018 +0900
+++ b/Paper/auto/sigos.el	Sun Apr 22 20:53:49 2018 +0900
@@ -6,12 +6,12 @@
    (TeX-add-to-alist 'LaTeX-provided-package-options
                      '(("graphicx" "dvipdfmx")))
    (add-to-list 'LaTeX-verbatim-environments-local "lstlisting")
-   (add-to-list 'LaTeX-verbatim-macros-with-braces-local "lstinline")
+   (add-to-list 'LaTeX-verbatim-macros-with-braces-local "path")
    (add-to-list 'LaTeX-verbatim-macros-with-braces-local "url")
-   (add-to-list 'LaTeX-verbatim-macros-with-braces-local "path")
+   (add-to-list 'LaTeX-verbatim-macros-with-braces-local "lstinline")
+   (add-to-list 'LaTeX-verbatim-macros-with-delims-local "path")
+   (add-to-list 'LaTeX-verbatim-macros-with-delims-local "url")
    (add-to-list 'LaTeX-verbatim-macros-with-delims-local "lstinline")
-   (add-to-list 'LaTeX-verbatim-macros-with-delims-local "url")
-   (add-to-list 'LaTeX-verbatim-macros-with-delims-local "path")
    (TeX-run-style-hooks
     "latex2e"
     "dummy"
@@ -31,7 +31,6 @@
     "caption")
    (LaTeX-add-labels
     "fig:cgdg"
-    "fig:meta-cgdg"
     "agda-interface-stack"
     "hoare-logic"
     "fig:hoare"
--- a/Paper/sigos.bib	Sun Apr 22 18:42:34 2018 +0900
+++ b/Paper/sigos.bib	Sun Apr 22 20:53:49 2018 +0900
@@ -23,18 +23,6 @@
   year = 2017
 }
 
-
-@Comment Reflection-Refarence                  
-@article{weko_5056_1,
-   author	 = "菅野,博靖 and 田中,二郎",
-   title	 = "非標準理論とその応用：メタ推論とリフレクション",
-   journal	 = "情報処理",
-   year 	 = "1989",
-   volume	 = "30",
-   number	 = "6",
-   month	 = "jun"
-}
-
 @Comment Agda-Reference
 
 @article{170000148438,
@@ -59,36 +47,6 @@
     note = {Accessed: 2018/2/9(Fri)}
 }
 
-@misc{coq,
-    title = {Welcome! | The Coq Proof Assistant},
-    howpublished = {\url{https://coq.inria.fr/}},
-    note = {Accessed: 2018/02/09(Fri)}
-}
-
-@misc{ats2,
-    title = {ATS-PL-SYS},
-    howpublished = {\url{http://www.ats-lang.org/}},
-    note = {Accessed: 2018/02/09(Fri)}
-}
-
-@misc{spin,
-    title = {Spin - Formal Verification},
-    howpublished = {\url{http://spinroot.com/spin/whatispin.html}},
-    note = {Accessed: 2018/02/09(Fri)}
-}
-
-@misc{nusmv,
-    title = {NuSMV home page},
-    howpublished = {\url{http://nusmv.fbk.eu/}},
-    note = {Accessed: 2018/02/09(Fri)}
-}
-
-@misc{cbmc,
-    title = {The CBMC Homepage},
-    howpublished = {\url{http://www.cprover.org/cbmc/}},
-    note = {Accessed: 2018/02/09(Fri)}
-}
-
 
 @phdthesis{norell:thesis,
   author  = {Ulf Norell},
Binary file Paper/sigos.pdf has changed
--- a/Paper/sigos.tex	Sun Apr 22 18:42:34 2018 +0900
+++ b/Paper/sigos.tex	Sun Apr 22 20:53:49 2018 +0900
@@ -10,6 +10,8 @@
 \usepackage{cite}
 \usepackage{listings}
 \usepackage{amssymb}
+%\usepackage{ucs}
+%\usepackage[utf8x]{inputenc}
 
 \lstset{
     language=C,
@@ -49,7 +51,7 @@
 \etitle{}
 
 % 所属ラベルの定義
-\affilabel{1}{琉球大学大学院理工学研究科情報工学専攻 \\Interdisciplinary Information Engineering, Graduate School of Engineering and Science, University of the Ryukyus.}
+\affilabel{1}{琉球大学大学院理工学研究科情報工学専攻 \\Interdisciplinary Information Engineering, Graduate Sc k533 hool of Engineering and Science, University of the Ryukyus.}
 \affilabel{2}{琉球大学工学部情報工学科\\Information Engineering, University of the Ryukyus.}
 
 % 和文著者名
@@ -103,11 +105,11 @@
 
 当研究室では検証の単位として CodeGear、DataGear という単位を用いてソフトウェアを
 記述する手法を提案しており、 CodeGear 、 DataGear という単位を用いてプログラミン
-グする言語として Countinuation based C\cite{kaito:2015} (以下CbC)を開発している。
+グする言語として Countinuation based C\cite{cbc} (以下CbC)を開発している。
 CbC はC言語と似た構文を持つ言語である。
-また、 CodeGear、DataGear を用いて信頼性と拡張性をメタレベルで保証する GearsOS を CbC で開発している。
+また、 CodeGear、DataGear を用いて信頼性と拡張性をメタレベルで保証する GearsOS\cite{mitsuki:2017} を CbC で開発している。
 
-本研究では検証を行うために証明支援系言語 Agda を使用している。
+本研究では検証を行うために証明支援系言語 Agda\cite{agda} を使用している。
 Agda では型で証明したい論理式を書き、その型に合った実装を記述することで証明を記
 述することができる。
  
@@ -121,7 +123,7 @@
 
 Gears OS ではプログラムとデータの単位として CodeGear、 DataGear を用いる。 Gear
  は並列実行の単位、データ分割、 Gear 間の接続等になる。
-CodeGear はプログラムの処理そのもので、図\ref{cgdg}で示しているように任意の数の
+CodeGear はプログラムの処理そのもので、図\ref{fig:cgdg}で示しているように任意の数の
 Input DataGear を参照し、処理が完了すると任意の数の Output DataGear に書き込む。
 
 CodeGear 間の移動は継続を用いて行われる。継続は関数呼び出しとは異なり、呼び出し
@@ -144,39 +146,45 @@
 CodeGear 自体も同じ型 \verb+t+ を返す関数となる。
 例えば、 Stack への push を行う関数 pushStack は以下のような型を持つ。
 
-\begin{verbatime}
+\begin{lstlisting}[caption=pushStack の型,label=push-stack]
    pushStack : a -> (Stack a si -> t) -> t
-\end{verbatime}
+\end{lstlisting}
 
 \verb+pushStack+ が関数名で、コロンの後ろに型を記述する。
 最初の引数は Stack に格納される型\verb+a+ を持つ。
 二つ目の引数は継続であり、\verb+Stack a si+ (\verb+si+という実装を持つ\verb+a+を格納するStack)を受け取り不定の型\verb+t+を返す関数である。
 この CodeGear 自体は不定の型\verb+t+を返す。
 
-GearsOS で CodeGear の性質を証明するには、 Agda で記述された CodeGear と DataGear に対してメタ計算として証明を行う。証明すべき性質は、不定の型を持つ継続 \verb+t+ に記述することができる。例えば、 Stack にある値\verb+x+をpushして、popすると \verb+ x'+ が取れてくる。Just x とJust x' は等しい必要がある。これはAgdaでは(Just x ≡ x' ) と記述される。
-ここでJustとはAgdaの以下のデータ構造である。
+GearsOS で CodeGear の性質を証明するには、 Agda で記述された CodeGear と
+DataGear に対してメタ計算として証明を行う。証明すべき性質は、不定の型を持つ継続
+\verb+t+ に記述することができる。例えば、 Stack にある値\verb+x+をpushして、pop
+すると \verb+ x'+ が取れてくる。\verb+Just x+ と\verb+Just x'+ は等しい必要があ
+る。これは Agda では \verb+(Just x ≡ x' )+ と記述される。
+ここで Just とは Agda の以下のデータ構造である。
 
-\begin{verbtim}
+% \begin{verbatim}
+\begin{lstlisting}[caption=data型の例:Maybe,label=maybe]
 data Maybe {n : Level } (a : Set n) : Set n where
   Nothing : Maybe a
   Just    : a -> Maybe a
-\end{verbtim}
+\end{lstlisting}
+% \end{verbatim}
 
-これはDataGearに相当し、Nothing と Just の二つの状態を保つ。
-popした時に、Stackが空であればNothing を返し、そうでなければJust のついた返り値を返す。
+これは DataGear に相当し、\verb+Nothing+ と \verb+Just+ の二つの状態を保つ。
+pop した時に、 Stack が空であれば\verb+Nothing+ を返し、そうでなければ\verb+Just+ のついた返り値を返す。
 
-この性質をAgda で表すと、以下のような型になる。
+この性質を Agda で表すと、以下のような型になる。
 Agda では証明すべき論理式は型で表される。
 継続部分に直接証明すべき性質を型として記述できる。
 Agda ではこの型に対応する$\lambda$項を与えると証明が完了したことになる。
 
-
-\begin{verbtim}
+\begin{lstlisting}[caption=pushとpop,label=push-pop]
    push->pop : {l : Level } {D : Set l} (x : D ) (s : SingleLinkedStack D ) ->
-       pushStack ( stackInSomeState s )  x (\s -> popStack s ( \s3 x1 -> (Just x ≡ x1 )  ))
-\end{verbtim}
+       pushStack ( stackInSomeState s )  x (\s -> popStack s ( \s3 x1 -> (Just x
+       ≡ x1 )  ))
+\end{lstlisting}
 
-このように、CodeGear を Agda で記述し、継続部分に証明すべき性質をAgda で記述する。
+このように、CodeGear を Agda で記述し、継続部分に証明すべき性質を Agda で記述する。
 
 GearsOS での記述は interface によってモジュール化される。
 このモジュール化もAgda により記述する必要がある。
@@ -184,16 +192,14 @@
 
 以下の節では、Agda の基本について復習を行う。
 
-\section{定理証明支援器 Agda での証明}
+% \section{定理証明支援器 Agda での証明}
 
 
-型システムを用いて証明を行うことができる言語として Agda \cite{agda}が存在する。
-Agda は依存型という型システムを持つ。依存型とは型も第一級オブジェクトとする型シ
-ステムで、依存型を持っている言語では型を基本的な操作に制限なしに使用できる
-。
-型システムは Curry-Howard 同型対応により命題と型付きラムダ計算が一対一で対応する。
-
-
+% 型システムを用いて証明を行うことができる言語として Agda \cite{agda}が存在する。
+% Agda は依存型という型システムを持つ。依存型とは型も第一級オブジェクトとする型シ
+% ステムで、依存型を持っている言語では型を基本的な操作に制限なしに使用できる
+% 。
+% 型システムは Curry-Howard 同型対応により命題と型付きラムダ計算が一対一で対応する。
 
 \section{Agda の文法}
 
@@ -201,89 +207,104 @@
 また、スペースの有無は厳格にチェックされる。
 
 Agda における型指定は $:$ を用いて行う。
-
-例えば、変数xが型Aを持つ、ということを表すには \verb/x : A/ と記述する。
+例えば、変数xが型Aを持つ、ということを表すには \verb+x : A+ と記述する。
 
-データ型は、代数的なデータ構造で、その定義には \verb/data/ キーワードを用いる。
-\verb/data/キーワードの後に \verb/data/ の名前と、型、 \verb/where/ 句を書きインデントを深くした後、値にコンストラクタとその型を列挙する。
-Maybe はこのdata型の例である。
+データ型は、代数的なデータ構造で、その定義には \verb+data+ キーワードを用いる。
+\verb+data+ キーワードの後に \verb+data+ の名前と、型、 \verb+where+ 句を書きインデントを深くした後、値にコンストラクタとその型を列挙する。
+Maybe(Code \ref{maybe})はこのdata型の例である。
 
+関数の定義は、関数名と型を記述した後に関数の本体を \verb+=+ の後に記述する。
+関数の型には $ \rightarrow $ 、 または\verb+->+ を用いる。
 
-関数の定義は、関数名と型を記述した後に関数の本体を \verb/=/ の後に記述する。
-関数の型には $ \rightarrow $ 、 または\verb/->/ を用いる。
-
-例えば引数が型 \verb/A/ で返り値が型 \verb/B/ の関数は \verb/A -> B/ のように書
+例えば引数が型 \verb+A+ で返り値が型 \verb+B+ の関数は \verb+A -> B+ のように書
 ける。
-また、複数の引数を取る関数の型は \verb/A -> A -> B/ のように書ける。この
-時の型は \verb/A -> (A -> B)/のように考えられる。
-Bool 変数 \verb/x/ を取って true を返す関数 \verb/f/はリスト~\ref{agda-function}のようになる。
+また、複数の引数を取る関数の型は \verb+A -> A -> B+ のように書ける。この
+時の型は \verb+A -> (A -> B)+ のように考えられる。
+前節に出てきた pushStack の型(Code \ref{push-stack})はこの例である。
+pushStack の型の本体は Code \ref{push-stack-func}のようになる。
 
-\lstinputlisting[label=agda-function, caption=Agda における関数定義] {src/AgdaFunction.agda}
+\begin{lstlisting}[caption=pushStack の関数定義,label=push-stack-func]
+  pushStack d next = push (stackMethods ) (stack ) d (\s1 -> next (record {stack = s1 ; stackMethods = stackMethods } ))
+\end{lstlisting}
+
+ここで書かれている \verb+record+ は C における構造体に相当するレコード型というデー
+タを構築しており、 \verb+record+ キーワードの後の {} の内部に \verb+fieldName = value+
+の形で値を列挙していく。複数の値を列挙する際は \verb+;+ で区切る必要がある。
 
-引数は変数名で受けることもでき、具体的なコンストラクタを指定することでそのコンストラクタが渡された時の挙動を定義できる。
-これはパターンマッチと呼ばれ、コンストラクタで case 文を行なっているようなもので
-例えば Bool 型の値を反転する \verb/not/ 関数を書くとリスト~\ref{agda-not}のようになる。
-% element の定義、縦棒　| の定義
-% SingleLinkedStack の説明に必要なものだけ
+定義を行う際は \verb+record+ のキーワード後にレコード名、型、 \verb+where+ の後
+に \verb+field+ キーワードを入れ、フィールド名と型名をを列挙する。
+\verb+record+ の定義の例として Stack のデータを操作する際に必要なレコード型のデータ
+\verb+Element+ (Code \ref{element-impl})を例とする。
 
+\verb+Element+ は単方向のリスト構造になっており、 \verb+datum+ に格納するデータ、
+\verb+next+ に次のデータを持っている。
 
-パターンマッチでは全てのコンストラクタのパターンを含まなくてはならない。
-例えば、Bool 型を受け取る関数で \verb/true/ の時の挙動のみを書くことはできない。
-なお、コンストラクタをいくつか指定した後に変数で受けると、変数が持ちうる値は指定した以外のコンストラクタとなる。
-例えばリスト~\ref{agda-pattern}の not は x には true しか入ることは無い。
-なお、マッチした値以外の挙動をまとめて書く際には \verb/_/ を用いることもできる。
+\begin{lstlisting}[caption=Element の定義,label=element-impl]
+record Element {l : Level} (a : Set l) : Set l where
+  inductive
+  constructor cons
+  field
+    datum : a  -- `data` is reserved by Agda.
+    next : Maybe (Element a)
+\end{lstlisting}
 
-\lstinputlisting[label=agda-pattern, caption=Agdaにおけるパターンマッチ] {src/AgdaPattern.agda}
+% 引数は変数名で受けることもでき、具体的なコンストラクタを指定することでそのコンストラクタが渡された時の挙動を定義できる。
+% これはパターンマッチと呼ばれ、コンストラクタで case 文を行なっているようなもので
 
-Agda にはラムダ式が存在している。ラムダ式とは関数内で生成できる無名の関数であり、
-\verb/\arg1 arg2 -> function body/ のように書くことができる。
-例えば Bool 型の引数 \verb/b/ を取って not を適用する \verb/not-apply/ をラムダ式で書くとリスト~\ref{agda-lambda}のようになる。
-関数 \verb/not-apply/ をラムダ式を使わずに定義すると \verb/not-apply-2/ になるが、この二つの関数は同一の動作をする。
-
-\lstinputlisting[label=agda-lambda, caption=Agda におけるラムダ式] {src/AgdaLambda.agda}
+%% element の定義、縦棒　| の定義
+%% SingleLinkedStack の説明に必要なものだけ
+%% push と pop だけ書いて必要なものだけ説明する
+%% testStack08 を説明する。
 
-Agda では特定の関数内のみで利用できる関数を \verb/where/ 句で記述できる。
-スコープは \verb/where/句が存在する関数内部のみであるため、名前空間が汚染させることも無い。
-例えば自然数3つを取ってそれぞれ3倍して加算する関数 \verb/f/ を定義するとき、 \verb/where/ を使うとリスト~\ref{agda-where} のように書ける。
-これは \verb/f'/ と同様の動作をする。
-\verb/where/ 句は利用したい関数の末尾にインデント付きで \verb/where/ キーワードを記述し、改行の後インデントをして関数内部で利用する関数を定義する。
+パターンマッチの説明、 | の定義、説明用のあれ。
 
-\lstinputlisting[label=agda-where, caption=Agda における where 句] {src/AgdaWhere.agda}
+\begin{lstlisting}[caption=test8,label=test8]
+testStack08 = pushSingleLinkedStack emptySingleLinkedStack 1 
+   $ \s -> pushSingleLinkedStack s 2 
+   $ \s -> pushSingleLinkedStack s 3 
+   $ \s -> pushSingleLinkedStack s 4 
+   $ \s -> pushSingleLinkedStack s 5 
+   $ \s -> top s
+\end{lstlisting}
 
-% Stackのinterface 部分を使ってrecord の説明をする
-Agda のデータには C における構造体に相当するレコード型も存在する。
-定義を行なう際は \verb/record/キーワードの後にレコード名、型、\verb/where/ の後に \verb/field/ キーワードを入れた後、フィールド名と型名を列挙する。
-例えば x と y の二つの自然数からなるレコード \verb/Point/ を定義するとリスト~\ref{agda-record}のようになる。
-レコードを構築する際は \verb/record/ キーワードの後の \verb/{}/ の内部に \verb/fieldName = value/ の形で値を列挙していく。
-複数の値を列挙する際は \verb/;/ で区切る。
+% パターンマッチでは全てのコンストラクタのパターンを含まなくてはならない。
+% 例えば、Bool 型を受け取る関数で \verb+true+ の時の挙動のみを書くことはできない。
+% なお、コンストラクタをいくつか指定した後に変数で受けると、変数が持ちうる値は指定した以外のコンストラクタとなる。
+% 例えばリスト~\ref{agda-pattern}の not は x には true しか入ることは無い。
+% なお、マッチした値以外の挙動をまとめて書く際には \verb+_+ を用いることもできる。
 
-\lstinputlisting[label=agda-record, caption=Agdaにおけるレコード型の定義] {src/AgdaRecord.agda}
+% \lstinputlisting[label=agda-pattern, caption=Agdaにおけるパターンマッチ] {src/AgdaPattern.agda}
+
+% Agda にはラムダ式が存在している。ラムダ式とは関数内で生成できる無名の関数であり、
+% \verb+\arg1 arg2 -> function body+ のように書くことができる。
+% 例えば Bool 型の引数 \verb+b+ を取って not を適用する \verb+not-apply+ をラムダ式で書くとリスト~\ref{agda-lambda}のようになる。
+% 関数 \verb+not-apply+ をラムダ式を使わずに定義すると \verb+not-apply-2+ になるが、この二つの関数は同一の動作をする。
 
-構築されたレコードから値を取得する際には \verb/RecordName.fieldName/ という名前の関数を適用する(リスト~\ref{agda-record-proj} 内2行目) 。
-なお、レコードにもパターンマッチが利用できる(リスト~\ref{agda-record-proj} 内5行目)。
-レコード内の値は \verb/record oldRecord {field = value ; ... }/ という構文を利用し更新することができる。
-Point の中の x の値を5増やす関数 \verb/xPlus5/ はリスト~\ref{agda-record-proj}の 7,8行目のように書ける。
+% \lstinputlisting[label=agda-lambda, caption=Agda におけるラムダ式] {src/AgdaLambda.agda}
 
-\lstinputlisting[label=agda-record-proj, caption=Agda におけるレコードの射影、パターンマッチ、値の更新] {src/AgdaRecordProj.agda}
+% Agda では特定の関数内のみで利用できる関数を \verb+where+ 句で記述できる。
+% スコープは \verb+where+ 句が存在する関数内部のみであるため、名前空間が汚染させることも無い。
+% 例えば自然数3つを取ってそれぞれ3倍して加算する関数 \verb+f+ を定義するとき、 \verb+where+ を使うとリスト~\ref{agda-where} のように書ける。
+% これは \verb+f'+ と同様の動作をする。
+% \verb+where+ 句は利用したい関数の末尾にインデント付きで \verb+where+ キーワードを記述し、改行の後インデントをして関数内部で利用する関数を定義する。
 
-% push と pop だけ書いて必要なものだけ説明する
-% testStack08 を説明する。
+% \lstinputlisting[label=agda-where, caption=Agda における where 句] {src/AgdaWhere.agda}
 
-\begin{itemize}
- \item 次に実行する CodeGear を指定する
- \item CodeGear に渡す DataGear を指定する
- \item 現在実行している CodeGear から制御を指定された CodeGear へと移す
-\end{itemize}
-
-の機能を持っている。
+% % Stackのinterface 部分を使ってrecord の説明をする
+% Agda のデータには C における構造体に相当するレコード型も存在する。
+% 定義を行なう際は \verb+record+キーワードの後にレコード名、型、\verb+where+ の後に \verb+field+ キーワードを入れた後、フィールド名と型名を列挙する。
+% 例えば x と y の二つの自然数からなるレコpード \verb+Point+ を定義するとリスト~\ref{agda-record}のようになる。
+% レコードを構築する際は \verb+record+ キーワードの後の \verb+{}+ の内部に \verb+fieldName = value+ の形で値を列挙していく。
+% 複数の値を列挙する際は \verb+;+ で区切る。
 
-この機能を満たす関数はソースコード\ref{agda-goto} として定義されている。
-
-\lstinputlisting[label=agda-goto, caption=Agdaにおける goto の定義] {src/Goto.agda}
+% \lstinputlisting[label=agda-record, caption=Agdaにおけるレコード型の定義] {src/AgdaRecord.agda}
 
-goto は CodeGear よりも一つ Level が上の Meta CodeGear にあたり、次に実行する
-CodeGear 型を受け取り、Input DataGear、 Output DataGear を返す。型になっている。
+% 構築されたレコードから値を取得する際には \verb+RecordName.fieldName+ という名前の関数を適用する(リスト~\ref{agda-record-proj} 内2行目) 。
+% なお、レコードにもパターンマッチが利用できる(リスト~\ref{agda-record-proj} 内5行目)。
+% レコード内の値は \verb+record oldRecord {field = value ; ... }+ という構文を利用し更新することができる。
+% Point の中の x の値を5増やす関数 \verb+xPlus5+ はリスト~\ref{agda-record-proj}の 7,8行目のように書ける。
 
+% \lstinputlisting[label=agda-record-proj, caption=Agda におけるレコードの射影、パターンマッチ、値の更新] {src/AgdaRecordProj.agda}
 
 \section{Agda での Stack、 Binary Tree の実装}
 
@@ -370,7 +391,7 @@
 タを push した後、 pop2 Interface を使って Stack に入っている 1、 2 が Stack の
 定義である First in Last out の通りに 2、 1 の順で取り出せるかを確認するために作成した。
 
-\lstinputlisting[label=agda-stack-test, caption=Agdaにおけるテスト]{src/AgdaStackTest.agda}
+%\lstinputlisting[label=agda-stack-test, caption=Agdaにおけるテスト]{src/}
 
 上の Test では、02 が 2つのデータを push し、 03 で 二つのデータを pop する pop2
 を行っている。それらをまとめて記述したものが 04 で 2 回 push し、 2つのデータを pop する動
--- a/Paper/src/AgdaStackSomeState.agda	Sun Apr 22 18:42:34 2018 +0900
+++ b/Paper/src/AgdaStackSomeState.agda	Sun Apr 22 20:53:49 2018 +0900
@@ -1,6 +1,5 @@
 stackInSomeState : {l m : Level } {D : Set l} {t : Set m } (s : SingleLinkedStack D ) -> Stack {l} {m} D {t}  ( SingleLinkedStack  D )
 stackInSomeState s =  record { stack = s ; stackMethods = singleLinkedStackSpec }
 
-push->push->pop2 : {l : Level } {D : Set l} (x y : D ) (s : SingleLinkedStack D ) ->
-pushStack ( stackInSomeState s )  x ( \s1 -> pushStack s1 y ( \s2 -> pop2Stack s2 ( \s3 y1 x1 -> (Just x ≡ x1 ) ∧ (Just y ≡ y1 ) ) ))
+push->push->pop2 : {l : Level } {D : Set l} (x y : D ) (s : SingleLinkedStack D ) -> pushStack ( stackInSomeState s )  x ( \s1 -> pushStack s1 y ( \s2 -> pop2Stack s2 ( \s3 y1 x1 -> (Just x ≡ x1 ) ∧ (Just y ≡ y1 ) ) ))
 push->push->pop2 {l} {D} x y s = record { pi1 = refl ; pi2 = refl }
--- a/Paper/src/stackTest.agda	Sun Apr 22 18:42:34 2018 +0900
+++ b/Paper/src/stackTest.agda	Sun Apr 22 20:53:49 2018 +0900
@@ -70,11 +70,11 @@
 testStack07 = pushSingleLinkedStack emptySingleLinkedStack 1 (
    \s -> pushSingleLinkedStack s 2 (\s -> top s))
 
-testStack08 = pushSingleLinkedStack emptySingleLinkedStack 1
-   $ \s -> pushSingleLinkedStack s 2
-   $ \s -> pushSingleLinkedStack s 3
-   $ \s -> pushSingleLinkedStack s 4
-   $ \s -> pushSingleLinkedStack s 5
+testStack08 = pushSingleLinkedStack emptySingleLinkedStack 1 
+   $ \s -> pushSingleLinkedStack s 2 
+   $ \s -> pushSingleLinkedStack s 3 
+   $ \s -> pushSingleLinkedStack s 4 
+   $ \s -> pushSingleLinkedStack s 5 
    $ \s -> top s
 
 ------
@@ -86,7 +86,7 @@
 --
 --    we cannot write "s ≡ s3", since level of the Set does not fit , but use stack s ≡ stack s3 is ok.
 --    anyway some implementations may result s != s3
---
+--  
 
 stackInSomeState : {l m : Level } {D : Set l} {t : Set m } (s : SingleLinkedStack D ) -> Stack {l} {m} D {t}  ( SingleLinkedStack  D )
 stackInSomeState s =  record { stack = s ; stackMethods = singleLinkedStackSpec }
@@ -103,7 +103,7 @@
 
 n-push : {n : Level} {A : Set n} {a : A} -> ℕ -> SingleLinkedStack A -> SingleLinkedStack A
 n-push zero s            = s
-n-push {l} {A} {a} (suc n) s = pushSingleLinkedStack (n-push {l} {A} {a} n s) a (\s -> s )
+n-push {l} {A} {a} (suc n) s = pushSingleLinkedStack (n-push {l} {A} {a} n s) a (\s -> s ) 
 
 n-pop :  {n : Level}{A : Set n} {a : A} -> ℕ -> SingleLinkedStack A -> SingleLinkedStack A
 n-pop zero    s         = s
@@ -120,12 +120,12 @@
    n-pop {_} {A} {a} (suc (suc n)) (pushSingleLinkedStack s a id)
   ≡⟨ refl ⟩
    popSingleLinkedStack (n-pop {_} {A} {a} (suc n) (pushSingleLinkedStack s a id)) (\s _ -> s)
-  ≡⟨ cong (\s -> popSingleLinkedStack s (\s _ -> s )) (push-and-n-pop n s) ⟩
+  ≡⟨ cong (\s -> popSingleLinkedStack s (\s _ -> s )) (push-and-n-pop n s) ⟩ 
    popSingleLinkedStack (n-pop {_} {A} {a} n s) (\s _ -> s)
   ≡⟨ refl ⟩
     n-pop {_} {A} {a} (suc n) s
   ∎
-
+  
 
 n-push-pop-equiv : {n : Level} {A : Set n} {a : A} (n : ℕ) (s : SingleLinkedStack A) -> (n-pop {_} {A} {a} n (n-push {_} {A} {a} n s)) ≡ s
 n-push-pop-equiv zero s            = refl