Mercurial > hg > Papers > 2022 > soto-sigos
diff Paper/src/MetaMetaCodeSegment.agda @ 0:14a0e409d574
ADD fast commit
author | soto <soto@cr.ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 24 Apr 2022 23:13:44 +0900 |
parents | |
children |
line wrap: on
line diff
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Paper/src/MetaMetaCodeSegment.agda Sun Apr 24 23:13:44 2022 +0900 @@ -0,0 +1,29 @@ +-- meta level +liftContext : {X Y : Set} {{_ : N.DataSegment X}} {{_ : N.DataSegment Y}} -> N.CodeSegment X Y -> N.CodeSegment Context Context +liftContext {{x}} {{y}} (N.cs f) = N.cs (\c -> N.DataSegment.set y c (f (N.DataSegment.get x c))) + +liftMeta : {X Y : Set} {{_ : M.DataSegment X}} {{_ : M.DataSegment Y}} -> N.CodeSegment X Y -> M.CodeSegment X Y +liftMeta (N.cs f) = M.cs f + +gotoMeta : {I O : Set} {{_ : N.DataSegment I}} {{_ : N.DataSegment O}} -> M.CodeSegment Meta Meta -> N.CodeSegment I O -> Meta -> Meta +gotoMeta mCode code m = M.exec mCode (record m {next = (liftContext code)}) + +push : M.CodeSegment Meta Meta +push = M.cs (\m -> M.exec (liftMeta (Meta.next m)) (record m {c' = Context.c (Meta.context m)})) + +-- normal level + +cs2 : N.CodeSegment ds1 ds1 +cs2 = N.cs id + +cs1 : N.CodeSegment ds1 ds1 +cs1 = N.cs (\d -> N.goto cs2 d) + +cs0 : N.CodeSegment ds0 ds1 +cs0 = N.cs (\d -> N.goto cs1 (record {c = (ds0.a d) + (ds0.b d)})) + +-- meta level (with extended normal) +main : Meta +main = gotoMeta push cs0 (record {context = (record {a = 100 ; b = 50 ; c = 70}) ; c' = 0 ; next = (N.cs id)}) +-- record {context = record {a = 100 ; b = 50 ; c = 150} ; c' = 70 ; next = (N.cs id)} +