Mercurial > hg > Papers > 2019 > oshiro-thesis
diff final_pre/src/AgdaStackImpl.agda @ 7:0e8b9646d43f
add final_pre
author | e155702 |
---|---|
date | Sun, 17 Feb 2019 05:39:59 +0900 |
parents | |
children |
line wrap: on
line diff
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/final_pre/src/AgdaStackImpl.agda Sun Feb 17 05:39:59 2019 +0900 @@ -0,0 +1,28 @@ +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 + }