Mercurial > hg > Papers > 2018 > ryokka-thesis

comparison final_main/src/stackImpl.agda @ 5:eafc166804f3

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix Capter4.2,5,1
author ryokka
date Mon, 19 Feb 2018 18:44:59 +0900
parents
children
comparison
equal deleted inserted replaced
4:12204a2c2eda 5:eafc166804f3
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 }