Mercurial > hg > Papers > 2020 > ryokka-master

annotate paper/src/subtype.agda @ 2:c7acb9211784

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add code, figure. and paper fix content
author ryokka
date Mon, 27 Jan 2020 20:41:36 +0900
parents
children
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
2
c7acb9211784 add code, figure. and paper fix content
ryokka
parents:
diff changeset
1 open import Level
c7acb9211784 add code, figure. and paper fix content
ryokka
parents:
diff changeset
2 open import Relation.Binary.PropositionalEquality
c7acb9211784 add code, figure. and paper fix content
ryokka
parents:
diff changeset
3
c7acb9211784 add code, figure. and paper fix content
ryokka
parents:
diff changeset
4 module subtype {l : Level} (Context : Set l) where
c7acb9211784 add code, figure. and paper fix content
ryokka
parents:
diff changeset
5
c7acb9211784 add code, figure. and paper fix content
ryokka
parents:
diff changeset
6
c7acb9211784 add code, figure. and paper fix content
ryokka
parents:
diff changeset
7 record DataSegment {ll : Level} (A : Set ll) : Set (l ⊔ ll) where
c7acb9211784 add code, figure. and paper fix content
ryokka
parents:
diff changeset
8 field
c7acb9211784 add code, figure. and paper fix content
ryokka
parents:
diff changeset
9 get : Context -> A
c7acb9211784 add code, figure. and paper fix content
ryokka
parents:
diff changeset
10 set : Context -> A -> Context
c7acb9211784 add code, figure. and paper fix content
ryokka
parents:
diff changeset
11 open DataSegment
c7acb9211784 add code, figure. and paper fix content
ryokka
parents:
diff changeset
12
c7acb9211784 add code, figure. and paper fix content
ryokka
parents:
diff changeset
13 data CodeSegment {l1 l2 : Level} (A : Set l1) (B : Set l2) : Set (l ⊔ l1 ⊔ l2) where
c7acb9211784 add code, figure. and paper fix content
ryokka
parents:
diff changeset
14 cs : {{_ : DataSegment A}} {{_ : DataSegment B}} -> (A -> B) -> CodeSegment A B
c7acb9211784 add code, figure. and paper fix content
ryokka
parents:
diff changeset
15
c7acb9211784 add code, figure. and paper fix content
ryokka
parents:
diff changeset
16 goto : {l1 l2 : Level} {I : Set l1} {O : Set l2} -> CodeSegment I O -> I -> O
c7acb9211784 add code, figure. and paper fix content
ryokka
parents:
diff changeset
17 goto (cs b) i = b i
c7acb9211784 add code, figure. and paper fix content
ryokka
parents:
diff changeset
18
c7acb9211784 add code, figure. and paper fix content
ryokka
parents:
diff changeset
19 exec : {l1 l2 : Level} {I : Set l1} {O : Set l2} {{_ : DataSegment I}} {{_ : DataSegment O}}
c7acb9211784 add code, figure. and paper fix content
ryokka
parents:
diff changeset
20 -> CodeSegment I O -> Context -> Context
c7acb9211784 add code, figure. and paper fix content
ryokka
parents:
diff changeset
21 exec {l} {{i}} {{o}} (cs b) c = set o c (b (get i c))
c7acb9211784 add code, figure. and paper fix content
ryokka
parents:
diff changeset
22
c7acb9211784 add code, figure. and paper fix content
ryokka
parents:
diff changeset
23
c7acb9211784 add code, figure. and paper fix content
ryokka
parents:
diff changeset
24 comp : {con : Context} -> {l1 l2 l3 l4 : Level}
c7acb9211784 add code, figure. and paper fix content
ryokka
parents:
diff changeset
25 {A : Set l1} {B : Set l2} {C : Set l3} {D : Set l4}
c7acb9211784 add code, figure. and paper fix content
ryokka
parents:
diff changeset
26 {{_ : DataSegment A}} {{_ : DataSegment B}} {{_ : DataSegment C}} {{_ : DataSegment D}}
c7acb9211784 add code, figure. and paper fix content
ryokka
parents:
diff changeset
27 -> (C -> D) -> (A -> B) -> A -> D
c7acb9211784 add code, figure. and paper fix content
ryokka
parents:
diff changeset
28 comp {con} {{i}} {{io}} {{oi}} {{o}} g f x = g (get oi (set io con (f x)))
c7acb9211784 add code, figure. and paper fix content
ryokka
parents:
diff changeset
29
c7acb9211784 add code, figure. and paper fix content
ryokka
parents:
diff changeset
30 csComp : {con : Context} -> {l1 l2 l3 l4 : Level}
c7acb9211784 add code, figure. and paper fix content
ryokka
parents:
diff changeset
31 {A : Set l1} {B : Set l2} {C : Set l3} {D : Set l4}
c7acb9211784 add code, figure. and paper fix content
ryokka
parents:
diff changeset
32 {{_ : DataSegment A}} {{_ : DataSegment B}} {{_ : DataSegment C}} {{_ : DataSegment D}}
c7acb9211784 add code, figure. and paper fix content
ryokka
parents:
diff changeset
33 -> CodeSegment C D -> CodeSegment A B -> CodeSegment A D
c7acb9211784 add code, figure. and paper fix content
ryokka
parents:
diff changeset
34 csComp {con} {A} {B} {C} {D} {{da}} {{db}} {{dc}} {{dd}} (cs g) (cs f)
c7acb9211784 add code, figure. and paper fix content
ryokka
parents:
diff changeset
35 = cs {{da}} {{dd}} (comp {con} {{da}} {{db}} {{dc}} {{dd}} g f)
c7acb9211784 add code, figure. and paper fix content
ryokka
parents:
diff changeset
36
c7acb9211784 add code, figure. and paper fix content
ryokka
parents:
diff changeset
37
c7acb9211784 add code, figure. and paper fix content
ryokka
parents:
diff changeset
38
c7acb9211784 add code, figure. and paper fix content
ryokka
parents:
diff changeset
39 comp-associative : {A B C D E F : Set l} {con : Context}
c7acb9211784 add code, figure. and paper fix content
ryokka
parents:
diff changeset
40 {{da : DataSegment A}} {{db : DataSegment B}} {{dc : DataSegment C}}
c7acb9211784 add code, figure. and paper fix content
ryokka
parents:
diff changeset
41 {{dd : DataSegment D}} {{de : DataSegment E}} {{df : DataSegment F}}
c7acb9211784 add code, figure. and paper fix content
ryokka
parents:
diff changeset
42 -> (a : CodeSegment A B) (b : CodeSegment C D) (c : CodeSegment E F)
c7acb9211784 add code, figure. and paper fix content
ryokka
parents:
diff changeset
43 -> csComp {con} c (csComp {con} b a) ≡ csComp {con} (csComp {con} c b) a
c7acb9211784 add code, figure. and paper fix content
ryokka
parents:
diff changeset
44 comp-associative (cs _) (cs _) (cs _) = refl