# HG changeset patch
# User atton <atton@cr.ie.u-ryukyu.ac.jp>
# Date 1483585343 0
# Node ID af1fe3bd9f1e86ec3722f06402c4047e6765760d
# Parent  08b695ca359c83cddca27a012ae33ec06711ebfb
Define code segment compose operator using type -> ds cast

diff -r 08b695ca359c -r af1fe3bd9f1e cbc/named-product.agda
--- a/cbc/named-product.agda	Wed Jan 04 08:16:02 2017 +0000
+++ b/cbc/named-product.agda	Thu Jan 05 03:02:23 2017 +0000
@@ -1,6 +1,6 @@
 module named-product where
 
-open import Function
+
 open import Data.Bool
 open import Data.Nat
 open import Data.Nat.Show
@@ -21,7 +21,7 @@
   field 
     get : Context -> A
     set : Context -> A -> Context
-
+open Datum
 
 record LoopCounter : Set where
   field
@@ -55,6 +55,7 @@
 firstContext : Context
 firstContext = record { cycle = 3 ; led = "q" ; signature = "aaa" }
 
+
 incContextCycle : {{_ : Datum LoopCounter }} -> Context -> Context
 incContextCycle {{l}} c = Datum.set l c (inc (Datum.get l c))
 
@@ -65,34 +66,61 @@
 
 
 data CodeSegment (A B : Set) : (List Set) -> Set where
-  cs : {l : List Set} {{_ : Datum A}} {{_ : Datum B}} -> (A -> B) -> CodeSegment A B (A ∷ B ∷ l)
+  cs : {l : List Set} {{_ : Datum A}} {{_ : Datum B}} -> (A -> B) -> CodeSegment A B (B ∷ A ∷ l)
+
+BasicCS : Set -> Set -> Set
+BasicCS A B = CodeSegment A B (A ∷ B ∷ [])
 
-basicCS : Set -> Set -> Set
-basicCS A B = CodeSegment A B (A ∷ B ∷ [])
+up : {A B : Set} {{_ : Datum A}} {{_ : Datum B}} -> (A -> B) -> Context -> B
+up {{i}} {{o}} f c = f (Datum.get i c)
 
-csInc : basicCS LoopCounter LoopCounter
+
+csInc : BasicCS LoopCounter LoopCounter
 csInc = cs inc
   
 
 exec : {I O : Set} -> {l : List Set} {{_ : Datum I}} {{_ : Datum O}} -> CodeSegment I O l -> Context -> Context
-exec {l} {{i}} {{o}}  (cs b) c =   Datum.set o c (b (Datum.get i c))
+exec {l} {{i}} {{o}}  (cs b) c = Datum.set o c (b (get i c))
+
+--upCast : {A B : Set} {{_ : Datum A}} {{_ : Datum B}} -> (A -> B) -> (Datum A -> Datum B)
+--upCast {{i}} {{o}} f a = record { get = (\c -> f (Datum.get a c))
+--                                ; set = (\c b -> Datum.set o c b)}
+
+--downCast : {A B : Set} {{i : Datum A}} {{o : Datum B}} -> (Datum A -> Datum B) -> A -> B
+--downCast {{i = record { get = get ; set = set }}} {{record { get = get₁ ; set = set₁ }}} f a = {!!}
 
 
-equiv-exec : {l : List Set} -> incContextCycle firstContext ≡ exec (cs {l = l} inc) firstContext
+apply : {A B : Set} {{_ : Datum A}} {{_ : Datum B}} -> (A -> B) -> Context -> B
+apply {{i}} {{o}} f c = f (get i c)
+
+
+_∘_ : {con : Context} -> {A B C D : Set} {{_ : Datum A}} {{_ : Datum B}} {{_ : Datum C}} {{_ : Datum D}}
+       -> (C -> D) -> (A -> B) -> A -> D
+_∘_ {con} {{i}} {{io}} {{oi}} {{o}} g f x = g (get oi (set io con (f x)))
+                                         
+                                           
+                                       
+
+
+
+equiv-exec : {l : List Set} -> incContextCycle firstContext ≡ exec csInc firstContext
 equiv-exec = refl
 
 
-_◎_ : {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)
+_◎_ : {con : Context} {A B C D : Set} {{_ : Datum A}} {{_ : Datum B}} {{_ : Datum C}} {{_ : Datum D}} {l ll : List Set}
+       -> CodeSegment C D (D ∷ C ∷ l) -> CodeSegment A B (B ∷ A ∷ ll) -> CodeSegment A D (D ∷ A ∷ C ∷ B ∷ (l ++ ll))
+_◎_ {con} {A} {B} {C} {D} {{da}} {{db}} {{dc}} {{dd}} {l} {ll} (cs g) (cs f)
+      = cs {l = (C ∷ B ∷ (l ++ ll))} {{da}} {{dd}} (_∘_ {con} {{da}} {{db}} {{dc}} {{dd}} g f)
 
 
-comp-sample : CodeSegment LoopCounter LoopCounter (LoopCounter ∷ LoopCounter ∷ LoopCounter ∷ [])
+comp-sample : CodeSegment LoopCounter LoopCounter (LoopCounter ∷ LoopCounter ∷ LoopCounter ∷ LoopCounter ∷ [])
 comp-sample = csInc ◎ csInc
 
+
 apply-sample : Context
 apply-sample = exec comp-sample firstContext
 
+{-
 
 updateSignature : SignatureWithNum -> SignatureWithNum
 updateSignature record { signature = signature ; num = num } = record { signature = (Data.String._++_) signature (show num ) ; num = num}
@@ -100,5 +128,6 @@
 csUpdateSignature : basicCS SignatureWithNum SignatureWithNum
 csUpdateSignature = cs updateSignature
 
-comp-sample-2 : CodeSegment LoopCounter SignatureWithNum ?
-comp-sample-2 = csUpdateSignature ◎ csInc
+--comp-sample-2 : CodeSegment LoopCounter SignatureWithNum ?
+--comp-sample-2 = csUpdateSignature ◎ csInc
+-}