Mercurial > hg > Papers > 2020 > soto-midterm

comparison src/AgdaPushPop.agda.replaced @ 1:73127e0ab57c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
(none)
author soto@cr.ie.u-ryukyu.ac.jp
date Tue, 08 Sep 2020 18:38:08 +0900
parents
children
comparison
equal deleted inserted replaced
0:b919985837a3 1:73127e0ab57c
1 pushSingleLinkedStack : Meta @$\rightarrow$@ 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 @$\rightarrow$@ Maybe A @$\rightarrow$@ SingleLinkedStack A
8 push s nothing = s
9 push s (just x) = record {top = just (cons x (top s))}
10
11 popSingleLinkedStack : Meta @$\rightarrow$@ 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 @$\rightarrow$@ Maybe A
17 elem record {stack = record { top = (just (cons x _)) }} = just x
18 elem record {stack = record { top = nothing }} = nothing
19 st : Meta @$\rightarrow$@ 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