Mercurial > hg > Members > atton > agda-proofs
comparison cbc/named-product.agda @ 37:60e604972f30
Trying define codesegment using named-product with subtype
author | atton <atton@cr.ie.u-ryukyu.ac.jp> |
---|---|
date | Mon, 02 Jan 2017 07:00:55 +0000 |
parents | |
children | a0ca5e29a9dc |
comparison
equal
deleted
inserted
replaced
36:f0759cb39d37 | 37:60e604972f30 |
---|---|
1 module named-product where | |
2 | |
3 open import Data.Nat | |
4 open import Data.String | |
5 open import Data.Vec | |
6 | |
7 record DataSegment (n : ℕ) : Set₁ where | |
8 field | |
9 name : String | |
10 ds : Vec (Set -> Set) (suc n) | |
11 | |
12 ids : {A : Set} {n : ℕ} -> DataSegment n -> Set | |
13 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 } | |
15 | |
16 record LoopCounter (A : Set) : Set where | |
17 field | |
18 counter : ℕ | |
19 name : String | |
20 | |
21 | |
22 record Context : Set where | |
23 field | |
24 cycle : ℕ | |
25 led : String | |
26 signature : String | |
27 | |
28 instance | |
29 contextHasLoopCounter : {A : Set} -> Context -> LoopCounter Context | |
30 contextHasLoopCounter c = record { counter = Context.cycle c ; name = Context.led c} | |
31 | |
32 inc : {A : Set} -> LoopCounter A -> LoopCounter A | |
33 inc c = record c { counter = (LoopCounter.counter c) + 1} | |
34 | |
35 firstContext : Context | |
36 firstContext = record { cycle = 3 ; led = "q" ; signature = "aaa" } | |
37 | |
38 incContextCycle : {{_ : Context -> LoopCounter Context}} -> Context -> Context | |
39 incContextCycle {{lp}} c = record c { cycle = incrementedCycle } | |
40 where | |
41 incrementedCycle = LoopCounter.counter (inc (lp c)) | |
42 | |
43 | |
44 | |
45 | |
46 | |
47 | |
48 --data CodeSegment (n m : ℕ) : Set₁ where | |
49 -- cs : (i : DataSegment n) -> (o : DataSegment m) -> CodeSegment n m | |
50 | |
51 | |
52 | |
53 --yoyo : DataSegment | |
54 --yoyo = record { name = "yoyo" ; ds = [ Yo ]} |