changeset 91:54cf3b3153fe

Update
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Thu, 09 Feb 2017 18:37:26 +0900
parents f535393e4043
children c407b7403548
files paper/atton-master.pdf paper/cbc-type.tex paper/sources.tex paper/src/struct-init.c paper/src/struct.c paper/type.tex
diffstat 6 files changed, 13 insertions(+), 5 deletions(-) [+]
line wrap: on
line diff
Binary file paper/atton-master.pdf has changed
--- a/paper/cbc-type.tex	Thu Feb 09 18:30:02 2017 +0900
+++ b/paper/cbc-type.tex	Thu Feb 09 18:37:26 2017 +0900
@@ -183,7 +183,7 @@
 
 \begin{figure}[htbp]
     \begin{center}
-        \includegraphics[width=450]{fig/meta-hierarchy.pdf}
+        \includegraphics[width=450pt]{fig/meta-hierarchy.pdf}
         \caption{fig:meta-hierarchy}
         \label{メタの階層構造}
     \end{center}
--- a/paper/sources.tex	Thu Feb 09 18:30:02 2017 +0900
+++ b/paper/sources.tex	Thu Feb 09 18:37:26 2017 +0900
@@ -5,7 +5,7 @@
 \section{部分型の定義}
 リスト~\ref{src:agda-subtype} に Agda 上で定義した CbC の部分型の定義を示す。
 
-\lstinputlisting[label=src:agda-subtype, caption=Agda 上で定義した CbC の部分型の定義(subtype.agda)] {src/subtype.agda}
+\lstinputlisting[label=src:agda-subtype, caption=Agda 上で定義した CbC の部分型の定義(subtype.agda)] {src/subtype.agda.replaced}
 
 \section{ノーマルレベル計算の実行}
 \ref{section:normal-level-exec}節で取り上げたソースコードをリスト~\ref{src:normal-level-exec}に示す。
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/src/struct-init.c	Thu Feb 09 18:37:26 2017 +0900
@@ -0,0 +1,1 @@
+struct Point p = {100 , 200};
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/src/struct.c	Thu Feb 09 18:37:26 2017 +0900
@@ -0,0 +1,4 @@
+struct Point {
+    int x;
+    int y;
+};
--- a/paper/type.tex	Thu Feb 09 18:30:02 2017 +0900
+++ b/paper/type.tex	Thu Feb 09 18:37:26 2017 +0900
@@ -89,11 +89,14 @@
 ここでレコード型という型を導入する。
 レコード型は複数の型を持ちえる型であり、内部に持っている値にはユニークな名前がラベルとして付いている。
 例えば「Intの変数x とIntの変数yを持つレコード型」は$ \{ x : Int , y : Bool\}$のように記述する。
-C における構造体ではリストに対応する。
-% TODO C の構造体
+C における構造体ではリスト~\ref{src:struct}にのソースコードに対応する。
+
+\lstinputlisting[label=src:struct, caption=C におけるレコード型である構造体の定義] {src/struct.c}
 
 レコード型の値を構成する際には、内部に格納する値を全て与えることで構成できる。
-% TODO C の構造体の初期化
+C 言語ならばフィールドの値を \verb/{}/ 内部に \verb/,/ 区切りで与えることで構造体を構成できる(リスト~\ref{src:struct-init})。
+\lstinputlisting[label=src:struct-init, caption=C 言語の構造体の初期化] {src/struct-init.c}
+
 レコード型から値を取り出す際にはラベル名を用いた射影を利用する。
 C 言語では構造体の後に \verb/./ キーワードを付けた後にラベル名を指定する。