{-# LANGUAGE ConstraintKinds, ScopedTypeVariables, StandaloneDeriving, UndecidableInstances, NoMonomorphismRestriction, MultiParamTypeClasses, TemplateHaskell, FunctionalDependencies #-}
module CHR.Solve.MonoBacktrackPrio
( Verbosity(..)
, CHRGlobState(..)
, emptyCHRGlobState
, chrgstVarToNmMp
, chrgstStatNrSolveSteps
, CHRBackState(..)
, emptyCHRBackState
, emptyCHRStore
, CHRMonoBacktrackPrioT
, MonoBacktrackPrio
, runCHRMonoBacktrackPrioT
, addRule
, addConstraintAsWork
, SolverResult(..)
, ppSolverResult
, CHRSolveOpts(..)
, defaultCHRSolveOpts
, StoredCHR
, storedChrRule'
, chrSolve
, slvFreshSubst
, getSolveTrace
, IsCHRSolvable(..)
)
where
import CHR.Utils
import CHR.Data.Lens
import CHR.Data.Lookup (Lookup, LookupApply, Scoped)
import qualified CHR.Data.Lookup as Lk
import qualified CHR.Data.TreeTrie as TT
import CHR.Data.VarLookup
import qualified Data.Set as Set
import qualified Data.PQueue.Prio.Min as Que
import qualified Data.Map.Strict as Map
import qualified Data.HashMap.Strict as MapH
import qualified Data.IntMap.Strict as IntMap
import qualified Data.IntSet as IntSet
import qualified Data.Sequence as Seq
import Data.List as List
import Data.Typeable
import Data.Maybe
import Control.Monad
import Control.Monad.Except
import Control.Monad.State.Strict
import Control.Monad.LogicState
import CHR.Pretty as Pretty
import CHR.Types.Core
import CHR.Types.Rule
import CHR.Data.Substitutable
import CHR.Data.AssocL
import CHR.Data.Fresh
import CHR.Types
data Verbosity
= Verbosity_Quiet
| Verbosity_Normal
| Verbosity_Debug
| Verbosity_ALot
deriving (Eq, Ord, Show, Enum, Typeable)
type CHRInx = Int
data CHRConstraintInx =
CHRConstraintInx
{ chrciInx :: {-# UNPACK #-} !CHRInx
, chrciAt :: {-# UNPACK #-} !Int
}
deriving (Eq, Ord, Show)
instance PP CHRConstraintInx where
pp (CHRConstraintInx i j) = i >|< "." >|< j
data StoredCHR c g bp p
= StoredCHR
{ _storedHeadKeys :: ![CHRKey c]
, _storedChrRule :: !(Rule c g bp p)
, _storedChrInx :: {-# UNPACK #-} !CHRInx
}
deriving (Typeable)
storedChrRule' :: StoredCHR c g bp p -> Rule c g bp p
storedChrRule' = _storedChrRule
data CHRStore cnstr guard bprio prio
= CHRStore
{ _chrstoreTrie :: TT.TreeTrie (TT.TrTrKey cnstr) [CHRConstraintInx]
, _chrstoreTable :: IntMap.IntMap (StoredCHR cnstr guard bprio prio)
}
deriving (Typeable)
emptyCHRStore :: TT.TTCtxt (TT.TrTrKey cnstr) => CHRStore cnstr guard bprio prio
emptyCHRStore = CHRStore TT.empty IntMap.empty
type WorkInx = WorkTime
type WorkInxSet = IntSet.IntSet
data WorkStore cnstr
= WorkStore
{ _wkstoreTrie :: !(TT.TreeTrie (TT.TrTrKey cnstr) [WorkInx])
, _wkstoreTable :: !(IntMap.IntMap (Work cnstr))
, _wkstoreNextFreeWorkInx :: {-# UNPACK #-} !WorkTime
}
deriving (Typeable)
emptyWorkStore :: TT.TTCtxt (TT.TrTrKey cnstr) => WorkStore cnstr
emptyWorkStore = WorkStore TT.empty IntMap.empty initWorkTime
data WorkQueue
= WorkQueue
{ _wkqueueActive :: !WorkInxSet
, _wkqueueRedo :: !WorkInxSet
, _wkqueueDidSomething :: !Bool
}
deriving (Typeable)
emptyWorkQueue :: WorkQueue
emptyWorkQueue = WorkQueue IntSet.empty IntSet.empty True
data MatchedCombi' c w =
MatchedCombi
{ mcCHR :: !c
, mcWork :: ![w]
}
deriving (Eq, Ord)
instance Show (MatchedCombi' c w) where
show _ = "MatchedCombi"
instance (PP c, PP w) => PP (MatchedCombi' c w) where
pp (MatchedCombi c ws) = ppParensCommas [pp c, ppBracketsCommas ws]
type MatchedCombi = MatchedCombi' CHRInx WorkInx
data SolverReductionStep' c w
= SolverReductionStep
{ slvredMatchedCombi :: !(MatchedCombi' c w)
, slvredChosenBodyAltInx :: {-# UNPACK #-} !Int
, slvredNewWork :: !(Map.Map ConstraintSolvesVia [w])
}
| SolverReductionDBG PP_Doc
type SolverReductionStep = SolverReductionStep' CHRInx WorkInx
instance Show (SolverReductionStep' c w) where
show _ = "SolverReductionStep"
instance {-# OVERLAPPABLE #-} (PP c, PP w) => PP (SolverReductionStep' c w) where
pp (SolverReductionStep (MatchedCombi ci ws) a wns) = "STEP" >#< ci >|< "." >|< a >-< indent 2 ("+" >#< ppBracketsCommas ws >-< "-> (new)" >#< (ppAssocL $ Map.toList $ Map.map ppBracketsCommas wns))
pp (SolverReductionDBG p) = "DBG" >#< p
instance (PP w) => PP (SolverReductionStep' Int w) where
pp (SolverReductionStep (MatchedCombi ci ws) a wns) = ci >|< "." >|< a >#< "+" >#< ppBracketsCommas ws >#< "-> (new)" >#< (ppAssocL $ Map.toList $ Map.map ppBracketsCommas wns)
pp (SolverReductionDBG p) = "DBG" >#< p
data WaitForVar s
= WaitForVar
{ _waitForVarVars :: !(CHRWaitForVarSet s)
, _waitForVarWorkInx :: {-# UNPACK #-} !WorkInx
}
deriving (Typeable)
type WaitInx = Int
data CHRGlobState cnstr guard bprio prio subst env m
= CHRGlobState
{ _chrgstStore :: !(CHRStore cnstr guard bprio prio)
, _chrgstNextFreeRuleInx :: {-# UNPACK #-} !CHRInx
, _chrgstScheduleQueue :: !(Que.MinPQueue (CHRPrioEvaluatableVal bprio) (CHRMonoBacktrackPrioT cnstr guard bprio prio subst env m (SolverResult subst)))
, _chrgstTrace :: !(SolveTrace' cnstr (StoredCHR cnstr guard bprio prio) subst)
, _chrgstStatNrSolveSteps :: {-# UNPACK #-} !Int
, _chrgstVarToNmMp :: !VarToNmMp
}
deriving (Typeable)
emptyCHRGlobState :: TT.TTCtxt (TT.TrTrKey c) => CHRGlobState c g b p s e m
emptyCHRGlobState = CHRGlobState emptyCHRStore 0 Que.empty emptySolveTrace 0 emptyVarToNmMp
data CHRBackState cnstr bprio subst env
= CHRBackState
{ _chrbstBacktrackPrio :: !(CHRPrioEvaluatableVal bprio)
, _chrbstRuleWorkQueue :: !WorkQueue
, _chrbstSolveQueue :: !WorkQueue
, _chrbstResidualQueue :: [WorkInx]
, _chrbstWorkStore :: !(WorkStore cnstr)
, _chrbstMatchedCombis :: !(Set.Set MatchedCombi)
, _chrbstFreshVar :: {-# UNPACK #-} !Int
, _chrbstSolveSubst :: !subst
, _chrbstWaitForVar :: !(Map.Map (VarLookupKey subst) [WaitForVar subst])
, _chrbstReductionSteps :: ![SolverReductionStep]
}
deriving (Typeable)
emptyCHRBackState :: (TT.TTCtxt (TT.TrTrKey c), CHREmptySubstitution s, Bounded (CHRPrioEvaluatableVal bp)) => CHRBackState c bp s e
emptyCHRBackState = CHRBackState minBound emptyWorkQueue emptyWorkQueue [] emptyWorkStore Set.empty 0 chrEmptySubst Map.empty []
type CHRMonoBacktrackPrioT cnstr guard bprio prio subst env m
= LogicStateT (CHRGlobState cnstr guard bprio prio subst env m) (CHRBackState cnstr bprio subst env) m
type CHRFullState cnstr guard bprio prio subst env m
= (CHRGlobState cnstr guard bprio prio subst env m, CHRBackState cnstr bprio subst env)
gst :: Lens (CHRFullState cnstr guard bprio prio subst env m) (CHRGlobState cnstr guard bprio prio subst env m)
gst = fstl
{-# INLINE gst #-}
bst :: Lens (CHRFullState cnstr guard bprio prio subst env m) (CHRBackState cnstr bprio subst env)
bst = sndl
{-# INLINE bst #-}
type MonoBacktrackPrio cnstr guard bprio prio subst env m
= ( IsCHRSolvable env cnstr guard bprio prio subst
, Monad m
, Lookup subst (VarLookupKey subst) (VarLookupVal subst)
, LookupApply subst subst
, Fresh Int (ExtrValVarKey (VarLookupVal subst))
, ExtrValVarKey (VarLookupVal subst) ~ VarLookupKey subst
, VarTerm (VarLookupVal subst)
)
data SolverResult subst =
SolverResult
{ slvresSubst :: !subst
, slvresResidualCnstr :: ![WorkInx]
, slvresWorkCnstr :: ![WorkInx]
, slvresWaitVarCnstr :: ![WorkInx]
, slvresReductionSteps :: ![SolverReductionStep]
}
type IsCHRSolvable env c g bp p s
= ( IsCHRConstraint env c s
, IsCHRGuard env g s
, IsCHRBacktrackPrio env bp s
, IsCHRPrio env p s
, PP (VarLookupKey s)
)
mkLabel ''WaitForVar
mkLabel ''StoredCHR
mkLabel ''CHRStore
mkLabel ''WorkStore
mkLabel ''WorkQueue
mkLabel ''CHRGlobState
mkLabel ''CHRBackState
getSolveTrace :: (PP c, PP g, PP bp, MonoBacktrackPrio c g bp p s e m) => CHRMonoBacktrackPrioT c g bp p s e m PP_Doc
getSolveTrace = fmap (ppSolveTrace . reverse) $ getl $ gst ^* chrgstTrace
instance Show (StoredCHR c g bp p) where
show _ = "StoredCHR"
ppStoredCHR :: (PP (TT.TrTrKey c), PP c, PP g, PP bp, PP p) => StoredCHR c g bp p -> PP_Doc
ppStoredCHR c@(StoredCHR {})
= ppParensCommas (_storedHeadKeys c)
>-< _storedChrRule c
>-< indent 2
(ppParensCommas
[ pp $ _storedChrInx c
])
instance (PP (TT.TrTrKey c), PP c, PP g, PP bp, PP p) => PP (StoredCHR c g bp p) where
pp = ppStoredCHR
addRule :: MonoBacktrackPrio c g bp p s e m => Rule c g bp p -> CHRMonoBacktrackPrioT c g bp p s e m ()
addRule chr = do
i <- modifyAndGet (gst ^* chrgstNextFreeRuleInx) $ \i -> (i, i + 1)
let ks = map TT.toTreeTrieKey $ ruleHead chr
gst ^* chrgstStore ^* chrstoreTable =$: IntMap.insert i (StoredCHR ks chr i)
gst ^* chrgstStore ^* chrstoreTrie =$: \t ->
foldr (TT.unionWith (++)) t [ TT.singleton k [CHRConstraintInx i j] | (k,c,j) <- zip3 ks (ruleHead chr) [0..] ]
return ()
addToWorkQueue :: MonoBacktrackPrio c g bp p s e m => WorkInx -> CHRMonoBacktrackPrioT c g bp p s e m ()
addToWorkQueue i = do
bst ^* chrbstRuleWorkQueue ^* wkqueueActive =$: (IntSet.insert i)
bst ^* chrbstRuleWorkQueue ^* wkqueueDidSomething =: True
{-# INLINE addToWorkQueue #-}
addRedoToWorkQueue :: MonoBacktrackPrio c g bp p s e m => WorkInx -> CHRMonoBacktrackPrioT c g bp p s e m ()
addRedoToWorkQueue i = do
bst ^* chrbstRuleWorkQueue ^* wkqueueRedo =$: (IntSet.insert i)
{-# INLINE addRedoToWorkQueue #-}
addWorkToWaitForVarQueue :: (MonoBacktrackPrio c g bp p s e m, Ord (VarLookupKey s)) => CHRWaitForVarSet s -> WorkInx -> CHRMonoBacktrackPrioT c g bp p s e m ()
addWorkToWaitForVarQueue wfvs wi = do
let w = WaitForVar wfvs wi
bst ^* chrbstWaitForVar =$: Map.unionWith (++) (Map.fromList [(v,[w]) | v <- Set.toList wfvs])
splitOffResolvedWaitForVarWork :: (MonoBacktrackPrio c g bp p s e m, Ord (VarLookupKey s)) => CHRWaitForVarSet s -> CHRMonoBacktrackPrioT c g bp p s e m [WorkInx]
splitOffResolvedWaitForVarWork vars = do
wm <- getl $ bst ^* chrbstWaitForVar
let
(wmRelease,wmRemain) = Map.partitionWithKey (\v _ -> Set.member v vars) wm
wfvs = concat $ Map.elems wmRelease
(wvars, winxs) = (\(vss,wis) -> (Set.unions vss, IntSet.fromList wis)) $ unzip [ (vs,wi) | (WaitForVar {_waitForVarVars=vs, _waitForVarWorkInx=wi}) <- wfvs ]
bst ^* chrbstWaitForVar =:
foldr (Map.alter $ maybe Nothing $ \wfvs -> case filter (\i -> _waitForVarWorkInx i `IntSet.notMember` winxs) wfvs of
[] -> Nothing
wfvs' -> Just wfvs'
)
wmRemain
(Set.toList wvars)
return $ IntSet.toList winxs
addWorkToSolveQueue :: MonoBacktrackPrio c g bp p s e m => WorkInx -> CHRMonoBacktrackPrioT c g bp p s e m ()
addWorkToSolveQueue i = do
bst ^* chrbstSolveQueue ^* wkqueueActive =$: (IntSet.insert i)
splitWorkFromSolveQueue :: MonoBacktrackPrio c g bp p s e m => CHRMonoBacktrackPrioT c g bp p s e m (Maybe (WorkInx))
splitWorkFromSolveQueue = do
wq <- getl $ bst ^* chrbstSolveQueue ^* wkqueueActive
case IntSet.minView wq of
Nothing ->
return Nothing
Just (workInx, wq') -> do
bst ^* chrbstSolveQueue ^* wkqueueActive =: wq'
return $ Just (workInx)
deleteFromWorkQueue :: MonoBacktrackPrio c g bp p s e m => WorkInxSet -> CHRMonoBacktrackPrioT c g bp p s e m ()
deleteFromWorkQueue is = do
bst ^* chrbstRuleWorkQueue ^* wkqueueActive =$: flip IntSet.difference is
bst ^* chrbstRuleWorkQueue ^* wkqueueRedo =$: flip IntSet.difference is
waitingInWorkQueue :: MonoBacktrackPrio c g bp p s e m => CHRMonoBacktrackPrioT c g bp p s e m WorkInxSet
waitingInWorkQueue = do
a <- getl $ bst ^* chrbstRuleWorkQueue ^* wkqueueActive
r <- getl $ bst ^* chrbstRuleWorkQueue ^* wkqueueRedo
return $ IntSet.union a r
splitFromWorkQueue :: MonoBacktrackPrio c g bp p s e m => CHRMonoBacktrackPrioT c g bp p s e m (Maybe WorkInx)
splitFromWorkQueue = do
wq <- getl $ bst ^* chrbstRuleWorkQueue ^* wkqueueActive
case IntSet.minView wq of
Nothing -> do
did <- modifyAndGet (bst ^* chrbstRuleWorkQueue ^* wkqueueDidSomething) $ \d -> (d, False)
if did
then do
wr <- modifyAndGet (bst ^* chrbstRuleWorkQueue ^* wkqueueRedo) $ \r -> (r, IntSet.empty)
bst ^* chrbstRuleWorkQueue ^* wkqueueActive =: wr
splitFromWorkQueue
else
return Nothing
Just (workInx, wq') -> do
bst ^* chrbstRuleWorkQueue ^* wkqueueActive =: wq'
return $ Just workInx
addConstraintAsWork
:: MonoBacktrackPrio c g bp p s e m
=> c
-> CHRMonoBacktrackPrioT c g bp p s e m (ConstraintSolvesVia, WorkInx)
addConstraintAsWork c = do
let via = cnstrSolvesVia c
addw i w = do
bst ^* chrbstWorkStore ^* wkstoreTable =$: IntMap.insert i w
return (via,i)
i <- fresh
w <- case via of
ConstraintSolvesVia_Rule -> do
bst ^* chrbstWorkStore ^* wkstoreTrie =$: TT.insertByKeyWith (++) k [i]
addToWorkQueue i
return $ Work k c i
where k = TT.toTreeTrieKey c
ConstraintSolvesVia_Solve -> do
addWorkToSolveQueue i
return $ Work_Solve c
ConstraintSolvesVia_Residual -> do
bst ^* chrbstResidualQueue =$: (i :)
return $ Work_Residue c
ConstraintSolvesVia_Fail -> do
addWorkToSolveQueue i
return Work_Fail
addw i w
where
fresh = modifyAndGet (bst ^* chrbstWorkStore ^* wkstoreNextFreeWorkInx) $ \i -> (i, i + 1)
slvSucces :: MonoBacktrackPrio c g bp p s e m => [WorkInx] -> CHRMonoBacktrackPrioT c g bp p s e m (SolverResult s)
slvSucces leftoverWork = do
bst <- getl $ bst
let ret = return $ SolverResult
{ slvresSubst = bst ^. chrbstSolveSubst
, slvresResidualCnstr = reverse $ bst ^. chrbstResidualQueue
, slvresWorkCnstr = leftoverWork
, slvresWaitVarCnstr = [ wfv ^. waitForVarWorkInx | wfvs <- Map.elems $ bst ^. chrbstWaitForVar, wfv <- wfvs ]
, slvresReductionSteps = reverse $ bst ^. chrbstReductionSteps
}
ret `mplus` slvScheduleRun
slvFail :: MonoBacktrackPrio c g bp p s e m => CHRMonoBacktrackPrioT c g bp p s e m (SolverResult s)
slvFail = do
slvScheduleRun
{-# INLINE slvFail #-}
slvSchedule :: MonoBacktrackPrio c g bp p s e m => CHRPrioEvaluatableVal bp -> CHRMonoBacktrackPrioT c g bp p s e m (SolverResult s) -> CHRMonoBacktrackPrioT c g bp p s e m ()
slvSchedule bprio slv = do
gst ^* chrgstScheduleQueue =$: Que.insert bprio slv
{-# INLINE slvSchedule #-}
slvSchedule' :: MonoBacktrackPrio c g bp p s e m => CHRMonoBacktrackPrioT c g bp p s e m (SolverResult s) -> CHRMonoBacktrackPrioT c g bp p s e m ()
slvSchedule' slv = do
bprio <- getl $ bst ^* chrbstBacktrackPrio
slvSchedule bprio slv
{-# INLINE slvSchedule' #-}
slvReschedule :: MonoBacktrackPrio c g bp p s e m => CHRMonoBacktrackPrioT c g bp p s e m (SolverResult s) -> CHRMonoBacktrackPrioT c g bp p s e m (SolverResult s)
slvReschedule slv = do
slvSchedule' slv
slvScheduleRun
{-# INLINE slvReschedule #-}
slvSplitFromSchedule :: MonoBacktrackPrio c g bp p s e m => CHRMonoBacktrackPrioT c g bp p s e m (Maybe (CHRPrioEvaluatableVal bp, CHRMonoBacktrackPrioT c g bp p s e m (SolverResult s)))
slvSplitFromSchedule = modifyAndGet (gst ^* chrgstScheduleQueue) $ \q -> (Que.getMin q, Que.deleteMin q)
{-# INLINE slvSplitFromSchedule #-}
slvScheduleRun :: MonoBacktrackPrio c g bp p s e m => CHRMonoBacktrackPrioT c g bp p s e m (SolverResult s)
slvScheduleRun = slvSplitFromSchedule >>= maybe mzero snd
{-# INLINE slvScheduleRun #-}
lkupWork :: MonoBacktrackPrio c g bp p s e m => WorkInx -> CHRMonoBacktrackPrioT c g bp p s e m (Work c)
lkupWork i = fmap (IntMap.findWithDefault (panic "MBP.wkstoreTable.lookup") i) $ getl $ bst ^* chrbstWorkStore ^* wkstoreTable
{-# INLINE lkupWork #-}
lkupChr :: MonoBacktrackPrio c g bp p s e m => CHRInx -> CHRMonoBacktrackPrioT c g bp p s e m (StoredCHR c g bp p)
lkupChr i = fmap (IntMap.findWithDefault (panic "MBP.chrSolve.chrstoreTable.lookup") i) $ getl $ gst ^* chrgstStore ^* chrstoreTable
{-# INLINE lkupChr #-}
cvtSolverReductionStep :: MonoBacktrackPrio c g bp p s e m => SolverReductionStep' CHRInx WorkInx -> CHRMonoBacktrackPrioT c g bp p s e m (SolverReductionStep' (StoredCHR c g bp p) (Work c))
cvtSolverReductionStep (SolverReductionStep mc ai nw) = do
mc <- cvtMC mc
nw <- fmap Map.fromList $ forM (Map.toList nw) $ \(via,i) -> do
i <- forM i lkupWork
return (via, i)
return $ SolverReductionStep mc ai nw
where
cvtMC (MatchedCombi {mcCHR = c, mcWork = ws}) = do
c' <- lkupChr c
ws' <- forM ws lkupWork
return $ MatchedCombi c' ws'
cvtSolverReductionStep (SolverReductionDBG pp) = return (SolverReductionDBG pp)
ppSolverResult
:: ( MonoBacktrackPrio c g bp p s e m
, VarUpdatable s s
, PP s
) => Verbosity
-> SolverResult s
-> CHRMonoBacktrackPrioT c g bp p s e m PP_Doc
ppSolverResult verbosity (SolverResult {slvresSubst = s, slvresResidualCnstr = ris, slvresWorkCnstr = wis, slvresWaitVarCnstr = wvis, slvresReductionSteps = steps}) = do
rs <- forM ris $ \i -> lkupWork i >>= return . pp . workCnstr
ws <- forM wis $ \i -> lkupWork i >>= return . pp . workCnstr
wvs <- forM wvis $ \i -> lkupWork i >>= return . pp . workCnstr
ss <- if verbosity >= Verbosity_ALot
then forM steps $ \step -> cvtSolverReductionStep step >>= (return . pp)
else return [pp $ "Only included with enough verbosity turned on"]
nrsteps <- getl $ gst ^* chrgstStatNrSolveSteps
let pextra | verbosity >= Verbosity_Normal =
"Residue" >-< indent 2 (vlist rs)
>-< "Wait" >-< indent 2 (vlist wvs)
>-< "Stats" >-< indent 2 (ppAssocLV [ ("Count of overall solve steps", pp nrsteps) ])
>-< "Steps" >-< indent 2 (vlist ss)
| otherwise = Pretty.empty
return $
"Subst" >-< indent 2 (s `varUpd` s)
>-< "Work" >-< indent 2 (vlist ws)
>-< pextra
runCHRMonoBacktrackPrioT
:: MonoBacktrackPrio cnstr guard bprio prio subst env m
=> CHRGlobState cnstr guard bprio prio subst env m
-> CHRBackState cnstr bprio subst env
-> CHRMonoBacktrackPrioT cnstr guard bprio prio subst env m (SolverResult subst)
-> m ([SolverResult subst], (CHRGlobState cnstr guard bprio prio subst env m, CHRBackState cnstr bprio subst env))
runCHRMonoBacktrackPrioT gs bs m = observeStateAllT (gs, bs ) m
{-# INLINABLE runCHRMonoBacktrackPrioT #-}
data FoundChr c g bp p
= FoundChr
{ foundChrInx :: {-# UNPACK #-} !CHRInx
, foundChrChr :: !(StoredCHR c g bp p)
, foundChrCnstr :: ![WorkInx]
}
data FoundWorkInx c g bp p
= FoundWorkInx
{ foundWorkInxInx :: {-# UNPACK #-} !CHRConstraintInx
, foundWorkInxChr :: !(StoredCHR c g bp p)
, foundWorkInxWorkInxs :: ![[WorkInx]]
}
data FoundMatchSortKey bp p s
= FoundMatchSortKey
{ foundMatchSortKeyPrio :: !(Maybe (s,p))
, foundMatchSortKeyWaitSize :: {-# UNPACK #-} !Int
, foundMatchSortKeyTextOrder :: {-# UNPACK #-} !CHRInx
}
instance Show (FoundMatchSortKey bp p s) where
show _ = "FoundMatchSortKey"
instance (PP p, PP s) => PP (FoundMatchSortKey bp p s) where
pp (FoundMatchSortKey {foundMatchSortKeyPrio=p, foundMatchSortKeyWaitSize=w, foundMatchSortKeyTextOrder=o}) = ppParensCommas [pp p, pp w, pp o]
compareFoundMatchSortKey :: ((s,p) -> (s,p) -> Ordering) -> FoundMatchSortKey bp p s -> FoundMatchSortKey bp p s -> Ordering
compareFoundMatchSortKey cmp_rp (FoundMatchSortKey rp1 ws1 to1) (FoundMatchSortKey rp2 ws2 to2) =
orderingLexic (rp1 `cmp_mbrp` rp2) $ orderingLexic (ws1 `compare` ws2) $ to1 `compare` to2
where
cmp_mbrp (Just rp1) (Just rp2) = cmp_rp rp1 rp2
cmp_mbrp (Just _ ) _ = GT
cmp_mbrp _ (Just _ ) = LT
cmp_mbrp _ _ = EQ
data FoundBodyAlt c bp
= FoundBodyAlt
{ foundBodyAltInx :: {-# UNPACK #-} !Int
, foundBodyAltBacktrackPrio :: !(CHRPrioEvaluatableVal bp)
, foundBodyAltAlt :: !(RuleBodyAlt c bp)
}
instance Show (FoundBodyAlt c bp) where
show _ = "FoundBodyAlt"
instance (PP c, PP bp, PP (CHRPrioEvaluatableVal bp)) => PP (FoundBodyAlt c bp) where
pp (FoundBodyAlt {foundBodyAltInx=i, foundBodyAltBacktrackPrio=bp, foundBodyAltAlt=a}) = i >|< ":" >|< ppParens bp >#< a
data FoundSlvMatch c g bp p s
= FoundSlvMatch
{ foundSlvMatchSubst :: !s
, foundSlvMatchFreeVars :: !(CHRWaitForVarSet s)
, foundSlvMatchWaitForVars :: !(CHRWaitForVarSet s)
, foundSlvMatchSortKey :: !(FoundMatchSortKey bp p s)
, foundSlvMatchBodyAlts :: ![FoundBodyAlt c bp]
}
instance Show (FoundSlvMatch c g bp p s) where
show _ = "FoundSlvMatch"
instance (PP s, PP p, PP c, PP bp, PP (VarLookupKey s), PP (CHRPrioEvaluatableVal bp)) => PP (FoundSlvMatch c g bp p s) where
pp (FoundSlvMatch {foundSlvMatchSubst=s, foundSlvMatchWaitForVars=ws, foundSlvMatchBodyAlts=as}) = ws >#< s >-< vlist as
data FoundWorkMatch c g bp p s
= FoundWorkMatch
{ foundWorkMatchInx :: {-# UNPACK #-} !CHRConstraintInx
, foundWorkMatchChr :: !(StoredCHR c g bp p)
, foundWorkMatchWorkInx :: ![WorkInx]
, foundWorkMatchSlvMatch :: !(Maybe (FoundSlvMatch c g bp p s))
}
instance Show (FoundWorkMatch c g bp p s) where
show _ = "FoundWorkMatch"
instance (PP c, PP bp, PP p, PP s, PP (VarLookupKey s), PP (CHRPrioEvaluatableVal bp)) => PP (FoundWorkMatch c g bp p s) where
pp (FoundWorkMatch {foundWorkMatchSlvMatch=sm}) = pp sm
data FoundWorkSortedMatch c g bp p s
= FoundWorkSortedMatch
{ foundWorkSortedMatchInx :: !CHRConstraintInx
, foundWorkSortedMatchChr :: !(StoredCHR c g bp p)
, foundWorkSortedMatchBodyAlts :: ![FoundBodyAlt c bp]
, foundWorkSortedMatchWorkInx :: ![WorkInx]
, foundWorkSortedMatchSubst :: !s
, foundWorkSortedMatchFreeVars :: !(CHRWaitForVarSet s)
, foundWorkSortedMatchWaitForVars :: !(CHRWaitForVarSet s)
}
instance Show (FoundWorkSortedMatch c g bp p s) where
show _ = "FoundWorkSortedMatch"
instance (PP c, PP bp, PP p, PP s, PP g, PP (VarLookupKey s), PP (CHRPrioEvaluatableVal bp)) => PP (FoundWorkSortedMatch c g bp p s) where
pp (FoundWorkSortedMatch {foundWorkSortedMatchBodyAlts=as, foundWorkSortedMatchWorkInx=wis, foundWorkSortedMatchSubst=s, foundWorkSortedMatchWaitForVars=wvs})
= wis >-< s >#< ppParens wvs >-< vlist as
data CHRSolveOpts
= CHRSolveOpts
{ chrslvOptSucceedOnLeftoverWork :: !Bool
, chrslvOptSucceedOnFailedSolve :: !Bool
, chrslvOptGatherDebugInfo :: !Bool
, chrslvOptGatherTraceInfo :: !Bool
}
defaultCHRSolveOpts :: CHRSolveOpts
defaultCHRSolveOpts
= CHRSolveOpts
{ chrslvOptSucceedOnLeftoverWork = False
, chrslvOptSucceedOnFailedSolve = False
, chrslvOptGatherDebugInfo = False
, chrslvOptGatherTraceInfo = False
}
{-# INLINABLE chrSolve #-}
chrSolve
:: forall c g bp p s e m .
( MonoBacktrackPrio c g bp p s e m
, PP s
) => CHRSolveOpts
-> e
-> CHRMonoBacktrackPrioT c g bp p s e m (SolverResult s)
chrSolve opts env = slv
where
dbg | chrslvOptGatherDebugInfo opts = \i -> bst ^* chrbstReductionSteps =$: (SolverReductionDBG i :)
| otherwise = \_ -> return ()
trc | chrslvOptGatherTraceInfo opts = \i -> gst ^* chrgstTrace =$: (i :)
| otherwise = \_ -> return ()
slv = do
gst ^* chrgstStatNrSolveSteps =$: (+1)
mbSlvWk <- splitWorkFromSolveQueue
case mbSlvWk of
Just (workInx) -> do
work <- lkupWork workInx
case work of
Work_Fail -> slvFail
_ -> do
subst <- getl $ bst ^* chrbstSolveSubst
let mbSlv = chrmatcherRun (chrBuiltinSolveM env $ workCnstr work) emptyCHRMatchEnv subst
dbg $
( "solve wk" >#< work
>-< "match" >#< mbSlv
)
case mbSlv of
Just (s,_) -> do
splitOffResolvedWaitForVarWork (Lk.keysSet s) >>= mapM_ addToWorkQueue
bst ^* chrbstSolveSubst =$: (s `Lk.apply`)
slv
_ | chrslvOptSucceedOnFailedSolve opts -> do
bst ^* chrbstResidualQueue =$: (workInx :)
slv
| otherwise -> do
slvFail
Nothing -> do
waitingWk <- waitingInWorkQueue
visitedChrWkCombis <- getl $ bst ^* chrbstMatchedCombis
mbWk <- splitFromWorkQueue
case mbWk of
Nothing -> do
wr <- getl $ bst ^* chrbstRuleWorkQueue ^* wkqueueRedo
if chrslvOptSucceedOnLeftoverWork opts || IntSet.null wr
then slvSucces $ IntSet.toList wr
else slvFail
Just workInx -> do
work <- lkupWork workInx
foundChrInxs <- slvLookup (workKey work ) (gst ^* chrgstStore ^* chrstoreTrie )
let foundChrGroupedInxs = Map.unionsWith Set.union $ map (\(CHRConstraintInx i j) -> Map.singleton i (Set.singleton j)) foundChrInxs
foundChrs <- forM (Map.toList foundChrGroupedInxs) $ \(chrInx,rlInxs) -> lkupChr chrInx >>= \chr -> return $ FoundChr chrInx chr $ Set.toList rlInxs
foundWorkInxs <- sequence
[ fmap (FoundWorkInx (CHRConstraintInx ci i) c) $ slvCandidate waitingWk visitedChrWkCombis workInx c i
| FoundChr ci c is <- foundChrs, i <- is
]
foundWorkMatches <- fmap concat $
forM foundWorkInxs $ \(FoundWorkInx ci c wis) -> do
forM wis $ \wi -> do
w <- forM wi lkupWork
fmap (FoundWorkMatch ci c wi) $ slvMatch env c (map workCnstr w) (chrciAt ci)
let foundWorkSortedMatches = sortByOn (compareFoundMatchSortKey $ chrPrioCompare env) fst
[ (k, FoundWorkSortedMatch (foundWorkMatchInx fwm) (foundWorkMatchChr fwm) (foundSlvMatchBodyAlts sm)
(foundWorkMatchWorkInx fwm) (foundSlvMatchSubst sm) (foundSlvMatchFreeVars sm) (foundSlvMatchWaitForVars sm))
| fwm@(FoundWorkMatch {foundWorkMatchSlvMatch = Just sm@(FoundSlvMatch {foundSlvMatchSortKey=k})}) <- foundWorkMatches
]
bprio <- getl $ bst ^* chrbstBacktrackPrio
subst <- getl $ bst ^* chrbstSolveSubst
dbgWaitInfo <- getl $ bst ^* chrbstWaitForVar
dbg $ "bprio" >#< bprio
>-< "wk" >#< (work >-< subst `varUpd` workCnstr work)
>-< "que" >#< ppBracketsCommas (IntSet.toList waitingWk)
>-< "subst" >#< subst
>-< "wait" >#< ppAssocL (assocLMapElt (ppAssocL . map (\i -> (_waitForVarWorkInx i, ppCommas $ Set.toList $ _waitForVarVars i))) $ Map.toList dbgWaitInfo)
>-< "visited" >#< ppBracketsCommas (Set.toList visitedChrWkCombis)
>-< "chrs" >#< vlist [ ci >|< ppParensCommas is >|< ":" >#< c | FoundChr ci c is <- foundChrs ]
>-< "works" >#< vlist [ ci >|< ":" >#< vlist (map ppBracketsCommas ws) | FoundWorkInx ci c ws <- foundWorkInxs ]
>-< "matches" >#< vlist [ ci >|< ":" >#< ppBracketsCommas wi >#< ":" >#< mbm | FoundWorkMatch ci _ wi mbm <- foundWorkMatches ]
case foundWorkSortedMatches of
((_,fwsm@(FoundWorkSortedMatch {foundWorkSortedMatchWaitForVars = waitForVars})):_)
| Set.null waitForVars -> do
addToWorkQueue workInx
slv1 bprio fwsm
| otherwise -> do
addWorkToWaitForVarQueue waitForVars workInx
slv
_ -> do
addRedoToWorkQueue workInx
slv
slv1 curbprio
(FoundWorkSortedMatch
{ foundWorkSortedMatchInx = CHRConstraintInx {chrciInx = ci}
, foundWorkSortedMatchChr = chr@StoredCHR {_storedChrRule = Rule {ruleSimpSz = simpSz}}
, foundWorkSortedMatchBodyAlts = alts
, foundWorkSortedMatchWorkInx = workInxs
, foundWorkSortedMatchSubst = matchSubst
, foundWorkSortedMatchFreeVars = freeHeadVars
}) = do
deleteFromWorkQueue $ IntSet.fromList $ take simpSz workInxs
case alts of
[] -> do
log Nothing
slv
[alt@(FoundBodyAlt {foundBodyAltBacktrackPrio=bprio})]
| curbprio == bprio -> do
log (Just alt)
nextwork bprio alt
| otherwise -> do
log (Just alt)
slvSchedule bprio $ nextwork bprio alt
slvScheduleRun
alts -> do
forM alts $ \alt@(FoundBodyAlt {foundBodyAltBacktrackPrio=bprio}) -> do
log (Just alt)
(backtrackWithRoll (\_ _ bs -> return bs) $ nextwork bprio alt) >>= slvSchedule bprio
slvScheduleRun
where
log alt = do
let a = (fmap (rbodyaltBody . foundBodyAltAlt) alt)
trc $ SolveStep chr matchSubst a [] []
nextwork bprio alt@(FoundBodyAlt {foundBodyAltAlt=(RuleBodyAlt {rbodyaltBody=body})}) = do
bst ^* chrbstBacktrackPrio =: bprio
freshSubst <- slvFreshSubst freeHeadVars body
newWkInxs <- forM body $ addConstraintAsWork . ((freshSubst `Lk.apply` matchSubst) `varUpd`)
let matchedCombi = MatchedCombi ci workInxs
bst ^* chrbstMatchedCombis =$: Set.insert matchedCombi
bst ^* chrbstReductionSteps =$: (SolverReductionStep matchedCombi (foundBodyAltInx alt) (Map.unionsWith (++) $ map (\(k,v) -> Map.singleton k [v]) $ newWkInxs) :)
slv
slvFreshSubst
:: forall c g bp p s e m x .
( MonoBacktrackPrio c g bp p s e m
, ExtrValVarKey x ~ ExtrValVarKey (VarLookupVal s)
, VarExtractable x
) => Set.Set (ExtrValVarKey x)
-> x
-> CHRMonoBacktrackPrioT c g bp p s e m s
slvFreshSubst except x =
fmap (foldr Lk.apply Lk.empty) $
forM (Set.toList $ varFreeSet x `Set.difference` except) $ \v ->
modifyAndGet (bst ^* chrbstFreshVar) (freshWith $ Just v) >>= \v' -> return $ (Lk.singleton v (varTermMkKey v') :: s)
{-# INLINE slvFreshSubst #-}
slvLookup
:: ( MonoBacktrackPrio c g bp p s e m
, Ord (TT.TrTrKey c)
) => CHRKey c
-> Lens (CHRGlobState c g bp p s e m, CHRBackState c bp s e) (TT.TreeTrie (TT.TrTrKey c) [x])
-> CHRMonoBacktrackPrioT c g bp p s e m [x]
slvLookup key t =
(getl t) >>= \t -> do
return $ concat $ TT.lookupResultToList $ TT.lookup key t
{-# INLINE slvLookup #-}
slvCandidate
:: forall c g bp p s e m
. ( MonoBacktrackPrio c g bp p s e m
) => WorkInxSet
-> Set.Set MatchedCombi
-> WorkInx
-> StoredCHR c g bp p
-> Int
-> CHRMonoBacktrackPrioT c g bp p s e m
( [[WorkInx]]
)
slvCandidate waitingWk alreadyMatchedCombis wi (StoredCHR {_storedHeadKeys = ks, _storedChrInx = ci}) headInx = do
let [ks1,_,ks2] = splitPlaces [headInx, headInx+1] ks
ws1 <- forM ks1 lkup
ws2 <- forM ks2 lkup
return $ filter (\wi -> all (`IntSet.member` waitingWk) wi
&& Set.notMember (MatchedCombi ci wi) alreadyMatchedCombis)
$ combineToDistinguishedEltsBy (==) $ ws1 ++ [[wi]] ++ ws2
where
lkup k = slvLookup k (bst ^* chrbstWorkStore ^* wkstoreTrie)
{-# INLINE slvCandidate #-}
slvMatch
:: forall c g bp p s env m
. ( MonoBacktrackPrio c g bp p s env m
, CHRMatchable env c s
, CHRCheckable env g s
, CHRMatchable env bp s
, CHRPrioEvaluatable env bp s
) => env
-> StoredCHR c g bp p
-> [c]
-> Int
-> CHRMonoBacktrackPrioT c g bp p s env m (Maybe (FoundSlvMatch c g bp p s))
slvMatch env chr@(StoredCHR {_storedChrRule = Rule {rulePrio = mbpr, ruleHead = hc, ruleGuard = gd, ruleBacktrackPrio = mbbpr, ruleBodyAlts = alts}}) cnstrs headInx = do
subst <- getl $ bst ^* chrbstSolveSubst
curbprio <- fmap (chrPrioLift (Proxy :: Proxy env) (Proxy :: Proxy s)) $ getl $ bst ^* chrbstBacktrackPrio
return $ fmap (\(s,ws) -> FoundSlvMatch s freevars ws (FoundMatchSortKey (fmap ((,) s) mbpr) (Set.size ws) (_storedChrInx chr))
[ FoundBodyAlt i bp a | (i,a) <- zip [0..] alts, let bp = maybe minBound (chrPrioEval env s) $ rbodyaltBacktrackPrio a
])
$ (\m -> chrmatcherRun m (emptyCHRMatchEnv {chrmatchenvMetaMayBind = (`Set.member` freevars)}) subst)
$ sequence_
$ prio curbprio ++ matches ++ checks
where
prio curbprio = maybe [] (\bpr -> [chrMatchToM env bpr curbprio]) mbbpr
matches = zipWith3 (\i h c -> chrMatchAndWaitToM (i == headInx) env h c) [0::Int ..] hc cnstrs
checks = map (chrCheckM env) gd
freevars = Set.unions [varFreeSet hc, maybe Set.empty varFreeSet mbbpr]
{-# INLINE slvMatch #-}