Mercurial > hg > Members > atton > agda-proofs

annotate cbc/named-product.agda @ 41:2abf1cd97f10

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Trying define type composition using list of subtype
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Tue, 03 Jan 2017 08:21:25 +0000
parents e6b965df2137
children f7916d13e2b1
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
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
6 open import Data.String
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
2abf1cd97f10 Trying define type composition using list of subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
67 cs : {l : List Set} {{_ : Datum A}} {{_ : Datum B}} -> (A -> B) -> CodeSegment A B (A ∷ (B ∷ l))
40
e6b965df2137 Trying define type composition using subtype through DS
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 39
diff changeset
68
e6b965df2137 Trying define type composition using subtype through DS
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 39
diff changeset
69
41
2abf1cd97f10 Trying define type composition using list of subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
70 exec : {I O : Set} -> {l : List Set} {{_ : Datum I}} {{_ : Datum O}} -> CodeSegment I O l -> Context -> Context
39
d8312361afdc Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
71 exec {{i}} {{o}} (cs b) c = Datum.set o c (b (Datum.get i c))
d8312361afdc Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
72
40
e6b965df2137 Trying define type composition using subtype through DS
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 39
diff changeset
73
41
2abf1cd97f10 Trying define type composition using list of subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
74 equiv-exec : {l : List Set} -> incContextCycle firstContext ≡ exec (cs {l = l} inc) firstContext
39
d8312361afdc Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
75 equiv-exec = refl
41
2abf1cd97f10 Trying define type composition using list of subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 40
diff changeset
76
40
e6b965df2137 Trying define type composition using subtype through DS
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 39
diff changeset
77 {-
37
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
78
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
79
40
e6b965df2137 Trying define type composition using subtype through DS
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 39
diff changeset
80 InputIsHead : {n : ℕ} {I O : Set} {l : Vec Set (suc (suc n))} -> (cs : CodeSegment I O l) -> I ≡ head l
e6b965df2137 Trying define type composition using subtype through DS
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 39
diff changeset
81 InputIsHead (cs _) = refl
37
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
82
40
e6b965df2137 Trying define type composition using subtype through DS
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 39
diff changeset
83 OutputIsLast : {n : ℕ} {I O : Set} {l : Vec Set (suc (suc n))} -> (cs : CodeSegment I O l) -> O ≡ last l
e6b965df2137 Trying define type composition using subtype through DS
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 39
diff changeset
84 OutputIsLast {_} {_} {_} {l} (cs x) = {!!}
37
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
85
40
e6b965df2137 Trying define type composition using subtype through DS
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 39
diff changeset
86 -}
39
d8312361afdc Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
87
d8312361afdc Call subtype using user-defined cast operator with subtype list
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 38
diff changeset
88
37
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
89
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
90 --yoyo : DataSegment
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
91 --yoyo = record { name = "yoyo" ; ds = [ Yo ]}