Mercurial > hg > Members > atton > agda-proofs

comparison cbc/subtype.agda @ 54:fa95e3070138

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