{-# OPTIONS -fglasgow-exts -fallow-overlapping-instances #-}

module Stack where

import TestMonad
import ADT

import Control.Monad
import qualified Debug.QuickCheck as Q

-- Specification ----------------------------------------------------------

type Elem   = Object Int
type Stack  = [Elem]

push :: Elem -> Stack -> Stack
push x s = x : s

pop :: Stack -> (Elem, Stack)
pop []	    = (Null, [])
pop (x:xs)  = (x, xs)

isEmpty :: Stack -> Bool
isEmpty []	= True
isEmpty (x:xs)	= False

-- The Stack ADT ----------------------------------------------------------

stackADT :: ADT Stack
stackADT = ADT
    { adtName		= "Stack"
    , namePrefix	= "stack"
    , imports		= []
    , constructors	= [ mkConstructor [] gNew ]
    , methods		= [ mkMethod "push" t_void [ t_Integer ] gPush
			  , mkMethod "pop" t_Integer [ ] gPop
			  , mkMethod "isEmpty" t_boolean [ ] gIsEmpty
			  ]
    , methodDistr	= frequencyDistribution [ 5, 5, 1 ]
    , constructorFreqs	= [ 1 ]
    }

-- Generators -------------------------------------------------------------

gNew	 = methodCallGen0 cNew return
gPush	 = methodCallGen1 cPush return intGen
gPop	 = methodCallGen0 cPop $ readObject readN
gIsEmpty = methodCallGen0 cIsEmpty readB

intGen :: Q.Gen (Object Int)
intGen = Q.frequency
	    [ (1, return Null)
	    , (10, liftM NotNull Q.arbitrary)
	    ]

-- Verification -----------------------------------------------------------

cNew	    = cConstructor []
cPush x	    = cVoidMethod   "push"	(push x)
cPop	    = cImpureMethod "pop"	pop
cIsEmpty    = cPureMethod   "isEmpty"	isEmpty