Mercurial > hg > Members > atton > agda-proofs
annotate cbc/subtype-sample.agda @ 51:16e27df74ec5
Split subtype definitions for reuse context
author | atton <atton@cr.ie.u-ryukyu.ac.jp> |
---|---|
date | Tue, 10 Jan 2017 02:04:55 +0000 |
parents | |
children | 4880184e4ab5 |
rev | line source |
---|---|
51
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
1 module subtype-sample where |
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
2 |
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
3 open import Data.Nat |
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
4 open import Data.Nat.Show |
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
5 open import Data.String hiding (_++_ ; show ; toList ; fromList) |
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
6 open import Data.List |
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
7 open import Relation.Binary.PropositionalEquality |
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
8 |
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
9 |
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
10 |
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
11 record Context : Set where |
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
12 field |
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
13 cycle : ℕ |
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
14 led : String |
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
15 signature : String |
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
16 |
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
17 open import subtype Context |
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
18 record LoopCounter : Set where |
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
19 field |
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
20 count : ℕ |
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
21 name : String |
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
22 |
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
23 record SignatureWithNum : Set where |
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
24 field |
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
25 signature : String |
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
26 num : ℕ |
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
27 |
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
28 instance |
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
29 contextHasLoopCounter : DataSegment LoopCounter |
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
30 contextHasLoopCounter = record {get = (\c -> record {count = Context.cycle c ; |
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
31 name = Context.led c }); |
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
32 set = (\c l -> record {cycle = LoopCounter.count l; |
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
33 led = LoopCounter.name l; |
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
34 signature = Context.signature c})} |
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
35 contextHasSignatureWithNum : DataSegment SignatureWithNum |
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
36 contextHasSignatureWithNum = record {get = (\c -> record { signature = Context.signature c |
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
37 ; num = Context.cycle c}) |
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
38 ;set = (\c s -> record { cycle = SignatureWithNum.num s |
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
39 ; led = Context.led c |
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
40 ; signature = SignatureWithNum.signature s}) |
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
41 } |
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
42 |
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
43 inc : LoopCounter -> LoopCounter |
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
44 inc l = record l {count = suc (LoopCounter.count l)} |
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
45 |
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
46 firstContext : Context |
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
47 firstContext = record { cycle = 3 ; led = "q" ; signature = "aaa" } |
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
48 |
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
49 |
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
50 incContextCycle : {{_ : DataSegment LoopCounter }} -> Context -> Context |
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
51 incContextCycle {{l}} c = DataSegment.set l c (inc (DataSegment.get l c)) |
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
52 |
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
53 |
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
54 equiv : incContextCycle firstContext ≡ record { cycle = 4 ; led = "q" ; signature = "aaa" } |
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
55 equiv = refl |
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
56 |
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
57 |
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
58 csInc : CodeSegment LoopCounter LoopCounter |
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
59 csInc = cs inc |
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
60 |
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
61 |
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
62 |
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
63 equiv-exec : {l : List Set} -> incContextCycle firstContext ≡ exec csInc firstContext |
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
64 equiv-exec = refl |
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
65 |
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
66 comp-sample : {c : Context} -> CodeSegment LoopCounter LoopCounter |
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
67 comp-sample {c} = (csComp {c} csInc csInc) |
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
68 |
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
69 |
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
70 apply-sample : Context |
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
71 apply-sample = exec (comp-sample {firstContext}) firstContext |
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
72 |
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
73 |
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
74 |
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
75 updateSignature : SignatureWithNum -> SignatureWithNum |
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
76 updateSignature record { signature = signature ; num = num } = record { signature = (Data.String._++_) signature (show num ) ; num = num} |
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
77 |
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
78 |
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
79 csUpdateSignature : CodeSegment SignatureWithNum SignatureWithNum |
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
80 csUpdateSignature = cs updateSignature |
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
81 |
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
82 |
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
83 |
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
84 comp-sample-2 : {c : Context} -> CodeSegment LoopCounter SignatureWithNum |
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
85 comp-sample-2 {c} = csComp {c} csUpdateSignature csInc |
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
86 |
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
87 apply-sample-2 : Context |
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
88 apply-sample-2 = exec (comp-sample-2 {firstContext}) firstContext |
16e27df74ec5
Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
89 |