Mercurial > hg > Members > atton > agda-proofs

comparison cbc/named-product.agda @ 37:60e604972f30

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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 ]}