Stepper.hs

module SSTG.Core.Execution.Stepper
    ( LiveState
    , DeadState
    , runBoundedBFS
    , runBoundedDFS
    ) where

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

import qualified Data.Map as M

type LiveState = ([Rule], State)

type DeadState = ([Rule], State)

incStatus :: Status -> Status
incStatus status = status { steps = (steps status) + 1 }

incState :: State -> State
incState state = state { state_status = incStatus (state_status state) }

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

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

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

runBoundedDFS = undefined