Mercurial > hg > Members > atton > agda-proofs

annotate cbc/subtype.agda @ 36:f0759cb39d37

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
36
f0759cb39d37 Trying define codesegment using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 module subtype where
f0759cb39d37 Trying define codesegment using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
2
f0759cb39d37 Trying define codesegment using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 open import Level
f0759cb39d37 Trying define codesegment using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 open import Function
f0759cb39d37 Trying define codesegment using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 open import Data.Nat hiding (_⊔_)
f0759cb39d37 Trying define codesegment using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
6 open import Data.Bool
f0759cb39d37 Trying define codesegment using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
7
f0759cb39d37 Trying define codesegment using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
8 data DataSegment (X : Set -> Set) : Set₁ where
f0759cb39d37 Trying define codesegment using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 ds : {x : Set} -> X x -> DataSegment X
f0759cb39d37 Trying define codesegment using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
10
f0759cb39d37 Trying define codesegment using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
11
f0759cb39d37 Trying define codesegment using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 record DS1 (A : Set) : Set where
f0759cb39d37 Trying define codesegment using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 field
f0759cb39d37 Trying define codesegment using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 counter : A -> ℕ
f0759cb39d37 Trying define codesegment using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
15
f0759cb39d37 Trying define codesegment using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 record DS2 (A : Set) : Set where
f0759cb39d37 Trying define codesegment using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
17 field
f0759cb39d37 Trying define codesegment using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
18 useSum : A -> Bool
f0759cb39d37 Trying define codesegment using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
19
f0759cb39d37 Trying define codesegment using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
20 record Context : Set where
f0759cb39d37 Trying define codesegment using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
21 field
f0759cb39d37 Trying define codesegment using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
22 loopCounter : ℕ
f0759cb39d37 Trying define codesegment using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
23 flag : Bool
f0759cb39d37 Trying define codesegment using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
24
f0759cb39d37 Trying define codesegment using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
25 instance
f0759cb39d37 Trying define codesegment using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
26 ds1 : DS1 Context
f0759cb39d37 Trying define codesegment using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
27 ds1 = record {counter = Context.loopCounter}
f0759cb39d37 Trying define codesegment using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
28
f0759cb39d37 Trying define codesegment using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
29 hoge : Context -> {{ins : DS1 Context}} -> DataSegment DS1
f0759cb39d37 Trying define codesegment using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
30 hoge _ {{i}} = ds i
f0759cb39d37 Trying define codesegment using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
31
f0759cb39d37 Trying define codesegment using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
32
f0759cb39d37 Trying define codesegment using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
33
f0759cb39d37 Trying define codesegment using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
34 data CodeSegment (I O : (Set -> Set)) : Set₁ where
f0759cb39d37 Trying define codesegment using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
35 cs : (DataSegment I -> DataSegment O) -> CodeSegment I O