chr-core (empty) → 0.1.0.0
raw patch · 9 files changed
+2224/−0 lines, 9 filesdep +basedep +chr-datadep +chr-prettysetup-changed
Dependencies added: base, chr-data, chr-pretty, containers, hashable, logict-state, mtl, pqueue, unordered-containers
Files
- ChangeLog.md +5/−0
- LICENSE +30/−0
- README.md +1/−0
- Setup.hs +2/−0
- chr-core.cabal +56/−0
- src/CHR/Solve/MonoBacktrackPrio.hs +1156/−0
- src/CHR/Types.hs +138/−0
- src/CHR/Types/Core.hs +588/−0
- src/CHR/Types/Rule.hs +248/−0
+ ChangeLog.md view
@@ -0,0 +1,5 @@+# Revision history for chr++## 0.1.0.0 -- YYYY-mm-dd++* First version. Released on an unsuspecting world.
+ LICENSE view
@@ -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.
+ README.md view
@@ -0,0 +1,1 @@+# Core solving part of CHR libraries
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ chr-core.cabal view
@@ -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
+ src/CHR/Solve/MonoBacktrackPrio.hs view
@@ -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++-}
+ src/CHR/Types.hs view
@@ -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 ]
+ src/CHR/Types/Core.hs view
@@ -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+-}++
+ src/CHR/Types/Rule.hs view
@@ -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+-}