|
1
|
1 pushSingleLinkedStack : Meta -> Meta
|
|
|
2 pushSingleLinkedStack m = M.exec (liftMeta n) (record m {stack = (push s e) })
|
|
|
3 where
|
|
|
4 n = Meta.nextCS m
|
|
|
5 s = Meta.stack m
|
|
|
6 e = Context.element (Meta.context m)
|
|
|
7 push : SingleLinkedStack A -> Maybe A -> SingleLinkedStack A
|
|
|
8 push s nothing = s
|
|
|
9 push s (just x) = record {top = just (cons x (top s))}
|
|
|
10
|
|
|
11 popSingleLinkedStack : Meta -> Meta
|
|
|
12 popSingleLinkedStack m = M.exec (liftMeta n) (record m {stack = (st m) ; context = record con {element = (elem m)}})
|
|
|
13 where
|
|
|
14 n = Meta.nextCS m
|
|
|
15 con = Meta.context m
|
|
|
16 elem : Meta -> Maybe A
|
|
|
17 elem record {stack = record { top = (just (cons x _)) }} = just x
|
|
|
18 elem record {stack = record { top = nothing }} = nothing
|
|
|
19 st : Meta -> SingleLinkedStack A
|
|
|
20 st record {stack = record { top = (just (cons _ s)) }} = record {top = s}
|
|
|
21 st record {stack = record { top = nothing }} = record {top = nothing}
|
|
|
22
|
|
|
23
|
|
|
24 pushSingleLinkedStackCS : M.CodeSegment Meta Meta
|
|
|
25 pushSingleLinkedStackCS = M.cs pushSingleLinkedStack
|
|
|
26
|
|
|
27 popSingleLinkedStackCS : M.CodeSegment Meta Meta
|
|
|
28 popSingleLinkedStackCS = M.cs popSingleLinkedStack
|
