open import Level renaming (suc to Suc ; zero to Zero )
module Stack  where

open import Relation.Binary.PropositionalEquality
open import Relation.Binary.Core
open import Data.Nat hiding (compare)
open import Data.Maybe
open import Data.List
open import Function
open import logic

record Stack {n m : Level } (a : Set n ) {t : Set m }  : Set (m Level.⊔ (Suc n)) where
  field
    stack : List a

  pushStack :  a → (Stack a {t} → t) → t
  pushStack d next = next ( record { stack = d ∷ stack } )

  popStack : (Stack a {t} → Maybe a  → t) → t
  popStack next with stack
  popStack next | [] = next record { stack = [] } nothing
  popStack next | x ∷ t = next record { stack = t } (just x)

  pop2Stack :  (Stack a {t}  → Maybe a → Maybe a → t) → t
  pop2Stack next with stack
  pop2Stack next | x ∷ x₁ ∷ t = next record { stack = t } (just x) (just x₁)
  pop2Stack next | x ∷ [] = next record { stack = [] } (just x) nothing
  pop2Stack next | _ =  next record {stack = stack} nothing nothing

  get2Stack :  (Stack a {t}  → Maybe a → Maybe a → t) → t
  get2Stack next with stack
  get2Stack next | x ∷ x₁ ∷ t = next record { stack = stack } (just x) (just x₁)
  get2Stack next | x ∷ [] = next record { stack = stack } (just x) nothing
  get2Stack next | _ =  next record {stack = stack } nothing nothing

  clearStack : (Stack a {t}   → t) → t
  clearStack next = next record { stack = [] } 

open Stack

createSingleLinkedStack : {n m : Level } {t : Set m } (a : Set n) → Stack {n} {m} a {t} 
createSingleLinkedStack a = record { stack = [] }

test2 : List (Maybe ℕ)
test2 = pushStack (createSingleLinkedStack ℕ) 1 $ λ s → pushStack s 2 $ λ s → pop2Stack s ( λ s a b → a ∷ b ∷ [] )