{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE UndecidableInstances #-}

{-| Module: G2.Execution.Reducer

Controls reduction of `State`s.

The `runReducer` function reduces States, guided by a `Reducer`, `Halter`, and `Orderer`.
The `Reducer` defines the reduction rules used to map a State to one or more further States.
The `Halter` determines when to accept (return) or completely discard a state,
and allows /temporarily/ stopping reduction of a particular state, to allow reduction of other states.
The `Orderer` determines which state should be executed next when the Halter chooses to accept, reject,
or switch to executing a different state.
-}
module G2.Execution.Reducer ( Reducer (..)

                            , Halter (..)
                            , InitHalter
                            , UpdatePerStateHalt
                            , StopRed
                            , StepHalter

                            , Orderer (..)
                            , InitOrderer
                            , OrderStates
                            , UpdateSelected

                            , Processed (..)
                            , mapProcessed

                            , ReducerRes (..)
                            , HaltC (..)

                            , SomeReducer (..)
                            , SomeHalter (..)
                            , SomeOrderer (..)

                            -- * Reducers
                            , InitReducer
                            , RedRules
                            , mkSimpleReducer
                            , liftReducer
                            , liftSomeReducer

                            , stdRed
                            , nonRedPCTemplates
                            , nonRedPCRed
                            , nonRedPCRedConst
                            , taggerRed
                            , getLogger
                            , simpleLogger
                            , prettyLogger
                            , limLogger
                            , LimLogger (..)

                            , ReducerEq (..)
                            , (.==)
                            , (~>)
                            , (.~>)
                            , (-->)
                            , (.-->)

                            , (.|.)

                            -- * Halters
                            , mkSimpleHalter
                            , liftHalter
                            , liftSomeHalter

                            , swhnfHalter
                            , acceptIfViolatedHalter
                            , (<~>)
                            , zeroHalter
                            , discardIfAcceptedTagHalter
                            , maxOutputsHalter
                            , switchEveryNHalter
                            , varLookupLimitHalter
                            , stdTimerHalter
                            , timerHalter

                            -- * Orderers
                            , mkSimpleOrderer
                            , (<->)
                            , ordComb
                            , nextOrderer
                            , pickLeastUsedOrderer
                            , bucketSizeOrderer
                            , adtHeightOrderer
                            , adtSizeOrderer
                            , pcSizeOrderer
                            , incrAfterN
                            , quotTrueAssert

                            -- * Execution
                            , runReducer ) where

import G2.Config
import qualified G2.Language.ExprEnv as E
import G2.Execution.Rules
import G2.Language
import qualified G2.Language.Monad as MD
import qualified G2.Language.PathConds as PC
import qualified G2.Language.Stack as Stck
import G2.Solver
import G2.Lib.Printers

import Control.Monad.IO.Class
import qualified Control.Monad.State as SM
import Data.Foldable
import qualified Data.HashSet as HS
import qualified Data.HashMap.Strict as HM
import qualified Data.Map as M
import Data.Maybe
import Data.Monoid ((<>))
import qualified Data.List as L
import qualified Data.Text as T
import Data.Tuple
import Data.Time.Clock
import System.Directory

-- | Used when applying execution rules
-- Allows tracking extra information to control halting of rule application,
-- and to reorder states
-- see also, the Reducer, Halter, Orderer typeclasses
-- cases is used for logging states
data ExState rv hv sov t = ExState { state :: State t
                                   , reducer_val :: rv
                                   , halter_val :: hv
                                   , order_val :: sov
                                   }

-- | Keeps track of type a's that have either been accepted or dropped
data Processed a = Processed { accepted :: [a]
                             , discarded :: [a] }

mapProcessed :: (a -> b) -> Processed a -> Processed b
mapProcessed f pr = Processed { accepted = map f (accepted pr)
                              , discarded = map f (discarded pr)}

-- | Used by Reducers to indicate their progress reducing.
data ReducerRes = NoProgress | InProgress | Finished deriving (Eq, Ord, Show, Read)

progPrioritizer :: ReducerRes -> ReducerRes -> ReducerRes
progPrioritizer InProgress _ = InProgress
progPrioritizer _ InProgress = InProgress
progPrioritizer Finished _ = Finished
progPrioritizer _ Finished = Finished
progPrioritizer _ _ = NoProgress

-- | Used by members of the Halter typeclass to control whether to continue
-- evaluating the current State, or switch to evaluating a new state.
data HaltC = Discard -- ^ Switch to evaluating a new state, and reject the current state
           | Accept -- ^ Switch to evaluating a new state, and accept the current state
           | Switch -- ^ Switch to evaluating a new state, but continue evaluating the current state later
           | Continue -- ^ Continue evaluating the current State
           deriving (Eq, Ord, Show, Read)

type InitReducer rv t = State t -> rv
type RedRules m rv t = rv -> State t -> Bindings -> m (ReducerRes, [(State t, rv)], Bindings)


-- | A Reducer is used to define a set of Reduction Rules.
-- Reduction Rules take a `State`, and output new `State`s.
-- The reducer value, rv, can be used to track extra information, on a per `State` basis.
data Reducer m rv t = Reducer {
        -- | Initialized the reducer value
          initReducer :: InitReducer rv t

        -- | Takes a State, and performs the appropriate Reduction Rule
        , redRules :: RedRules m rv t

        -- | After a reducer returns multiple states,
        -- gives an opportunity to update with all States and Reducer values's,
        -- visible.
        -- Errors if the returned list is too short.
        -- If only one state is returned by all reducers, updateWithAll does not run.
        , updateWithAll :: [(State t, rv)] -> [rv]

        -- Action to run after a State is accepted.
        , onAccept :: State t -> rv -> m ()

        -- | Action to run after execution of all states has terminated.
        , afterRed :: m ()
    }

-- | A simple, default reducer.
-- `updateWithAll` does not change or adjust the reducer values.
-- `onAccept` immediately returns the empty tuple.
mkSimpleReducer :: Monad m => InitReducer rv t -> RedRules m rv t -> Reducer m rv t
mkSimpleReducer init_red red_rules =
    Reducer {
      initReducer = init_red
    , redRules = red_rules
    , updateWithAll = map snd
    , onAccept = \_ _ -> return ()
    , afterRed = return ()
    }
{-# INLINE mkSimpleReducer #-}

-- | Lift a reducer from a component monad to a constructed monad. 
liftReducer :: (Monad m1, SM.MonadTrans m2) => Reducer m1 rv t -> Reducer (m2 m1) rv t
liftReducer r = Reducer { initReducer = initReducer r
                        , redRules = \rv s b -> SM.lift ((redRules r) rv s b)
                        , updateWithAll = updateWithAll r
                        , onAccept = \s rv -> SM.lift ((onAccept r) s rv)
                        , afterRed = SM.lift (afterRed r)}

-- | Lift a SomeReducer from a component monad to a constructed monad. 
liftSomeReducer :: (Monad m1, SM.MonadTrans m2) => SomeReducer m1 t -> SomeReducer (m2 m1) t
liftSomeReducer (SomeReducer r) = SomeReducer (liftReducer r)

type InitHalter hv t = State t -> hv
type UpdatePerStateHalt hv t = hv -> Processed (State t) -> State t -> hv
type StopRed m hv t = hv -> Processed (State t) -> State t -> m HaltC
type StepHalter hv t = hv -> Processed (State t) -> [State t] -> State t -> hv

-- | Determines when to stop evaluating a state
-- The halter value, hv, can be used to track extra information, on a per `State` basis.
data Halter m hv t = Halter {
    -- | Initializes each state halter value
      initHalt :: InitHalter hv t

    -- | Runs whenever we switch to evaluating a different state,
    -- to update the halter value of that new state
    , updatePerStateHalt :: UpdatePerStateHalt hv t

    -- | Runs when we start execution on a state, immediately after
    -- `updatePerStateHalt`.  Allows a State to be discarded right
    -- before execution is about to (re-)begin.
    -- Return True if execution should proceed, False to discard
    , discardOnStart :: hv -> Processed (State t) -> State t -> Bool

    -- | Determines whether to continue reduction on the current state
    , stopRed :: StopRed m hv t

    -- | Takes a state, and updates its halter record field
    , stepHalter :: StepHalter hv t

    -- | After multiple states, are returned
    -- gives an opportunity to update halters with all States and halter values visible.
    -- Errors if the returned list is too short.
    -- If only one state is returned, updateHalterWithAll does not run.
    , updateHalterWithAll :: [(State t, hv)] -> [hv]
    }

-- | A simple, default halter.
mkSimpleHalter :: Monad m => InitHalter hv t -> UpdatePerStateHalt hv t -> StopRed m hv t -> StepHalter hv t -> Halter m hv t
mkSimpleHalter initial update stop step = Halter { initHalt = initial
                                                 , updatePerStateHalt = update
                                                 , discardOnStart = \_ _ _ -> False
                                                 , stopRed = stop
                                                 , stepHalter = step
                                                 , updateHalterWithAll = map snd }
{-# INLINE mkSimpleHalter #-}

-- | Lift a halter from a component monad to a constructed monad. 
liftHalter :: (Monad m1, SM.MonadTrans m2) => Halter m1 rv t -> Halter (m2 m1) rv t
liftHalter h = Halter { initHalt = initHalt h
                      , updatePerStateHalt = updatePerStateHalt h
                      , discardOnStart = discardOnStart h
                      , stopRed = \hv pr s -> SM.lift ((stopRed h) hv pr s)
                      , stepHalter = stepHalter h
                      , updateHalterWithAll = updateHalterWithAll h }

-- | Lift a SomeHalter from a component monad to a constructed monad. 
liftSomeHalter :: (Monad m1, SM.MonadTrans m2) => SomeHalter m1 t -> SomeHalter (m2 m1) t
liftSomeHalter (SomeHalter r) = SomeHalter (liftHalter r)

{-# INLINE mkStoppingHalter #-}
mkStoppingHalter :: Monad m => StopRed m () t -> Halter m () t
mkStoppingHalter stop =
            mkSimpleHalter
                (const ())
                (\_ _ _ -> ())
                stop
                (\_ _ _ _ -> ())

type InitOrderer sov t = State t -> sov
type OrderStates m sov b t = sov -> Processed (State t) -> State t -> m b
type UpdateSelected sov t = sov -> Processed (State t) -> State t -> sov

-- | Picks an order to evaluate the states, to allow prioritizing some over others.
-- The orderer value, sov, can be used to track extra information, on a per `State` basis.
-- The ordering type b, is used to determine what order to execute the states in.
-- In practice, `b` must be an instance of `Ord`.  When the orderer is called, the `State` corresponding
-- to the minimal `b` is executed.
data Orderer m sov b t = Orderer {
    -- | Initializing the per state ordering value 
      initPerStateOrder :: InitOrderer sov t

    -- | Assigns each state some value of an ordered type, and then proceeds with execution on the
    -- state assigned the minimal value
    , orderStates :: OrderStates m sov b t

    -- | Run on the selected state, to update it's sov field
    , updateSelected :: UpdateSelected sov t

    -- | Run on the state at each step, to update it's sov field
    , stepOrderer :: sov -> Processed (State t) -> [State t] -> State t -> m sov
    }

-- | A simple, default orderer.
mkSimpleOrderer :: Monad m => InitOrderer sov t -> OrderStates m sov b t -> UpdateSelected sov t -> Orderer m sov b t
mkSimpleOrderer initial order update = Orderer { initPerStateOrder = initial
                                               , orderStates = order
                                               , updateSelected = update
                                               , stepOrderer = \sov _ _ _ -> return sov}

getState :: M.Map b [s] -> Maybe (b, [s])
getState = M.lookupMin

-- | Hide the details of a Reducer's reducer value.
data SomeReducer m t where
    SomeReducer :: forall m rv t . Reducer m rv t -> SomeReducer m t

-- | Hide the details of a Halter's halter value.
data SomeHalter m t where
    SomeHalter :: forall m hv t . Halter m hv t -> SomeHalter m t

-- | Hide the details of an Orderer's orderer value and ordering type.
data SomeOrderer m t where
    SomeOrderer :: forall m sov b t . Ord b => Orderer m sov b t -> SomeOrderer m t


-- Combines multiple reducers together into a single reducer.

-- We use RC to combine the reducer values for RCombiner
-- We should never define any other instance of Reducer with RC, or export it
-- because this could lead to undecidable instances
data RC a b = RC a b

-- | Check if a `Reducer` returns some specific `ReducerRes`
data ReducerEq m t where
    (:==) :: forall m rv t . Reducer m rv t -> ReducerRes -> ReducerEq m t

(.==) :: SomeReducer m t -> ReducerRes -> ReducerEq m t
SomeReducer r .== res = r :== res

infixr 8 .==

infixr 7 ~>, .~>

infixr 5 -->, .-->

-- | @r1 ~> r2@ applies `Reducer` `r1`, followed by reducer `r2`. 
(~>) :: Monad m => Reducer m rv1 t -> Reducer m rv2 t -> Reducer m (RC rv1 rv2) t
r1 ~> r2 =
    Reducer { initReducer = \s -> RC (initReducer r1 s) (initReducer r2 s)

            , redRules = \(RC rv1 rv2) s b -> do
                (rr1, srv1, b') <- redRules r1 rv1 s b
                (rr2, srv2, b'') <- redRulesToStates r2 rv2 srv1 b'

                return (progPrioritizer rr1 rr2, srv2, b'')

            , updateWithAll = updateWithAllPair (updateWithAll r1) (updateWithAll r2)

            , onAccept = \s (RC rv1 rv2) -> do
                onAccept r1 s rv1
                onAccept r2 s rv2

            , afterRed = do
                afterRed r1
                afterRed r2

            }
{-# INLINE (~>) #-}

-- | `~>` adjusted to work on `SomeReducer`s, rather than `Reducer`s.
(.~>) :: Monad m => SomeReducer m t -> SomeReducer m t -> SomeReducer m t
SomeReducer r1 .~> SomeReducer r2 = SomeReducer (r1 ~> r2)
{-# INLINE (.~>) #-}

-- | @r1 := res --> r2@ applies `Reducer` `r1`.  If `r1` returns the `ReducerRes` `res`,
-- then `Reducer` `r2` is applied.  Otherwise, reduction halts.  
(-->) :: Monad m => ReducerEq m t -> Reducer m rv2 t -> SomeReducer m t
(r1 :== res) --> r2 =
    SomeReducer $
        Reducer { initReducer = \s -> RC (initReducer r1 s) (initReducer r2 s)

                , redRules = \(RC rv1 rv2) s b -> do
                    (rr1, srv1, b') <- redRules r1 rv1 s b
                    let (s', rv1') = unzip srv1

                    case rr1 == res of
                        True -> do
                            (rr2, ss, b'') <- redRulesToStates r2 rv2 srv1 b'
                            return (rr2, ss, b'')
                        False -> return (rr1, zip s' (map (flip RC rv2) rv1'), b')

                , updateWithAll = updateWithAllPair (updateWithAll r1) (updateWithAll r2)

                , onAccept = \s (RC rv1 rv2) -> do
                    onAccept r1 s rv1
                    onAccept r2 s rv2

                , afterRed = do
                    afterRed r1
                    afterRed r2
                }
{-# INLINE (-->) #-}

-- | `.-->` adjusted to take a `SomeReducer`, rather than a `Reducer`s.
(.-->) :: Monad m => ReducerEq m t -> SomeReducer m t -> SomeReducer m t
req .--> SomeReducer r = req --> r

redRulesToStatesAux :: Monad m =>  Reducer m rv2 t -> rv2 -> Bindings -> (State t, rv1) -> m (Bindings, (ReducerRes, [(State t, RC rv1 rv2)]))
redRulesToStatesAux r rv2 b (is, rv1) = do
        (rr_, is', b') <- redRules r rv2 is b
        return (b', (rr_, map (\(is'', rv2') -> (is'', RC rv1 rv2') ) is'))

redRulesToStates :: Monad m => Reducer m rv2 t -> rv2 -> [(State t, rv1)] -> Bindings -> m (ReducerRes, [(State t, RC rv1 rv2)], Bindings)
redRulesToStates r rv1 s b = do
    let redRulesToStatesAux' = redRulesToStatesAux r rv1
    (b', rs) <- MD.mapMAccumB redRulesToStatesAux' b s

    let (rr, s') = L.unzip rs

    let rf = foldr progPrioritizer NoProgress rr

    return $ (rf, concat s', b')

-- | @r1 .|. r2@ applies both Reducer r1 and Reducer r2 to the \inital\ state passed to the reducer,
-- and returns the list of states returned from both reducers combined.
-- Care should be taken to avoid unwanted duplication of states if, for example, neither of the reducers
-- makes progress.
(.|.) :: Monad m => Reducer m rv1 t -> Reducer m rv2 t -> Reducer m (RC rv1 rv2) t
r1 .|. r2 =
    Reducer { initReducer = \s -> RC (initReducer r1 s) (initReducer r2 s)

            , redRules = \(RC rv1 rv2) s b -> do
                (rr2, srv2, b') <- redRules r2 rv2 s b
                (rr1, srv1, b'') <- redRules r1 rv1 s b'

                let srv2' = map (\(s_, rv2_) -> (s_, RC rv1 rv2_) ) srv2
                    srv1' = map (\(s_, rv1_) -> (s_, RC rv1_ rv2) ) srv1

                return (progPrioritizer rr1 rr2, srv2' ++ srv1', b'')

            , updateWithAll = updateWithAllPair (updateWithAll r1) (updateWithAll r2)

            , onAccept = \s (RC rv1 rv2) -> do
                onAccept r1 s rv1
                onAccept r2 s rv2

            , afterRed = do
                afterRed r1
                afterRed r2

            }
{-# INLINE (.|.) #-}

updateWithAllPair :: ([(State t, rv1)] -> [rv1]) -> ([(State t, rv2)] -> [rv2]) -> [(State t, RC rv1 rv2)] -> [RC rv1 rv2]
updateWithAllPair update1 update2 srv =
                let
                    srv1 = map (\(s, RC rv1 _) -> (s, rv1)) srv
                    srv2 = map (\(s, RC _ rv2) -> (s, rv2)) srv

                    rv1' = update1 srv1
                    rv2' = update2 srv2
                in
                map (uncurry RC) $ zip rv1' rv2'

{-#INLINE stdRed #-}
{-# SPECIALIZE stdRed :: (Solver solver, Simplifier simplifier) => Sharing -> SymbolicFuncEval t -> solver -> simplifier -> Reducer IO () t #-}
stdRed :: (MonadIO m, Solver solver, Simplifier simplifier) => Sharing -> SymbolicFuncEval t -> solver -> simplifier -> Reducer m () t
stdRed share symb_func_eval solver simplifier =
        mkSimpleReducer (\_ -> ())
                        (\_ s b -> do
                            (r, s', b') <- liftIO $ stdReduce share symb_func_eval solver simplifier s b

                            return (if r == RuleIdentity then Finished else InProgress, s', b')
                        )

-- | Pushes non_red_path_conds onto the exec_stack for solving higher order symbolic function 
nonRedPCTemplates :: Monad m => Reducer m () t
nonRedPCTemplates = mkSimpleReducer (\_ -> ())
                        nonRedPCTemplatesFunc

nonRedPCTemplatesFunc :: Monad m => RedRules m () t
nonRedPCTemplatesFunc _
                      s@(State { expr_env = eenv
                         , curr_expr = cexpr
                         , exec_stack = stck
                         , non_red_path_conds = (nre1, nre2):nrs
                         , model = m })
                        b@(Bindings { name_gen = ng }) =
    
    let
        stck' = Stck.push (CurrExprFrame (EnsureEq nre2) cexpr) stck
        s' = s { exec_stack = stck', non_red_path_conds = nrs }
    in
    case retReplaceSymbFuncTemplate s' ng nre1 of
        Just (r, s'', ng') -> return (InProgress, zip s'' (repeat ()), b {name_gen = ng'})
        Nothing ->
            let 
                s'' = s' {curr_expr = CurrExpr Evaluate nre1}
            in return (InProgress, [(s'', ())], b)
nonRedPCTemplatesFunc _ s b = return (Finished, [(s, ())], b)

-- | Removes and reduces the values in a State's non_red_path_conds field. 
{-#INLINE nonRedPCRed #-}
nonRedPCRed :: Monad m => Reducer m () t
nonRedPCRed = mkSimpleReducer (\_ -> ())
                              nonRedPCRedFunc

nonRedPCRedFunc :: Monad m => RedRules m () t
nonRedPCRedFunc _
                s@(State { expr_env = eenv
                         , curr_expr = cexpr
                         , exec_stack = stck
                         , non_red_path_conds = (nre1, nre2):nrs
                         , model = m })
                b@(Bindings { higher_order_inst = inst })
    | Var (Id n t) <- nre2
    , E.isSymbolic n eenv
    , hasFuncType (PresType t) =
        let
            s' = s { expr_env = E.insert n nre1 eenv
                   , non_red_path_conds  = nrs }
        in
        return (InProgress, [(s', ())], b)
    | Var (Id n t) <- nre1
    , E.isSymbolic n eenv
    , hasFuncType (PresType t) =
        let
            s' = s { expr_env = E.insert n nre2 eenv
                   , non_red_path_conds  = nrs }
        in
        return (InProgress, [(s', ())], b)
    | otherwise = do
        let stck' = Stck.push (CurrExprFrame (EnsureEq nre2) cexpr) stck

        let cexpr' = CurrExpr Evaluate nre1

        let eenv_si_ces = substHigherOrder eenv m inst cexpr'

        let s' = s { exec_stack = stck'
                   , non_red_path_conds = nrs
                   }
            xs = map (\(eenv', m', ce) -> (s' { expr_env = eenv'
                                              , model = m'
                                              , curr_expr = ce }, ())) eenv_si_ces

        return (InProgress, xs, b)
nonRedPCRedFunc _ s b = return (Finished, [(s, ())], b)

-- [Higher-Order Model]
-- Substitutes all possible higher order functions for symbolic higher order functions.
-- We insert the substituted higher order function directly into the model, because, due
-- to the VAR-RED rule, the function name will (if the function is called) be lost during execution.
substHigherOrder :: ExprEnv -> Model -> HS.HashSet Name -> CurrExpr -> [(ExprEnv, Model, CurrExpr)]
substHigherOrder eenv m ns ce =
    let
        is = mapMaybe (\n -> case E.lookup n eenv of
                                Just e -> Just $ Id n (typeOf e)
                                Nothing -> Nothing) $ HS.toList ns

        higherOrd = filter (isTyFun . typeOf) . symbVars eenv $ ce
        higherOrdSub = map (\v -> (v, mapMaybe (genSubstitutable v) is)) higherOrd
    in
    substHigherOrder' [(eenv, m, ce)] higherOrdSub
    where
        genSubstitutable v i
            | Just bm <- specializes (typeOf v) (typeOf i) =
                let
                    bnds = map idName $ leadingTyForAllBindings i
                    tys = mapMaybe (\b -> fmap Type $ M.lookup b bm) bnds
                in
                Just . mkApp $ Var i:tys
            | otherwise = Nothing

substHigherOrder' :: [(ExprEnv, Model, CurrExpr)] -> [(Id, [Expr])] -> [(ExprEnv, Model, CurrExpr)]
substHigherOrder' eenvsice [] = eenvsice
substHigherOrder' eenvsice ((i, es):iss) =
    substHigherOrder'
        (concatMap (\e_rep ->
                        map (\(eenv, m, ce) -> ( E.insert (idName i) e_rep eenv
                                               , HM.insert (idName i) e_rep m
                                               , replaceASTs (Var i) e_rep ce)
                            ) eenvsice)
        es) iss

-- | Removes and reduces the values in a State's non_red_path_conds field
-- by instantiating higher order functions to be constant.
-- Does not return any states if the state does not contain at least one
-- higher order symbolic variable.
nonRedPCRedConst :: Monad m => Reducer m () t
nonRedPCRedConst = mkSimpleReducer (\_ -> ())
                                   nonRedPCRedConstFunc

nonRedPCRedConstFunc :: Monad m => RedRules m () t
nonRedPCRedConstFunc _
                     s@(State { expr_env = eenv
                              , curr_expr = cexpr
                              , exec_stack = stck
                              , non_red_path_conds = (nre1, nre2):nrs
                              , model = m })
                     b@(Bindings { name_gen = ng })
    | higher_ord <- L.filter (isTyFun . typeOf) $ E.symbolicIds eenv
    , not (null higher_ord) = do
        let stck' = Stck.push (CurrExprFrame (EnsureEq nre2) cexpr) stck

        let cexpr' = CurrExpr Evaluate nre1

        let (ng', new_lam_is) = L.mapAccumL (\ng_ ts -> swap $ freshIds ts ng_) ng (map anonArgumentTypes higher_ord)
            (new_sym_gen, ng'') = freshIds (map returnType higher_ord) ng'

            es = map (\(f_id, lam_i, sg_i) -> (f_id, mkLams (zip (repeat TermL) lam_i) (Var sg_i)) )
               $ zip3 higher_ord new_lam_is new_sym_gen

            eenv' = foldr (uncurry E.insert) eenv (map (\(i, e) -> (idName i, e)) es)
            eenv'' = foldr E.insertSymbolic eenv' new_sym_gen
            m' = foldr (\(i, e) -> HM.insert (idName i) e) m es

        let s' = s { expr_env = eenv''
                , curr_expr = cexpr'
                , model = m'
                , exec_stack = stck'
                , non_red_path_conds = nrs
                }

        return (InProgress, [(s', ())], b { name_gen = ng'' })
nonRedPCRedConstFunc _ s b = return (Finished, [], b)

{-# INLINE taggerRed #-}
taggerRed :: Monad m => Name -> Reducer m () t
taggerRed n = mkSimpleReducer (const ()) (taggerRedStep n)

taggerRedStep :: Monad m => Name -> RedRules m () t
taggerRedStep n _ s@(State {tags = ts}) b@(Bindings { name_gen = ng }) =
    let
        (n'@(Name n_ m_ _ _), ng') = freshSeededName n ng
    in
    if null $ HS.filter (\(Name n__ m__ _ _) -> n_ == n__ && m_ == m__) ts then
        return (Finished, [(s {tags = HS.insert n' ts}, ())], b { name_gen = ng' })
    else
        return (Finished, [(s, ())], b)


getLogger :: (MonadIO m, SM.MonadState PrettyGuide m, Show t) => Config -> Maybe (Reducer m [Int] t)
getLogger config = case logStates config of
                        Log Raw fp -> Just (simpleLogger fp)
                        Log Pretty fp -> Just (prettyLogger fp)
                        NoLog -> Nothing

-- | A Reducer to producer logging output 
simpleLogger :: (MonadIO m, Show t) => FilePath -> Reducer m [Int] t
simpleLogger fn =
    (mkSimpleReducer (const [])
                     (\li s b -> do
                        liftIO $ outputState fn li s b pprExecStateStr
                        return (NoProgress, [(s, li)], b) ))
                    { updateWithAll = \s -> map (\(l, i) -> l ++ [i]) $ zip (map snd s) [1..] }

-- | A Reducer to producer logging output 
prettyLogger :: (MonadIO m, SM.MonadState PrettyGuide m, Show t) => FilePath -> Reducer m [Int] t
prettyLogger fp =
    (mkSimpleReducer
        (const [])
        (\li s b -> do
            pg <- SM.get
            let pg' = updatePrettyGuide (s { track = () }) pg
            SM.put pg'
            liftIO $ outputState fp li s b (\s_ _ -> T.unpack $ prettyState pg' s_)
            return (NoProgress, [(s, li)], b)
        )
    ) { updateWithAll = \s -> map (\(l, i) -> l ++ [i]) $ zip (map snd s) [1..]
      , onAccept = \_ ll -> liftIO . putStrLn $ "Accepted on path " ++ show ll }

-- | A Reducer to producer limited logging output.
data LimLogger =
    LimLogger { every_n :: Int -- Output a state every n steps
              , after_n :: Int -- Only begin outputting after passing a certain n
              , before_n :: Maybe Int -- Only output before a certain n
              , down_path :: [Int] -- Output states that have gone down or are going down the given path prefix
              , lim_output_path :: String
              }

data LLTracker = LLTracker { ll_count :: Int, ll_offset :: [Int]}

limLogger :: (MonadIO m, Show t) => LimLogger -> Reducer m LLTracker t
limLogger ll@(LimLogger { after_n = aft, before_n = bfr, down_path = down }) =
    (mkSimpleReducer (const $ LLTracker { ll_count = every_n ll, ll_offset = []}) rr)
        { updateWithAll = updateWithAllLL
        , onAccept = \_ llt -> liftIO . putStrLn $ "Accepted on path " ++ show (ll_offset llt)}
    where
        rr llt@(LLTracker { ll_count = 0, ll_offset = off }) s b
            | down `L.isPrefixOf` off || off `L.isPrefixOf` down
            , aft <= length_rules && maybe True (length_rules <=) bfr = do
                liftIO $ outputState (lim_output_path ll) off s b pprExecStateStr
                return (NoProgress, [(s, llt { ll_count = every_n ll })], b)
            | otherwise =
                return (NoProgress, [(s, llt { ll_count = every_n ll })], b)
            where
                length_rules = length (rules s)
        rr llt@(LLTracker {ll_count = n}) s b =
            return (NoProgress, [(s, llt { ll_count = n - 1 })], b)

        updateWithAllLL [(_, l)] = [l]
        updateWithAllLL ss =
            map (\(llt, i) -> llt { ll_offset = ll_offset llt ++ [i] }) $ zip (map snd ss) [1..]

outputState :: FilePath -> [Int] -> State t -> Bindings -> (State t -> Bindings -> String) -> IO ()
outputState dn is s b printer = do
    fn <- getFile dn is "state" s

    -- Don't re-output states that  already exist
    exists <- doesPathExist fn

    if not exists
        then do
            let write = printer s b
            writeFile fn write

            putStrLn fn
        else return ()

getFile :: String -> [Int] -> String -> State t -> IO String
getFile dn is n s = do
    let dir = dn ++ "/" ++ foldl' (\str i -> str ++ show i ++ "/") "" is
    createDirectoryIfMissing True dir
    let fn = dir ++ n ++ show (length $ rules s) ++ ".txt"
    return fn

-- We use C to combine the halter values for HCombiner
-- We should never define any other instance of Halter with C, or export it
-- because this could lead to undecidable instances
data C a b = C a b deriving Eq

instance (ASTContainer a Expr, ASTContainer b Expr) => ASTContainer (C a b) Expr where
    containedASTs (C a b) = containedASTs a ++ containedASTs b
    modifyContainedASTs f (C a b) = C (modifyContainedASTs f a) (modifyContainedASTs f b)

instance (ASTContainer a Type, ASTContainer b Type) => ASTContainer (C a b) Type where
    containedASTs (C a b) = containedASTs a ++ containedASTs b
    modifyContainedASTs f (C a b) = C (modifyContainedASTs f a) (modifyContainedASTs f b)

instance (Named a, Named b) => Named (C a b) where
    names (C a b) = names a <> names b
    rename old new (C a b) = C (rename old new a) (rename old new b)
    renames hm (C a b) = C (renames hm a) (renames hm b)

-- | Allows executing multiple halters.
-- If the halters disagree, prioritizes the order:
-- Discard, Accept, Switch, Continue
(<~>) :: Monad m => Halter m hv1 t -> Halter m hv2 t -> Halter m (C hv1 hv2) t
h1 <~> h2 =
    Halter {
              initHalt = \s ->
                let
                    hv1 = initHalt h1 s
                    hv2 = initHalt h2 s
                in
                C hv1 hv2

            , updatePerStateHalt = \(C hv1 hv2) proc s ->
                let
                    hv1' = updatePerStateHalt h1 hv1 proc s
                    hv2' = updatePerStateHalt h2 hv2 proc s
                in
                C hv1' hv2'

            , discardOnStart = \(C hv1 hv2) proc s ->
                let
                    b1 = discardOnStart h1 hv1 proc s
                    b2 = discardOnStart h2 hv2 proc s
                in
                b1 || b2

            , stopRed = \(C hv1 hv2) proc s -> do
                hc1 <- stopRed h1 hv1 proc s
                hc2 <- stopRed h2 hv2 proc s

                return $ min hc1 hc2

            , stepHalter = \(C hv1 hv2) proc xs s ->
                let
                    hv1' = stepHalter h1 hv1 proc xs s
                    hv2' = stepHalter h2 hv2 proc xs s
                in
                C hv1' hv2'

            , updateHalterWithAll = \shv ->
                let
                    shv1 = map (\(s, C hv1 _) -> (s, hv1)) shv
                    shv2 = map (\(s, C _ hv2) -> (s, hv2)) shv

                    shv1' = updateHalterWithAll h1 shv1
                    shv2' = updateHalterWithAll h2 shv2
                in
                map (uncurry C) $ zip shv1' shv2'
            }
{-# INLINE (<~>) #-}

{-# INLINE swhnfHalter #-}
swhnfHalter :: Monad m => Halter m () t
swhnfHalter = mkStoppingHalter stop
    where
        stop _ _ s =
            case isExecValueForm s of
                True -> return Accept
                False -> return Continue

-- | Accepts a state when it is in SWHNF and true_assert is true
-- Discards it if in SWHNF and true_assert is false
acceptIfViolatedHalter :: Monad m => Halter m () t
acceptIfViolatedHalter = mkStoppingHalter stop
    where
        stop _ _ s =
            case isExecValueForm s of
                True
                    | true_assert s -> return Accept
                    | otherwise -> return Discard
                False -> return Continue

-- | Allows execution to continue until the step counter hits 0, then discards the state
zeroHalter :: Monad m => Int -> Halter m Int t
zeroHalter n = mkSimpleHalter
                    (const n)
                    (\h _ _ -> h)
                    (\h _ _ -> if h == 0 then return Discard else return Continue)
                    (\h _ _ _ -> h - 1)

maxOutputsHalter :: Monad m => Maybe Int -> Halter m (Maybe Int) t
maxOutputsHalter m = mkSimpleHalter
                        (const m)
                        (\hv _ _ -> hv)
                        (\_ (Processed {accepted = acc}) _ ->
                            case m of
                                Just m' -> return $ if length acc >= m' then Discard else Continue
                                _ -> return Continue)
                        (\hv _ _ _ -> hv)

-- | Switch execution every n steps
{-# INLINE switchEveryNHalter #-}
switchEveryNHalter :: Monad m => Int -> Halter m Int t
switchEveryNHalter sw = (mkSimpleHalter
                            (const sw)
                            (\_ _ _ -> sw)
                            (\i _ _ -> return $ if i <= 0 then Switch else Continue)
                            (\i _ _ _ -> i - 1))
                        { updateHalterWithAll = updateAll }
    where
        updateAll [] = []
        updateAll xs@((_, c):_) =
            let
                len = length xs
                c' = c `quot` len
            in
            replicate len c'

-- | If the Name, disregarding the Unique, in the DiscardIfAcceptedTag
-- matches a Tag in the Accepted State list,
-- and in the State being evaluated, discard the State
discardIfAcceptedTagHalter :: Monad m => Name -> Halter m (HS.HashSet Name) t
discardIfAcceptedTagHalter (Name n m _ _) =
                            mkSimpleHalter
                                (const HS.empty)
                                ups
                                (\ns _ _ -> return $ if not (HS.null ns) then Discard else Continue)
                                (\hv _ _ _ -> hv)
    where
        ups _
            (Processed {accepted = acc})
            (State {tags = ts}) =
                let
                    allAccTags = HS.unions $ map tags acc
                    matchCurrState = HS.intersection ts allAccTags
                in
                HS.filter (\(Name n' m' _ _) -> n == n' && m == m') matchCurrState

-- | Counts the number of variable lookups are made, and switches the state
-- whenever we've hit a threshold
varLookupLimitHalter :: Monad m => Int -> Halter m Int t
varLookupLimitHalter lim = mkSimpleHalter
                        (const lim)
                        (\_ _ _ -> lim)
                        (\l _ _ -> return $ if l <= 0 then Switch else Continue)
                        step
    where
        step l _ _ (State { curr_expr = CurrExpr Evaluate (Var _) }) = l - 1
        step l _ _ _ = l

{-# INLINE stdTimerHalter #-}
stdTimerHalter :: (MonadIO m, MonadIO m_run) => NominalDiffTime -> m (Halter m_run Int t)
stdTimerHalter ms = timerHalter ms Discard 10

{-# INLINE timerHalter #-}
timerHalter :: (MonadIO m, MonadIO m_run) => NominalDiffTime -> HaltC -> Int -> m (Halter m_run Int t)
timerHalter ms def ce = do
    curr <- liftIO $ getCurrentTime
    return $ mkSimpleHalter
                (const 0)
                (\_ _ _ -> 0)
                (stop curr)
                step
    where
        stop it v (Processed { accepted = acc }) _
            | v == 0
            , not (null acc) = do
                curr <- liftIO $ getCurrentTime
                let diff = diffUTCTime curr it

                if diff > ms
                    then return def
                    else return Continue
            | otherwise = return Continue

        step v _ _ _
            | v >= ce = 0
            | otherwise = v + 1

-- Orderer things
(<->) :: Monad m => Orderer m sov1 b1 t -> Orderer m sov2 b2 t -> Orderer m (C sov1 sov2) (b1, b2) t
or1 <-> or2 = Orderer {
      initPerStateOrder = \s ->
          let
              sov1 = initPerStateOrder or1 s
              sov2 = initPerStateOrder or2 s
          in
          C sov1 sov2

    , orderStates = \(C sov1 sov2) pr s -> do
          sov1' <- orderStates or1 sov1 pr s
          sov2' <- orderStates or2 sov2 pr s
          return (sov1', sov2')

    , updateSelected = \(C sov1 sov2) proc s ->
          let
              sov1' = updateSelected or1 sov1 proc s
              sov2' = updateSelected or2 sov2 proc s
          in
          C sov1' sov2'

    , stepOrderer = \(C sov1 sov2) proc xs s -> do
            sov1' <- stepOrderer or1 sov1 proc xs s
            sov2' <- stepOrderer or2 sov2 proc xs s
            
            return (C sov1' sov2')
    }

ordComb :: Monad m => (v1 -> v2 -> v3) -> Orderer m sov1 v1 t  -> Orderer m sov2 v2 t -> Orderer m (C sov1 sov2) v3 t
ordComb f or1 or2 = Orderer {
      initPerStateOrder = \s ->
          let
              sov1 = initPerStateOrder or1 s
              sov2 = initPerStateOrder or2 s
          in
          C sov1 sov2

    , orderStates = \(C sov1 sov2) pr s -> do
          sov1' <- orderStates or1 sov1 pr s
          sov2' <- orderStates or2 sov2 pr s
          return (f sov1' sov2')

    , updateSelected = \(C sov1 sov2) proc s ->
          let
              sov1' = updateSelected or1 sov1 proc s
              sov2' = updateSelected or2 sov2 proc s
          in
          C sov1' sov2'

    , stepOrderer = \(C sov1 sov2) proc xs s -> do
          sov1' <- stepOrderer or1 sov1 proc xs s
          sov2' <- stepOrderer or2 sov2 proc xs s
          return (C sov1' sov2')
    }

nextOrderer :: Monad m => Orderer m () Int t
nextOrderer = mkSimpleOrderer (const ()) (\_ _ _ -> return 0) (\v _ _ -> v)

-- | Continue execution on the state that has been picked the least in the past. 
pickLeastUsedOrderer :: Monad m => Orderer m Int Int t
pickLeastUsedOrderer = mkSimpleOrderer (const 0) (\v _ _ -> return v) (\v _ _ -> v + 1)

-- | Floors and does bucket size
bucketSizeOrderer :: Monad m => Int -> Orderer m Int Int t
bucketSizeOrderer b =
    mkSimpleOrderer (const 0)
                    (\v _ _ -> return $ floor (fromIntegral v / fromIntegral b :: Float))
                    (\v _ _ -> v + 1)

-- | Orders by the size (in terms of height) of (previously) symbolic ADT.
-- In particular, aims to first execute those states with a height closest to
-- the specified height.
adtHeightOrderer :: Monad m => Int -> Maybe Name -> Orderer m (HS.HashSet Name, Bool) Int t
adtHeightOrderer pref_height mn =
    (mkSimpleOrderer initial
                    order
                    (\v _ _ -> v))
                    { stepOrderer = \sov pr st s -> return $ step sov pr st s }
    where
        -- Normally, each state tracks the names of currently symbolic variables,
        -- but here we want all variables that were ever symbolic.
        -- To track this, we use a HashSet.
        -- The tracked bool is to speed up adjusting this hashset- if it is set to false,
        -- we do not update the hashset.  If it is set to true,
        -- after the next step the hashset will be updated, and the bool will be set
        -- back to false.
        -- This avoids repeated operations on the hashset after rules that we know
        -- will not add symbolic variables.
        initial s = (HS.fromList . map idName . E.symbolicIds . expr_env $ s, False)
        order (v, _) _ s =
            let
                m = maximum $ (-1):(HS.toList $ HS.map (flip adtHeight s) v)
                h = abs (pref_height - m)
            in
            return h

        step (v, _) _ _
                      (State { curr_expr = CurrExpr _ (SymGen _ _) }) = (v, True)
        step(v, True) _ _ s =
            (v `HS.union` (HS.fromList . map idName . E.symbolicIds . expr_env $ s), False)
        step (v, _) _ _
                       (State { curr_expr = CurrExpr _ (Tick (NamedLoc n') (Var (Id vn _))) })
                | Just n <- mn, n == n' =
                    (HS.insert vn v, False)
        step  v _ _ _ = v

adtHeight :: Name -> State t -> Int
adtHeight n s@(State { expr_env = eenv })
    | Just (E.Sym _) <- v = 0
    | Just (E.Conc e) <- v =
        1 + adtHeight' e s
    | otherwise = 0
    where
        v = E.lookupConcOrSym n eenv

adtHeight' :: Expr -> State t -> Int
adtHeight' e s =
    let
        _:es = unApp e
    in
    maximum $ 0:map (\e' -> case e' of
                        Var (Id n _) -> adtHeight n s
                        _ -> 0) es

-- | Orders by the combined size of (previously) symbolic ADT.
-- In particular, aims to first execute those states with a combined ADT size closest to
-- the specified zize.
adtSizeOrderer :: Monad m => Int -> Maybe Name -> Orderer m (HS.HashSet Name, Bool) Int t
adtSizeOrderer pref_height mn =
    (mkSimpleOrderer initial
                    order
                    (\v _ _ -> v))
                    { stepOrderer = \sov pr st s -> return $ step sov pr st s }
    where
        -- Normally, each state tracks the names of currently symbolic variables,
        -- but here we want all variables that were ever symbolic.
        -- To track this, we use a HashSet.
        -- The tracked bool is to speed up adjusting this hashset- if it is set to false,
        -- we do not update the hashset.  If it is set to true,
        -- after the next step the hashset will be updated, and the bool will be set
        -- back to false.
        -- This avoids repeated operations on the hashset after rules that we know
        -- will not add symbolic variables.
        initial s = (HS.fromList . map idName . E.symbolicIds . expr_env $ s, False)
        order (v, _) _ s =
            let
                m = sum (HS.toList $ HS.map (flip adtSize s) v)
                h = abs (pref_height - m)
            in
            return h

        step (v, _) _ _
                      (State { curr_expr = CurrExpr _ (SymGen _ _) }) = (v, True)
        step (v, True) _ _ s =
            (v `HS.union` (HS.fromList . map idName . E.symbolicIds . expr_env $ s), False)
        step (v, _) _ _
                       (State { curr_expr = CurrExpr _ (Tick (NamedLoc n') (Var (Id vn _))) })
                | Just n <- mn, n == n' = (HS.insert vn v, False)
        step v _ _ _ = v

adtSize :: Name -> State t -> Int
adtSize n s@(State { expr_env = eenv })
    | Just (E.Sym _) <- v = 0
    | Just (E.Conc e) <- v =
        1 + adtSize' e s
    | otherwise = 0
    where
        v = E.lookupConcOrSym n eenv

adtSize' :: Expr -> State t -> Int
adtSize' e s =
    let
        _:es = unApp e
    in
    sum $ 0:map (\e' -> case e' of
                        Var (Id n _) -> adtSize n s
                        _ -> 0) es

-- | Orders by the number of Path Constraints
pcSizeOrderer :: Monad m =>
                 Int  -- ^ What size should we prioritize?
              -> Orderer m () Int t
pcSizeOrderer pref_height = mkSimpleOrderer (const ())
                                            order
                                            (\v _ _ -> v)
    where
        order _ _ s =
            let
                m = PC.number (path_conds s)
                h = abs (pref_height - m)
            in
            return h

data IncrAfterNTr sov = IncrAfterNTr { steps_since_change :: Int
                                     , incr_by :: Int
                                     , underlying :: sov }

-- | Wraps an existing Orderer, and increases it's value by 1, every time
-- it doesn't change after N steps 
incrAfterN :: (Eq sov, Enum b, Monad m) => Int -> Orderer m sov b t -> Orderer m (IncrAfterNTr sov) b t
incrAfterN n ord = (mkSimpleOrderer initial order update) { stepOrderer = step }
    where
        initial s =
            IncrAfterNTr { steps_since_change = 0
                         , incr_by = 0
                         , underlying = initPerStateOrder ord s }

        order sov pr s = do
            b <- orderStates ord (underlying sov) pr s
            return $ succNTimes (incr_by sov) b

        update sov pr s =
            sov { underlying = updateSelected ord (underlying sov) pr s }

        step sov pr xs s = do
            let under = underlying sov
            under' <- stepOrderer ord under pr xs s
            let sov' = sov { underlying = under' }

            if | steps_since_change sov >= n ->
                    return $ sov' { incr_by = incr_by sov' + 1
                                  , steps_since_change = 0 }
               | under /= under' ->
                    return $ sov' { steps_since_change = 0 }
               | otherwise ->
                    return $ sov' { steps_since_change = steps_since_change sov' + 1}

succNTimes :: Enum b => Int -> b -> b
succNTimes x b
    | x <= 0 = b
    | otherwise = succNTimes (x - 1) (succ b)

-- | Wraps an existing orderer, and divides its value by 2 if true_assert is true
quotTrueAssert :: (Monad m, Integral b) => Orderer m sov b t -> Orderer m sov b t
quotTrueAssert ord = (mkSimpleOrderer (initPerStateOrder ord)
                                      order
                                      (updateSelected ord))
                                      { stepOrderer = stepOrderer ord}
    where
        order sov pr s = do
            b <- orderStates ord sov pr s
            return (if true_assert s then b `quot` 2 else b)

--------
--------

{-# INLINABLE runReducer #-}
{-# SPECIALIZE runReducer :: Ord b =>
                             Reducer IO rv t
                          -> Halter IO hv t
                          -> Orderer IO sov b t
                          -> State t
                          -> Bindings
                          -> IO (Processed (State t), Bindings)
    #-}
{-# SPECIALIZE runReducer :: Ord b =>
                             Reducer (SM.StateT PrettyGuide IO) rv t
                          -> Halter (SM.StateT PrettyGuide IO) hv t
                          -> Orderer (SM.StateT PrettyGuide IO) sov b t
                          -> State t
                          -> Bindings
                          -> SM.StateT PrettyGuide IO (Processed (State t), Bindings)
    #-}
-- | Uses a passed Reducer, Halter and Orderer to execute the reduce on the State, and generated States
runReducer :: (Monad m, Ord b) =>
              Reducer m rv t
           -> Halter m hv t
           -> Orderer m sov b t
           -> State t
           -> Bindings
           -> m (Processed (State t), Bindings)
runReducer red hal ord s b = do
    let pr = Processed {accepted = [], discarded = []}
    let s' = ExState { state = s
                     , reducer_val = initReducer red s
                     , halter_val = initHalt hal s
                     , order_val = initPerStateOrder ord s }

    (states, b') <- runReducer' red hal ord pr s' b M.empty
    afterRed red
    return (states, b')

{-# INLINABLE runReducer' #-}
runReducer' :: (Monad m, Ord b)
            => Reducer m rv t
            -> Halter m hv t
            -> Orderer m sov b t
            -> Processed (State t)
            -> ExState rv hv sov t
            -> Bindings
            -> M.Map b [ExState rv hv sov t]
            -> m (Processed (State t), Bindings)
runReducer' red hal ord pr rs@(ExState { state = s, reducer_val = r_val, halter_val = h_val, order_val = o_val }) b xs = do
    hc <- stopRed hal h_val pr s
    case () of
        ()
            | hc == Accept -> do
                onAccept red s r_val
                let pr' = pr {accepted = state rs:accepted pr}
                    jrs = minState ord pr' xs
                case jrs of
                    Just (rs', xs') -> switchState red hal ord pr' rs' b xs'
                    Nothing -> return (pr', b)
            | hc == Discard ->
                let
                    pr' = pr {discarded = state rs:discarded pr}
                    jrs = minState ord pr' xs
                in
                case jrs of
                    Just (rs', xs') ->
                        switchState red hal ord pr' rs' b xs'
                    Nothing -> return (pr', b)
            | hc == Switch -> do
                let rs' = rs { order_val = updateSelected ord (order_val rs) pr (state rs) }
                k <- orderStates ord (order_val rs') pr (state rs)
                let Just (rs'', xs') = minState ord pr (M.insertWith (++) k [rs'] xs)
                switchState red hal ord pr rs'' b xs'
            | otherwise -> do
                (_, reduceds, b') <- redRules red r_val s b
                let reduceds' = map (\(r, rv) -> (r {num_steps = num_steps r + 1}, rv)) reduceds

                    r_vals = if length reduceds' > 1
                                then updateWithAll red reduceds' ++ error "List returned by updateWithAll is too short."
                                else map snd reduceds

                    reduceds_h_vals = map (\(r, _) -> (r, h_val)) reduceds'
                    h_vals = if length reduceds' > 1
                                then updateHalterWithAll hal reduceds_h_vals ++ error "List returned by updateWithAll is too short."
                                else repeat h_val

                    new_states = map fst reduceds'

                mod_info <- mapM (\(s', r_val', h_val') -> do
                                        or_v <- stepOrderer ord o_val pr new_states s'
                                        return $ rs { state = s'
                                                    , reducer_val = r_val'
                                                    , halter_val = stepHalter hal h_val' pr new_states s'
                                                    , order_val = or_v}) $ zip3 new_states r_vals h_vals




                case mod_info of
                    (s_h:ss_tail) -> do
                        b_ss_tail <- mapM (\s' -> do
                                                    n_b <- orderStates ord (order_val s') pr (state s')
                                                    return (n_b, s')) ss_tail

                        let xs' = foldr (\(or_b, s') -> M.insertWith (++) or_b [s']) xs b_ss_tail

                        runReducer' red hal ord pr s_h b' xs'
                    [] -> runReducerList red hal ord pr xs b'

{-# INLINABLE switchState #-}
switchState :: (Monad m, Ord b)
            => Reducer m rv t
            -> Halter m hv t
            -> Orderer m sov b t
            -> Processed (State t)
            -> ExState rv hv sov t
            -> Bindings
            -> M.Map b [ExState rv hv sov t]
            -> m (Processed (State t), Bindings)
switchState red hal ord pr rs b xs
    | not $ discardOnStart hal (halter_val rs') pr (state rs') =
        runReducer' red hal ord pr rs' b xs
    | otherwise =
        runReducerListSwitching red hal ord (pr {discarded = state rs':discarded pr}) xs b
    where
        rs' = rs { halter_val = updatePerStateHalt hal (halter_val rs) pr (state rs) }

{-# INLINABLE runReducerList #-}
-- To be used when we we need to select a state without switching 
runReducerList :: (Monad m, Ord b)
               => Reducer m rv t
               -> Halter m hv t
               -> Orderer m sov b t
               -> Processed (State t)
               -> M.Map b [ExState rv hv sov t]
               -> Bindings
               -> m (Processed (State t), Bindings)
runReducerList red hal ord pr m binds =
    case minState ord pr m of
        Just (rs, m') ->
            let
                rs' = rs { halter_val = updatePerStateHalt hal (halter_val rs) pr (state rs) }
            in
            runReducer' red hal ord pr rs' binds m'
        Nothing -> return (pr, binds)

{-# INLINABLE runReducerListSwitching #-}
-- To be used when we are possibly switching states 
runReducerListSwitching :: (Monad m, Ord b)
                        => Reducer m rv t
                        -> Halter m hv t
                        -> Orderer m sov b t
                        -> Processed (State t)
                        -> M.Map b [ExState rv hv sov t]
                        -> Bindings
                        -> m (Processed (State t), Bindings)
runReducerListSwitching red hal ord pr m binds =
    case minState ord pr m of
        Just (x, m') -> switchState red hal ord pr x binds m'
        Nothing -> return (pr, binds)

{-# INLINABLE minState #-}
-- Uses the Orderer to determine which state to continue execution on.
-- Returns that State, and a list of the rest of the states 
minState :: Ord b
         => Orderer m sov b t
         -> Processed (State t)
         -> M.Map b [ExState rv hv sov t]
         -> Maybe ((ExState rv hv sov t), M.Map b [ExState rv hv sov t])
minState ord pr m =
    case getState m of
      Just (k, x:[]) -> Just (x, M.delete k m)
      Just (k, x:xs) -> Just (x, M.insert k xs m)
      Just (k, []) -> minState ord pr $ M.delete k m
      Nothing -> Nothing