# HG changeset patch
# User atton <atton@cr.ie.u-ryukyu.ac.jp>
# Date 1482047991 0
# Node ID 853318ff55f979a2ae57369b4b67b36c0e0f0e47
# Parent  782a11f3eea44c8e112c97628d09990a1ae9960f
Trying define output data segment

diff -r 782a11f3eea4 -r 853318ff55f9 cbc/variable-tuple.agda
--- a/cbc/variable-tuple.agda	Sun Dec 18 06:41:39 2016 +0000
+++ b/cbc/variable-tuple.agda	Sun Dec 18 07:59:51 2016 +0000
@@ -4,6 +4,7 @@
 open import Data.String
 open import Data.List
 open import Data.Unit
+open import Data.Product
 open import Function using (_∘_)
 open import Relation.Binary.PropositionalEquality
 
@@ -48,14 +49,20 @@
 data CodeSegment : Set₁ where
   cs : Format -> Format -> CodeSegment
 
-ods : CodeSegment -> List Set
-ods (cs ids FEnd)         = []
-ods (cs ids (FSet s f))   = s ∷ (ods (cs ids f))
+csDouble : CodeSegment
+csDouble = cs double double
+
+ods : CodeSegment -> Set
+ods (cs ids FEnd)         = ⊤
+ods (cs ids (FSet s f))   = s × (ods (cs ids f))
+
+ods-double : ods csDouble
+ods-double = "hoge" , zero , tt
+
 
 ids : {A : Set} -> CodeSegment ->  Set
 ids {A} (cs i o) = DataSegment {A} i
 
-
-ids-double : {A : Set} {a : A} -> ids {A} (cs double double)
+ids-double : {A : Set} {a : A} -> ids {A} csDouble
 ids-double {_} {a}  =  \(s : String) -> \(n : ℕ) -> a