|
0
|
1 -- meta level
|
|
5
|
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)))
|
|
0
|
4
|
|
5
|
5 liftMeta : {X Y : Set} {{_ : M.DataSegment X}} {{_ : M.DataSegment Y}} !$\rightarrow$! N.CodeSegment X Y !$\rightarrow$! M.CodeSegment X Y
|
|
0
|
6 liftMeta (N.cs f) = M.cs f
|
|
|
7
|
|
5
|
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
|
|
0
|
9 gotoMeta mCode code m = M.exec mCode (record m {next = (liftContext code)})
|
|
|
10
|
|
|
11 push : M.CodeSegment Meta Meta
|
|
5
|
12 push = M.cs (\m !$\rightarrow$! M.exec (liftMeta (Meta.next m)) (record m {c!$\prime$! = Context.c (Meta.context m)}))
|
|
0
|
13
|
|
|
14 -- normal level
|
|
|
15
|
|
|
16 cs2 : N.CodeSegment ds1 ds1
|
|
|
17 cs2 = N.cs id
|
|
|
18
|
|
|
19 cs1 : N.CodeSegment ds1 ds1
|
|
5
|
20 cs1 = N.cs (\d !$\rightarrow$! N.goto cs2 d)
|
|
0
|
21
|
|
|
22 cs0 : N.CodeSegment ds0 ds1
|
|
5
|
23 cs0 = N.cs (\d !$\rightarrow$! N.goto cs1 (record {c = (ds0.a d) + (ds0.b d)}))
|
|
0
|
24
|
|
|
25 -- meta level (with extended normal)
|
|
|
26 main : Meta
|
|
5
|
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!$\prime$! = 70 ; next = (N.cs id)}
|
|
0
|
29
|
