# HG changeset patch
# User atton <atton@cr.ie.u-ryukyu.ac.jp>
# Date 1483684191 0
# Node ID 8031568638d01e91556a2c4e1cdd4d99e83d84e2
# Parent  fe57557440713b8c9ff641037a86f30291f05f61
Define composition of codesegment using subtype without constraint list

diff -r fe5755744071 -r 8031568638d0 cbc/named-product.agda
--- a/cbc/named-product.agda	Thu Jan 05 07:01:32 2017 +0000
+++ b/cbc/named-product.agda	Fri Jan 06 06:29:51 2017 +0000
@@ -62,14 +62,14 @@
 equiv = refl
 
 
-data CodeSegment (A B : Set) : (List Set) -> Set where
-  cs : {l : List Set} {{_ : Datum A}} {{_ : Datum B}} -> (A -> B) -> CodeSegment A B l
+data CodeSegment (A B : Set) : Set where
+  cs : {{_ : Datum A}} {{_ : Datum B}} -> (A -> B) -> CodeSegment A B
 
 BasicCS :  Set -> Set -> Set
-BasicCS A B = CodeSegment  A B (A ∷ B ∷ [])
+BasicCS A B = CodeSegment  A B
   
 
-exec : {I O : Set} -> {l : List Set} {{_ : Datum I}} {{_ : Datum O}} -> CodeSegment I O l -> Context -> Context
+exec : {I O : Set} {{_ : Datum I}} {{_ : Datum O}} -> CodeSegment I O -> Context -> Context
 exec {l} {{i}} {{o}}  (cs b) c = Datum.set o c (b (get i c))
 
 
@@ -87,12 +87,12 @@
 equiv-exec = refl
 
 
-csComp : {con : Context} {A B C D : Set} {{_ : Datum A}} {{_ : Datum B}} {{_ : Datum C}} {{_ : Datum D}} {l ll : List Set}
-       -> CodeSegment C D l -> CodeSegment A B ll -> CodeSegment A D (l ++ ll)
-csComp {con} {A} {B} {C} {D} {{da}} {{db}} {{dc}} {{dd}} {l} {ll} (cs g) (cs f)
+csComp : {con : Context} {A B C D : Set} {{_ : Datum A}} {{_ : Datum B}} {{_ : Datum C}} {{_ : Datum D}}
+       -> CodeSegment C D -> CodeSegment A B -> CodeSegment A D
+csComp {con} {A} {B} {C} {D} {{da}} {{db}} {{dc}} {{dd}} (cs g) (cs f)
       = cs {{da}} {{dd}} (comp {con} {{da}} {{db}} {{dc}} {{dd}} g f)
 
-comp-sample : {c : Context} -> CodeSegment LoopCounter LoopCounter (LoopCounter ∷ LoopCounter ∷ LoopCounter ∷ LoopCounter ∷ [])
+comp-sample : {c : Context} -> CodeSegment LoopCounter LoopCounter
 comp-sample {c}  = (csComp {c} csInc csInc)
 
 
@@ -110,45 +110,16 @@
 
 
 
---comp-sample-2 : {c : Context} -> CodeSegment LoopCounter SignatureWithNum (SignatureWithNum ∷ LoopCounter ∷ SignatureWithNum ∷ LoopCounter ∷ [])
---comp-sample-2  = csComp  csUpdateSignature  csInc
-
---apply-sample-2 : Context
---apply-sample-2 = exec (comp-sample-2 {firstContext}) firstContext
+comp-sample-2 : {c : Context} -> CodeSegment LoopCounter SignatureWithNum
+comp-sample-2 {c}  = csComp {c}  csUpdateSignature  csInc
 
-
-open ≡-Reasoning
-
-++empty : {A : Set} -> (l : List A) -> l ++ [] ≡ l
-++empty [] = refl
-++empty (x ∷ l) = cong (\l -> x ∷ l) (++empty l)
+apply-sample-2 : Context
+apply-sample-2 = exec (comp-sample-2 {firstContext}) firstContext
 
 
 
-list-associative : {A : Set} -> (l ll lll : List A) -> l ++ (ll ++ lll) ≡ (l ++ ll) ++ lll
-list-associative [] ll lll       = refl
-list-associative (x ∷ l) [] []  = begin
-  (x ∷ l) ++ [] ++ [] 
-  ≡⟨ ++empty ((x ∷ l)) ⟩ 
-  x ∷ l
-  ≡⟨ sym (++empty (x ∷ l)) ⟩
-  x ∷ l ++ []
-  ≡⟨ sym (++empty ((x ∷ l) ++ [])) ⟩
-  ((x ∷ l) ++ []) ++ []
-  ∎
-list-associative (x ∷ l) [] (xxx ∷ lll) = {!!}
-list-associative (x ∷ l) (x₁ ∷ ll) [] = {!!}
-list-associative (x ∷ l) (x₁ ∷ ll) (x₂ ∷ lll) = {!!}
-
-
-
-
-
-comp-associative : {A B C D E F : Set} {l ll lll : List Set} {con : Context}
+comp-associative : {A B C D E F : Set} {con : Context}
                    {{da : Datum A}} {{db : Datum B}} {{dc : Datum C}} {{dd : Datum D}} {{de : Datum E}} {{df : Datum F}}
-                   -> {a : CodeSegment A B l} {b : CodeSegment C D ll} {c : CodeSegment E F lll} 
-                   -> csComp {con} c (csComp {con} b a)  ≡ {!!} -- csComp (csComp c b) a -- cannot define directly
-                   -- csComp c (csComp b a) has CodeSegment A F (lll ++ ll ++ l)
-                   -- csComp (csComp c b) a has CodeSegment A F ((lll ++ ll) ++ l)
-comp-associative = {!!}
-
+                   -> (a : CodeSegment A B) (b : CodeSegment C D) (c : CodeSegment E F)
+                   -> csComp {con} c (csComp {con} b a)  ≡ csComp {con} (csComp {con} c b) a
+comp-associative (cs _) (cs _) (cs _) = refl