Mercurial > hg > Papers > 2019 > oshiro-thesis
diff final_main/src/AgdaPushPop.agda @ 0:83f997abf3b5
first commit
author | e155702 |
---|---|
date | Thu, 14 Feb 2019 16:51:50 +0900 |
parents | |
children |
line wrap: on
line diff
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_main/src/AgdaPushPop.agda Thu Feb 14 16:51:50 2019 +0900 @@ -0,0 +1,28 @@ +pushSingleLinkedStack : Meta -> Meta +pushSingleLinkedStack m = M.exec (liftMeta n) (record m {stack = (push s e) }) + where + 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 {stack = (st m) ; context = record con {element = (elem m)}}) + where + n = Meta.nextCS m + 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 : Meta -> 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 Meta Meta +pushSingleLinkedStackCS = M.cs pushSingleLinkedStack + +popSingleLinkedStackCS : M.CodeSegment Meta Meta +popSingleLinkedStackCS = M.cs popSingleLinkedStack