Mercurial > hg > Papers > 2021 > soto-thesis

comparison prepaper/src/stackImpl.agda.replaced @ 0:3dba680da508

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
init-test
author soto
date Tue, 08 Dec 2020 19:06:49 +0900
parents
children
comparison
equal deleted inserted replaced
-1:000000000000 0:3dba680da508
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} @$\rightarrow$@ SingleLinkedStack Data @$\rightarrow$@ Data @$\rightarrow$@ (Code : SingleLinkedStack Data @$\rightarrow$@ t) @$\rightarrow$@ 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} @$\rightarrow$@ 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} @$\rightarrow$@ Stack {n} {m} a {t} (SingleLinkedStack a)
35 createSingleLinkedStack = record {
36 stack = emptySingleLinkedStack ;
37 stackMethods = singleLinkedStackSpec
38 }