view cbc/subtype.agda @ 36:f0759cb39d37

Trying define codesegment using subtype
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Mon, 02 Jan 2017 04:40:48 +0000
parents
children
line wrap: on
line source

module subtype where

open import Level
open import Function
open import Data.Nat hiding (_⊔_)
open import Data.Bool

data DataSegment  (X : Set -> Set) : Set₁  where
  ds : {x : Set} -> X x -> DataSegment X


record DS1 (A : Set) : Set where
  field
    counter : A -> ℕ

record DS2 (A : Set) : Set where
  field
    useSum : A -> Bool

record Context : Set where
  field
    loopCounter : ℕ
    flag        : Bool

instance
  ds1 : DS1 Context
  ds1 = record {counter = Context.loopCounter}

hoge :  Context -> {{ins : DS1 Context}} -> DataSegment DS1
hoge _ {{i}}  = ds i



data CodeSegment (I O : (Set -> Set)) : Set₁ where
  cs : (DataSegment I -> DataSegment O) -> CodeSegment I O