Mercurial > hg > Papers > 2020 > ryokka-master

comparison paper/src/stackImpl.agda @ 2:c7acb9211784

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add code, figure. and paper fix content
author ryokka
date Mon, 27 Jan 2020 20:41:36 +0900
parents
children
comparison
equal deleted inserted replaced
1:ee44dbda6bd3 2:c7acb9211784
1 record Element {l : Level} (a : Set l) : Set l where
2 inductive
3 constructor cons
4 field
5 datum : a -- `data` is reserved by Agda.
6 next : Maybe (Element a)
7 open Element
8
9 record SingleLinkedStack {n : Level } (a : Set n) : Set n where
10 field
11 top : Maybe (Element a)
12 open SingleLinkedStack
13
14 pushSingleLinkedStack : {n m : Level } {t : Set m } {Data : Set n} -> SingleLinkedStack Data -> Data -> (Code : SingleLinkedStack Data -> t) -> t
15 pushSingleLinkedStack stack datum next = next stack1
16 where
17 element = cons datum (top stack)
18 stack1 = record {top = Just element}
19
20 -- push 以下は省略
21
22 -- Basic stack implementations are specifications of a Stack
23
24 singleLinkedStackSpec : {n m : Level } {t : Set m } {a : Set n} -> StackMethods {n} {m} a {t} (SingleLinkedStack a)
25 singleLinkedStackSpec = record {
26 push = pushSingleLinkedStack
27 ; pop = popSingleLinkedStack
28 ; pop2 = pop2SingleLinkedStack
29 ; get = getSingleLinkedStack
30 ; get2 = get2SingleLinkedStack
31 ; clear = clearSingleLinkedStack
32 }
33
34 createSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> Stack {n} {m} a {t} (SingleLinkedStack a)
35 createSingleLinkedStack = record {
36 stack = emptySingleLinkedStack ;
37 stackMethods = singleLinkedStackSpec
38 }