Mercurial > hg > Papers > 2018 > ryokka-sigos

--- a/Paper/Makefile	Mon Apr 23 19:06:07 2018 +0900
+++ b/Paper/Makefile	Mon Apr 23 21:44:32 2018 +0900
@@ -1,35 +1,44 @@
-TARGET = sigos
+# Settings
+TARGET=sigos
+BIBTEX=pbibtex
+BB=extractbb

-LATEX   = platex
-BIBTEX  = pbibtex
-#DVIPS   = dvips
-#DVIPDFM = dvipdfmx
-RM      = rm -f
-DVIPDF=dvipdfmx -p a4
-#  Option definitions
-#DVIPDFMOPT =
-#DVIPSOPT   = -D 720 -mode esphi -O 0mm,0mm -N0
+vpath pdf fig
+FIGURES=$(wildcard fig/*.pdf)
+FIGURES_FOR_TEX=$(subst .pdf,.xbb,$(FIGURES))
+
+vpath agda src
+SOURCES=$(wildcard src/*agda)
+SOURCES_FOR_TEX=$(subst .agda,.agda.replaced,$(SOURCES))

-#  Suffixes definitions
-.SUFFIXES: .tex .dvi .pdf
+# dependencies
+$(TARGET).pdf : $(TARGET).dvi
+	dvipdfmx $<

-.tex.dvi:
-	$(LATEX) $<
+$(TARGET).dvi : $(wildcard *.tex) $(FIGURES_FOR_TEX) $(SOURCES_FOR_TEX)
+	platex  $(TARGET).tex
 	$(BIBTEX) $(TARGET)
-	$(LATEX) $<
-	$(LATEX) $<
+	platex  $(TARGET).tex
+	platex  $(TARGET).tex

-.dvi.pdf:
-	$(DVIPDF) $(DVIPDF_OPT) $<
+%.xbb: %.pdf
+	$(BB) $<
+
+%.agda.replaced: %.agda
+	ruby escape_agda.rb $<


+# commands
+.PHONY : clean all open remake
+
+clean:
+	rm -f *.dvi *.aux *.log *.pdf *.ps *.gz *.bbl *.blg *.toc *~ *.core *.cpt *.lof *.lot *.lol *.bbl *.blg *.idx src/*.replaced
+
 all: $(TARGET).pdf
+
+open: $(TARGET).pdf
 	open $(TARGET).pdf

-dvi: $(TARGET).dvi
-
-pdf: $(TARGET).pdf
-
-
-clean:
-	rm -f *.dvi *.aux *.log *.pdf *.ps *.gz *.bbl *.blg *~ *.core
+remake:
+	make clean
+	make all
--- a/Paper/auto/sigos.el	Mon Apr 23 19:06:07 2018 +0900
+++ b/Paper/auto/sigos.el	Mon Apr 23 21:44:32 2018 +0900
@@ -4,14 +4,23 @@
    (TeX-add-to-alist 'LaTeX-provided-class-options
                      '(("ipsjpapers" "techrep")))
    (TeX-add-to-alist 'LaTeX-provided-package-options
-                     '(("graphicx" "dvipdfmx") ("otf" "deluxe" "multi") ("inputenc" "utf8x")))
+                     '(("graphicx" "dvipdfmx") ("otf" "deluxe" "multi") ("inputenc" "utf8")))
+   (add-to-list 'LaTeX-verbatim-environments-local "VerbatimOut")
+   (add-to-list 'LaTeX-verbatim-environments-local "SaveVerbatim")
+   (add-to-list 'LaTeX-verbatim-environments-local "LVerbatim*")
+   (add-to-list 'LaTeX-verbatim-environments-local "LVerbatim")
+   (add-to-list 'LaTeX-verbatim-environments-local "BVerbatim*")
+   (add-to-list 'LaTeX-verbatim-environments-local "BVerbatim")
+   (add-to-list 'LaTeX-verbatim-environments-local "Verbatim*")
+   (add-to-list 'LaTeX-verbatim-environments-local "Verbatim")
    (add-to-list 'LaTeX-verbatim-environments-local "lstlisting")
-   (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-braces-local "url")
-   (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-delims-local "Verb")
+   (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")
-   (add-to-list 'LaTeX-verbatim-macros-with-delims-local "url")
-   (add-to-list 'LaTeX-verbatim-macros-with-delims-local "lstinline")
    (TeX-run-style-hooks
     "latex2e"
     "ipsjpapers"
@@ -28,18 +37,14 @@
     "otf"
     "url"
     "cite"
+    "inputenc"
     "amssymb"
     "amsmath"
     "colonequals"
-    "inputenc"
     "caption")
    (LaTeX-add-labels
     "fig:cgdg"
-    "agda-interface-stack"
-    "hoare-logic"
-    "fig:hoare"
-    "fig:cbc-hoare"
-    "fig:tree-hoare")
+    "agda-interface-stack")
    (LaTeX-add-bibliographies))
  :latex)
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/escape_agda.rb	Mon Apr 23 21:44:32 2018 +0900
@@ -0,0 +1,27 @@
+#!/usr/bin/env ruby
+
+Suffix     = '.agda.replaced'
+EscapeChar = '@'
+FileName   = ARGV.first
+
+ReplaceTable = {
+  '->' => 'rightarrow',
+  '⊔'  => 'sqcup',
+  '∷' => 'text{::}',
+  '∙'  => 'circ',
+  '≡' => 'equiv',
+  '×' => 'times',
+  '⟨'  => 'langle',
+  '⟩'  => 'rangle',
+  '₁' => 'text{1}',
+  'ℕ' => 'mathbb{N}',
+  '∎'  => 'blacksquare'
+}
+
+code = File.read(FileName)
+ReplaceTable.each do |k, v|
+  escaped_str = EscapeChar + "$\\#{v}$" + EscapeChar
+  code = code.gsub(k, escaped_str)
+end
+
+File.write(FileName.sub(/.agda$/, Suffix), code)
--- a/Paper/sigos.bib	Mon Apr 23 19:06:07 2018 +0900
+++ b/Paper/sigos.bib	Mon Apr 23 21:44:32 2018 +0900
@@ -82,25 +82,3 @@
  address = {New York, NY, USA},
 }

-
-@Comment Hoare-Reference
-
-@article{Hoare1969AnAB,
-  title={An Axiomatic Basis for Computer Programming},
-  author={C. A. R. Hoare},
-  journal={Commun. ACM},
-  year={1969},
-  volume={12},
-  pages={576-580}
-}
-
-@book{Girard:1989:PT:64805,
- author    = {Girard, Jean-Yves and Taylor, Paul and Lafont, Yves},
- title     = {Proofs and Types},
- year      = {1989},
- isbn      = {0-521-37181-3},
- publisher = {Cambridge University Press},
- address   = {New York, NY, USA},
-}
-
-
Binary file Paper/sigos.pdf has changed
--- a/Paper/sigos.tex	Mon Apr 23 19:06:07 2018 +0900
+++ b/Paper/sigos.tex	Mon Apr 23 21:44:32 2018 +0900
@@ -63,7 +63,7 @@

 % 和文表題
 \title{GearsOS の Agda による記述と検証}
-% 英文表題
+% 英文$\lambda$式表題
 \etitle{}

 % 所属ラベルの定義
@@ -93,7 +93,21 @@

 % 和文概要
 \begin{abstract}
-    Gears OS は継続を主とするプログラミング言語 CbC で記述されている。 OS やアプリケーションの信頼性を上げるには仕様を満たしていることを確認する必要がある。 確認方法にはモデル検査と証明がある。 ここでは定理証明支援系Agdaを用いた、CbC 言語の証明方法を考える。 CbC は関数呼び出しを用いず goto 文により遷移する。 これを継続を用いた関数型プログラムとして記述することができる。 この記述はAgda上で決まった形を持つ関数として表すことができる。 Gears OS のモジュールシステムは、実装とAPI を分離することを可能にしている。 このモジュールシステムを Agda 上で記述することができた。 継続は不定の型を返す関数で表されるので、継続に直接要求仕様を Agda の論理式として渡すことができる。 継続には仕様以外にも関数を呼び出すときの前提条件(pre-condition)を追加することが可能である。 これにより、Hoare Logic 的な証明を Agda で記述した CbC に直接載せることが可能になる。 Agda で記述された CbC と実装に用いる CbC は並行した形で存在する。 つまり、CbC のモジュールシステムで記述されたプログラムを比較的機械的に Agda で記述された CbC 変換することができる。 本論文ではAgda 上での CbC の記述手法とその上での Hoare Logic 的な証明手法について考察する。
+    Gears OS は継続を主とするプログラミング言語 CbC で記述されている。 OS やアプ
+    リケーションの信頼性を上げるには仕様を満たしていることを確認する必要がある。
+    確認方法にはモデル検査と証明がある。 ここでは定理証明支援系Agdaを用いた、CbC
+    言語の証明方法を考える。 CbC は関数呼び出しを用いず goto 文により遷移する。
+    これを継続を用いた関数型プログラムとして記述することができる。 この記述は
+    Agda上で決まった形を持つ関数として表すことができる。 Gears OS のモジュールシ
+    ステムは、実装とAPI を分離することを可能にしている。 このモジュールシステム
+    を Agda 上で記述することができた。 継続は不定の型を返す関数で表されるので、
+    継続に直接要求仕様を Agda の論理式として渡すことができる。 継続には仕様以外
+    にも関数を呼び出すときの前提条件(pre-condition)を追加することが可能である。
+    これにより、Hoare Logic 的な証明を Agda で記述した CbC に直接載せることが可
+    能になる。 Agda で記述された CbC と実装に用いる CbC は並行した形で存在する。
+    つまり、CbC のモジュールシステムで記述されたプログラムを比較的機械的に Agda
+    で記述された CbC 変換することができる。 本論文ではAgda 上での CbC の記述手法
+    を検討し、モジュール化を含めた形で検証を行う。
 \end{abstract}

 % 英文概要
@@ -132,8 +146,7 @@
 本論文では CodeGear、DataGear での記述を Agda で表現した。
 また、GearsOS で使われている interface の記述を Agda で表現し、その記述を通して
 実装の仕様の一部に対して証明を行なった。
-さらに、 Agda で継続を用いた記述をした際得られた知見や、継続と hoare logic を使っ
-た今後の検証の方針を示す。
+さらに、 Agda で継続を用いた記述をした際得られた知見を示す。

 \section{CodeGear、 DataGear}

@@ -151,7 +164,7 @@

 \begin{figure}[htpb]
  \begin{center}
-  \scalebox{0.3}{\includegraphics{pic/codeGear_dataGear.pdf}}
+  \scalebox{0.4}{\includegraphics{pic/codeGear_dataGear.pdf}}
  \end{center}
  \caption{CodeGear と DataGear の関係}
  \label{fig:cgdg}
@@ -203,20 +216,11 @@
 このように、CodeGear を Agda で記述し、継続部分に証明すべき性質を Agda で記述する。

 GearsOS での記述は interface によってモジュール化される。
-このモジュール化もAgda により記述する必要がある。
+よって、このモジュール化もAgda により記述する必要がある。
 CbC で記述された任意の CodeGear と Meta CodeGear が Agda にそのまま変換されるわけではないが、変換可能なように記述されると仮定する。

 以下の節では、Agda の基本について復習を行う。

-% \section{定理証明支援器 Agda での証明}
-
-
-% 型システムを用いて証明を行うことができる言語として Agda \cite{agda}が存在する。
-% Agda は依存型という型システムを持つ。依存型とは型も第一級オブジェクトとする型シ
-% ステムで、依存型を持っている言語では型を基本的な操作に制限なしに使用できる
-% 。
-% 型システムは Curry-Howard 同型対応により命題と型付きラムダ計算が一対一で対応する。
-
 \section{Agda の文法}

 Agda はインデントに意味を持つため、きちんと揃える必要がある。
@@ -238,10 +242,9 @@
 時の型は \verb+A -> (A -> B)+ のように考えられる。
 前節に出てきた pushStack の型(Code \ref{push-stack})はこの例である。
 pushStack の型の本体は Code \ref{push-stack-func}のようになる。
-Code \ref{push-stack-funk} では\verb+\+の表記が出ている。これは$\lambda$式で初め
+Code \ref{push-stack-func} では\verb+\+の表記が出ている。これは$\lambda$式で初め
 の pushStack で返した stack である s1 を受け取り、次の関数へ渡している。 Agda の
-$\lambda$式では\verb+\+の他に\verb+λ+で表記することもできる。
-\verb++
+$\lambda$式では\verb+\+の他に$\lambda$で表記することもできる。

 \begin{lstlisting}[caption=pushStack の関数定義,label=push-stack-func]
   pushStack d next = push (stackMethods ) (stack ) d (\s1 -> next (record {stack = s1 ; stackMethods = stackMethods } ))
@@ -268,11 +271,6 @@
     next : Maybe (Element a)
 \end{lstlisting}

-%% element の定義、縦棒　| の定義
-%% SingleLinkedStack の説明に必要なものだけ
-% パターンマッチの説明、 | の定義、説明用のあれ。
-%% push と pop だけ書いて必要なものだけ説明する
-%% testStack08 を説明する。

 引数は変数名で受けることもでき、具体的なコンストラクタを指定することでそのコンストラクタが渡された時の挙動を定義できる。
 これはパターンマッチと呼ばれ、コンストラクタで case 文を行なっているようなものである。
@@ -301,6 +299,10 @@
     stack1 = record { top = (next d) }
 \end{lstlisting}

+popStack は stack を引数として受け取り、stack の top を取って top を次の Element
+ に変更した新しい stack を構築し、継続に stack と data を渡す interface で、実装
+ 部分の popSingleLinkedStack に接続されている。
+
 pushStack と popStack を使った証明の例は Code\ref{push-pop}のようになる。
 ここでは、stack に対し push を行なった直後に pop を行うと取れるデータは push し
 たものと同じになるという論理式を型に書き、証明を行なった。
@@ -346,7 +348,7 @@
 Stack の実装を以下の Code \ref{stack-impl}で示す。
 実装は SingleLinkedStack という名前の\verb+record+で定義されている。

-\lstinputlisting[label=stack-impl, caption=Agdaにおける Stack の実装の一部] {src/AgdaStackImpl.agda}
+\lstinputlisting[label=stack-impl, caption=Agdaにおける Stack の実装の一部] {src/AgdaStackImpl.agda.replaced}

 % Element は SingleLinkedStack で扱われる要素の定義で、現在のデータ datum と次のデー
 % タを Maybe 型という値の存在が不確かな場合の型で包み、自身で再帰的に定義している。
@@ -361,31 +363,6 @@

 \lstinputlisting[label=tree-impl, caption=Agdaにおける Tree の実装]{src/AgdaTreeImpl.agda.replaced}

-%% \begin{lstlisting}[caption=Treeの実装,label=tree-impl]
-%% record TreeMethods {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.@$\sqcup$@ n) where
-%%   field
-%%     putImpl : treeImpl -> a -> (treeImpl -> t) -> t
-%%     getImpl  : treeImpl -> (treeImpl -> Maybe a -> t) -> t
-
-%% record Tree  {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.⊔ n) where
-%%   field
-%%     tree : treeImpl
-%%     treeMethods : TreeMethods {n} {m} {a} {t} treeImpl
-%%   putTree : a -> (Tree treeImpl -> t) -> t
-%%   putTree d next = putImpl (treeMethods ) tree d (\t1 -> next (record {tree = t1 ; treeMethods = treeMethods} ))
-%%   getTree : (Tree treeImpl -> Maybe a -> t) -> t
-%%   getTree next = getImpl (treeMethods ) tree (\t1 d -> next (record {tree = t1 ; treeMethods = treeMethods} ) d )
-
-%% record Node {n : Level } (a k : Set n) : Set n where
-%%   inductive
-%%   field
-%%     key   : k
-%%     value : a
-%%     right : Maybe (Node a k)
-%%     left  : Maybe (Node a k)
-%%     color : Color {n}
-%% \end{lstlisting}
-
 Tree を構成する Node の型は \verb+Node+型で定義され key、 value、 Color、rihgt、
 left などの情報を持っている。
 Tree を構成する末端の Node は \verb+leafNode+ 型で定義されている。
@@ -409,24 +386,23 @@
 interface は record で列挙し、Code~\ref{agda-interface}のように紐付けることができる。
 Agda では型を明記する必要があるため record 内に型を記述している。

-例として Agda で実装した Stack 上の interface ( Code \ref{agda-interface})
+例として Agda で実装した Stack 上の interface (Code \ref{agda-interface})
 の一部を見る。
-Stack の実装は SingleLinkedStack( Code \ref{agda-single-linked-stack}) として書かれている。それを Stack 側からinterface を通して呼び出している。
+Stack の実装は SingleLinkedStack として書かれている。それを Stack 側からinterface を通して呼び出している。

 ここでの interface の型は Stack の record 内にある pushStack や popStack などで、
 実際に使われる Stack の操作は StackMethods にある push や popである。この push
 や pop は SingleLinkedStack で実装されている。

 \lstinputlisting[label=agda-interface, caption=Agda における Interface の定義の
-一部] {src/AgdaInterface.agda}
+一部] {src/AgdaInterface.agda.replaced}

 interface を通すことで、実際には Stack の push では stackImpl と何らかのデータ a を取
 り、 stack を変更し、継続を返す型であったのが、 pushStack では 何らかのデータ a を取り stack を変更
 して継続を返す型に変わっている。

 また、 Tree でも interface を記述した。
-
-\lstinputlisting[label=agda-tree, caption=Tree Interface の定義]{src/AgdaTree.agda}
+\lstinputlisting[label=agda-tree, caption=Tree Interface の定義]{src/AgdaTree.agda.replaced}

 interface を記述することによって、データを push する際に予め決まっている引数を省
 略することができた。
@@ -477,57 +453,64 @@
 これにより、抽象化した Stack に対して push 、 pop を行うと push したものと同じも
 のを受け取れることが証明できた。

- \lstinputlisting[label=agda-in-some-state, caption=抽象的なStackの定義とpush$->$push$->$pop2 の証明]{src/AgdaStackSomeState.agda}
+ \lstinputlisting[label=agda-in-some-state, caption=抽象的なStackの定義とpush$->$push$->$pop2 の証明]{src/AgdaStackSomeState.agda.replaced}
+
+今回の研究では、Agda を用いて GearsOS 上のモジュール化である interface の記述に
+ついて検討、実装した。また、継続を用いた記述をすることで計算途中のデータの形など
+を確認することができることが分かった。その他に、interface の記述を通しての証明が行えることが分かった。

-しかし、同様の証明を Tree 側で記述した際、 Agda 側で等しいことを認識できず記述が
-複雑になっていったため、今後の証明は Hoare Logic をベースにしたものを取り入れて
-行きたいと考えている。
-
-\section{Hoare Logic}
-\label{hoare-logic}
+今後は Agda での継続に hoare logic をベースにした検証方法を考案、実装し、実際の
+プログラムに対して検証が可能かどうかを検討する。
+
+% しかし、同様の証明を Tree 側で記述した際、 Agda 側で等しいことを認識できず記述が
+% 複雑になっていったため、今後の証明は Hoare Logic をベースにしたものを取り入れて
+% 行きたいと考えている。

-Hoare Logic \cite{Hoare1969AnAB} とは Tony Hoare によって提案されたプログラム正
-しさを推論する手法である。図\ref{fig:hoare}のように、 P を前状態(Pre Condition)
-、C を処理(Command) 、 Q を後状態(Post Condition) とし、$\{P\} \  C  \ \{Q\}$ のように考えたとき、
-プログラムの処理を「前状態を満たした後、処理を行い状態が後状態に変化する」といった形で考える事ができる。
+% \section{Hoare Logic}
+% \label{hoare-logic}
+
+% Hoare Logic \cite{Hoare1969AnAB} とは Tony Hoare によって提案されたプログラム正
+% しさを推論する手法である。図\ref{fig:hoare}のように、 P を前状態(Pre Condition)
+% 、C を処理(Command) 、 Q を後状態(Post Condition) とし、$\{P\} \  C  \ \{Q\}$ のように考えたとき、
+% プログラムの処理を「前状態を満たした後、処理を行い状態が後状態に変化する」といった形で考える事ができる。

-\begin{figure}[htpb]
- \begin{center}
-  \scalebox{0.3}[0.3]{\includegraphics{pic/hoare-logic.pdf}}
- \end{center}
- \caption{hoare logicの流れ}
- \label{fig:hoare}
-\end{figure}
+% \begin{figure}[htpb]
+%  \begin{center}
+%   \scalebox{0.3}[0.3]{\includegraphics{pic/hoare-logic.pdf}}
+%  \end{center}
+%  \caption{hoare logicの流れ}
+%  \label{fig:hoare}
+% \end{figure}


-このとき、後状態から前状態を推論することができればそのプログラムは部分的に正しい
-動きをすることを証明することができる。
+% このとき、後状態から前状態を推論することができればそのプログラムは部分的に正しい
+% 動きをすることを証明することができる。

-この Hoare Logic の前状態、処理、後状態を CodeGear、 input/output の DataGear が表
-\ref{fig:cbc-hoare} のように表せると考えている。
+% この Hoare Logic の前状態、処理、後状態を CodeGear、 input/output の DataGear が表
+% \ref{fig:cbc-hoare} のように表せると考えている。

-\begin{figure}[htpb]
- \begin{center}
-  \scalebox{0.3}[0.3]{\includegraphics{pic/cbc-hoare.pdf}}
- \end{center}
- \caption{cbc と hoare logic}
- \label{fig:cbc-hoare}
-\end{figure}
+% \begin{figure}[htpb]
+%  \begin{center}
+%   \scalebox{0.3}[0.3]{\includegraphics{pic/cbc-hoare.pdf}}
+%  \end{center}
+%  \caption{cbc と hoare logic}
+%  \label{fig:cbc-hoare}
+% \end{figure}

-この状態を当研究室で提案している CodeGear、 DataGear の単位で考えると
-PreCondition は CodeGear に入力として与えられる Input DataGear として、
- Command は処理の単位である CodeGear、 PostCondition を Output DataGear として当てはめることができると考える。
+% この状態を当研究室で提案している CodeGear、 DataGear の単位で考えると
+% PreCondition は CodeGear に入力として与えられる Input DataGear として、
+%  Command は処理の単位である CodeGear、 PostCondition を Output DataGear として当てはめることができると考える。

- ここでは binary tree での findNode、 replaceNode、 getRedBlackTree の流れを図
- \ref{fig:tree-hoare} で示す。
+%  ここでは binary tree での findNode、 replaceNode、 getRedBlackTree の流れを図
+%  \ref{fig:tree-hoare} で示す。

- \begin{figure}[htpb]
- \begin{center}
-  \scalebox{0.3}[0.3]{\includegraphics{pic/funcLoopinAutomata.pdf}}
- \end{center}
- \caption{binary tree での hoare logic の考え方}
- \label{fig:tree-hoare}
-\end{figure}
+%  \begin{figure}[htpb]
+%  \begin{center}
+%   \scalebox{0.3}[0.3]{\includegraphics{pic/funcLoopinAutomata.pdf}}
+%  \end{center}
+%  \caption{binary tree での hoare logic の考え方}
+%  \label{fig:tree-hoare}
+% \end{figure}

 % ここでは key に 1 の入った Node を put する際に内部で動く findNode について考え
 % ている。
@@ -540,8 +523,8 @@
 % ると考えている。


-今後の研究では CodeGear、 DataGear、継続の概念を Hoare Logic に当てはめ Agda に
-当てはめ、幾つかの実装を証明していく。
+% 今後の研究では codegear、 datagear、継続の概念を hoare logic に当てはめ agda に
+% 当てはめ、幾つかの実装を証明していく。


 % Hoare Logic ではプログラムの動作が部分的に正しいことが証明できる。
--- a/Paper/src/AgdaBasics.agda.replaced	Mon Apr 23 19:06:07 2018 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,1 +0,0 @@
-module AgdaBasics where
--- a/Paper/src/AgdaInterface.agda.replaced	Mon Apr 23 19:06:07 2018 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,22 +0,0 @@
-data Maybe {n : Level } (a : Set n) : Set n where
-  Nothing : Maybe a
-  Just    : a $\rightarrow$ Maybe a
-
-record StackMethods {n m : Level } (a : Set n ) {t : Set m }(stackImpl : Set n ) : Set (m Level.$\sqcup$ n) where
-  field
-    push : stackImpl $\rightarrow$ a $\rightarrow$ (stackImpl $\rightarrow$ t) $\rightarrow$ t
-    pop  : stackImpl $\rightarrow$ (stackImpl $\rightarrow$ Maybe a $\rightarrow$ t) $\rightarrow$ t
-    get  : stackImpl $\rightarrow$ (stackImpl $\rightarrow$ Maybe a $\rightarrow$ t) $\rightarrow$ t
-open StackMethods
-
-record Stack {n m : Level } (a : Set n ) {t : Set m } (si : Set n ) : Set (m Level.$\sqcup$ n) where
-  field
-    stack : si
-    stackMethods : StackMethods {n} {m} a {t} si
-  pushStack :  a $\rightarrow$ (Stack a si $\rightarrow$ t) $\rightarrow$ t
-  pushStack d next = push (stackMethods ) (stack ) d (\s1 $\rightarrow$ next (record {stack = s1 ; stackMethods = stackMethods } ))
-  popStack : (Stack a si $\rightarrow$ Maybe a  $\rightarrow$ t) $\rightarrow$ t
-  popStack next = pop (stackMethods ) (stack ) (\s1 d1 $\rightarrow$ next (record {stack = s1 ; stackMethods = stackMethods }) d1 )
-  getStack :  (Stack a si $\rightarrow$ Maybe a  $\rightarrow$ t) $\rightarrow$ t
-  getStack next = get (stackMethods ) (stack ) (\s1 d1 $\rightarrow$ next (record {stack = s1 ; stackMethods = stackMethods }) d1 )
-open Stack
--- a/Paper/src/AgdaSingleLinkedStack.agda.replaced	Mon Apr 23 19:06:07 2018 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,63 +0,0 @@
-singleLinkedStackSpec : {n m : Level } {t : Set m } {a : Set n} @$\rightarrow$@ StackMethods {n} {m} a {t} (SingleLinkedStack a)
-singleLinkedStackSpec = record {
-push = pushSingleLinkedStack
-; pop  = popSingleLinkedStack
-; pop2 = pop2SingleLinkedStack
-; get  = getSingleLinkedStack
-; get2 = get2SingleLinkedStack
-; clear = clearSingleLinkedStack
-}
-
-createSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} @$\rightarrow$@ Stack {n} {m} a {t} (SingleLinkedStack a)
-createSingleLinkedStack = record {
-stack = emptySingleLinkedStack ;
-stackMethods = singleLinkedStackSpec
-}
-
--- Implementation
-
-pushSingleLinkedStack : {n m : Level } {t : Set m } {Data : Set n} @$\rightarrow$@ SingleLinkedStack Data @$\rightarrow$@ Data @$\rightarrow$@ (Code : SingleLinkedStack Data @$\rightarrow$@ t) @$\rightarrow$@ t
-pushSingleLinkedStack stack datum next = next stack1
-  where
-    element = cons datum (top stack)
-    stack1  = record {top = Just element}
-
-
-popSingleLinkedStack : {n m : Level } {t : Set m } {a  : Set n} @$\rightarrow$@ SingleLinkedStack a @$\rightarrow$@ (Code : SingleLinkedStack a @$\rightarrow$@ (Maybe a) @$\rightarrow$@ t) @$\rightarrow$@ t
-popSingleLinkedStack stack cs with (top stack)
-...                                | Nothing = cs stack  Nothing
-...                                | Just d  = cs stack1 (Just data1)
-  where
-    data1  = datum d
-    stack1 = record { top = (next d) }
-
-pop2SingleLinkedStack : {n m : Level } {t : Set m } {a  : Set n} @$\rightarrow$@ SingleLinkedStack a @$\rightarrow$@ (Code : SingleLinkedStack a @$\rightarrow$@ (Maybe a) @$\rightarrow$@ (Maybe a) @$\rightarrow$@ t) @$\rightarrow$@ t
-pop2SingleLinkedStack {n} {m} {t} {a} stack cs with (top stack)
-...                                | Nothing = cs stack Nothing Nothing
-...                                | Just d = pop2SingleLinkedStack' {n} {m} stack cs
-  where
-    pop2SingleLinkedStack' : {n m : Level } {t : Set m }  @$\rightarrow$@ SingleLinkedStack a @$\rightarrow$@ (Code : SingleLinkedStack a @$\rightarrow$@ (Maybe a) @$\rightarrow$@ (Maybe a) @$\rightarrow$@ t) @$\rightarrow$@ t
-    pop2SingleLinkedStack' stack cs with (next d)
-    ...              | Nothing = cs stack Nothing Nothing
-    ...              | Just d1 = cs (record {top = (next d1)}) (Just (datum d)) (Just (datum d1))
-
-
-getSingleLinkedStack : {n m : Level } {t : Set m } {a  : Set n} @$\rightarrow$@ SingleLinkedStack a @$\rightarrow$@ (Code : SingleLinkedStack a @$\rightarrow$@ (Maybe a) @$\rightarrow$@ t) @$\rightarrow$@ t
-getSingleLinkedStack stack cs with (top stack)
-...                                | Nothing = cs stack  Nothing
-...                                | Just d  = cs stack (Just data1)
-  where
-    data1  = datum d
-
-get2SingleLinkedStack : {n m : Level } {t : Set m } {a  : Set n} @$\rightarrow$@ SingleLinkedStack a @$\rightarrow$@ (Code : SingleLinkedStack a @$\rightarrow$@ (Maybe a) @$\rightarrow$@ (Maybe a) @$\rightarrow$@ t) @$\rightarrow$@ t
-get2SingleLinkedStack {n} {m} {t} {a} stack cs with (top stack)
-...                                | Nothing = cs stack Nothing Nothing
-...                                | Just d = get2SingleLinkedStack' {n} {m} stack cs
-  where
-    get2SingleLinkedStack' : {n m : Level} {t : Set m } @$\rightarrow$@ SingleLinkedStack a @$\rightarrow$@ (Code : SingleLinkedStack a @$\rightarrow$@ (Maybe a) @$\rightarrow$@ (Maybe a) @$\rightarrow$@ t) @$\rightarrow$@ t
-    get2SingleLinkedStack' stack cs with (next d)
-    ...              | Nothing = cs stack Nothing Nothing
-    ...              | Just d1 = cs stack (Just (datum d)) (Just (datum d1))
-
-clearSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} @$\rightarrow$@ SingleLinkedStack a @$\rightarrow$@ (SingleLinkedStack a @$\rightarrow$@ t) @$\rightarrow$@ t
-clearSingleLinkedStack stack next = next (record {top = Nothing})
--- a/Paper/src/AgdaStackImpl.agda	Mon Apr 23 19:06:07 2018 +0900
+++ b/Paper/src/AgdaStackImpl.agda	Mon Apr 23 21:44:32 2018 +0900
@@ -1,8 +1,3 @@
-record SingleLinkedStack {n : Level } (a : Set n) : Set n where
-  field
-  top : Maybe (Element a)
-open SingleLinkedStack
-
 pushSingleLinkedStack : {n m : Level } {t : Set m } {Data : Set n} -> SingleLinkedStack Data -> Data -> (Code : SingleLinkedStack Data -> t) -> t
 pushSingleLinkedStack stack datum next = next stack1
   where
@@ -15,7 +10,6 @@
 singleLinkedStackSpec = record {
                            push = pushSingleLinkedStack
                          ; pop  = popSingleLinkedStack
-                         ; get  = getSingleLinkedStack
                          }

 createSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> Stack {n} {m} a {t} (SingleLinkedStack a)
--- a/Paper/src/AgdaStackImpl.agda.replaced	Mon Apr 23 19:06:07 2018 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,28 +0,0 @@
-record SingleLinkedStack {n : Level } (a : Set n) : Set n where
-  field
-  top : Maybe (Element a)
-open SingleLinkedStack
-
-pushSingleLinkedStack : {n m : Level } {t : Set m } {Data : Set n} @$\rightarrow$@ SingleLinkedStack Data @$\rightarrow$@ Data @$\rightarrow$@ (Code : SingleLinkedStack Data @$\rightarrow$@ t) @$\rightarrow$@ t
-pushSingleLinkedStack stack datum next = next stack1
-  where
-    element = cons datum (top stack)
-    stack1  = record {top = Just element}
-
--- Basic stack implementations are specifications of a Stack
-
-singleLinkedStackSpec : {n m : Level } {t : Set m } {a : Set n} @$\rightarrow$@ StackMethods {n} {m} a {t} (SingleLinkedStack a)
-singleLinkedStackSpec = record {
-                                   push = pushSingleLinkedStack
-                                 ; pop  = popSingleLinkedStack
-                                 ; pop2 = pop2SingleLinkedStack
-                                 ; get  = getSingleLinkedStack
-                                 ; get2 = get2SingleLinkedStack
-                                 ; clear = clearSingleLinkedStack
-                               }
-
-createSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} @$\rightarrow$@ Stack {n} {m} a {t} (SingleLinkedStack a)
-createSingleLinkedStack = record {
-                            stack = emptySingleLinkedStack ;
-                            stackMethods = singleLinkedStackSpec
-                          }
--- a/Paper/src/AgdaStackSomeState.agda.replaced	Mon Apr 23 19:06:07 2018 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,6 +0,0 @@
-stackInSomeState : {l m : Level } {D : Set l} {t : Set m } (s : SingleLinkedStack D ) @$\rightarrow$@ Stack {l} {m} D {t}  ( SingleLinkedStack  D )
-stackInSomeState s =  record { stack = s ; stackMethods = singleLinkedStackSpec }
-
-push@$\rightarrow$@push@$\rightarrow$@pop2 : {l : Level } {D : Set l} (x y : D ) (s : SingleLinkedStack D ) @$\rightarrow$@ pushStack (stackInSomeState s)  x (\s1 @$\rightarrow$@ pushStack s1 y (\s2 @$\rightarrow$@ pop2Stack s2 (\s3 y1 x1 @$\rightarrow$@
-   (Just x @$\equiv$@ x1) ∧ (Just y @$\equiv$@ y1))))
-push@$\rightarrow$@push@$\rightarrow$@pop2 {l} {D} x y s = record { pi1 = refl ; pi2 = refl }
--- a/Paper/src/AgdaStackTest.agda.replaced	Mon Apr 23 19:06:07 2018 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,22 +0,0 @@
--- after push 1 and 2, pop2 get 1 and 2
-
-testStack02 : {m : Level } @$\rightarrow$@  ( Stack  @$\mathbb{N}$@ (SingleLinkedStack @$\mathbb{N}$@) @$\rightarrow$@ Bool {m} ) @$\rightarrow$@ Bool {m}
-testStack02 cs = pushStack createSingleLinkedStack 1 (\s @$\rightarrow$@ pushStack s 2 cs)
-
-
-testStack031 : (d1 d2 : $\mathbb{N}$ ) @$\rightarrow$@ Bool {Zero}
-testStack031 2 1 = True
-testStack031 _ _ = False
-
-testStack032 : (d1 d2 : Maybe @$\mathbb{N}$@) @$\rightarrow$@ Bool {Zero}
-testStack032  (Just d1) (Just d2) = testStack031 d1 d2
-testStack032  _ _ = False
-
-testStack03 : {m : Level } @$\rightarrow$@ Stack  @$\mathbb{N}$@ (SingleLinkedStack @$\mathbb{N}$@) @$\rightarrow$@ ((Maybe @$\mathbb{N}$@) @$\rightarrow$@ (Maybe @$\mathbb{N}$@) @$\rightarrow$@ Bool {m} ) @$\rightarrow$@ Bool {m}
-testStack03 s cs = pop2Stack s (\s d1 d2 @$\rightarrow$@ cs d1 d2 )
-
-testStack04 : Bool
-testStack04 = testStack02 (\s @$\rightarrow$@ testStack03 s testStack032)
-
-testStack05 : testStack04 @$\equiv$@ True
-testStack05 = refl
--- a/Paper/src/AgdaTree.agda.replaced	Mon Apr 23 19:06:07 2018 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,17 +0,0 @@
-record TreeMethods {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.@$\sqcup$@ n) where
-  field
-    putImpl : treeImpl @$\rightarrow$@ a @$\rightarrow$@ (treeImpl @$\rightarrow$@ t) @$\rightarrow$@ t
-    getImpl  : treeImpl @$\rightarrow$@ (treeImpl @$\rightarrow$@ Maybe a @$\rightarrow$@ t) @$\rightarrow$@ t
-open TreeMethods
-
-record Tree  {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.@$\sqcup$@ n) where
-  field
-    tree : treeImpl
-    treeMethods : TreeMethods {n} {m} {a} {t} treeImpl
-    putTree : a @$\rightarrow$@ (Tree treeImpl @$\rightarrow$@ t) @$\rightarrow$@ t
-    putTree d next = putImpl (treeMethods ) tree d (\t1 @$\rightarrow$@ next (record {tree = t1 ; treeMethods = treeMethods} ))
-    getTree : (Tree treeImpl @$\rightarrow$@ Maybe a @$\rightarrow$@ t) @$\rightarrow$@ t
-    getTree next = getImpl (treeMethods ) tree (\t1 d @$\rightarrow$@ next (record {tree = t1 ; treeMethods = treeMethods} ) d )
-
-open Tree
-
--- a/Paper/src/AgdaTreeDebug.agda.replaced	Mon Apr 23 19:06:07 2018 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,15 +0,0 @@
-test31 = putTree1 {_} {_} {@$\mathbb{N}$@} {@$\mathbb{N}$@} (createEmptyRedBlackTree@$\mathbb{N}$@ @$\mathbb{N}$@ ) 1 1
-  $ \t @$\rightarrow$@ putTree1 t 2 2
-  $ \t @$\rightarrow$@ putTree1 t 3 3
-  $ \t @$\rightarrow$@ putTree1 t 4 4
-  $ \t @$\rightarrow$@ getRedBlackTree t 4
-  $ \t x @$\rightarrow$@ x
-
--- Just
--- (record
--- { key = 4
--- ; value = 4
--- ; right = Nothing
--- ; left = Nothing
--- ; color = Red
--- })
--- a/Paper/src/AgdaTreeImpl.agda.replaced	Mon Apr 23 19:06:07 2018 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,14 +0,0 @@
-record TreeMethods {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.@$\sqcup$@ n) where
-  field
-    putImpl : treeImpl @$\rightarrow$@ a @$\rightarrow$@ (treeImpl @$\rightarrow$@ t) @$\rightarrow$@ t
-  getImpl  : treeImpl @$\rightarrow$@ (treeImpl @$\rightarrow$@ Maybe a @$\rightarrow$@ t) @$\rightarrow$@ t
-
-record Tree  {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.@$\sqcup$@ n) where
-  field
-    tree : treeImpl
-    treeMethods : TreeMethods {n} {m} {a} {t} treeImpl
-  putTree : a @$\rightarrow$@ (Tree treeImpl @$\rightarrow$@ t) @$\rightarrow$@ t
-  putTree d next = putImpl (treeMethods ) tree d (\t1 @$\rightarrow$@ next (record {tree = t1 ; treeMethods = treeMethods} ))
-  getTree : (Tree treeImpl @$\rightarrow$@ Maybe a @$\rightarrow$@ t) @$\rightarrow$@ t
-  getTree next = getImpl (treeMethods ) tree (\t1 d @$\rightarrow$@ next (record {tree = t1 ; treeMethods = treeMethods} ) d )
-
--- a/Paper/src/AgdaTreeProof.agda.replaced	Mon Apr 23 19:06:07 2018 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,34 +0,0 @@
-redBlackInSomeState : { m : Level } (a : Set Level.zero) (n : Maybe (Node a @$\mathbb{N}$@)) {t : Set m} @$\rightarrow$@ RedBlackTree {Level.zero} {m} {t} a @$\mathbb{N}$@
-redBlackInSomeState {m} a n {t} = record { root = n ; nodeStack = emptySingleLinkedStack ; compare = compare2 }
-
-putTest1 :{ m : Level } (n : Maybe (Node @$\mathbb{N}$@ @$\mathbb{N}$@))
-         @$\rightarrow$@ (k : @$\mathbb{N}$@) (x : @$\mathbb{N}$@)
-         @$\rightarrow$@ putTree1 {_} {_} {@$\mathbb{N}$@} {@$\mathbb{N}$@} (redBlackInSomeState {_} @$\mathbb{N}$@ n {Set Level.zero}) k x
-         (\ t @$\rightarrow$@ getRedBlackTree t k (\ t x1 @$\rightarrow$@ check2 x1 x  @$\equiv$@ True))
-putTest1 n k x with n
-...  | Just n1 = lemma2 ( record { top = Nothing } )
-   where
-     lemma2 : (s : SingleLinkedStack (Node @$\mathbb{N}$@ @$\mathbb{N}$@) ) @$\rightarrow$@ putTree1 (record { root = Just n1 ; nodeStack = s ; compare = compare2 }) k x (λ t →
-         GetRedBlackTree.checkNode t k (λ t@$\text{1}$@ x1 → check2 x1 x @$\equiv$@ True) (root t))
-     lemma2 s with compare2 k (key n1)
-     ... |  EQ = lemma3 {!!}
-        where
-           lemma3 : compare2 k (key n1) @$\equiv$@  EQ @$\rightarrow$@ getRedBlackTree {_} {_} {@$\mathbb{N}$@} {@$\mathbb{N}$@} {Set Level.zero} ( record {  root = Just ( record {
-               key   = key n1 ; value = x ; right = right n1 ; left  = left n1 ; color = Black
-               } ) ; nodeStack = s ; compare = λ x@$\text{1}$@ y → compare2 x@$\text{1}$@ y  } ) k ( \ t x1 @$\rightarrow$@ check2 x1 x  @$\equiv$@ True)
-           lemma3 eq with compare2 x x | putTest1Lemma2 x
-           ... | EQ | refl with compare2 k (key n1)  | eq
-           ...              | EQ | refl with compare2 x x | putTest1Lemma2 x
-           ...                    | EQ | refl = refl
-     ... |  GT = {!!}
-     ... |  LT = {!!}
-
-...  | Nothing =  lemma1
-   where
-     lemma1 : getRedBlackTree {_} {_} {@$\mathbb{N}$@} {@$\mathbb{N}$@} {Set Level.zero} ( record {  root = Just ( record {
-               key   = k ; value = x ; right = Nothing ; left  = Nothing ; color = Red
-        } ) ; nodeStack = record { top = Nothing } ; compare = λ x@$\text{1}$@ y → compare2 x@$\text{1}$@ y  } ) k
-        ( \ t x1 @$\rightarrow$@ check2 x1 x  @$\equiv$@ True)
-     lemma1 with compare2 k k | putTest1Lemma2 k
-     ... | EQ | refl with compare2 x x | putTest1Lemma2 x
-     ...              | EQ | refl = refl
--- a/Paper/src/CodeSegment.agda.replaced	Mon Apr 23 19:06:07 2018 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,2 +0,0 @@
-data CodeSegment {l1 l2 : Level} (I : Set l1) (O : Set l2) : Set (l @$\sqcup$@ l1 @$\sqcup$@ l2) where
-  cs : (I @$\rightarrow$@ O) @$\rightarrow$@ CodeSegment I O
--- a/Paper/src/DataSegment.agda.replaced	Mon Apr 23 19:06:07 2018 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,8 +0,0 @@
-record ds0 : Set where
-  field
-    a : Int
-    b : Int
-
-record ds1 : Set where
-  field
-    c : Int
--- a/Paper/src/Goto.agda.replaced	Mon Apr 23 19:06:07 2018 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,4 +0,0 @@
-goto : {l1 l2 : Level} {I : Set l1} {O : Set l2}
-   @$\rightarrow$@ CodeSegment I O @$\rightarrow$@ I @$\rightarrow$@ O
-goto (cs b) i = b i
-