Mercurial > hg > Papers > 2018 > ryokka-sigos
comparison 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 |
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 } |