Mercurial > hg > Members > atton > agda-proofs
changeset 61:7af6c894f411
Trying define n-push
author | atton <atton@cr.ie.u-ryukyu.ac.jp> |
---|---|
date | Sat, 14 Jan 2017 02:10:28 +0000 |
parents | bd428bd6b394 |
children | 29b069a0c409 |
files | cbc/stack-subtype-sample.agda cbc/stack-subtype.agda |
diffstat | 2 files changed, 73 insertions(+), 33 deletions(-) [+] |
line wrap: on
line diff
--- a/cbc/stack-subtype-sample.agda Sat Jan 14 00:00:40 2017 +0000 +++ b/cbc/stack-subtype-sample.agda Sat Jan 14 02:10:28 2017 +0000 @@ -1,12 +1,13 @@ module stack-subtype-sample where +open import Function open import Data.Nat open import Data.Maybe open import Relation.Binary.PropositionalEquality open import stack-subtype ℕ as S -open import subtype Context as N -open import subtype (Meta Context) as M +open import subtype Context as N +open import subtype Meta as M record Num : Set where @@ -29,17 +30,9 @@ plus3CS = N.cs plus3 -setNext : {X Y : Set} {{x : N.DataSegment X}} {{y : N.DataSegment Y}} - -> (N.CodeSegment X Y) -> M.CodeSegment (Meta Context) (Meta Context) -setNext c = M.cs (\mc -> record mc {nextCS = liftContext c}) -setElement : ℕ -> M.CodeSegment (Meta Context) (Meta Context) -setElement x = M.cs (\mc -> record mc {context = record (Meta.context mc) {element = just x}}) - - - -plus5AndPushWithPlus3 : {mc : Meta Context} {{_ : N.DataSegment Num}} - -> M.CodeSegment Num (Meta Context) +plus5AndPushWithPlus3 : {mc : Meta} {{_ : N.DataSegment Num}} + -> M.CodeSegment Num (Meta) plus5AndPushWithPlus3 {mc} {{nn}} = M.cs (\n -> record {context = con n ; nextCS = (liftContext {{nn}} {{nn}} plus3CS) ; stack = st} ) where co = Meta.context mc @@ -50,7 +43,7 @@ -push-sample : {{_ : N.DataSegment Num}} {{_ : M.DataSegment Num}} -> Meta Context +push-sample : {{_ : N.DataSegment Num}} {{_ : M.DataSegment Num}} -> Meta push-sample {{nd}} {{md}} = M.exec {{md}} (plus5AndPushWithPlus3 {mc} {{nd}}) mc where con = record { n = 4 ; element = just 0} @@ -64,7 +57,7 @@ push-sample-equiv = refl -pushed-sample : {m : Meta Context} {{_ : N.DataSegment Num}} {{_ : M.DataSegment Num}} -> Meta Context +pushed-sample : {m : Meta} {{_ : N.DataSegment Num}} {{_ : M.DataSegment Num}} -> Meta pushed-sample {m} {{nd}} {{md}} = M.exec {{md}} (M.csComp {m} {{md}} pushSingleLinkedStackCS (plus5AndPushWithPlus3 {mc} {{nd}})) mc where con = record { n = 4 ; element = just 0} @@ -73,7 +66,7 @@ -pushed-sample-equiv : {m : Meta Context} -> +pushed-sample-equiv : {m : Meta} -> pushed-sample {m} ≡ record { nextCS = liftContext plus3CS ; stack = record { top = just (cons 0 nothing) } ; context = record { n = 12} } @@ -81,6 +74,41 @@ -n-push : {{_ : M.DataSegment (Meta Context)}} -> Meta Context -> Meta Context -n-push m = M.csComp (pushSingleLinkedStackCS) (setElement ?) +pushNum : N.CodeSegment Context Context +pushNum = N.cs pn + where + pn : Context -> Context + pn record { n = n } = record { n = n ; element = just n} + +n-push : {{_ : N.DataSegment Num}} -> Meta -> Meta +n-push {{x}} record { context = record { n = zero ; element = el } ; stack = st ; nextCS = code} = + M.exec pushSingleLinkedStackCS record { context = record { n = zero ; element = el } + ; stack = st ; nextCS = code} +n-push {{x}} record { context = record { n = (suc n) ; element = el } ; stack = st ; nextCS = code} = + n-push {{x}} record {context = record {n = n ; element = e} ; stack = s ; nextCS = c} + where + pushedMeta = M.exec pushSingleLinkedStackCS record { context = record { n = (suc n) ; element = el} + ; stack = st ; nextCS = code} + e = Context.element (Meta.context pushedMeta) + s = Meta.stack pushedMeta + c = Meta.nextCS pushedMeta + + +n-push-cs : M.CodeSegment Meta Meta +n-push-cs = M.cs n-push + + +initMeta : ℕ -> N.CodeSegment Context Context -> Meta +initMeta n code = record { context = record { n = n ; element = nothing} + ; stack = emptySingleLinkedStack + ; nextCS = code + } + +n-push-cs-exec = M.exec n-push-cs (initMeta 4 pushNum) + + +n-push-cs-exec-equiv : n-push-cs-exec ≡ record { nextCS = {!!} + ; context = {!!} + ; stack = record { top = {!!} }} +n-push-cs-exec-equiv = refl
--- a/cbc/stack-subtype.agda Sat Jan 14 00:00:40 2017 +0000 +++ b/cbc/stack-subtype.agda Sat Jan 14 02:10:28 2017 +0000 @@ -2,6 +2,7 @@ open import Data.Maybe open import Data.Product open import Data.Nat hiding (suc) +open import Function module stack-subtype (A : Set) where @@ -23,11 +24,12 @@ record Context : Set where field + -- fields for concrete data segments + n : ℕ -- fields for stack element : Maybe A - stack : SingleLinkedStack A - -- fields for data segments - n : ℕ + + @@ -40,8 +42,11 @@ record Meta : Set₁ where field + -- context as set of data segments context : Context + stack : SingleLinkedStack A nextCS : N.CodeSegment Context Context + @@ -69,28 +74,30 @@ pushSingleLinkedStack : Meta -> Meta -pushSingleLinkedStack m = M.exec (liftMeta n) (record m {context = record c {stack = (push s e)}}) +pushSingleLinkedStack m = M.exec (liftMeta n) (record m {stack = (push s e) }) where - c = (Meta.context m) - n = Meta.nextCS m - e = Context.element c - s = Context.stack c + n = Meta.nextCS m + s = Meta.stack m + e = Context.element (Meta.context m) push : SingleLinkedStack A -> Maybe A -> SingleLinkedStack A push s nothing = s push s (just x) = record {top = just (cons x (top s))} + popSingleLinkedStack : Meta -> Meta -popSingleLinkedStack m = M.exec (liftMeta n) (record m { context = record c { stack = (st c) ; element = (elem c)}}) +popSingleLinkedStack m = M.exec (liftMeta n) (record m {stack = (st m) ; context = record con {element = (elem m)}}) where n = Meta.nextCS m - c = Meta.context m - elem : Context -> Maybe A + con = Meta.context m + elem : Meta -> Maybe A elem record {stack = record { top = (just (cons x _)) }} = just x - elem record {stack = record { top = nothing } } = nothing - st : Context -> SingleLinkedStack A + elem record {stack = record { top = nothing }} = nothing + st : Meta -> SingleLinkedStack A st record {stack = record { top = (just (cons _ s)) }} = record {top = s} - st record {stack = record { top = nothing } } = record {top = nothing} + st record {stack = record { top = nothing }} = record {top = nothing} + + pushSingleLinkedStackCS : M.CodeSegment Meta Meta @@ -103,9 +110,14 @@ -- for sample firstContext : Context -firstContext = record {stack = emptySingleLinkedStack ; element = nothing ; n = 0} +firstContext = record {element = nothing ; n = 0} firstMeta : Meta -firstMeta = record {nextCS = (N.cs (\m -> m)) ; context = firstContext} +firstMeta = record { context = firstContext + ; stack = emptySingleLinkedStack + ; nextCS = (N.cs (\m -> m)) + } + +