Mercurial > hg > Members > atton > agda-proofs
annotate cbc/named-product.agda @ 43:0a780145c5ff
Define compose operator using list of subtype
author | atton <atton@cr.ie.u-ryukyu.ac.jp> |
---|---|
date | Wed, 04 Jan 2017 02:21:11 +0000 |
parents | f7916d13e2b1 |
children | 72cf35fb82af |
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 |
42
f7916d13e2b1
Trying define type composition using list of subtype...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
41
diff
changeset
|
6 open import Data.String hiding (_++_) |
41
2abf1cd97f10
Trying define type composition using list of subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
40
diff
changeset
|
7 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
|
8 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
|
9 |
37
60e604972f30
Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
10 |
40
e6b965df2137
Trying define type composition using subtype through DS
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
39
diff
changeset
|
11 |
39
d8312361afdc
Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
38
diff
changeset
|
12 |
d8312361afdc
Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
38
diff
changeset
|
13 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
|
14 field |
d8312361afdc
Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
38
diff
changeset
|
15 cycle : ℕ |
d8312361afdc
Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
38
diff
changeset
|
16 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
|
17 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
|
18 |
d8312361afdc
Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
38
diff
changeset
|
19 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
|
20 field |
d8312361afdc
Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
38
diff
changeset
|
21 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
|
22 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
|
23 |
38
a0ca5e29a9dc
Call subtype using user-defined cast operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
37
diff
changeset
|
24 |
a0ca5e29a9dc
Call subtype using user-defined cast operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
37
diff
changeset
|
25 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
|
26 field |
38
a0ca5e29a9dc
Call subtype using user-defined cast operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
37
diff
changeset
|
27 count : ℕ |
a0ca5e29a9dc
Call subtype using user-defined cast operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
37
diff
changeset
|
28 name : String |
37
60e604972f30
Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
29 |
39
d8312361afdc
Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
38
diff
changeset
|
30 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
|
31 field |
60e604972f30
Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
32 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
|
33 num : ℕ |
38
a0ca5e29a9dc
Call subtype using user-defined cast operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
37
diff
changeset
|
34 |
37
60e604972f30
Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
35 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
|
36 contextHasLoopCounter : Datum LoopCounter |
38
a0ca5e29a9dc
Call subtype using user-defined cast operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
37
diff
changeset
|
37 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
|
38 name = Context.led c }); |
a0ca5e29a9dc
Call subtype using user-defined cast operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
37
diff
changeset
|
39 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
|
40 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
|
41 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
|
42 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
|
43 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
|
44 ; 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
|
45 ;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
|
46 ; 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
|
47 ; 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
|
48 } |
37
60e604972f30
Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
49 |
38
a0ca5e29a9dc
Call subtype using user-defined cast operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
37
diff
changeset
|
50 |
a0ca5e29a9dc
Call subtype using user-defined cast operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
37
diff
changeset
|
51 inc : LoopCounter -> LoopCounter |
a0ca5e29a9dc
Call subtype using user-defined cast operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
37
diff
changeset
|
52 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
|
53 |
60e604972f30
Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
54 firstContext : Context |
60e604972f30
Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
55 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
|
56 |
39
d8312361afdc
Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
38
diff
changeset
|
57 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
|
58 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
|
59 |
60e604972f30
Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
60 |
38
a0ca5e29a9dc
Call subtype using user-defined cast operator
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
37
diff
changeset
|
61 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
|
62 equiv = refl |
37
60e604972f30
Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
63 |
40
e6b965df2137
Trying define type composition using subtype through DS
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
39
diff
changeset
|
64 |
39
d8312361afdc
Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
38
diff
changeset
|
65 |
41
2abf1cd97f10
Trying define type composition using list of subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
40
diff
changeset
|
66 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
|
67 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
|
68 |
0a780145c5ff
Define compose operator using list of subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
42
diff
changeset
|
69 |
40
e6b965df2137
Trying define type composition using subtype through DS
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
39
diff
changeset
|
70 |
e6b965df2137
Trying define type composition using subtype through DS
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
39
diff
changeset
|
71 |
42
f7916d13e2b1
Trying define type composition using list of subtype...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
41
diff
changeset
|
72 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
|
73 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
|
74 |
60e604972f30
Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
75 |
42
f7916d13e2b1
Trying define type composition using list of subtype...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
41
diff
changeset
|
76 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
|
77 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
|
78 |
37
60e604972f30
Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
79 |
43
0a780145c5ff
Define compose operator using list of subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
42
diff
changeset
|
80 _◎_ : {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
|
81 -> 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
|
82 _◎_ {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
|
83 |
f7916d13e2b1
Trying define type composition using list of subtype...
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
41
diff
changeset
|
84 |