# HG changeset patch
# User atton <atton@cr.ie.u-ryukyu.ac.jp>
# Date 1483496818 0
# Node ID 72cf35fb82af48b3d2de4244ce57e06c748cdf7a
# Parent  0a780145c5ff53253160f38c6a64ce847a2c6095
Add composition sample

diff -r 0a780145c5ff -r 72cf35fb82af cbc/named-product.agda
--- a/cbc/named-product.agda	Wed Jan 04 02:21:11 2017 +0000
+++ b/cbc/named-product.agda	Wed Jan 04 02:26:58 2017 +0000
@@ -66,7 +66,11 @@
 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)
 
+basicCS : Set -> Set -> Set
+basicCS A B = CodeSegment A B (A ∷ B ∷ [])
 
+csInc : basicCS LoopCounter LoopCounter
+csInc = cs inc
   
 
 exec : {I O : Set} -> {l : List Set} {{_ : Datum I}} {{_ : Datum O}} -> CodeSegment I O l -> Context -> Context
@@ -82,3 +86,8 @@
 _◎_ {A} {B} {C} {{da}} {{_}} {{dc}} {l} {ll} (cs g) (cs f) =  cs {l = (B ∷ (l ++ ll))} {{da}} {{dc}} (g ∘ f)
 
 
+comp-sample : CodeSegment LoopCounter LoopCounter (LoopCounter ∷ LoopCounter ∷ LoopCounter ∷ [])
+comp-sample = csInc ◎ csInc
+
+apply-sample : Context
+apply-sample = exec comp-sample firstContext