Mercurial > hg > Members > atton > agda-proofs

comparison cbc/variable-tuple.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 da78bb99d654
children
comparison
equal deleted inserted replaced
25:da78bb99d654 26:d503a73186ce
39 double = < String || ℕ > 39 double = < String || ℕ >
40 40
41 triple : Format 41 triple : Format
42 triple = < String || ℕ || (List ℕ) > 42 triple = < String || ℕ || (List ℕ) >
43 43
44 data CodeSegment (I O : Set) : Set₁ where
45 cs : (I -> O) -> CodeSegment I O
46
47
48 twiceWithName : (String × ℕ ) -> (String × ℕ )
49 twiceWithName (s , n) = s , twice n
50 where
51 twice : ℕ -> ℕ
52 twice zero = zero
53 twice (ℕ.suc n₁) = (ℕ.suc (ℕ.suc (twice n₁)))
54
55 csDouble : CodeSegment (String × ℕ) (String × ℕ)
56 csDouble = cs twiceWithName
57
58
59 ods : {I O : Set} -> CodeSegment I O -> Set
60 ods {i} {o} c = o
61
62 ods-double : ods csDouble
63 ods-double = "hoge" , zero
64
65
66 ids : {I O : Set} -> CodeSegment I O -> Set
67 ids {i} {o} c = i
68
69 ids-double : ids csDouble
70 ids-double = "fuga" , 3
71
72 --ids-double : {A : Set} {a : A} -> ids csDouble
73 --ids-double {_} {a} = \(s : String) -> \(n : ℕ) -> a
74
75
76
77 executeCS : {A B : Set} -> CodeSegment A B -> (A -> B)
78 executeCS (cs b) = b
79
80
81
82 infixr 30 _◎_
83 _◎_ : {A B C : Set} -> CodeSegment A B -> CodeSegment B C -> CodeSegment A C
84 (cs b1) ◎ (cs b2) = cs (b2 ∘ b1)
85
86
87
88
89 ◎-double : CodeSegment (String × ℕ) (String × ℕ )
90 --◎-double = csDouble ◎ csDouble ◎ csDouble -- ok
91 ◎-double = csDouble ◎ (cs (\s -> tt)) ◎ (cs (\t -> ("yo" , 100))) -- ok
92 --◎-double = csDouble ◎ (cs (\s -> tt)) ◎ csDouble -- ng (valid type check)
93
94