Mercurial > hg > Members > atton > agda-proofs

comparison cbc/subtype-sample.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
children 4880184e4ab5
comparison
equal deleted inserted replaced
50:ccb34e3f1514 51:16e27df74ec5
1 module subtype-sample where
2
3 open import Data.Nat
4 open import Data.Nat.Show
5 open import Data.String hiding (_++_ ; show ; toList ; fromList)
6 open import Data.List
7 open import Relation.Binary.PropositionalEquality
8
9
10
11 record Context : Set where
12 field
13 cycle : ℕ
14 led : String
15 signature : String
16
17 open import subtype Context
18 record LoopCounter : Set where
19 field
20 count : ℕ
21 name : String
22
23 record SignatureWithNum : Set where
24 field
25 signature : String
26 num : ℕ
27
28 instance
29 contextHasLoopCounter : DataSegment LoopCounter
30 contextHasLoopCounter = record {get = (\c -> record {count = Context.cycle c ;
31 name = Context.led c });
32 set = (\c l -> record {cycle = LoopCounter.count l;
33 led = LoopCounter.name l;
34 signature = Context.signature c})}
35 contextHasSignatureWithNum : DataSegment SignatureWithNum
36 contextHasSignatureWithNum = record {get = (\c -> record { signature = Context.signature c
37 ; num = Context.cycle c})
38 ;set = (\c s -> record { cycle = SignatureWithNum.num s
39 ; led = Context.led c
40 ; signature = SignatureWithNum.signature s})
41 }
42
43 inc : LoopCounter -> LoopCounter
44 inc l = record l {count = suc (LoopCounter.count l)}
45
46 firstContext : Context
47 firstContext = record { cycle = 3 ; led = "q" ; signature = "aaa" }
48
49
50 incContextCycle : {{_ : DataSegment LoopCounter }} -> Context -> Context
51 incContextCycle {{l}} c = DataSegment.set l c (inc (DataSegment.get l c))
52
53
54 equiv : incContextCycle firstContext ≡ record { cycle = 4 ; led = "q" ; signature = "aaa" }
55 equiv = refl
56
57
58 csInc : CodeSegment LoopCounter LoopCounter
59 csInc = cs inc
60
61
62
63 equiv-exec : {l : List Set} -> incContextCycle firstContext ≡ exec csInc firstContext
64 equiv-exec = refl
65
66 comp-sample : {c : Context} -> CodeSegment LoopCounter LoopCounter
67 comp-sample {c} = (csComp {c} csInc csInc)
68
69
70 apply-sample : Context
71 apply-sample = exec (comp-sample {firstContext}) firstContext
72
73
74
75 updateSignature : SignatureWithNum -> SignatureWithNum
76 updateSignature record { signature = signature ; num = num } = record { signature = (Data.String._++_) signature (show num ) ; num = num}
77
78
79 csUpdateSignature : CodeSegment SignatureWithNum SignatureWithNum
80 csUpdateSignature = cs updateSignature
81
82
83
84 comp-sample-2 : {c : Context} -> CodeSegment LoopCounter SignatureWithNum
85 comp-sample-2 {c} = csComp {c} csUpdateSignature csInc
86
87 apply-sample-2 : Context
88 apply-sample-2 = exec (comp-sample-2 {firstContext}) firstContext
89