# HG changeset patch
# User atton <atton@cr.ie.u-ryukyu.ac.jp>
# Date 1483425706 0
# Node ID d8312361afdc7aecfa63a1d24538c8f7d713609a
# Parent  a0ca5e29a9dcc86c2d3f786937fa1dde0b792a70
Call subtype using user-defined cast operator with subtype list

diff -r a0ca5e29a9dc -r d8312361afdc cbc/named-product.agda
--- a/cbc/named-product.agda	Tue Jan 03 05:19:04 2017 +0000
+++ b/cbc/named-product.agda	Tue Jan 03 06:41:46 2017 +0000
@@ -1,13 +1,13 @@
 module named-product where
 
 open import Function
+open import Data.Bool
 open import Data.Nat
 open import Data.String
-open import Data.Vec
+open import Data.List
 open import Relation.Binary.PropositionalEquality
 
-
-
+{-
 record DataSegment (n : ℕ) : Set₁ where
   field
     name : String
@@ -16,14 +16,20 @@
 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 Context : Set where
+  field
+    cycle : ℕ
+    led   : String
+    signature : String
+
+record Datum (A : Set) : Set where
+  field 
+    get : Context -> A
+    set : Context -> A -> Context
 
 
-record _<<<_ (A : Set) (B : Set) : Set where
-  field 
-    get : B -> A
-    set : B -> A -> B
-
-open _<<<_
 
 
 record LoopCounter : Set where
@@ -31,21 +37,25 @@
     count : ℕ
     name  : String
 
-record Context : Set where
+record SignatureWithNum : Set where
   field
-    cycle : ℕ
-    led   : String
     signature : String
-
+    num       : ℕ
 
 instance
-  contextHasLoopCounter : LoopCounter <<< Context
+  contextHasLoopCounter : Datum LoopCounter
   contextHasLoopCounter = record {get = (\c   -> record {count = Context.cycle c ;
                                                          name  = Context.led   c });
                                   set = (\c l -> record {cycle     = LoopCounter.count l;
                                                          led       = LoopCounter.name  l;
-                                                         signature = Context.signature c})
-                                  }
+                                                         signature = Context.signature c})}
+  contextHasSignatureWithNum : Datum SignatureWithNum
+  contextHasSignatureWithNum = record {get = (\c -> record { signature = Context.signature c
+                                                           ; num       = Context.cycle     c})
+                                      ;set = (\c s -> record { cycle = SignatureWithNum.num s
+                                                             ; led    = Context.led c
+                                                             ; signature = SignatureWithNum.signature s})
+                                      }
 
 
 inc :  LoopCounter -> LoopCounter
@@ -54,19 +64,29 @@
 firstContext : Context
 firstContext = record { cycle = 3 ; led = "q" ; signature = "aaa" }
 
-incContextCycle : {{_ : LoopCounter <<< Context }} -> Context -> Context
-incContextCycle {{l}} c = set l c (inc (get l c))
+incContextCycle : {{_ : Datum LoopCounter }} -> Context -> Context
+incContextCycle {{l}} c = Datum.set l c (inc (Datum.get l c))
 
 
 equiv : incContextCycle firstContext ≡ record { cycle = 4 ; led = "q" ; signature = "aaa" }
 equiv = refl
 
+data CodeSegment (A B : Set) : (List Set) -> Set₁ where
+  cs : {{_ : Datum A}} {{_ : Datum B}} -> (A -> B) -> CodeSegment A B (A ∷ B ∷ [])
+
+exec : {I O : Set} -> {l : List Set} {{_ : Datum I}} {{_ : Datum O}} -> CodeSegment I O l -> Context -> Context
+exec {{i}} {{o}} (cs b) c = Datum.set o c (b (Datum.get i c))
+
+equiv-exec : incContextCycle firstContext ≡ exec (cs inc) firstContext
+equiv-exec = refl
 
 
---data CodeSegment (n m : ℕ) : Set₁ where
---  cs : (i : DataSegment n) -> (o : DataSegment m) -> CodeSegment n m
+--InputIsHead : {I : Set} (l : List Set) -> (cs : CodeSegment I _ l) -> I ≡ head l
+--InputIsHead = ?
 
 
+  
+
 
 --yoyo : DataSegment
 --yoyo = record { name = "yoyo" ; ds = [ Yo ]}