# HG changeset patch
# User atton <atton@cr.ie.u-ryukyu.ac.jp>
# Date 1486343716 -32400
# Node ID b0cfef1cd89f6059c30ba2a1924bb5f1fd4ab1e6
# Parent  4b8a75618f36e47380ad5f1604c625c1b7b47719
Add sample source

diff -r 4b8a75618f36 -r b0cfef1cd89f paper/atton-master.pdf
Binary file paper/atton-master.pdf has changed
diff -r 4b8a75618f36 -r b0cfef1cd89f paper/atton-master.tex
--- a/paper/atton-master.tex	Sun Feb 05 16:53:16 2017 +0900
+++ b/paper/atton-master.tex	Mon Feb 06 10:15:16 2017 +0900
@@ -138,5 +138,6 @@
 
 %付録
 \addcontentsline{toc}{chapter}{付録}
-% \input{appendix.tex}
+\appendix
+\input{sources.tex}
 \end{document}
diff -r 4b8a75618f36 -r b0cfef1cd89f paper/cbc-type.tex
--- a/paper/cbc-type.tex	Sun Feb 05 16:53:16 2017 +0900
+++ b/paper/cbc-type.tex	Mon Feb 06 10:15:16 2017 +0900
@@ -57,6 +57,7 @@
 
 % {{{ ノーマルレベル計算の実行
 \section{ノーマルレベル計算の実行}
+\label{section:normal-level-exec}
 プログラムを実行することは \verb/goto/ を定義することと同義である。
 軽量継続\verb/goto/ の性質としては
 
@@ -78,7 +79,7 @@
 
 この \verb/goto/ の定義を用いることで main などの関数が評価できるようになり、値150が得られる。
 本文中での CodeSegment の定義は一部を抜粋している。
-実行可能な Agda のソースコードは付録に載せる。% TODO: Appendix
+実行可能な Agda のソースコードは付録に載せる。
 
 % }}}
 
diff -r 4b8a75618f36 -r b0cfef1cd89f paper/sources.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/sources.tex	Mon Feb 06 10:15:16 2017 +0900
@@ -0,0 +1,9 @@
+\chapter{chapter:sources}
+本論文中に取り上げた Agda の動作するソースコードを示す。
+
+\section{ノーマルレベル動作の実行}
+\label{appendix:normal-level-exec}
+\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}
diff -r 4b8a75618f36 -r b0cfef1cd89f paper/src/atton-master-meta-sample.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/src/atton-master-meta-sample.agda	Mon Feb 06 10:15:16 2017 +0900
@@ -0,0 +1,77 @@
+module atton-master-meta-sample where
+
+open import Data.Nat
+open import Data.Unit
+open import Function
+Int = ℕ
+
+record Context : Set where
+  field
+    a  : Int
+    b  : Int
+    c  : Int
+
+open import subtype Context as N
+
+record Meta : Set where 
+  field
+    context : Context
+    c'      : Int
+    next    : N.CodeSegment Context Context
+
+open import subtype Meta as M
+
+instance
+  _ : N.DataSegment Context
+  _ = record { get = id ; set = (\_ c -> c) }
+  _ : M.DataSegment Context
+  _ = record { get = (\m -> Meta.context m)  ;
+               set = (\m c -> record m {context = c}) }
+  _ : M.DataSegment Meta
+  _ = record { get = id ; set = (\_ m -> m) }
+
+
+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)))
+
+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
+
+
+gotoMeta : {I O : Set} {{_ : N.DataSegment I}} {{_ : N.DataSegment O}} -> M.CodeSegment Meta Meta -> N.CodeSegment I O -> Meta -> Meta
+gotoMeta mCode code m = M.exec mCode (record m {next = (liftContext code)})
+
+push : M.CodeSegment Meta Meta
+push = M.cs (\m -> M.exec (liftMeta (Meta.next m)) (record m {c' = Context.c (Meta.context m)}))
+
+
+record ds0 : Set where
+  field
+    a : Int
+    b : Int
+
+record ds1 : Set where
+  field
+    c : Int
+
+instance
+  _ : N.DataSegment ds0
+  _ = record { set = (\c d -> record c {a = (ds0.a d) ; b = (ds0.b d)})
+             ; get = (\c ->   record { a = (Context.a c) ; b = (Context.b c)})}
+  _ : N.DataSegment ds1
+  _ = record { set = (\c d -> record c {c = (ds1.c d)})
+             ; get = (\c ->   record { c = (Context.c c)})}
+
+cs2 : N.CodeSegment ds1 ds1
+cs2 = N.cs id
+
+cs1 : N.CodeSegment ds1 ds1
+cs1 = N.cs (\d -> N.goto cs2 d)
+
+cs0 : N.CodeSegment ds0 ds1
+cs0 = N.cs (\d -> N.goto cs1 (record {c = (ds0.a d) + (ds0.b d)}))
+
+
+main : Meta
+main = gotoMeta push cs0 (record {context = (record {a = 100 ; b = 50 ; c = 70}) ; c' = 0 ; next = (N.cs id)})
+-- record {context = record {a = 100 ; b = 50 ; c = 150} ; c' = 70 ; next = (N.cs id)}
diff -r 4b8a75618f36 -r b0cfef1cd89f paper/src/atton-master-sample.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/src/atton-master-sample.agda	Mon Feb 06 10:15:16 2017 +0900
@@ -0,0 +1,46 @@
+module atton-master-sample where
+
+open import Data.Nat
+open import Data.Unit
+open import Function
+Int = ℕ
+
+record Context : Set where
+  field
+    a : Int
+    b : Int
+    c : Int
+
+
+open import subtype Context
+
+
+
+record ds0 : Set where
+  field
+    a : Int
+    b : Int
+
+record ds1 : Set where
+  field
+    c : Int
+
+instance
+  _ : DataSegment ds0
+  _ = record { set = (\c d -> record c {a = (ds0.a d) ; b = (ds0.b d)})
+             ; get = (\c ->   record { a = (Context.a c) ; b = (Context.b c)})}
+  _ : DataSegment ds1
+  _ = record { set = (\c d -> record c {c = (ds1.c d)})
+             ; get = (\c ->   record { c = (Context.c c)})}
+
+cs2 : CodeSegment ds1 ds1
+cs2 = cs id
+
+cs1 : CodeSegment ds1 ds1
+cs1 = cs (\d -> goto cs2 d)
+
+cs0 : CodeSegment ds0 ds1
+cs0 = cs (\d -> goto cs1 (record {c = (ds0.a d) + (ds0.b d)}))
+
+main : ds1
+main = goto cs0 (record {a = 100 ; b = 50})