Mercurial > hg > Members > atton > agda-proofs
changeset 55:81c6779583b6
Add push-sample
| author | atton <atton@cr.ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 11 Jan 2017 13:37:23 +0000 |
| parents | fa95e3070138 |
| children | ddcd652969e0 |
| files | cbc/stack-subtype.agda cbc/subtype.agda |
| diffstat | 2 files changed, 19 insertions(+), 4 deletions(-) [+] |
line wrap: on
line diff
--- a/cbc/stack-subtype.agda Wed Jan 11 10:56:13 2017 +0000 +++ b/cbc/stack-subtype.agda Wed Jan 11 13:37:23 2017 +0000 @@ -123,9 +123,23 @@ -> (N.CodeSegment X Y) -> M.CodeSegment (MetaContext Context) (MetaContext Context) setNext c = M.cs (\mc -> record mc {nextCS = liftContext c}) - - - +setElement : A -> M.CodeSegment (MetaContext Context) (MetaContext Context) +setElement x = M.cs (\mc -> record mc {context = record (MetaContext.context mc) {element = just x}}) pushPlus3CS : {mc : MetaContext Context} -> M.CodeSegment (MetaContext Context) (MetaContext Context) pushPlus3CS {mc} = M.csComp {mc} pushSingleLinkedStackCS (setNext plus3CS) + +plus5AndPush : {mc : MetaContext Context} {{_ : N.DataSegment Num}} {{_ : M.DataSegment Num}} + -> M.CodeSegment Num (MetaContext Context) +plus5AndPush {mc} {{nn}} = M.cs (\n -> record {context = con ; nextCS = (liftContext {{nn}} {{nn}} plus3CS) ; stack = st} ) + where + con = MetaContext.context mc + st = MetaContext.stack mc + + +push-sample : {{_ : M.DataSegment Num}} -> MetaContext Context +push-sample = M.exec (plus5AndPush {mc}) mc + where + con = record { n = 4 ; element = nothing} + code = N.cs (\c -> c) + mc = record {context = con ; stack = emptySingleLinkedStack ; nextCS = code}
--- a/cbc/subtype.agda Wed Jan 11 10:56:13 2017 +0000 +++ b/cbc/subtype.agda Wed Jan 11 13:37:23 2017 +0000 @@ -14,7 +14,8 @@ cs : {{_ : DataSegment A}} {{_ : DataSegment B}} -> (A -> B) -> CodeSegment A B -exec : {I O : Set} {{_ : DataSegment I}} {{_ : DataSegment O}} -> CodeSegment I O -> Context -> Context +exec : {l1 l2 : Level} {I : Set l1} {O : Set l2} {{_ : DataSegment I}} {{_ : DataSegment O}} + -> CodeSegment I O -> Context -> Context exec {l} {{i}} {{o}} (cs b) c = set o c (b (get i c))