Mercurial > hg > Papers > 2018 > ryokka-sigos

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

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix section, source code,etc
author ryokka
date Thu, 19 Apr 2018 20:28:12 +0900
parents bf2887cd22c1
children
comparison
equal deleted inserted replaced
2:43e263faf88b 3:576637483425
1 record SingleLinkedStack {n : Level } (a : Set n) : Set n where 1 record SingleLinkedStack {n : Level } (a : Set n) : Set n where
2 field 2 field
3 top : Maybe (Element a) 3 top : Maybe (Element a)
4 open SingleLinkedStack 4 open SingleLinkedStack
5 5
6 pushSingleLinkedStack : {n m : Level } {t : Set m } {Data : Set n} $\rightarrow$ SingleLinkedStack Data $\rightarrow$ Data $\rightarrow$ (Code : SingleLinkedStack Data $\rightarrow$ t) $\rightarrow$ t 6 pushSingleLinkedStack : {n m : Level } {t : Set m } {Data : Set n} @$\rightarrow$@ SingleLinkedStack Data @$\rightarrow$@ Data @$\rightarrow$@ (Code : SingleLinkedStack Data @$\rightarrow$@ t) @$\rightarrow$@ t
7 pushSingleLinkedStack stack datum next = next stack1 7 pushSingleLinkedStack stack datum next = next stack1
8 where 8 where
9 element = cons datum (top stack) 9 element = cons datum (top stack)
10 stack1 = record {top = Just element} 10 stack1 = record {top = Just element}
11 11
12 -- Basic stack implementations are specifications of a Stack 12 -- Basic stack implementations are specifications of a Stack
13 13
14 singleLinkedStackSpec : {n m : Level } {t : Set m } {a : Set n} $\rightarrow$ StackMethods {n} {m} a {t} (SingleLinkedStack a) 14 singleLinkedStackSpec : {n m : Level } {t : Set m } {a : Set n} @$\rightarrow$@ StackMethods {n} {m} a {t} (SingleLinkedStack a)
15 singleLinkedStackSpec = record { 15 singleLinkedStackSpec = record {
16 push = pushSingleLinkedStack 16 push = pushSingleLinkedStack
17 ; pop = popSingleLinkedStack 17 ; pop = popSingleLinkedStack
18 ; pop2 = pop2SingleLinkedStack 18 ; pop2 = pop2SingleLinkedStack
19 ; get = getSingleLinkedStack 19 ; get = getSingleLinkedStack
20 ; get2 = get2SingleLinkedStack 20 ; get2 = get2SingleLinkedStack
21 ; clear = clearSingleLinkedStack 21 ; clear = clearSingleLinkedStack
22 } 22 }
23 23
24 createSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} $\rightarrow$ Stack {n} {m} a {t} (SingleLinkedStack a) 24 createSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} @$\rightarrow$@ Stack {n} {m} a {t} (SingleLinkedStack a)
25 createSingleLinkedStack = record { 25 createSingleLinkedStack = record {
26 stack = emptySingleLinkedStack ; 26 stack = emptySingleLinkedStack ;
27 stackMethods = singleLinkedStackSpec 27 stackMethods = singleLinkedStackSpec
28 } 28 }