-- | Stepping Methods
module SSTG.Core.Execution.Stepping
    ( LiveState
    , DeadState
    , runBoundedBFS
    , runBoundedBFSLogged
    , runBoundedDFS
    , runBoundedDFSLogged
    ) where

import SSTG.Core.Execution.Models
import SSTG.Core.Execution.Rules

-- | A `State` that is not in value form yet, capable of being evaluated. A
-- list of `Rule`s is kept to denote reduction history.
type LiveState = ([Rule], State)

-- | A `State` that is in value form. A list of `Rule`s is kept to denote
-- reduction history.
type DeadState = ([Rule], State)

-- | Increment the `steps` counter of a `Status`.
incStatus :: Status -> Status
incStatus status = status { steps = (steps status) + 1 }

-- | Increment the `steps` counter inside the `state_status`.
incState :: State -> State
incState state = state { state_status = incStatus (state_status state) }

-- | Given a list of `State` along with its list of past `Rule` reductions,
-- apply STG reduction. If reduction yields `Nothing`, simply return itself.
step :: ([Rule], State) -> [([Rule], State)]
step (hist, state) = case reduce state of
    Nothing             -> [(hist, state)]
    Just (rule, states) -> map (\s -> (hist ++ [rule], incState s)) states

-- | This is what we use the `<*>` over.
pass :: [LiveState] -> ([LiveState], [DeadState] -> [DeadState])
pass rule_states = (lives, \prev -> prev ++ deads)
  where stepped = concatMap step rule_states
        lives   = filter (not . isStateValueForm . snd) stepped
        deads   = filter       (isStateValueForm . snd) stepped

-- | Run bounded breadth-first-search of the execution space with an `Int` to
-- denote the maximum number of steps to take.
runBoundedBFS :: Int -> State -> ([LiveState], [DeadState])
runBoundedBFS n state = (run execution) [([], state)]
  where passes    = take n (repeat (SymbolicT { run = pass }))
        start     = SymbolicT { run = (\lives -> (lives, [])) }
        execution = foldl (\acc s -> s <*> acc) start passes

-- | Run bounded breadth-first-search of the execution state with an `Int` to
-- denote the maximum number of steps to take. We keep track of a list to track
-- a history of all the execution snapshots. As it stands, this is currently
-- very NOT optimized.
runBoundedBFSLogged :: Int -> State -> [([LiveState], [DeadState])]
runBoundedBFSLogged n state = map (\i -> runBoundedBFS i state) [1..n]

-- | Currently @undefined@.
runBoundedDFS :: Int -> State -> ([LiveState], [DeadState])
runBoundedDFS = undefined

-- | Currently @undefined@.
runBoundedDFSLogged :: Int -> State -> [([LiveState], [DeadState])]
runBoundedDFSLogged = undefined