Mercurial > hg > Members > atton > agda-proofs
diff cbc/subtype.agda @ 52:4880184e4ab5
Define push/pop using subtype
author | atton <atton@cr.ie.u-ryukyu.ac.jp> |
---|---|
date | Tue, 10 Jan 2017 09:04:55 +0000 |
parents | 16e27df74ec5 |
children | 6af88ee5c4ca |
line wrap: on
line diff
--- a/cbc/subtype.agda Tue Jan 10 02:04:55 2017 +0000 +++ b/cbc/subtype.agda Tue Jan 10 09:04:55 2017 +0000 @@ -1,27 +1,28 @@ -module subtype (Context : Set) where - +open import Level open import Relation.Binary.PropositionalEquality +module subtype {l : Level} (Context : Set l) where -record DataSegment (A : Set) : Set where + +record DataSegment {ll : Level} (A : Set ll) : Set (l ⊔ ll) where field get : Context -> A set : Context -> A -> Context open DataSegment -data CodeSegment (A B : Set) : Set where +data CodeSegment {ll : Level} (A B : Set ll) : Set (l ⊔ ll) where cs : {{_ : DataSegment A}} {{_ : DataSegment B}} -> (A -> B) -> CodeSegment A B -exec : {I O : Set} {{_ : DataSegment I}} {{_ : DataSegment O}} -> CodeSegment I O -> Context -> Context -exec {l} {{i}} {{o}} (cs b) c = DataSegment.set o c (b (get i c)) +exec : {I O : Set l} {{_ : DataSegment I}} {{_ : DataSegment O}} -> CodeSegment I O -> Context -> Context +exec {l} {{i}} {{o}} (cs b) c = set o c (b (get i c)) -comp : {con : Context} -> {A B C D : Set} {{_ : DataSegment A}} {{_ : DataSegment B}} {{_ : DataSegment C}} {{_ : DataSegment D}} +comp : {con : Context} -> {A B C D : Set l} {{_ : DataSegment A}} {{_ : DataSegment B}} {{_ : DataSegment C}} {{_ : DataSegment D}} -> (C -> D) -> (A -> B) -> A -> D comp {con} {{i}} {{io}} {{oi}} {{o}} g f x = g (get oi (set io con (f x))) -csComp : {con : Context} {A B C D : Set} +csComp : {con : Context} {A B C D : Set l} {{_ : DataSegment A}} {{_ : DataSegment B}} {{_ : DataSegment C}} {{_ : DataSegment D}} -> CodeSegment C D -> CodeSegment A B -> CodeSegment A D csComp {con} {A} {B} {C} {D} {{da}} {{db}} {{dc}} {{dd}} (cs g) (cs f) @@ -29,7 +30,7 @@ -comp-associative : {A B C D E F : Set} {con : Context} +comp-associative : {A B C D E F : Set l} {con : Context} {{da : DataSegment A}} {{db : DataSegment B}} {{dc : DataSegment C}} {{dd : DataSegment D}} {{de : DataSegment E}} {{df : DataSegment F}} -> (a : CodeSegment A B) (b : CodeSegment C D) (c : CodeSegment E F)