Mercurial > hg > Papers > 2018 > nozomi-master

annotate paper/src/MetaMetaCodeSegment.agda @ 63:6d8825f3b051

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add example of meta code segment execution
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Fri, 03 Feb 2017 11:59:41 +0900
parents
children ebe838b83ada
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
63
6d8825f3b051 Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 ...
6d8825f3b051 Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
2 -- meta level
6d8825f3b051 Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 liftContext : {X Y : Set} {{_ : N.DataSegment X}} {{_ : N.DataSegment Y}} -> N.CodeSegment X Y -> N.CodeSegment Context Context
6d8825f3b051 Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 liftContext {{x}} {{y}} (N.cs f) = N.cs (\c -> N.DataSegment.set y c (f (N.DataSegment.get x c)))
6d8825f3b051 Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
5
6d8825f3b051 Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
6 liftMeta : {X Y : Set} {{_ : M.DataSegment X}} {{_ : M.DataSegment Y}} -> N.CodeSegment X Y -> M.CodeSegment X Y
6d8825f3b051 Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 liftMeta (N.cs f) = M.cs f
6d8825f3b051 Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
8
6d8825f3b051 Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 gotoMeta : {I O : Set} {{_ : N.DataSegment I}} {{_ : N.DataSegment O}} -> M.CodeSegment Meta Meta -> N.CodeSegment I O -> Meta -> Meta
6d8825f3b051 Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 gotoMeta mCode code m = M.exec mCode (record m {next = (liftContext code)})
6d8825f3b051 Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
11
6d8825f3b051 Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 push : M.CodeSegment Meta Meta
6d8825f3b051 Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 push = M.cs (\m -> M.exec (liftMeta (Meta.next m)) (record m {c' = Context.c (Meta.context m)}))
6d8825f3b051 Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
14
6d8825f3b051 Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
15 -- normal level
6d8825f3b051 Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
16
6d8825f3b051 Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
17 cs2 : N.CodeSegment ds1 ds1
6d8825f3b051 Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
18 cs2 = N.cs id
6d8825f3b051 Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
19
6d8825f3b051 Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
20 cs1 : N.CodeSegment ds1 ds1
6d8825f3b051 Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
21 cs1 = N.cs (\d -> N.goto cs2 d)
6d8825f3b051 Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
22
6d8825f3b051 Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
23 cs0 : N.CodeSegment ds0 ds1
6d8825f3b051 Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
24 cs0 = N.cs (\d -> N.goto cs1 (record {c = (ds0.a d) + (ds0.b d)}))
6d8825f3b051 Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
25
6d8825f3b051 Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
26 -- meta level (with extended normal)
6d8825f3b051 Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
27 main : Meta
6d8825f3b051 Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
28 main = gotoMeta push cs0 (record {context = (record {a = 100 ; b = 50 ; c = 70}) ; c' = 0 ; next = (N.cs id)})
6d8825f3b051 Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
29 -- record {context = record {a = 100 ; b = 50 ; c = 150} ; c' = 70 ; next = (N.cs id)}
6d8825f3b051 Add example of meta code segment execution
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
30