# HG changeset patch
# User atton <atton@cr.ie.u-ryukyu.ac.jp>
# Date 1482043299 0
# Node ID 782a11f3eea44c8e112c97628d09990a1ae9960f
# Parent  7bfae9affc84682c95fb5b68644f47e779a17d86
Trying define input data segment

diff -r 7bfae9affc84 -r 782a11f3eea4 cbc/variable-tuple.agda
--- a/cbc/variable-tuple.agda	Sun Dec 18 01:35:31 2016 +0000
+++ b/cbc/variable-tuple.agda	Sun Dec 18 06:41:39 2016 +0000
@@ -3,6 +3,7 @@
 open import Data.Nat hiding (_<_ ; _>_)
 open import Data.String
 open import Data.List
+open import Data.Unit
 open import Function using (_∘_)
 open import Relation.Binary.PropositionalEquality
 
@@ -13,23 +14,6 @@
 <> : Format
 <> = FEnd
 
-{-
-  begin_ : ∀{x y : A} → x ≡ y → x ≡ y
-  begin_ x≡y = x≡y
-
-  _≡⟨⟩_ : ∀ (x {y} : A) → x ≡ y → x ≡ y
-  _ ≡⟨⟩ x≡y = x≡y
-
-  _≡⟨_⟩_ : ∀ (x {y z} : A) → x ≡ y → y ≡ z → x ≡ z
-  _ ≡⟨ x≡y ⟩ y≡z = trans x≡y y≡z
-
-  _≅⟨_⟩_ : ∀ (x {y z} : A) → x ≅ y → y ≡ z → x ≡ z
-  _ ≅⟨ x≅y ⟩ y≡z = trans (H.≅-to-≡ x≅y) y≡z
-
-  _∎ : ∀ (x : A) → x ≡ x
-  _∎ _ = refl
--}
-
 infix  51 _>
 _> : (Format -> Format) -> Format
 _> f = f FEnd
@@ -38,7 +22,7 @@
 _||_ : (Format -> Format) -> Set -> (Format -> Format)
 _||_ f1 s = f1 ∘ (FSet s)
 
-infix 54 <_
+infix 53 <_
 <_ : Set -> Format -> Format
 <_ s = FSet s
 
@@ -54,3 +38,24 @@
 
 triple : Format
 triple = < String || ℕ  || (List ℕ) >
+
+
+DataSegment : {A : Set} -> Format -> Set
+DataSegment {A} FEnd       = A
+DataSegment {A} (FSet x f) = x -> (DataSegment {A} f)
+
+
+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))
+
+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}  =  \(s : String) -> \(n : ℕ) -> a
+