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
}

-- Implementation

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}


popSingleLinkedStack : {n m : Level } {t : Set m } {a  : Set n} !$\rightarrow$! SingleLinkedStack a !$\rightarrow$! (Code : SingleLinkedStack a !$\rightarrow$! (Maybe a) !$\rightarrow$! t) !$\rightarrow$! t
popSingleLinkedStack stack cs with (top stack)
...                                | Nothing = cs stack  Nothing
...                                | Just d  = cs stack1 (Just data1)
  where
    data1  = datum d
    stack1 = record { top = (next d) }

pop2SingleLinkedStack : {n m : Level } {t : Set m } {a  : Set n} !$\rightarrow$! SingleLinkedStack a !$\rightarrow$! (Code : SingleLinkedStack a !$\rightarrow$! (Maybe a) !$\rightarrow$! (Maybe a) !$\rightarrow$! t) !$\rightarrow$! t
pop2SingleLinkedStack {n} {m} {t} {a} stack cs with (top stack)
...                                | Nothing = cs stack Nothing Nothing
...                                | Just d = pop2SingleLinkedStack!$\prime$! {n} {m} stack cs
  where
    pop2SingleLinkedStack!$\prime$! : {n m : Level } {t : Set m }  !$\rightarrow$! SingleLinkedStack a !$\rightarrow$! (Code : SingleLinkedStack a !$\rightarrow$! (Maybe a) !$\rightarrow$! (Maybe a) !$\rightarrow$! t) !$\rightarrow$! t
    pop2SingleLinkedStack!$\prime$! stack cs with (next d)
    ...              | Nothing = cs stack Nothing Nothing
    ...              | Just d1 = cs (record {top = (next d1)}) (Just (datum d)) (Just (datum d1))


getSingleLinkedStack : {n m : Level } {t : Set m } {a  : Set n} !$\rightarrow$! SingleLinkedStack a !$\rightarrow$! (Code : SingleLinkedStack a !$\rightarrow$! (Maybe a) !$\rightarrow$! t) !$\rightarrow$! t
getSingleLinkedStack stack cs with (top stack)
...                                | Nothing = cs stack  Nothing
...                                | Just d  = cs stack (Just data1)
  where
    data1  = datum d

get2SingleLinkedStack : {n m : Level } {t : Set m } {a  : Set n} !$\rightarrow$! SingleLinkedStack a !$\rightarrow$! (Code : SingleLinkedStack a !$\rightarrow$! (Maybe a) !$\rightarrow$! (Maybe a) !$\rightarrow$! t) !$\rightarrow$! t
get2SingleLinkedStack {n} {m} {t} {a} stack cs with (top stack)
...                                | Nothing = cs stack Nothing Nothing
...                                | Just d = get2SingleLinkedStack!$\prime$! {n} {m} stack cs
  where
    get2SingleLinkedStack!$\prime$! : {n m : Level} {t : Set m } !$\rightarrow$! SingleLinkedStack a !$\rightarrow$! (Code : SingleLinkedStack a !$\rightarrow$! (Maybe a) !$\rightarrow$! (Maybe a) !$\rightarrow$! t) !$\rightarrow$! t
    get2SingleLinkedStack!$\prime$! stack cs with (next d)
    ...              | Nothing = cs stack Nothing Nothing
    ...              | Just d1 = cs stack (Just (datum d)) (Just (datum d1))

clearSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} !$\rightarrow$! SingleLinkedStack a !$\rightarrow$! (SingleLinkedStack a !$\rightarrow$! t) !$\rightarrow$! t
clearSingleLinkedStack stack next = next (record {top = Nothing})