Mercurial > hg > Members > atton > agda-proofs

annotate 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
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
37
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 module named-product where
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
2
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 open import Data.Nat
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 open import Data.String
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 open import Data.Vec
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
6
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 record DataSegment (n : ℕ) : Set₁ where
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
8 field
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 name : String
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 ds : Vec (Set -> Set) (suc n)
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
11
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 ids : {A : Set} {n : ℕ} -> DataSegment n -> Set
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 ids {a} {zero} record { name = name ; ds = (x ∷ []) } = x a
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 ids {a} {suc n} record { name = name ; ds = (x ∷ ds) } = x a -> ids {a} {n} record { name = name ; ds = ds }
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
15
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 record LoopCounter (A : Set) : Set where
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
17 field
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
18 counter : ℕ
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
19 name : String
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
20
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
21
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
22 record Context : Set where
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
23 field
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
24 cycle : ℕ
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
25 led : String
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
26 signature : String
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
27
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
28 instance
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
29 contextHasLoopCounter : {A : Set} -> Context -> LoopCounter Context
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
30 contextHasLoopCounter c = record { counter = Context.cycle c ; name = Context.led c}
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
31
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
32 inc : {A : Set} -> LoopCounter A -> LoopCounter A
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
33 inc c = record c { counter = (LoopCounter.counter c) + 1}
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
34
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
35 firstContext : Context
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
36 firstContext = record { cycle = 3 ; led = "q" ; signature = "aaa" }
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
37
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
38 incContextCycle : {{_ : Context -> LoopCounter Context}} -> Context -> Context
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
39 incContextCycle {{lp}} c = record c { cycle = incrementedCycle }
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
40 where
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
41 incrementedCycle = LoopCounter.counter (inc (lp c))
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
42
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
43
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
44
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
45
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
46
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
47
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
48 --data CodeSegment (n m : ℕ) : Set₁ where
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
49 -- cs : (i : DataSegment n) -> (o : DataSegment m) -> CodeSegment n m
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
50
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
51
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
52
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
53 --yoyo : DataSegment
60e604972f30 Trying define codesegment using named-product with subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
54 --yoyo = record { name = "yoyo" ; ds = [ Yo ]}