# HG changeset patch
# User atton <atton@cr.ie.u-ryukyu.ac.jp>
# Date 1483340455 0
# Node ID 60e604972f30368d63fcae2b078f7b0eb501eee8
# Parent  f0759cb39d37922a5dd6e4d6387b11aa6cdf81e5
Trying define codesegment using named-product with subtype

diff -r f0759cb39d37 -r 60e604972f30 cbc/named-product.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/cbc/named-product.agda	Mon Jan 02 07:00:55 2017 +0000
@@ -0,0 +1,54 @@
+module named-product where
+
+open import Data.Nat
+open import Data.String
+open import Data.Vec
+
+record DataSegment (n : ℕ) : Set₁ where
+  field
+    name : String
+    ds   : Vec (Set -> Set) (suc n)
+
+ids : {A : Set} {n : ℕ} -> DataSegment n -> Set
+ids {a} {zero}  record { name = name ; ds = (x ∷ []) } = x a
+ids {a} {suc n} record { name = name ; ds = (x ∷ ds) } = x a -> ids {a} {n} record { name = name ; ds = ds }
+
+record LoopCounter (A : Set) : Set where
+  field
+    counter : ℕ
+    name    : String
+
+
+record Context : Set where
+  field
+    cycle : ℕ
+    led   : String
+    signature : String
+
+instance
+  contextHasLoopCounter : {A : Set} -> Context -> LoopCounter Context
+  contextHasLoopCounter c = record { counter = Context.cycle c ; name = Context.led c}
+
+inc : {A :  Set} -> LoopCounter A -> LoopCounter A
+inc c = record c { counter =  (LoopCounter.counter c) + 1}
+
+firstContext : Context
+firstContext = record { cycle = 3 ; led = "q" ; signature = "aaa" }
+
+incContextCycle : {{_ : Context -> LoopCounter Context}} -> Context -> Context
+incContextCycle {{lp}} c = record c { cycle = incrementedCycle }
+  where
+    incrementedCycle = LoopCounter.counter (inc (lp c))
+
+
+
+
+
+
+--data CodeSegment (n m : ℕ) : Set₁ where
+--  cs : (i : DataSegment n) -> (o : DataSegment m) -> CodeSegment n m
+
+
+
+--yoyo : DataSegment
+--yoyo = record { name = "yoyo" ; ds = [ Yo ]}