Mercurial > hg > Members > atton > agda-proofs

annotate cbc/stack-subtype.agda @ 54:fa95e3070138

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Define SingleLinkedStack using subtype
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Wed, 11 Jan 2017 10:56:13 +0000
parents 6af88ee5c4ca
children 81c6779583b6
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
54
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
1 open import Level hiding (lift)
52
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
2 open import Data.Maybe
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 open import Data.Product
54
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
4 open import Data.Nat hiding (suc)
52
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
5
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
6 module stack-subtype (A : Set) where
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
7
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
8 -- data definitions
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
9
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 data Element (a : Set) : Set where
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 cons : a -> Maybe (Element a) -> Element a
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
12
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 datum : {a : Set} -> Element a -> a
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 datum (cons a _) = a
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
15
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 next : {a : Set} -> Element a -> Maybe (Element a)
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
17 next (cons _ n) = n
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
18
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
19 record SingleLinkedStack (a : Set) : Set where
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
20 field
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
21 top : Maybe (Element a)
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
22 open SingleLinkedStack
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
23
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
24 record Context : Set where
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
25 field
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
26 element : Maybe A
54
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
27 n : ℕ
52
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
28
54
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
29
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
30 open import subtype Context as N
52
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
31
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
32 instance
54
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
33 ContextIsDataSegment : N.DataSegment Context
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
34 ContextIsDataSegment = record {get = (\c -> c) ; set = (\_ c -> c)}
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
35
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
36
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
37 record MetaContext (X : Set) {{_ : N.DataSegment X}} : Set₁ where
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
38 field
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
39 context : Context
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
40 stack : SingleLinkedStack A
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
41 nextCS : N.CodeSegment X X
52
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
42
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
43
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
44
54
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
45
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
46 open import subtype (MetaContext Context) as M
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
47
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
48 instance
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
49 MetaContextIncludeContext : M.DataSegment Context
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
50 MetaContextIncludeContext = record { get = MetaContext.context
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
51 ; set = (\m c -> record m {context = c}) }
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
52
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
53 MetaContextIsMetaDataSegment : M.DataSegment (MetaContext Context)
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
54 MetaContextIsMetaDataSegment = record { get = (\m -> m) ; set = (\_ m -> m) }
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
55
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
56
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
57 liftMeta : {X Y : Set} {{_ : M.DataSegment X}} {{_ : M.DataSegment Y}} -> N.CodeSegment X Y -> M.CodeSegment X Y
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
58 liftMeta (N.cs f) = M.cs f
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
59
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
60 liftContext : {X Y : Set} {{_ : N.DataSegment X}} {{_ : N.DataSegment Y}} -> N.CodeSegment X Y -> N.CodeSegment Context Context
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
61 liftContext {{x}} {{y}} (N.cs f) = N.cs (\c -> N.DataSegment.set y c (f (N.DataSegment.get x c)))
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
62
52
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
63 -- definition based from Gears(209:5708390a9d88) src/parallel_execution
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
64
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
65 emptySingleLinkedStack : SingleLinkedStack A
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
66 emptySingleLinkedStack = record {top = nothing}
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
67
54
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
68
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
69 pushSingleLinkedStack : MetaContext Context -> MetaContext Context
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
70 pushSingleLinkedStack m = M.exec (liftMeta n) (record m {stack = (push s e) })
52
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
71 where
54
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
72 n = MetaContext.nextCS m
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
73 e = Context.element (MetaContext.context m)
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
74 s = MetaContext.stack m
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
75 push : SingleLinkedStack A -> Maybe A -> SingleLinkedStack A
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
76 push s nothing = s
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
77 push s (just x) = record {top = just (cons x (top s))}
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
78
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
79
52
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
80
54
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
81 popSingleLinkedStack : MetaContext Context -> MetaContext Context
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
82 popSingleLinkedStack m = M.exec (liftMeta n) (record m {stack = (st m) ; context = record con {element = (elem m)}})
52
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
83 where
54
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
84 n = MetaContext.nextCS m
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
85 con = MetaContext.context m
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
86 elem : MetaContext Context -> Maybe A
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
87 elem record {stack = record { top = (just (cons x _)) }} = just x
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
88 elem record {stack = record { top = nothing }} = nothing
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
89 st : MetaContext Context -> SingleLinkedStack A
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
90 st record {stack = record { top = (just (cons _ s)) }} = record {top = s}
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
91 st record {stack = record { top = nothing }} = record {top = nothing}
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
92
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
93 pushSingleLinkedStackCS : M.CodeSegment (MetaContext Context) (MetaContext Context)
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
94 pushSingleLinkedStackCS = M.cs pushSingleLinkedStack
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
95
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
96 popSingleLinkedStackCS : M.CodeSegment (MetaContext Context) (MetaContext Context)
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
97 popSingleLinkedStackCS = M.cs popSingleLinkedStack
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
98
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
99
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
100
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
101
52
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
102
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
103 -- sample
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
104
54
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
105 record Num : Set where
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
106 field
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
107 num : ℕ
52
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
108
54
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
109 instance
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
110 NumIsNormalDataSegment : N.DataSegment Num
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
111 NumIsNormalDataSegment = record { get = (\c -> record { num = Context.n c})
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
112 ; set = (\c n -> record c {n = Num.num n})}
52
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
113
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
114
54
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
115 plus3 : Num -> Num
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
116 plus3 record { num = n } = record {num = n + 3}
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
117
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
118 plus3CS : N.CodeSegment Num Num
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
119 plus3CS = N.cs plus3
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
120
52
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
121
54
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
122 setNext : {X Y : Set} {{x : N.DataSegment X}} {{y : N.DataSegment Y}}
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
123 -> (N.CodeSegment X Y) -> M.CodeSegment (MetaContext Context) (MetaContext Context)
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
124 setNext c = M.cs (\mc -> record mc {nextCS = liftContext c})
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
125
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
126
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
127
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
128
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
129
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
130 pushPlus3CS : {mc : MetaContext Context} -> M.CodeSegment (MetaContext Context) (MetaContext Context)
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
131 pushPlus3CS {mc} = M.csComp {mc} pushSingleLinkedStackCS (setNext plus3CS)