Mercurial > hg > Papers > 2018 > nozomi-master
changeset 62:a40033d3e10f
Add Meta CodeSegment description
| author | atton <atton@cr.ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 03 Feb 2017 10:29:28 +0900 |
| parents | 3981580ece72 |
| children | 6d8825f3b051 |
| files | paper/atton-master.pdf paper/cbc-type.tex paper/src/MetaCodeSegment.agda |
| diffstat | 3 files changed, 16 insertions(+), 2 deletions(-) [+] |
line wrap: on
line diff
--- a/paper/cbc-type.tex Fri Feb 03 10:23:26 2017 +0900 +++ b/paper/cbc-type.tex Fri Feb 03 10:29:28 2017 +0900 @@ -100,7 +100,7 @@ Context を Meta DataSegment とするプログラム上では DataSegment は Meta CodeSegment の上位型となる。 その制約を \verb/DataSegment/ 型は表わしている。 -\lstinputlisting[label=src:agda-mds, caption=Agda における Meta DataSegment の定義] {src/MetaDataSegment.agda} +\lstinputlisting[label=src:agda-mds, caption=Agda における Meta DataSegment の定義] {src/MetaDataSegment.agda.replaced} ここで、関数を部分型に拡張する S-ARROW をもう一度示す。 @@ -127,7 +127,17 @@ % }}} -\section{MetaCodeSegment の定義} +% {{{ Meta CodeSegment の定義 + +\section{Meta CodeSegment の定義} +Meta DataSegment が定義できたので Meta CodeSegment を定義する。 +実際、DataSegment が Meta DataSegment に拡張できたため、Meta CodeSegment の定義には比較的変更は無い。 +ノーマルレベルの \verb/CodeSegment/ 型に、DataSegment を取って DataSegment を返す、という制約を明示的に付けるだけである(リスト~\ref{src:agda-mcs}) + +\lstinputlisting[label=src:agda-mcs, caption=Agda における Meta CodeSegment の定義] {src/MetaCodeSegment.agda.replaced} + +% }}} + \section{メタレベル計算の実行} \section{Agda を用いたContinuation based C の検証} \section{スタックの実装の検証}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/MetaCodeSegment.agda Fri Feb 03 10:29:28 2017 +0900 @@ -0,0 +1,4 @@ +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 +