Mercurial > hg > Members > atton > agda-proofs

annotate cbc/product.agda @ 26:d503a73186ce

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Split cbc type definition using product
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Fri, 23 Dec 2016 02:50:03 +0000
parents
children 892f8b3aa57e
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
26
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 module product where
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
2
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 open import Data.String
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 open import Data.Product
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 open import Data.Nat
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
6 open import Function using (_∘_ ; id)
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 open import Data.Unit
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
8
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 data CodeSegment (I O : Set) : Set₁ where
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 cs : (I -> O) -> CodeSegment I O
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
11
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
12
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 twiceWithName : (String × ℕ ) -> (String × ℕ )
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 twiceWithName (s , n) = s , twice n
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
15 where
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 twice : ℕ -> ℕ
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
17 twice zero = zero
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
18 twice (ℕ.suc n₁) = (ℕ.suc (ℕ.suc (twice n₁)))
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
19
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
20 csDouble : CodeSegment (String × ℕ) (String × ℕ)
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
21 csDouble = cs twiceWithName
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
22
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
23
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
24 ods : {I O : Set} -> CodeSegment I O -> Set
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
25 ods {i} {o} c = o
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
26
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
27 ods-double : ods csDouble
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
28 ods-double = "hoge" , zero
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
29
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
30
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
31 ids : {I O : Set} -> CodeSegment I O -> Set
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
32 ids {i} {o} c = i
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
33
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
34 ids-double : ids csDouble
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
35 ids-double = "fuga" , 3
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
36
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
37 --ids-double : {A : Set} {a : A} -> ids csDouble
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
38 --ids-double {_} {a} = \(s : String) -> \(n : ℕ) -> a
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
39
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
40
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
41
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
42 executeCS : {A B : Set} -> CodeSegment A B -> (A -> B)
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
43 executeCS (cs b) = b
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
44
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
45
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
46
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
47 infixr 30 _◎_
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
48 _◎_ : {A B C : Set} -> CodeSegment A B -> CodeSegment B C -> CodeSegment A C
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
49 (cs b1) ◎ (cs b2) = cs (b2 ∘ b1)
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
50
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
51
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
52
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
53
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
54 ◎-double : CodeSegment (String × ℕ) (String × ℕ )
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
55 --◎-double = csDouble ◎ csDouble ◎ csDouble -- ok
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
56 ◎-double = csDouble ◎ (cs (\s -> tt)) ◎ (cs (\t -> ("yo" , 100))) -- ok
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
57 --◎-double = csDouble ◎ (cs (\s -> tt)) ◎ csDouble -- ng (valid type check)
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
58
d503a73186ce Split cbc type definition using product
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
59