Mercurial > hg > Members > atton > agda-proofs
comparison cbc/atton-master-meta-sample.agda @ 75:79d435b16241
Add attom-master-meta-sample
author | atton <atton@cr.ie.u-ryukyu.ac.jp> |
---|---|
date | Fri, 03 Feb 2017 02:20:25 +0000 |
parents | |
children | 29a3a4b79d4d |
comparison
equal
deleted
inserted
replaced
74:f1ab418bc37f | 75:79d435b16241 |
---|---|
1 module atton-master-meta-sample where | |
2 | |
3 open import Data.Nat | |
4 open import Data.Unit | |
5 open import Function | |
6 Int = ℕ | |
7 | |
8 record Context : Set where | |
9 field | |
10 a : Int | |
11 b : Int | |
12 c : Int | |
13 | |
14 open import subtype Context as N | |
15 | |
16 record Meta : Set where | |
17 field | |
18 context : Context | |
19 c' : Int | |
20 next : N.CodeSegment Context Context | |
21 | |
22 open import subtype Meta as M | |
23 | |
24 instance | |
25 _ : N.DataSegment Context | |
26 _ = record { get = id ; set = (\_ c -> c) } | |
27 _ : M.DataSegment Context | |
28 _ = record { get = (\m -> Meta.context m) ; | |
29 set = (\m c -> record m {context = c}) } | |
30 _ : M.DataSegment Meta | |
31 _ = record { get = id ; set = (\_ m -> m) } | |
32 | |
33 | |
34 liftContext : {X Y : Set} {{_ : N.DataSegment X}} {{_ : N.DataSegment Y}} -> N.CodeSegment X Y -> N.CodeSegment Context Context | |
35 liftContext {{x}} {{y}} (N.cs f) = N.cs (\c -> N.DataSegment.set y c (f (N.DataSegment.get x c))) | |
36 | |
37 liftMeta : {X Y : Set} {{_ : M.DataSegment X}} {{_ : M.DataSegment Y}} -> N.CodeSegment X Y -> M.CodeSegment X Y | |
38 liftMeta (N.cs f) = M.cs f | |
39 | |
40 | |
41 gotoMeta : {I O : Set} {{_ : N.DataSegment I}} {{_ : N.DataSegment O}} -> M.CodeSegment Meta Meta -> N.CodeSegment I O -> Meta -> Meta | |
42 gotoMeta mCode code m = M.exec mCode (record m {next = (liftContext code)}) | |
43 | |
44 push : M.CodeSegment Meta Meta | |
45 push = M.cs (\m -> M.exec (liftMeta (Meta.next m)) (record m {c' = Context.c (Meta.context m)})) | |
46 | |
47 | |
48 record ds0 : Set where | |
49 field | |
50 a : Int | |
51 b : Int | |
52 | |
53 record ds1 : Set where | |
54 field | |
55 c : Int | |
56 | |
57 instance | |
58 _ : N.DataSegment ds0 | |
59 _ = record { set = (\c d -> record c {a = (ds0.a d) ; b = (ds0.b d)}) | |
60 ; get = (\c -> record { a = (Context.a c) ; b = (Context.b c)})} | |
61 _ : N.DataSegment ds1 | |
62 _ = record { set = (\c d -> record c {c = (ds1.c d)}) | |
63 ; get = (\c -> record { c = (Context.c c)})} | |
64 | |
65 cs2 : N.CodeSegment ds1 ds1 | |
66 cs2 = N.cs id | |
67 | |
68 cs1 : N.CodeSegment ds1 ds1 | |
69 cs1 = N.cs (\d -> N.goto cs2 d) | |
70 | |
71 cs0 : N.CodeSegment ds0 ds1 | |
72 cs0 = N.cs (\d -> N.goto cs1 (record {c = (ds0.a d) + (ds0.b d)})) | |
73 | |
74 | |
75 main : Meta | |
76 main = gotoMeta push cs0 (record {context = (record {a = 100 ; b = 50 ; c = 70}) ; c' = 0 ; next = (N.cs id)}) |