open import Level renaming (suc to succ ; zero to Zero )
module AgdaStackTest where

open import stack

open import Relation.Binary.PropositionalEquality
open import Relation.Binary.Core
open import Data.Nat
open import Function


open SingleLinkedStack
open Stack


-- after push 1 and 2, pop2 get 1 and 2

testStack02 : {m : Level } ->  ( Stack  ℕ (SingleLinkedStack ℕ) -> Bool {m} ) -> Bool {m}
testStack02 cs = pushStack createSingleLinkedStack 1 (\s -> pushStack s 2 cs)


testStack031 : (d1 d2 : ℕ ) -> Bool {Zero}
testStack031 2 1 = True
testStack031 _ _ = False

testStack032 : (d1 d2 : Maybe ℕ) -> Bool {Zero}
testStack032  (Just d1) (Just d2) = testStack031 d1 d2
testStack032  _ _ = False

testStack03 : {m : Level } -> Stack  ℕ (SingleLinkedStack ℕ) -> ((Maybe ℕ) -> (Maybe ℕ) -> Bool {m} ) -> Bool {m}
testStack03 s cs = pop2Stack s (\s d1 d2 -> cs d1 d2 )

testStack04 : Bool
testStack04 = testStack02 (\s -> testStack03 s testStack032)

testStack05 : testStack04 ≡ True
testStack05 = refl