{-# LANGUAGE ConstraintKinds, ScopedTypeVariables, StandaloneDeriving, UndecidableInstances, NoMonomorphismRestriction, MultiParamTypeClasses, TemplateHaskell, FunctionalDependencies #-}

-------------------------------------------------------------------------------------------
--- CHR solver
-------------------------------------------------------------------------------------------

{-|
Under development (as of 20160218).

Solver is:
- Monomorphic, i.e. the solver is polymorph but therefore can only work on 1 type of constraints, rules, etc.
- Knows about variables for which substitutions can be found, substitutions are part of found solutions.
- Backtracking (on variable bindings/substitutions), multiple solution alternatives are explored.
- Found rules are applied in an order described by priorities associated with rules. Priorities can be dynamic, i.e. depend on terms in rules.

See

"A Flexible Search Framework for CHR", Leslie De Koninck, Tom Schrijvers, and Bart Demoen.
http://link.springer.com/10.1007/978-3-540-92243-8_2
-}

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.IO.Class
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

-------------------------------------------------------------------------------------------
--- Verbosity
-------------------------------------------------------------------------------------------

data Verbosity
  = Verbosity_Quiet         -- default
  | Verbosity_Normal
  | Verbosity_Debug
  | Verbosity_ALot
  deriving (Verbosity -> Verbosity -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Verbosity -> Verbosity -> Bool
$c/= :: Verbosity -> Verbosity -> Bool
== :: Verbosity -> Verbosity -> Bool
$c== :: Verbosity -> Verbosity -> Bool
Eq, Eq Verbosity
Verbosity -> Verbosity -> Bool
Verbosity -> Verbosity -> Ordering
Verbosity -> Verbosity -> Verbosity
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Verbosity -> Verbosity -> Verbosity
$cmin :: Verbosity -> Verbosity -> Verbosity
max :: Verbosity -> Verbosity -> Verbosity
$cmax :: Verbosity -> Verbosity -> Verbosity
>= :: Verbosity -> Verbosity -> Bool
$c>= :: Verbosity -> Verbosity -> Bool
> :: Verbosity -> Verbosity -> Bool
$c> :: Verbosity -> Verbosity -> Bool
<= :: Verbosity -> Verbosity -> Bool
$c<= :: Verbosity -> Verbosity -> Bool
< :: Verbosity -> Verbosity -> Bool
$c< :: Verbosity -> Verbosity -> Bool
compare :: Verbosity -> Verbosity -> Ordering
$ccompare :: Verbosity -> Verbosity -> Ordering
Ord, Int -> Verbosity -> ShowS
[Verbosity] -> ShowS
Verbosity -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Verbosity] -> ShowS
$cshowList :: [Verbosity] -> ShowS
show :: Verbosity -> String
$cshow :: Verbosity -> String
showsPrec :: Int -> Verbosity -> ShowS
$cshowsPrec :: Int -> Verbosity -> ShowS
Show, Int -> Verbosity
Verbosity -> Int
Verbosity -> [Verbosity]
Verbosity -> Verbosity
Verbosity -> Verbosity -> [Verbosity]
Verbosity -> Verbosity -> Verbosity -> [Verbosity]
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
enumFromThenTo :: Verbosity -> Verbosity -> Verbosity -> [Verbosity]
$cenumFromThenTo :: Verbosity -> Verbosity -> Verbosity -> [Verbosity]
enumFromTo :: Verbosity -> Verbosity -> [Verbosity]
$cenumFromTo :: Verbosity -> Verbosity -> [Verbosity]
enumFromThen :: Verbosity -> Verbosity -> [Verbosity]
$cenumFromThen :: Verbosity -> Verbosity -> [Verbosity]
enumFrom :: Verbosity -> [Verbosity]
$cenumFrom :: Verbosity -> [Verbosity]
fromEnum :: Verbosity -> Int
$cfromEnum :: Verbosity -> Int
toEnum :: Int -> Verbosity
$ctoEnum :: Int -> Verbosity
pred :: Verbosity -> Verbosity
$cpred :: Verbosity -> Verbosity
succ :: Verbosity -> Verbosity
$csucc :: Verbosity -> Verbosity
Enum, Typeable)

-------------------------------------------------------------------------------------------
--- A CHR as stored
-------------------------------------------------------------------------------------------

-- | Index into table of CHR's, allowing for indirection required for sharing of rules by search for different constraints in the head
type CHRInx = Int

-- | Index into rule and head constraint
data CHRConstraintInx =
  CHRConstraintInx 
    { CHRConstraintInx -> Int
chrciInx :: {-# UNPACK #-} !CHRInx
    , CHRConstraintInx -> Int
chrciAt  :: {-# UNPACK #-} !Int
    }
  deriving (CHRConstraintInx -> CHRConstraintInx -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: CHRConstraintInx -> CHRConstraintInx -> Bool
$c/= :: CHRConstraintInx -> CHRConstraintInx -> Bool
== :: CHRConstraintInx -> CHRConstraintInx -> Bool
$c== :: CHRConstraintInx -> CHRConstraintInx -> Bool
Eq, Eq CHRConstraintInx
CHRConstraintInx -> CHRConstraintInx -> Bool
CHRConstraintInx -> CHRConstraintInx -> Ordering
CHRConstraintInx -> CHRConstraintInx -> CHRConstraintInx
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: CHRConstraintInx -> CHRConstraintInx -> CHRConstraintInx
$cmin :: CHRConstraintInx -> CHRConstraintInx -> CHRConstraintInx
max :: CHRConstraintInx -> CHRConstraintInx -> CHRConstraintInx
$cmax :: CHRConstraintInx -> CHRConstraintInx -> CHRConstraintInx
>= :: CHRConstraintInx -> CHRConstraintInx -> Bool
$c>= :: CHRConstraintInx -> CHRConstraintInx -> Bool
> :: CHRConstraintInx -> CHRConstraintInx -> Bool
$c> :: CHRConstraintInx -> CHRConstraintInx -> Bool
<= :: CHRConstraintInx -> CHRConstraintInx -> Bool
$c<= :: CHRConstraintInx -> CHRConstraintInx -> Bool
< :: CHRConstraintInx -> CHRConstraintInx -> Bool
$c< :: CHRConstraintInx -> CHRConstraintInx -> Bool
compare :: CHRConstraintInx -> CHRConstraintInx -> Ordering
$ccompare :: CHRConstraintInx -> CHRConstraintInx -> Ordering
Ord, Int -> CHRConstraintInx -> ShowS
[CHRConstraintInx] -> ShowS
CHRConstraintInx -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [CHRConstraintInx] -> ShowS
$cshowList :: [CHRConstraintInx] -> ShowS
show :: CHRConstraintInx -> String
$cshow :: CHRConstraintInx -> String
showsPrec :: Int -> CHRConstraintInx -> ShowS
$cshowsPrec :: Int -> CHRConstraintInx -> ShowS
Show)

instance PP CHRConstraintInx where
  pp :: CHRConstraintInx -> PP_Doc
pp (CHRConstraintInx Int
i Int
j) = Int
i forall a b. (PP a, PP b) => a -> b -> PP_Doc
>|< String
"." forall a b. (PP a, PP b) => a -> b -> PP_Doc
>|< Int
j

-- | A CHR as stored in a CHRStore, requiring additional info for efficiency
data StoredCHR c g bp p
  = StoredCHR
      { forall c g bp p. StoredCHR c g bp p -> [CHRKey c]
_storedHeadKeys  :: ![CHRKey c]                        -- ^ the keys corresponding to the head of the rule
      , forall c g bp p. StoredCHR c g bp p -> Rule c g bp p
_storedChrRule   :: !(Rule c g bp p)                          -- ^ the rule
      , forall c g bp p. StoredCHR c g bp p -> Int
_storedChrInx    :: {-# UNPACK #-} !CHRInx                                -- ^ index of constraint for which is keyed into store
      }
  deriving (Typeable)
  
storedChrRule' :: StoredCHR c g bp p -> Rule c g bp p
storedChrRule' :: forall c g bp p. StoredCHR c g bp p -> Rule c g bp p
storedChrRule' = forall c g bp p. StoredCHR c g bp p -> Rule c g bp p
_storedChrRule

-- | A CHR store is a trie structure
data CHRStore cnstr guard bprio prio
  = CHRStore
      { forall cnstr guard bprio prio.
CHRStore cnstr guard bprio prio
-> TreeTrie (TrTrKey cnstr) [CHRConstraintInx]
_chrstoreTrie    :: TT.TreeTrie (TT.TrTrKey cnstr) [CHRConstraintInx]                       -- ^ map from the search key of a rule to the index into tabl
      , forall cnstr guard bprio prio.
CHRStore cnstr guard bprio prio
-> IntMap (StoredCHR cnstr guard bprio prio)
_chrstoreTable   :: IntMap.IntMap (StoredCHR cnstr guard bprio prio)      -- ^ (possibly multiple) rules for a key
      }
  deriving (Typeable)

emptyCHRStore :: TT.TTCtxt (TT.TrTrKey cnstr) => CHRStore cnstr guard bprio prio
emptyCHRStore :: forall cnstr guard bprio prio.
TTCtxt (TrTrKey cnstr) =>
CHRStore cnstr guard bprio prio
emptyCHRStore = forall cnstr guard bprio prio.
TreeTrie (TrTrKey cnstr) [CHRConstraintInx]
-> IntMap (StoredCHR cnstr guard bprio prio)
-> CHRStore cnstr guard bprio prio
CHRStore forall k v. TTCtxt k => TreeTrie k v
TT.empty forall a. IntMap a
IntMap.empty

-------------------------------------------------------------------------------------------
--- Store holding work, split up in global and backtrackable part
-------------------------------------------------------------------------------------------

type WorkInx = WorkTime

type WorkInxSet = IntSet.IntSet

data WorkStore cnstr
  = WorkStore
      { forall cnstr. WorkStore cnstr -> TreeTrie (TrTrKey cnstr) [Int]
_wkstoreTrie     :: !(TT.TreeTrie (TT.TrTrKey cnstr) [WorkInx])                -- ^ map from the search key of a constraint to index in table
      , forall cnstr. WorkStore cnstr -> IntMap (Work cnstr)
_wkstoreTable    :: !(IntMap.IntMap (Work cnstr))      -- ^ all the work ever entered. FIXME: do GC
      , forall cnstr. WorkStore cnstr -> Int
_wkstoreNextFreeWorkInx       :: {-# UNPACK #-} !WorkTime                                        -- ^ Next free work/constraint identification, used by solving to identify whether a rule has been used for a constraint.
      }
  deriving (Typeable)

emptyWorkStore :: TT.TTCtxt (TT.TrTrKey cnstr) => WorkStore cnstr
emptyWorkStore :: forall cnstr. TTCtxt (TrTrKey cnstr) => WorkStore cnstr
emptyWorkStore = forall cnstr.
TreeTrie (TrTrKey cnstr) [Int]
-> IntMap (Work cnstr) -> Int -> WorkStore cnstr
WorkStore forall k v. TTCtxt k => TreeTrie k v
TT.empty forall a. IntMap a
IntMap.empty Int
initWorkTime

data WorkQueue
  = WorkQueue
      { WorkQueue -> WorkInxSet
_wkqueueActive          :: !WorkInxSet                  -- ^ active queue, work will be taken off from this one
      , WorkQueue -> WorkInxSet
_wkqueueRedo            :: !WorkInxSet                  -- ^ redo queue, holding work which could not immediately be reduced, but later on might be
      , WorkQueue -> Bool
_wkqueueDidSomething    :: !Bool                        -- ^ flag indicating some work was done; if False and active queue is empty we stop solving
      }
  deriving (Typeable)

emptyWorkQueue :: WorkQueue
emptyWorkQueue :: WorkQueue
emptyWorkQueue = WorkInxSet -> WorkInxSet -> Bool -> WorkQueue
WorkQueue WorkInxSet
IntSet.empty WorkInxSet
IntSet.empty Bool
True

-------------------------------------------------------------------------------------------
--- A matched combi of chr and work
-------------------------------------------------------------------------------------------

-- | Already matched combi of chr and work
data MatchedCombi' c w =
  MatchedCombi
    { forall c w. MatchedCombi' c w -> c
mcCHR      :: !c              -- ^ the CHR
    , forall c w. MatchedCombi' c w -> [w]
mcWork     :: ![w]            -- ^ the work matched for this CHR
    }
  deriving (MatchedCombi' c w -> MatchedCombi' c w -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall c w.
(Eq c, Eq w) =>
MatchedCombi' c w -> MatchedCombi' c w -> Bool
/= :: MatchedCombi' c w -> MatchedCombi' c w -> Bool
$c/= :: forall c w.
(Eq c, Eq w) =>
MatchedCombi' c w -> MatchedCombi' c w -> Bool
== :: MatchedCombi' c w -> MatchedCombi' c w -> Bool
$c== :: forall c w.
(Eq c, Eq w) =>
MatchedCombi' c w -> MatchedCombi' c w -> Bool
Eq, MatchedCombi' c w -> MatchedCombi' c w -> Bool
MatchedCombi' c w -> MatchedCombi' c w -> Ordering
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall {c} {w}. (Ord c, Ord w) => Eq (MatchedCombi' c w)
forall c w.
(Ord c, Ord w) =>
MatchedCombi' c w -> MatchedCombi' c w -> Bool
forall c w.
(Ord c, Ord w) =>
MatchedCombi' c w -> MatchedCombi' c w -> Ordering
forall c w.
(Ord c, Ord w) =>
MatchedCombi' c w -> MatchedCombi' c w -> MatchedCombi' c w
min :: MatchedCombi' c w -> MatchedCombi' c w -> MatchedCombi' c w
$cmin :: forall c w.
(Ord c, Ord w) =>
MatchedCombi' c w -> MatchedCombi' c w -> MatchedCombi' c w
max :: MatchedCombi' c w -> MatchedCombi' c w -> MatchedCombi' c w
$cmax :: forall c w.
(Ord c, Ord w) =>
MatchedCombi' c w -> MatchedCombi' c w -> MatchedCombi' c w
>= :: MatchedCombi' c w -> MatchedCombi' c w -> Bool
$c>= :: forall c w.
(Ord c, Ord w) =>
MatchedCombi' c w -> MatchedCombi' c w -> Bool
> :: MatchedCombi' c w -> MatchedCombi' c w -> Bool
$c> :: forall c w.
(Ord c, Ord w) =>
MatchedCombi' c w -> MatchedCombi' c w -> Bool
<= :: MatchedCombi' c w -> MatchedCombi' c w -> Bool
$c<= :: forall c w.
(Ord c, Ord w) =>
MatchedCombi' c w -> MatchedCombi' c w -> Bool
< :: MatchedCombi' c w -> MatchedCombi' c w -> Bool
$c< :: forall c w.
(Ord c, Ord w) =>
MatchedCombi' c w -> MatchedCombi' c w -> Bool
compare :: MatchedCombi' c w -> MatchedCombi' c w -> Ordering
$ccompare :: forall c w.
(Ord c, Ord w) =>
MatchedCombi' c w -> MatchedCombi' c w -> Ordering
Ord)

instance Show (MatchedCombi' c w) where
  show :: MatchedCombi' c w -> String
show MatchedCombi' c w
_ = String
"MatchedCombi"

instance (PP c, PP w) => PP (MatchedCombi' c w) where
  pp :: MatchedCombi' c w -> PP_Doc
pp (MatchedCombi c
c [w]
ws) = forall a. PP a => [a] -> PP_Doc
ppParensCommas [forall a. PP a => a -> PP_Doc
pp c
c, forall a. PP a => [a] -> PP_Doc
ppBracketsCommas [w]
ws]

type MatchedCombi = MatchedCombi' CHRInx WorkInx

-------------------------------------------------------------------------------------------
--- Solver reduction step
-------------------------------------------------------------------------------------------

-- | Description of 1 chr reduction step taken by the solver
data SolverReductionStep' c w
  = SolverReductionStep
      { forall c w. SolverReductionStep' c w -> MatchedCombi' c w
slvredMatchedCombi        :: !(MatchedCombi' c w)
      , forall c w. SolverReductionStep' c w -> Int
slvredChosenBodyAltInx    :: {-# UNPACK #-} !Int
      , forall c w. SolverReductionStep' c w -> Map ConstraintSolvesVia [w]
slvredNewWork             :: !(Map.Map ConstraintSolvesVia [w])
      }
  | SolverReductionDBG PP_Doc

type SolverReductionStep = SolverReductionStep' CHRInx WorkInx

instance Show (SolverReductionStep' c w) where
  show :: SolverReductionStep' c w -> String
show SolverReductionStep' c w
_ = String
"SolverReductionStep"

instance {-# OVERLAPPABLE #-} (PP c, PP w) => PP (SolverReductionStep' c w) where
  pp :: SolverReductionStep' c w -> PP_Doc
pp (SolverReductionStep (MatchedCombi c
ci [w]
ws) Int
a Map ConstraintSolvesVia [w]
wns) = String
"STEP" forall a b. (PP a, PP b) => a -> b -> PP_Doc
>#< c
ci forall a b. (PP a, PP b) => a -> b -> PP_Doc
>|< String
"." forall a b. (PP a, PP b) => a -> b -> PP_Doc
>|< Int
a forall a b. (PP a, PP b) => a -> b -> PP_Doc
>-< forall a. PP a => Int -> a -> PP_Doc
indent Int
2 (String
"+" forall a b. (PP a, PP b) => a -> b -> PP_Doc
>#< forall a. PP a => [a] -> PP_Doc
ppBracketsCommas [w]
ws forall a b. (PP a, PP b) => a -> b -> PP_Doc
>-< String
"-> (new)" forall a b. (PP a, PP b) => a -> b -> PP_Doc
>#< (forall k v. (PP k, PP v) => AssocL k v -> PP_Doc
ppAssocL forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [(k, a)]
Map.toList forall a b. (a -> b) -> a -> b
$ forall a b k. (a -> b) -> Map k a -> Map k b
Map.map forall a. PP a => [a] -> PP_Doc
ppBracketsCommas Map ConstraintSolvesVia [w]
wns)) -- (ppBracketsCommas wns >-< ppBracketsCommas wnbs)
  pp (SolverReductionDBG PP_Doc
p) = String
"DBG" forall a b. (PP a, PP b) => a -> b -> PP_Doc
>#< PP_Doc
p

instance (PP w) => PP (SolverReductionStep' Int w) where
  pp :: SolverReductionStep' Int w -> PP_Doc
pp (SolverReductionStep (MatchedCombi Int
ci [w]
ws) Int
a Map ConstraintSolvesVia [w]
wns) = Int
ci forall a b. (PP a, PP b) => a -> b -> PP_Doc
>|< String
"." forall a b. (PP a, PP b) => a -> b -> PP_Doc
>|< Int
a forall a b. (PP a, PP b) => a -> b -> PP_Doc
>#< String
"+" forall a b. (PP a, PP b) => a -> b -> PP_Doc
>#< forall a. PP a => [a] -> PP_Doc
ppBracketsCommas [w]
ws forall a b. (PP a, PP b) => a -> b -> PP_Doc
>#< String
"-> (new)" forall a b. (PP a, PP b) => a -> b -> PP_Doc
>#< (forall k v. (PP k, PP v) => AssocL k v -> PP_Doc
ppAssocL forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [(k, a)]
Map.toList forall a b. (a -> b) -> a -> b
$ forall a b k. (a -> b) -> Map k a -> Map k b
Map.map forall a. PP a => [a] -> PP_Doc
ppBracketsCommas Map ConstraintSolvesVia [w]
wns) -- (ppBracketsCommas wns >-< ppBracketsCommas wnbs)
  pp (SolverReductionDBG PP_Doc
p) = String
"DBG" forall a b. (PP a, PP b) => a -> b -> PP_Doc
>#< PP_Doc
p

-------------------------------------------------------------------------------------------
--- Waiting (for var resolution) work
-------------------------------------------------------------------------------------------

-- | Admin for waiting work
data WaitForVar s
  = WaitForVar
      { forall s. WaitForVar s -> CHRWaitForVarSet s
_waitForVarVars      :: !(CHRWaitForVarSet s)
      , forall s. WaitForVar s -> Int
_waitForVarWorkInx   :: {-# UNPACK #-} !WorkInx
      }
  deriving (Typeable)

-- | Index into collection of 'WaitForVar'
type WaitInx = Int

-------------------------------------------------------------------------------------------
--- The CHR monad, state, etc. Used to interact with store and solver
-------------------------------------------------------------------------------------------

-- | Global state
data CHRGlobState cnstr guard bprio prio subst env m
  = CHRGlobState
      { forall cnstr guard bprio prio subst env (m :: * -> *).
CHRGlobState cnstr guard bprio prio subst env m
-> CHRStore cnstr guard bprio prio
_chrgstStore                 :: !(CHRStore cnstr guard bprio prio)                     -- ^ Actual database of rules, to be searched
      , forall cnstr guard bprio prio subst env (m :: * -> *).
CHRGlobState cnstr guard bprio prio subst env m -> Int
_chrgstNextFreeRuleInx       :: {-# UNPACK #-} !CHRInx                                          -- ^ Next free rule identification, used by solving to identify whether a rule has been used for a constraint.
                                                                                         --   The numbering is applied to constraints inside a rule which can be matched.
      , forall cnstr guard bprio prio subst env (m :: * -> *).
CHRGlobState cnstr guard bprio prio subst env m
-> MinPQueue
     (CHRPrioEvaluatableVal bprio)
     (CHRMonoBacktrackPrioT
        cnstr guard bprio prio subst env m (SolverResult subst))
_chrgstScheduleQueue         :: !(Que.MinPQueue (CHRPrioEvaluatableVal bprio) (CHRMonoBacktrackPrioT cnstr guard bprio prio subst env m (SolverResult subst)))
      , forall cnstr guard bprio prio subst env (m :: * -> *).
CHRGlobState cnstr guard bprio prio subst env m
-> SolveTrace' cnstr (StoredCHR cnstr guard bprio prio) subst
_chrgstTrace                 :: !(SolveTrace' cnstr (StoredCHR cnstr guard bprio prio) subst)
      , forall cnstr guard bprio prio subst env (m :: * -> *).
CHRGlobState cnstr guard bprio prio subst env m -> Int
_chrgstStatNrSolveSteps      :: {-# UNPACK #-} !Int
      , forall cnstr guard bprio prio subst env (m :: * -> *).
CHRGlobState cnstr guard bprio prio subst env m -> VarToNmMp
_chrgstVarToNmMp             :: !VarToNmMp
      }
  deriving (Typeable)

emptyCHRGlobState :: TT.TTCtxt (TT.TrTrKey c) => CHRGlobState c g b p s e m
emptyCHRGlobState :: forall c g b p s e (m :: * -> *).
TTCtxt (TrTrKey c) =>
CHRGlobState c g b p s e m
emptyCHRGlobState = forall cnstr guard bprio prio subst env (m :: * -> *).
CHRStore cnstr guard bprio prio
-> Int
-> MinPQueue
     (CHRPrioEvaluatableVal bprio)
     (CHRMonoBacktrackPrioT
        cnstr guard bprio prio subst env m (SolverResult subst))
-> SolveTrace' cnstr (StoredCHR cnstr guard bprio prio) subst
-> Int
-> VarToNmMp
-> CHRGlobState cnstr guard bprio prio subst env m
CHRGlobState forall cnstr guard bprio prio.
TTCtxt (TrTrKey cnstr) =>
CHRStore cnstr guard bprio prio
emptyCHRStore Int
0 forall k a. MinPQueue k a
Que.empty forall c r s. SolveTrace' c r s
emptySolveTrace Int
0 VarToNmMp
emptyVarToNmMp

-- | Backtrackable state
data CHRBackState cnstr bprio subst env
  = CHRBackState
      { forall cnstr bprio subst env.
CHRBackState cnstr bprio subst env -> CHRPrioEvaluatableVal bprio
_chrbstBacktrackPrio         :: !(CHRPrioEvaluatableVal bprio)                          -- ^ the current backtrack prio the solver runs on
      
      , forall cnstr bprio subst env.
CHRBackState cnstr bprio subst env -> WorkQueue
_chrbstRuleWorkQueue         :: !WorkQueue                                              -- ^ work queue for rule matching
      , forall cnstr bprio subst env.
CHRBackState cnstr bprio subst env -> WorkQueue
_chrbstSolveQueue            :: !WorkQueue                                              -- ^ solve queue, constraints which are not solved by rule matching but with some domain specific solver, yielding variable subst constributing to backtrackable bindings
      , forall cnstr bprio subst env.
CHRBackState cnstr bprio subst env -> [Int]
_chrbstResidualQueue         :: [WorkInx]                                               -- ^ residual queue, constraints which are residual, no need to solve, etc
      , forall cnstr bprio subst env.
CHRBackState cnstr bprio subst env -> WorkStore cnstr
_chrbstWorkStore             :: !(WorkStore cnstr)                               -- ^ Actual database of solvable constraints
      
      , forall cnstr bprio subst env.
CHRBackState cnstr bprio subst env -> Set MatchedCombi
_chrbstMatchedCombis         :: !(Set.Set MatchedCombi)                                 -- ^ all combis of chr + work which were reduced, to prevent this from happening a second time (when propagating)
      
      , forall cnstr bprio subst env.
CHRBackState cnstr bprio subst env -> Int
_chrbstFreshVar              :: {-# UNPACK #-} !Int                                                    -- ^ for fresh var
      , forall cnstr bprio subst env.
CHRBackState cnstr bprio subst env -> subst
_chrbstSolveSubst            :: !subst                                                  -- ^ subst for variable bindings found during solving, not for the ones binding rule metavars during matching but for the user ones (in to be solved constraints)
      , forall cnstr bprio subst env.
CHRBackState cnstr bprio subst env
-> Map (VarLookupKey subst) [WaitForVar subst]
_chrbstWaitForVar            :: !(Map.Map (VarLookupKey subst) [WaitForVar subst])       -- ^ work waiting for a var to be bound
      
      , forall cnstr bprio subst env.
CHRBackState cnstr bprio subst env -> [SolverReductionStep]
_chrbstReductionSteps        :: ![SolverReductionStep]                                   -- ^ trace of reduction steps taken (excluding solve steps)
      }
  deriving (Typeable)

emptyCHRBackState :: (TT.TTCtxt (TT.TrTrKey c), CHREmptySubstitution s, Bounded (CHRPrioEvaluatableVal bp)) => CHRBackState c bp s e
emptyCHRBackState :: forall c s bp e.
(TTCtxt (TrTrKey c), CHREmptySubstitution s,
 Bounded (CHRPrioEvaluatableVal bp)) =>
CHRBackState c bp s e
emptyCHRBackState = forall cnstr bprio subst env.
CHRPrioEvaluatableVal bprio
-> WorkQueue
-> WorkQueue
-> [Int]
-> WorkStore cnstr
-> Set MatchedCombi
-> Int
-> subst
-> Map (VarLookupKey subst) [WaitForVar subst]
-> [SolverReductionStep]
-> CHRBackState cnstr bprio subst env
CHRBackState forall a. Bounded a => a
minBound WorkQueue
emptyWorkQueue WorkQueue
emptyWorkQueue [] forall cnstr. TTCtxt (TrTrKey cnstr) => WorkStore cnstr
emptyWorkStore forall a. Set a
Set.empty Int
0 forall subst. CHREmptySubstitution subst => subst
chrEmptySubst forall k a. Map k a
Map.empty []

-- | Monad for CHR, taking from 'LogicStateT' the state and backtracking behavior
type CHRMonoBacktrackPrioT cnstr guard bprio prio subst env m
  = LogicStateT (CHRGlobState cnstr guard bprio prio subst env m) (CHRBackState cnstr bprio subst env) m

-- | Full state as returned and used by running 'CHRMonoBacktrackPrioT'
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 :: forall cnstr guard bprio prio subst env (m :: * -> *).
Lens
  (CHRFullState cnstr guard bprio prio subst env m)
  (CHRGlobState cnstr guard bprio prio subst env m)
gst = forall a b. Lens (a, b) a
fstl
{-# INLINE gst #-}

bst :: Lens (CHRFullState cnstr guard bprio prio subst env m) (CHRBackState cnstr bprio subst env)
bst :: forall cnstr guard bprio prio subst env (m :: * -> *).
Lens
  (CHRFullState cnstr guard bprio prio subst env m)
  (CHRBackState cnstr bprio subst env)
bst = forall a b. Lens (a, b) b
sndl
{-# INLINE bst #-}

-- | All required behavior, as alias
type MonoBacktrackPrio cnstr guard bprio prio subst env m
    = ( IsCHRSolvable env cnstr guard bprio prio subst
      , Monad m
      -- TODO: replace MonadIO with API abstracting away access to persistent structures
      -- , MonadIO m
      , Lookup subst (VarLookupKey subst) (VarLookupVal subst)
      , LookupApply subst subst
      , Fresh Int (ExtrValVarKey (VarLookupVal subst))
      , ExtrValVarKey (VarLookupVal subst) ~ VarLookupKey subst
      , VarTerm (VarLookupVal subst)
      )

-------------------------------------------------------------------------------------------
--- Solver result
-------------------------------------------------------------------------------------------

-- | Solver solution
data SolverResult subst =
  SolverResult
    { forall subst. SolverResult subst -> subst
slvresSubst                 :: !subst                            -- ^ global found variable bindings
    , forall subst. SolverResult subst -> [Int]
slvresResidualCnstr         :: ![WorkInx]                        -- ^ constraints which are residual, no need to solve, etc, leftover when ready, taken from backtrack state
    , forall subst. SolverResult subst -> [Int]
slvresWorkCnstr             :: ![WorkInx]                        -- ^ constraints which are still unsolved, taken from backtrack state
    , forall subst. SolverResult subst -> [Int]
slvresWaitVarCnstr          :: ![WorkInx]                        -- ^ constraints which are still unsolved, waiting for variable resolution
    , forall subst. SolverResult subst -> [SolverReductionStep]
slvresReductionSteps        :: ![SolverReductionStep]            -- ^ how did we get to the result (taken from the backtrack state when a result is given back)
    }

-------------------------------------------------------------------------------------------
--- Solver: required instances
-------------------------------------------------------------------------------------------

-- | Alias API for solving requirements
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)
      ) 

-------------------------------------------------------------------------------------------
--- Lens construction
-------------------------------------------------------------------------------------------

mkLabel ''WaitForVar
mkLabel ''StoredCHR
mkLabel ''CHRStore
mkLabel ''WorkStore
mkLabel ''WorkQueue
mkLabel ''CHRGlobState
mkLabel ''CHRBackState

-------------------------------------------------------------------------------------------
--- Misc utils
-------------------------------------------------------------------------------------------

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 :: forall c g bp p s e (m :: * -> *).
(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 = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall r c s. (PP r, PP c) => SolveTrace' c r s -> PP_Doc
ppSolveTrace forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> [a]
reverse) forall a b. (a -> b) -> a -> b
$ forall f (m :: * -> *) o. MonadState f m => (f :-> o) -> m o
getl forall a b. (a -> b) -> a -> b
$ forall cnstr guard bprio prio subst env (m :: * -> *).
Lens
  (CHRFullState cnstr guard bprio prio subst env m)
  (CHRGlobState cnstr guard bprio prio subst env m)
gst forall a b c. (a :-> b) -> (b :-> c) -> a :-> c
^* forall cnstr guard bprio prio subst env (m :: * -> *).
Lens'
  (CHRGlobState cnstr guard bprio prio subst env m)
  (SolveTrace' cnstr (StoredCHR cnstr guard bprio prio) subst)
chrgstTrace

-------------------------------------------------------------------------------------------
--- CHR store, API for adding rules
-------------------------------------------------------------------------------------------

instance Show (StoredCHR c g bp p) where
  show :: StoredCHR c g bp p -> String
show StoredCHR c g bp p
_ = String
"StoredCHR"

ppStoredCHR :: (PP (TT.TrTrKey c), PP c, PP g, PP bp, PP p) => StoredCHR c g bp p -> PP_Doc
ppStoredCHR :: forall c g bp p.
(PP (TrTrKey c), PP c, PP g, PP bp, PP p) =>
StoredCHR c g bp p -> PP_Doc
ppStoredCHR c :: StoredCHR c g bp p
c@(StoredCHR {})
  = forall a. PP a => [a] -> PP_Doc
ppParensCommas (forall c g bp p. StoredCHR c g bp p -> [CHRKey c]
_storedHeadKeys StoredCHR c g bp p
c)
    forall a b. (PP a, PP b) => a -> b -> PP_Doc
>-< forall c g bp p. StoredCHR c g bp p -> Rule c g bp p
_storedChrRule StoredCHR c g bp p
c
    forall a b. (PP a, PP b) => a -> b -> PP_Doc
>-< forall a. PP a => Int -> a -> PP_Doc
indent Int
2
          (forall a. PP a => [a] -> PP_Doc
ppParensCommas
            [ forall a. PP a => a -> PP_Doc
pp forall a b. (a -> b) -> a -> b
$ forall c g bp p. StoredCHR c g bp p -> Int
_storedChrInx StoredCHR c g bp p
c
            -- , pp $ storedSimpSz c
            -- , "keys" >#< (ppBracketsCommas $ map (maybe (pp "?") ppTreeTrieKey) $ storedKeys c)
            -- , "ident" >#< ppParensCommas [ppTreeTrieKey idKey,pp idSeqNr]
            ])

instance (PP (TT.TrTrKey c), PP c, PP g, PP bp, PP p) => PP (StoredCHR c g bp p) where
  pp :: StoredCHR c g bp p -> PP_Doc
pp = forall c g bp p.
(PP (TrTrKey c), PP c, PP g, PP bp, PP p) =>
StoredCHR c g bp p -> PP_Doc
ppStoredCHR

-- | Add a rule as a CHR
addRule :: MonoBacktrackPrio c g bp p s e m => Rule c g bp p -> CHRMonoBacktrackPrioT c g bp p s e m ()
addRule :: forall c g bp p s e (m :: * -> *).
MonoBacktrackPrio c g bp p s e m =>
Rule c g bp p -> CHRMonoBacktrackPrioT c g bp p s e m ()
addRule Rule c g bp p
chr = do
    Int
i <- forall f (m :: * -> *) o a.
MonadState f m =>
(f :-> o) -> (o -> (a, o)) -> m a
modifyAndGet (forall cnstr guard bprio prio subst env (m :: * -> *).
Lens
  (CHRFullState cnstr guard bprio prio subst env m)
  (CHRGlobState cnstr guard bprio prio subst env m)
gst forall a b c. (a :-> b) -> (b :-> c) -> a :-> c
^* forall cnstr guard bprio prio subst env (m :: * -> *).
Lens' (CHRGlobState cnstr guard bprio prio subst env m) Int
chrgstNextFreeRuleInx) forall a b. (a -> b) -> a -> b
$ \Int
i -> (Int
i, Int
i forall a. Num a => a -> a -> a
+ Int
1)
    let ks :: [Key (TrTrKey c)]
ks = forall a b. (a -> b) -> [a] -> [b]
map forall x. TreeTrieKeyable x => x -> Key (TrTrKey x)
TT.toTreeTrieKey forall a b. (a -> b) -> a -> b
$ forall cnstr guard bprio prio.
Rule cnstr guard bprio prio -> [cnstr]
ruleHead Rule c g bp p
chr
    forall cnstr guard bprio prio subst env (m :: * -> *).
Lens
  (CHRFullState cnstr guard bprio prio subst env m)
  (CHRGlobState cnstr guard bprio prio subst env m)
gst forall a b c. (a :-> b) -> (b :-> c) -> a :-> c
^* forall cnstr guard bprio prio subst env (m :: * -> *).
Lens'
  (CHRGlobState cnstr guard bprio prio subst env m)
  (CHRStore cnstr guard bprio prio)
chrgstStore forall a b c. (a :-> b) -> (b :-> c) -> a :-> c
^* forall cnstr guard bprio prio guard bprio prio.
Lens
  (CHRStore cnstr guard bprio prio)
  (CHRStore cnstr guard bprio prio)
  (IntMap (StoredCHR cnstr guard bprio prio))
  (IntMap (StoredCHR cnstr guard bprio prio))
chrstoreTable forall f (m :: * -> *) o.
MonadState f m =>
(f :-> o) -> (o -> o) -> m ()
=$: forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
i (forall c g bp p.
[CHRKey c] -> Rule c g bp p -> Int -> StoredCHR c g bp p
StoredCHR [Key (TrTrKey c)]
ks Rule c g bp p
chr Int
i)
    forall cnstr guard bprio prio subst env (m :: * -> *).
Lens
  (CHRFullState cnstr guard bprio prio subst env m)
  (CHRGlobState cnstr guard bprio prio subst env m)
gst forall a b c. (a :-> b) -> (b :-> c) -> a :-> c
^* forall cnstr guard bprio prio subst env (m :: * -> *).
Lens'
  (CHRGlobState cnstr guard bprio prio subst env m)
  (CHRStore cnstr guard bprio prio)
chrgstStore forall a b c. (a :-> b) -> (b :-> c) -> a :-> c
^* forall cnstr guard bprio prio.
Lens'
  (CHRStore cnstr guard bprio prio)
  (TreeTrie (TrTrKey cnstr) [CHRConstraintInx])
chrstoreTrie forall f (m :: * -> *) o.
MonadState f m =>
(f :-> o) -> (o -> o) -> m ()
=$: \TreeTrie (TrTrKey c) [CHRConstraintInx]
t ->
      forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (forall k v.
Ord k =>
(v -> v -> v) -> TreeTrie k v -> TreeTrie k v -> TreeTrie k v
TT.unionWith forall a. [a] -> [a] -> [a]
(++)) TreeTrie (TrTrKey c) [CHRConstraintInx]
t [ forall k v. Ord k => Key k -> v -> TreeTrie k v
TT.singleton Key (TrTrKey c)
k [Int -> Int -> CHRConstraintInx
CHRConstraintInx Int
i Int
j] | (Key (TrTrKey c)
k,c
c,Int
j) <- forall a b c. [a] -> [b] -> [c] -> [(a, b, c)]
zip3 [Key (TrTrKey c)]
ks (forall cnstr guard bprio prio.
Rule cnstr guard bprio prio -> [cnstr]
ruleHead Rule c g bp p
chr) [Int
0..] ]
    forall (m :: * -> *) a. Monad m => a -> m a
return ()


-- | Add work to the rule work queue
addToWorkQueue :: MonoBacktrackPrio c g bp p s e m => WorkInx -> CHRMonoBacktrackPrioT c g bp p s e m ()
addToWorkQueue :: forall c g bp p s e (m :: * -> *).
MonoBacktrackPrio c g bp p s e m =>
Int -> CHRMonoBacktrackPrioT c g bp p s e m ()
addToWorkQueue Int
i = do
    forall cnstr guard bprio prio subst env (m :: * -> *).
Lens
  (CHRFullState cnstr guard bprio prio subst env m)
  (CHRBackState cnstr bprio subst env)
bst forall a b c. (a :-> b) -> (b :-> c) -> a :-> c
^* forall cnstr bprio subst env env.
Lens
  (CHRBackState cnstr bprio subst env)
  (CHRBackState cnstr bprio subst env)
  WorkQueue
  WorkQueue
chrbstRuleWorkQueue forall a b c. (a :-> b) -> (b :-> c) -> a :-> c
^* Lens' WorkQueue WorkInxSet
wkqueueActive forall f (m :: * -> *) o.
MonadState f m =>
(f :-> o) -> (o -> o) -> m ()
=$: (Int -> WorkInxSet -> WorkInxSet
IntSet.insert Int
i)
    forall cnstr guard bprio prio subst env (m :: * -> *).
Lens
  (CHRFullState cnstr guard bprio prio subst env m)
  (CHRBackState cnstr bprio subst env)
bst forall a b c. (a :-> b) -> (b :-> c) -> a :-> c
^* forall cnstr bprio subst env env.
Lens
  (CHRBackState cnstr bprio subst env)
  (CHRBackState cnstr bprio subst env)
  WorkQueue
  WorkQueue
chrbstRuleWorkQueue forall a b c. (a :-> b) -> (b :-> c) -> a :-> c
^* Lens' WorkQueue Bool
wkqueueDidSomething forall f (m :: * -> *) o. MonadState f m => (f :-> o) -> o -> m ()
=: Bool
True
{-# INLINE addToWorkQueue #-}

-- | Add redo work to the rule work queue
addRedoToWorkQueue :: MonoBacktrackPrio c g bp p s e m => WorkInx -> CHRMonoBacktrackPrioT c g bp p s e m ()
addRedoToWorkQueue :: forall c g bp p s e (m :: * -> *).
MonoBacktrackPrio c g bp p s e m =>
Int -> CHRMonoBacktrackPrioT c g bp p s e m ()
addRedoToWorkQueue Int
i = do
    forall cnstr guard bprio prio subst env (m :: * -> *).
Lens
  (CHRFullState cnstr guard bprio prio subst env m)
  (CHRBackState cnstr bprio subst env)
bst forall a b c. (a :-> b) -> (b :-> c) -> a :-> c
^* forall cnstr bprio subst env env.
Lens
  (CHRBackState cnstr bprio subst env)
  (CHRBackState cnstr bprio subst env)
  WorkQueue
  WorkQueue
chrbstRuleWorkQueue forall a b c. (a :-> b) -> (b :-> c) -> a :-> c
^* Lens' WorkQueue WorkInxSet
wkqueueRedo forall f (m :: * -> *) o.
MonadState f m =>
(f :-> o) -> (o -> o) -> m ()
=$: (Int -> WorkInxSet -> WorkInxSet
IntSet.insert Int
i)
{-# INLINE addRedoToWorkQueue #-}

-- | Add work to the wait for var queue
addWorkToWaitForVarQueue :: (MonoBacktrackPrio c g bp p s e m, Ord (VarLookupKey s)) => CHRWaitForVarSet s -> WorkInx -> CHRMonoBacktrackPrioT c g bp p s e m ()
addWorkToWaitForVarQueue :: forall c g bp p s e (m :: * -> *).
(MonoBacktrackPrio c g bp p s e m, Ord (VarLookupKey s)) =>
CHRWaitForVarSet s
-> Int -> CHRMonoBacktrackPrioT c g bp p s e m ()
addWorkToWaitForVarQueue CHRWaitForVarSet s
wfvs Int
wi = do
    let w :: WaitForVar s
w = forall s. CHRWaitForVarSet s -> Int -> WaitForVar s
WaitForVar CHRWaitForVarSet s
wfvs Int
wi
    forall cnstr guard bprio prio subst env (m :: * -> *).
Lens
  (CHRFullState cnstr guard bprio prio subst env m)
  (CHRBackState cnstr bprio subst env)
bst forall a b c. (a :-> b) -> (b :-> c) -> a :-> c
^* forall cnstr bprio subst env env.
Lens
  (CHRBackState cnstr bprio subst env)
  (CHRBackState cnstr bprio subst env)
  (Map (VarLookupKey subst) [WaitForVar subst])
  (Map (VarLookupKey subst) [WaitForVar subst])
chrbstWaitForVar forall f (m :: * -> *) o.
MonadState f m =>
(f :-> o) -> (o -> o) -> m ()
=$: forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith forall a. [a] -> [a] -> [a]
(++) (forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(ExtrValVarKey bp
v,[WaitForVar s
w]) | ExtrValVarKey bp
v <- forall a. Set a -> [a]
Set.toList CHRWaitForVarSet s
wfvs])

-- | For (new) found subst split off work waiting for it
splitOffResolvedWaitForVarWork :: (MonoBacktrackPrio c g bp p s e m, Ord (VarLookupKey s)) => CHRWaitForVarSet s -> CHRMonoBacktrackPrioT c g bp p s e m [WorkInx]
splitOffResolvedWaitForVarWork :: forall c g bp p s e (m :: * -> *).
(MonoBacktrackPrio c g bp p s e m, Ord (VarLookupKey s)) =>
CHRWaitForVarSet s -> CHRMonoBacktrackPrioT c g bp p s e m [Int]
splitOffResolvedWaitForVarWork CHRWaitForVarSet s
vars = do
    -- wait admin
    Map (ExtrValVarKey bp) [WaitForVar s]
wm <- forall f (m :: * -> *) o. MonadState f m => (f :-> o) -> m o
getl forall a b. (a -> b) -> a -> b
$ forall cnstr guard bprio prio subst env (m :: * -> *).
Lens
  (CHRFullState cnstr guard bprio prio subst env m)
  (CHRBackState cnstr bprio subst env)
bst forall a b c. (a :-> b) -> (b :-> c) -> a :-> c
^* forall cnstr bprio subst env env.
Lens
  (CHRBackState cnstr bprio subst env)
  (CHRBackState cnstr bprio subst env)
  (Map (VarLookupKey subst) [WaitForVar subst])
  (Map (VarLookupKey subst) [WaitForVar subst])
chrbstWaitForVar
    let -- split off the part which can be released
        (Map (ExtrValVarKey bp) [WaitForVar s]
wmRelease,Map (ExtrValVarKey bp) [WaitForVar s]
wmRemain) = forall k a. (k -> a -> Bool) -> Map k a -> (Map k a, Map k a)
Map.partitionWithKey (\ExtrValVarKey bp
v [WaitForVar s]
_ -> forall a. Ord a => a -> Set a -> Bool
Set.member ExtrValVarKey bp
v CHRWaitForVarSet s
vars) Map (ExtrValVarKey bp) [WaitForVar s]
wm
        wfvs :: [WaitForVar s]
wfvs = forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [a]
Map.elems Map (ExtrValVarKey bp) [WaitForVar s]
wmRelease
        -- get all influenced vars and released work
        (Set (ExtrValVarKey bp)
wvars, WorkInxSet
winxs) = (\([Set (ExtrValVarKey bp)]
vss,[Int]
wis) -> (forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions [Set (ExtrValVarKey bp)]
vss, [Int] -> WorkInxSet
IntSet.fromList [Int]
wis)) forall a b. (a -> b) -> a -> b
$ forall a b. [(a, b)] -> ([a], [b])
unzip [ (CHRWaitForVarSet s
vs,Int
wi) | (WaitForVar {_waitForVarVars :: forall s. WaitForVar s -> CHRWaitForVarSet s
_waitForVarVars=CHRWaitForVarSet s
vs, _waitForVarWorkInx :: forall s. WaitForVar s -> Int
_waitForVarWorkInx=Int
wi}) <- [WaitForVar s]
wfvs ]
    -- remove released work from remaining admin for influenced vars
    forall cnstr guard bprio prio subst env (m :: * -> *).
Lens
  (CHRFullState cnstr guard bprio prio subst env m)
  (CHRBackState cnstr bprio subst env)
bst forall a b c. (a :-> b) -> (b :-> c) -> a :-> c
^* forall cnstr bprio subst env env.
Lens
  (CHRBackState cnstr bprio subst env)
  (CHRBackState cnstr bprio subst env)
  (Map (VarLookupKey subst) [WaitForVar subst])
  (Map (VarLookupKey subst) [WaitForVar subst])
chrbstWaitForVar forall f (m :: * -> *) o. MonadState f m => (f :-> o) -> o -> m ()
=:
      forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (forall k a.
Ord k =>
(Maybe a -> Maybe a) -> k -> Map k a -> Map k a
Map.alter forall a b. (a -> b) -> a -> b
$ forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. Maybe a
Nothing forall a b. (a -> b) -> a -> b
$ \[WaitForVar s]
wfvs -> case forall a. (a -> Bool) -> [a] -> [a]
filter (\WaitForVar s
i -> forall s. WaitForVar s -> Int
_waitForVarWorkInx WaitForVar s
i Int -> WorkInxSet -> Bool
`IntSet.notMember` WorkInxSet
winxs) [WaitForVar s]
wfvs of
                [] -> forall a. Maybe a
Nothing
                [WaitForVar s]
wfvs' -> forall a. a -> Maybe a
Just [WaitForVar s]
wfvs'
            )
            Map (ExtrValVarKey bp) [WaitForVar s]
wmRemain
            (forall a. Set a -> [a]
Set.toList Set (ExtrValVarKey bp)
wvars)

    -- released work
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ WorkInxSet -> [Int]
IntSet.toList WorkInxSet
winxs


-- | Add work to the solve queue
addWorkToSolveQueue :: MonoBacktrackPrio c g bp p s e m => WorkInx -> CHRMonoBacktrackPrioT c g bp p s e m ()
addWorkToSolveQueue :: forall c g bp p s e (m :: * -> *).
MonoBacktrackPrio c g bp p s e m =>
Int -> CHRMonoBacktrackPrioT c g bp p s e m ()
addWorkToSolveQueue Int
i = do
    forall cnstr guard bprio prio subst env (m :: * -> *).
Lens
  (CHRFullState cnstr guard bprio prio subst env m)
  (CHRBackState cnstr bprio subst env)
bst forall a b c. (a :-> b) -> (b :-> c) -> a :-> c
^* forall cnstr bprio subst env env.
Lens
  (CHRBackState cnstr bprio subst env)
  (CHRBackState cnstr bprio subst env)
  WorkQueue
  WorkQueue
chrbstSolveQueue forall a b c. (a :-> b) -> (b :-> c) -> a :-> c
^* Lens' WorkQueue WorkInxSet
wkqueueActive forall f (m :: * -> *) o.
MonadState f m =>
(f :-> o) -> (o -> o) -> m ()
=$: (Int -> WorkInxSet -> WorkInxSet
IntSet.insert Int
i)

-- | Split off work from the solve work queue, possible none left
splitWorkFromSolveQueue :: MonoBacktrackPrio c g bp p s e m => CHRMonoBacktrackPrioT c g bp p s e m (Maybe (WorkInx))
splitWorkFromSolveQueue :: forall c g bp p s e (m :: * -> *).
MonoBacktrackPrio c g bp p s e m =>
CHRMonoBacktrackPrioT c g bp p s e m (Maybe Int)
splitWorkFromSolveQueue = do
    WorkInxSet
wq <- forall f (m :: * -> *) o. MonadState f m => (f :-> o) -> m o
getl forall a b. (a -> b) -> a -> b
$ forall cnstr guard bprio prio subst env (m :: * -> *).
Lens
  (CHRFullState cnstr guard bprio prio subst env m)
  (CHRBackState cnstr bprio subst env)
bst forall a b c. (a :-> b) -> (b :-> c) -> a :-> c
^* forall cnstr bprio subst env env.
Lens
  (CHRBackState cnstr bprio subst env)
  (CHRBackState cnstr bprio subst env)
  WorkQueue
  WorkQueue
chrbstSolveQueue forall a b c. (a :-> b) -> (b :-> c) -> a :-> c
^* Lens' WorkQueue WorkInxSet
wkqueueActive
    case WorkInxSet -> Maybe (Int, WorkInxSet)
IntSet.minView WorkInxSet
wq of
      Maybe (Int, WorkInxSet)
Nothing ->
          forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
      Just (Int
workInx, WorkInxSet
wq') -> do
          forall cnstr guard bprio prio subst env (m :: * -> *).
Lens
  (CHRFullState cnstr guard bprio prio subst env m)
  (CHRBackState cnstr bprio subst env)
bst forall a b c. (a :-> b) -> (b :-> c) -> a :-> c
^* forall cnstr bprio subst env env.
Lens
  (CHRBackState cnstr bprio subst env)
  (CHRBackState cnstr bprio subst env)
  WorkQueue
  WorkQueue
chrbstSolveQueue forall a b c. (a :-> b) -> (b :-> c) -> a :-> c
^* Lens' WorkQueue WorkInxSet
wkqueueActive forall f (m :: * -> *) o. MonadState f m => (f :-> o) -> o -> m ()
=: WorkInxSet
wq'
          forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just (Int
workInx)

-- | Remove work from the work queue
deleteFromWorkQueue :: MonoBacktrackPrio c g bp p s e m => WorkInxSet -> CHRMonoBacktrackPrioT c g bp p s e m ()
deleteFromWorkQueue :: forall c g bp p s e (m :: * -> *).
MonoBacktrackPrio c g bp p s e m =>
WorkInxSet -> CHRMonoBacktrackPrioT c g bp p s e m ()
deleteFromWorkQueue WorkInxSet
is = do
    -- bst ^* chrbstRuleWorkQueue ^* wkqueueActive =$: (\s -> foldr (IntSet.delete) s is)
    forall cnstr guard bprio prio subst env (m :: * -> *).
Lens
  (CHRFullState cnstr guard bprio prio subst env m)
  (CHRBackState cnstr bprio subst env)
bst forall a b c. (a :-> b) -> (b :-> c) -> a :-> c
^* forall cnstr bprio subst env env.
Lens
  (CHRBackState cnstr bprio subst env)
  (CHRBackState cnstr bprio subst env)
  WorkQueue
  WorkQueue
chrbstRuleWorkQueue forall a b c. (a :-> b) -> (b :-> c) -> a :-> c
^* Lens' WorkQueue WorkInxSet
wkqueueActive forall f (m :: * -> *) o.
MonadState f m =>
(f :-> o) -> (o -> o) -> m ()
=$: forall a b c. (a -> b -> c) -> b -> a -> c
flip WorkInxSet -> WorkInxSet -> WorkInxSet
IntSet.difference WorkInxSet
is
    forall cnstr guard bprio prio subst env (m :: * -> *).
Lens
  (CHRFullState cnstr guard bprio prio subst env m)
  (CHRBackState cnstr bprio subst env)
bst forall a b c. (a :-> b) -> (b :-> c) -> a :-> c
^* forall cnstr bprio subst env env.
Lens
  (CHRBackState cnstr bprio subst env)
  (CHRBackState cnstr bprio subst env)
  WorkQueue
  WorkQueue
chrbstRuleWorkQueue forall a b c. (a :-> b) -> (b :-> c) -> a :-> c
^* Lens' WorkQueue WorkInxSet
wkqueueRedo forall f (m :: * -> *) o.
MonadState f m =>
(f :-> o) -> (o -> o) -> m ()
=$: forall a b c. (a -> b -> c) -> b -> a -> c
flip WorkInxSet -> WorkInxSet -> WorkInxSet
IntSet.difference WorkInxSet
is

-- | Extract the active work in the queue
waitingInWorkQueue :: MonoBacktrackPrio c g bp p s e m => CHRMonoBacktrackPrioT c g bp p s e m WorkInxSet
waitingInWorkQueue :: forall c g bp p s e (m :: * -> *).
MonoBacktrackPrio c g bp p s e m =>
CHRMonoBacktrackPrioT c g bp p s e m WorkInxSet
waitingInWorkQueue = do
    WorkInxSet
a <- forall f (m :: * -> *) o. MonadState f m => (f :-> o) -> m o
getl forall a b. (a -> b) -> a -> b
$ forall cnstr guard bprio prio subst env (m :: * -> *).
Lens
  (CHRFullState cnstr guard bprio prio subst env m)
  (CHRBackState cnstr bprio subst env)
bst forall a b c. (a :-> b) -> (b :-> c) -> a :-> c
^* forall cnstr bprio subst env env.
Lens
  (CHRBackState cnstr bprio subst env)
  (CHRBackState cnstr bprio subst env)
  WorkQueue
  WorkQueue
chrbstRuleWorkQueue forall a b c. (a :-> b) -> (b :-> c) -> a :-> c
^* Lens' WorkQueue WorkInxSet
wkqueueActive
    WorkInxSet
r <- forall f (m :: * -> *) o. MonadState f m => (f :-> o) -> m o
getl forall a b. (a -> b) -> a -> b
$ forall cnstr guard bprio prio subst env (m :: * -> *).
Lens
  (CHRFullState cnstr guard bprio prio subst env m)
  (CHRBackState cnstr bprio subst env)
bst forall a b c. (a :-> b) -> (b :-> c) -> a :-> c
^* forall cnstr bprio subst env env.
Lens
  (CHRBackState cnstr bprio subst env)
  (CHRBackState cnstr bprio subst env)
  WorkQueue
  WorkQueue
chrbstRuleWorkQueue forall a b c. (a :-> b) -> (b :-> c) -> a :-> c
^* Lens' WorkQueue WorkInxSet
wkqueueRedo
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ WorkInxSet -> WorkInxSet -> WorkInxSet
IntSet.union WorkInxSet
a WorkInxSet
r

-- | Split off work from the work queue, possible none left
splitFromWorkQueue :: MonoBacktrackPrio c g bp p s e m => CHRMonoBacktrackPrioT c g bp p s e m (Maybe WorkInx)
splitFromWorkQueue :: forall c g bp p s e (m :: * -> *).
MonoBacktrackPrio c g bp p s e m =>
CHRMonoBacktrackPrioT c g bp p s e m (Maybe Int)
splitFromWorkQueue = do
    WorkInxSet
wq <- forall f (m :: * -> *) o. MonadState f m => (f :-> o) -> m o
getl forall a b. (a -> b) -> a -> b
$ forall cnstr guard bprio prio subst env (m :: * -> *).
Lens
  (CHRFullState cnstr guard bprio prio subst env m)
  (CHRBackState cnstr bprio subst env)
bst forall a b c. (a :-> b) -> (b :-> c) -> a :-> c
^* forall cnstr bprio subst env env.
Lens
  (CHRBackState cnstr bprio subst env)
  (CHRBackState cnstr bprio subst env)
  WorkQueue
  WorkQueue
chrbstRuleWorkQueue forall a b c. (a :-> b) -> (b :-> c) -> a :-> c
^* Lens' WorkQueue WorkInxSet
wkqueueActive
    case WorkInxSet -> Maybe (Int, WorkInxSet)
IntSet.minView WorkInxSet
wq of
      -- If no more work, ready if nothing was done anymore
      Maybe (Int, WorkInxSet)
Nothing -> do
          Bool
did <- forall f (m :: * -> *) o a.
MonadState f m =>
(f :-> o) -> (o -> (a, o)) -> m a
modifyAndGet (forall cnstr guard bprio prio subst env (m :: * -> *).
Lens
  (CHRFullState cnstr guard bprio prio subst env m)
  (CHRBackState cnstr bprio subst env)
bst forall a b c. (a :-> b) -> (b :-> c) -> a :-> c
^* forall cnstr bprio subst env env.
Lens
  (CHRBackState cnstr bprio subst env)
  (CHRBackState cnstr bprio subst env)
  WorkQueue
  WorkQueue
chrbstRuleWorkQueue forall a b c. (a :-> b) -> (b :-> c) -> a :-> c
^* Lens' WorkQueue Bool
wkqueueDidSomething) forall a b. (a -> b) -> a -> b
$ \Bool
d -> (Bool
d, Bool
False)
          if Bool
did -- && not (IntSet.null wr)
            then do
              WorkInxSet
wr  <- forall f (m :: * -> *) o a.
MonadState f m =>
(f :-> o) -> (o -> (a, o)) -> m a
modifyAndGet (forall cnstr guard bprio prio subst env (m :: * -> *).
Lens
  (CHRFullState cnstr guard bprio prio subst env m)
  (CHRBackState cnstr bprio subst env)
bst forall a b c. (a :-> b) -> (b :-> c) -> a :-> c
^* forall cnstr bprio subst env env.
Lens
  (CHRBackState cnstr bprio subst env)
  (CHRBackState cnstr bprio subst env)
  WorkQueue
  WorkQueue
chrbstRuleWorkQueue forall a b c. (a :-> b) -> (b :-> c) -> a :-> c
^* Lens' WorkQueue WorkInxSet
wkqueueRedo) forall a b. (a -> b) -> a -> b
$ \WorkInxSet
r -> (WorkInxSet
r, WorkInxSet
IntSet.empty)
              forall cnstr guard bprio prio subst env (m :: * -> *).
Lens
  (CHRFullState cnstr guard bprio prio subst env m)
  (CHRBackState cnstr bprio subst env)
bst forall a b c. (a :-> b) -> (b :-> c) -> a :-> c
^* forall cnstr bprio subst env env.
Lens
  (CHRBackState cnstr bprio subst env)
  (CHRBackState cnstr bprio subst env)
  WorkQueue
  WorkQueue
chrbstRuleWorkQueue forall a b c. (a :-> b) -> (b :-> c) -> a :-> c
^* Lens' WorkQueue WorkInxSet
wkqueueActive forall f (m :: * -> *) o. MonadState f m => (f :-> o) -> o -> m ()
=: WorkInxSet
wr
              forall c g bp p s e (m :: * -> *).
MonoBacktrackPrio c g bp p s e m =>
CHRMonoBacktrackPrioT c g bp p s e m (Maybe Int)
splitFromWorkQueue
            else
              forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
      
      -- There is work in the queue
      Just (Int
workInx, WorkInxSet
wq') -> do
          forall cnstr guard bprio prio subst env (m :: * -> *).
Lens
  (CHRFullState cnstr guard bprio prio subst env m)
  (CHRBackState cnstr bprio subst env)
bst forall a b c. (a :-> b) -> (b :-> c) -> a :-> c
^* forall cnstr bprio subst env env.
Lens
  (CHRBackState cnstr bprio subst env)
  (CHRBackState cnstr bprio subst env)
  WorkQueue
  WorkQueue
chrbstRuleWorkQueue forall a b c. (a :-> b) -> (b :-> c) -> a :-> c
^* Lens' WorkQueue WorkInxSet
wkqueueActive forall f (m :: * -> *) o. MonadState f m => (f :-> o) -> o -> m ()
=: WorkInxSet
wq'
          forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just Int
workInx

-- | Add a constraint to be solved or residualised
addConstraintAsWork
  :: MonoBacktrackPrio c g bp p s e m
  => c
  -> CHRMonoBacktrackPrioT c g bp p s e m (ConstraintSolvesVia, WorkInx)
addConstraintAsWork :: forall c g bp p s e (m :: * -> *).
MonoBacktrackPrio c g bp p s e m =>
c
-> CHRMonoBacktrackPrioT c g bp p s e m (ConstraintSolvesVia, Int)
addConstraintAsWork c
c = do
    let via :: ConstraintSolvesVia
via = forall c. IsConstraint c => c -> ConstraintSolvesVia
cnstrSolvesVia c
c
        addw :: Int
-> Work' (Key (TrTrKey c)) c
-> CHRMonoBacktrackPrioT c g bp p s e m (ConstraintSolvesVia, Int)
addw Int
i Work' (Key (TrTrKey c)) c
w = do
          forall cnstr guard bprio prio subst env (m :: * -> *).
Lens
  (CHRFullState cnstr guard bprio prio subst env m)
  (CHRBackState cnstr bprio subst env)
bst forall a b c. (a :-> b) -> (b :-> c) -> a :-> c
^* forall cnstr bprio subst env cnstr env.
Lens
  (CHRBackState cnstr bprio subst env)
  (CHRBackState cnstr bprio subst env)
  (WorkStore cnstr)
  (WorkStore cnstr)
chrbstWorkStore forall a b c. (a :-> b) -> (b :-> c) -> a :-> c
^* forall cnstr. Lens' (WorkStore cnstr) (IntMap (Work cnstr))
wkstoreTable forall f (m :: * -> *) o.
MonadState f m =>
(f :-> o) -> (o -> o) -> m ()
=$: forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
i Work' (Key (TrTrKey c)) c
w
          forall (m :: * -> *) a. Monad m => a -> m a
return (ConstraintSolvesVia
via,Int
i)
    Int
i <- forall {cnstr} {guard} {bprio} {prio} {subst} {env} {m :: * -> *}
       {m :: * -> *}.
MonadState (CHRFullState cnstr guard bprio prio subst env m) m =>
m Int
fresh
    Work' (Key (TrTrKey c)) c
w <- case ConstraintSolvesVia
via of
        -- a plain rule is added to the work store
        ConstraintSolvesVia
ConstraintSolvesVia_Rule -> do
            forall cnstr guard bprio prio subst env (m :: * -> *).
Lens
  (CHRFullState cnstr guard bprio prio subst env m)
  (CHRBackState cnstr bprio subst env)
bst forall a b c. (a :-> b) -> (b :-> c) -> a :-> c
^* forall cnstr bprio subst env cnstr env.
Lens
  (CHRBackState cnstr bprio subst env)
  (CHRBackState cnstr bprio subst env)
  (WorkStore cnstr)
  (WorkStore cnstr)
chrbstWorkStore forall a b c. (a :-> b) -> (b :-> c) -> a :-> c
^* forall cnstr.
Lens' (WorkStore cnstr) (TreeTrie (TrTrKey cnstr) [Int])
wkstoreTrie forall f (m :: * -> *) o.
MonadState f m =>
(f :-> o) -> (o -> o) -> m ()
=$: forall k v.
Ord k =>
(v -> v -> v) -> Key k -> v -> TreeTrie k v -> TreeTrie k v
TT.insertByKeyWith forall a. [a] -> [a] -> [a]
(++) Key (TrTrKey c)
k [Int
i]
            forall c g bp p s e (m :: * -> *).
MonoBacktrackPrio c g bp p s e m =>
Int -> CHRMonoBacktrackPrioT c g bp p s e m ()
addToWorkQueue Int
i
            forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall k c. k -> c -> Int -> Work' k c
Work Key (TrTrKey c)
k c
c Int
i
          where k :: Key (TrTrKey c)
k = forall x. TreeTrieKeyable x => x -> Key (TrTrKey x)
TT.toTreeTrieKey c
c -- chrToKey c -- chrToWorkKey c
        -- work for the solver is added to its own queue
        ConstraintSolvesVia
ConstraintSolvesVia_Solve -> do
            forall c g bp p s e (m :: * -> *).
MonoBacktrackPrio c g bp p s e m =>
Int -> CHRMonoBacktrackPrioT c g bp p s e m ()
addWorkToSolveQueue Int
i
            forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall k c. c -> Work' k c
Work_Solve c
c
        -- residue is just remembered
        ConstraintSolvesVia
ConstraintSolvesVia_Residual -> do
            forall cnstr guard bprio prio subst env (m :: * -> *).
Lens
  (CHRFullState cnstr guard bprio prio subst env m)
  (CHRBackState cnstr bprio subst env)
bst forall a b c. (a :-> b) -> (b :-> c) -> a :-> c
^* forall cnstr bprio subst env env.
Lens
  (CHRBackState cnstr bprio subst env)
  (CHRBackState cnstr bprio subst env)
  [Int]
  [Int]
chrbstResidualQueue forall f (m :: * -> *) o.
MonadState f m =>
(f :-> o) -> (o -> o) -> m ()
=$: (Int
i forall a. a -> [a] -> [a]
:)
            forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall k c. c -> Work' k c
Work_Residue c
c
        -- fail right away if this constraint is a fail constraint
        ConstraintSolvesVia
ConstraintSolvesVia_Fail -> do
            forall c g bp p s e (m :: * -> *).
MonoBacktrackPrio c g bp p s e m =>
Int -> CHRMonoBacktrackPrioT c g bp p s e m ()
addWorkToSolveQueue Int
i
            forall (m :: * -> *) a. Monad m => a -> m a
return forall k c. Work' k c
Work_Fail
    Int
-> Work' (Key (TrTrKey c)) c
-> CHRMonoBacktrackPrioT c g bp p s e m (ConstraintSolvesVia, Int)
addw Int
i Work' (Key (TrTrKey c)) c
w
{-
        -- succeed right away if this constraint is a succes constraint
        -- TBD, different return value of slvSucces...
        ConstraintSolvesVia_Succeed -> do
            slvSucces
-}
  where
    fresh :: m Int
fresh = forall f (m :: * -> *) o a.
MonadState f m =>
(f :-> o) -> (o -> (a, o)) -> m a
modifyAndGet (forall cnstr guard bprio prio subst env (m :: * -> *).
Lens
  (CHRFullState cnstr guard bprio prio subst env m)
  (CHRBackState cnstr bprio subst env)
bst forall a b c. (a :-> b) -> (b :-> c) -> a :-> c
^* forall cnstr bprio subst env cnstr env.
Lens
  (CHRBackState cnstr bprio subst env)
  (CHRBackState cnstr bprio subst env)
  (WorkStore cnstr)
  (WorkStore cnstr)
chrbstWorkStore forall a b c. (a :-> b) -> (b :-> c) -> a :-> c
^* forall cnstr. Lens' (WorkStore cnstr) Int
wkstoreNextFreeWorkInx) forall a b. (a -> b) -> a -> b
$ \Int
i -> (Int
i, Int
i forall a. Num a => a -> a -> a
+ Int
1)

-------------------------------------------------------------------------------------------
--- Solver combinators
-------------------------------------------------------------------------------------------

-- | Succesful return, solution is found
slvSucces :: MonoBacktrackPrio c g bp p s e m => [WorkInx] -> CHRMonoBacktrackPrioT c g bp p s e m (SolverResult s)
slvSucces :: forall c g bp p s e (m :: * -> *).
MonoBacktrackPrio c g bp p s e m =>
[Int] -> CHRMonoBacktrackPrioT c g bp p s e m (SolverResult s)
slvSucces [Int]
leftoverWork = do
    CHRBackState c bp s e
bst <- forall f (m :: * -> *) o. MonadState f m => (f :-> o) -> m o
getl forall a b. (a -> b) -> a -> b
$ forall cnstr guard bprio prio subst env (m :: * -> *).
Lens
  (CHRFullState cnstr guard bprio prio subst env m)
  (CHRBackState cnstr bprio subst env)
bst
    let ret :: CHRMonoBacktrackPrioT c g bp p s e m (SolverResult s)
ret = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ SolverResult
          { slvresSubst :: s
slvresSubst = CHRBackState c bp s e
bst forall s a. s -> Getting a s a -> a
^. forall cnstr bprio subst env env.
Lens
  (CHRBackState cnstr bprio subst env)
  (CHRBackState cnstr bprio subst env)
  subst
  subst
chrbstSolveSubst
          , slvresResidualCnstr :: [Int]
slvresResidualCnstr = forall a. [a] -> [a]
reverse forall a b. (a -> b) -> a -> b
$ CHRBackState c bp s e
bst forall s a. s -> Getting a s a -> a
^. forall cnstr bprio subst env env.
Lens
  (CHRBackState cnstr bprio subst env)
  (CHRBackState cnstr bprio subst env)
  [Int]
  [Int]
chrbstResidualQueue
          , slvresWorkCnstr :: [Int]
slvresWorkCnstr = [Int]
leftoverWork
          , slvresWaitVarCnstr :: [Int]
slvresWaitVarCnstr = [ WaitForVar s
wfv forall s a. s -> Getting a s a -> a
^. forall s. Lens' (WaitForVar s) Int
waitForVarWorkInx | [WaitForVar s]
wfvs <- forall k a. Map k a -> [a]
Map.elems forall a b. (a -> b) -> a -> b
$ CHRBackState c bp s e
bst forall s a. s -> Getting a s a -> a
^. forall cnstr bprio subst env env.
Lens
  (CHRBackState cnstr bprio subst env)
  (CHRBackState cnstr bprio subst env)
  (Map (VarLookupKey subst) [WaitForVar subst])
  (Map (VarLookupKey subst) [WaitForVar subst])
chrbstWaitForVar, WaitForVar s
wfv <- [WaitForVar s]
wfvs ]
          , slvresReductionSteps :: [SolverReductionStep]
slvresReductionSteps = forall a. [a] -> [a]
reverse forall a b. (a -> b) -> a -> b
$ CHRBackState c bp s e
bst forall s a. s -> Getting a s a -> a
^. forall cnstr bprio subst env env.
Lens
  (CHRBackState cnstr bprio subst env)
  (CHRBackState cnstr bprio subst env)
  [SolverReductionStep]
  [SolverReductionStep]
chrbstReductionSteps
          }
    -- when ready, just return and backtrack into the scheduler
    CHRMonoBacktrackPrioT c g bp p s e m (SolverResult s)
ret forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` forall c g bp p s e (m :: * -> *).
MonoBacktrackPrio c g bp p s e m =>
CHRMonoBacktrackPrioT c g bp p s e m (SolverResult s)
slvScheduleRun

-- | Failure return, no solution is found
slvFail :: MonoBacktrackPrio c g bp p s e m => CHRMonoBacktrackPrioT c g bp p s e m (SolverResult s)
slvFail :: forall c g bp p s e (m :: * -> *).
MonoBacktrackPrio c g bp p s e m =>
CHRMonoBacktrackPrioT c g bp p s e m (SolverResult s)
slvFail = do
    -- failing just terminates this slv, scheduling to another, if any
    forall c g bp p s e (m :: * -> *).
MonoBacktrackPrio c g bp p s e m =>
CHRMonoBacktrackPrioT c g bp p s e m (SolverResult s)
slvScheduleRun
{-# INLINE slvFail #-}

-- | Schedule a solver with the current backtrack prio, assuming this is the same as 'slv' has administered itself in its backtracking state
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 :: forall c g bp p s e (m :: * -> *).
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 CHRPrioEvaluatableVal bp
bprio CHRMonoBacktrackPrioT c g bp p s e m (SolverResult s)
slv = do
    -- bprio <- getl $ bst ^* chrbstBacktrackPrio
    forall cnstr guard bprio prio subst env (m :: * -> *).
Lens
  (CHRFullState cnstr guard bprio prio subst env m)
  (CHRGlobState cnstr guard bprio prio subst env m)
gst forall a b c. (a :-> b) -> (b :-> c) -> a :-> c
^* forall cnstr guard bprio prio subst env (m :: * -> *) env
       (m :: * -> *).
Lens
  (CHRGlobState cnstr guard bprio prio subst env m)
  (CHRGlobState cnstr guard bprio prio subst env m)
  (MinPQueue
     (CHRPrioEvaluatableVal bprio)
     (CHRMonoBacktrackPrioT
        cnstr guard bprio prio subst env m (SolverResult subst)))
  (MinPQueue
     (CHRPrioEvaluatableVal bprio)
     (CHRMonoBacktrackPrioT
        cnstr guard bprio prio subst env m (SolverResult subst)))
chrgstScheduleQueue forall f (m :: * -> *) o.
MonadState f m =>
(f :-> o) -> (o -> o) -> m ()
=$: forall k a. Ord k => k -> a -> MinPQueue k a -> MinPQueue k a
Que.insert CHRPrioEvaluatableVal bp
bprio CHRMonoBacktrackPrioT c g bp p s e m (SolverResult s)
slv
{-# INLINE slvSchedule #-}

-- | Schedule a solver with the current backtrack prio, assuming this is the same as 'slv' has administered itself in its backtracking state
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' :: forall c g bp p s e (m :: * -> *).
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' CHRMonoBacktrackPrioT c g bp p s e m (SolverResult s)
slv = do
    CHRPrioEvaluatableVal bp
bprio <- forall f (m :: * -> *) o. MonadState f m => (f :-> o) -> m o
getl forall a b. (a -> b) -> a -> b
$ forall cnstr guard bprio prio subst env (m :: * -> *).
Lens
  (CHRFullState cnstr guard bprio prio subst env m)
  (CHRBackState cnstr bprio subst env)
bst forall a b c. (a :-> b) -> (b :-> c) -> a :-> c
^* forall cnstr bprio subst env bprio env.
Lens
  (CHRBackState cnstr bprio subst env)
  (CHRBackState cnstr bprio subst env)
  (CHRPrioEvaluatableVal bprio)
  (CHRPrioEvaluatableVal bprio)
chrbstBacktrackPrio
    forall c g bp p s e (m :: * -> *).
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 CHRPrioEvaluatableVal bp
bprio CHRMonoBacktrackPrioT c g bp p s e m (SolverResult s)
slv
{-# INLINE slvSchedule' #-}

-- | Rechedule a solver, switching context/prio
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 :: forall c g bp p s e (m :: * -> *).
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 CHRMonoBacktrackPrioT c g bp p s e m (SolverResult s)
slv = do
    forall c g bp p s e (m :: * -> *).
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' CHRMonoBacktrackPrioT c g bp p s e m (SolverResult s)
slv
    forall c g bp p s e (m :: * -> *).
MonoBacktrackPrio c g bp p s e m =>
CHRMonoBacktrackPrioT c g bp p s e m (SolverResult s)
slvScheduleRun
{-# INLINE slvReschedule #-}

-- | Retrieve solver with the highest prio from the schedule queue
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 :: forall c g bp p s e (m :: * -> *).
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 = forall f (m :: * -> *) o a.
MonadState f m =>
(f :-> o) -> (o -> (a, o)) -> m a
modifyAndGet (forall cnstr guard bprio prio subst env (m :: * -> *).
Lens
  (CHRFullState cnstr guard bprio prio subst env m)
  (CHRGlobState cnstr guard bprio prio subst env m)
gst forall a b c. (a :-> b) -> (b :-> c) -> a :-> c
^* forall cnstr guard bprio prio subst env (m :: * -> *) env
       (m :: * -> *).
Lens
  (CHRGlobState cnstr guard bprio prio subst env m)
  (CHRGlobState cnstr guard bprio prio subst env m)
  (MinPQueue
     (CHRPrioEvaluatableVal bprio)
     (CHRMonoBacktrackPrioT
        cnstr guard bprio prio subst env m (SolverResult subst)))
  (MinPQueue
     (CHRPrioEvaluatableVal bprio)
     (CHRMonoBacktrackPrioT
        cnstr guard bprio prio subst env m (SolverResult subst)))
chrgstScheduleQueue) forall a b. (a -> b) -> a -> b
$ \MinPQueue
  (CHRPrioEvaluatableVal bp)
  (CHRMonoBacktrackPrioT c g bp p s e m (SolverResult s))
q -> (forall k a. MinPQueue k a -> Maybe (k, a)
Que.getMin MinPQueue
  (CHRPrioEvaluatableVal bp)
  (CHRMonoBacktrackPrioT c g bp p s e m (SolverResult s))
q, forall k a. Ord k => MinPQueue k a -> MinPQueue k a
Que.deleteMin MinPQueue
  (CHRPrioEvaluatableVal bp)
  (CHRMonoBacktrackPrioT c g bp p s e m (SolverResult s))
q)
{-# INLINE slvSplitFromSchedule #-}

-- | Run from the schedule que, fail if nothing left to be done
slvScheduleRun :: MonoBacktrackPrio c g bp p s e m => CHRMonoBacktrackPrioT c g bp p s e m (SolverResult s)
slvScheduleRun :: forall c g bp p s e (m :: * -> *).
MonoBacktrackPrio c g bp p s e m =>
CHRMonoBacktrackPrioT c g bp p s e m (SolverResult s)
slvScheduleRun = forall c g bp p s e (m :: * -> *).
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 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall (m :: * -> *) a. MonadPlus m => m a
mzero forall a b. (a, b) -> b
snd
{-# INLINE slvScheduleRun #-}

-------------------------------------------------------------------------------------------
--- Solver utils
-------------------------------------------------------------------------------------------

lkupWork :: MonoBacktrackPrio c g bp p s e m => WorkInx -> CHRMonoBacktrackPrioT c g bp p s e m (Work c)
lkupWork :: forall c g bp p s e (m :: * -> *).
MonoBacktrackPrio c g bp p s e m =>
Int -> CHRMonoBacktrackPrioT c g bp p s e m (Work c)
lkupWork Int
i = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a. a -> Int -> IntMap a -> a
IntMap.findWithDefault (forall {a}. String -> a
panic String
"MBP.wkstoreTable.lookup") Int
i) forall a b. (a -> b) -> a -> b
$ forall f (m :: * -> *) o. MonadState f m => (f :-> o) -> m o
getl forall a b. (a -> b) -> a -> b
$ forall cnstr guard bprio prio subst env (m :: * -> *).
Lens
  (CHRFullState cnstr guard bprio prio subst env m)
  (CHRBackState cnstr bprio subst env)
bst forall a b c. (a :-> b) -> (b :-> c) -> a :-> c
^* forall cnstr bprio subst env cnstr env.
Lens
  (CHRBackState cnstr bprio subst env)
  (CHRBackState cnstr bprio subst env)
  (WorkStore cnstr)
  (WorkStore cnstr)
chrbstWorkStore forall a b c. (a :-> b) -> (b :-> c) -> a :-> c
^* forall cnstr. Lens' (WorkStore cnstr) (IntMap (Work cnstr))
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 :: forall c g bp p s e (m :: * -> *).
MonoBacktrackPrio c g bp p s e m =>
Int -> CHRMonoBacktrackPrioT c g bp p s e m (StoredCHR c g bp p)
lkupChr  Int
i = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a. a -> Int -> IntMap a -> a
IntMap.findWithDefault (forall {a}. String -> a
panic String
"MBP.chrSolve.chrstoreTable.lookup") Int
i) forall a b. (a -> b) -> a -> b
$ forall f (m :: * -> *) o. MonadState f m => (f :-> o) -> m o
getl forall a b. (a -> b) -> a -> b
$ forall cnstr guard bprio prio subst env (m :: * -> *).
Lens
  (CHRFullState cnstr guard bprio prio subst env m)
  (CHRGlobState cnstr guard bprio prio subst env m)
gst forall a b c. (a :-> b) -> (b :-> c) -> a :-> c
^* forall cnstr guard bprio prio subst env (m :: * -> *).
Lens'
  (CHRGlobState cnstr guard bprio prio subst env m)
  (CHRStore cnstr guard bprio prio)
chrgstStore forall a b c. (a :-> b) -> (b :-> c) -> a :-> c
^* forall cnstr guard bprio prio guard bprio prio.
Lens
  (CHRStore cnstr guard bprio prio)
  (CHRStore cnstr guard bprio prio)
  (IntMap (StoredCHR cnstr guard bprio prio))
  (IntMap (StoredCHR cnstr guard bprio prio))
chrstoreTable
{-# INLINE lkupChr #-}

-- | Convert
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 :: forall c g bp p s e (m :: * -> *).
MonoBacktrackPrio c g bp p s e m =>
SolverReductionStep
-> CHRMonoBacktrackPrioT
     c g bp p s e m (SolverReductionStep' (StoredCHR c g bp p) (Work c))
cvtSolverReductionStep (SolverReductionStep MatchedCombi
mc Int
ai Map ConstraintSolvesVia [Int]
nw) = do
    MatchedCombi' (StoredCHR c g bp p) (Work c)
mc  <- forall {s} {c} {e} {g} {bp} {p} {m :: * -> *}.
(ExtrValVarKey (VarLookupVal s) ~ VarLookupKey s,
 TreeTrieKeyable c, IsConstraint c, CHRCheckable e g s,
 VarUpdatable c s, VarUpdatable g s, CHRMatchable e c s,
 CHRMatchable e bp s, CHRPrioEvaluatable e bp s,
 CHRPrioEvaluatable e p s, Typeable c, Typeable g, Typeable bp,
 Typeable p, PP c, PP g, PP bp, PP p, PP (TrTrKey c),
 PP (CHRPrioEvaluatableVal bp), PP (VarLookupKey s), Monad m,
 Lookup s (VarLookupKey s) (VarLookupVal s),
 Fresh Int (ExtrValVarKey (VarLookupVal s)),
 VarTerm (VarLookupVal s), VarExtractable g, Ord c,
 Ord (TrTrKey c)) =>
MatchedCombi
-> LogicStateT
     (CHRGlobState c g bp p s e m)
     (CHRBackState c bp s e)
     m
     (MatchedCombi' (StoredCHR c g bp p) (Work' (Key (TrTrKey c)) c))
cvtMC MatchedCombi
mc
    Map ConstraintSolvesVia [Work c]
nw  <- forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (forall k a. Map k a -> [(k, a)]
Map.toList Map ConstraintSolvesVia [Int]
nw) forall a b. (a -> b) -> a -> b
$ \(ConstraintSolvesVia
via,[Int]
i) -> do
             [Work c]
i <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Int]
i forall c g bp p s e (m :: * -> *).
MonoBacktrackPrio c g bp p s e m =>
Int -> CHRMonoBacktrackPrioT c g bp p s e m (Work c)
lkupWork
             forall (m :: * -> *) a. Monad m => a -> m a
return (ConstraintSolvesVia
via, [Work c]
i)
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall c w.
MatchedCombi' c w
-> Int -> Map ConstraintSolvesVia [w] -> SolverReductionStep' c w
SolverReductionStep MatchedCombi' (StoredCHR c g bp p) (Work c)
mc Int
ai Map ConstraintSolvesVia [Work c]
nw
  where
    cvtMC :: MatchedCombi
-> LogicStateT
     (CHRGlobState c g bp p s e m)
     (CHRBackState c bp s e)
     m
     (MatchedCombi' (StoredCHR c g bp p) (Work' (Key (TrTrKey c)) c))
cvtMC (MatchedCombi {mcCHR :: forall c w. MatchedCombi' c w -> c
mcCHR = Int
c, mcWork :: forall c w. MatchedCombi' c w -> [w]
mcWork = [Int]
ws}) = do
      StoredCHR c g bp p
c'  <- forall c g bp p s e (m :: * -> *).
MonoBacktrackPrio c g bp p s e m =>
Int -> CHRMonoBacktrackPrioT c g bp p s e m (StoredCHR c g bp p)
lkupChr Int
c
      [Work' (Key (TrTrKey c)) c]
ws' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Int]
ws forall c g bp p s e (m :: * -> *).
MonoBacktrackPrio c g bp p s e m =>
Int -> CHRMonoBacktrackPrioT c g bp p s e m (Work c)
lkupWork
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall c w. c -> [w] -> MatchedCombi' c w
MatchedCombi StoredCHR c g bp p
c' [Work' (Key (TrTrKey c)) c]
ws'
cvtSolverReductionStep (SolverReductionDBG PP_Doc
pp) = forall (m :: * -> *) a. Monad m => a -> m a
return (forall c w. PP_Doc -> SolverReductionStep' c w
SolverReductionDBG PP_Doc
pp)

-- | PP result
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 :: forall c g bp p s e (m :: * -> *).
(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
verbosity (SolverResult {slvresSubst :: forall subst. SolverResult subst -> subst
slvresSubst = s
s, slvresResidualCnstr :: forall subst. SolverResult subst -> [Int]
slvresResidualCnstr = [Int]
ris, slvresWorkCnstr :: forall subst. SolverResult subst -> [Int]
slvresWorkCnstr = [Int]
wis, slvresWaitVarCnstr :: forall subst. SolverResult subst -> [Int]
slvresWaitVarCnstr = [Int]
wvis, slvresReductionSteps :: forall subst. SolverResult subst -> [SolverReductionStep]
slvresReductionSteps = [SolverReductionStep]
steps}) = do
    [PP_Doc]
rs  <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Int]
ris  forall a b. (a -> b) -> a -> b
$ \Int
i -> forall c g bp p s e (m :: * -> *).
MonoBacktrackPrio c g bp p s e m =>
Int -> CHRMonoBacktrackPrioT c g bp p s e m (Work c)
lkupWork Int
i forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. PP a => a -> PP_Doc
pp forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k c. Work' k c -> c
workCnstr
    [PP_Doc]
ws  <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Int]
wis  forall a b. (a -> b) -> a -> b
$ \Int
i -> forall c g bp p s e (m :: * -> *).
MonoBacktrackPrio c g bp p s e m =>
Int -> CHRMonoBacktrackPrioT c g bp p s e m (Work c)
lkupWork Int
i forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. PP a => a -> PP_Doc
pp forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k c. Work' k c -> c
workCnstr
    [PP_Doc]
wvs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Int]
wvis forall a b. (a -> b) -> a -> b
$ \Int
i -> forall c g bp p s e (m :: * -> *).
MonoBacktrackPrio c g bp p s e m =>
Int -> CHRMonoBacktrackPrioT c g bp p s e m (Work c)
lkupWork Int
i forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. PP a => a -> PP_Doc
pp forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k c. Work' k c -> c
workCnstr
    [PP_Doc]
ss  <- if Verbosity
verbosity forall a. Ord a => a -> a -> Bool
>= Verbosity
Verbosity_ALot
      then forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [SolverReductionStep]
steps forall a b. (a -> b) -> a -> b
$ \SolverReductionStep
step -> forall c g bp p s e (m :: * -> *).
MonoBacktrackPrio c g bp p s e m =>
SolverReductionStep
-> CHRMonoBacktrackPrioT
     c g bp p s e m (SolverReductionStep' (StoredCHR c g bp p) (Work c))
cvtSolverReductionStep SolverReductionStep
step forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. PP a => a -> PP_Doc
pp)
      else forall (m :: * -> *) a. Monad m => a -> m a
return [forall a. PP a => a -> PP_Doc
pp forall a b. (a -> b) -> a -> b
$ String
"Only included with enough verbosity turned on"]
    Int
nrsteps <- forall f (m :: * -> *) o. MonadState f m => (f :-> o) -> m o
getl forall a b. (a -> b) -> a -> b
$ forall cnstr guard bprio prio subst env (m :: * -> *).
Lens
  (CHRFullState cnstr guard bprio prio subst env m)
  (CHRGlobState cnstr guard bprio prio subst env m)
gst forall a b c. (a :-> b) -> (b :-> c) -> a :-> c
^* forall cnstr guard bprio prio subst env (m :: * -> *).
Lens' (CHRGlobState cnstr guard bprio prio subst env m) Int
chrgstStatNrSolveSteps
    let pextra :: PP_Doc
pextra | Verbosity
verbosity forall a. Ord a => a -> a -> Bool
>= Verbosity
Verbosity_Normal = 
                      String
"Residue" forall a b. (PP a, PP b) => a -> b -> PP_Doc
>-< forall a. PP a => Int -> a -> PP_Doc
indent Int
2 (forall a. PP a => [a] -> PP_Doc
vlist [PP_Doc]
rs)
                  forall a b. (PP a, PP b) => a -> b -> PP_Doc
>-< String
"Wait"    forall a b. (PP a, PP b) => a -> b -> PP_Doc
>-< forall a. PP a => Int -> a -> PP_Doc
indent Int
2 (forall a. PP a => [a] -> PP_Doc
vlist [PP_Doc]
wvs)
                  forall a b. (PP a, PP b) => a -> b -> PP_Doc
>-< String
"Stats"   forall a b. (PP a, PP b) => a -> b -> PP_Doc
>-< forall a. PP a => Int -> a -> PP_Doc
indent Int
2 (forall k v. (PP k, PP v) => AssocL k v -> PP_Doc
ppAssocLV [ (String
"Count of overall solve steps", forall a. PP a => a -> PP_Doc
pp Int
nrsteps) ])
                  forall a b. (PP a, PP b) => a -> b -> PP_Doc
>-< String
"Steps"   forall a b. (PP a, PP b) => a -> b -> PP_Doc
>-< forall a. PP a => Int -> a -> PP_Doc
indent Int
2 (forall a. PP a => [a] -> PP_Doc
vlist [PP_Doc]
ss)
               | Bool
otherwise = PP_Doc
Pretty.empty
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 
          String
"Subst"   forall a b. (PP a, PP b) => a -> b -> PP_Doc
>-< forall a. PP a => Int -> a -> PP_Doc
indent Int
2 (s
s forall vv subst. VarUpdatable vv subst => subst -> vv -> vv
`varUpd` s
s)
      forall a b. (PP a, PP b) => a -> b -> PP_Doc
>-< String
"Work"    forall a b. (PP a, PP b) => a -> b -> PP_Doc
>-< forall a. PP a => Int -> a -> PP_Doc
indent Int
2 (forall a. PP a => [a] -> PP_Doc
vlist [PP_Doc]
ws)
      forall a b. (PP a, PP b) => a -> b -> PP_Doc
>-< PP_Doc
pextra

-------------------------------------------------------------------------------------------
--- Solver: running it
-------------------------------------------------------------------------------------------

-- | Run and observe results
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 :: forall cnstr guard bprio prio subst env (m :: * -> *).
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 CHRGlobState cnstr guard bprio prio subst env m
gs CHRBackState cnstr bprio subst env
bs {- bp -} CHRMonoBacktrackPrioT
  cnstr guard bprio prio subst env m (SolverResult subst)
m = forall s (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(TransLogicState s t, Monad m) =>
s -> t m a -> m ([a], s)
observeStateAllT (CHRGlobState cnstr guard bprio prio subst env m
gs, CHRBackState cnstr bprio subst env
bs {- _chrbstBacktrackPrio=bp -}) CHRMonoBacktrackPrioT
  cnstr guard bprio prio subst env m (SolverResult subst)
m
{-# INLINABLE runCHRMonoBacktrackPrioT #-}

-------------------------------------------------------------------------------------------
--- Solver: Intermediate structures
-------------------------------------------------------------------------------------------

-- | Intermediate Solver structure
data FoundChr c g bp p
  = FoundChr
      { forall c g bp p. FoundChr c g bp p -> Int
foundChrInx             :: {-# UNPACK #-} !CHRInx
      , forall c g bp p. FoundChr c g bp p -> StoredCHR c g bp p
foundChrChr             :: !(StoredCHR c g bp p)
      , forall c g bp p. FoundChr c g bp p -> [Int]
foundChrCnstr           :: ![WorkInx]
      }

-- | Intermediate Solver structure
data FoundWorkInx c g bp p
  = FoundWorkInx
      { forall c g bp p. FoundWorkInx c g bp p -> CHRConstraintInx
foundWorkInxInx         :: {-# UNPACK #-} !CHRConstraintInx
      , forall c g bp p. FoundWorkInx c g bp p -> StoredCHR c g bp p
foundWorkInxChr         :: !(StoredCHR c g bp p)
      , forall c g bp p. FoundWorkInx c g bp p -> [[Int]]
foundWorkInxWorkInxs    :: ![[WorkInx]]
      }

-- | Intermediate Solver structure: sorting key for matches
data FoundMatchSortKey bp p s
  = FoundMatchSortKey
      { forall bp p s. FoundMatchSortKey bp p s -> Maybe (s, p)
foundMatchSortKeyPrio           :: !(Maybe (s,p))
      , forall bp p s. FoundMatchSortKey bp p s -> Int
foundMatchSortKeyWaitSize       :: {-# UNPACK #-} !Int
      , forall bp p s. FoundMatchSortKey bp p s -> Int
foundMatchSortKeyTextOrder      :: {-# UNPACK #-} !CHRInx
      }

instance Show (FoundMatchSortKey bp p s) where
  show :: FoundMatchSortKey bp p s -> String
show FoundMatchSortKey bp p s
_ = String
"FoundMatchSortKey"

instance (PP p, PP s) => PP (FoundMatchSortKey bp p s) where
  pp :: FoundMatchSortKey bp p s -> PP_Doc
pp (FoundMatchSortKey {foundMatchSortKeyPrio :: forall bp p s. FoundMatchSortKey bp p s -> Maybe (s, p)
foundMatchSortKeyPrio=Maybe (s, p)
p, foundMatchSortKeyWaitSize :: forall bp p s. FoundMatchSortKey bp p s -> Int
foundMatchSortKeyWaitSize=Int
w, foundMatchSortKeyTextOrder :: forall bp p s. FoundMatchSortKey bp p s -> Int
foundMatchSortKeyTextOrder=Int
o}) = forall a. PP a => [a] -> PP_Doc
ppParensCommas [forall a. PP a => a -> PP_Doc
pp Maybe (s, p)
p, forall a. PP a => a -> PP_Doc
pp Int
w, forall a. PP a => a -> PP_Doc
pp Int
o]

compareFoundMatchSortKey :: {- (Ord (CHRPrioEvaluatableVal bp)) => -} ((s,p) -> (s,p) -> Ordering) -> FoundMatchSortKey bp p s -> FoundMatchSortKey bp p s -> Ordering
compareFoundMatchSortKey :: forall s p bp.
((s, p) -> (s, p) -> Ordering)
-> FoundMatchSortKey bp p s -> FoundMatchSortKey bp p s -> Ordering
compareFoundMatchSortKey (s, p) -> (s, p) -> Ordering
cmp_rp (FoundMatchSortKey {- bp1 -} Maybe (s, p)
rp1 Int
ws1 Int
to1) (FoundMatchSortKey {- bp2 -} Maybe (s, p)
rp2 Int
ws2 Int
to2) =
    {- orderingLexic (bp1 `compare` bp2) $ -} Ordering -> Ordering -> Ordering
orderingLexic (Maybe (s, p)
rp1 Maybe (s, p) -> Maybe (s, p) -> Ordering
`cmp_mbrp` Maybe (s, p)
rp2) forall a b. (a -> b) -> a -> b
$ Ordering -> Ordering -> Ordering
orderingLexic (Int
ws1 forall a. Ord a => a -> a -> Ordering
`compare` Int
ws2) forall a b. (a -> b) -> a -> b
$ Int
to1 forall a. Ord a => a -> a -> Ordering
`compare` Int
to2
  where
    cmp_mbrp :: Maybe (s, p) -> Maybe (s, p) -> Ordering
cmp_mbrp (Just (s, p)
rp1) (Just (s, p)
rp2) = (s, p) -> (s, p) -> Ordering
cmp_rp (s, p)
rp1 (s, p)
rp2
    cmp_mbrp (Just (s, p)
_  ) Maybe (s, p)
_          = Ordering
GT
    cmp_mbrp Maybe (s, p)
_          (Just (s, p)
_  ) = Ordering
LT
    cmp_mbrp Maybe (s, p)
_          Maybe (s, p)
_          = Ordering
EQ

-- | Intermediate Solver structure: body alternative, together with index position
data FoundBodyAlt c bp
  = FoundBodyAlt
      { forall c bp. FoundBodyAlt c bp -> Int
foundBodyAltInx             :: {-# UNPACK #-} !Int
      , forall c bp. FoundBodyAlt c bp -> CHRPrioEvaluatableVal bp
foundBodyAltBacktrackPrio   :: !(CHRPrioEvaluatableVal bp)
      , forall c bp. FoundBodyAlt c bp -> RuleBodyAlt c bp
foundBodyAltAlt             :: !(RuleBodyAlt c bp)
      }

instance Show (FoundBodyAlt c bp) where
  show :: FoundBodyAlt c bp -> String
show FoundBodyAlt c bp
_ = String
"FoundBodyAlt"

instance (PP c, PP bp, PP (CHRPrioEvaluatableVal bp)) => PP (FoundBodyAlt c bp) where
  pp :: FoundBodyAlt c bp -> PP_Doc
pp (FoundBodyAlt {foundBodyAltInx :: forall c bp. FoundBodyAlt c bp -> Int
foundBodyAltInx=Int
i, foundBodyAltBacktrackPrio :: forall c bp. FoundBodyAlt c bp -> CHRPrioEvaluatableVal bp
foundBodyAltBacktrackPrio=CHRPrioEvaluatableVal bp
bp, foundBodyAltAlt :: forall c bp. FoundBodyAlt c bp -> RuleBodyAlt c bp
foundBodyAltAlt=RuleBodyAlt c bp
a}) = Int
i forall a b. (PP a, PP b) => a -> b -> PP_Doc
>|< String
":" forall a b. (PP a, PP b) => a -> b -> PP_Doc
>|< forall a. PP a => a -> PP_Doc
ppParens CHRPrioEvaluatableVal bp
bp forall a b. (PP a, PP b) => a -> b -> PP_Doc
>#< RuleBodyAlt c bp
a

-- | Intermediate Solver structure: all matched combis with their body alternatives + backtrack priorities
data FoundSlvMatch c g bp p s
  = FoundSlvMatch
      { forall c g bp p s. FoundSlvMatch c g bp p s -> s
foundSlvMatchSubst          :: !s                                   -- ^ the subst of rule meta vars making this a rule + work combi match
      , forall c g bp p s. FoundSlvMatch c g bp p s -> CHRWaitForVarSet s
foundSlvMatchFreeVars       :: !(CHRWaitForVarSet s)                -- ^ free meta vars of head
      , forall c g bp p s. FoundSlvMatch c g bp p s -> CHRWaitForVarSet s
foundSlvMatchWaitForVars    :: !(CHRWaitForVarSet s)                -- ^ for the work we try to solve the (global) vars on which we have to wait to continue
      , forall c g bp p s.
FoundSlvMatch c g bp p s -> FoundMatchSortKey bp p s
foundSlvMatchSortKey        :: !(FoundMatchSortKey bp p s)          -- ^ key to sort found matches
      , forall c g bp p s. FoundSlvMatch c g bp p s -> [FoundBodyAlt c bp]
foundSlvMatchBodyAlts       :: ![FoundBodyAlt c bp]                 -- ^ the body alternatives of the rule which matches
      }

instance Show (FoundSlvMatch c g bp p s) where
  show :: FoundSlvMatch c g bp p s -> String
show FoundSlvMatch c g bp p s
_ = String
"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 c g bp p s -> PP_Doc
pp (FoundSlvMatch {foundSlvMatchSubst :: forall c g bp p s. FoundSlvMatch c g bp p s -> s
foundSlvMatchSubst=s
s, foundSlvMatchWaitForVars :: forall c g bp p s. FoundSlvMatch c g bp p s -> CHRWaitForVarSet s
foundSlvMatchWaitForVars=Set (VarLookupKey s)
ws, foundSlvMatchBodyAlts :: forall c g bp p s. FoundSlvMatch c g bp p s -> [FoundBodyAlt c bp]
foundSlvMatchBodyAlts=[FoundBodyAlt c bp]
as}) = Set (VarLookupKey s)
ws forall a b. (PP a, PP b) => a -> b -> PP_Doc
>#< s
s forall a b. (PP a, PP b) => a -> b -> PP_Doc
>-< forall a. PP a => [a] -> PP_Doc
vlist [FoundBodyAlt c bp]
as

-- | Intermediate Solver structure: all matched combis with their backtrack prioritized body alternatives
data FoundWorkMatch c g bp p s
  = FoundWorkMatch
      { forall c g bp p s. FoundWorkMatch c g bp p s -> CHRConstraintInx
foundWorkMatchInx       :: {-# UNPACK #-} !CHRConstraintInx
      , forall c g bp p s. FoundWorkMatch c g bp p s -> StoredCHR c g bp p
foundWorkMatchChr       :: !(StoredCHR c g bp p)
      , forall c g bp p s. FoundWorkMatch c g bp p s -> [Int]
foundWorkMatchWorkInx   :: ![WorkInx]
      , forall c g bp p s.
FoundWorkMatch c g bp p s -> Maybe (FoundSlvMatch c g bp p s)
foundWorkMatchSlvMatch  :: !(Maybe (FoundSlvMatch c g bp p s))
      }

instance Show (FoundWorkMatch c g bp p s) where
  show :: FoundWorkMatch c g bp p s -> String
show FoundWorkMatch c g bp p s
_ = String
"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 c g bp p s -> PP_Doc
pp (FoundWorkMatch {foundWorkMatchSlvMatch :: forall c g bp p s.
FoundWorkMatch c g bp p s -> Maybe (FoundSlvMatch c g bp p s)
foundWorkMatchSlvMatch=Maybe (FoundSlvMatch c g bp p s)
sm}) = forall a. PP a => a -> PP_Doc
pp Maybe (FoundSlvMatch c g bp p s)
sm

-- | Intermediate Solver structure: all matched combis with their backtrack prioritized body alternatives
data FoundWorkSortedMatch c g bp p s
  = FoundWorkSortedMatch
      { forall c g bp p s.
FoundWorkSortedMatch c g bp p s -> CHRConstraintInx
foundWorkSortedMatchInx             :: !CHRConstraintInx
      , forall c g bp p s.
FoundWorkSortedMatch c g bp p s -> StoredCHR c g bp p
foundWorkSortedMatchChr             :: !(StoredCHR c g bp p)
      , forall c g bp p s.
FoundWorkSortedMatch c g bp p s -> [FoundBodyAlt c bp]
foundWorkSortedMatchBodyAlts        :: ![FoundBodyAlt c bp]
      , forall c g bp p s. FoundWorkSortedMatch c g bp p s -> [Int]
foundWorkSortedMatchWorkInx         :: ![WorkInx]
      , forall c g bp p s. FoundWorkSortedMatch c g bp p s -> s
foundWorkSortedMatchSubst           :: !s
      , forall c g bp p s.
FoundWorkSortedMatch c g bp p s -> CHRWaitForVarSet s
foundWorkSortedMatchFreeVars        :: !(CHRWaitForVarSet s)
      , forall c g bp p s.
FoundWorkSortedMatch c g bp p s -> CHRWaitForVarSet s
foundWorkSortedMatchWaitForVars     :: !(CHRWaitForVarSet s)
      }

instance Show (FoundWorkSortedMatch c g bp p s) where
  show :: FoundWorkSortedMatch c g bp p s -> String
show FoundWorkSortedMatch c g bp p s
_ = String
"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 c g bp p s -> PP_Doc
pp (FoundWorkSortedMatch {foundWorkSortedMatchBodyAlts :: forall c g bp p s.
FoundWorkSortedMatch c g bp p s -> [FoundBodyAlt c bp]
foundWorkSortedMatchBodyAlts=[FoundBodyAlt c bp]
as, foundWorkSortedMatchWorkInx :: forall c g bp p s. FoundWorkSortedMatch c g bp p s -> [Int]
foundWorkSortedMatchWorkInx=[Int]
wis, foundWorkSortedMatchSubst :: forall c g bp p s. FoundWorkSortedMatch c g bp p s -> s
foundWorkSortedMatchSubst=s
s, foundWorkSortedMatchWaitForVars :: forall c g bp p s.
FoundWorkSortedMatch c g bp p s -> CHRWaitForVarSet s
foundWorkSortedMatchWaitForVars=Set (VarLookupKey s)
wvs})
    = [Int]
wis forall a b. (PP a, PP b) => a -> b -> PP_Doc
>-< s
s forall a b. (PP a, PP b) => a -> b -> PP_Doc
>#< forall a. PP a => a -> PP_Doc
ppParens Set (VarLookupKey s)
wvs forall a b. (PP a, PP b) => a -> b -> PP_Doc
>-< forall a. PP a => [a] -> PP_Doc
vlist [FoundBodyAlt c bp]
as

-------------------------------------------------------------------------------------------
--- Solver options
-------------------------------------------------------------------------------------------

-- | Solve specific options
data CHRSolveOpts
  = CHRSolveOpts
      { CHRSolveOpts -> Bool
chrslvOptSucceedOnLeftoverWork  :: !Bool        -- ^ left over unresolvable (non residue) work is also a successful result
      , CHRSolveOpts -> Bool
chrslvOptSucceedOnFailedSolve   :: !Bool        -- ^ failed solve is considered also a successful result, with the failed constraint as a residue
      , CHRSolveOpts -> Bool
chrslvOptGatherDebugInfo        :: !Bool        -- ^ gather debug info
      , CHRSolveOpts -> Bool
chrslvOptGatherTraceInfo        :: !Bool        -- ^ gather trace info
      }

defaultCHRSolveOpts :: CHRSolveOpts
defaultCHRSolveOpts :: CHRSolveOpts
defaultCHRSolveOpts
  = CHRSolveOpts
      { chrslvOptSucceedOnLeftoverWork :: Bool
chrslvOptSucceedOnLeftoverWork  = Bool
False
      , chrslvOptSucceedOnFailedSolve :: Bool
chrslvOptSucceedOnFailedSolve   = Bool
False
      , chrslvOptGatherDebugInfo :: Bool
chrslvOptGatherDebugInfo        = Bool
False
      , chrslvOptGatherTraceInfo :: Bool
chrslvOptGatherTraceInfo        = Bool
False
      }

-------------------------------------------------------------------------------------------
--- Solver
-------------------------------------------------------------------------------------------

{-# INLINABLE chrSolve #-}
-- | (Under dev) solve
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 :: 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 CHRSolveOpts
opts e
env = LogicStateT
  (CHRGlobState c g bp p s e m)
  (CHRBackState c bp s e)
  m
  (SolverResult s)
slv
  where
    -- gather debug info
    dbg :: PP_Doc
-> LogicStateT
     (CHRGlobState c g bp p s e m) (CHRBackState c bp s e) m ()
dbg | CHRSolveOpts -> Bool
chrslvOptGatherDebugInfo CHRSolveOpts
opts = \PP_Doc
i -> forall cnstr guard bprio prio subst env (m :: * -> *).
Lens
  (CHRFullState cnstr guard bprio prio subst env m)
  (CHRBackState cnstr bprio subst env)
bst forall a b c. (a :-> b) -> (b :-> c) -> a :-> c
^* forall cnstr bprio subst env env.
Lens
  (CHRBackState cnstr bprio subst env)
  (CHRBackState cnstr bprio subst env)
  [SolverReductionStep]
  [SolverReductionStep]
chrbstReductionSteps forall f (m :: * -> *) o.
MonadState f m =>
(f :-> o) -> (o -> o) -> m ()
=$: (forall c w. PP_Doc -> SolverReductionStep' c w
SolverReductionDBG PP_Doc
i forall a. a -> [a] -> [a]
:)
        | Bool
otherwise                     = \PP_Doc
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
    -- gather trace info
    trc :: SolveStep' c (StoredCHR c g bp p) s
-> LogicStateT
     (CHRGlobState c g bp p s e m) (CHRBackState c bp s e) m ()
trc | CHRSolveOpts -> Bool
chrslvOptGatherTraceInfo CHRSolveOpts
opts = \SolveStep' c (StoredCHR c g bp p) s
i -> forall cnstr guard bprio prio subst env (m :: * -> *).
Lens
  (CHRFullState cnstr guard bprio prio subst env m)
  (CHRGlobState cnstr guard bprio prio subst env m)
gst forall a b c. (a :-> b) -> (b :-> c) -> a :-> c
^* forall cnstr guard bprio prio subst env (m :: * -> *).
Lens'
  (CHRGlobState cnstr guard bprio prio subst env m)
  (SolveTrace' cnstr (StoredCHR cnstr guard bprio prio) subst)
chrgstTrace forall f (m :: * -> *) o.
MonadState f m =>
(f :-> o) -> (o -> o) -> m ()
=$: (SolveStep' c (StoredCHR c g bp p) s
i forall a. a -> [a] -> [a]
:)
        | Bool
otherwise                     = \SolveStep' c (StoredCHR c g bp p) s
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
    -- leave this unconditional, does not seem not make a difference for performance
    -- trc i = gst ^* chrgstTrace =$: (i :)
    -- solve
    slv :: LogicStateT
  (CHRGlobState c g bp p s e m)
  (CHRBackState c bp s e)
  m
  (SolverResult s)
slv = do
        forall cnstr guard bprio prio subst env (m :: * -> *).
Lens
  (CHRFullState cnstr guard bprio prio subst env m)
  (CHRGlobState cnstr guard bprio prio subst env m)
gst forall a b c. (a :-> b) -> (b :-> c) -> a :-> c
^* forall cnstr guard bprio prio subst env (m :: * -> *).
Lens' (CHRGlobState cnstr guard bprio prio subst env m) Int
chrgstStatNrSolveSteps forall f (m :: * -> *) o.
MonadState f m =>
(f :-> o) -> (o -> o) -> m ()
=$: (forall a. Num a => a -> a -> a
+Int
1)
        Maybe Int
mbSlvWk <- forall c g bp p s e (m :: * -> *).
MonoBacktrackPrio c g bp p s e m =>
CHRMonoBacktrackPrioT c g bp p s e m (Maybe Int)
splitWorkFromSolveQueue
        case Maybe Int
mbSlvWk of
          -- There is work in the solve work queue
          Just (Int
workInx) -> do
              Work' (Key (TrTrKey c)) c
work <- forall c g bp p s e (m :: * -> *).
MonoBacktrackPrio c g bp p s e m =>
Int -> CHRMonoBacktrackPrioT c g bp p s e m (Work c)
lkupWork Int
workInx
              case Work' (Key (TrTrKey c)) c
work of
                Work' (Key (TrTrKey c)) c
Work_Fail -> forall c g bp p s e (m :: * -> *).
MonoBacktrackPrio c g bp p s e m =>
CHRMonoBacktrackPrioT c g bp p s e m (SolverResult s)
slvFail
                Work' (Key (TrTrKey c)) c
_ -> do
                  s
subst <- forall f (m :: * -> *) o. MonadState f m => (f :-> o) -> m o
getl forall a b. (a -> b) -> a -> b
$ forall cnstr guard bprio prio subst env (m :: * -> *).
Lens
  (CHRFullState cnstr guard bprio prio subst env m)
  (CHRBackState cnstr bprio subst env)
bst forall a b c. (a :-> b) -> (b :-> c) -> a :-> c
^* forall cnstr bprio subst env env.
Lens
  (CHRBackState cnstr bprio subst env)
  (CHRBackState cnstr bprio subst env)
  subst
  subst
chrbstSolveSubst
                  let mbSlv :: Maybe (s, Set (VarLookupKey s))
mbSlv = forall subst.
CHREmptySubstitution subst =>
CHRMatcher subst ()
-> CHRMatchEnv (VarLookupKey subst)
-> subst
-> Maybe (subst, CHRWaitForVarSet subst)
chrmatcherRun (forall env x subst.
CHRMatchable env x subst =>
env -> x -> CHRMatcher subst ()
chrBuiltinSolveM e
env forall a b. (a -> b) -> a -> b
$ forall k c. Work' k c -> c
workCnstr Work' (Key (TrTrKey c)) c
work) forall x. CHRMatchEnv x
emptyCHRMatchEnv s
subst
                  
                  -- debug info
                  PP_Doc
-> LogicStateT
     (CHRGlobState c g bp p s e m) (CHRBackState c bp s e) m ()
dbg forall a b. (a -> b) -> a -> b
$ 
                    (    String
"solve wk" forall a b. (PP a, PP b) => a -> b -> PP_Doc
>#< Work' (Key (TrTrKey c)) c
work
                     forall a b. (PP a, PP b) => a -> b -> PP_Doc
>-< String
"match" forall a b. (PP a, PP b) => a -> b -> PP_Doc
>#< Maybe (s, Set (VarLookupKey s))
mbSlv
                    )

                  case Maybe (s, Set (VarLookupKey s))
mbSlv of
                    Just (s
s,Set (VarLookupKey s)
_) -> do
                          -- the newfound subst may reactivate waiting work
                          forall c g bp p s e (m :: * -> *).
(MonoBacktrackPrio c g bp p s e m, Ord (VarLookupKey s)) =>
CHRWaitForVarSet s -> CHRMonoBacktrackPrioT c g bp p s e m [Int]
splitOffResolvedWaitForVarWork (forall c k v. (Lookup c k v, Ord k) => c -> Set k
Lk.keysSet s
s) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ forall c g bp p s e (m :: * -> *).
MonoBacktrackPrio c g bp p s e m =>
Int -> CHRMonoBacktrackPrioT c g bp p s e m ()
addToWorkQueue
                          forall cnstr guard bprio prio subst env (m :: * -> *).
Lens
  (CHRFullState cnstr guard bprio prio subst env m)
  (CHRBackState cnstr bprio subst env)
bst forall a b c. (a :-> b) -> (b :-> c) -> a :-> c
^* forall cnstr bprio subst env env.
Lens
  (CHRBackState cnstr bprio subst env)
  (CHRBackState cnstr bprio subst env)
  subst
  subst
chrbstSolveSubst forall f (m :: * -> *) o.
MonadState f m =>
(f :-> o) -> (o -> o) -> m ()
=$: (s
s forall l1 l2. LookupApply l1 l2 => l1 -> l2 -> l2
`Lk.apply`)
                          -- just continue with next work
                          LogicStateT
  (CHRGlobState c g bp p s e m)
  (CHRBackState c bp s e)
  m
  (SolverResult s)
slv
                    Maybe (s, Set (VarLookupKey s))
_ | CHRSolveOpts -> Bool
chrslvOptSucceedOnFailedSolve CHRSolveOpts
opts -> do
                          forall cnstr guard bprio prio subst env (m :: * -> *).
Lens
  (CHRFullState cnstr guard bprio prio subst env m)
  (CHRBackState cnstr bprio subst env)
bst forall a b c. (a :-> b) -> (b :-> c) -> a :-> c
^* forall cnstr bprio subst env env.
Lens
  (CHRBackState cnstr bprio subst env)
  (CHRBackState cnstr bprio subst env)
  [Int]
  [Int]
chrbstResidualQueue forall f (m :: * -> *) o.
MonadState f m =>
(f :-> o) -> (o -> o) -> m ()
=$: (Int
workInx forall a. a -> [a] -> [a]
:)
                          -- just continue with next work
                          LogicStateT
  (CHRGlobState c g bp p s e m)
  (CHRBackState c bp s e)
  m
  (SolverResult s)
slv
                      | Bool
otherwise -> do
                          forall c g bp p s e (m :: * -> *).
MonoBacktrackPrio c g bp p s e m =>
CHRMonoBacktrackPrioT c g bp p s e m (SolverResult s)
slvFail


          -- If no more solve work, continue with normal work
          Maybe Int
Nothing -> do
              WorkInxSet
waitingWk <- forall c g bp p s e (m :: * -> *).
MonoBacktrackPrio c g bp p s e m =>
CHRMonoBacktrackPrioT c g bp p s e m WorkInxSet
waitingInWorkQueue
              Set MatchedCombi
visitedChrWkCombis <- forall f (m :: * -> *) o. MonadState f m => (f :-> o) -> m o
getl forall a b. (a -> b) -> a -> b
$ forall cnstr guard bprio prio subst env (m :: * -> *).
Lens
  (CHRFullState cnstr guard bprio prio subst env m)
  (CHRBackState cnstr bprio subst env)
bst forall a b c. (a :-> b) -> (b :-> c) -> a :-> c
^* forall cnstr bprio subst env env.
Lens
  (CHRBackState cnstr bprio subst env)
  (CHRBackState cnstr bprio subst env)
  (Set MatchedCombi)
  (Set MatchedCombi)
chrbstMatchedCombis
              Maybe Int
mbWk <- forall c g bp p s e (m :: * -> *).
MonoBacktrackPrio c g bp p s e m =>
CHRMonoBacktrackPrioT c g bp p s e m (Maybe Int)
splitFromWorkQueue
              case Maybe Int
mbWk of
                -- If no more work, ready or cannot proceed
                Maybe Int
Nothing -> do
                    WorkInxSet
wr <- forall f (m :: * -> *) o. MonadState f m => (f :-> o) -> m o
getl forall a b. (a -> b) -> a -> b
$ forall cnstr guard bprio prio subst env (m :: * -> *).
Lens
  (CHRFullState cnstr guard bprio prio subst env m)
  (CHRBackState cnstr bprio subst env)
bst forall a b c. (a :-> b) -> (b :-> c) -> a :-> c
^* forall cnstr bprio subst env env.
Lens
  (CHRBackState cnstr bprio subst env)
  (CHRBackState cnstr bprio subst env)
  WorkQueue
  WorkQueue
chrbstRuleWorkQueue forall a b c. (a :-> b) -> (b :-> c) -> a :-> c
^* Lens' WorkQueue WorkInxSet
wkqueueRedo
                    if CHRSolveOpts -> Bool
chrslvOptSucceedOnLeftoverWork CHRSolveOpts
opts Bool -> Bool -> Bool
|| WorkInxSet -> Bool
IntSet.null WorkInxSet
wr
                      then forall c g bp p s e (m :: * -> *).
MonoBacktrackPrio c g bp p s e m =>
[Int] -> CHRMonoBacktrackPrioT c g bp p s e m (SolverResult s)
slvSucces forall a b. (a -> b) -> a -> b
$ WorkInxSet -> [Int]
IntSet.toList WorkInxSet
wr
                      else forall c g bp p s e (m :: * -> *).
MonoBacktrackPrio c g bp p s e m =>
CHRMonoBacktrackPrioT c g bp p s e m (SolverResult s)
slvFail
      
                -- There is work in the queue
                Just Int
workInx -> do
                    -- lookup the work
                    Work' (Key (TrTrKey c)) c
work  <- forall c g bp p s e (m :: * -> *).
MonoBacktrackPrio c g bp p s e m =>
Int -> CHRMonoBacktrackPrioT c g bp p s e m (Work c)
lkupWork  Int
workInx
                    -- work2 <- lkupWork workInx
          
                    -- find all matching chrs for the work
                    [CHRConstraintInx]
foundChrInxs  <- forall c g bp p s e (m :: * -> *) x.
(MonoBacktrackPrio c g bp p s e m, Ord (TrTrKey c)) =>
CHRKey c
-> Lens
     (CHRGlobState c g bp p s e m, CHRBackState c bp s e)
     (TreeTrie (TrTrKey c) [x])
-> CHRMonoBacktrackPrioT c g bp p s e m [x]
slvLookup  (forall k c. Work' k c -> k
workKey Work' (Key (TrTrKey c)) c
work ) (forall cnstr guard bprio prio subst env (m :: * -> *).
Lens
  (CHRFullState cnstr guard bprio prio subst env m)
  (CHRGlobState cnstr guard bprio prio subst env m)
gst forall a b c. (a :-> b) -> (b :-> c) -> a :-> c
^* forall cnstr guard bprio prio subst env (m :: * -> *).
Lens'
  (CHRGlobState cnstr guard bprio prio subst env m)
  (CHRStore cnstr guard bprio prio)
chrgstStore forall a b c. (a :-> b) -> (b :-> c) -> a :-> c
^* forall cnstr guard bprio prio.
Lens'
  (CHRStore cnstr guard bprio prio)
  (TreeTrie (TrTrKey cnstr) [CHRConstraintInx])
chrstoreTrie )
                    -- foundChrInxs2 <- slvLookup2 (workKey work2) (chrgstStore ^* chrstoreTrie2)
                    -- remove duplicates, regroup
                    let foundChrGroupedInxs :: Map Int (Set Int)
foundChrGroupedInxs = forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
(a -> a -> a) -> f (Map k a) -> Map k a
Map.unionsWith forall a. Ord a => Set a -> Set a -> Set a
Set.union forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (\(CHRConstraintInx Int
i Int
j) -> forall k a. k -> a -> Map k a
Map.singleton Int
i (forall a. a -> Set a
Set.singleton Int
j)) [CHRConstraintInx]
foundChrInxs
                    [FoundChr c g bp p]
foundChrs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (forall k a. Map k a -> [(k, a)]
Map.toList Map Int (Set Int)
foundChrGroupedInxs) forall a b. (a -> b) -> a -> b
$ \(Int
chrInx,Set Int
rlInxs) -> forall c g bp p s e (m :: * -> *).
MonoBacktrackPrio c g bp p s e m =>
Int -> CHRMonoBacktrackPrioT c g bp p s e m (StoredCHR c g bp p)
lkupChr Int
chrInx forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \StoredCHR c g bp p
chr -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall c g bp p.
Int -> StoredCHR c g bp p -> [Int] -> FoundChr c g bp p
FoundChr Int
chrInx StoredCHR c g bp p
chr forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
Set.toList Set Int
rlInxs

                    -- found chrs for the work correspond to 1 single position in the head, find all combinations with work in the queue
                    [FoundWorkInx c g bp p]
foundWorkInxs <- forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence
                      [ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall c g bp p.
CHRConstraintInx
-> StoredCHR c g bp p -> [[Int]] -> FoundWorkInx c g bp p
FoundWorkInx (Int -> Int -> CHRConstraintInx
CHRConstraintInx Int
ci Int
i) StoredCHR c g bp p
c) forall a b. (a -> b) -> a -> b
$ forall c g bp p s e (m :: * -> *).
MonoBacktrackPrio c g bp p s e m =>
WorkInxSet
-> Set MatchedCombi
-> Int
-> StoredCHR c g bp p
-> Int
-> CHRMonoBacktrackPrioT c g bp p s e m [[Int]]
slvCandidate WorkInxSet
waitingWk Set MatchedCombi
visitedChrWkCombis Int
workInx StoredCHR c g bp p
c Int
i
                      | FoundChr Int
ci StoredCHR c g bp p
c [Int]
is <- [FoundChr c g bp p]
foundChrs, Int
i <- [Int]
is
                      ]
          
                    -- each found combi has to match
                    [FoundWorkMatch c g bp p s]
foundWorkMatches <- forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall a b. (a -> b) -> a -> b
$
                      forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [FoundWorkInx c g bp p]
foundWorkInxs forall a b. (a -> b) -> a -> b
$ \(FoundWorkInx CHRConstraintInx
ci StoredCHR c g bp p
c [[Int]]
wis) -> do
                        forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [[Int]]
wis forall a b. (a -> b) -> a -> b
$ \[Int]
wi -> do
                          [Work' (Key (TrTrKey c)) c]
w <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Int]
wi forall c g bp p s e (m :: * -> *).
MonoBacktrackPrio c g bp p s e m =>
Int -> CHRMonoBacktrackPrioT c g bp p s e m (Work c)
lkupWork
                          forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall c g bp p s.
CHRConstraintInx
-> StoredCHR c g bp p
-> [Int]
-> Maybe (FoundSlvMatch c g bp p s)
-> FoundWorkMatch c g bp p s
FoundWorkMatch CHRConstraintInx
ci StoredCHR c g bp p
c [Int]
wi) forall a b. (a -> b) -> a -> b
$ 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 e
env StoredCHR c g bp p
c (forall a b. (a -> b) -> [a] -> [b]
map forall k c. Work' k c -> c
workCnstr [Work' (Key (TrTrKey c)) c]
w) (CHRConstraintInx -> Int
chrciAt CHRConstraintInx
ci)

                    -- split off the work which has to wait for variable bindings (as indicated by matching)
                    -- let () = partition () foundWorkMatches
                    -- sort over priorities
                    let foundWorkSortedMatches :: [(FoundMatchSortKey bp p s, FoundWorkSortedMatch c g bp p s)]
foundWorkSortedMatches = forall b a. (b -> b -> Ordering) -> (a -> b) -> [a] -> [a]
sortByOn (forall s p bp.
((s, p) -> (s, p) -> Ordering)
-> FoundMatchSortKey bp p s -> FoundMatchSortKey bp p s -> Ordering
compareFoundMatchSortKey forall a b. (a -> b) -> a -> b
$ forall env x subst.
CHRPrioEvaluatable env x subst =>
env -> (subst, x) -> (subst, x) -> Ordering
chrPrioCompare e
env) forall a b. (a, b) -> a
fst
                          [ (FoundMatchSortKey bp p s
k, forall c g bp p s.
CHRConstraintInx
-> StoredCHR c g bp p
-> [FoundBodyAlt c bp]
-> [Int]
-> s
-> CHRWaitForVarSet s
-> CHRWaitForVarSet s
-> FoundWorkSortedMatch c g bp p s
FoundWorkSortedMatch (forall c g bp p s. FoundWorkMatch c g bp p s -> CHRConstraintInx
foundWorkMatchInx FoundWorkMatch c g bp p s
fwm) (forall c g bp p s. FoundWorkMatch c g bp p s -> StoredCHR c g bp p
foundWorkMatchChr FoundWorkMatch c g bp p s
fwm) (forall c g bp p s. FoundSlvMatch c g bp p s -> [FoundBodyAlt c bp]
foundSlvMatchBodyAlts FoundSlvMatch c g bp p s
sm)
                                                     (forall c g bp p s. FoundWorkMatch c g bp p s -> [Int]
foundWorkMatchWorkInx FoundWorkMatch c g bp p s
fwm) (forall c g bp p s. FoundSlvMatch c g bp p s -> s
foundSlvMatchSubst FoundSlvMatch c g bp p s
sm) (forall c g bp p s. FoundSlvMatch c g bp p s -> CHRWaitForVarSet s
foundSlvMatchFreeVars FoundSlvMatch c g bp p s
sm) (forall c g bp p s. FoundSlvMatch c g bp p s -> CHRWaitForVarSet s
foundSlvMatchWaitForVars FoundSlvMatch c g bp p s
sm))
                          | fwm :: FoundWorkMatch c g bp p s
fwm@(FoundWorkMatch {foundWorkMatchSlvMatch :: forall c g bp p s.
FoundWorkMatch c g bp p s -> Maybe (FoundSlvMatch c g bp p s)
foundWorkMatchSlvMatch = Just sm :: FoundSlvMatch c g bp p s
sm@(FoundSlvMatch {foundSlvMatchSortKey :: forall c g bp p s.
FoundSlvMatch c g bp p s -> FoundMatchSortKey bp p s
foundSlvMatchSortKey=FoundMatchSortKey bp p s
k})}) <- [FoundWorkMatch c g bp p s]
foundWorkMatches
                          -- , (k,a) <- foundSlvMatchBodyAlts sm
                          ]

                    CHRPrioEvaluatableVal bp
bprio <- forall f (m :: * -> *) o. MonadState f m => (f :-> o) -> m o
getl forall a b. (a -> b) -> a -> b
$ forall cnstr guard bprio prio subst env (m :: * -> *).
Lens
  (CHRFullState cnstr guard bprio prio subst env m)
  (CHRBackState cnstr bprio subst env)
bst forall a b c. (a :-> b) -> (b :-> c) -> a :-> c
^* forall cnstr bprio subst env bprio env.
Lens
  (CHRBackState cnstr bprio subst env)
  (CHRBackState cnstr bprio subst env)
  (CHRPrioEvaluatableVal bprio)
  (CHRPrioEvaluatableVal bprio)
chrbstBacktrackPrio
                    s
subst <- forall f (m :: * -> *) o. MonadState f m => (f :-> o) -> m o
getl forall a b. (a -> b) -> a -> b
$ forall cnstr guard bprio prio subst env (m :: * -> *).
Lens
  (CHRFullState cnstr guard bprio prio subst env m)
  (CHRBackState cnstr bprio subst env)
bst forall a b c. (a :-> b) -> (b :-> c) -> a :-> c
^* forall cnstr bprio subst env env.
Lens
  (CHRBackState cnstr bprio subst env)
  (CHRBackState cnstr bprio subst env)
  subst
  subst
chrbstSolveSubst
                    Map (VarLookupKey s) [WaitForVar s]
dbgWaitInfo <- forall f (m :: * -> *) o. MonadState f m => (f :-> o) -> m o
getl forall a b. (a -> b) -> a -> b
$ forall cnstr guard bprio prio subst env (m :: * -> *).
Lens
  (CHRFullState cnstr guard bprio prio subst env m)
  (CHRBackState cnstr bprio subst env)
bst forall a b c. (a :-> b) -> (b :-> c) -> a :-> c
^* forall cnstr bprio subst env env.
Lens
  (CHRBackState cnstr bprio subst env)
  (CHRBackState cnstr bprio subst env)
  (Map (VarLookupKey subst) [WaitForVar subst])
  (Map (VarLookupKey subst) [WaitForVar subst])
chrbstWaitForVar
                    -- sque <- getl $ gst ^* chrgstScheduleQueue
                    -- debug info
                    PP_Doc
-> LogicStateT
     (CHRGlobState c g bp p s e m) (CHRBackState c bp s e) m ()
dbg forall a b. (a -> b) -> a -> b
$          String
"bprio" forall a b. (PP a, PP b) => a -> b -> PP_Doc
>#< CHRPrioEvaluatableVal bp
bprio
                               forall a b. (PP a, PP b) => a -> b -> PP_Doc
>-< String
"wk" forall a b. (PP a, PP b) => a -> b -> PP_Doc
>#< (Work' (Key (TrTrKey c)) c
work forall a b. (PP a, PP b) => a -> b -> PP_Doc
>-< s
subst forall vv subst. VarUpdatable vv subst => subst -> vv -> vv
`varUpd` forall k c. Work' k c -> c
workCnstr Work' (Key (TrTrKey c)) c
work)
                               forall a b. (PP a, PP b) => a -> b -> PP_Doc
>-< String
"que" forall a b. (PP a, PP b) => a -> b -> PP_Doc
>#< forall a. PP a => [a] -> PP_Doc
ppBracketsCommas (WorkInxSet -> [Int]
IntSet.toList WorkInxSet
waitingWk)
                               forall a b. (PP a, PP b) => a -> b -> PP_Doc
>-< String
"subst" forall a b. (PP a, PP b) => a -> b -> PP_Doc
>#< s
subst
                               forall a b. (PP a, PP b) => a -> b -> PP_Doc
>-< String
"wait" forall a b. (PP a, PP b) => a -> b -> PP_Doc
>#< forall k v. (PP k, PP v) => AssocL k v -> PP_Doc
ppAssocL (forall v v' k. (v -> v') -> AssocL k v -> AssocL k v'
assocLMapElt (forall k v. (PP k, PP v) => AssocL k v -> PP_Doc
ppAssocL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (\WaitForVar s
i -> (forall s. WaitForVar s -> Int
_waitForVarWorkInx WaitForVar s
i, forall a. PP a => [a] -> PP_Doc
ppCommas forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
Set.toList forall a b. (a -> b) -> a -> b
$ forall s. WaitForVar s -> CHRWaitForVarSet s
_waitForVarVars WaitForVar s
i))) forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [(k, a)]
Map.toList Map (VarLookupKey s) [WaitForVar s]
dbgWaitInfo)
                               forall a b. (PP a, PP b) => a -> b -> PP_Doc
>-< String
"visited" forall a b. (PP a, PP b) => a -> b -> PP_Doc
>#< forall a. PP a => [a] -> PP_Doc
ppBracketsCommas (forall a. Set a -> [a]
Set.toList Set MatchedCombi
visitedChrWkCombis)
                               forall a b. (PP a, PP b) => a -> b -> PP_Doc
>-< String
"chrs" forall a b. (PP a, PP b) => a -> b -> PP_Doc
>#< forall a. PP a => [a] -> PP_Doc
vlist [ Int
ci forall a b. (PP a, PP b) => a -> b -> PP_Doc
>|< forall a. PP a => [a] -> PP_Doc
ppParensCommas [Int]
is forall a b. (PP a, PP b) => a -> b -> PP_Doc
>|< String
":" forall a b. (PP a, PP b) => a -> b -> PP_Doc
>#< StoredCHR c g bp p
c | FoundChr Int
ci StoredCHR c g bp p
c [Int]
is <- [FoundChr c g bp p]
foundChrs ]
                               forall a b. (PP a, PP b) => a -> b -> PP_Doc
>-< String
"works" forall a b. (PP a, PP b) => a -> b -> PP_Doc
>#< forall a. PP a => [a] -> PP_Doc
vlist [ CHRConstraintInx
ci forall a b. (PP a, PP b) => a -> b -> PP_Doc
>|< String
":" forall a b. (PP a, PP b) => a -> b -> PP_Doc
>#< forall a. PP a => [a] -> PP_Doc
vlist (forall a b. (a -> b) -> [a] -> [b]
map forall a. PP a => [a] -> PP_Doc
ppBracketsCommas [[Int]]
ws) | FoundWorkInx CHRConstraintInx
ci StoredCHR c g bp p
c [[Int]]
ws <- [FoundWorkInx c g bp p]
foundWorkInxs ]
                               forall a b. (PP a, PP b) => a -> b -> PP_Doc
>-< String
"matches" forall a b. (PP a, PP b) => a -> b -> PP_Doc
>#< forall a. PP a => [a] -> PP_Doc
vlist [ CHRConstraintInx
ci forall a b. (PP a, PP b) => a -> b -> PP_Doc
>|< String
":" forall a b. (PP a, PP b) => a -> b -> PP_Doc
>#< forall a. PP a => [a] -> PP_Doc
ppBracketsCommas [Int]
wi forall a b. (PP a, PP b) => a -> b -> PP_Doc
>#< String
":" forall a b. (PP a, PP b) => a -> b -> PP_Doc
>#< Maybe (FoundSlvMatch c g bp p s)
mbm | FoundWorkMatch CHRConstraintInx
ci StoredCHR c g bp p
_ [Int]
wi Maybe (FoundSlvMatch c g bp p s)
mbm <- [FoundWorkMatch c g bp p s]
foundWorkMatches ]
                               -- >-< "prio'd" >#< (vlist $ zipWith (\g ms -> g >|< ":" >#< vlist [ ci >|< ":" >#< ppBracketsCommas wi >#< ":" >#< s | (ci,_,wi,s) <- ms ]) [0::Int ..] foundWorkMatchesFilteredPriod)
                               -- >-< "prio'd" >#< ppAssocL (zip [0::Int ..] $ map ppAssocL foundWorkSortedMatches)

                    -- pick the first and highest rule prio solution
                    case [(FoundMatchSortKey bp p s, FoundWorkSortedMatch c g bp p s)]
foundWorkSortedMatches of
                      ((FoundMatchSortKey bp p s
_,fwsm :: FoundWorkSortedMatch c g bp p s
fwsm@(FoundWorkSortedMatch {foundWorkSortedMatchWaitForVars :: forall c g bp p s.
FoundWorkSortedMatch c g bp p s -> CHRWaitForVarSet s
foundWorkSortedMatchWaitForVars = Set (VarLookupKey s)
waitForVars})):[(FoundMatchSortKey bp p s, FoundWorkSortedMatch c g bp p s)]
_)
                        | forall a. Set a -> Bool
Set.null Set (VarLookupKey s)
waitForVars -> do
                            -- addRedoToWorkQueue workInx
                            forall c g bp p s e (m :: * -> *).
MonoBacktrackPrio c g bp p s e m =>
Int -> CHRMonoBacktrackPrioT c g bp p s e m ()
addToWorkQueue Int
workInx
                            CHRPrioEvaluatableVal bp
-> FoundWorkSortedMatch c g bp p s
-> LogicStateT
     (CHRGlobState c g bp p s e m)
     (CHRBackState c bp s e)
     m
     (SolverResult s)
slv1 CHRPrioEvaluatableVal bp
bprio FoundWorkSortedMatch c g bp p s
fwsm
                        | Bool
otherwise -> do
                            -- put on wait queue if there are unresolved variables
                            forall c g bp p s e (m :: * -> *).
(MonoBacktrackPrio c g bp p s e m, Ord (VarLookupKey s)) =>
CHRWaitForVarSet s
-> Int -> CHRMonoBacktrackPrioT c g bp p s e m ()
addWorkToWaitForVarQueue Set (VarLookupKey s)
waitForVars Int
workInx
                            -- continue without reschedule
                            LogicStateT
  (CHRGlobState c g bp p s e m)
  (CHRBackState c bp s e)
  m
  (SolverResult s)
slv
                      [(FoundMatchSortKey bp p s, FoundWorkSortedMatch c g bp p s)]
_ -> do
                            forall c g bp p s e (m :: * -> *).
MonoBacktrackPrio c g bp p s e m =>
Int -> CHRMonoBacktrackPrioT c g bp p s e m ()
addRedoToWorkQueue Int
workInx
                            LogicStateT
  (CHRGlobState c g bp p s e m)
  (CHRBackState c bp s e)
  m
  (SolverResult s)
slv
{-
                      _ | chrslvOptSucceedOnLeftoverWork opts -> do
                            -- no chr applies for this work, so consider it to be residual
                            bst ^* chrbstLeftWorkQueue =$: (workInx :)
                            -- continue without reschedule
                            slv
                        | otherwise -> do
                            -- no chr applies for this work, can never be resolved, consider this a failure unless prevented by option
                            slvFail
-}

    -- solve one step further, allowing a backtrack point here
    slv1 :: CHRPrioEvaluatableVal bp
-> FoundWorkSortedMatch c g bp p s
-> LogicStateT
     (CHRGlobState c g bp p s e m)
     (CHRBackState c bp s e)
     m
     (SolverResult s)
slv1 CHRPrioEvaluatableVal bp
curbprio
         (FoundWorkSortedMatch
            { foundWorkSortedMatchInx :: forall c g bp p s.
FoundWorkSortedMatch c g bp p s -> CHRConstraintInx
foundWorkSortedMatchInx = CHRConstraintInx {chrciInx :: CHRConstraintInx -> Int
chrciInx = Int
ci}
            , foundWorkSortedMatchChr :: forall c g bp p s.
FoundWorkSortedMatch c g bp p s -> StoredCHR c g bp p
foundWorkSortedMatchChr = chr :: StoredCHR c g bp p
chr@StoredCHR {_storedChrRule :: forall c g bp p. StoredCHR c g bp p -> Rule c g bp p
_storedChrRule = Rule {ruleSimpSz :: forall cnstr guard bprio prio. Rule cnstr guard bprio prio -> Int
ruleSimpSz = Int
simpSz}}
            , foundWorkSortedMatchBodyAlts :: forall c g bp p s.
FoundWorkSortedMatch c g bp p s -> [FoundBodyAlt c bp]
foundWorkSortedMatchBodyAlts = [FoundBodyAlt c bp]
alts
            , foundWorkSortedMatchWorkInx :: forall c g bp p s. FoundWorkSortedMatch c g bp p s -> [Int]
foundWorkSortedMatchWorkInx = [Int]
workInxs
            , foundWorkSortedMatchSubst :: forall c g bp p s. FoundWorkSortedMatch c g bp p s -> s
foundWorkSortedMatchSubst = s
matchSubst
            , foundWorkSortedMatchFreeVars :: forall c g bp p s.
FoundWorkSortedMatch c g bp p s -> CHRWaitForVarSet s
foundWorkSortedMatchFreeVars = Set (VarLookupKey s)
freeHeadVars
            }) = do
        -- remove the simplification part from the work queue
        forall c g bp p s e (m :: * -> *).
MonoBacktrackPrio c g bp p s e m =>
WorkInxSet -> CHRMonoBacktrackPrioT c g bp p s e m ()
deleteFromWorkQueue forall a b. (a -> b) -> a -> b
$ [Int] -> WorkInxSet
IntSet.fromList forall a b. (a -> b) -> a -> b
$ forall a. Int -> [a] -> [a]
take Int
simpSz [Int]
workInxs
        -- depending on nr of alts continue slightly different
        case [FoundBodyAlt c bp]
alts of
          -- just continue if no alts 
          [] -> do
            Maybe (FoundBodyAlt c bp)
-> LogicStateT
     (CHRGlobState c g bp p s e m) (CHRBackState c bp s e) m ()
log forall a. Maybe a
Nothing
            LogicStateT
  (CHRGlobState c g bp p s e m)
  (CHRBackState c bp s e)
  m
  (SolverResult s)
slv
          -- just reschedule
          [alt :: FoundBodyAlt c bp
alt@(FoundBodyAlt {foundBodyAltBacktrackPrio :: forall c bp. FoundBodyAlt c bp -> CHRPrioEvaluatableVal bp
foundBodyAltBacktrackPrio=CHRPrioEvaluatableVal bp
bprio})]
            | CHRPrioEvaluatableVal bp
curbprio forall a. Eq a => a -> a -> Bool
== CHRPrioEvaluatableVal bp
bprio -> do
                Maybe (FoundBodyAlt c bp)
-> LogicStateT
     (CHRGlobState c g bp p s e m) (CHRBackState c bp s e) m ()
log (forall a. a -> Maybe a
Just FoundBodyAlt c bp
alt)
                CHRPrioEvaluatableVal bp
-> FoundBodyAlt c bp
-> LogicStateT
     (CHRGlobState c g bp p s e m)
     (CHRBackState c bp s e)
     m
     (SolverResult s)
nextwork CHRPrioEvaluatableVal bp
bprio FoundBodyAlt c bp
alt
            | Bool
otherwise -> do
                Maybe (FoundBodyAlt c bp)
-> LogicStateT
     (CHRGlobState c g bp p s e m) (CHRBackState c bp s e) m ()
log (forall a. a -> Maybe a
Just FoundBodyAlt c bp
alt)
                forall c g bp p s e (m :: * -> *).
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 CHRPrioEvaluatableVal bp
bprio forall a b. (a -> b) -> a -> b
$ CHRPrioEvaluatableVal bp
-> FoundBodyAlt c bp
-> LogicStateT
     (CHRGlobState c g bp p s e m)
     (CHRBackState c bp s e)
     m
     (SolverResult s)
nextwork CHRPrioEvaluatableVal bp
bprio FoundBodyAlt c bp
alt
                forall c g bp p s e (m :: * -> *).
MonoBacktrackPrio c g bp p s e m =>
CHRMonoBacktrackPrioT c g bp p s e m (SolverResult s)
slvScheduleRun
          -- otherwise backtrack and schedule all and then reschedule
          [FoundBodyAlt c bp]
alts -> do
                forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [FoundBodyAlt c bp]
alts forall a b. (a -> b) -> a -> b
$ \alt :: FoundBodyAlt c bp
alt@(FoundBodyAlt {foundBodyAltBacktrackPrio :: forall c bp. FoundBodyAlt c bp -> CHRPrioEvaluatableVal bp
foundBodyAltBacktrackPrio=CHRPrioEvaluatableVal bp
bprio}) -> do
                  Maybe (FoundBodyAlt c bp)
-> LogicStateT
     (CHRGlobState c g bp p s e m) (CHRBackState c bp s e) m ()
log (forall a. a -> Maybe a
Just FoundBodyAlt c bp
alt)
                  (forall (f :: * -> * -> *) gs bs (ms :: * -> *) (m :: * -> *) a.
MonadLogicState f gs bs ms m =>
(gs -> bs -> bs -> ms bs) -> m a -> m (m a)
backtrackWithRoll (\CHRGlobState c g bp p s e m
_ CHRBackState c bp s e
_ CHRBackState c bp s e
bs -> {- (liftIO $ putStrLn "TEST") >> -} forall (m :: * -> *) a. Monad m => a -> m a
return CHRBackState c bp s e
bs) forall a b. (a -> b) -> a -> b
$ CHRPrioEvaluatableVal bp
-> FoundBodyAlt c bp
-> LogicStateT
     (CHRGlobState c g bp p s e m)
     (CHRBackState c bp s e)
     m
     (SolverResult s)
nextwork CHRPrioEvaluatableVal bp
bprio FoundBodyAlt c bp
alt) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall c g bp p s e (m :: * -> *).
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 CHRPrioEvaluatableVal bp
bprio
                forall c g bp p s e (m :: * -> *).
MonoBacktrackPrio c g bp p s e m =>
CHRMonoBacktrackPrioT c g bp p s e m (SolverResult s)
slvScheduleRun

      where
        log :: Maybe (FoundBodyAlt c bp)
-> LogicStateT
     (CHRGlobState c g bp p s e m) (CHRBackState c bp s e) m ()
log Maybe (FoundBodyAlt c bp)
alt = do
          let a :: Maybe [c]
a = (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall cnstr bprio. RuleBodyAlt cnstr bprio -> [cnstr]
rbodyaltBody forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall c bp. FoundBodyAlt c bp -> RuleBodyAlt c bp
foundBodyAltAlt) Maybe (FoundBodyAlt c bp)
alt)
          SolveStep' c (StoredCHR c g bp p) s
-> LogicStateT
     (CHRGlobState c g bp p s e m) (CHRBackState c bp s e) m ()
trc forall a b. (a -> b) -> a -> b
$ forall c r s. r -> s -> Maybe [c] -> [c] -> [c] -> SolveStep' c r s
SolveStep StoredCHR c g bp p
chr s
matchSubst Maybe [c]
a [] [] -- TODO: Set stepNewTodo, stepNewDone (last two arguments)
        nextwork :: CHRPrioEvaluatableVal bp
-> FoundBodyAlt c bp
-> LogicStateT
     (CHRGlobState c g bp p s e m)
     (CHRBackState c bp s e)
     m
     (SolverResult s)
nextwork CHRPrioEvaluatableVal bp
bprio alt :: FoundBodyAlt c bp
alt@(FoundBodyAlt {foundBodyAltAlt :: forall c bp. FoundBodyAlt c bp -> RuleBodyAlt c bp
foundBodyAltAlt=(RuleBodyAlt {rbodyaltBody :: forall cnstr bprio. RuleBodyAlt cnstr bprio -> [cnstr]
rbodyaltBody=[c]
body})}) = do
          -- set prio for this alt
          forall cnstr guard bprio prio subst env (m :: * -> *).
Lens
  (CHRFullState cnstr guard bprio prio subst env m)
  (CHRBackState cnstr bprio subst env)
bst forall a b c. (a :-> b) -> (b :-> c) -> a :-> c
^* forall cnstr bprio subst env bprio env.
Lens
  (CHRBackState cnstr bprio subst env)
  (CHRBackState cnstr bprio subst env)
  (CHRPrioEvaluatableVal bprio)
  (CHRPrioEvaluatableVal bprio)
chrbstBacktrackPrio forall f (m :: * -> *) o. MonadState f m => (f :-> o) -> o -> m ()
=: CHRPrioEvaluatableVal bp
bprio
          -- fresh vars for unbound body metavars
          s
freshSubst <- 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 (ExtrValVarKey x)
-> x -> CHRMonoBacktrackPrioT c g bp p s e m s
slvFreshSubst Set (VarLookupKey s)
freeHeadVars [c]
body
          -- add each constraint from the body, applying the meta var subst
          [(ConstraintSolvesVia, Int)]
newWkInxs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [c]
body forall a b. (a -> b) -> a -> b
$ forall c g bp p s e (m :: * -> *).
MonoBacktrackPrio c g bp p s e m =>
c
-> CHRMonoBacktrackPrioT c g bp p s e m (ConstraintSolvesVia, Int)
addConstraintAsWork forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((s
freshSubst forall l1 l2. LookupApply l1 l2 => l1 -> l2 -> l2
`Lk.apply` s
matchSubst) forall vv subst. VarUpdatable vv subst => subst -> vv -> vv
`varUpd`)
          -- mark this combi of chr and work as visited
          let matchedCombi :: MatchedCombi
matchedCombi = forall c w. c -> [w] -> MatchedCombi' c w
MatchedCombi Int
ci [Int]
workInxs
          forall cnstr guard bprio prio subst env (m :: * -> *).
Lens
  (CHRFullState cnstr guard bprio prio subst env m)
  (CHRBackState cnstr bprio subst env)
bst forall a b c. (a :-> b) -> (b :-> c) -> a :-> c
^* forall cnstr bprio subst env env.
Lens
  (CHRBackState cnstr bprio subst env)
  (CHRBackState cnstr bprio subst env)
  (Set MatchedCombi)
  (Set MatchedCombi)
chrbstMatchedCombis forall f (m :: * -> *) o.
MonadState f m =>
(f :-> o) -> (o -> o) -> m ()
=$: forall a. Ord a => a -> Set a -> Set a
Set.insert MatchedCombi
matchedCombi
          -- add this reduction step as being taken
          forall cnstr guard bprio prio subst env (m :: * -> *).
Lens
  (CHRFullState cnstr guard bprio prio subst env m)
  (CHRBackState cnstr bprio subst env)
bst forall a b c. (a :-> b) -> (b :-> c) -> a :-> c
^* forall cnstr bprio subst env env.
Lens
  (CHRBackState cnstr bprio subst env)
  (CHRBackState cnstr bprio subst env)
  [SolverReductionStep]
  [SolverReductionStep]
chrbstReductionSteps forall f (m :: * -> *) o.
MonadState f m =>
(f :-> o) -> (o -> o) -> m ()
=$: (forall c w.
MatchedCombi' c w
-> Int -> Map ConstraintSolvesVia [w] -> SolverReductionStep' c w
SolverReductionStep MatchedCombi
matchedCombi (forall c bp. FoundBodyAlt c bp -> Int
foundBodyAltInx FoundBodyAlt c bp
alt) (forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
(a -> a -> a) -> f (Map k a) -> Map k a
Map.unionsWith forall a. [a] -> [a] -> [a]
(++) forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (\(ConstraintSolvesVia
k,Int
v) -> forall k a. k -> a -> Map k a
Map.singleton ConstraintSolvesVia
k [Int
v]) forall a b. (a -> b) -> a -> b
$ [(ConstraintSolvesVia, Int)]
newWkInxs) forall a. a -> [a] -> [a]
:)
          -- take next step
          LogicStateT
  (CHRGlobState c g bp p s e m)
  (CHRBackState c bp s e)
  m
  (SolverResult s)
slv

    -- misc utils

-- | Fresh variables in the form of a subst
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 :: 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 (ExtrValVarKey x)
-> x -> CHRMonoBacktrackPrioT c g bp p s e m s
slvFreshSubst Set (ExtrValVarKey x)
except x
x = 
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall l1 l2. LookupApply l1 l2 => l1 -> l2 -> l2
Lk.apply forall c k v. Lookup c k v => c
Lk.empty) forall a b. (a -> b) -> a -> b
$
      forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (forall a. Set a -> [a]
Set.toList forall a b. (a -> b) -> a -> b
$ forall vv. VarExtractable vv => vv -> Set (ExtrValVarKey vv)
varFreeSet x
x forall a. Ord a => Set a -> Set a -> Set a
`Set.difference` Set (ExtrValVarKey x)
except) forall a b. (a -> b) -> a -> b
$ \ExtrValVarKey bp
v ->
        forall f (m :: * -> *) o a.
MonadState f m =>
(f :-> o) -> (o -> (a, o)) -> m a
modifyAndGet (forall cnstr guard bprio prio subst env (m :: * -> *).
Lens
  (CHRFullState cnstr guard bprio prio subst env m)
  (CHRBackState cnstr bprio subst env)
bst forall a b c. (a :-> b) -> (b :-> c) -> a :-> c
^* forall cnstr bprio subst env env.
Lens
  (CHRBackState cnstr bprio subst env)
  (CHRBackState cnstr bprio subst env)
  Int
  Int
chrbstFreshVar) (forall fs f. Fresh fs f => Maybe f -> fs -> (f, fs)
freshWith forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just ExtrValVarKey bp
v) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ExtrValVarKey bp
v' -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ (forall c k v. Lookup c k v => k -> v -> c
Lk.singleton ExtrValVarKey bp
v (forall vv. VarTerm vv => ExtrValVarKey vv -> vv
varTermMkKey ExtrValVarKey bp
v') :: s)
{-# INLINE slvFreshSubst #-}

-- | Lookup work in a store part of the global state
slvLookup
  :: ( MonoBacktrackPrio c g bp p s e m
     , Ord (TT.TrTrKey c)
     ) => CHRKey c                                   -- ^ work key
       -> 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 :: forall c g bp p s e (m :: * -> *) x.
(MonoBacktrackPrio c g bp p s e m, Ord (TrTrKey c)) =>
CHRKey c
-> Lens
     (CHRGlobState c g bp p s e m, CHRBackState c bp s e)
     (TreeTrie (TrTrKey c) [x])
-> CHRMonoBacktrackPrioT c g bp p s e m [x]
slvLookup CHRKey c
key Lens
  (CHRGlobState c g bp p s e m, CHRBackState c bp s e)
  (TreeTrie (TrTrKey c) [x])
t =
    (forall f (m :: * -> *) o. MonadState f m => (f :-> o) -> m o
getl Lens
  (CHRGlobState c g bp p s e m, CHRBackState c bp s e)
  (TreeTrie (TrTrKey c) [x])
t) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \TreeTrie (TrTrKey c) [x]
t -> do
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall a b. (a -> b) -> a -> b
$ forall v. LkRes v -> [v]
TT.lookupResultToList forall a b. (a -> b) -> a -> b
$ forall k v. Ord k => Key k -> TreeTrie k v -> LkRes v
TT.lookup CHRKey c
key TreeTrie (TrTrKey c) [x]
t
{-# INLINE slvLookup #-}

-- | Extract candidates matching a CHRKey.
--   Return a list of CHR matches,
--     each match expressed as the list of constraints (in the form of Work + Key) found in the workList wlTrie, thus giving all combis with constraints as part of a CHR,
--     partititioned on before or after last query time (to avoid work duplication later)
slvCandidate
  :: forall c g bp p s e m
   . ( MonoBacktrackPrio c g bp p s e m
     ) => WorkInxSet                           -- ^ active in queue
       -> Set.Set MatchedCombi                      -- ^ already matched combis
       -> WorkInx                                   -- ^ work inx
       -> StoredCHR c g bp p                        -- ^ found chr for the work
       -> Int                                       -- ^ position in the head where work was found
       -> CHRMonoBacktrackPrioT c g bp p s e m
            ( [[WorkInx]]                           -- All matches of the head, unfiltered w.r.t. deleted work
            )
slvCandidate :: forall c g bp p s e (m :: * -> *).
MonoBacktrackPrio c g bp p s e m =>
WorkInxSet
-> Set MatchedCombi
-> Int
-> StoredCHR c g bp p
-> Int
-> CHRMonoBacktrackPrioT c g bp p s e m [[Int]]
slvCandidate WorkInxSet
waitingWk Set MatchedCombi
alreadyMatchedCombis Int
wi (StoredCHR {_storedHeadKeys :: forall c g bp p. StoredCHR c g bp p -> [CHRKey c]
_storedHeadKeys = [CHRKey c]
ks, _storedChrInx :: forall c g bp p. StoredCHR c g bp p -> Int
_storedChrInx = Int
ci}) Int
headInx = do
    let [[CHRKey c]
ks1,[CHRKey c]
_,[CHRKey c]
ks2] = forall e. [Int] -> [e] -> [[e]]
splitPlaces [Int
headInx, Int
headInxforall a. Num a => a -> a -> a
+Int
1] [CHRKey c]
ks
    [[Int]]
ws1 <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [CHRKey c]
ks1 forall {s} {c} {e} {g} {bp} {p} {m :: * -> *}.
(ExtrValVarKey (VarLookupVal s) ~ VarLookupKey s,
 TreeTrieKeyable c, IsConstraint c, CHRCheckable e g s,
 VarUpdatable c s, VarUpdatable g s, CHRMatchable e c s,
 CHRMatchable e bp s, CHRPrioEvaluatable e bp s,
 CHRPrioEvaluatable e p s, Typeable c, Typeable g, Typeable bp,
 Typeable p, PP c, PP g, PP bp, PP p, PP (TrTrKey c),
 PP (CHRPrioEvaluatableVal bp), PP (VarLookupKey s), Monad m,
 Lookup s (VarLookupKey s) (VarLookupVal s),
 Fresh Int (ExtrValVarKey (VarLookupVal s)),
 VarTerm (VarLookupVal s), VarExtractable g, Ord c,
 Ord (TrTrKey c)) =>
Key (TrTrKey c) -> CHRMonoBacktrackPrioT c g bp p s e m [Int]
lkup
    [[Int]]
ws2 <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [CHRKey c]
ks2 forall {s} {c} {e} {g} {bp} {p} {m :: * -> *}.
(ExtrValVarKey (VarLookupVal s) ~ VarLookupKey s,
 TreeTrieKeyable c, IsConstraint c, CHRCheckable e g s,
 VarUpdatable c s, VarUpdatable g s, CHRMatchable e c s,
 CHRMatchable e bp s, CHRPrioEvaluatable e bp s,
 CHRPrioEvaluatable e p s, Typeable c, Typeable g, Typeable bp,
 Typeable p, PP c, PP g, PP bp, PP p, PP (TrTrKey c),
 PP (CHRPrioEvaluatableVal bp), PP (VarLookupKey s), Monad m,
 Lookup s (VarLookupKey s) (VarLookupVal s),
 Fresh Int (ExtrValVarKey (VarLookupVal s)),
 VarTerm (VarLookupVal s), VarExtractable g, Ord c,
 Ord (TrTrKey c)) =>
Key (TrTrKey c) -> CHRMonoBacktrackPrioT c g bp p s e m [Int]
lkup
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> [a] -> [a]
filter (\[Int]
wi ->    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Int -> WorkInxSet -> Bool
`IntSet.member` WorkInxSet
waitingWk) [Int]
wi
                            Bool -> Bool -> Bool
&& forall a. Ord a => a -> Set a -> Bool
Set.notMember (forall c w. c -> [w] -> MatchedCombi' c w
MatchedCombi Int
ci [Int]
wi) Set MatchedCombi
alreadyMatchedCombis)
           forall a b. (a -> b) -> a -> b
$ forall e. (e -> e -> Bool) -> [[e]] -> [[e]]
combineToDistinguishedEltsBy forall a. Eq a => a -> a -> Bool
(==) forall a b. (a -> b) -> a -> b
$ [[Int]]
ws1 forall a. [a] -> [a] -> [a]
++ [[Int
wi]] forall a. [a] -> [a] -> [a]
++ [[Int]]
ws2
  where
    -- lkup :: CHRKey c -> CHRMonoBacktrackPrioT c g bp p s e m [WorkInx]
    lkup :: Key (TrTrKey c) -> CHRMonoBacktrackPrioT c g bp p s e m [Int]
lkup Key (TrTrKey c)
k = forall c g bp p s e (m :: * -> *) x.
(MonoBacktrackPrio c g bp p s e m, Ord (TrTrKey c)) =>
CHRKey c
-> Lens
     (CHRGlobState c g bp p s e m, CHRBackState c bp s e)
     (TreeTrie (TrTrKey c) [x])
-> CHRMonoBacktrackPrioT c g bp p s e m [x]
slvLookup Key (TrTrKey c)
k (forall cnstr guard bprio prio subst env (m :: * -> *).
Lens
  (CHRFullState cnstr guard bprio prio subst env m)
  (CHRBackState cnstr bprio subst env)
bst forall a b c. (a :-> b) -> (b :-> c) -> a :-> c
^* forall cnstr bprio subst env cnstr env.
Lens
  (CHRBackState cnstr bprio subst env)
  (CHRBackState cnstr bprio subst env)
  (WorkStore cnstr)
  (WorkStore cnstr)
chrbstWorkStore forall a b c. (a :-> b) -> (b :-> c) -> a :-> c
^* forall cnstr.
Lens' (WorkStore cnstr) (TreeTrie (TrTrKey cnstr) [Int])
wkstoreTrie)
{-# INLINE slvCandidate #-}

-- | Match the stored CHR with a set of possible constraints, giving a substitution on success
slvMatch
  :: forall c g bp p s env m
   . ( MonoBacktrackPrio c g bp p s env m
     -- these below should not be necessary as they are implied (via superclasses) by MonoBacktrackPrio, but deeper nested superclasses seem not to be picked up...
     , CHRMatchable env c s
     , CHRCheckable env g s
     , CHRMatchable env bp s
     , CHRPrioEvaluatable env bp s
     ) => env
       -> StoredCHR c g bp p
       -> [c]
       -> Int                                       -- ^ position in the head where work was found, on that work specifically we might have to wait
       -> CHRMonoBacktrackPrioT c g bp p s env m (Maybe (FoundSlvMatch c g bp p s))
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
env chr :: StoredCHR c g bp p
chr@(StoredCHR {_storedChrRule :: forall c g bp p. StoredCHR c g bp p -> Rule c g bp p
_storedChrRule = Rule {rulePrio :: forall cnstr guard bprio prio.
Rule cnstr guard bprio prio -> Maybe prio
rulePrio = Maybe p
mbpr, ruleHead :: forall cnstr guard bprio prio.
Rule cnstr guard bprio prio -> [cnstr]
ruleHead = [c]
hc, ruleGuard :: forall cnstr guard bprio prio.
Rule cnstr guard bprio prio -> [guard]
ruleGuard = [g]
gd, ruleBacktrackPrio :: forall cnstr guard bprio prio.
Rule cnstr guard bprio prio -> Maybe bprio
ruleBacktrackPrio = Maybe bp
mbbpr, ruleBodyAlts :: forall cnstr guard bprio prio.
Rule cnstr guard bprio prio -> [RuleBodyAlt cnstr bprio]
ruleBodyAlts = [RuleBodyAlt c bp]
alts}}) [c]
cnstrs Int
headInx = do
    s
subst <- forall f (m :: * -> *) o. MonadState f m => (f :-> o) -> m o
getl forall a b. (a -> b) -> a -> b
$ forall cnstr guard bprio prio subst env (m :: * -> *).
Lens
  (CHRFullState cnstr guard bprio prio subst env m)
  (CHRBackState cnstr bprio subst env)
bst forall a b c. (a :-> b) -> (b :-> c) -> a :-> c
^* forall cnstr bprio subst env env.
Lens
  (CHRBackState cnstr bprio subst env)
  (CHRBackState cnstr bprio subst env)
  subst
  subst
chrbstSolveSubst
    bp
curbprio <- forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall env x subst (proxy :: * -> *).
CHRPrioEvaluatable env x subst =>
proxy env -> proxy subst -> CHRPrioEvaluatableVal x -> x
chrPrioLift (forall {k} (t :: k). Proxy t
Proxy :: Proxy env) (forall {k} (t :: k). Proxy t
Proxy :: Proxy s)) forall a b. (a -> b) -> a -> b
$ forall f (m :: * -> *) o. MonadState f m => (f :-> o) -> m o
getl forall a b. (a -> b) -> a -> b
$ forall cnstr guard bprio prio subst env (m :: * -> *).
Lens
  (CHRFullState cnstr guard bprio prio subst env m)
  (CHRBackState cnstr bprio subst env)
bst forall a b c. (a :-> b) -> (b :-> c) -> a :-> c
^* forall cnstr bprio subst env bprio env.
Lens
  (CHRBackState cnstr bprio subst env)
  (CHRBackState cnstr bprio subst env)
  (CHRPrioEvaluatableVal bprio)
  (CHRPrioEvaluatableVal bprio)
chrbstBacktrackPrio
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(s
s,Set (ExtrValVarKey bp)
ws) -> forall c g bp p s.
s
-> CHRWaitForVarSet s
-> CHRWaitForVarSet s
-> FoundMatchSortKey bp p s
-> [FoundBodyAlt c bp]
-> FoundSlvMatch c g bp p s
FoundSlvMatch s
s Set (ExtrValVarKey bp)
freevars Set (ExtrValVarKey bp)
ws (forall bp p s.
Maybe (s, p) -> Int -> Int -> FoundMatchSortKey bp p s
FoundMatchSortKey (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((,) s
s) Maybe p
mbpr) (forall a. Set a -> Int
Set.size Set (ExtrValVarKey bp)
ws) (forall c g bp p. StoredCHR c g bp p -> Int
_storedChrInx StoredCHR c g bp p
chr))
                    [ forall c bp.
Int
-> CHRPrioEvaluatableVal bp
-> RuleBodyAlt c bp
-> FoundBodyAlt c bp
FoundBodyAlt Int
i CHRPrioEvaluatableVal bp
bp RuleBodyAlt c bp
a | (Int
i,RuleBodyAlt c bp
a) <- forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] [RuleBodyAlt c bp]
alts, let bp :: CHRPrioEvaluatableVal bp
bp = forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. Bounded a => a
minBound (forall env x subst.
CHRPrioEvaluatable env x subst =>
env -> subst -> x -> CHRPrioEvaluatableVal x
chrPrioEval env
env s
s) forall a b. (a -> b) -> a -> b
$ forall cnstr bprio. RuleBodyAlt cnstr bprio -> Maybe bprio
rbodyaltBacktrackPrio RuleBodyAlt c bp
a
                    ])
           forall a b. (a -> b) -> a -> b
$ (\StateT
  (StackedVarLookup s, Set (VarLookupKey s),
   CHRMatchEnv (VarLookupKey s))
  (Either CHRMatcherFailure)
  ()
m -> forall subst.
CHREmptySubstitution subst =>
CHRMatcher subst ()
-> CHRMatchEnv (VarLookupKey subst)
-> subst
-> Maybe (subst, CHRWaitForVarSet subst)
chrmatcherRun StateT
  (StackedVarLookup s, Set (VarLookupKey s),
   CHRMatchEnv (VarLookupKey s))
  (Either CHRMatcherFailure)
  ()
m (forall x. CHRMatchEnv x
emptyCHRMatchEnv {chrmatchenvMetaMayBind :: ExtrValVarKey bp -> Bool
chrmatchenvMetaMayBind = (forall a. Ord a => a -> Set a -> Bool
`Set.member` Set (ExtrValVarKey bp)
freevars)}) s
subst)
           forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_
           forall a b. (a -> b) -> a -> b
$ bp
-> [StateT
      (StackedVarLookup s, Set (VarLookupKey s),
       CHRMatchEnv (VarLookupKey s))
      (Either CHRMatcherFailure)
      ()]
prio bp
curbprio forall a. [a] -> [a] -> [a]
++ [StateT
   (StackedVarLookup s, Set (VarLookupKey s),
    CHRMatchEnv (VarLookupKey s))
   (Either CHRMatcherFailure)
   ()]
matches forall a. [a] -> [a] -> [a]
++ [StateT
   (StackedVarLookup s, Set (VarLookupKey s),
    CHRMatchEnv (VarLookupKey s))
   (Either CHRMatcherFailure)
   ()]
checks
  where
    prio :: bp
-> [StateT
      (StackedVarLookup s, Set (VarLookupKey s),
       CHRMatchEnv (VarLookupKey s))
      (Either CHRMatcherFailure)
      ()]
prio bp
curbprio = forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] (\bp
bpr -> [forall env x subst.
CHRMatchable env x subst =>
env -> x -> x -> CHRMatcher subst ()
chrMatchToM env
env bp
bpr bp
curbprio]) Maybe bp
mbbpr
    matches :: [StateT
   (StackedVarLookup s, Set (VarLookupKey s),
    CHRMatchEnv (VarLookupKey s))
   (Either CHRMatcherFailure)
   ()]
matches = forall a b c d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
zipWith3 (\Int
i c
h c
c -> forall env x subst.
CHRMatchable env x subst =>
Bool -> env -> x -> x -> CHRMatcher subst ()
chrMatchAndWaitToM (Int
i forall a. Eq a => a -> a -> Bool
== Int
headInx) env
env c
h c
c) [Int
0::Int ..] [c]
hc [c]
cnstrs
    -- ignoreWait 
    checks :: [StateT
   (StackedVarLookup s, Set (VarLookupKey s),
    CHRMatchEnv (VarLookupKey s))
   (Either CHRMatcherFailure)
   ()]
checks  = forall a b. (a -> b) -> [a] -> [b]
map (forall env x subst.
CHRCheckable env x subst =>
env -> x -> CHRMatcher subst ()
chrCheckM env
env) [g]
gd
    freevars :: Set (ExtrValVarKey bp)
freevars = forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions [forall vv. VarExtractable vv => vv -> Set (ExtrValVarKey vv)
varFreeSet [c]
hc, forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. Set a
Set.empty forall vv. VarExtractable vv => vv -> Set (ExtrValVarKey vv)
varFreeSet Maybe bp
mbbpr]
{-# INLINE slvMatch #-}