# HG changeset patch
# User atton <atton@cr.ie.u-ryukyu.ac.jp>
# Date 1483332048 0
# Node ID f0759cb39d37922a5dd6e4d6387b11aa6cdf81e5
# Parent  bf667ec8cba42e94726e4b50c2dafaba9ec4e63c
Trying define codesegment using subtype

diff -r bf667ec8cba4 -r f0759cb39d37 cbc/subtype.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/cbc/subtype.agda	Mon Jan 02 04:40:48 2017 +0000
@@ -0,0 +1,35 @@
+module subtype where
+
+open import Level
+open import Function
+open import Data.Nat hiding (_⊔_)
+open import Data.Bool
+
+data DataSegment  (X : Set -> Set) : Set₁  where
+  ds : {x : Set} -> X x -> DataSegment X
+
+
+record DS1 (A : Set) : Set where
+  field
+    counter : A -> ℕ
+
+record DS2 (A : Set) : Set where
+  field
+    useSum : A -> Bool
+
+record Context : Set where
+  field
+    loopCounter : ℕ
+    flag        : Bool
+
+instance
+  ds1 : DS1 Context
+  ds1 = record {counter = Context.loopCounter}
+
+hoge :  Context -> {{ins : DS1 Context}} -> DataSegment DS1
+hoge _ {{i}}  = ds i
+
+
+
+data CodeSegment (I O : (Set -> Set)) : Set₁ where
+  cs : (DataSegment I -> DataSegment O) -> CodeSegment I O