Mercurial > hg > Members > atton > agda-proofs

comparison cbc/subtype.agda @ 51:16e27df74ec5

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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 ccb34e3f1514
children 4880184e4ab5
comparison
equal deleted inserted replaced
50:ccb34e3f1514 51:16e27df74ec5
1 module subtype where 1 module subtype (Context : Set) where
2 2
3 open import Data.Bool
4 open import Data.Nat
5 open import Data.Nat.Show
6 open import Data.String hiding (_++_ ; show ; toList ; fromList)
7 open import Data.List
8 open import Data.AVL.Sets
9 open import Relation.Binary.PropositionalEquality 3 open import Relation.Binary.PropositionalEquality
10 4
11 5
12 record Context : Set where 6 record DataSegment (A : Set) : Set where
13 field 7 field
14 cycle : ℕ
15 led : String
16 signature : String
17
18 record Datum (A : Set) : Set where
19 field
20 get : Context -> A 8 get : Context -> A
21 set : Context -> A -> Context 9 set : Context -> A -> Context
22 open Datum 10 open DataSegment
23 11
24 record LoopCounter : Set where 12 data CodeSegment (A B : Set) : Set where
25 field 13 cs : {{_ : DataSegment A}} {{_ : DataSegment B}} -> (A -> B) -> CodeSegment A B
26 count : ℕ
27 name : String
28
29 record SignatureWithNum : Set where
30 field
31 signature : String
32 num : ℕ
33
34 instance
35 contextHasLoopCounter : Datum LoopCounter
36 contextHasLoopCounter = record {get = (\c -> record {count = Context.cycle c ;
37 name = Context.led c });
38 set = (\c l -> record {cycle = LoopCounter.count l;
39 led = LoopCounter.name l;
40 signature = Context.signature c})}
41 contextHasSignatureWithNum : Datum SignatureWithNum
42 contextHasSignatureWithNum = record {get = (\c -> record { signature = Context.signature c
43 ; num = Context.cycle c})
44 ;set = (\c s -> record { cycle = SignatureWithNum.num s
45 ; led = Context.led c
46 ; signature = SignatureWithNum.signature s})
47 }
48 14
49 15
50 inc : LoopCounter -> LoopCounter 16 exec : {I O : Set} {{_ : DataSegment I}} {{_ : DataSegment O}} -> CodeSegment I O -> Context -> Context
51 inc l = record l {count = suc (LoopCounter.count l)} 17 exec {l} {{i}} {{o}} (cs b) c = DataSegment.set o c (b (get i c))
52
53 firstContext : Context
54 firstContext = record { cycle = 3 ; led = "q" ; signature = "aaa" }
55 18
56 19
57 incContextCycle : {{_ : Datum LoopCounter }} -> Context -> Context 20 comp : {con : Context} -> {A B C D : Set} {{_ : DataSegment A}} {{_ : DataSegment B}} {{_ : DataSegment C}} {{_ : DataSegment D}}
58 incContextCycle {{l}} c = Datum.set l c (inc (Datum.get l c))
59
60
61 equiv : incContextCycle firstContext ≡ record { cycle = 4 ; led = "q" ; signature = "aaa" }
62 equiv = refl
63
64
65 data CodeSegment (A B : Set) : Set where
66 cs : {{_ : Datum A}} {{_ : Datum B}} -> (A -> B) -> CodeSegment A B
67
68 BasicCS : Set -> Set -> Set
69 BasicCS A B = CodeSegment A B
70
71
72 exec : {I O : Set} {{_ : Datum I}} {{_ : Datum O}} -> CodeSegment I O -> Context -> Context
73 exec {l} {{i}} {{o}} (cs b) c = Datum.set o c (b (get i c))
74
75
76 comp : {con : Context} -> {A B C D : Set} {{_ : Datum A}} {{_ : Datum B}} {{_ : Datum C}} {{_ : Datum D}}
77 -> (C -> D) -> (A -> B) -> A -> D 21 -> (C -> D) -> (A -> B) -> A -> D
78 comp {con} {{i}} {{io}} {{oi}} {{o}} g f x = g (get oi (set io con (f x))) 22 comp {con} {{i}} {{io}} {{oi}} {{o}} g f x = g (get oi (set io con (f x)))
79
80
81 csInc : BasicCS LoopCounter LoopCounter
82 csInc = cs inc
83
84 23
85 24 csComp : {con : Context} {A B C D : Set}
86 equiv-exec : {l : List Set} -> incContextCycle firstContext ≡ exec csInc firstContext 25 {{_ : DataSegment A}} {{_ : DataSegment B}} {{_ : DataSegment C}} {{_ : DataSegment D}}
87 equiv-exec = refl
88
89
90 csComp : {con : Context} {A B C D : Set} {{_ : Datum A}} {{_ : Datum B}} {{_ : Datum C}} {{_ : Datum D}}
91 -> CodeSegment C D -> CodeSegment A B -> CodeSegment A D 26 -> CodeSegment C D -> CodeSegment A B -> CodeSegment A D
92 csComp {con} {A} {B} {C} {D} {{da}} {{db}} {{dc}} {{dd}} (cs g) (cs f) 27 csComp {con} {A} {B} {C} {D} {{da}} {{db}} {{dc}} {{dd}} (cs g) (cs f)
93 = cs {{da}} {{dd}} (comp {con} {{da}} {{db}} {{dc}} {{dd}} g f) 28 = cs {{da}} {{dd}} (comp {con} {{da}} {{db}} {{dc}} {{dd}} g f)
94 29
95 comp-sample : {c : Context} -> CodeSegment LoopCounter LoopCounter
96 comp-sample {c} = (csComp {c} csInc csInc)
97
98
99 apply-sample : Context
100 apply-sample = exec (comp-sample {firstContext}) firstContext
101
102
103
104 updateSignature : SignatureWithNum -> SignatureWithNum
105 updateSignature record { signature = signature ; num = num } = record { signature = (Data.String._++_) signature (show num ) ; num = num}
106
107
108 csUpdateSignature : BasicCS SignatureWithNum SignatureWithNum
109 csUpdateSignature = cs updateSignature
110
111
112
113 comp-sample-2 : {c : Context} -> CodeSegment LoopCounter SignatureWithNum
114 comp-sample-2 {c} = csComp {c} csUpdateSignature csInc
115
116 apply-sample-2 : Context
117 apply-sample-2 = exec (comp-sample-2 {firstContext}) firstContext
118
119 30
120 31
121 comp-associative : {A B C D E F : Set} {con : Context} 32 comp-associative : {A B C D E F : Set} {con : Context}
122 {{da : Datum A}} {{db : Datum B}} {{dc : Datum C}} {{dd : Datum D}} {{de : Datum E}} {{df : Datum F}} 33 {{da : DataSegment A}} {{db : DataSegment B}} {{dc : DataSegment C}}
34 {{dd : DataSegment D}} {{de : DataSegment E}} {{df : DataSegment F}}
123 -> (a : CodeSegment A B) (b : CodeSegment C D) (c : CodeSegment E F) 35 -> (a : CodeSegment A B) (b : CodeSegment C D) (c : CodeSegment E F)
124 -> csComp {con} c (csComp {con} b a) ≡ csComp {con} (csComp {con} c b) a 36 -> csComp {con} c (csComp {con} b a) ≡ csComp {con} (csComp {con} c b) a
125 comp-associative (cs _) (cs _) (cs _) = refl 37 comp-associative (cs _) (cs _) (cs _) = refl