module stack where

record Stack {a : Set} (stackImpl : Set a) where
  stack : stackImpl
  push : stackImpl -> a -> (stackImpl -> T) -> T
  pop  : stackImpl -> (stackImpl -> maybe a -> T) -> T
  

createSingleLinkedStack : Stack (SingleLinkedStack {a})
createSingleLinkedStack = record { 
  stack = record { top = nothing;}
  push  = pushSingleLinkedStack;
  pop   = popSingleLinkedStack;
}


record Element {a : Set} : Set where
  data : a
  next : Maybe (Element a)

record SingleLinkedStack {a : Set} : Set where
  top : Maybe (Element a)

pushSingleLinkedStack : Stack -> Data -> (Code : Stack -> T) -> T
pushSingleLinkedStack stack data next = next stack1
  where
    element = record {next = top stack; data = data}
    stack1  = record {top = just element}


popSingleLinkedStack : {a : Set} -> Stack -> (Code : Stack -> (Maybe a) -> T) -> T
popSingleLinkedStack stack next with (top  stack) =
  ... | nothing = next stack nothing
  ... | just d  = next stack1 data1
    where
      data1 = data d
      stack1 = record { top = (next d)}


test01 : Stack -> Maybe a -> T
test01 stack nothing  = false
test01 stack (just _) = true

test02 : Stack -> T
test02 stack = (pop stack) test01

test03 : T
test03 = push createSingleLinkedStack true test02

lemma : test01 == false
lemma = refl