Mercurial > hg > Papers > 2018 > nozomi-master

comparison paper/src/subtype.agda @ 72:fd984cfd5425

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add sources
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Mon, 06 Feb 2017 10:32:49 +0900
parents
children
comparison
equal deleted inserted replaced
71:b0cfef1cd89f 72:fd984cfd5425
1 open import Level
2 open import Relation.Binary.PropositionalEquality
3
4 module subtype {l : Level} (Context : Set l) where
5
6
7 record DataSegment {ll : Level} (A : Set ll) : Set (l ⊔ ll) where
8 field
9 get : Context -> A
10 set : Context -> A -> Context
11 open DataSegment
12
13 data CodeSegment {l1 l2 : Level} (A : Set l1) (B : Set l2) : Set (l ⊔ l1 ⊔ l2) where
14 cs : {{_ : DataSegment A}} {{_ : DataSegment B}} -> (A -> B) -> CodeSegment A B
15
16 goto : {l1 l2 : Level} {I : Set l1} {O : Set l2} -> CodeSegment I O -> I -> O
17 goto (cs b) i = b i
18
19 exec : {l1 l2 : Level} {I : Set l1} {O : Set l2} {{_ : DataSegment I}} {{_ : DataSegment O}}
20 -> CodeSegment I O -> Context -> Context
21 exec {l} {{i}} {{o}} (cs b) c = set o c (b (get i c))
22
23
24 comp : {con : Context} -> {l1 l2 l3 l4 : Level}
25 {A : Set l1} {B : Set l2} {C : Set l3} {D : Set l4}
26 {{_ : DataSegment A}} {{_ : DataSegment B}} {{_ : DataSegment C}} {{_ : DataSegment D}}
27 -> (C -> D) -> (A -> B) -> A -> D
28 comp {con} {{i}} {{io}} {{oi}} {{o}} g f x = g (get oi (set io con (f x)))
29
30 csComp : {con : Context} -> {l1 l2 l3 l4 : Level}
31 {A : Set l1} {B : Set l2} {C : Set l3} {D : Set l4}
32 {{_ : DataSegment A}} {{_ : DataSegment B}} {{_ : DataSegment C}} {{_ : DataSegment D}}
33 -> CodeSegment C D -> CodeSegment A B -> CodeSegment A D
34 csComp {con} {A} {B} {C} {D} {{da}} {{db}} {{dc}} {{dd}} (cs g) (cs f)
35 = cs {{da}} {{dd}} (comp {con} {{da}} {{db}} {{dc}} {{dd}} g f)
36
37
38
39 comp-associative : {A B C D E F : Set l} {con : Context}
40 {{da : DataSegment A}} {{db : DataSegment B}} {{dc : DataSegment C}}
41 {{dd : DataSegment D}} {{de : DataSegment E}} {{df : DataSegment F}}
42 -> (a : CodeSegment A B) (b : CodeSegment C D) (c : CodeSegment E F)
43 -> csComp {con} c (csComp {con} b a) ≡ csComp {con} (csComp {con} c b) a
44 comp-associative (cs _) (cs _) (cs _) = refl