diff --git a/ChangeLog.md b/ChangeLog.md new file mode 100644 --- /dev/null +++ b/ChangeLog.md @@ -0,0 +1,5 @@ +# Revision history for chr + +## 0.1.0.0 -- YYYY-mm-dd + +* First version. Released on an unsuspecting world. diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,30 @@ +Copyright (c) 2017, Atze Dijkstra + +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are met: + + * Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + + * Redistributions in binary form must reproduce the above + copyright notice, this list of conditions and the following + disclaimer in the documentation and/or other materials provided + with the distribution. + + * Neither the name of Atze Dijkstra nor the names of other + contributors may be used to endorse or promote products derived + from this software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT +OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, +SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT +LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, +DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY +THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT +(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE +OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -0,0 +1,1 @@ +# Core solving part of CHR libraries diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/chr-core.cabal b/chr-core.cabal new file mode 100644 --- /dev/null +++ b/chr-core.cabal @@ -0,0 +1,56 @@ +-- Initial chr.cabal generated by cabal init. For further documentation, +-- see http://haskell.org/cabal/users-guide/ + +name: chr-core +version: 0.1.0.0 +synopsis: Constraint Handling Rules +description: Constraint Handling Rules evaluation engine +license: BSD3 +license-file: LICENSE +author: Atze Dijkstra +maintainer: atzedijkstra@gmail.com +Homepage: https://github.com/atzedijkstra/chr +Bug-Reports: https://github.com/atzedijkstra/chr/issues +-- copyright: +category: Control +build-type: Simple +extra-source-files: ChangeLog.md, README.md +cabal-version: >=1.10 + +source-repository head + type: git + location: git@github.com:atzedijkstra/chr.git + +library + exposed-modules: + CHR.Solve.MonoBacktrackPrio, + CHR.Types, + CHR.Types.Rule, + CHR.Types.Core + other-modules: + + -- other-extensions: + default-extensions: + NoMagicHash, + DeriveGeneric, + DeriveDataTypeable, + TypeFamilies, + FlexibleContexts, + FunctionalDependencies, + FlexibleInstances, + RankNTypes + build-depends: + base >=4.9 && < 5, + -- array >= 0.3, + hashable >= 1.2.4, + unordered-containers >= 0.2.7, + containers >= 0.4, + mtl >= 2, + pqueue >= 1.3.1, + -- vector >= 0.11, + -- fclabels >= 2.0.3, + chr-data >= 0.1.0.0, + chr-pretty >= 0.1.0.0, + logict-state >= 0.1.0.4 + hs-source-dirs: src + default-language: Haskell2010 diff --git a/src/CHR/Solve/MonoBacktrackPrio.hs b/src/CHR/Solve/MonoBacktrackPrio.hs new file mode 100644 --- /dev/null +++ b/src/CHR/Solve/MonoBacktrackPrio.hs @@ -0,0 +1,1156 @@ +{-# 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 + -- , addRule2 + + , addConstraintAsWork + + , SolverResult(..) + , ppSolverResult + + , CHRSolveOpts(..) + , defaultCHRSolveOpts + + , StoredCHR + , storedChrRule' + + , chrSolve + + , slvFreshSubst + + , getSolveTrace + + , IsCHRSolvable(..) + ) + where + +import CHR.Utils +import CHR.Data.Lens +import CHR.Data.Lookup (Lookup, LookupApply, Scoped) +import qualified CHR.Data.Lookup as Lk +import qualified CHR.Data.TreeTrie as TT +import CHR.Data.VarLookup + +import qualified Data.Set as Set +import qualified Data.PQueue.Prio.Min as Que +import qualified Data.Map.Strict as Map +import qualified Data.HashMap.Strict as MapH +import qualified Data.IntMap.Strict as IntMap +import qualified Data.IntSet as IntSet +import qualified Data.Sequence as Seq +import Data.List as List +import Data.Typeable +import Data.Maybe + +import Control.Monad +import Control.Monad.Except +import Control.Monad.State.Strict +import Control.Monad.LogicState + +import CHR.Pretty as Pretty +-- import UHC.Util.Serialize +import CHR.Types.Core +import CHR.Types.Rule +import CHR.Data.Substitutable +import CHR.Data.AssocL +import CHR.Data.Fresh +-- +-- import UHC.Util.Debug + +import CHR.Types + +------------------------------------------------------------------------------------------- +--- Verbosity +------------------------------------------------------------------------------------------- + +data Verbosity + = Verbosity_Quiet -- default + | Verbosity_Normal + | Verbosity_Debug + | Verbosity_ALot + deriving (Eq, Ord, Show, 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 + { chrciInx :: {-# UNPACK #-} !CHRInx + , chrciAt :: {-# UNPACK #-} !Int + } + deriving (Eq, Ord, Show) + +instance PP CHRConstraintInx where + pp (CHRConstraintInx i j) = i >|< "." >|< j + +-- | A CHR as stored in a CHRStore, requiring additional info for efficiency +data StoredCHR c g bp p + = StoredCHR + { _storedHeadKeys :: ![CHRKey c] -- ^ the keys corresponding to the head of the rule + , _storedChrRule :: !(Rule c g bp p) -- ^ the rule + , _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' = _storedChrRule + +-- | A CHR store is a trie structure +data CHRStore cnstr guard bprio prio + = CHRStore + { _chrstoreTrie :: TT.TreeTrie (TT.TrTrKey cnstr) [CHRConstraintInx] -- ^ map from the search key of a rule to the index into tabl + , _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 = CHRStore TT.empty IntMap.empty + +------------------------------------------------------------------------------------------- +--- Store holding work, split up in global and backtrackable part +------------------------------------------------------------------------------------------- + +type WorkInx = WorkTime + +type WorkInxSet = IntSet.IntSet + +data WorkStore cnstr + = WorkStore + { _wkstoreTrie :: !(TT.TreeTrie (TT.TrTrKey cnstr) [WorkInx]) -- ^ map from the search key of a constraint to index in table + , _wkstoreTable :: !(IntMap.IntMap (Work cnstr)) -- ^ all the work ever entered. FIXME: do GC + , _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 = WorkStore TT.empty IntMap.empty initWorkTime + +data WorkQueue + = WorkQueue + { _wkqueueActive :: !WorkInxSet -- ^ active queue, work will be taken off from this one + , _wkqueueRedo :: !WorkInxSet -- ^ redo queue, holding work which could not immediately be reduced, but later on might be + , _wkqueueDidSomething :: !Bool -- ^ flag indicating some work was done; if False and active queue is empty we stop solving + } + deriving (Typeable) + +emptyWorkQueue :: WorkQueue +emptyWorkQueue = WorkQueue IntSet.empty IntSet.empty True + +------------------------------------------------------------------------------------------- +--- A matched combi of chr and work +------------------------------------------------------------------------------------------- + +-- | Already matched combi of chr and work +data MatchedCombi' c w = + MatchedCombi + { mcCHR :: !c -- ^ the CHR + , mcWork :: ![w] -- ^ the work matched for this CHR + } + deriving (Eq, Ord) + +instance Show (MatchedCombi' c w) where + show _ = "MatchedCombi" + +instance (PP c, PP w) => PP (MatchedCombi' c w) where + pp (MatchedCombi c ws) = ppParensCommas [pp c, ppBracketsCommas ws] + +type MatchedCombi = MatchedCombi' CHRInx WorkInx + +------------------------------------------------------------------------------------------- +--- Solver reduction step +------------------------------------------------------------------------------------------- + +-- | Description of 1 chr reduction step taken by the solver +data SolverReductionStep' c w + = SolverReductionStep + { slvredMatchedCombi :: !(MatchedCombi' c w) + , slvredChosenBodyAltInx :: {-# UNPACK #-} !Int + , slvredNewWork :: !(Map.Map ConstraintSolvesVia [w]) + } + | SolverReductionDBG PP_Doc + +type SolverReductionStep = SolverReductionStep' CHRInx WorkInx + +instance Show (SolverReductionStep' c w) where + show _ = "SolverReductionStep" + +instance {-# OVERLAPPABLE #-} (PP c, PP w) => PP (SolverReductionStep' c w) where + pp (SolverReductionStep (MatchedCombi ci ws) a wns) = "STEP" >#< ci >|< "." >|< a >-< indent 2 ("+" >#< ppBracketsCommas ws >-< "-> (new)" >#< (ppAssocL $ Map.toList $ Map.map ppBracketsCommas wns)) -- (ppBracketsCommas wns >-< ppBracketsCommas wnbs) + pp (SolverReductionDBG p) = "DBG" >#< p + +instance (PP w) => PP (SolverReductionStep' Int w) where + pp (SolverReductionStep (MatchedCombi ci ws) a wns) = ci >|< "." >|< a >#< "+" >#< ppBracketsCommas ws >#< "-> (new)" >#< (ppAssocL $ Map.toList $ Map.map ppBracketsCommas wns) -- (ppBracketsCommas wns >-< ppBracketsCommas wnbs) + pp (SolverReductionDBG p) = "DBG" >#< p + +------------------------------------------------------------------------------------------- +--- Waiting (for var resolution) work +------------------------------------------------------------------------------------------- + +-- | Admin for waiting work +data WaitForVar s + = WaitForVar + { _waitForVarVars :: !(CHRWaitForVarSet s) + , _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 + { _chrgstStore :: !(CHRStore cnstr guard bprio prio) -- ^ Actual database of rules, to be searched + , _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. + -- , _chrgstWorkStore :: !(WorkStore cnstr) -- ^ Actual database of solvable constraints + -- , _chrgstNextFreeWorkInx :: {-# UNPACK #-} !WorkTime -- ^ Next free work/constraint identification, used by solving to identify whether a rule has been used for a constraint. + , _chrgstScheduleQueue :: !(Que.MinPQueue (CHRPrioEvaluatableVal bprio) (CHRMonoBacktrackPrioT cnstr guard bprio prio subst env m (SolverResult subst))) + , _chrgstTrace :: !(SolveTrace' cnstr (StoredCHR cnstr guard bprio prio) subst) + , _chrgstStatNrSolveSteps :: {-# UNPACK #-} !Int + , _chrgstVarToNmMp :: !VarToNmMp + } + deriving (Typeable) + +emptyCHRGlobState :: TT.TTCtxt (TT.TrTrKey c) => CHRGlobState c g b p s e m +emptyCHRGlobState = CHRGlobState emptyCHRStore 0 Que.empty emptySolveTrace 0 emptyVarToNmMp + +-- | Backtrackable state +data CHRBackState cnstr bprio subst env + = CHRBackState + { _chrbstBacktrackPrio :: !(CHRPrioEvaluatableVal bprio) -- ^ the current backtrack prio the solver runs on + + , _chrbstRuleWorkQueue :: !WorkQueue -- ^ work queue for rule matching + , _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 + , _chrbstResidualQueue :: [WorkInx] -- ^ residual queue, constraints which are residual, no need to solve, etc + , _chrbstWorkStore :: !(WorkStore cnstr) -- ^ Actual database of solvable constraints + + , _chrbstMatchedCombis :: !(Set.Set MatchedCombi) -- ^ all combis of chr + work which were reduced, to prevent this from happening a second time (when propagating) + + , _chrbstFreshVar :: {-# UNPACK #-} !Int -- ^ for fresh var + , _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) + , _chrbstWaitForVar :: !(Map.Map (VarLookupKey subst) [WaitForVar subst]) -- ^ work waiting for a var to be bound + + , _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 = CHRBackState minBound emptyWorkQueue emptyWorkQueue [] emptyWorkStore Set.empty 0 chrEmptySubst 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 = fstl +{-# INLINE gst #-} + +bst :: Lens (CHRFullState cnstr guard bprio prio subst env m) (CHRBackState cnstr bprio subst env) +bst = sndl +{-# INLINE bst #-} + +-- | All required behavior, as alias +{- +class ( IsCHRSolvable env cnstr guard bprio prio subst + , Monad m + , Lookup subst (VarLookupKey subst) (VarLookupVal subst) + , LookupApply subst subst + , Fresh Int (ExtrValVarKey (VarLookupVal subst)) + , ExtrValVarKey (VarLookupVal subst) ~ VarLookupKey subst + , VarTerm (VarLookupVal subst) + ) => MonoBacktrackPrio cnstr guard bprio prio subst env m +-} +type MonoBacktrackPrio cnstr guard bprio prio subst env m + = ( IsCHRSolvable env cnstr guard bprio prio subst + , Monad m + , Lookup subst (VarLookupKey subst) (VarLookupVal subst) + , LookupApply subst subst + , Fresh Int (ExtrValVarKey (VarLookupVal subst)) + , ExtrValVarKey (VarLookupVal subst) ~ VarLookupKey subst + , VarTerm (VarLookupVal subst) + ) + +------------------------------------------------------------------------------------------- +--- Solver result +------------------------------------------------------------------------------------------- + +-- | Solver solution +data SolverResult subst = + SolverResult + { slvresSubst :: !subst -- ^ global found variable bindings + , slvresResidualCnstr :: ![WorkInx] -- ^ constraints which are residual, no need to solve, etc, leftover when ready, taken from backtrack state + , slvresWorkCnstr :: ![WorkInx] -- ^ constraints which are still unsolved, taken from backtrack state + , slvresWaitVarCnstr :: ![WorkInx] -- ^ constraints which are still unsolved, waiting for variable resolution + , 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 +{- +class ( IsCHRConstraint env c s + , IsCHRGuard env g s + , IsCHRBacktrackPrio env bp s + , IsCHRPrio env p s + , PP (VarLookupKey s) + ) => IsCHRSolvable env c g bp p s +-} +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 = fmap (ppSolveTrace . reverse) $ getl $ gst ^* chrgstTrace + +------------------------------------------------------------------------------------------- +--- CHR store, API for adding rules +------------------------------------------------------------------------------------------- + +instance Show (StoredCHR c g bp p) where + show _ = "StoredCHR" + +ppStoredCHR :: (PP (TT.TrTrKey c), PP c, PP g, PP bp, PP p) => StoredCHR c g bp p -> PP_Doc +ppStoredCHR c@(StoredCHR {}) + = ppParensCommas (_storedHeadKeys c) + >-< _storedChrRule c + >-< indent 2 + (ppParensCommas + [ pp $ _storedChrInx c + -- , 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 = 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 chr = do + i <- modifyAndGet (gst ^* chrgstNextFreeRuleInx) $ \i -> (i, i + 1) + let ks = map TT.toTreeTrieKey $ ruleHead chr + gst ^* chrgstStore ^* chrstoreTable =$: IntMap.insert i (StoredCHR ks chr i) + gst ^* chrgstStore ^* chrstoreTrie =$: \t -> + foldr (TT.unionWith (++)) t [ TT.singleton k [CHRConstraintInx i j] | (k,c,j) <- zip3 ks (ruleHead chr) [0..] ] + return () + + +-- | 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 i = do + bst ^* chrbstRuleWorkQueue ^* wkqueueActive =$: (IntSet.insert i) + bst ^* chrbstRuleWorkQueue ^* wkqueueDidSomething =: 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 i = do + bst ^* chrbstRuleWorkQueue ^* wkqueueRedo =$: (IntSet.insert 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 wfvs wi = do + let w = WaitForVar wfvs wi + bst ^* chrbstWaitForVar =$: Map.unionWith (++) (Map.fromList [(v,[w]) | v <- Set.toList 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 vars = do + -- wait admin + wm <- getl $ bst ^* chrbstWaitForVar + let -- split off the part which can be released + (wmRelease,wmRemain) = Map.partitionWithKey (\v _ -> Set.member v vars) wm + wfvs = concat $ Map.elems wmRelease + -- get all influenced vars and released work + (wvars, winxs) = (\(vss,wis) -> (Set.unions vss, IntSet.fromList wis)) $ unzip [ (vs,wi) | (WaitForVar {_waitForVarVars=vs, _waitForVarWorkInx=wi}) <- wfvs ] + -- remove released work from remaining admin for influenced vars + bst ^* chrbstWaitForVar =: + foldr (Map.alter $ maybe Nothing $ \wfvs -> case filter (\i -> _waitForVarWorkInx i `IntSet.notMember` winxs) wfvs of + [] -> Nothing + wfvs' -> Just wfvs' + ) + wmRemain + (Set.toList wvars) + + -- released work + return $ IntSet.toList 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 i = do + bst ^* chrbstSolveQueue ^* wkqueueActive =$: (IntSet.insert 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 = do + wq <- getl $ bst ^* chrbstSolveQueue ^* wkqueueActive + case IntSet.minView wq of + Nothing -> + return Nothing + Just (workInx, wq') -> do + bst ^* chrbstSolveQueue ^* wkqueueActive =: wq' + return $ Just (workInx) + +-- | 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 is = do + -- bst ^* chrbstRuleWorkQueue ^* wkqueueActive =$: (\s -> foldr (IntSet.delete) s is) + bst ^* chrbstRuleWorkQueue ^* wkqueueActive =$: flip IntSet.difference is + bst ^* chrbstRuleWorkQueue ^* wkqueueRedo =$: flip IntSet.difference 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 = do + a <- getl $ bst ^* chrbstRuleWorkQueue ^* wkqueueActive + r <- getl $ bst ^* chrbstRuleWorkQueue ^* wkqueueRedo + return $ IntSet.union a 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 = do + wq <- getl $ bst ^* chrbstRuleWorkQueue ^* wkqueueActive + case IntSet.minView wq of + -- If no more work, ready if nothing was done anymore + Nothing -> do + did <- modifyAndGet (bst ^* chrbstRuleWorkQueue ^* wkqueueDidSomething) $ \d -> (d, False) + if did -- && not (IntSet.null wr) + then do + wr <- modifyAndGet (bst ^* chrbstRuleWorkQueue ^* wkqueueRedo) $ \r -> (r, IntSet.empty) + bst ^* chrbstRuleWorkQueue ^* wkqueueActive =: wr + splitFromWorkQueue + else + return Nothing + + -- There is work in the queue + Just (workInx, wq') -> do + bst ^* chrbstRuleWorkQueue ^* wkqueueActive =: wq' + return $ Just 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 c = do + let via = cnstrSolvesVia c + addw i w = do + bst ^* chrbstWorkStore ^* wkstoreTable =$: IntMap.insert i w + return (via,i) + i <- fresh + w <- case via of + -- a plain rule is added to the work store + ConstraintSolvesVia_Rule -> do + bst ^* chrbstWorkStore ^* wkstoreTrie =$: TT.insertByKeyWith (++) k [i] + addToWorkQueue i + return $ Work k c i + where k = TT.toTreeTrieKey c -- chrToKey c -- chrToWorkKey c + -- work for the solver is added to its own queue + ConstraintSolvesVia_Solve -> do + addWorkToSolveQueue i + return $ Work_Solve c + -- residue is just remembered + ConstraintSolvesVia_Residual -> do + bst ^* chrbstResidualQueue =$: (i :) + return $ Work_Residue c + -- fail right away if this constraint is a fail constraint + ConstraintSolvesVia_Fail -> do + addWorkToSolveQueue i + return Work_Fail + addw i w +{- + -- succeed right away if this constraint is a succes constraint + -- TBD, different return value of slvSucces... + ConstraintSolvesVia_Succeed -> do + slvSucces +-} + where + fresh = modifyAndGet (bst ^* chrbstWorkStore ^* wkstoreNextFreeWorkInx) $ \i -> (i, i + 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 leftoverWork = do + bst <- getl $ bst + let ret = return $ SolverResult + { slvresSubst = bst ^. chrbstSolveSubst + , slvresResidualCnstr = reverse $ bst ^. chrbstResidualQueue + , slvresWorkCnstr = leftoverWork + , slvresWaitVarCnstr = [ wfv ^. waitForVarWorkInx | wfvs <- Map.elems $ bst ^. chrbstWaitForVar, wfv <- wfvs ] + , slvresReductionSteps = reverse $ bst ^. chrbstReductionSteps + } + -- when ready, just return and backtrack into the scheduler + ret `mplus` 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 = do + -- failing just terminates this slv, scheduling to another, if any + 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 bprio slv = do + -- bprio <- getl $ bst ^* chrbstBacktrackPrio + gst ^* chrgstScheduleQueue =$: Que.insert bprio 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' slv = do + bprio <- getl $ bst ^* chrbstBacktrackPrio + slvSchedule bprio 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 slv = do + slvSchedule' slv + 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 = modifyAndGet (gst ^* chrgstScheduleQueue) $ \q -> (Que.getMin q, Que.deleteMin 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 = slvSplitFromSchedule >>= maybe mzero 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 i = fmap (IntMap.findWithDefault (panic "MBP.wkstoreTable.lookup") i) $ getl $ bst ^* chrbstWorkStore ^* wkstoreTable +{-# INLINE lkupWork #-} + +lkupChr :: MonoBacktrackPrio c g bp p s e m => CHRInx -> CHRMonoBacktrackPrioT c g bp p s e m (StoredCHR c g bp p) +lkupChr i = fmap (IntMap.findWithDefault (panic "MBP.chrSolve.chrstoreTable.lookup") i) $ getl $ gst ^* chrgstStore ^* chrstoreTable +{-# INLINE lkupChr #-} + +-- | 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 (SolverReductionStep mc ai nw) = do + mc <- cvtMC mc + nw <- fmap Map.fromList $ forM (Map.toList nw) $ \(via,i) -> do + i <- forM i lkupWork + return (via, i) + return $ SolverReductionStep mc ai nw + where + cvtMC (MatchedCombi {mcCHR = c, mcWork = ws}) = do + c' <- lkupChr c + ws' <- forM ws lkupWork + return $ MatchedCombi c' ws' +cvtSolverReductionStep (SolverReductionDBG pp) = return (SolverReductionDBG pp) + +-- | 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 verbosity (SolverResult {slvresSubst = s, slvresResidualCnstr = ris, slvresWorkCnstr = wis, slvresWaitVarCnstr = wvis, slvresReductionSteps = steps}) = do + rs <- forM ris $ \i -> lkupWork i >>= return . pp . workCnstr + ws <- forM wis $ \i -> lkupWork i >>= return . pp . workCnstr + wvs <- forM wvis $ \i -> lkupWork i >>= return . pp . workCnstr + ss <- if verbosity >= Verbosity_ALot + then forM steps $ \step -> cvtSolverReductionStep step >>= (return . pp) + else return [pp $ "Only included with enough verbosity turned on"] + nrsteps <- getl $ gst ^* chrgstStatNrSolveSteps + let pextra | verbosity >= Verbosity_Normal = + "Residue" >-< indent 2 (vlist rs) + >-< "Wait" >-< indent 2 (vlist wvs) + >-< "Stats" >-< indent 2 (ppAssocLV [ ("Count of overall solve steps", pp nrsteps) ]) + >-< "Steps" >-< indent 2 (vlist ss) + | otherwise = Pretty.empty + return $ + "Subst" >-< indent 2 (s `varUpd` s) + >-< "Work" >-< indent 2 (vlist ws) + >-< pextra + +------------------------------------------------------------------------------------------- +--- 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 + -- -> CHRPrioEvaluatableVal bprio + -> CHRMonoBacktrackPrioT cnstr guard bprio prio subst env m (SolverResult subst) + -> m ([SolverResult subst], (CHRGlobState cnstr guard bprio prio subst env m, CHRBackState cnstr bprio subst env)) +runCHRMonoBacktrackPrioT gs bs {- bp -} m = observeStateAllT (gs, bs {- _chrbstBacktrackPrio=bp -}) m +{-# INLINABLE runCHRMonoBacktrackPrioT #-} + +------------------------------------------------------------------------------------------- +--- Solver: Intermediate structures +------------------------------------------------------------------------------------------- + +-- | Intermediate Solver structure +data FoundChr c g bp p + = FoundChr + { foundChrInx :: {-# UNPACK #-} !CHRInx + , foundChrChr :: !(StoredCHR c g bp p) + , foundChrCnstr :: ![WorkInx] + } + +-- | Intermediate Solver structure +data FoundWorkInx c g bp p + = FoundWorkInx + { foundWorkInxInx :: {-# UNPACK #-} !CHRConstraintInx + , foundWorkInxChr :: !(StoredCHR c g bp p) + , foundWorkInxWorkInxs :: ![[WorkInx]] + } + +-- | Intermediate Solver structure: sorting key for matches +data FoundMatchSortKey bp p s + = FoundMatchSortKey + { foundMatchSortKeyPrio :: !(Maybe (s,p)) + , foundMatchSortKeyWaitSize :: {-# UNPACK #-} !Int + , foundMatchSortKeyTextOrder :: {-# UNPACK #-} !CHRInx + } + +instance Show (FoundMatchSortKey bp p s) where + show _ = "FoundMatchSortKey" + +instance (PP p, PP s) => PP (FoundMatchSortKey bp p s) where + pp (FoundMatchSortKey {foundMatchSortKeyPrio=p, foundMatchSortKeyWaitSize=w, foundMatchSortKeyTextOrder=o}) = ppParensCommas [pp p, pp w, pp o] + +compareFoundMatchSortKey :: {- (Ord (CHRPrioEvaluatableVal bp)) => -} ((s,p) -> (s,p) -> Ordering) -> FoundMatchSortKey bp p s -> FoundMatchSortKey bp p s -> Ordering +compareFoundMatchSortKey cmp_rp (FoundMatchSortKey {- bp1 -} rp1 ws1 to1) (FoundMatchSortKey {- bp2 -} rp2 ws2 to2) = + {- orderingLexic (bp1 `compare` bp2) $ -} orderingLexic (rp1 `cmp_mbrp` rp2) $ orderingLexic (ws1 `compare` ws2) $ to1 `compare` to2 + where + cmp_mbrp (Just rp1) (Just rp2) = cmp_rp rp1 rp2 + cmp_mbrp (Just _ ) _ = GT + cmp_mbrp _ (Just _ ) = LT + cmp_mbrp _ _ = EQ + +-- | Intermediate Solver structure: body alternative, together with index position +data FoundBodyAlt c bp + = FoundBodyAlt + { foundBodyAltInx :: {-# UNPACK #-} !Int + , foundBodyAltBacktrackPrio :: !(CHRPrioEvaluatableVal bp) + , foundBodyAltAlt :: !(RuleBodyAlt c bp) + } + +instance Show (FoundBodyAlt c bp) where + show _ = "FoundBodyAlt" + +instance (PP c, PP bp, PP (CHRPrioEvaluatableVal bp)) => PP (FoundBodyAlt c bp) where + pp (FoundBodyAlt {foundBodyAltInx=i, foundBodyAltBacktrackPrio=bp, foundBodyAltAlt=a}) = i >|< ":" >|< ppParens bp >#< a + +-- | Intermediate Solver structure: all matched combis with their body alternatives + backtrack priorities +data FoundSlvMatch c g bp p s + = FoundSlvMatch + { foundSlvMatchSubst :: !s -- ^ the subst of rule meta vars making this a rule + work combi match + , foundSlvMatchFreeVars :: !(CHRWaitForVarSet s) -- ^ free meta vars of head + , foundSlvMatchWaitForVars :: !(CHRWaitForVarSet s) -- ^ for the work we try to solve the (global) vars on which we have to wait to continue + , foundSlvMatchSortKey :: !(FoundMatchSortKey bp p s) -- ^ key to sort found matches + , foundSlvMatchBodyAlts :: ![FoundBodyAlt c bp] -- ^ the body alternatives of the rule which matches + } + +instance Show (FoundSlvMatch c g bp p s) where + show _ = "FoundSlvMatch" + +instance (PP s, PP p, PP c, PP bp, PP (VarLookupKey s), PP (CHRPrioEvaluatableVal bp)) => PP (FoundSlvMatch c g bp p s) where + pp (FoundSlvMatch {foundSlvMatchSubst=s, foundSlvMatchWaitForVars=ws, foundSlvMatchBodyAlts=as}) = ws >#< s >-< vlist as + +-- | Intermediate Solver structure: all matched combis with their backtrack prioritized body alternatives +data FoundWorkMatch c g bp p s + = FoundWorkMatch + { foundWorkMatchInx :: {-# UNPACK #-} !CHRConstraintInx + , foundWorkMatchChr :: !(StoredCHR c g bp p) + , foundWorkMatchWorkInx :: ![WorkInx] + , foundWorkMatchSlvMatch :: !(Maybe (FoundSlvMatch c g bp p s)) + } + +instance Show (FoundWorkMatch c g bp p s) where + show _ = "FoundWorkMatch" + +instance (PP c, PP bp, PP p, PP s, PP (VarLookupKey s), PP (CHRPrioEvaluatableVal bp)) => PP (FoundWorkMatch c g bp p s) where + pp (FoundWorkMatch {foundWorkMatchSlvMatch=sm}) = pp sm + +-- | Intermediate Solver structure: all matched combis with their backtrack prioritized body alternatives +data FoundWorkSortedMatch c g bp p s + = FoundWorkSortedMatch + { foundWorkSortedMatchInx :: !CHRConstraintInx + , foundWorkSortedMatchChr :: !(StoredCHR c g bp p) + , foundWorkSortedMatchBodyAlts :: ![FoundBodyAlt c bp] + , foundWorkSortedMatchWorkInx :: ![WorkInx] + , foundWorkSortedMatchSubst :: !s + , foundWorkSortedMatchFreeVars :: !(CHRWaitForVarSet s) + , foundWorkSortedMatchWaitForVars :: !(CHRWaitForVarSet s) + } + +instance Show (FoundWorkSortedMatch c g bp p s) where + show _ = "FoundWorkSortedMatch" + +instance (PP c, PP bp, PP p, PP s, PP g, PP (VarLookupKey s), PP (CHRPrioEvaluatableVal bp)) => PP (FoundWorkSortedMatch c g bp p s) where + pp (FoundWorkSortedMatch {foundWorkSortedMatchBodyAlts=as, foundWorkSortedMatchWorkInx=wis, foundWorkSortedMatchSubst=s, foundWorkSortedMatchWaitForVars=wvs}) + = wis >-< s >#< ppParens wvs >-< vlist as + +------------------------------------------------------------------------------------------- +--- Solver options +------------------------------------------------------------------------------------------- + +-- | Solve specific options +data CHRSolveOpts + = CHRSolveOpts + { chrslvOptSucceedOnLeftoverWork :: !Bool -- ^ left over unresolvable (non residue) work is also a successful result + , chrslvOptSucceedOnFailedSolve :: !Bool -- ^ failed solve is considered also a successful result, with the failed constraint as a residue + , chrslvOptGatherDebugInfo :: !Bool -- ^ gather debug info + , chrslvOptGatherTraceInfo :: !Bool -- ^ gather trace info + } + +defaultCHRSolveOpts :: CHRSolveOpts +defaultCHRSolveOpts + = CHRSolveOpts + { chrslvOptSucceedOnLeftoverWork = False + , chrslvOptSucceedOnFailedSolve = False + , chrslvOptGatherDebugInfo = False + , chrslvOptGatherTraceInfo = False + } + +------------------------------------------------------------------------------------------- +--- Solver +------------------------------------------------------------------------------------------- + +{-# INLINABLE chrSolve #-} +{- # SPECIALIZE chrSolve + :: ( MonoBacktrackPrio c g bp p s e IO + , PP s + ) => CHRSolveOpts + -> e + -> CHRMonoBacktrackPrioT c g bp p s e IO (SolverResult s) + # -} +-- | (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 opts env = slv + where + -- gather debug info + dbg | chrslvOptGatherDebugInfo opts = \i -> bst ^* chrbstReductionSteps =$: (SolverReductionDBG i :) + | otherwise = \_ -> return () + -- gather trace info + trc | chrslvOptGatherTraceInfo opts = \i -> gst ^* chrgstTrace =$: (i :) + | otherwise = \_ -> return () + -- leave this unconditional, does not seem not make a difference for performance + -- trc i = gst ^* chrgstTrace =$: (i :) + -- solve + slv = do + gst ^* chrgstStatNrSolveSteps =$: (+1) + mbSlvWk <- splitWorkFromSolveQueue + case mbSlvWk of + -- There is work in the solve work queue + Just (workInx) -> do + work <- lkupWork workInx + case work of + Work_Fail -> slvFail + _ -> do + subst <- getl $ bst ^* chrbstSolveSubst + let mbSlv = chrmatcherRun (chrBuiltinSolveM env $ workCnstr work) emptyCHRMatchEnv subst + + -- debug info + dbg $ + ( "solve wk" >#< work + >-< "match" >#< mbSlv + ) + + case mbSlv of + Just (s,_) -> do + -- the newfound subst may reactivate waiting work + splitOffResolvedWaitForVarWork (Lk.keysSet s) >>= mapM_ addToWorkQueue + bst ^* chrbstSolveSubst =$: (s `Lk.apply`) + -- just continue with next work + slv + _ | chrslvOptSucceedOnFailedSolve opts -> do + bst ^* chrbstResidualQueue =$: (workInx :) + -- just continue with next work + slv + | otherwise -> do + slvFail + + + -- If no more solve work, continue with normal work + Nothing -> do + waitingWk <- waitingInWorkQueue + visitedChrWkCombis <- getl $ bst ^* chrbstMatchedCombis + mbWk <- splitFromWorkQueue + case mbWk of + -- If no more work, ready or cannot proceed + Nothing -> do + wr <- getl $ bst ^* chrbstRuleWorkQueue ^* wkqueueRedo + if chrslvOptSucceedOnLeftoverWork opts || IntSet.null wr + then slvSucces $ IntSet.toList wr + else slvFail + + -- There is work in the queue + Just workInx -> do + -- lookup the work + work <- lkupWork workInx + -- work2 <- lkupWork workInx + + -- find all matching chrs for the work + foundChrInxs <- slvLookup (workKey work ) (gst ^* chrgstStore ^* chrstoreTrie ) + -- foundChrInxs2 <- slvLookup2 (workKey work2) (chrgstStore ^* chrstoreTrie2) + -- remove duplicates, regroup + let foundChrGroupedInxs = Map.unionsWith Set.union $ map (\(CHRConstraintInx i j) -> Map.singleton i (Set.singleton j)) foundChrInxs + foundChrs <- forM (Map.toList foundChrGroupedInxs) $ \(chrInx,rlInxs) -> lkupChr chrInx >>= \chr -> return $ FoundChr chrInx chr $ Set.toList rlInxs + + -- found chrs for the work correspond to 1 single position in the head, find all combinations with work in the queue + foundWorkInxs <- sequence + [ fmap (FoundWorkInx (CHRConstraintInx ci i) c) $ slvCandidate waitingWk visitedChrWkCombis workInx c i + | FoundChr ci c is <- foundChrs, i <- is + ] + + -- each found combi has to match + foundWorkMatches <- fmap concat $ + forM foundWorkInxs $ \(FoundWorkInx ci c wis) -> do + forM wis $ \wi -> do + w <- forM wi lkupWork + fmap (FoundWorkMatch ci c wi) $ slvMatch env c (map workCnstr w) (chrciAt ci) + + -- split off the work which has to wait for variable bindings (as indicated by matching) + -- let () = partition () foundWorkMatches + -- sort over priorities + let foundWorkSortedMatches = sortByOn (compareFoundMatchSortKey $ chrPrioCompare env) fst + [ (k, FoundWorkSortedMatch (foundWorkMatchInx fwm) (foundWorkMatchChr fwm) (foundSlvMatchBodyAlts sm) + (foundWorkMatchWorkInx fwm) (foundSlvMatchSubst sm) (foundSlvMatchFreeVars sm) (foundSlvMatchWaitForVars sm)) + | fwm@(FoundWorkMatch {foundWorkMatchSlvMatch = Just sm@(FoundSlvMatch {foundSlvMatchSortKey=k})}) <- foundWorkMatches + -- , (k,a) <- foundSlvMatchBodyAlts sm + ] + + bprio <- getl $ bst ^* chrbstBacktrackPrio + subst <- getl $ bst ^* chrbstSolveSubst + dbgWaitInfo <- getl $ bst ^* chrbstWaitForVar + -- sque <- getl $ gst ^* chrgstScheduleQueue + -- debug info + dbg $ "bprio" >#< bprio + >-< "wk" >#< (work >-< subst `varUpd` workCnstr work) + >-< "que" >#< ppBracketsCommas (IntSet.toList waitingWk) + >-< "subst" >#< subst + >-< "wait" >#< ppAssocL (assocLMapElt (ppAssocL . map (\i -> (_waitForVarWorkInx i, ppCommas $ Set.toList $ _waitForVarVars i))) $ Map.toList dbgWaitInfo) + >-< "visited" >#< ppBracketsCommas (Set.toList visitedChrWkCombis) + >-< "chrs" >#< vlist [ ci >|< ppParensCommas is >|< ":" >#< c | FoundChr ci c is <- foundChrs ] + >-< "works" >#< vlist [ ci >|< ":" >#< vlist (map ppBracketsCommas ws) | FoundWorkInx ci c ws <- foundWorkInxs ] + >-< "matches" >#< vlist [ ci >|< ":" >#< ppBracketsCommas wi >#< ":" >#< mbm | FoundWorkMatch ci _ wi mbm <- foundWorkMatches ] + -- >-< "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 foundWorkSortedMatches of + ((_,fwsm@(FoundWorkSortedMatch {foundWorkSortedMatchWaitForVars = waitForVars})):_) + | Set.null waitForVars -> do + -- addRedoToWorkQueue workInx + addToWorkQueue workInx + slv1 bprio fwsm + | otherwise -> do + -- put on wait queue if there are unresolved variables + addWorkToWaitForVarQueue waitForVars workInx + -- continue without reschedule + slv + _ -> do + addRedoToWorkQueue workInx + 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 curbprio + (FoundWorkSortedMatch + { foundWorkSortedMatchInx = CHRConstraintInx {chrciInx = ci} + , foundWorkSortedMatchChr = chr@StoredCHR {_storedChrRule = Rule {ruleSimpSz = simpSz}} + , foundWorkSortedMatchBodyAlts = alts + , foundWorkSortedMatchWorkInx = workInxs + , foundWorkSortedMatchSubst = matchSubst + , foundWorkSortedMatchFreeVars = freeHeadVars + }) = do + -- remove the simplification part from the work queue + deleteFromWorkQueue $ IntSet.fromList $ take simpSz workInxs + -- depending on nr of alts continue slightly different + case alts of + -- just continue if no alts + [] -> do + log Nothing + slv + -- just reschedule + [alt@(FoundBodyAlt {foundBodyAltBacktrackPrio=bprio})] + | curbprio == bprio -> do + log (Just alt) + nextwork bprio alt + | otherwise -> do + log (Just alt) + slvSchedule bprio $ nextwork bprio alt + slvScheduleRun + -- otherwise backtrack and schedule all and then reschedule + alts -> do + forM alts $ \alt@(FoundBodyAlt {foundBodyAltBacktrackPrio=bprio}) -> do + log (Just alt) + (backtrack $ nextwork bprio alt) >>= slvSchedule bprio + slvScheduleRun + + where + log alt = do + let a = (fmap (rbodyaltBody . foundBodyAltAlt) alt) + trc $ SolveStep chr matchSubst a [] [] -- TODO: Set stepNewTodo, stepNewDone (last two arguments) + nextwork bprio alt@(FoundBodyAlt {foundBodyAltAlt=(RuleBodyAlt {rbodyaltBody=body})}) = do + -- set prio for this alt + bst ^* chrbstBacktrackPrio =: bprio + -- fresh vars for unbound body metavars + freshSubst <- slvFreshSubst freeHeadVars body + -- add each constraint from the body, applying the meta var subst + newWkInxs <- forM body $ addConstraintAsWork . ((freshSubst `Lk.apply` matchSubst) `varUpd`) + -- mark this combi of chr and work as visited + let matchedCombi = MatchedCombi ci workInxs + bst ^* chrbstMatchedCombis =$: Set.insert matchedCombi + -- add this reduction step as being taken + bst ^* chrbstReductionSteps =$: (SolverReductionStep matchedCombi (foundBodyAltInx alt) (Map.unionsWith (++) $ map (\(k,v) -> Map.singleton k [v]) $ newWkInxs) :) + -- take next step + 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 except x = + fmap (foldr Lk.apply Lk.empty) $ + forM (Set.toList $ varFreeSet x `Set.difference` except) $ \v -> + modifyAndGet (bst ^* chrbstFreshVar) (freshWith $ Just v) >>= \v' -> return $ (Lk.singleton v (varTermMkKey v') :: s) +{-# INLINE slvFreshSubst #-} + +{- +-- | Lookup work in a store part of the global state +slvLookup + :: ( MonoBacktrackPrio c g bp p s e m + , Ord x + ) => CHRKey c -- ^ work key + -> Lens (CHRGlobState c g bp p s e m) (CHRTrie' c [x]) + -> CHRMonoBacktrackPrioT c g bp p s e m [x] +slvLookup key t = + (getl $ gst ^* t) >>= \t -> do + let lkup how = concat $ TreeTrie.lookupResultToList $ TreeTrie.lookupPartialByKey how key t + return $ Set.toList $ Set.fromList $ lkup TTL_WildInTrie ++ lkup TTL_WildInKey +-} + +-- | 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 key t = + (getl t) >>= \t -> do + {- + let lkup how = concat $ TreeTrie.lookupResultToList $ TreeTrie.lookupPartialByKey how key t + return $ Set.toList $ Set.fromList $ lkup TTL_WildInTrie ++ lkup TTL_WildInKey + -} + return $ concat $ TT.lookupResultToList $ TT.lookup key 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 + :: ( MonoBacktrackPrio c g bp p s e m + -- , Ord (TTKey c), PP (TTKey c) + ) => 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 waitingWk alreadyMatchedCombis wi (StoredCHR {_storedHeadKeys = ks, _storedChrInx = ci}) headInx = do + let [ks1,_,ks2] = splitPlaces [headInx, headInx+1] ks + ws1 <- forM ks1 lkup + ws2 <- forM ks2 lkup + return $ filter (\wi -> all (`IntSet.member` waitingWk) wi + && Set.notMember (MatchedCombi ci wi) alreadyMatchedCombis) + $ combineToDistinguishedEltsBy (==) $ ws1 ++ [[wi]] ++ ws2 + where + lkup k = slvLookup k (chrgstWorkStore ^* wkstoreTrie) +-} + +-- | 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 + -- , Ord (TTKey c), PP (TTKey c) + -- , ExtrValVarKey (VarLookupVal s) ~ VarLookupKey s + ) => 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 waitingWk alreadyMatchedCombis wi (StoredCHR {_storedHeadKeys = ks, _storedChrInx = ci}) headInx = do + let [ks1,_,ks2] = splitPlaces [headInx, headInx+1] ks + ws1 <- forM ks1 lkup + ws2 <- forM ks2 lkup + return $ filter (\wi -> all (`IntSet.member` waitingWk) wi + && Set.notMember (MatchedCombi ci wi) alreadyMatchedCombis) + $ combineToDistinguishedEltsBy (==) $ ws1 ++ [[wi]] ++ ws2 + where + -- lkup :: CHRKey c -> CHRMonoBacktrackPrioT c g bp p s e m [WorkInx] + lkup k = slvLookup k (bst ^* chrbstWorkStore ^* wkstoreTrie) +{-# INLINE slvCandidate #-} + +-- | Match the stored CHR with a set of possible constraints, giving a substitution on success +slvMatch + :: ( 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 p s + , CHRPrioEvaluatable env bp s + -- , CHRBuiltinSolvable env b s + -- , PP 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 env chr@(StoredCHR {_storedChrRule = Rule {rulePrio = mbpr, ruleHead = hc, ruleGuard = gd, ruleBacktrackPrio = mbbpr, ruleBodyAlts = alts}}) cnstrs headInx = do + subst <- getl $ bst ^* chrbstSolveSubst + curbprio <- fmap chrPrioLift $ getl $ bst ^* chrbstBacktrackPrio + return $ fmap (\(s,ws) -> FoundSlvMatch s freevars ws (FoundMatchSortKey (fmap ((,) s) mbpr) (Set.size ws) (_storedChrInx chr)) + [ FoundBodyAlt i bp a | (i,a) <- zip [0..] alts, let bp = maybe minBound (chrPrioEval env s) $ rbodyaltBacktrackPrio a + ]) + $ (\m -> chrmatcherRun m (emptyCHRMatchEnv {chrmatchenvMetaMayBind = (`Set.member` freevars)}) subst) + $ sequence_ + $ prio curbprio ++ matches ++ checks + where + prio curbprio = maybe [] (\bpr -> [chrMatchToM env bpr curbprio]) mbbpr + matches = zipWith3 (\i h c -> chrMatchAndWaitToM (i == headInx) env h c) [0::Int ..] hc cnstrs + -- ignoreWait + checks = map (chrCheckM env) gd + freevars = Set.unions [varFreeSet hc, maybe Set.empty varFreeSet mbbpr] +{-# INLINE slvMatch #-} + +------------------------------------------------------------------------------------------- +--- Instances: Serialize +------------------------------------------------------------------------------------------- + +{- +instance (Ord (TTKey c), Serialize (TTKey c), Serialize c, Serialize g, Serialize b, Serialize p) => Serialize (CHRStore c g b p) where + sput (CHRStore a) = sput a + sget = liftM CHRStore sget + +instance (Serialize c, Serialize g, Serialize b, Serialize p, Serialize (TTKey c)) => Serialize (StoredCHR c g bp p) where + sput (StoredCHR a b c d) = sput a >> sput b >> sput c >> sput d + sget = liftM4 StoredCHR sget sget sget sget + +-} diff --git a/src/CHR/Types.hs b/src/CHR/Types.hs new file mode 100644 --- /dev/null +++ b/src/CHR/Types.hs @@ -0,0 +1,138 @@ +{-# LANGUAGE ScopedTypeVariables, StandaloneDeriving, UndecidableInstances, NoMonomorphismRestriction, MultiParamTypeClasses #-} + +------------------------------------------------------------------------------------------- +-- | CHR TreeTrie based solver shared internals, for all solvers +------------------------------------------------------------------------------------------- + +module CHR.Types + ( module CHR.Types.Core + , module CHR.Data.TreeTrie + + , CHRKey + + , WorkTime + , initWorkTime + + , Work'(..) + , Work + + , SolveStep'(..) + , SolveTrace' + , emptySolveTrace + , ppSolveTrace + ) + where + +import qualified CHR.Data.TreeTrie as TT +import CHR.Data.TreeTrie ( TrTrKey ) + +import CHR.Pretty as Pretty +import CHR.Data.AssocL + +import CHR.Types.Core ( IVar + , NmToVarMp, emptyNmToVarMp + , Prio + , CHRPrioEvaluatableVal + , IsConstraint + , IsCHRGuard + , IsCHRConstraint + , IsCHRPrio + , IsCHRBacktrackPrio + , CHRCheckable + , CHRMatchable + , CHRPrioEvaluatable + , CHREmptySubstitution + , CHRMatcher + , CHRMatchableKey + , CHRMatcherFailure + ) + +import qualified Data.Map as Map + +------------------------------------------------------------------------------------------- +--- CHR key +------------------------------------------------------------------------------------------- + +-- | Convenience alias for key into CHR store +type CHRKey v = TT.Key (TT.TrTrKey v) + +------------------------------------------------------------------------------------------- +--- WorkTime, the time/history counter for solver work +------------------------------------------------------------------------------------------- + +-- | All solver constraints are identified individually with a timestamp, also serving as its identification depending on the solver +type WorkTime = Int + +initWorkTime :: WorkTime +initWorkTime = 0 + +------------------------------------------------------------------------------------------- +--- Solver work and/or residual (non)work +------------------------------------------------------------------------------------------- + +type WorkKey v = CHRKey v + +-- | A chunk of work to do when solving, a constraint + sequence nr +data Work' k c + = Work + { workKey :: k -- ^ the key into the CHR store + , workCnstr :: !c -- ^ the constraint to be reduced + , workTime :: WorkTime -- ^ the timestamp identification at which the work was added + } + | Work_Residue + { workCnstr :: !c -- ^ the residual constraint + } + | Work_Solve + { workCnstr :: !c -- ^ constraint which must be solved + } + | Work_Fail + +type Work c = Work' (WorkKey c) c + +type instance TT.TrTrKey (Work' k c) = TT.TrTrKey c + +instance Show (Work' k c) where + show _ = "SolveWork" + +instance (PP k, PP c) => PP (Work' k c) where + pp (Work {workKey=k, workCnstr=c, workTime=t}) + = ppParens k >|< "@" >|< t >#< c + pp (Work_Residue c ) = pp c + pp (Work_Solve c ) = pp c + pp (Work_Fail ) = pp "fail" + +------------------------------------------------------------------------------------------- +--- Solver trace +------------------------------------------------------------------------------------------- + +-- | A trace step +data SolveStep' c r s + = SolveStep + { stepChr :: r + , stepSubst :: s + , stepAlt :: Maybe [c] + , stepNewTodo :: [c] + , stepNewDone :: [c] + } + | SolveStats + { stepStats :: Map.Map String PP_Doc + } + | SolveDbg + { stepPP :: PP_Doc + } + +type SolveTrace' c r s = [SolveStep' c r s] + +emptySolveTrace :: SolveTrace' c r s +emptySolveTrace = [] + +instance Show (SolveStep' c r s) where + show _ = "SolveStep" + +instance (PP r, PP c) => {- (PP c, PP g) => -} PP (SolveStep' c r s) where + pp (SolveStep step _ _ todo done) = "STEP" >#< (step >-< "new todo:" >#< ppBracketsCommas todo >-< "new done:" >#< ppBracketsCommas done) + pp (SolveStats stats ) = "STATS" >#< (ppAssocLV (Map.toList stats)) + pp (SolveDbg p ) = "DBG" >#< p + +ppSolveTrace :: (PP r, PP c) => {- (PP s, PP c, PP g) => -} SolveTrace' c r s -> PP_Doc +ppSolveTrace tr = ppBracketsCommasBlock [ pp st | st <- tr ] diff --git a/src/CHR/Types/Core.hs b/src/CHR/Types/Core.hs new file mode 100644 --- /dev/null +++ b/src/CHR/Types/Core.hs @@ -0,0 +1,588 @@ +{-# LANGUAGE ConstraintKinds, MultiParamTypeClasses, FlexibleInstances, FunctionalDependencies, UndecidableInstances, ExistentialQuantification, ScopedTypeVariables, StandaloneDeriving, GeneralizedNewtypeDeriving, TemplateHaskell, NoMonomorphismRestriction #-} + +------------------------------------------------------------------------------------------- +--- Constraint Handling Rules +------------------------------------------------------------------------------------------- + +{- | +Derived from work by Gerrit vd Geest, but with searching structures for predicates +to avoid explosion of search space during resolution. +-} + +module CHR.Types.Core + ( IsConstraint(..) + , ConstraintSolvesVia(..) + + , IsCHRConstraint(..) + -- , CHRConstraint(..) + + , IsCHRGuard(..) + -- , CHRGuard(..) + + -- , IsCHRBuiltin(..) + -- , CHRBuiltin(..) + + , IsCHRPrio(..) + -- , CHRPrio(..) + + , IsCHRBacktrackPrio(..) + + , CHREmptySubstitution(..) + + , CHRMatcherFailure(..) + + , CHRMatcher + , chrmatcherRun' + , chrmatcherRun + -- , chrmatcherLift + -- , chrmatcherUnlift + + , chrmatcherstateEnv + , chrmatcherstateVarLookup + + , chrMatchResolveCompareAndContinue + , chrMatchSubst + , chrMatchBind + , chrMatchFail + , chrMatchFailNoBinding + , chrMatchSuccess + , chrMatchWait + , chrMatchSucces + -- , chrMatchVarUpd + + , CHRMatchEnv(..) + , emptyCHRMatchEnv + + , CHRMatchable(..) + , CHRMatchableKey + , CHRMatchHow(..) + , chrMatchAndWaitToM + + , CHRWaitForVarSet + + , CHRCheckable(..) + + , Prio(..) + , CHRPrioEvaluatable(..) + , CHRPrioEvaluatableVal + + -- , CHRBuiltinSolvable(..) + + , CHRTrOpt(..) + + , IVar + + , VarToNmMp + , emptyVarToNmMp + + , NmToVarMp + , emptyNmToVarMp + ) + where + +-- import qualified UHC.Util.TreeTrie as TreeTrie +import CHR.Data.VarMp +import CHR.Data.Lookup (Lookup, Stacked, LookupApply) +import qualified CHR.Data.Lookup as Lk +import qualified CHR.Data.Lookup.Stacked as Lk +import qualified Data.Map.Strict as Map +import qualified Data.HashMap.Strict as MapH +import qualified Data.IntMap.Strict as IntMap +import Data.Word +import Data.Monoid +import Data.Typeable +import Data.Function +import Unsafe.Coerce +import qualified Data.Set as Set +import CHR.Pretty +-- import UHC.Util.CHR.Key +import qualified CHR.Data.TreeTrie as TT +import Control.Monad +import Control.Monad.State -- .Strict +import Control.Monad.Except +import Control.Monad.Identity +import CHR.Data.Lens +import CHR.Utils +-- import UHC.Util.Binary +-- import UHC.Util.Serialize +import CHR.Data.Substitutable + +-- import UHC.Util.Debug + +------------------------------------------------------------------------------------------- +--- Name <-> Var mapping +------------------------------------------------------------------------------------------- + +type IVar = IntMap.Key + +type VarToNmMp = IntMap.IntMap String +type NmToVarMp = MapH.HashMap String IVar + +emptyVarToNmMp :: VarToNmMp = IntMap.empty +emptyNmToVarMp :: NmToVarMp = MapH.empty + +------------------------------------------------------------------------------------------- +--- CHRMatchHow +------------------------------------------------------------------------------------------- + +-- | How to match, increasingly more binding is allowed +data CHRMatchHow + = CHRMatchHow_Check -- ^ equality check only + | CHRMatchHow_Match -- ^ also allow one-directional (left to right) matching/binding of (meta)vars + | CHRMatchHow_MatchAndWait -- ^ also allow giving back of global vars on which we wait + | CHRMatchHow_Unify -- ^ also allow bi-directional matching, i.e. unification + deriving (Ord, Eq) + +------------------------------------------------------------------------------------------- +--- CHRMatchEnv +------------------------------------------------------------------------------------------- + +-- | Context/environment required for matching itself +data CHRMatchEnv k + = CHRMatchEnv + { {- chrmatchenvHow :: !CHRMatchHow + , -} + chrmatchenvMetaMayBind :: !(k -> Bool) + } + +emptyCHRMatchEnv :: CHRMatchEnv x +emptyCHRMatchEnv = CHRMatchEnv {- CHRMatchHow_Check -} (const True) + +------------------------------------------------------------------------------------------- +--- Wait for var +------------------------------------------------------------------------------------------- + +type CHRWaitForVarSet s = Set.Set (VarLookupKey s) + +------------------------------------------------------------------------------------------- +--- CHRMatcher, call back API used during matching +------------------------------------------------------------------------------------------- + +{- +data CHRMatcherState subst k + = CHRMatcherState + { _chrmatcherstateVarLookup :: !(StackedVarLookup subst) + , _chrmatcherstateWaitForVarSet :: !(CHRWaitForVarSet subst) + , _chrmatcherstateEnv :: !(CHRMatchEnv k) + } + deriving Typeable +-} +type CHRMatcherState subst k = (StackedVarLookup subst, CHRWaitForVarSet (Lk.StackedElt (StackedVarLookup subst)), CHRMatchEnv k) + +mkCHRMatcherState :: StackedVarLookup subst -> CHRWaitForVarSet (Lk.StackedElt (StackedVarLookup subst)) -> CHRMatchEnv k -> CHRMatcherState subst k +mkCHRMatcherState s w e = (s, w, e) +-- mkCHRMatcherState s w e = CHRMatcherState s w e +{-# INLINE mkCHRMatcherState #-} + +unCHRMatcherState :: CHRMatcherState subst k -> (StackedVarLookup subst, CHRWaitForVarSet (Lk.StackedElt (StackedVarLookup subst)), CHRMatchEnv k) +unCHRMatcherState = id +-- unCHRMatcherState (CHRMatcherState s w e) = (s,w,e) +{-# INLINE unCHRMatcherState #-} + +-- | Failure of CHRMatcher +data CHRMatcherFailure + = CHRMatcherFailure + | CHRMatcherFailure_NoBinding -- ^ absence of binding + +-- | Matching monad, keeping a stacked (pair) of subst (local + global), and a set of global variables upon which the solver has to wait in order to (possibly) match further/again +-- type CHRMatcher subst = StateT (StackedVarLookup subst, CHRWaitForVarSet subst) (Either ()) +type CHRMatcher subst = StateT (CHRMatcherState subst (VarLookupKey subst)) (Either CHRMatcherFailure) + +-- instance (k ~ VarLookupKey subst) => MonadState (CHRMatcherState subst k) (CHRMatcher subst) + +chrmatcherstateVarLookup = fst3l +chrmatcherstateWaitForVarSet = snd3l +chrmatcherstateEnv = trd3l + +{- +mkLabel ''CHRMatcherState +-} + +------------------------------------------------------------------------------------------- +--- Common part w.r.t. variable lookup +------------------------------------------------------------------------------------------- + +-- | Do the resolution part of a comparison, continuing with a function which can assume variable resolution has been done for the terms being compared +chrMatchResolveCompareAndContinue + :: forall s . + ( Lookup s (VarLookupKey s) (VarLookupVal s) + , LookupApply s s + , Ord (VarLookupKey s) + , VarTerm (VarLookupVal s) + , ExtrValVarKey (VarLookupVal s) ~ VarLookupKey s + ) + => CHRMatchHow -- ^ how to do the resolution + -> (VarLookupVal s -> VarLookupVal s -> CHRMatcher s ()) -- ^ succeed with successful varlookup continuation + -> VarLookupVal s -- ^ left/fst val + -> VarLookupVal s -- ^ right/snd val + -> CHRMatcher s () +chrMatchResolveCompareAndContinue how ok t1 t2 + = cmp t1 t2 + where cmp t1 t2 = do + menv <- getl chrmatcherstateEnv + case (varTermMbKey t1, varTermMbKey t2) of + (Just v1, Just v2) | v1 == v2 -> chrMatchSuccess + | how == CHRMatchHow_Check -> varContinue + (varContinue (waitv v1 >> waitv v2) (ok t1) v2) + (\t1 -> varContinue (waitt t1 >> waitv v2) (ok t1) v2) + v1 + where waitv v = unless (chrmatchenvMetaMayBind menv v) $ chrMatchWait v + waitt = maybe (return ()) waitv . varTermMbKey + (Just v1, _ ) | how == CHRMatchHow_Check -> varContinue (if maybind then chrMatchFail else chrMatchWait v1) (flip ok t2) v1 + | how >= CHRMatchHow_Match && maybind + -> varContinue (chrMatchBind v1 t2) (flip ok t2) v1 + | otherwise -> varContinue chrMatchFail (flip ok t2) v1 + where maybind = chrmatchenvMetaMayBind menv v1 + (_ , Just v2) | how == CHRMatchHow_Check -> varContinue (if maybind then chrMatchFail else chrMatchWait v2) (ok t1) v2 + | how == CHRMatchHow_MatchAndWait -> varContinue (chrMatchWait v2) (ok t1) v2 + | how == CHRMatchHow_Unify && maybind + -> varContinue (chrMatchBind v2 t1) (ok t1) v2 + | otherwise -> varContinue chrMatchFail (ok t1) v2 + where maybind = chrmatchenvMetaMayBind menv v2 + _ -> chrMatchFail -- ok t1 t2 + varContinue = Lk.lookupResolveAndContinueM varTermMbKey chrMatchSubst + +------------------------------------------------------------------------------------------- +--- CHRCheckable +------------------------------------------------------------------------------------------- + +-- | A Checkable participates in the reduction process as a guard, to be checked. +-- Checking is allowed to find/return substitutions for meta variables (not for global variables). +class (CHREmptySubstitution subst, LookupApply subst subst) => CHRCheckable env x subst where + chrCheck :: env -> subst -> x -> Maybe subst + chrCheck e s x = chrmatcherUnlift (chrCheckM e x) emptyCHRMatchEnv s + + chrCheckM :: env -> x -> CHRMatcher subst () + chrCheckM e x = chrmatcherLift $ \sg -> chrCheck e sg x + +------------------------------------------------------------------------------------------- +--- CHRPrioEvaluatable +------------------------------------------------------------------------------------------- + +-- | The type of value a prio representation evaluates to, must be Ord instance +type family CHRPrioEvaluatableVal p :: * + +-- | A PrioEvaluatable participates in the reduction process to indicate the rule priority, higher prio takes precedence +class (Ord (CHRPrioEvaluatableVal x), Bounded (CHRPrioEvaluatableVal x)) => CHRPrioEvaluatable env x subst | x -> env subst where + -- | Reduce to a prio representation + chrPrioEval :: env -> subst -> x -> CHRPrioEvaluatableVal x + chrPrioEval _ _ _ = minBound + + -- | Compare priorities + chrPrioCompare :: env -> (subst,x) -> (subst,x) -> Ordering + chrPrioCompare e (s1,x1) (s2,x2) = chrPrioEval e s1 x1 `compare` chrPrioEval e s2 x2 + + -- | Lift prio val into prio + chrPrioLift :: CHRPrioEvaluatableVal x -> x + +------------------------------------------------------------------------------------------- +--- Prio +------------------------------------------------------------------------------------------- + +-- | Separate priority type, where minBound represents lowest prio, and compare sorts from high to low prio (i.e. high `compare` low == LT) +newtype Prio = Prio {unPrio :: Word32} + deriving (Eq, Bounded, Num, Enum, Integral, Real) + +instance Ord Prio where + compare = flip compare `on` unPrio + {-# INLINE compare #-} + +------------------------------------------------------------------------------------------- +--- Constraint API +------------------------------------------------------------------------------------------- + +-- | Alias API for constraint requirements +{- +class ( CHRMatchable env c subst + -- , CHRBuiltinSolvable env c subst + , VarExtractable c + , VarUpdatable c subst + , Typeable c + -- , Serialize c + -- , TTKeyable c + , TT.TreeTrieKeyable c + , IsConstraint c + , Ord c + -- , Ord (TTKey c) + , Ord (TT.TrTrKey c) + , PP c + -- , PP (TTKey c) + , PP (TT.TrTrKey c) + ) => IsCHRConstraint env c subst +-} +type IsCHRConstraint env c subst + = ( CHRMatchable env c subst + -- , CHRBuiltinSolvable env c subst + , VarExtractable c + , VarUpdatable c subst + , Typeable c + -- , Serialize c + -- , TTKeyable c + , TT.TreeTrieKeyable c + , IsConstraint c + , Ord c + -- , Ord (TTKey c) + , Ord (TT.TrTrKey c) + , PP c + -- , PP (TTKey c) + , PP (TT.TrTrKey c) + ) + +------------------------------------------------------------------------------------------- +--- Guard API +------------------------------------------------------------------------------------------- + +-- | Alias API for guard requirements +{- +class ( CHRCheckable env g subst + , VarExtractable g + , VarUpdatable g subst + , Typeable g + -- , Serialize g + , PP g + ) => IsCHRGuard env g subst +-} +type IsCHRGuard env g subst + = ( CHRCheckable env g subst + , VarExtractable g + , VarUpdatable g subst + , Typeable g + -- , Serialize g + , PP g + ) + +------------------------------------------------------------------------------------------- +--- Prio API +------------------------------------------------------------------------------------------- + +-- | Alias API for priority requirements +{- +class ( CHRPrioEvaluatable env p subst + , Typeable p + -- , Serialize p + , PP p + ) => IsCHRPrio env p subst +-} +type IsCHRPrio env p subst + = ( CHRPrioEvaluatable env p subst + , Typeable p + -- , Serialize p + , PP p + ) + +-- | Alias API for backtrack priority requirements +{- +class ( IsCHRPrio env bp subst + , CHRMatchable env bp subst + , PP (CHRPrioEvaluatableVal bp) + -- -- , Num (CHRPrioEvaluatableVal bp) + ) => IsCHRBacktrackPrio env bp subst +-} +type IsCHRBacktrackPrio env bp subst + = ( IsCHRPrio env bp subst + , CHRMatchable env bp subst + , PP (CHRPrioEvaluatableVal bp) + -- -- , Num (CHRPrioEvaluatableVal bp) + ) + +------------------------------------------------------------------------------------------- +--- What a constraint must be capable of +------------------------------------------------------------------------------------------- + +-- | Different ways of solving +data ConstraintSolvesVia + = ConstraintSolvesVia_Rule -- ^ rewrite/CHR rules apply + | ConstraintSolvesVia_Solve -- ^ solving involving finding of variable bindings (e.g. unification) + | ConstraintSolvesVia_Residual -- ^ a leftover, residue + | ConstraintSolvesVia_Fail -- ^ triggers explicit fail + | ConstraintSolvesVia_Succeed -- ^ triggers explicit succes + deriving (Show, Enum, Eq, Ord) + +instance PP ConstraintSolvesVia where + pp = pp . show + +-- | The things a constraints needs to be capable of in order to participate in solving +class IsConstraint c where + -- | Requires solving? Or is just a residue... + cnstrRequiresSolve :: c -> Bool + cnstrRequiresSolve c = case cnstrSolvesVia c of + ConstraintSolvesVia_Residual -> False + _ -> True + + cnstrSolvesVia :: c -> ConstraintSolvesVia + cnstrSolvesVia c | cnstrRequiresSolve c = ConstraintSolvesVia_Rule + | otherwise = ConstraintSolvesVia_Residual + +------------------------------------------------------------------------------------------- +--- Tracing options, specific for CHR solvers +------------------------------------------------------------------------------------------- + +data CHRTrOpt + = CHRTrOpt_Lookup -- ^ trie query + | CHRTrOpt_Stats -- ^ various stats + deriving (Eq, Ord, Show) +------------------------------------------------------------------------------------------- +--- CHREmptySubstitution +------------------------------------------------------------------------------------------- + +-- | Capability to yield an empty substitution. +class CHREmptySubstitution subst where + chrEmptySubst :: subst + +------------------------------------------------------------------------------------------- +--- CHRMatchable +------------------------------------------------------------------------------------------- + +-- | The key of a substitution +type family CHRMatchableKey subst :: * + +type instance CHRMatchableKey (StackedVarLookup subst) = CHRMatchableKey subst + +-- | A Matchable participates in the reduction process as a reducable constraint. +-- Unification may be incorporated as well, allowing matching to be expressed in terms of unification. +-- This facilitates implementations of 'CHRBuiltinSolvable'. +class (CHREmptySubstitution subst, LookupApply subst subst, VarExtractable x, VarLookupKey subst ~ ExtrValVarKey x) => CHRMatchable env x subst where + -- | One-directional (1st to 2nd 'x') unify + chrMatchTo :: env -> subst -> x -> x -> Maybe subst + chrMatchTo env s x1 x2 = chrUnify CHRMatchHow_Match (emptyCHRMatchEnv {chrmatchenvMetaMayBind = (`Set.member` varFreeSet x1)}) env s x1 x2 + -- where free = varFreeSet x1 + + -- | One-directional (1st to 2nd 'x') unify + chrUnify :: CHRMatchHow -> CHRMatchEnv (VarLookupKey subst) -> env -> subst -> x -> x -> Maybe subst + chrUnify how menv e s x1 x2 = chrmatcherUnlift (chrUnifyM how e x1 x2) menv s + + -- | Match one-directional (from 1st to 2nd arg), under a subst, yielding a subst for the metavars in the 1st arg, waiting for those in the 2nd + chrMatchToM :: env -> x -> x -> CHRMatcher subst () + chrMatchToM e x1 x2 = chrUnifyM CHRMatchHow_Match e x1 x2 + + -- | Unify bi-directional or match one-directional (from 1st to 2nd arg), under a subst, yielding a subst for the metavars in the 1st arg, waiting for those in the 2nd + chrUnifyM :: CHRMatchHow -> env -> x -> x -> CHRMatcher subst () + chrUnifyM how e x1 x2 = getl chrmatcherstateEnv >>= \menv -> chrmatcherLift $ \sg -> chrUnify how menv e sg x1 x2 + + -- | Solve a constraint which is categorized as 'ConstraintSolvesVia_Solve' + chrBuiltinSolveM :: env -> x -> CHRMatcher subst () + chrBuiltinSolveM e x = return () -- chrmatcherLift $ \sg -> chrBuiltinSolve e sg x + +instance {-# OVERLAPPABLE #-} (CHRMatchable env x subst) => CHRMatchable env (Maybe x) subst where + chrUnifyM how e (Just x1) (Just x2) = chrUnifyM how e x1 x2 + chrUnifyM how e Nothing Nothing = chrMatchSuccess + chrUnifyM how e _ _ = chrMatchFail + +instance {-# OVERLAPPABLE #-} (CHRMatchable env x subst) => CHRMatchable env [x] subst where + chrUnifyM how e x1 x2 | length x1 == length x2 = sequence_ $ zipWith (chrUnifyM how e) x1 x2 + chrUnifyM how e _ _ = chrMatchFail + +------------------------------------------------------------------------------------------- +--- CHRMatcher API, part I +------------------------------------------------------------------------------------------- + +-- | Unlift/observe (or run) a CHRMatcher +chrmatcherUnlift :: (CHREmptySubstitution subst) => CHRMatcher subst () -> CHRMatchEnv (VarLookupKey subst) -> (subst -> Maybe subst) +chrmatcherUnlift mtch menv s = do + (s,w) <- chrmatcherRun mtch menv s + if Set.null w then Just s else Nothing + +-- | Lift into CHRMatcher +chrmatcherLift :: (LookupApply subst subst) => (subst -> Maybe subst) -> CHRMatcher subst () +chrmatcherLift f = do + [sl,sg] <- fmap Lk.unlifts $ getl chrmatcherstateVarLookup -- gets (unStackedVarLookup . _chrmatcherstateVarLookup) + maybe chrMatchFail (\snew -> chrmatcherstateVarLookup =$: (Lk.apply snew)) $ f sg + +-- | Run a CHRMatcher +chrmatcherRun' :: (CHREmptySubstitution subst) => (CHRMatcherFailure -> r) -> (subst -> CHRWaitForVarSet subst -> x -> r) -> CHRMatcher subst x -> CHRMatchEnv (VarLookupKey subst) -> StackedVarLookup subst -> r +chrmatcherRun' fail succes mtch menv s = either + fail + ((\(x,ms) -> let (s, w, _) = unCHRMatcherState ms in succes (Lk.top s) w x)) + $ flip runStateT (mkCHRMatcherState s Set.empty menv) + $ mtch + +-- | Run a CHRMatcher +chrmatcherRun :: (CHREmptySubstitution subst) => CHRMatcher subst () -> CHRMatchEnv (VarLookupKey subst) -> subst -> Maybe (subst, CHRWaitForVarSet subst) +chrmatcherRun mtch menv s = chrmatcherRun' (const Nothing) (\s w _ -> Just (s,w)) mtch menv (Lk.push chrEmptySubst $ Lk.lifts s) -- (StackedVarLookup [chrEmptySubst,s]) + +------------------------------------------------------------------------------------------- +--- CHRMatcher API, part II +------------------------------------------------------------------------------------------- + +chrMatchSubst :: CHRMatcher subst (StackedVarLookup subst) +chrMatchSubst = getl chrmatcherstateVarLookup +{-# INLINE chrMatchSubst #-} + +chrMatchBind :: forall subst k v . (LookupApply subst subst, Lookup subst k v, k ~ VarLookupKey subst, v ~ VarLookupVal subst) => k -> v -> CHRMatcher subst () +chrMatchBind k v = chrmatcherstateVarLookup =$: ((Lk.singleton k v :: subst) `Lk.apply`) +{-# INLINE chrMatchBind #-} + +chrMatchWait :: (Ord k, k ~ VarLookupKey subst) => k -> CHRMatcher subst () +chrMatchWait k = chrMatchModifyWait (Set.insert k) +{-# INLINE chrMatchWait #-} + +chrMatchSuccess :: CHRMatcher subst () +chrMatchSuccess = return () +{-# INLINE chrMatchSuccess #-} + +-- | Normal CHRMatcher failure +chrMatchFail :: CHRMatcher subst a +chrMatchFail = throwError CHRMatcherFailure +{-# INLINE chrMatchFail #-} + +-- | CHRMatcher failure because a variable binding is missing +chrMatchFailNoBinding :: CHRMatcher subst a +chrMatchFailNoBinding = throwError CHRMatcherFailure_NoBinding +{-# INLINE chrMatchFailNoBinding #-} + +chrMatchSucces :: CHRMatcher subst () +chrMatchSucces = return () +{-# INLINE chrMatchSucces #-} + +chrMatchModifyWait :: (CHRWaitForVarSet subst -> CHRWaitForVarSet subst) -> CHRMatcher subst () +chrMatchModifyWait f = + -- modify (\st -> st {_chrmatcherstateWaitForVarSet = f $ _chrmatcherstateWaitForVarSet st}) + -- (chrmatcherstateWaitForVarSet =$:) + modify (\(s,w,e) -> (s,f w,e)) +{-# INLINE chrMatchModifyWait #-} + +-- | Match one-directional (from 1st to 2nd arg), under a subst, yielding a subst for the metavars in the 1st arg, waiting for those in the 2nd +chrMatchAndWaitToM :: CHRMatchable env x subst => Bool -> env -> x -> x -> CHRMatcher subst () +chrMatchAndWaitToM wait env x1 x2 = chrUnifyM (if wait then CHRMatchHow_MatchAndWait else CHRMatchHow_Match) env x1 x2 + +------------------------------------------------------------------------------------------- +--- CHRMatchable: instances +------------------------------------------------------------------------------------------- + +-- TBD: move to other file... +instance {-# OVERLAPPABLE #-} Ord (ExtrValVarKey ()) => VarExtractable () where + varFreeSet _ = Set.empty + +instance {-# OVERLAPPABLE #-} (Ord (ExtrValVarKey ()), CHREmptySubstitution subst, LookupApply subst subst, VarLookupKey subst ~ ExtrValVarKey ()) => CHRMatchable env () subst where + chrUnifyM _ _ _ _ = chrMatchSuccess + +------------------------------------------------------------------------------------------- +--- Prio: instances +------------------------------------------------------------------------------------------- + +instance Show Prio where + show = show . unPrio + +instance PP Prio where + pp = pp . unPrio + +------------------------------------------------------------------------------------------- +--- CHRPrioEvaluatable: instances +------------------------------------------------------------------------------------------- + +type instance CHRPrioEvaluatableVal () = Prio + +{- +instance {-# OVERLAPPABLE #-} Ord x => CHRPrioEvaluatable env x subst where + -- chrPrioEval _ _ _ = minBound + chrPrioCompare _ (_,x) (_,y) = compare x y +-} + +{- +instance {-# OVERLAPPABLE #-} CHRPrioEvaluatable env () subst where + chrPrioLift _ = () + chrPrioEval _ _ _ = minBound + chrPrioCompare _ _ _ = EQ +-} + + diff --git a/src/CHR/Types/Rule.hs b/src/CHR/Types/Rule.hs new file mode 100644 --- /dev/null +++ b/src/CHR/Types/Rule.hs @@ -0,0 +1,248 @@ +{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, FunctionalDependencies, UndecidableInstances, ExistentialQuantification, ScopedTypeVariables, StandaloneDeriving #-} +-- {-# LANGUAGE AllowAmbiguousTypes #-} + +------------------------------------------------------------------------------------------- +--- Constraint Handling Rules +------------------------------------------------------------------------------------------- + +{- | +The representation of rules, which should allow an implementation of: + +"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.Types.Rule + ( RuleBodyAlt(..) + + , Rule(..) + , ruleBody, ruleBody' + -- , ruleBodyBuiltin + , ruleSz + + -- , CHRRule(..) + + , (/\) + , (\/) + , (\!) + , (<=>>), (==>>), (<\>>) + , (<==>), (<=>), (==>), (<\>) + , (|>), (=|) + , (=!), (=!!) + , (=@), (@=) + ) + where + +import qualified CHR.Data.TreeTrie as TT +import CHR.Data.VarMp +import CHR.Utils +import Data.Monoid +import Data.List as List +import Data.Typeable +-- import Data.Data +import qualified Data.Set as Set +import CHR.Pretty +-- import UHC.Util.CHR.Key +import Control.Monad +-- import UHC.Util.Binary +-- import UHC.Util.Serialize +import CHR.Data.Substitutable + +------------------------------------------------------------------------------------------- +--- CHR, derived structures +------------------------------------------------------------------------------------------- + +data RuleBodyAlt cnstr bprio + = RuleBodyAlt + { rbodyaltBacktrackPrio :: !(Maybe bprio) -- ^ optional backtrack priority, if absent it is inherited from the active backtrack prio + , rbodyaltBody :: ![cnstr] -- ^ body constraints to be dealt with by rules + -- , rbodyaltBodyBuiltin :: ![builtin] -- ^ builtin constraints to be dealt with by builtin solving + } + deriving (Typeable) + +instance Show (RuleBodyAlt c bp) where + show _ = "RuleBodyAlt" + +instance (PP bp, PP c) => PP (RuleBodyAlt c bp) where + pp a = ppParens (rbodyaltBacktrackPrio a) >#< ppCommas' (rbodyaltBody a) + +-- | A CHR (rule) consist of head (simplification + propagation, boundary indicated by an Int), guard, and a body. All may be empty, but not all at the same time. +data Rule cnstr guard bprio prio + = Rule + { ruleHead :: ![cnstr] + , ruleSimpSz :: !Int -- ^ length of the part of the head which is the simplification part + , ruleGuard :: ![guard] + , ruleBodyAlts :: ![RuleBodyAlt cnstr bprio] + , ruleBacktrackPrio :: !(Maybe bprio) -- ^ backtrack priority, should be something which can be substituted with the actual prio, later to be referred to at backtrack prios of alternatives + , rulePrio :: !(Maybe prio) -- ^ rule priority, to choose between rules with equal backtrack priority + , ruleName :: (Maybe String) + } + deriving (Typeable) + +-- | Backwards compatibility: if only one alternative, extract it, ignore other alts +ruleBody' :: Rule c g bp p -> ([c],[c]) +ruleBody' (Rule {ruleBodyAlts = (a:_)}) = (rbodyaltBody a, []) +ruleBody' (Rule {ruleBodyAlts = [] }) = ([], []) + +-- | Backwards compatibility: if only one alternative, extract it, ignore other alts +ruleBody :: Rule c g bp p -> [c] +ruleBody = fst . ruleBody' +{-# INLINE ruleBody #-} + + +-- | Total nr of cnstrs in rule +ruleSz :: Rule c g bp p -> Int +ruleSz = length . ruleHead +{-# INLINE ruleSz #-} + +emptyCHRGuard :: [a] +emptyCHRGuard = [] + +instance Show (Rule c g bp p) where + show _ = "Rule" + +instance (PP c, PP g, PP p, PP bp) => PP (Rule c g bp p) where + pp chr = ppMbPre (\p -> p >#< "::") rPrio $ ppMbPre (\n -> pp n >#< "@") (ruleName chr) $ base + where base = case chr of + Rule {} | ruleSimpSz chr == 0 -> ppChr ([ppL (ruleHead chr), pp "==>"] ++ ppGB (ruleGuard chr) body) + | ruleSimpSz chr == length (ruleHead chr) -> ppChr ([ppL (ruleHead chr), pp "<=>"] ++ ppGB (ruleGuard chr) body) + | length (ruleHead chr) == 0 -> ppChr (ppGB (ruleGuard chr) body) + | otherwise -> ppChr ([ppL (drop (ruleSimpSz chr) (ruleHead chr)), pp "\\", ppL (take (ruleSimpSz chr) (ruleHead chr)), pp "<=>"] ++ ppGB (ruleGuard chr) body) + rPrio = case (ruleBacktrackPrio chr, rulePrio chr) of + (Nothing, Nothing) -> Nothing + (Just bp, Just rp) -> Just $ ppParensCommas [pp bp , pp rp ] + (Just bp, _ ) -> Just $ ppParensCommas [pp bp , pp "_"] + (_ , Just rp) -> Just $ ppParensCommas [pp "_", pp rp ] + body = ppSpaces $ intersperse (pp "\\/") $ map ppAlt $ ruleBodyAlts chr + where ppAlt a = ppMbPre (\p -> ppParens p >#< "::") (rbodyaltBacktrackPrio a) $ ppL $ map pp (rbodyaltBody a) -- ++ map pp (rbodyaltBodyBuiltin a) + ppGB g@(_:_) b = [ppL g, "|" >#< b] -- g b = ppListPre (\g -> ppL g >#< "|") g + ppGB [] b = [b] + -- ppL [x] = pp x + ppL xs = ppCommas' xs -- ppParensCommasBlock xs + ppChr l = ppSpaces l -- vlist l -- ppCurlysBlock + +-- type instance TTKey (Rule cnstr guard bprio prio) = TTKey cnstr +type instance TT.TrTrKey (Rule cnstr guard bprio prio) = TT.TrTrKey cnstr + +instance (TT.TreeTrieKeyable cnstr) => TT.TreeTrieKeyable (Rule cnstr guard bprio prio) where + toTreeTriePreKey1 chr = TT.prekey1Delegate $ head $ ruleHead chr + +------------------------------------------------------------------------------------------- +--- Var instances +------------------------------------------------------------------------------------------- + +type instance ExtrValVarKey (Rule c g bp p) = ExtrValVarKey c +type instance ExtrValVarKey (RuleBodyAlt c p) = ExtrValVarKey c + +-- TBD: should vars be extracted from prio and builtin as well? +instance (VarExtractable c) => VarExtractable (RuleBodyAlt c p) where + varFreeSet (RuleBodyAlt {rbodyaltBody=b}) + = Set.unions $ map varFreeSet b + +-- TBD: should vars be extracted from prio as well? +instance (VarExtractable c, VarExtractable g, ExtrValVarKey c ~ ExtrValVarKey g) => VarExtractable (Rule c g bp p) where + varFreeSet (Rule {ruleHead=h, ruleGuard=g, ruleBodyAlts=b}) + = Set.unions $ concat [map varFreeSet h, map varFreeSet g, map varFreeSet b] + +instance (VarUpdatable c s, VarUpdatable p s) => VarUpdatable (RuleBodyAlt c p) s where + varUpd s r@(RuleBodyAlt {rbodyaltBacktrackPrio=p, rbodyaltBody=b}) + = r {rbodyaltBacktrackPrio = fmap (varUpd s) p, rbodyaltBody = map (varUpd s) b} + +instance (VarUpdatable c s, VarUpdatable g s, VarUpdatable bp s, VarUpdatable p s) => VarUpdatable (Rule c g bp p) s where + varUpd s r@(Rule {ruleHead=h, ruleGuard=g, ruleBodyAlts=b}) + = r {ruleHead = map (varUpd s) h, ruleGuard = map (varUpd s) g, ruleBodyAlts = map (varUpd s) b} + +------------------------------------------------------------------------------------------- +--- Construction: Rule +------------------------------------------------------------------------------------------- + +mkRule h l g b bi p = Rule h l g [RuleBodyAlt Nothing b] Nothing p Nothing +guardRule g r = r {ruleGuard = ruleGuard r ++ g} +prioritizeRule p r = r {rulePrio = Just p} +prioritizeBacktrackRule p r = r {ruleBacktrackPrio = Just p} +labelRule l r = r {ruleName = Just l} + + +infixl 6 /\ +infixl 5 \! +infixr 4 \/ +infix 3 <==>, <=>, ==>, <\> +infixl 2 |>, =| +infixl 2 =!, =!! +infixl 2 =@ +infixr 1 @= + +-- | Rule body backtracking alternative +(/\) :: [c] -> [c] -> RuleBodyAlt c p +c /\ b = RuleBodyAlt Nothing (c ++ b) + +-- | Rule body backtracking alternatives +(\/) :: [RuleBodyAlt c p] -> [RuleBodyAlt c p] -> [RuleBodyAlt c p] +(\/) = (++) + +-- | Add backtrack priority to body alternative +(\!) :: RuleBodyAlt c p -> p -> RuleBodyAlt c p +r \! p = r {rbodyaltBacktrackPrio = Just p} + +-- | Construct simplification rule out of head, body, and builtin constraints +hs <=>> (bs,bis) = mkRule hs (length hs) [] bs bis Nothing +-- | Construct propagation rule out of head, body, and builtin constraints +hs ==>> (bs,bis) = mkRule hs 0 [] bs bis Nothing + +-- | Construct simpagation rule out of head, body, and builtin constraints +(hsprop,hssimp) <\>> (bs,bis) = mkRule (hssimp ++ hsprop) (length hssimp) [] (bs) (bis) Nothing + +-- | Construct simplification rule out of head and body constraints +hs <==> bs = mkRule (hs) (length hs) [] (bs) [] Nothing +-- | Construct propagation rule out of head and body constraints +hs ==> bs = mkRule (hs) 0 [] (bs) [] Nothing +(<=>) = (<==>) + +-- | Construct simpagation rule out of head and body constraints +(hsprop,hssimp) <\> bs = mkRule (hssimp ++ hsprop) (length hssimp) [] (bs) [] Nothing + +{-# DEPRECATED (|>) "Use (=|)" #-} +-- | Add guards to rule +r |> g = guardRule (g) r +(=|) = (|>) +{-# INLINE (=|) #-} + +-- | Add priority to rule +r =!! p = prioritizeRule (p) r + +-- | Add backtrack priority to rule +r =! p = prioritizeBacktrackRule (p) r + +-- | Add label to rule +r =@ l = labelRule l r + +-- | Add label to rule +l @= r = r =@ l +{-# INLINE (@=) #-} + +------------------------------------------------------------------------------------------- +--- Instances: Serialize +------------------------------------------------------------------------------------------- + +{- +instance (Serialize c,Serialize p) => Serialize (RuleBodyAlt c p) where + sput (RuleBodyAlt a b) = sput a >> sput b + sget = liftM2 RuleBodyAlt sget sget + +instance (Serialize c,Serialize g,Serialize bp,Serialize p) => Serialize (Rule c g bp p) where + sput (Rule a b c d e f g) = sput a >> sput b >> sput c >> sput d >> sput e >> sput f >> sput g + sget = liftM7 Rule sget sget sget sget sget sget sget +-} + +{- +instance (MkSolverConstraint (CHRConstraint e s) x', Serialize x') => Serialize (CHRConstraint e s) where + sput x = maybe (panic "CHR.Types.Rule.Serialize.MkSolverConstraint.sput") sput $ fromSolverConstraint x + sget = liftM toSolverConstraint sget +-} + +{- +instance Serialize (CHRRule e s) where + sput (CHRRule a) = sput a + sget = liftM CHRRule sget +-}