Mercurial > hg > Members > atton > agda-proofs

comparison cbc/named-product.agda @ 39:d8312361afdc

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Call subtype using user-defined cast operator with subtype list
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Tue, 03 Jan 2017 06:41:46 +0000
parents a0ca5e29a9dc
children e6b965df2137
comparison
equal deleted inserted replaced
38:a0ca5e29a9dc 39:d8312361afdc
1 module named-product where 1 module named-product where
2 2
3 open import Function 3 open import Function
4 open import Data.Bool
4 open import Data.Nat 5 open import Data.Nat
5 open import Data.String 6 open import Data.String
6 open import Data.Vec 7 open import Data.List
7 open import Relation.Binary.PropositionalEquality 8 open import Relation.Binary.PropositionalEquality
8 9
9 10 {-
10
11 record DataSegment (n : ℕ) : Set₁ where 11 record DataSegment (n : ℕ) : Set₁ where
12 field 12 field
13 name : String 13 name : String
14 ds : Vec (Set -> Set) (suc n) 14 ds : Vec (Set -> Set) (suc n)
15 15
16 ids : {A : Set} {n : ℕ} -> DataSegment n -> Set 16 ids : {A : Set} {n : ℕ} -> DataSegment n -> Set
17 ids {a} {zero} record { name = name ; ds = (x ∷ []) } = x a 17 ids {a} {zero} record { name = name ; ds = (x ∷ []) } = x a
18 ids {a} {suc n} record { name = name ; ds = (x ∷ ds) } = x a -> ids {a} {n} record { name = name ; ds = ds } 18 ids {a} {suc n} record { name = name ; ds = (x ∷ ds) } = x a -> ids {a} {n} record { name = name ; ds = ds }
19 -}
20
21 record Context : Set where
22 field
23 cycle : ℕ
24 led : String
25 signature : String
26
27 record Datum (A : Set) : Set where
28 field
29 get : Context -> A
30 set : Context -> A -> Context
19 31
20 32
21 record _<<<_ (A : Set) (B : Set) : Set where
22 field
23 get : B -> A
24 set : B -> A -> B
25
26 open _<<<_
27 33
28 34
29 record LoopCounter : Set where 35 record LoopCounter : Set where
30 field 36 field
31 count : ℕ 37 count : ℕ
32 name : String 38 name : String
33 39
34 record Context : Set where 40 record SignatureWithNum : Set where
35 field 41 field
36 cycle : ℕ
37 led : String
38 signature : String 42 signature : String
39 43 num : ℕ
40 44
41 instance 45 instance
42 contextHasLoopCounter : LoopCounter <<< Context 46 contextHasLoopCounter : Datum LoopCounter
43 contextHasLoopCounter = record {get = (\c -> record {count = Context.cycle c ; 47 contextHasLoopCounter = record {get = (\c -> record {count = Context.cycle c ;
44 name = Context.led c }); 48 name = Context.led c });
45 set = (\c l -> record {cycle = LoopCounter.count l; 49 set = (\c l -> record {cycle = LoopCounter.count l;
46 led = LoopCounter.name l; 50 led = LoopCounter.name l;
47 signature = Context.signature c}) 51 signature = Context.signature c})}
48 } 52 contextHasSignatureWithNum : Datum SignatureWithNum
53 contextHasSignatureWithNum = record {get = (\c -> record { signature = Context.signature c
54 ; num = Context.cycle c})
55 ;set = (\c s -> record { cycle = SignatureWithNum.num s
56 ; led = Context.led c
57 ; signature = SignatureWithNum.signature s})
58 }
49 59
50 60
51 inc : LoopCounter -> LoopCounter 61 inc : LoopCounter -> LoopCounter
52 inc l = record l {count = suc (LoopCounter.count l)} 62 inc l = record l {count = suc (LoopCounter.count l)}
53 63
54 firstContext : Context 64 firstContext : Context
55 firstContext = record { cycle = 3 ; led = "q" ; signature = "aaa" } 65 firstContext = record { cycle = 3 ; led = "q" ; signature = "aaa" }
56 66
57 incContextCycle : {{_ : LoopCounter <<< Context }} -> Context -> Context 67 incContextCycle : {{_ : Datum LoopCounter }} -> Context -> Context
58 incContextCycle {{l}} c = set l c (inc (get l c)) 68 incContextCycle {{l}} c = Datum.set l c (inc (Datum.get l c))
59 69
60 70
61 equiv : incContextCycle firstContext ≡ record { cycle = 4 ; led = "q" ; signature = "aaa" } 71 equiv : incContextCycle firstContext ≡ record { cycle = 4 ; led = "q" ; signature = "aaa" }
62 equiv = refl 72 equiv = refl
63 73
74 data CodeSegment (A B : Set) : (List Set) -> Set₁ where
75 cs : {{_ : Datum A}} {{_ : Datum B}} -> (A -> B) -> CodeSegment A B (A ∷ B ∷ [])
76
77 exec : {I O : Set} -> {l : List Set} {{_ : Datum I}} {{_ : Datum O}} -> CodeSegment I O l -> Context -> Context
78 exec {{i}} {{o}} (cs b) c = Datum.set o c (b (Datum.get i c))
79
80 equiv-exec : incContextCycle firstContext ≡ exec (cs inc) firstContext
81 equiv-exec = refl
64 82
65 83
66 --data CodeSegment (n m : ℕ) : Set₁ where 84 --InputIsHead : {I : Set} (l : List Set) -> (cs : CodeSegment I _ l) -> I ≡ head l
67 -- cs : (i : DataSegment n) -> (o : DataSegment m) -> CodeSegment n m 85 --InputIsHead = ?
68 86
87
88
69 89
70 90
71 --yoyo : DataSegment 91 --yoyo : DataSegment
72 --yoyo = record { name = "yoyo" ; ds = [ Yo ]} 92 --yoyo = record { name = "yoyo" ; ds = [ Yo ]}