Mercurial > hg > Papers > 2019 > oshiro-thesis
view final_main/src/AgdaStackImpl.agda @ 0:83f997abf3b5
first commit
author | e155702 |
---|---|
date | Thu, 14 Feb 2019 16:51:50 +0900 |
parents | |
children |
line wrap: on
line source
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} -> SingleLinkedStack Data -> Data -> (Code : SingleLinkedStack Data -> t) -> t pushSingleLinkedStack stack datum next = next stack1 where element = cons datum (top stack) stack1 = record {top = Just element} -- Basic stack implementations are specifications of a Stack singleLinkedStackSpec : {n m : Level } {t : Set m } {a : Set n} -> 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} -> Stack {n} {m} a {t} (SingleLinkedStack a) createSingleLinkedStack = record { stack = emptySingleLinkedStack ; stackMethods = singleLinkedStackSpec }