Mercurial > hg > Members > atton > agda-proofs
changeset 54:fa95e3070138
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 |
| files | cbc/stack-product.agda cbc/stack-subtype.agda cbc/subtype.agda |
| diffstat | 3 files changed, 96 insertions(+), 38 deletions(-) [+] |
line wrap: on
line diff
--- a/cbc/stack-product.agda Tue Jan 10 09:07:07 2017 +0000 +++ b/cbc/stack-product.agda Wed Jan 11 10:56:13 2017 +0000 @@ -108,7 +108,7 @@ where push : {A : Set} {a : A} -> (ℕ × SingleLinkedStack A) -> (ℕ × SingleLinkedStack A) push {A} {a} (zero , s) = (zero , s) - push {A} {a} (suc n , s) = goto pushSingleLinkedStack (s , a , {!!} {- n-push -}) -- needs subtype + push {A} {a} (suc n , s) = goto pushSingleLinkedStack (s , a , ? {- n-push -}) -- needs subtype {-
--- a/cbc/stack-subtype.agda Tue Jan 10 09:07:07 2017 +0000 +++ b/cbc/stack-subtype.agda Wed Jan 11 10:56:13 2017 +0000 @@ -1,7 +1,7 @@ -open import Level +open import Level hiding (lift) open import Data.Maybe open import Data.Product -open import Data.Nat +open import Data.Nat hiding (suc) module stack-subtype (A : Set) where @@ -23,54 +23,109 @@ record Context : Set where field - stack : SingleLinkedStack A element : Maybe A - n : ℕ + n : ℕ -open import subtype Context + +open import subtype Context as N instance - ContextIsDataSegment : DataSegment Context - ContextIsDataSegment = record {get = (\x -> x) ; set = (\_ c -> c)} + ContextIsDataSegment : N.DataSegment Context + ContextIsDataSegment = record {get = (\c -> c) ; set = (\_ c -> c)} + + +record MetaContext (X : Set) {{_ : N.DataSegment X}} : Set₁ where + field + context : Context + stack : SingleLinkedStack A + nextCS : N.CodeSegment X X + +open import subtype (MetaContext Context) as M + +instance + MetaContextIncludeContext : M.DataSegment Context + MetaContextIncludeContext = record { get = MetaContext.context + ; set = (\m c -> record m {context = c}) } + + MetaContextIsMetaDataSegment : M.DataSegment (MetaContext Context) + MetaContextIsMetaDataSegment = record { get = (\m -> m) ; set = (\_ m -> m) } + + +liftMeta : {X Y : Set} {{_ : M.DataSegment X}} {{_ : M.DataSegment Y}} -> N.CodeSegment X Y -> M.CodeSegment X Y +liftMeta (N.cs f) = M.cs f + +liftContext : {X Y : Set} {{_ : N.DataSegment X}} {{_ : N.DataSegment Y}} -> N.CodeSegment X Y -> N.CodeSegment Context Context +liftContext {{x}} {{y}} (N.cs f) = N.cs (\c -> N.DataSegment.set y c (f (N.DataSegment.get x c))) + -- definition based from Gears(209:5708390a9d88) src/parallel_execution emptySingleLinkedStack : SingleLinkedStack A emptySingleLinkedStack = record {top = nothing} -pushSingleLinkedStack : Context -> Context -pushSingleLinkedStack c = record c { stack = (push c) ; element = nothing} + +pushSingleLinkedStack : MetaContext Context -> MetaContext Context +pushSingleLinkedStack m = M.exec (liftMeta n) (record m {stack = (push s e) }) where - push : Context -> SingleLinkedStack A - push record { stack = stack ; element = nothing } = stack - push record { stack = stack ; element = (just x) } = stack1 - where - el = cons x (top stack) - stack1 = record {top = just el} + n = MetaContext.nextCS m + e = Context.element (MetaContext.context m) + s = MetaContext.stack m + push : SingleLinkedStack A -> Maybe A -> SingleLinkedStack A + push s nothing = s + push s (just x) = record {top = just (cons x (top s))} + + -popSingleLinkedStack : Context -> Context -popSingleLinkedStack c = record c {element = (elem c) ; stack = (popdStack c)} +popSingleLinkedStack : MetaContext Context -> MetaContext Context +popSingleLinkedStack m = M.exec (liftMeta n) (record m {stack = (st m) ; context = record con {element = (elem m)}}) where - elem : Context -> Maybe A - elem record { stack = record { top = (just (cons x _)) } } = just x - elem record { stack = record { top = nothing } } = nothing - popdStack : Context -> SingleLinkedStack A - popdStack record { stack = record { top = (just (cons _ s)) } } = record { top = s } - popdStack record { stack = record { top = nothing } } = record { top = nothing } + n = MetaContext.nextCS m + con = MetaContext.context m + elem : MetaContext Context -> Maybe A + elem record {stack = record { top = (just (cons x _)) }} = just x + elem record {stack = record { top = nothing }} = nothing + st : MetaContext Context -> SingleLinkedStack A + st record {stack = record { top = (just (cons _ s)) }} = record {top = s} + st record {stack = record { top = nothing }} = record {top = nothing} + +pushSingleLinkedStackCS : M.CodeSegment (MetaContext Context) (MetaContext Context) +pushSingleLinkedStackCS = M.cs pushSingleLinkedStack + +popSingleLinkedStackCS : M.CodeSegment (MetaContext Context) (MetaContext Context) +popSingleLinkedStackCS = M.cs popSingleLinkedStack + + + + -- sample +record Num : Set where + field + num : ℕ -pushCS = cs pushSingleLinkedStack -popCS = cs popSingleLinkedStack +instance + NumIsNormalDataSegment : N.DataSegment Num + NumIsNormalDataSegment = record { get = (\c -> record { num = Context.n c}) + ; set = (\c n -> record c {n = Num.num n})} --- stack -record Stack {X Y : Set} (stackImpl : Set -> Set) : Set where - field - stack : stackImpl A - push : {{_ : DataSegment X}} {{_ : DataSegment Y}} -> CodeSegment X Y - pop : {{_ : DataSegment X}} {{_ : DataSegment Y}} -> CodeSegment X Y +plus3 : Num -> Num +plus3 record { num = n } = record {num = n + 3} + +plus3CS : N.CodeSegment Num Num +plus3CS = N.cs plus3 + +setNext : {X Y : Set} {{x : N.DataSegment X}} {{y : N.DataSegment Y}} + -> (N.CodeSegment X Y) -> M.CodeSegment (MetaContext Context) (MetaContext Context) +setNext c = M.cs (\mc -> record mc {nextCS = liftContext c}) + + + + + +pushPlus3CS : {mc : MetaContext Context} -> M.CodeSegment (MetaContext Context) (MetaContext Context) +pushPlus3CS {mc} = M.csComp {mc} pushSingleLinkedStackCS (setNext plus3CS)
--- a/cbc/subtype.agda Tue Jan 10 09:07:07 2017 +0000 +++ b/cbc/subtype.agda Wed Jan 11 10:56:13 2017 +0000 @@ -1,16 +1,16 @@ open import Level open import Relation.Binary.PropositionalEquality -module subtype (Context : Set) where +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 {l1 l2 : Level} (A : Set l1) (B : Set l2) : Set (l ⊔ l1 ⊔ l2) where cs : {{_ : DataSegment A}} {{_ : DataSegment B}} -> (A -> B) -> CodeSegment A B @@ -18,11 +18,14 @@ 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} -> {l1 l2 l3 l4 : Level} + {A : Set l1} {B : Set l2} {C : Set l3} {D : Set l4} + {{_ : 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} -> {l1 l2 l3 l4 : Level} + {A : Set l1} {B : Set l2} {C : Set l3} {D : Set l4} {{_ : 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) @@ -30,7 +33,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)