annotate Paper/src/AgdaStackImpl.agda.replaced @ 3:576637483425

fix section, source code,etc
author ryokka
date Thu, 19 Apr 2018 20:28:12 +0900
parents bf2887cd22c1
children
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
1
bf2887cd22c1 fix Paper
ryokka
parents:
diff changeset
1 record SingleLinkedStack {n : Level } (a : Set n) : Set n where
bf2887cd22c1 fix Paper
ryokka
parents:
diff changeset
2 field
bf2887cd22c1 fix Paper
ryokka
parents:
diff changeset
3 top : Maybe (Element a)
bf2887cd22c1 fix Paper
ryokka
parents:
diff changeset
4 open SingleLinkedStack
bf2887cd22c1 fix Paper
ryokka
parents:
diff changeset
5
3
576637483425 fix section, source code,etc
ryokka
parents: 1
diff changeset
6 pushSingleLinkedStack : {n m : Level } {t : Set m } {Data : Set n} @$\rightarrow$@ SingleLinkedStack Data @$\rightarrow$@ Data @$\rightarrow$@ (Code : SingleLinkedStack Data @$\rightarrow$@ t) @$\rightarrow$@ t
1
bf2887cd22c1 fix Paper
ryokka
parents:
diff changeset
7 pushSingleLinkedStack stack datum next = next stack1
bf2887cd22c1 fix Paper
ryokka
parents:
diff changeset
8 where
bf2887cd22c1 fix Paper
ryokka
parents:
diff changeset
9 element = cons datum (top stack)
bf2887cd22c1 fix Paper
ryokka
parents:
diff changeset
10 stack1 = record {top = Just element}
bf2887cd22c1 fix Paper
ryokka
parents:
diff changeset
11
bf2887cd22c1 fix Paper
ryokka
parents:
diff changeset
12 -- Basic stack implementations are specifications of a Stack
bf2887cd22c1 fix Paper
ryokka
parents:
diff changeset
13
3
576637483425 fix section, source code,etc
ryokka
parents: 1
diff changeset
14 singleLinkedStackSpec : {n m : Level } {t : Set m } {a : Set n} @$\rightarrow$@ StackMethods {n} {m} a {t} (SingleLinkedStack a)
1
bf2887cd22c1 fix Paper
ryokka
parents:
diff changeset
15 singleLinkedStackSpec = record {
bf2887cd22c1 fix Paper
ryokka
parents:
diff changeset
16 push = pushSingleLinkedStack
bf2887cd22c1 fix Paper
ryokka
parents:
diff changeset
17 ; pop = popSingleLinkedStack
bf2887cd22c1 fix Paper
ryokka
parents:
diff changeset
18 ; pop2 = pop2SingleLinkedStack
bf2887cd22c1 fix Paper
ryokka
parents:
diff changeset
19 ; get = getSingleLinkedStack
bf2887cd22c1 fix Paper
ryokka
parents:
diff changeset
20 ; get2 = get2SingleLinkedStack
bf2887cd22c1 fix Paper
ryokka
parents:
diff changeset
21 ; clear = clearSingleLinkedStack
bf2887cd22c1 fix Paper
ryokka
parents:
diff changeset
22 }
bf2887cd22c1 fix Paper
ryokka
parents:
diff changeset
23
3
576637483425 fix section, source code,etc
ryokka
parents: 1
diff changeset
24 createSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} @$\rightarrow$@ Stack {n} {m} a {t} (SingleLinkedStack a)
1
bf2887cd22c1 fix Paper
ryokka
parents:
diff changeset
25 createSingleLinkedStack = record {
bf2887cd22c1 fix Paper
ryokka
parents:
diff changeset
26 stack = emptySingleLinkedStack ;
bf2887cd22c1 fix Paper
ryokka
parents:
diff changeset
27 stackMethods = singleLinkedStackSpec
bf2887cd22c1 fix Paper
ryokka
parents:
diff changeset
28 }