--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/cbc/subtype-sample.agda	Tue Jan 10 02:04:55 2017 +0000
@@ -0,0 +1,89 @@
+module subtype-sample where
+
+open import Data.Nat
+open import Data.Nat.Show
+open import Data.String hiding (_++_ ; show ; toList ; fromList)
+open import Data.List
+open import Relation.Binary.PropositionalEquality
+
+
+
+record Context : Set where
+  field
+    cycle : ℕ
+    led   : String
+    signature : String
+    
+open import subtype Context
+record LoopCounter : Set where
+  field
+    count : ℕ
+    name  : String
+
+record SignatureWithNum : Set where
+  field
+    signature : String
+    num       : ℕ
+
+instance
+  contextHasLoopCounter : DataSegment 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})}
+  contextHasSignatureWithNum : DataSegment 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
+inc  l = record l {count = suc (LoopCounter.count l)}
+
+firstContext : Context
+firstContext = record { cycle = 3 ; led = "q" ; signature = "aaa" }
+
+
+incContextCycle : {{_ : DataSegment LoopCounter }} -> Context -> Context
+incContextCycle {{l}} c = DataSegment.set l c (inc (DataSegment.get l c))
+
+
+equiv : incContextCycle firstContext ≡ record { cycle = 4 ; led = "q" ; signature = "aaa" }
+equiv = refl
+
+
+csInc : CodeSegment LoopCounter LoopCounter
+csInc = cs inc
+
+
+
+equiv-exec : {l : List Set} -> incContextCycle firstContext ≡ exec csInc firstContext
+equiv-exec = refl
+
+comp-sample : {c : Context} -> CodeSegment LoopCounter LoopCounter
+comp-sample {c}  = (csComp {c} csInc csInc)
+
+
+apply-sample : Context
+apply-sample = exec (comp-sample {firstContext}) firstContext
+
+
+
+updateSignature : SignatureWithNum -> SignatureWithNum
+updateSignature record { signature = signature ; num = num } = record { signature = (Data.String._++_) signature (show num ) ; num = num}
+
+
+csUpdateSignature : CodeSegment SignatureWithNum SignatureWithNum
+csUpdateSignature = cs updateSignature
+
+
+
+comp-sample-2 : {c : Context} -> CodeSegment LoopCounter SignatureWithNum
+comp-sample-2 {c}  = csComp {c}  csUpdateSignature  csInc
+
+apply-sample-2 : Context
+apply-sample-2 = exec (comp-sample-2 {firstContext}) firstContext
+