Mercurial > hg > Papers > 2021 > soto-prosym

comparison Paper/src/MetaMetaCodeSegment.agda.replaced @ 5:339fb67b4375

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
INIT rbt.agda
author soto <soto@cr.ie.u-ryukyu.ac.jp>
date Sun, 07 Nov 2021 00:51:16 +0900
parents c59202657321
children
comparison
equal deleted inserted replaced
4:72667e8198e2 5:339fb67b4375
1 -- meta level 1 -- meta level
2 liftContext : {X Y : Set} {{_ : N.DataSegment X}} {{_ : N.DataSegment Y}} @$\rightarrow$@ N.CodeSegment X Y @$\rightarrow$@ N.CodeSegment Context Context 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))) 3 liftContext {{x}} {{y}} (N.cs f) = N.cs (\c !$\rightarrow$! N.DataSegment.set y c (f (N.DataSegment.get x c)))
4 4
5 liftMeta : {X Y : Set} {{_ : M.DataSegment X}} {{_ : M.DataSegment Y}} @$\rightarrow$@ N.CodeSegment X Y @$\rightarrow$@ M.CodeSegment X Y 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 6 liftMeta (N.cs f) = M.cs f
7 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 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)}) 9 gotoMeta mCode code m = M.exec mCode (record m {next = (liftContext code)})
10 10
11 push : M.CodeSegment Meta Meta 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)})) 12 push = M.cs (\m !$\rightarrow$! M.exec (liftMeta (Meta.next m)) (record m {c!$\prime$! = Context.c (Meta.context m)}))
13 13
14 -- normal level 14 -- normal level
15 15
16 cs2 : N.CodeSegment ds1 ds1 16 cs2 : N.CodeSegment ds1 ds1
17 cs2 = N.cs id 17 cs2 = N.cs id
18 18
19 cs1 : N.CodeSegment ds1 ds1 19 cs1 : N.CodeSegment ds1 ds1
20 cs1 = N.cs (\d @$\rightarrow$@ N.goto cs2 d) 20 cs1 = N.cs (\d !$\rightarrow$! N.goto cs2 d)
21 21
22 cs0 : N.CodeSegment ds0 ds1 22 cs0 : N.CodeSegment ds0 ds1
23 cs0 = N.cs (\d @$\rightarrow$@ N.goto cs1 (record {c = (ds0.a d) + (ds0.b d)})) 23 cs0 = N.cs (\d !$\rightarrow$! N.goto cs1 (record {c = (ds0.a d) + (ds0.b d)}))
24 24
25 -- meta level (with extended normal) 25 -- meta level (with extended normal)
26 main : Meta 26 main : Meta
27 main = gotoMeta push cs0 (record {context = (record {a = 100 ; b = 50 ; c = 70}) ; c' = 0 ; next = (N.cs id)}) 27 main = gotoMeta push cs0 (record {context = (record {a = 100 ; b = 50 ; c = 70}) ; c!$\prime$! = 0 ; next = (N.cs id)})
28 -- record {context = record {a = 100 ; b = 50 ; c = 150} ; c' = 70 ; next = (N.cs id)} 28 -- record {context = record {a = 100 ; b = 50 ; c = 150} ; c!$\prime$! = 70 ; next = (N.cs id)}
29 29