{-# LANGUAGE ScopedTypeVariables, StandaloneDeriving, UndecidableInstances, NoMonomorphismRestriction, MultiParamTypeClasses #-}

-------------------------------------------------------------------------------------------
-- | CHR TreeTrie based solver shared internals, for all solvers
-------------------------------------------------------------------------------------------

module CHR.Types
  ( module CHR.Types.Core
  , module CHR.Data.TreeTrie
  
  , CHRKey

  , WorkTime
  , initWorkTime

  , Work'(..)
  , Work

  , SolveStep'(..)
  , SolveTrace'
  , emptySolveTrace
  , ppSolveTrace
  )
  where

import qualified CHR.Data.TreeTrie          as TT
import           CHR.Data.TreeTrie          ( TrTrKey )
import           CHR.Pretty                 as Pretty
import           CHR.Data.AssocL
import           CHR.Types.Core             ( IVar
                                            , NmToVarMp, emptyNmToVarMp
                                            , Prio
                                            , CHRPrioEvaluatableVal
                                            , IsConstraint
                                            , IsCHRGuard
                                            , IsCHRConstraint
                                            , IsCHRPrio
                                            , IsCHRBacktrackPrio
                                            , CHRCheckable
                                            , CHRMatchable
                                            , CHRPrioEvaluatable
                                            , CHREmptySubstitution
                                            , CHRMatcher
                                            , CHRMatchableKey
                                            , CHRMatcherFailure
                                            )

import qualified Data.Map                   as Map

-------------------------------------------------------------------------------------------
--- CHR key
-------------------------------------------------------------------------------------------

-- | Convenience alias for key into CHR store
type CHRKey v = TT.Key (TT.TrTrKey v)

-------------------------------------------------------------------------------------------
--- WorkTime, the time/history counter for solver work
-------------------------------------------------------------------------------------------

-- | All solver constraints are identified individually with a timestamp, also serving as its identification depending on the solver
type WorkTime = Int

initWorkTime :: WorkTime
initWorkTime :: WorkTime
initWorkTime = WorkTime
0

-------------------------------------------------------------------------------------------
--- Solver work and/or residual (non)work
-------------------------------------------------------------------------------------------

type WorkKey      v = CHRKey v

-- | A chunk of work to do when solving, a constraint + sequence nr
data Work' k c
  = Work
      { forall k c. Work' k c -> k
workKey     :: k                            -- ^ the key into the CHR store
      , forall k c. Work' k c -> c
workCnstr   :: !c                           -- ^ the constraint to be reduced
      , forall k c. Work' k c -> WorkTime
workTime    :: WorkTime                     -- ^ the timestamp identification at which the work was added
      }
  | Work_Residue
      { workCnstr   :: !c                           -- ^ the residual constraint
      }
  | Work_Solve
      { workCnstr   :: !c                           -- ^ constraint which must be solved
      }
  | Work_Fail

type Work c = Work' (WorkKey c) c

type instance TT.TrTrKey (Work' k c) = TT.TrTrKey c

instance Show (Work' k c) where
  show :: Work' k c -> String
show Work' k c
_ = String
"SolveWork"

instance (PP k, PP c) => PP (Work' k c) where
  pp :: Work' k c -> PP_Doc
pp (Work {workKey :: forall k c. Work' k c -> k
workKey=k
k, workCnstr :: forall k c. Work' k c -> c
workCnstr=c
c, workTime :: forall k c. Work' k c -> WorkTime
workTime=WorkTime
t})
                          = forall p. PP p => p -> PP_Doc
ppParens k
k forall a b. (PP a, PP b) => a -> b -> PP_Doc
>|< String
"@" forall a b. (PP a, PP b) => a -> b -> PP_Doc
>|< WorkTime
t forall a b. (PP a, PP b) => a -> b -> PP_Doc
>#< c
c
  pp (Work_Residue   c
c  ) = forall p. PP p => p -> PP_Doc
pp                           c
c
  pp (Work_Solve     c
c  ) = forall p. PP p => p -> PP_Doc
pp                           c
c
  pp (Work' k c
Work_Fail         ) = forall p. PP p => p -> PP_Doc
pp String
"fail"

-------------------------------------------------------------------------------------------
--- Solver trace
-------------------------------------------------------------------------------------------

-- | A trace step
data SolveStep' c r s
  = SolveStep
      { forall c r s. SolveStep' c r s -> r
stepChr         :: r
      , forall c r s. SolveStep' c r s -> s
stepSubst       :: s
      , forall c r s. SolveStep' c r s -> Maybe [c]
stepAlt         :: Maybe [c]
      , forall c r s. SolveStep' c r s -> [c]
stepNewTodo     :: [c]
      , forall c r s. SolveStep' c r s -> [c]
stepNewDone     :: [c]
      }
  | SolveStats
      { forall c r s. SolveStep' c r s -> Map String PP_Doc
stepStats       :: Map.Map String PP_Doc
      }
  | SolveDbg
      { forall c r s. SolveStep' c r s -> PP_Doc
stepPP          :: PP_Doc
      }

type SolveTrace' c r s = [SolveStep' c r s]

emptySolveTrace :: SolveTrace' c r s
emptySolveTrace :: forall c r s. SolveTrace' c r s
emptySolveTrace = []

instance Show (SolveStep' c r s) where
  show :: SolveStep' c r s -> String
show SolveStep' c r s
_ = String
"SolveStep"

instance (PP r, PP c) => {- (PP c, PP g) => -} PP (SolveStep' c r s) where
  pp :: SolveStep' c r s -> PP_Doc
pp (SolveStep   r
step s
_ Maybe [c]
_ [c]
todo [c]
done) = String
"STEP" forall a b. (PP a, PP b) => a -> b -> PP_Doc
>#< (r
step forall a b. (PP a, PP b) => a -> b -> PP_Doc
>-< String
"new todo:" forall a b. (PP a, PP b) => a -> b -> PP_Doc
>#< forall a. PP a => [a] -> PP_Doc
ppBracketsCommas [c]
todo forall a b. (PP a, PP b) => a -> b -> PP_Doc
>-< String
"new done:" forall a b. (PP a, PP b) => a -> b -> PP_Doc
>#< forall a. PP a => [a] -> PP_Doc
ppBracketsCommas [c]
done)
  pp (SolveStats  Map String PP_Doc
stats             ) = String
"STATS"  forall a b. (PP a, PP b) => a -> b -> PP_Doc
>#< (forall k v. (PP k, PP v) => AssocL k v -> PP_Doc
ppAssocLV (forall k a. Map k a -> [(k, a)]
Map.toList Map String PP_Doc
stats))
  pp (SolveDbg    PP_Doc
p                 ) = String
"DBG"  forall a b. (PP a, PP b) => a -> b -> PP_Doc
>#< PP_Doc
p

ppSolveTrace :: (PP r, PP c) => {- (PP s, PP c, PP g) => -} SolveTrace' c r s -> PP_Doc
ppSolveTrace :: forall r c s. (PP r, PP c) => [SolveStep' c r s] -> PP_Doc
ppSolveTrace SolveTrace' c r s
tr = forall a. PP a => [a] -> PP_Doc
ppBracketsCommasBlock [ forall p. PP p => p -> PP_Doc
pp SolveStep' c r s
st | SolveStep' c r s
st <- SolveTrace' c r s
tr ]