|
72
|
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
|
