Mercurial > hg > Members > atton > agda-proofs

comparison cbc/named-product.agda @ 38:a0ca5e29a9dc

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Call subtype using user-defined cast operator
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Tue, 03 Jan 2017 05:19:04 +0000
parents 60e604972f30
children d8312361afdc
comparison
equal deleted inserted replaced
37:60e604972f30 38:a0ca5e29a9dc
1 module named-product where 1 module named-product where
2 2
3 open import Function
3 open import Data.Nat 4 open import Data.Nat
4 open import Data.String 5 open import Data.String
5 open import Data.Vec 6 open import Data.Vec
7 open import Relation.Binary.PropositionalEquality
8
9
6 10
7 record DataSegment (n : ℕ) : Set₁ where 11 record DataSegment (n : ℕ) : Set₁ where
8 field 12 field
9 name : String 13 name : String
10 ds : Vec (Set -> Set) (suc n) 14 ds : Vec (Set -> Set) (suc n)
11 15
12 ids : {A : Set} {n : ℕ} -> DataSegment n -> Set 16 ids : {A : Set} {n : ℕ} -> DataSegment n -> Set
13 ids {a} {zero} record { name = name ; ds = (x ∷ []) } = x a 17 ids {a} {zero} record { name = name ; ds = (x ∷ []) } = x a
14 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 }
15 19
16 record LoopCounter (A : Set) : Set where 20
21 record _<<<_ (A : Set) (B : Set) : Set where
22 field
23 get : B -> A
24 set : B -> A -> B
25
26 open _<<<_
27
28
29 record LoopCounter : Set where
17 field 30 field
18 counter : ℕ 31 count : ℕ
19 name : String 32 name : String
20
21 33
22 record Context : Set where 34 record Context : Set where
23 field 35 field
24 cycle : ℕ 36 cycle : ℕ
25 led : String 37 led : String
26 signature : String 38 signature : String
27 39
40
28 instance 41 instance
29 contextHasLoopCounter : {A : Set} -> Context -> LoopCounter Context 42 contextHasLoopCounter : LoopCounter <<< Context
30 contextHasLoopCounter c = record { counter = Context.cycle c ; name = Context.led c} 43 contextHasLoopCounter = record {get = (\c -> record {count = Context.cycle c ;
44 name = Context.led c });
45 set = (\c l -> record {cycle = LoopCounter.count l;
46 led = LoopCounter.name l;
47 signature = Context.signature c})
48 }
31 49
32 inc : {A : Set} -> LoopCounter A -> LoopCounter A 50
33 inc c = record c { counter = (LoopCounter.counter c) + 1} 51 inc : LoopCounter -> LoopCounter
52 inc l = record l {count = suc (LoopCounter.count l)}
34 53
35 firstContext : Context 54 firstContext : Context
36 firstContext = record { cycle = 3 ; led = "q" ; signature = "aaa" } 55 firstContext = record { cycle = 3 ; led = "q" ; signature = "aaa" }
37 56
38 incContextCycle : {{_ : Context -> LoopCounter Context}} -> Context -> Context 57 incContextCycle : {{_ : LoopCounter <<< Context }} -> Context -> Context
39 incContextCycle {{lp}} c = record c { cycle = incrementedCycle } 58 incContextCycle {{l}} c = set l c (inc (get l c))
40 where
41 incrementedCycle = LoopCounter.counter (inc (lp c))
42 59
43 60
44 61 equiv : incContextCycle firstContext ≡ record { cycle = 4 ; led = "q" ; signature = "aaa" }
62 equiv = refl
45 63
46 64
47 65
48 --data CodeSegment (n m : ℕ) : Set₁ where 66 --data CodeSegment (n m : ℕ) : Set₁ where
49 -- cs : (i : DataSegment n) -> (o : DataSegment m) -> CodeSegment n m 67 -- cs : (i : DataSegment n) -> (o : DataSegment m) -> CodeSegment n m