-- typedefs for clarity
type Stack = String
type Stream = String
-- an ADT that describes the possible states of a PDA. `Fail` is used to 
-- indicate that we're in a trap state and should return
data Result = Accept | Reject | Fail deriving (Show, Eq)
-- the PDA has a stream, a stack, the initial state (which is reused to
-- save the result of the last computation), and a function that takes
-- a member of the stream, the stack, and returns the new stack and whether
-- or not the PDA is currently in an accept or reject state
data PDA = PDA Stream Stack Result (Char -> Stack -> (Result, Stack))
 
decide :: PDA -> Bool
decide (PDA _ _ Fail _) = False -- if we ever enter a fail state, return False
decide (PDA [] _ r _) = r == Accept -- if the stream is empty, return the last computation
-- otherwise, recurse
decide (PDA (c:rest) s _ f) = 
  let (result, newStack) = f c s in
    decide (PDA rest newStack result f)
 
-- this particular PDA recognizes a^n b^n (that's n a's followed by n b's for all n >= 0)
-- modify the first parameter to try different strings
pda1 :: PDA
pda1 = PDA "aabb" [] Accept (\c stack ->
  case (c, stack) of 
     -- if there's one a on the stack and we read a b, then we will accept
     -- the word assuming we run out of input immediately afterward
    ('b', "a") -> (Accept, [])
    -- if we see an a, push it onto the stack
    ('a', s) -> (Reject, 'a' : s)
    -- if we see a b and we have more than 1 a on the stack, pop the a off
    ('b', 'a':s) -> (Reject, s)
    -- all other combinations need to fail immediately
    otherwise -> (Fail, undefined))
 
main :: IO ()
main = print $ decide pda1