# HG changeset patch
# User atton <atton@cr.ie.u-ryukyu.ac.jp>
# Date 1482461403 0
# Node ID d503a73186ceb4e3378989fc026f4725c91b8144
# Parent  da78bb99d65493022cc20a7122fc4f18235409a6
Split cbc type definition using product

diff -r da78bb99d654 -r d503a73186ce cbc/product.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/cbc/product.agda	Fri Dec 23 02:50:03 2016 +0000
@@ -0,0 +1,59 @@
+module product where
+
+open import Data.String
+open import Data.Product
+open import Data.Nat
+open import Function using (_∘_ ; id)
+open import Data.Unit
+
+data CodeSegment (I O : Set) : Set₁ where
+  cs : (I -> O) -> CodeSegment I O
+
+
+twiceWithName : (String × ℕ ) -> (String × ℕ )
+twiceWithName (s , n) = s , twice n
+  where
+    twice : ℕ -> ℕ
+    twice zero        = zero
+    twice (ℕ.suc n₁) = (ℕ.suc (ℕ.suc (twice n₁)))
+
+csDouble : CodeSegment (String × ℕ) (String × ℕ)
+csDouble = cs twiceWithName
+
+
+ods : {I O : Set} -> CodeSegment I O -> Set
+ods {i} {o} c = o
+
+ods-double : ods csDouble
+ods-double = "hoge" , zero
+
+
+ids : {I O : Set} -> CodeSegment I O -> Set
+ids {i} {o} c = i
+
+ids-double : ids csDouble
+ids-double = "fuga" , 3
+
+--ids-double : {A : Set} {a : A} -> ids csDouble
+--ids-double {_} {a}  =  \(s : String) -> \(n : ℕ) -> a
+
+
+
+executeCS : {A B : Set} ->  CodeSegment A B -> (A -> B)
+executeCS (cs b) = b
+
+
+
+infixr 30  _◎_
+_◎_ : {A B C : Set} -> CodeSegment A B -> CodeSegment B C -> CodeSegment A C
+(cs b1) ◎ (cs b2) = cs (b2 ∘ b1)
+
+
+
+
+◎-double : CodeSegment (String × ℕ) (String × ℕ )
+--◎-double = csDouble ◎ csDouble ◎ csDouble  -- ok
+◎-double = csDouble ◎ (cs (\s -> tt)) ◎ (cs (\t -> ("yo" , 100))) -- ok
+--◎-double = csDouble ◎ (cs (\s -> tt)) ◎ csDouble  -- ng (valid type check)
+
+
diff -r da78bb99d654 -r d503a73186ce cbc/variable-tuple.agda
--- a/cbc/variable-tuple.agda	Fri Dec 23 02:36:46 2016 +0000
+++ b/cbc/variable-tuple.agda	Fri Dec 23 02:50:03 2016 +0000
@@ -41,54 +41,3 @@
 triple : Format
 triple = < String || ℕ  || (List ℕ) >
 
-data CodeSegment (I O : Set) : Set₁ where
-  cs : (I -> O) -> CodeSegment I O
-
-
-twiceWithName : (String × ℕ ) -> (String × ℕ )
-twiceWithName (s , n) = s , twice n
-  where
-    twice : ℕ -> ℕ
-    twice zero        = zero
-    twice (ℕ.suc n₁) = (ℕ.suc (ℕ.suc (twice n₁)))
-
-csDouble : CodeSegment (String × ℕ) (String × ℕ)
-csDouble = cs twiceWithName
-
-
-ods : {I O : Set} -> CodeSegment I O -> Set
-ods {i} {o} c = o
-
-ods-double : ods csDouble
-ods-double = "hoge" , zero
-
-
-ids : {I O : Set} -> CodeSegment I O -> Set
-ids {i} {o} c = i
-
-ids-double : ids csDouble
-ids-double = "fuga" , 3
-
---ids-double : {A : Set} {a : A} -> ids csDouble
---ids-double {_} {a}  =  \(s : String) -> \(n : ℕ) -> a
-
-
-
-executeCS : {A B : Set} ->  CodeSegment A B -> (A -> B)
-executeCS (cs b) = b
-
-
-
-infixr 30  _◎_
-_◎_ : {A B C : Set} -> CodeSegment A B -> CodeSegment B C -> CodeSegment A C
-(cs b1) ◎ (cs b2) = cs (b2 ∘ b1)
-
-
-
-
-◎-double : CodeSegment (String × ℕ) (String × ℕ )
---◎-double = csDouble ◎ csDouble ◎ csDouble  -- ok
-◎-double = csDouble ◎ (cs (\s -> tt)) ◎ (cs (\t -> ("yo" , 100))) -- ok
---◎-double = csDouble ◎ (cs (\s -> tt)) ◎ csDouble  -- ng (valid type check)
-
-