# HG changeset patch
# User atton <atton@cr.ie.u-ryukyu.ac.jp>
# Date 1483420744 0
# Node ID a0ca5e29a9dcc86c2d3f786937fa1dde0b792a70
# Parent  60e604972f30368d63fcae2b078f7b0eb501eee8
Call subtype using user-defined cast operator

diff -r 60e604972f30 -r a0ca5e29a9dc cbc/named-product.agda
--- a/cbc/named-product.agda	Mon Jan 02 07:00:55 2017 +0000
+++ b/cbc/named-product.agda	Tue Jan 03 05:19:04 2017 +0000
@@ -1,8 +1,12 @@
 module named-product where
 
+open import Function
 open import Data.Nat
 open import Data.String
 open import Data.Vec
+open import Relation.Binary.PropositionalEquality
+
+
 
 record DataSegment (n : ℕ) : Set₁ where
   field
@@ -13,11 +17,19 @@
 ids {a} {zero}  record { name = name ; ds = (x ∷ []) } = x a
 ids {a} {suc n} record { name = name ; ds = (x ∷ ds) } = x a -> ids {a} {n} record { name = name ; ds = ds }
 
-record LoopCounter (A : Set) : Set where
+
+record _<<<_ (A : Set) (B : Set) : Set where
+  field 
+    get : B -> A
+    set : B -> A -> B
+
+open _<<<_
+
+
+record LoopCounter : Set where
   field
-    counter : ℕ
-    name    : String
-
+    count : ℕ
+    name  : String
 
 record Context : Set where
   field
@@ -25,23 +37,29 @@
     led   : String
     signature : String
 
+
 instance
-  contextHasLoopCounter : {A : Set} -> Context -> LoopCounter Context
-  contextHasLoopCounter c = record { counter = Context.cycle c ; name = Context.led c}
+  contextHasLoopCounter : LoopCounter <<< Context
+  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})
+                                  }
 
-inc : {A :  Set} -> LoopCounter A -> LoopCounter A
-inc c = record c { counter =  (LoopCounter.counter c) + 1}
+
+inc :  LoopCounter -> LoopCounter
+inc  l = record l {count = suc (LoopCounter.count l)}
 
 firstContext : Context
 firstContext = record { cycle = 3 ; led = "q" ; signature = "aaa" }
 
-incContextCycle : {{_ : Context -> LoopCounter Context}} -> Context -> Context
-incContextCycle {{lp}} c = record c { cycle = incrementedCycle }
-  where
-    incrementedCycle = LoopCounter.counter (inc (lp c))
+incContextCycle : {{_ : LoopCounter <<< Context }} -> Context -> Context
+incContextCycle {{l}} c = set l c (inc (get l c))
 
 
-
+equiv : incContextCycle firstContext ≡ record { cycle = 4 ; led = "q" ; signature = "aaa" }
+equiv = refl