module HW23a where

-- |Data type representing a second order DFA, parametrized by a type of states.
-- As for DFAs, the set of accepting states is implemented as a predicate
type DFA2 st = ([st], [Char], st->st->Char->st, st, st->Bool)

-- |Configurations 
type ConfigDFA2 st = ... -- Define the type of configurations

-- |Function mapping input strings to the corresponding initial configuration of a DFA2
initConfigDFA2 :: DFA2 st -> String -> ConfigDFA2 st
initConfigDFA2 (qs, sigma, delta, s, inF) w = ... -- Define the initial configuration of the DFA2 on input w

-- |Function mapping a configuration C1 to
--  (Nothing)  if C1 is a halting configuration
--  (Just C2)  if C2 is the next configuration in a valid computation
nextConfigDFA2 :: DFA2 st -> ConfigDFA2 st -> Maybe (ConfigDFA2 st)
nextConfigDFA2 (qs, sigma, delta, s, inF) ... = Nothing  -- Halting configuration
nextConfigDFA2 (qs, sigma, delta, s, inF) ... = Just ... -- Next configuration

-- |Function testing if a halting configuration is accepting or not
acceptConfigDFA2 :: DFA2 st -> ConfigDFA2 st -> Bool
acceptConfigDFA2 (qs, sigma, delta, s, inF) ... = ... -- Define which configurations are accepting

-- |Run a DFA2 on an input string, until it reaches a final configuration
runDFA2 :: DFA2 st -> String -> ConfigDFA2 st
runDFA2 dfa2 w = run (initConfigDFA2 dfa2 w) where
  run conf = 
    case (nextConfigDFA2 dfa2 conf) of 
      Nothing      -> conf         -- a final configuration has been reached
      Just newConf -> run newConf  -- otherwise, keep running

-- |Similar to runDFA, but just output True or False, rather than the final configuration
execDFA2 :: DFA2 st -> String -> Bool
execDFA2 dfa2 w = acceptConfigDFA2 dfa2 (runDFA2 dfa2 w)