Mercurial > hg > Members > Moririn

annotate src/parallel_execution/stack.agda @ 154:efef5d4df54f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add normal level and agda code
author atton
date Tue, 15 Nov 2016 19:02:36 +0900
parents
children 19cc626943e4
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
154
efef5d4df54f Add normal level and agda code
atton
parents:
diff changeset
1 module stack where
efef5d4df54f Add normal level and agda code
atton
parents:
diff changeset
2
efef5d4df54f Add normal level and agda code
atton
parents:
diff changeset
3 pushSingleLinkedStack : Stack -> Data -> (Code : Stack -> ?) -> ?
efef5d4df54f Add normal level and agda code
atton
parents:
diff changeset
4 pushSingleLinkedStack stack data next = next stack1
efef5d4df54f Add normal level and agda code
atton
parents:
diff changeset
5 where
efef5d4df54f Add normal level and agda code
atton
parents:
diff changeset
6 element = record {next = top stack; data = data}
efef5d4df54f Add normal level and agda code
atton
parents:
diff changeset
7 stack1 = record {top = just element}
efef5d4df54f Add normal level and agda code
atton
parents:
diff changeset
8
efef5d4df54f Add normal level and agda code
atton
parents:
diff changeset
9
efef5d4df54f Add normal level and agda code
atton
parents:
diff changeset
10 popSingleLinkedStack : Maybe ?? -> Data -> (Code : Stack -> (Maybe ??) -> ?) -> ?
efef5d4df54f Add normal level and agda code
atton
parents:
diff changeset
11 popSingleLinkedStack stack data next with (top stack) =
efef5d4df54f Add normal level and agda code
atton
parents:
diff changeset
12 ... | nothing = next stack nothing
efef5d4df54f Add normal level and agda code
atton
parents:
diff changeset
13 ... | just a = next stack1 data1
efef5d4df54f Add normal level and agda code
atton
parents:
diff changeset
14 where
efef5d4df54f Add normal level and agda code
atton
parents:
diff changeset
15 data1 = data a
efef5d4df54f Add normal level and agda code
atton
parents:
diff changeset
16 stack1 = record { top = (next a)}