Mercurial > hg > Papers > 2021 > soto-prosym
view Paper/src/stackImpl.agda.replaced @ 0:c59202657321
init
author | soto <soto@cr.ie.u-ryukyu.ac.jp> |
---|---|
date | Tue, 02 Nov 2021 06:55:58 +0900 |
parents | |
children | 339fb67b4375 |
line wrap: on
line source
record Element {l : Level} (a : Set l) : Set l where inductive constructor cons field datum : a -- `data` is reserved by Agda. next : Maybe (Element a) open Element record SingleLinkedStack {n : Level } (a : Set n) : Set n where field top : Maybe (Element a) open SingleLinkedStack pushSingleLinkedStack : {n m : Level } {t : Set m } {Data : Set n} @$\rightarrow$@ SingleLinkedStack Data @$\rightarrow$@ Data @$\rightarrow$@ (Code : SingleLinkedStack Data @$\rightarrow$@ t) @$\rightarrow$@ t pushSingleLinkedStack stack datum next = next stack1 where element = cons datum (top stack) stack1 = record {top = Just element} -- push 以下は省略 -- Basic stack implementations are specifications of a Stack singleLinkedStackSpec : {n m : Level } {t : Set m } {a : Set n} @$\rightarrow$@ StackMethods {n} {m} a {t} (SingleLinkedStack a) singleLinkedStackSpec = record { push = pushSingleLinkedStack ; pop = popSingleLinkedStack ; pop2 = pop2SingleLinkedStack ; get = getSingleLinkedStack ; get2 = get2SingleLinkedStack ; clear = clearSingleLinkedStack } createSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} @$\rightarrow$@ Stack {n} {m} a {t} (SingleLinkedStack a) createSingleLinkedStack = record { stack = emptySingleLinkedStack ; stackMethods = singleLinkedStackSpec }