Mercurial > hg > Members > atton > agda-proofs

annotate cbc/subtype-sample.agda @ 52:4880184e4ab5

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Define push/pop using subtype
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Tue, 10 Jan 2017 09:04:55 +0000
parents 16e27df74ec5
children
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
51
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 module subtype-sample where
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
2
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 open import Data.Nat
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 open import Data.Nat.Show
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 open import Data.String hiding (_++_ ; show ; toList ; fromList)
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
6 open import Data.List
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 open import Relation.Binary.PropositionalEquality
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
8
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
9
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
10
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 record Context : Set where
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 field
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 cycle : ℕ
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 led : String
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
15 signature : String
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
16
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
17 open import subtype Context
52
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 51
diff changeset
18
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 51
diff changeset
19
51
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
20 record LoopCounter : Set where
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
21 field
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
22 count : ℕ
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
23 name : String
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
24
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
25 record SignatureWithNum : Set where
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
26 field
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
27 signature : String
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
28 num : ℕ
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
29
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
30 instance
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
31 contextHasLoopCounter : DataSegment LoopCounter
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
32 contextHasLoopCounter = record {get = (\c -> record {count = Context.cycle c ;
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
33 name = Context.led c });
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
34 set = (\c l -> record {cycle = LoopCounter.count l;
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
35 led = LoopCounter.name l;
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
36 signature = Context.signature c})}
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
37 contextHasSignatureWithNum : DataSegment SignatureWithNum
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
38 contextHasSignatureWithNum = record {get = (\c -> record { signature = Context.signature c
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
39 ; num = Context.cycle c})
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
40 ;set = (\c s -> record { cycle = SignatureWithNum.num s
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
41 ; led = Context.led c
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
42 ; signature = SignatureWithNum.signature s})
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
43 }
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
44
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
45 inc : LoopCounter -> LoopCounter
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
46 inc l = record l {count = suc (LoopCounter.count l)}
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
47
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
48 firstContext : Context
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
49 firstContext = record { cycle = 3 ; led = "q" ; signature = "aaa" }
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
50
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
51
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
52 incContextCycle : {{_ : DataSegment LoopCounter }} -> Context -> Context
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
53 incContextCycle {{l}} c = DataSegment.set l c (inc (DataSegment.get l c))
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
54
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
55
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
56 equiv : incContextCycle firstContext ≡ record { cycle = 4 ; led = "q" ; signature = "aaa" }
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
57 equiv = refl
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
58
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
59
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
60 csInc : CodeSegment LoopCounter LoopCounter
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
61 csInc = cs inc
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
62
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
63
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
64
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
65 equiv-exec : {l : List Set} -> incContextCycle firstContext ≡ exec csInc firstContext
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
66 equiv-exec = refl
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
67
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
68 comp-sample : {c : Context} -> CodeSegment LoopCounter LoopCounter
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
69 comp-sample {c} = (csComp {c} csInc csInc)
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
70
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
71
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
72 apply-sample : Context
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
73 apply-sample = exec (comp-sample {firstContext}) firstContext
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
74
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
75
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
76
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
77 updateSignature : SignatureWithNum -> SignatureWithNum
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
78 updateSignature record { signature = signature ; num = num } = record { signature = (Data.String._++_) signature (show num ) ; num = num}
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
79
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
80
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
81 csUpdateSignature : CodeSegment SignatureWithNum SignatureWithNum
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
82 csUpdateSignature = cs updateSignature
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
83
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
84
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
85
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
86 comp-sample-2 : {c : Context} -> CodeSegment LoopCounter SignatureWithNum
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
87 comp-sample-2 {c} = csComp {c} csUpdateSignature csInc
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
88
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
89 apply-sample-2 : Context
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
90 apply-sample-2 = exec (comp-sample-2 {firstContext}) firstContext
16e27df74ec5 Split subtype definitions for reuse context
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
91