Mercurial > hg > Members > atton > agda-proofs

annotate cbc/atton-master-meta-sample.agda @ 77:a2e6f61d5f2b default tip

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add modus-ponens
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Thu, 09 Feb 2017 06:32:03 +0000
parents 29a3a4b79d4d
children
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
75
79d435b16241 Add attom-master-meta-sample
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 module atton-master-meta-sample where
79d435b16241 Add attom-master-meta-sample
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
2
79d435b16241 Add attom-master-meta-sample
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 open import Data.Nat
79d435b16241 Add attom-master-meta-sample
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 open import Data.Unit
79d435b16241 Add attom-master-meta-sample
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 open import Function
79d435b16241 Add attom-master-meta-sample
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
6 Int = ℕ
79d435b16241 Add attom-master-meta-sample
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
7
79d435b16241 Add attom-master-meta-sample
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
8 record Context : Set where
79d435b16241 Add attom-master-meta-sample
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 field
79d435b16241 Add attom-master-meta-sample
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 a : Int
79d435b16241 Add attom-master-meta-sample
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 b : Int
79d435b16241 Add attom-master-meta-sample
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 c : Int
79d435b16241 Add attom-master-meta-sample
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
13
79d435b16241 Add attom-master-meta-sample
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 open import subtype Context as N
79d435b16241 Add attom-master-meta-sample
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
15
79d435b16241 Add attom-master-meta-sample
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 record Meta : Set where
79d435b16241 Add attom-master-meta-sample
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
17 field
79d435b16241 Add attom-master-meta-sample
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
18 context : Context
79d435b16241 Add attom-master-meta-sample
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
19 c' : Int
79d435b16241 Add attom-master-meta-sample
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
20 next : N.CodeSegment Context Context
79d435b16241 Add attom-master-meta-sample
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
21
79d435b16241 Add attom-master-meta-sample
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
22 open import subtype Meta as M
79d435b16241 Add attom-master-meta-sample
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
23
79d435b16241 Add attom-master-meta-sample
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
24 instance
79d435b16241 Add attom-master-meta-sample
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
25 _ : N.DataSegment Context
79d435b16241 Add attom-master-meta-sample
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
26 _ = record { get = id ; set = (\_ c -> c) }
79d435b16241 Add attom-master-meta-sample
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
27 _ : M.DataSegment Context
79d435b16241 Add attom-master-meta-sample
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
28 _ = record { get = (\m -> Meta.context m) ;
79d435b16241 Add attom-master-meta-sample
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
29 set = (\m c -> record m {context = c}) }
79d435b16241 Add attom-master-meta-sample
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
30 _ : M.DataSegment Meta
79d435b16241 Add attom-master-meta-sample
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
31 _ = record { get = id ; set = (\_ m -> m) }
79d435b16241 Add attom-master-meta-sample
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
32
79d435b16241 Add attom-master-meta-sample
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
33
79d435b16241 Add attom-master-meta-sample
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
34 liftContext : {X Y : Set} {{_ : N.DataSegment X}} {{_ : N.DataSegment Y}} -> N.CodeSegment X Y -> N.CodeSegment Context Context
79d435b16241 Add attom-master-meta-sample
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
35 liftContext {{x}} {{y}} (N.cs f) = N.cs (\c -> N.DataSegment.set y c (f (N.DataSegment.get x c)))
79d435b16241 Add attom-master-meta-sample
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
36
79d435b16241 Add attom-master-meta-sample
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
37 liftMeta : {X Y : Set} {{_ : M.DataSegment X}} {{_ : M.DataSegment Y}} -> N.CodeSegment X Y -> M.CodeSegment X Y
79d435b16241 Add attom-master-meta-sample
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
38 liftMeta (N.cs f) = M.cs f
79d435b16241 Add attom-master-meta-sample
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
39
79d435b16241 Add attom-master-meta-sample
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
40
79d435b16241 Add attom-master-meta-sample
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
41 gotoMeta : {I O : Set} {{_ : N.DataSegment I}} {{_ : N.DataSegment O}} -> M.CodeSegment Meta Meta -> N.CodeSegment I O -> Meta -> Meta
79d435b16241 Add attom-master-meta-sample
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
42 gotoMeta mCode code m = M.exec mCode (record m {next = (liftContext code)})
79d435b16241 Add attom-master-meta-sample
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
43
79d435b16241 Add attom-master-meta-sample
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
44 push : M.CodeSegment Meta Meta
79d435b16241 Add attom-master-meta-sample
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
45 push = M.cs (\m -> M.exec (liftMeta (Meta.next m)) (record m {c' = Context.c (Meta.context m)}))
79d435b16241 Add attom-master-meta-sample
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
46
79d435b16241 Add attom-master-meta-sample
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
47
79d435b16241 Add attom-master-meta-sample
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
48 record ds0 : Set where
79d435b16241 Add attom-master-meta-sample
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
49 field
79d435b16241 Add attom-master-meta-sample
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
50 a : Int
79d435b16241 Add attom-master-meta-sample
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
51 b : Int
79d435b16241 Add attom-master-meta-sample
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
52
79d435b16241 Add attom-master-meta-sample
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
53 record ds1 : Set where
79d435b16241 Add attom-master-meta-sample
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
54 field
79d435b16241 Add attom-master-meta-sample
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
55 c : Int
79d435b16241 Add attom-master-meta-sample
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
56
79d435b16241 Add attom-master-meta-sample
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
57 instance
79d435b16241 Add attom-master-meta-sample
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
58 _ : N.DataSegment ds0
79d435b16241 Add attom-master-meta-sample
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
59 _ = record { set = (\c d -> record c {a = (ds0.a d) ; b = (ds0.b d)})
79d435b16241 Add attom-master-meta-sample
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
60 ; get = (\c -> record { a = (Context.a c) ; b = (Context.b c)})}
79d435b16241 Add attom-master-meta-sample
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
61 _ : N.DataSegment ds1
79d435b16241 Add attom-master-meta-sample
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
62 _ = record { set = (\c d -> record c {c = (ds1.c d)})
79d435b16241 Add attom-master-meta-sample
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
63 ; get = (\c -> record { c = (Context.c c)})}
79d435b16241 Add attom-master-meta-sample
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
64
79d435b16241 Add attom-master-meta-sample
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
65 cs2 : N.CodeSegment ds1 ds1
79d435b16241 Add attom-master-meta-sample
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
66 cs2 = N.cs id
79d435b16241 Add attom-master-meta-sample
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
67
79d435b16241 Add attom-master-meta-sample
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
68 cs1 : N.CodeSegment ds1 ds1
79d435b16241 Add attom-master-meta-sample
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
69 cs1 = N.cs (\d -> N.goto cs2 d)
79d435b16241 Add attom-master-meta-sample
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
70
79d435b16241 Add attom-master-meta-sample
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
71 cs0 : N.CodeSegment ds0 ds1
79d435b16241 Add attom-master-meta-sample
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
72 cs0 = N.cs (\d -> N.goto cs1 (record {c = (ds0.a d) + (ds0.b d)}))
79d435b16241 Add attom-master-meta-sample
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
73
79d435b16241 Add attom-master-meta-sample
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
74
79d435b16241 Add attom-master-meta-sample
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
75 main : Meta
79d435b16241 Add attom-master-meta-sample
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
76 main = gotoMeta push cs0 (record {context = (record {a = 100 ; b = 50 ; c = 70}) ; c' = 0 ; next = (N.cs id)})
76
29a3a4b79d4d Add comment
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 75
diff changeset
77 -- record {context = record {a = 100 ; b = 50 ; c = 150} ; c' = 70 ; next = (N.cs id)}