view cbc/subtype-sample.agda @ 51:16e27df74ec5

Split subtype definitions for reuse context
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Tue, 10 Jan 2017 02:04:55 +0000
parents
children 4880184e4ab5
line wrap: on
line source

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