{-# LANGUAGE ConstraintKinds, MultiParamTypeClasses, FlexibleInstances, FunctionalDependencies, UndecidableInstances, ExistentialQuantification, ScopedTypeVariables, StandaloneDeriving, GeneralizedNewtypeDeriving, TemplateHaskell, NoMonomorphismRestriction #-}
module CHR.Types.Core
( IsConstraint(..)
, ConstraintSolvesVia(..)
, IsCHRConstraint(..)
, IsCHRGuard(..)
, IsCHRPrio(..)
, IsCHRBacktrackPrio(..)
, CHREmptySubstitution(..)
, CHRMatcherFailure(..)
, CHRMatcher
, chrmatcherRun'
, chrmatcherRun
, chrmatcherstateEnv
, chrmatcherstateVarLookup
, chrMatchResolveCompareAndContinue
, chrMatchSubst
, chrMatchBind
, chrMatchFail
, chrMatchFailNoBinding
, chrMatchSuccess
, chrMatchWait
, chrMatchSucces
, CHRMatchEnv(..)
, emptyCHRMatchEnv
, CHRMatchable(..)
, CHRMatchableKey
, CHRMatchHow(..)
, chrMatchAndWaitToM
, CHRWaitForVarSet
, CHRCheckable(..)
, Prio(..)
, CHRPrioEvaluatable(..)
, CHRPrioEvaluatableVal
, CHRTrOpt(..)
, IVar
, VarToNmMp
, emptyVarToNmMp
, NmToVarMp
, emptyNmToVarMp
)
where
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 qualified Data.Set as Set
import Unsafe.Coerce
import Control.Monad
import Control.Monad.State
import Control.Monad.Except
import Control.Monad.Identity
import CHR.Pretty
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 CHR.Data.TreeTrie as TT
import CHR.Data.Lens
import CHR.Utils
import CHR.Data.Substitutable
type IVar = IntMap.Key
type VarToNmMp = IntMap.IntMap String
type NmToVarMp = MapH.HashMap String IVar
emptyVarToNmMp :: VarToNmMp = IntMap.empty
emptyNmToVarMp :: NmToVarMp = MapH.empty
data CHRMatchHow
= CHRMatchHow_Check
| CHRMatchHow_Match
| CHRMatchHow_MatchAndWait
| CHRMatchHow_Unify
deriving (Ord, Eq)
data CHRMatchEnv k
= CHRMatchEnv
{
chrmatchenvMetaMayBind :: !(k -> Bool)
}
emptyCHRMatchEnv :: CHRMatchEnv x
emptyCHRMatchEnv = CHRMatchEnv (const True)
type CHRWaitForVarSet s = Set.Set (VarLookupKey s)
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)
{-# INLINE mkCHRMatcherState #-}
unCHRMatcherState :: CHRMatcherState subst k -> (StackedVarLookup subst, CHRWaitForVarSet (Lk.StackedElt (StackedVarLookup subst)), CHRMatchEnv k)
unCHRMatcherState = id
{-# INLINE unCHRMatcherState #-}
data CHRMatcherFailure
= CHRMatcherFailure
| CHRMatcherFailure_NoBinding
type CHRMatcher subst = StateT (CHRMatcherState subst (VarLookupKey subst)) (Either CHRMatcherFailure)
chrmatcherstateVarLookup = fst3l
chrmatcherstateWaitForVarSet = snd3l
chrmatcherstateEnv = trd3l
chrMatchResolveCompareAndContinue
:: forall s .
( Lookup s (VarLookupKey s) (VarLookupVal s)
, LookupApply s s
, Ord (VarLookupKey s)
, VarTerm (VarLookupVal s)
, ExtrValVarKey (VarLookupVal s) ~ VarLookupKey s
)
=> CHRMatchHow
-> (VarLookupVal s -> VarLookupVal s -> CHRMatcher s ())
-> VarLookupVal s
-> VarLookupVal s
-> 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
varContinue = Lk.lookupResolveAndContinueM varTermMbKey chrMatchSubst
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
type family CHRPrioEvaluatableVal p :: *
class (Ord (CHRPrioEvaluatableVal x), Bounded (CHRPrioEvaluatableVal x)) => CHRPrioEvaluatable env x subst where
chrPrioEval :: env -> subst -> x -> CHRPrioEvaluatableVal x
chrPrioEval _ _ _ = minBound
chrPrioCompare :: env -> (subst,x) -> (subst,x) -> Ordering
chrPrioCompare e (s1,x1) (s2,x2) = chrPrioEval e s1 x1 `compare` chrPrioEval e s2 x2
chrPrioLift :: proxy env -> proxy subst -> CHRPrioEvaluatableVal x -> x
newtype Prio = Prio {unPrio :: Word32}
deriving (Eq, Bounded, Num, Enum, Integral, Real)
instance Ord Prio where
compare = flip compare `on` unPrio
{-# INLINE compare #-}
type IsCHRConstraint env c subst
= ( CHRMatchable env c subst
, VarExtractable c
, VarUpdatable c subst
, Typeable c
, TT.TreeTrieKeyable c
, IsConstraint c
, Ord c
, Ord (TT.TrTrKey c)
, PP c
, PP (TT.TrTrKey c)
)
type IsCHRGuard env g subst
= ( CHRCheckable env g subst
, VarExtractable g
, VarUpdatable g subst
, Typeable g
, PP g
)
type IsCHRPrio env p subst
= ( CHRPrioEvaluatable env p subst
, Typeable p
, PP p
)
type IsCHRBacktrackPrio env bp subst
= ( IsCHRPrio env bp subst
, CHRMatchable env bp subst
, PP (CHRPrioEvaluatableVal bp)
)
data ConstraintSolvesVia
= ConstraintSolvesVia_Rule
| ConstraintSolvesVia_Solve
| ConstraintSolvesVia_Residual
| ConstraintSolvesVia_Fail
| ConstraintSolvesVia_Succeed
deriving (Show, Enum, Eq, Ord)
instance PP ConstraintSolvesVia where
pp = pp . show
class IsConstraint c where
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
data CHRTrOpt
= CHRTrOpt_Lookup
| CHRTrOpt_Stats
deriving (Eq, Ord, Show)
class CHREmptySubstitution subst where
chrEmptySubst :: subst
type family CHRMatchableKey subst :: *
type instance CHRMatchableKey (StackedVarLookup subst) = CHRMatchableKey subst
class (CHREmptySubstitution subst, LookupApply subst subst, VarExtractable x, VarLookupKey subst ~ ExtrValVarKey x) => CHRMatchable env x subst where
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
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
chrMatchToM :: env -> x -> x -> CHRMatcher subst ()
chrMatchToM e x1 x2 = chrUnifyM CHRMatchHow_Match e x1 x2
chrUnifyM :: CHRMatchHow -> env -> x -> x -> CHRMatcher subst ()
chrUnifyM how e x1 x2 = getl chrmatcherstateEnv >>= \menv -> chrmatcherLift $ \sg -> chrUnify how menv e sg x1 x2
chrBuiltinSolveM :: env -> x -> CHRMatcher subst ()
chrBuiltinSolveM e x = return ()
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
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
chrmatcherLift :: (LookupApply subst subst) => (subst -> Maybe subst) -> CHRMatcher subst ()
chrmatcherLift f = do
[sl,sg] <- fmap Lk.unlifts $ getl chrmatcherstateVarLookup
maybe chrMatchFail (\snew -> chrmatcherstateVarLookup =$: (Lk.apply snew)) $ f sg
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
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)
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 #-}
chrMatchFail :: CHRMatcher subst a
chrMatchFail = throwError CHRMatcherFailure
{-# INLINE chrMatchFail #-}
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 (\(s,w,e) -> (s,f w,e))
{-# INLINE chrMatchModifyWait #-}
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
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
instance Show Prio where
show = show . unPrio
instance PP Prio where
pp = pp . unPrio
type instance CHRPrioEvaluatableVal () = Prio