Mercurial > hg > Papers > 2020 > soto-midterm
comparison src/MetaMetaCodeSegment.agda.replaced @ 1:73127e0ab57c
(none)
| author | soto@cr.ie.u-ryukyu.ac.jp |
|---|---|
| date | Tue, 08 Sep 2020 18:38:08 +0900 |
| parents | |
| children |
comparison
equal
deleted
inserted
replaced
| 0:b919985837a3 | 1:73127e0ab57c |
|---|---|
| 1 -- meta level | |
| 2 liftContext : {X Y : Set} {{_ : N.DataSegment X}} {{_ : N.DataSegment Y}} @$\rightarrow$@ N.CodeSegment X Y @$\rightarrow$@ N.CodeSegment Context Context | |
| 3 liftContext {{x}} {{y}} (N.cs f) = N.cs (\c @$\rightarrow$@ N.DataSegment.set y c (f (N.DataSegment.get x c))) | |
| 4 | |
| 5 liftMeta : {X Y : Set} {{_ : M.DataSegment X}} {{_ : M.DataSegment Y}} @$\rightarrow$@ N.CodeSegment X Y @$\rightarrow$@ M.CodeSegment X Y | |
| 6 liftMeta (N.cs f) = M.cs f | |
| 7 | |
| 8 gotoMeta : {I O : Set} {{_ : N.DataSegment I}} {{_ : N.DataSegment O}} @$\rightarrow$@ M.CodeSegment Meta Meta @$\rightarrow$@ N.CodeSegment I O @$\rightarrow$@ Meta @$\rightarrow$@ Meta | |
| 9 gotoMeta mCode code m = M.exec mCode (record m {next = (liftContext code)}) | |
| 10 | |
| 11 push : M.CodeSegment Meta Meta | |
| 12 push = M.cs (\m @$\rightarrow$@ M.exec (liftMeta (Meta.next m)) (record m {c' = Context.c (Meta.context m)})) | |
| 13 | |
| 14 -- normal level | |
| 15 | |
| 16 cs2 : N.CodeSegment ds1 ds1 | |
| 17 cs2 = N.cs id | |
| 18 | |
| 19 cs1 : N.CodeSegment ds1 ds1 | |
| 20 cs1 = N.cs (\d @$\rightarrow$@ N.goto cs2 d) | |
| 21 | |
| 22 cs0 : N.CodeSegment ds0 ds1 | |
| 23 cs0 = N.cs (\d @$\rightarrow$@ N.goto cs1 (record {c = (ds0.a d) + (ds0.b d)})) | |
| 24 | |
| 25 -- meta level (with extended normal) | |
| 26 main : Meta | |
| 27 main = gotoMeta push cs0 (record {context = (record {a = 100 ; b = 50 ; c = 70}) ; c' = 0 ; next = (N.cs id)}) | |
| 28 -- record {context = record {a = 100 ; b = 50 ; c = 150} ; c' = 70 ; next = (N.cs id)} | |
| 29 |