Mercurial > hg > Members > atton > agda-proofs
annotate cbc/named-product.agda @ 45:08b695ca359c
Cannot compose code segments has another type signature ...
author | atton <atton@cr.ie.u-ryukyu.ac.jp> |
---|---|
date | Wed, 04 Jan 2017 08:16:02 +0000 |
parents | 72cf35fb82af |
children | af1fe3bd9f1e |
rev | line source |
---|---|
37
60e604972f30
Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
1 module named-product where |
60e604972f30
Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
2 |
38
a0ca5e29a9dc
Call subtype using user-defined cast operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
37
diff
changeset
|
3 open import Function |
39
d8312361afdc
Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
38
diff
changeset
|
4 open import Data.Bool |
37
60e604972f30
Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
5 open import Data.Nat |
45
08b695ca359c
Cannot compose code segments has another type signature ...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
44
diff
changeset
|
6 open import Data.Nat.Show |
08b695ca359c
Cannot compose code segments has another type signature ...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
44
diff
changeset
|
7 open import Data.String hiding (_++_ ; show) |
41
2abf1cd97f10
Trying define type composition using list of subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
40
diff
changeset
|
8 open import Data.List |
38
a0ca5e29a9dc
Call subtype using user-defined cast operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
37
diff
changeset
|
9 open import Relation.Binary.PropositionalEquality |
a0ca5e29a9dc
Call subtype using user-defined cast operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
37
diff
changeset
|
10 |
37
60e604972f30
Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
11 |
40
e6b965df2137
Trying define type composition using subtype through DS
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
39
diff
changeset
|
12 |
39
d8312361afdc
Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
38
diff
changeset
|
13 |
d8312361afdc
Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
38
diff
changeset
|
14 record Context : Set where |
d8312361afdc
Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
38
diff
changeset
|
15 field |
d8312361afdc
Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
38
diff
changeset
|
16 cycle : ℕ |
d8312361afdc
Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
38
diff
changeset
|
17 led : String |
d8312361afdc
Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
38
diff
changeset
|
18 signature : String |
d8312361afdc
Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
38
diff
changeset
|
19 |
d8312361afdc
Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
38
diff
changeset
|
20 record Datum (A : Set) : Set where |
d8312361afdc
Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
38
diff
changeset
|
21 field |
d8312361afdc
Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
38
diff
changeset
|
22 get : Context -> A |
d8312361afdc
Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
38
diff
changeset
|
23 set : Context -> A -> Context |
37
60e604972f30
Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
24 |
38
a0ca5e29a9dc
Call subtype using user-defined cast operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
37
diff
changeset
|
25 |
a0ca5e29a9dc
Call subtype using user-defined cast operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
37
diff
changeset
|
26 record LoopCounter : Set where |
37
60e604972f30
Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
27 field |
38
a0ca5e29a9dc
Call subtype using user-defined cast operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
37
diff
changeset
|
28 count : ℕ |
a0ca5e29a9dc
Call subtype using user-defined cast operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
37
diff
changeset
|
29 name : String |
37
60e604972f30
Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
30 |
39
d8312361afdc
Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
38
diff
changeset
|
31 record SignatureWithNum : Set where |
37
60e604972f30
Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
32 field |
60e604972f30
Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
33 signature : String |
39
d8312361afdc
Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
38
diff
changeset
|
34 num : ℕ |
38
a0ca5e29a9dc
Call subtype using user-defined cast operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
37
diff
changeset
|
35 |
37
60e604972f30
Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
36 instance |
39
d8312361afdc
Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
38
diff
changeset
|
37 contextHasLoopCounter : Datum LoopCounter |
38
a0ca5e29a9dc
Call subtype using user-defined cast operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
37
diff
changeset
|
38 contextHasLoopCounter = record {get = (\c -> record {count = Context.cycle c ; |
a0ca5e29a9dc
Call subtype using user-defined cast operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
37
diff
changeset
|
39 name = Context.led c }); |
a0ca5e29a9dc
Call subtype using user-defined cast operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
37
diff
changeset
|
40 set = (\c l -> record {cycle = LoopCounter.count l; |
a0ca5e29a9dc
Call subtype using user-defined cast operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
37
diff
changeset
|
41 led = LoopCounter.name l; |
39
d8312361afdc
Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
38
diff
changeset
|
42 signature = Context.signature c})} |
d8312361afdc
Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
38
diff
changeset
|
43 contextHasSignatureWithNum : Datum SignatureWithNum |
d8312361afdc
Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
38
diff
changeset
|
44 contextHasSignatureWithNum = record {get = (\c -> record { signature = Context.signature c |
d8312361afdc
Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
38
diff
changeset
|
45 ; num = Context.cycle c}) |
d8312361afdc
Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
38
diff
changeset
|
46 ;set = (\c s -> record { cycle = SignatureWithNum.num s |
d8312361afdc
Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
38
diff
changeset
|
47 ; led = Context.led c |
d8312361afdc
Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
38
diff
changeset
|
48 ; signature = SignatureWithNum.signature s}) |
d8312361afdc
Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
38
diff
changeset
|
49 } |
37
60e604972f30
Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
50 |
38
a0ca5e29a9dc
Call subtype using user-defined cast operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
37
diff
changeset
|
51 |
a0ca5e29a9dc
Call subtype using user-defined cast operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
37
diff
changeset
|
52 inc : LoopCounter -> LoopCounter |
a0ca5e29a9dc
Call subtype using user-defined cast operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
37
diff
changeset
|
53 inc l = record l {count = suc (LoopCounter.count l)} |
37
60e604972f30
Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
54 |
60e604972f30
Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
55 firstContext : Context |
60e604972f30
Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
56 firstContext = record { cycle = 3 ; led = "q" ; signature = "aaa" } |
60e604972f30
Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
57 |
39
d8312361afdc
Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
38
diff
changeset
|
58 incContextCycle : {{_ : Datum LoopCounter }} -> Context -> Context |
d8312361afdc
Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
38
diff
changeset
|
59 incContextCycle {{l}} c = Datum.set l c (inc (Datum.get l c)) |
37
60e604972f30
Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
60 |
60e604972f30
Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
61 |
38
a0ca5e29a9dc
Call subtype using user-defined cast operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
37
diff
changeset
|
62 equiv : incContextCycle firstContext ≡ record { cycle = 4 ; led = "q" ; signature = "aaa" } |
a0ca5e29a9dc
Call subtype using user-defined cast operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
37
diff
changeset
|
63 equiv = refl |
37
60e604972f30
Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
64 |
40
e6b965df2137
Trying define type composition using subtype through DS
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
39
diff
changeset
|
65 |
39
d8312361afdc
Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
38
diff
changeset
|
66 |
41
2abf1cd97f10
Trying define type composition using list of subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
40
diff
changeset
|
67 data CodeSegment (A B : Set) : (List Set) -> Set where |
43
0a780145c5ff
Define compose operator using list of subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
42
diff
changeset
|
68 cs : {l : List Set} {{_ : Datum A}} {{_ : Datum B}} -> (A -> B) -> CodeSegment A B (A ∷ B ∷ l) |
0a780145c5ff
Define compose operator using list of subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
42
diff
changeset
|
69 |
44 | 70 basicCS : Set -> Set -> Set |
71 basicCS A B = CodeSegment A B (A ∷ B ∷ []) | |
43
0a780145c5ff
Define compose operator using list of subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
42
diff
changeset
|
72 |
44 | 73 csInc : basicCS LoopCounter LoopCounter |
74 csInc = cs inc | |
40
e6b965df2137
Trying define type composition using subtype through DS
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
39
diff
changeset
|
75 |
e6b965df2137
Trying define type composition using subtype through DS
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
39
diff
changeset
|
76 |
42
f7916d13e2b1
Trying define type composition using list of subtype...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
41
diff
changeset
|
77 exec : {I O : Set} -> {l : List Set} {{_ : Datum I}} {{_ : Datum O}} -> CodeSegment I O l -> Context -> Context |
f7916d13e2b1
Trying define type composition using list of subtype...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
41
diff
changeset
|
78 exec {l} {{i}} {{o}} (cs b) c = Datum.set o c (b (Datum.get i c)) |
37
60e604972f30
Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
79 |
60e604972f30
Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
80 |
42
f7916d13e2b1
Trying define type composition using list of subtype...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
41
diff
changeset
|
81 equiv-exec : {l : List Set} -> incContextCycle firstContext ≡ exec (cs {l = l} inc) firstContext |
f7916d13e2b1
Trying define type composition using list of subtype...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
41
diff
changeset
|
82 equiv-exec = refl |
39
d8312361afdc
Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
38
diff
changeset
|
83 |
37
60e604972f30
Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
84 |
43
0a780145c5ff
Define compose operator using list of subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
42
diff
changeset
|
85 _◎_ : {A B C : Set} {{_ : Datum A}} {{_ : Datum B}} {{_ : Datum C}} {l ll : List Set} |
0a780145c5ff
Define compose operator using list of subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
42
diff
changeset
|
86 -> CodeSegment B C (B ∷ C ∷ l) -> CodeSegment A B (A ∷ B ∷ ll) -> CodeSegment A C (A ∷ C ∷ B ∷ (l ++ ll)) |
0a780145c5ff
Define compose operator using list of subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
42
diff
changeset
|
87 _◎_ {A} {B} {C} {{da}} {{_}} {{dc}} {l} {ll} (cs g) (cs f) = cs {l = (B ∷ (l ++ ll))} {{da}} {{dc}} (g ∘ f) |
42
f7916d13e2b1
Trying define type composition using list of subtype...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
41
diff
changeset
|
88 |
f7916d13e2b1
Trying define type composition using list of subtype...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
41
diff
changeset
|
89 |
44 | 90 comp-sample : CodeSegment LoopCounter LoopCounter (LoopCounter ∷ LoopCounter ∷ LoopCounter ∷ []) |
91 comp-sample = csInc ◎ csInc | |
92 | |
93 apply-sample : Context | |
94 apply-sample = exec comp-sample firstContext | |
45
08b695ca359c
Cannot compose code segments has another type signature ...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
44
diff
changeset
|
95 |
08b695ca359c
Cannot compose code segments has another type signature ...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
44
diff
changeset
|
96 |
08b695ca359c
Cannot compose code segments has another type signature ...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
44
diff
changeset
|
97 updateSignature : SignatureWithNum -> SignatureWithNum |
08b695ca359c
Cannot compose code segments has another type signature ...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
44
diff
changeset
|
98 updateSignature record { signature = signature ; num = num } = record { signature = (Data.String._++_) signature (show num ) ; num = num} |
08b695ca359c
Cannot compose code segments has another type signature ...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
44
diff
changeset
|
99 |
08b695ca359c
Cannot compose code segments has another type signature ...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
44
diff
changeset
|
100 csUpdateSignature : basicCS SignatureWithNum SignatureWithNum |
08b695ca359c
Cannot compose code segments has another type signature ...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
44
diff
changeset
|
101 csUpdateSignature = cs updateSignature |
08b695ca359c
Cannot compose code segments has another type signature ...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
44
diff
changeset
|
102 |
08b695ca359c
Cannot compose code segments has another type signature ...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
44
diff
changeset
|
103 comp-sample-2 : CodeSegment LoopCounter SignatureWithNum ? |
08b695ca359c
Cannot compose code segments has another type signature ...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
44
diff
changeset
|
104 comp-sample-2 = csUpdateSignature ◎ csInc |