changeset 43:0a780145c5ff

Define compose operator using list of subtype
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Wed, 04 Jan 2017 02:21:11 +0000
parents f7916d13e2b1
children 72cf35fb82af
files cbc/named-product.agda
diffstat 1 files changed, 6 insertions(+), 4 deletions(-) [+]
line wrap: on
line diff
--- a/cbc/named-product.agda	Tue Jan 03 09:04:11 2017 +0000
+++ b/cbc/named-product.agda	Wed Jan 04 02:21:11 2017 +0000
@@ -64,7 +64,9 @@
 
 
 data CodeSegment (A B : Set) : (List Set) -> Set where
-  cs : {l : List Set} {{_ : Datum A}} {{_ : Datum B}} -> (A -> B) -> CodeSegment A B l
+  cs : {l : List Set} {{_ : Datum A}} {{_ : Datum B}} -> (A -> B) -> CodeSegment A B (A ∷ B ∷ l)
+
+
   
 
 exec : {I O : Set} -> {l : List Set} {{_ : Datum I}} {{_ : Datum O}} -> CodeSegment I O l -> Context -> Context
@@ -75,8 +77,8 @@
 equiv-exec = refl
 
 
-_◎_ : {A B C : Set} {{_ : Datum A}} {{_ : Datum B}} {{_ : Datum C}} {l ll : List Set}
-       -> CodeSegment B C l -> CodeSegment A B ll -> CodeSegment A C (l ++ ll)
-_◎_ {{da}} {{_}} {{dc}} {l = l} {ll = ll} (cs g) (cs f) = cs  {l = l ++ ll} {{da}} {{dc}} (g ∘ f)
+_◎_ : {A B C : Set} {{_ : Datum A}} {{_ : Datum B}} {{_ : Datum C}} {l ll  : List Set}
+       -> CodeSegment B C (B ∷ C ∷ l) -> CodeSegment A B (A ∷ B ∷ ll) -> CodeSegment A C (A ∷ C ∷ B ∷ (l ++ ll))
+_◎_ {A} {B} {C} {{da}} {{_}} {{dc}} {l} {ll} (cs g) (cs f) =  cs {l = (B ∷ (l ++ ll))} {{da}} {{dc}} (g ∘ f)