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
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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