Mercurial > hg > Papers > 2018 > nozomi-master

annotate paper/src/MetaMetaDataSegment.agda @ 100:ebe838b83ada

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Self review
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Sun, 12 Feb 2017 11:52:20 +0900
parents 6d8825f3b051
children
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
100
ebe838b83ada Self review
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 63
diff changeset
1 -- 上で各 DataSegement の定義を行なっているとする
ebe838b83ada Self review
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 63
diff changeset
2 open import subtype Context as N -- Meta Datasegment を定義
63
6d8825f3b051 Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
3
100
ebe838b83ada Self review
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 63
diff changeset
4 -- Meta DataSegment を持つ Meta Meta DataSegment を定義できる
63
6d8825f3b051 Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 record Meta : Set where
6d8825f3b051 Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
6 field
6d8825f3b051 Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 context : Context
6d8825f3b051 Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
8 c' : Int
6d8825f3b051 Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 next : N.CodeSegment Context Context
6d8825f3b051 Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
10
6d8825f3b051 Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 open import subtype Meta as M
100
ebe838b83ada Self review
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 63
diff changeset
12 -- 以下よりメタメタレベルのプログラムを記述できる