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

-------------------------------------------------------------------------------------------
--- Constraint Handling Rules
-------------------------------------------------------------------------------------------

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 -- .Strict
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

-------------------------------------------------------------------------------------------
--- Name <-> Var mapping
-------------------------------------------------------------------------------------------

type IVar      = IntMap.Key

type VarToNmMp = IntMap.IntMap   String
type NmToVarMp = MapH.HashMap    String  IVar

VarToNmMp
emptyVarToNmMp :: VarToNmMp = forall a. IntMap a
IntMap.empty
NmToVarMp
emptyNmToVarMp :: NmToVarMp = forall k v. HashMap k v
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 (Eq CHRMatchHow
CHRMatchHow -> CHRMatchHow -> Bool
CHRMatchHow -> CHRMatchHow -> Ordering
CHRMatchHow -> CHRMatchHow -> CHRMatchHow
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: CHRMatchHow -> CHRMatchHow -> CHRMatchHow
$cmin :: CHRMatchHow -> CHRMatchHow -> CHRMatchHow
max :: CHRMatchHow -> CHRMatchHow -> CHRMatchHow
$cmax :: CHRMatchHow -> CHRMatchHow -> CHRMatchHow
>= :: CHRMatchHow -> CHRMatchHow -> Bool
$c>= :: CHRMatchHow -> CHRMatchHow -> Bool
> :: CHRMatchHow -> CHRMatchHow -> Bool
$c> :: CHRMatchHow -> CHRMatchHow -> Bool
<= :: CHRMatchHow -> CHRMatchHow -> Bool
$c<= :: CHRMatchHow -> CHRMatchHow -> Bool
< :: CHRMatchHow -> CHRMatchHow -> Bool
$c< :: CHRMatchHow -> CHRMatchHow -> Bool
compare :: CHRMatchHow -> CHRMatchHow -> Ordering
$ccompare :: CHRMatchHow -> CHRMatchHow -> Ordering
Ord, CHRMatchHow -> CHRMatchHow -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: CHRMatchHow -> CHRMatchHow -> Bool
$c/= :: CHRMatchHow -> CHRMatchHow -> Bool
== :: CHRMatchHow -> CHRMatchHow -> Bool
$c== :: CHRMatchHow -> CHRMatchHow -> Bool
Eq)

-------------------------------------------------------------------------------------------
--- CHRMatchEnv
-------------------------------------------------------------------------------------------

-- | Context/environment required for matching itself
data CHRMatchEnv k
  = CHRMatchEnv
      { {- chrmatchenvHow          :: !CHRMatchHow
      , -} 
        forall k. CHRMatchEnv k -> k -> Bool
chrmatchenvMetaMayBind  :: !(k -> Bool)
      }

emptyCHRMatchEnv :: CHRMatchEnv x
emptyCHRMatchEnv :: forall x. CHRMatchEnv x
emptyCHRMatchEnv = forall k. (k -> Bool) -> CHRMatchEnv k
CHRMatchEnv {- CHRMatchHow_Check -} (forall a b. a -> b -> a
const Bool
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 :: forall subst k.
StackedVarLookup subst
-> CHRWaitForVarSet (StackedElt (StackedVarLookup subst))
-> CHRMatchEnv k
-> CHRMatcherState subst k
mkCHRMatcherState StackedVarLookup subst
s CHRWaitForVarSet (StackedElt (StackedVarLookup subst))
w CHRMatchEnv k
e = (StackedVarLookup subst
s, CHRWaitForVarSet (StackedElt (StackedVarLookup subst))
w, CHRMatchEnv k
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 :: forall subst k. CHRMatcherState subst k -> CHRMatcherState subst k
unCHRMatcherState = forall a. a -> a
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 :: (a -> f a) -> (a, b, c) -> f (a, b, c)
chrmatcherstateVarLookup     = forall a b c. Lens (a, b, c) a
fst3l
chrmatcherstateWaitForVarSet :: (b -> f b) -> (a, b, c) -> f (a, b, c)
chrmatcherstateWaitForVarSet = forall a b c. Lens (a, b, c) b
snd3l
chrmatcherstateEnv :: (c -> f c) -> (a, b, c) -> f (a, b, c)
chrmatcherstateEnv           = forall a b c. Lens (a, b, c) c
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 :: 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 CHRMatchHow
how VarLookupVal s -> VarLookupVal s -> CHRMatcher s ()
ok VarLookupVal s
t1 VarLookupVal s
t2
  = VarLookupVal s
-> VarLookupVal s
-> StateT
     (StackedVarLookup s, Set (VarLookupKey s),
      CHRMatchEnv (VarLookupKey s))
     (Either CHRMatcherFailure)
     ()
cmp VarLookupVal s
t1 VarLookupVal s
t2
  where cmp :: VarLookupVal s
-> VarLookupVal s
-> StateT
     (StackedVarLookup s, Set (VarLookupKey s),
      CHRMatchEnv (VarLookupKey s))
     (Either CHRMatcherFailure)
     ()
cmp VarLookupVal s
t1 VarLookupVal s
t2 = do
          CHRMatchEnv (ExtrValVarKey (VarLookupVal s))
menv <- forall f (m :: * -> *) o. MonadState f m => (f :-> o) -> m o
getl forall {f :: * -> *} {c} {a} {b}.
Functor f =>
(c -> f c) -> (a, b, c) -> f (a, b, c)
chrmatcherstateEnv
          case (forall vv. VarTerm vv => vv -> Maybe (ExtrValVarKey vv)
varTermMbKey VarLookupVal s
t1, forall vv. VarTerm vv => vv -> Maybe (ExtrValVarKey vv)
varTermMbKey VarLookupVal s
t2) of
              (Just ExtrValVarKey (VarLookupVal s)
v1, Just ExtrValVarKey (VarLookupVal s)
v2) | ExtrValVarKey (VarLookupVal s)
v1 forall a. Eq a => a -> a -> Bool
== ExtrValVarKey (VarLookupVal s)
v2                         -> forall subst. CHRMatcher subst ()
chrMatchSuccess
                                 | CHRMatchHow
how forall a. Eq a => a -> a -> Bool
== CHRMatchHow
CHRMatchHow_Check         -> forall {subst} {a}.
(ExtrValVarKey (VarLookupVal subst) ~ VarLookupKey subst,
 Lookup subst (VarLookupKey subst) (VarLookupVal subst),
 VarTerm (VarLookupVal subst)) =>
StateT
  (StackedVarLookup subst, Set (VarLookupKey subst),
   CHRMatchEnv (VarLookupKey subst))
  (Either CHRMatcherFailure)
  a
-> (VarLookupVal subst
    -> StateT
         (StackedVarLookup subst, Set (VarLookupKey subst),
          CHRMatchEnv (VarLookupKey subst))
         (Either CHRMatcherFailure)
         a)
-> VarLookupKey subst
-> StateT
     (StackedVarLookup subst, Set (VarLookupKey subst),
      CHRMatchEnv (VarLookupKey subst))
     (Either CHRMatcherFailure)
     a
varContinue
                                                                         (forall {subst} {a}.
(ExtrValVarKey (VarLookupVal subst) ~ VarLookupKey subst,
 Lookup subst (VarLookupKey subst) (VarLookupVal subst),
 VarTerm (VarLookupVal subst)) =>
StateT
  (StackedVarLookup subst, Set (VarLookupKey subst),
   CHRMatchEnv (VarLookupKey subst))
  (Either CHRMatcherFailure)
  a
-> (VarLookupVal subst
    -> StateT
         (StackedVarLookup subst, Set (VarLookupKey subst),
          CHRMatchEnv (VarLookupKey subst))
         (Either CHRMatcherFailure)
         a)
-> VarLookupKey subst
-> StateT
     (StackedVarLookup subst, Set (VarLookupKey subst),
      CHRMatchEnv (VarLookupKey subst))
     (Either CHRMatcherFailure)
     a
varContinue (ExtrValVarKey (VarLookupVal s)
-> StateT
     (StackedVarLookup s, Set (VarLookupKey s),
      CHRMatchEnv (VarLookupKey s))
     (Either CHRMatcherFailure)
     ()
waitv ExtrValVarKey (VarLookupVal s)
v1 forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ExtrValVarKey (VarLookupVal s)
-> StateT
     (StackedVarLookup s, Set (VarLookupKey s),
      CHRMatchEnv (VarLookupKey s))
     (Either CHRMatcherFailure)
     ()
waitv ExtrValVarKey (VarLookupVal s)
v2) (VarLookupVal s -> VarLookupVal s -> CHRMatcher s ()
ok VarLookupVal s
t1) ExtrValVarKey (VarLookupVal s)
v2)
                                                                         (\VarLookupVal s
t1 -> forall {subst} {a}.
(ExtrValVarKey (VarLookupVal subst) ~ VarLookupKey subst,
 Lookup subst (VarLookupKey subst) (VarLookupVal subst),
 VarTerm (VarLookupVal subst)) =>
StateT
  (StackedVarLookup subst, Set (VarLookupKey subst),
   CHRMatchEnv (VarLookupKey subst))
  (Either CHRMatcherFailure)
  a
-> (VarLookupVal subst
    -> StateT
         (StackedVarLookup subst, Set (VarLookupKey subst),
          CHRMatchEnv (VarLookupKey subst))
         (Either CHRMatcherFailure)
         a)
-> VarLookupKey subst
-> StateT
     (StackedVarLookup subst, Set (VarLookupKey subst),
      CHRMatchEnv (VarLookupKey subst))
     (Either CHRMatcherFailure)
     a
varContinue (VarLookupVal s
-> StateT
     (StackedVarLookup s, Set (VarLookupKey s),
      CHRMatchEnv (VarLookupKey s))
     (Either CHRMatcherFailure)
     ()
waitt VarLookupVal s
t1 forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ExtrValVarKey (VarLookupVal s)
-> StateT
     (StackedVarLookup s, Set (VarLookupKey s),
      CHRMatchEnv (VarLookupKey s))
     (Either CHRMatcherFailure)
     ()
waitv ExtrValVarKey (VarLookupVal s)
v2) (VarLookupVal s -> VarLookupVal s -> CHRMatcher s ()
ok VarLookupVal s
t1) ExtrValVarKey (VarLookupVal s)
v2)
                                                                         ExtrValVarKey (VarLookupVal s)
v1
                                 where waitv :: ExtrValVarKey (VarLookupVal s)
-> StateT
     (StackedVarLookup s, Set (VarLookupKey s),
      CHRMatchEnv (VarLookupKey s))
     (Either CHRMatcherFailure)
     ()
waitv ExtrValVarKey (VarLookupVal s)
v = forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall k. CHRMatchEnv k -> k -> Bool
chrmatchenvMetaMayBind CHRMatchEnv (ExtrValVarKey (VarLookupVal s))
menv ExtrValVarKey (VarLookupVal s)
v) forall a b. (a -> b) -> a -> b
$ forall k subst.
(Ord k, k ~ VarLookupKey subst) =>
k -> CHRMatcher subst ()
chrMatchWait ExtrValVarKey (VarLookupVal s)
v
                                       waitt :: VarLookupVal s
-> StateT
     (StackedVarLookup s, Set (VarLookupKey s),
      CHRMatchEnv (VarLookupKey s))
     (Either CHRMatcherFailure)
     ()
waitt = forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall (m :: * -> *) a. Monad m => a -> m a
return ()) ExtrValVarKey (VarLookupVal s)
-> StateT
     (StackedVarLookup s, Set (VarLookupKey s),
      CHRMatchEnv (VarLookupKey s))
     (Either CHRMatcherFailure)
     ()
waitv forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall vv. VarTerm vv => vv -> Maybe (ExtrValVarKey vv)
varTermMbKey
              (Just ExtrValVarKey (VarLookupVal s)
v1, Maybe (ExtrValVarKey (VarLookupVal s))
_      ) | CHRMatchHow
how forall a. Eq a => a -> a -> Bool
== CHRMatchHow
CHRMatchHow_Check         -> forall {subst} {a}.
(ExtrValVarKey (VarLookupVal subst) ~ VarLookupKey subst,
 Lookup subst (VarLookupKey subst) (VarLookupVal subst),
 VarTerm (VarLookupVal subst)) =>
StateT
  (StackedVarLookup subst, Set (VarLookupKey subst),
   CHRMatchEnv (VarLookupKey subst))
  (Either CHRMatcherFailure)
  a
-> (VarLookupVal subst
    -> StateT
         (StackedVarLookup subst, Set (VarLookupKey subst),
          CHRMatchEnv (VarLookupKey subst))
         (Either CHRMatcherFailure)
         a)
-> VarLookupKey subst
-> StateT
     (StackedVarLookup subst, Set (VarLookupKey subst),
      CHRMatchEnv (VarLookupKey subst))
     (Either CHRMatcherFailure)
     a
varContinue (if Bool
maybind then forall subst a. CHRMatcher subst a
chrMatchFail else forall k subst.
(Ord k, k ~ VarLookupKey subst) =>
k -> CHRMatcher subst ()
chrMatchWait ExtrValVarKey (VarLookupVal s)
v1) (forall a b c. (a -> b -> c) -> b -> a -> c
flip VarLookupVal s -> VarLookupVal s -> CHRMatcher s ()
ok VarLookupVal s
t2) ExtrValVarKey (VarLookupVal s)
v1
                                 | CHRMatchHow
how forall a. Ord a => a -> a -> Bool
>= CHRMatchHow
CHRMatchHow_Match Bool -> Bool -> Bool
&& Bool
maybind
                                                                    -> forall {subst} {a}.
(ExtrValVarKey (VarLookupVal subst) ~ VarLookupKey subst,
 Lookup subst (VarLookupKey subst) (VarLookupVal subst),
 VarTerm (VarLookupVal subst)) =>
StateT
  (StackedVarLookup subst, Set (VarLookupKey subst),
   CHRMatchEnv (VarLookupKey subst))
  (Either CHRMatcherFailure)
  a
-> (VarLookupVal subst
    -> StateT
         (StackedVarLookup subst, Set (VarLookupKey subst),
          CHRMatchEnv (VarLookupKey subst))
         (Either CHRMatcherFailure)
         a)
-> VarLookupKey subst
-> StateT
     (StackedVarLookup subst, Set (VarLookupKey subst),
      CHRMatchEnv (VarLookupKey subst))
     (Either CHRMatcherFailure)
     a
varContinue (forall subst k v.
(LookupApply subst subst, Lookup subst k v, k ~ VarLookupKey subst,
 v ~ VarLookupVal subst) =>
k -> v -> CHRMatcher subst ()
chrMatchBind ExtrValVarKey (VarLookupVal s)
v1 VarLookupVal s
t2) (forall a b c. (a -> b -> c) -> b -> a -> c
flip VarLookupVal s -> VarLookupVal s -> CHRMatcher s ()
ok VarLookupVal s
t2) ExtrValVarKey (VarLookupVal s)
v1
                                 | Bool
otherwise                        -> forall {subst} {a}.
(ExtrValVarKey (VarLookupVal subst) ~ VarLookupKey subst,
 Lookup subst (VarLookupKey subst) (VarLookupVal subst),
 VarTerm (VarLookupVal subst)) =>
StateT
  (StackedVarLookup subst, Set (VarLookupKey subst),
   CHRMatchEnv (VarLookupKey subst))
  (Either CHRMatcherFailure)
  a
-> (VarLookupVal subst
    -> StateT
         (StackedVarLookup subst, Set (VarLookupKey subst),
          CHRMatchEnv (VarLookupKey subst))
         (Either CHRMatcherFailure)
         a)
-> VarLookupKey subst
-> StateT
     (StackedVarLookup subst, Set (VarLookupKey subst),
      CHRMatchEnv (VarLookupKey subst))
     (Either CHRMatcherFailure)
     a
varContinue forall subst a. CHRMatcher subst a
chrMatchFail (forall a b c. (a -> b -> c) -> b -> a -> c
flip VarLookupVal s -> VarLookupVal s -> CHRMatcher s ()
ok VarLookupVal s
t2) ExtrValVarKey (VarLookupVal s)
v1
                                 where maybind :: Bool
maybind = forall k. CHRMatchEnv k -> k -> Bool
chrmatchenvMetaMayBind CHRMatchEnv (ExtrValVarKey (VarLookupVal s))
menv ExtrValVarKey (VarLookupVal s)
v1
              (Maybe (ExtrValVarKey (VarLookupVal s))
_      , Just ExtrValVarKey (VarLookupVal s)
v2) | CHRMatchHow
how forall a. Eq a => a -> a -> Bool
== CHRMatchHow
CHRMatchHow_Check         -> forall {subst} {a}.
(ExtrValVarKey (VarLookupVal subst) ~ VarLookupKey subst,
 Lookup subst (VarLookupKey subst) (VarLookupVal subst),
 VarTerm (VarLookupVal subst)) =>
StateT
  (StackedVarLookup subst, Set (VarLookupKey subst),
   CHRMatchEnv (VarLookupKey subst))
  (Either CHRMatcherFailure)
  a
-> (VarLookupVal subst
    -> StateT
         (StackedVarLookup subst, Set (VarLookupKey subst),
          CHRMatchEnv (VarLookupKey subst))
         (Either CHRMatcherFailure)
         a)
-> VarLookupKey subst
-> StateT
     (StackedVarLookup subst, Set (VarLookupKey subst),
      CHRMatchEnv (VarLookupKey subst))
     (Either CHRMatcherFailure)
     a
varContinue (if Bool
maybind then forall subst a. CHRMatcher subst a
chrMatchFail else forall k subst.
(Ord k, k ~ VarLookupKey subst) =>
k -> CHRMatcher subst ()
chrMatchWait ExtrValVarKey (VarLookupVal s)
v2) (VarLookupVal s -> VarLookupVal s -> CHRMatcher s ()
ok VarLookupVal s
t1) ExtrValVarKey (VarLookupVal s)
v2
                                 | CHRMatchHow
how forall a. Eq a => a -> a -> Bool
== CHRMatchHow
CHRMatchHow_MatchAndWait  -> forall {subst} {a}.
(ExtrValVarKey (VarLookupVal subst) ~ VarLookupKey subst,
 Lookup subst (VarLookupKey subst) (VarLookupVal subst),
 VarTerm (VarLookupVal subst)) =>
StateT
  (StackedVarLookup subst, Set (VarLookupKey subst),
   CHRMatchEnv (VarLookupKey subst))
  (Either CHRMatcherFailure)
  a
-> (VarLookupVal subst
    -> StateT
         (StackedVarLookup subst, Set (VarLookupKey subst),
          CHRMatchEnv (VarLookupKey subst))
         (Either CHRMatcherFailure)
         a)
-> VarLookupKey subst
-> StateT
     (StackedVarLookup subst, Set (VarLookupKey subst),
      CHRMatchEnv (VarLookupKey subst))
     (Either CHRMatcherFailure)
     a
varContinue (forall k subst.
(Ord k, k ~ VarLookupKey subst) =>
k -> CHRMatcher subst ()
chrMatchWait ExtrValVarKey (VarLookupVal s)
v2) (VarLookupVal s -> VarLookupVal s -> CHRMatcher s ()
ok VarLookupVal s
t1) ExtrValVarKey (VarLookupVal s)
v2
                                 | CHRMatchHow
how forall a. Eq a => a -> a -> Bool
== CHRMatchHow
CHRMatchHow_Unify Bool -> Bool -> Bool
&& Bool
maybind
                                                                    -> forall {subst} {a}.
(ExtrValVarKey (VarLookupVal subst) ~ VarLookupKey subst,
 Lookup subst (VarLookupKey subst) (VarLookupVal subst),
 VarTerm (VarLookupVal subst)) =>
StateT
  (StackedVarLookup subst, Set (VarLookupKey subst),
   CHRMatchEnv (VarLookupKey subst))
  (Either CHRMatcherFailure)
  a
-> (VarLookupVal subst
    -> StateT
         (StackedVarLookup subst, Set (VarLookupKey subst),
          CHRMatchEnv (VarLookupKey subst))
         (Either CHRMatcherFailure)
         a)
-> VarLookupKey subst
-> StateT
     (StackedVarLookup subst, Set (VarLookupKey subst),
      CHRMatchEnv (VarLookupKey subst))
     (Either CHRMatcherFailure)
     a
varContinue (forall subst k v.
(LookupApply subst subst, Lookup subst k v, k ~ VarLookupKey subst,
 v ~ VarLookupVal subst) =>
k -> v -> CHRMatcher subst ()
chrMatchBind ExtrValVarKey (VarLookupVal s)
v2 VarLookupVal s
t1) (VarLookupVal s -> VarLookupVal s -> CHRMatcher s ()
ok VarLookupVal s
t1) ExtrValVarKey (VarLookupVal s)
v2
                                 | Bool
otherwise                        -> forall {subst} {a}.
(ExtrValVarKey (VarLookupVal subst) ~ VarLookupKey subst,
 Lookup subst (VarLookupKey subst) (VarLookupVal subst),
 VarTerm (VarLookupVal subst)) =>
StateT
  (StackedVarLookup subst, Set (VarLookupKey subst),
   CHRMatchEnv (VarLookupKey subst))
  (Either CHRMatcherFailure)
  a
-> (VarLookupVal subst
    -> StateT
         (StackedVarLookup subst, Set (VarLookupKey subst),
          CHRMatchEnv (VarLookupKey subst))
         (Either CHRMatcherFailure)
         a)
-> VarLookupKey subst
-> StateT
     (StackedVarLookup subst, Set (VarLookupKey subst),
      CHRMatchEnv (VarLookupKey subst))
     (Either CHRMatcherFailure)
     a
varContinue forall subst a. CHRMatcher subst a
chrMatchFail (VarLookupVal s -> VarLookupVal s -> CHRMatcher s ()
ok VarLookupVal s
t1) ExtrValVarKey (VarLookupVal s)
v2
                                 where maybind :: Bool
maybind = forall k. CHRMatchEnv k -> k -> Bool
chrmatchenvMetaMayBind CHRMatchEnv (ExtrValVarKey (VarLookupVal s))
menv ExtrValVarKey (VarLookupVal s)
v2
              (Maybe (ExtrValVarKey (VarLookupVal s)),
 Maybe (ExtrValVarKey (VarLookupVal s)))
_                                                     -> forall subst a. CHRMatcher subst a
chrMatchFail -- ok t1 t2
        varContinue :: StateT
  (StackedVarLookup subst, Set (VarLookupKey subst),
   CHRMatchEnv (VarLookupKey subst))
  (Either CHRMatcherFailure)
  a
-> (VarLookupVal (StackedVarLookup subst)
    -> StateT
         (StackedVarLookup subst, Set (VarLookupKey subst),
          CHRMatchEnv (VarLookupKey subst))
         (Either CHRMatcherFailure)
         a)
-> VarLookupKey (StackedVarLookup subst)
-> StateT
     (StackedVarLookup subst, Set (VarLookupKey subst),
      CHRMatchEnv (VarLookupKey subst))
     (Either CHRMatcherFailure)
     a
varContinue = forall (m :: * -> *) s a.
(Monad m, Lookup s (VarLookupKey s) (VarLookupVal s)) =>
(VarLookupVal s -> Maybe (VarLookupKey s))
-> m s -> m a -> (VarLookupVal s -> m a) -> VarLookupKey s -> m a
Lk.lookupResolveAndContinueM forall vv. VarTerm vv => vv -> Maybe (ExtrValVarKey vv)
varTermMbKey forall subst. CHRMatcher subst (StackedVarLookup subst)
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 env
e subst
s x
x = forall subst.
CHREmptySubstitution subst =>
CHRMatcher subst ()
-> CHRMatchEnv (VarLookupKey subst) -> subst -> Maybe subst
chrmatcherUnlift (forall env x subst.
CHRCheckable env x subst =>
env -> x -> CHRMatcher subst ()
chrCheckM env
e x
x) forall x. CHRMatchEnv x
emptyCHRMatchEnv subst
s

  chrCheckM :: env -> x -> CHRMatcher subst ()
  chrCheckM env
e x
x = forall subst.
LookupApply subst subst =>
(subst -> Maybe subst) -> CHRMatcher subst ()
chrmatcherLift forall a b. (a -> b) -> a -> b
$ \subst
sg -> forall env x subst.
CHRCheckable env x subst =>
env -> subst -> x -> Maybe subst
chrCheck env
e subst
sg x
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 where
  -- | Reduce to a prio representation
  chrPrioEval :: env -> subst -> x -> CHRPrioEvaluatableVal x
  chrPrioEval env
_ subst
_ x
_ = forall a. Bounded a => a
minBound

  -- | Compare priorities
  chrPrioCompare :: env -> (subst,x) -> (subst,x) -> Ordering
  chrPrioCompare env
e (subst
s1,x
x1) (subst
s2,x
x2) = forall env x subst.
CHRPrioEvaluatable env x subst =>
env -> subst -> x -> CHRPrioEvaluatableVal x
chrPrioEval env
e subst
s1 x
x1 forall a. Ord a => a -> a -> Ordering
`compare` forall env x subst.
CHRPrioEvaluatable env x subst =>
env -> subst -> x -> CHRPrioEvaluatableVal x
chrPrioEval env
e subst
s2 x
x2
  
  -- | Lift prio val into prio
  chrPrioLift :: proxy env -> proxy subst -> 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 {Prio -> Word32
unPrio :: Word32}
  deriving (Prio -> Prio -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Prio -> Prio -> Bool
$c/= :: Prio -> Prio -> Bool
== :: Prio -> Prio -> Bool
$c== :: Prio -> Prio -> Bool
Eq, Prio
forall a. a -> a -> Bounded a
maxBound :: Prio
$cmaxBound :: Prio
minBound :: Prio
$cminBound :: Prio
Bounded, Integer -> Prio
Prio -> Prio
Prio -> Prio -> Prio
forall a.
(a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a)
-> (a -> a)
-> (a -> a)
-> (Integer -> a)
-> Num a
fromInteger :: Integer -> Prio
$cfromInteger :: Integer -> Prio
signum :: Prio -> Prio
$csignum :: Prio -> Prio
abs :: Prio -> Prio
$cabs :: Prio -> Prio
negate :: Prio -> Prio
$cnegate :: Prio -> Prio
* :: Prio -> Prio -> Prio
$c* :: Prio -> Prio -> Prio
- :: Prio -> Prio -> Prio
$c- :: Prio -> Prio -> Prio
+ :: Prio -> Prio -> Prio
$c+ :: Prio -> Prio -> Prio
Num, Int -> Prio
Prio -> Int
Prio -> [Prio]
Prio -> Prio
Prio -> Prio -> [Prio]
Prio -> Prio -> Prio -> [Prio]
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
enumFromThenTo :: Prio -> Prio -> Prio -> [Prio]
$cenumFromThenTo :: Prio -> Prio -> Prio -> [Prio]
enumFromTo :: Prio -> Prio -> [Prio]
$cenumFromTo :: Prio -> Prio -> [Prio]
enumFromThen :: Prio -> Prio -> [Prio]
$cenumFromThen :: Prio -> Prio -> [Prio]
enumFrom :: Prio -> [Prio]
$cenumFrom :: Prio -> [Prio]
fromEnum :: Prio -> Int
$cfromEnum :: Prio -> Int
toEnum :: Int -> Prio
$ctoEnum :: Int -> Prio
pred :: Prio -> Prio
$cpred :: Prio -> Prio
succ :: Prio -> Prio
$csucc :: Prio -> Prio
Enum, Enum Prio
Real Prio
Prio -> Integer
Prio -> Prio -> (Prio, Prio)
Prio -> Prio -> Prio
forall a.
Real a
-> Enum a
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> (a, a))
-> (a -> a -> (a, a))
-> (a -> Integer)
-> Integral a
toInteger :: Prio -> Integer
$ctoInteger :: Prio -> Integer
divMod :: Prio -> Prio -> (Prio, Prio)
$cdivMod :: Prio -> Prio -> (Prio, Prio)
quotRem :: Prio -> Prio -> (Prio, Prio)
$cquotRem :: Prio -> Prio -> (Prio, Prio)
mod :: Prio -> Prio -> Prio
$cmod :: Prio -> Prio -> Prio
div :: Prio -> Prio -> Prio
$cdiv :: Prio -> Prio -> Prio
rem :: Prio -> Prio -> Prio
$crem :: Prio -> Prio -> Prio
quot :: Prio -> Prio -> Prio
$cquot :: Prio -> Prio -> Prio
Integral, Num Prio
Ord Prio
Prio -> Rational
forall a. Num a -> Ord a -> (a -> Rational) -> Real a
toRational :: Prio -> Rational
$ctoRational :: Prio -> Rational
Real)

instance Ord Prio where
  compare :: Prio -> Prio -> Ordering
compare = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a. Ord a => a -> a -> Ordering
compare forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Prio -> Word32
unPrio
  {-# INLINE compare #-}
  
-------------------------------------------------------------------------------------------
--- Constraint API
-------------------------------------------------------------------------------------------

-- | Alias API for constraint requirements
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
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
type IsCHRPrio env p subst
    = ( CHRPrioEvaluatable env p subst
      , Typeable p
      -- , Serialize p
      , PP p
      )

-- | Alias API for backtrack priority requirements
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 (Int -> ConstraintSolvesVia -> ShowS
[ConstraintSolvesVia] -> ShowS
ConstraintSolvesVia -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ConstraintSolvesVia] -> ShowS
$cshowList :: [ConstraintSolvesVia] -> ShowS
show :: ConstraintSolvesVia -> String
$cshow :: ConstraintSolvesVia -> String
showsPrec :: Int -> ConstraintSolvesVia -> ShowS
$cshowsPrec :: Int -> ConstraintSolvesVia -> ShowS
Show, Int -> ConstraintSolvesVia
ConstraintSolvesVia -> Int
ConstraintSolvesVia -> [ConstraintSolvesVia]
ConstraintSolvesVia -> ConstraintSolvesVia
ConstraintSolvesVia -> ConstraintSolvesVia -> [ConstraintSolvesVia]
ConstraintSolvesVia
-> ConstraintSolvesVia
-> ConstraintSolvesVia
-> [ConstraintSolvesVia]
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
enumFromThenTo :: ConstraintSolvesVia
-> ConstraintSolvesVia
-> ConstraintSolvesVia
-> [ConstraintSolvesVia]
$cenumFromThenTo :: ConstraintSolvesVia
-> ConstraintSolvesVia
-> ConstraintSolvesVia
-> [ConstraintSolvesVia]
enumFromTo :: ConstraintSolvesVia -> ConstraintSolvesVia -> [ConstraintSolvesVia]
$cenumFromTo :: ConstraintSolvesVia -> ConstraintSolvesVia -> [ConstraintSolvesVia]
enumFromThen :: ConstraintSolvesVia -> ConstraintSolvesVia -> [ConstraintSolvesVia]
$cenumFromThen :: ConstraintSolvesVia -> ConstraintSolvesVia -> [ConstraintSolvesVia]
enumFrom :: ConstraintSolvesVia -> [ConstraintSolvesVia]
$cenumFrom :: ConstraintSolvesVia -> [ConstraintSolvesVia]
fromEnum :: ConstraintSolvesVia -> Int
$cfromEnum :: ConstraintSolvesVia -> Int
toEnum :: Int -> ConstraintSolvesVia
$ctoEnum :: Int -> ConstraintSolvesVia
pred :: ConstraintSolvesVia -> ConstraintSolvesVia
$cpred :: ConstraintSolvesVia -> ConstraintSolvesVia
succ :: ConstraintSolvesVia -> ConstraintSolvesVia
$csucc :: ConstraintSolvesVia -> ConstraintSolvesVia
Enum, ConstraintSolvesVia -> ConstraintSolvesVia -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ConstraintSolvesVia -> ConstraintSolvesVia -> Bool
$c/= :: ConstraintSolvesVia -> ConstraintSolvesVia -> Bool
== :: ConstraintSolvesVia -> ConstraintSolvesVia -> Bool
$c== :: ConstraintSolvesVia -> ConstraintSolvesVia -> Bool
Eq, Eq ConstraintSolvesVia
ConstraintSolvesVia -> ConstraintSolvesVia -> Bool
ConstraintSolvesVia -> ConstraintSolvesVia -> Ordering
ConstraintSolvesVia -> ConstraintSolvesVia -> ConstraintSolvesVia
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: ConstraintSolvesVia -> ConstraintSolvesVia -> ConstraintSolvesVia
$cmin :: ConstraintSolvesVia -> ConstraintSolvesVia -> ConstraintSolvesVia
max :: ConstraintSolvesVia -> ConstraintSolvesVia -> ConstraintSolvesVia
$cmax :: ConstraintSolvesVia -> ConstraintSolvesVia -> ConstraintSolvesVia
>= :: ConstraintSolvesVia -> ConstraintSolvesVia -> Bool
$c>= :: ConstraintSolvesVia -> ConstraintSolvesVia -> Bool
> :: ConstraintSolvesVia -> ConstraintSolvesVia -> Bool
$c> :: ConstraintSolvesVia -> ConstraintSolvesVia -> Bool
<= :: ConstraintSolvesVia -> ConstraintSolvesVia -> Bool
$c<= :: ConstraintSolvesVia -> ConstraintSolvesVia -> Bool
< :: ConstraintSolvesVia -> ConstraintSolvesVia -> Bool
$c< :: ConstraintSolvesVia -> ConstraintSolvesVia -> Bool
compare :: ConstraintSolvesVia -> ConstraintSolvesVia -> Ordering
$ccompare :: ConstraintSolvesVia -> ConstraintSolvesVia -> Ordering
Ord)

instance PP ConstraintSolvesVia where
  pp :: ConstraintSolvesVia -> PP_Doc
pp = forall a. PP a => a -> PP_Doc
pp forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
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
c = case forall c. IsConstraint c => c -> ConstraintSolvesVia
cnstrSolvesVia c
c of
    ConstraintSolvesVia
ConstraintSolvesVia_Residual -> Bool
False
    ConstraintSolvesVia
_                            -> Bool
True
  
  cnstrSolvesVia :: c -> ConstraintSolvesVia
  cnstrSolvesVia c
c | forall c. IsConstraint c => c -> Bool
cnstrRequiresSolve c
c = ConstraintSolvesVia
ConstraintSolvesVia_Rule
                   | Bool
otherwise            = ConstraintSolvesVia
ConstraintSolvesVia_Residual

-------------------------------------------------------------------------------------------
--- Tracing options, specific for CHR solvers
-------------------------------------------------------------------------------------------

data CHRTrOpt
  = CHRTrOpt_Lookup     -- ^ trie query
  | CHRTrOpt_Stats      -- ^ various stats
  deriving (CHRTrOpt -> CHRTrOpt -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: CHRTrOpt -> CHRTrOpt -> Bool
$c/= :: CHRTrOpt -> CHRTrOpt -> Bool
== :: CHRTrOpt -> CHRTrOpt -> Bool
$c== :: CHRTrOpt -> CHRTrOpt -> Bool
Eq, Eq CHRTrOpt
CHRTrOpt -> CHRTrOpt -> Bool
CHRTrOpt -> CHRTrOpt -> Ordering
CHRTrOpt -> CHRTrOpt -> CHRTrOpt
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: CHRTrOpt -> CHRTrOpt -> CHRTrOpt
$cmin :: CHRTrOpt -> CHRTrOpt -> CHRTrOpt
max :: CHRTrOpt -> CHRTrOpt -> CHRTrOpt
$cmax :: CHRTrOpt -> CHRTrOpt -> CHRTrOpt
>= :: CHRTrOpt -> CHRTrOpt -> Bool
$c>= :: CHRTrOpt -> CHRTrOpt -> Bool
> :: CHRTrOpt -> CHRTrOpt -> Bool
$c> :: CHRTrOpt -> CHRTrOpt -> Bool
<= :: CHRTrOpt -> CHRTrOpt -> Bool
$c<= :: CHRTrOpt -> CHRTrOpt -> Bool
< :: CHRTrOpt -> CHRTrOpt -> Bool
$c< :: CHRTrOpt -> CHRTrOpt -> Bool
compare :: CHRTrOpt -> CHRTrOpt -> Ordering
$ccompare :: CHRTrOpt -> CHRTrOpt -> Ordering
Ord, Int -> CHRTrOpt -> ShowS
[CHRTrOpt] -> ShowS
CHRTrOpt -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [CHRTrOpt] -> ShowS
$cshowList :: [CHRTrOpt] -> ShowS
show :: CHRTrOpt -> String
$cshow :: CHRTrOpt -> String
showsPrec :: Int -> CHRTrOpt -> ShowS
$cshowsPrec :: Int -> CHRTrOpt -> ShowS
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
env subst
s x
x1 x
x2 = forall env x subst.
CHRMatchable env x subst =>
CHRMatchHow
-> CHRMatchEnv (VarLookupKey subst)
-> env
-> subst
-> x
-> x
-> Maybe subst
chrUnify CHRMatchHow
CHRMatchHow_Match (forall x. CHRMatchEnv x
emptyCHRMatchEnv {chrmatchenvMetaMayBind :: ExtrValVarKey x -> Bool
chrmatchenvMetaMayBind = (forall a. Ord a => a -> Set a -> Bool
`Set.member` forall vv. VarExtractable vv => vv -> Set (ExtrValVarKey vv)
varFreeSet x
x1)}) env
env subst
s x
x1 x
x2
    -- where free = varFreeSet x1
  
  -- | One-directional (1st to 2nd 'x') unify
  chrUnify :: CHRMatchHow -> CHRMatchEnv (VarLookupKey subst) -> env -> subst -> x -> x -> Maybe subst
  chrUnify CHRMatchHow
how CHRMatchEnv (VarLookupKey subst)
menv env
e subst
s x
x1 x
x2 = forall subst.
CHREmptySubstitution subst =>
CHRMatcher subst ()
-> CHRMatchEnv (VarLookupKey subst) -> subst -> Maybe subst
chrmatcherUnlift (forall env x subst.
CHRMatchable env x subst =>
CHRMatchHow -> env -> x -> x -> CHRMatcher subst ()
chrUnifyM CHRMatchHow
how env
e x
x1 x
x2) CHRMatchEnv (VarLookupKey subst)
menv subst
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 env
e x
x1 x
x2 = forall env x subst.
CHRMatchable env x subst =>
CHRMatchHow -> env -> x -> x -> CHRMatcher subst ()
chrUnifyM CHRMatchHow
CHRMatchHow_Match env
e x
x1 x
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 CHRMatchHow
how env
e x
x1 x
x2 = forall f (m :: * -> *) o. MonadState f m => (f :-> o) -> m o
getl forall {f :: * -> *} {c} {a} {b}.
Functor f =>
(c -> f c) -> (a, b, c) -> f (a, b, c)
chrmatcherstateEnv forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \CHRMatchEnv (ExtrValVarKey x)
menv -> forall subst.
LookupApply subst subst =>
(subst -> Maybe subst) -> CHRMatcher subst ()
chrmatcherLift forall a b. (a -> b) -> a -> b
$ \subst
sg -> forall env x subst.
CHRMatchable env x subst =>
CHRMatchHow
-> CHRMatchEnv (VarLookupKey subst)
-> env
-> subst
-> x
-> x
-> Maybe subst
chrUnify CHRMatchHow
how CHRMatchEnv (ExtrValVarKey x)
menv env
e subst
sg x
x1 x
x2

  -- | Solve a constraint which is categorized as 'ConstraintSolvesVia_Solve'
  chrBuiltinSolveM :: env -> x -> CHRMatcher subst ()
  chrBuiltinSolveM env
e x
x = forall (m :: * -> *) a. Monad m => a -> m a
return () -- chrmatcherLift $ \sg -> chrBuiltinSolve e sg x

instance {-# OVERLAPPABLE #-} (CHRMatchable env x subst) => CHRMatchable env (Maybe x) subst where
  chrUnifyM :: CHRMatchHow -> env -> Maybe x -> Maybe x -> CHRMatcher subst ()
chrUnifyM CHRMatchHow
how env
e (Just x
x1) (Just x
x2) = forall env x subst.
CHRMatchable env x subst =>
CHRMatchHow -> env -> x -> x -> CHRMatcher subst ()
chrUnifyM CHRMatchHow
how env
e x
x1 x
x2
  chrUnifyM CHRMatchHow
how env
e  Maybe x
Nothing   Maybe x
Nothing  = forall subst. CHRMatcher subst ()
chrMatchSuccess
  chrUnifyM CHRMatchHow
how env
e Maybe x
_         Maybe x
_         = forall subst a. CHRMatcher subst a
chrMatchFail

instance {-# OVERLAPPABLE #-} (CHRMatchable env x subst) => CHRMatchable env [x] subst where
  chrUnifyM :: CHRMatchHow -> env -> [x] -> [x] -> CHRMatcher subst ()
chrUnifyM CHRMatchHow
how env
e [x]
x1 [x]
x2 | forall (t :: * -> *) a. Foldable t => t a -> Int
length [x]
x1 forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Int
length [x]
x2 = forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_ forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (forall env x subst.
CHRMatchable env x subst =>
CHRMatchHow -> env -> x -> x -> CHRMatcher subst ()
chrUnifyM CHRMatchHow
how env
e) [x]
x1 [x]
x2
  chrUnifyM CHRMatchHow
how env
e [x]
_  [x]
_                           = forall subst a. CHRMatcher subst a
chrMatchFail

-------------------------------------------------------------------------------------------
--- CHRMatcher API, part I
-------------------------------------------------------------------------------------------

-- | Unlift/observe (or run) a CHRMatcher
chrmatcherUnlift :: (CHREmptySubstitution subst) => CHRMatcher subst () -> CHRMatchEnv (VarLookupKey subst) -> (subst -> Maybe subst)
chrmatcherUnlift :: forall subst.
CHREmptySubstitution subst =>
CHRMatcher subst ()
-> CHRMatchEnv (VarLookupKey subst) -> subst -> Maybe subst
chrmatcherUnlift CHRMatcher subst ()
mtch CHRMatchEnv (VarLookupKey subst)
menv subst
s = do
    (subst
s,Set (VarLookupKey subst)
w) <- forall subst.
CHREmptySubstitution subst =>
CHRMatcher subst ()
-> CHRMatchEnv (VarLookupKey subst)
-> subst
-> Maybe (subst, CHRWaitForVarSet subst)
chrmatcherRun CHRMatcher subst ()
mtch CHRMatchEnv (VarLookupKey subst)
menv subst
s
    if forall a. Set a -> Bool
Set.null Set (VarLookupKey subst)
w then forall a. a -> Maybe a
Just subst
s else forall a. Maybe a
Nothing

-- | Lift into CHRMatcher
chrmatcherLift :: (LookupApply subst subst) => (subst -> Maybe subst) -> CHRMatcher subst ()
chrmatcherLift :: forall subst.
LookupApply subst subst =>
(subst -> Maybe subst) -> CHRMatcher subst ()
chrmatcherLift subst -> Maybe subst
f = do
    StackedVarLookup subst
stLk <- forall f (m :: * -> *) o. MonadState f m => (f :-> o) -> m o
getl forall {f :: * -> *} {a} {b} {c}.
Functor f =>
(a -> f a) -> (a, b, c) -> f (a, b, c)
chrmatcherstateVarLookup -- gets (unStackedVarLookup . _chrmatcherstateVarLookup)
    case forall stk. Stacked stk => stk -> [StackedElt stk]
Lk.unlifts StackedVarLookup subst
stLk of
      [StackedElt (StackedVarLookup subst)
sl,StackedElt (StackedVarLookup subst)
sg] -> forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall subst a. CHRMatcher subst a
chrMatchFail (\subst
snew -> forall {f :: * -> *} {a} {b} {c}.
Functor f =>
(a -> f a) -> (a, b, c) -> f (a, b, c)
chrmatcherstateVarLookup forall f (m :: * -> *) o.
MonadState f m =>
(f :-> o) -> (o -> o) -> m ()
=$: (forall l1 l2. LookupApply l1 l2 => l1 -> l2 -> l2
Lk.apply subst
snew)) forall a b. (a -> b) -> a -> b
$ subst -> Maybe subst
f StackedElt (StackedVarLookup subst)
sg
      [StackedElt (StackedVarLookup subst)]
_ -> forall subst a. CHRMatcher subst a
chrMatchFail

-- | Run a CHRMatcher
chrmatcherRun' :: (CHREmptySubstitution subst) => (CHRMatcherFailure -> r) -> (subst -> CHRWaitForVarSet subst -> x -> r) -> CHRMatcher subst x -> CHRMatchEnv (VarLookupKey subst) -> StackedVarLookup subst -> r
chrmatcherRun' :: forall subst r x.
CHREmptySubstitution subst =>
(CHRMatcherFailure -> r)
-> (subst -> CHRWaitForVarSet subst -> x -> r)
-> CHRMatcher subst x
-> CHRMatchEnv (VarLookupKey subst)
-> StackedVarLookup subst
-> r
chrmatcherRun' CHRMatcherFailure -> r
fail subst -> CHRWaitForVarSet subst -> x -> r
succes CHRMatcher subst x
mtch CHRMatchEnv (VarLookupKey subst)
menv StackedVarLookup subst
s = forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either
    CHRMatcherFailure -> r
fail
    ((\(x
x,(StackedVarLookup subst, CHRWaitForVarSet subst,
 CHRMatchEnv (VarLookupKey subst))
ms) -> let (StackedVarLookup subst
s, CHRWaitForVarSet (StackedElt (StackedVarLookup subst))
w, CHRMatchEnv (VarLookupKey subst)
_) = forall subst k. CHRMatcherState subst k -> CHRMatcherState subst k
unCHRMatcherState (StackedVarLookup subst, CHRWaitForVarSet subst,
 CHRMatchEnv (VarLookupKey subst))
ms in subst -> CHRWaitForVarSet subst -> x -> r
succes (forall stk. Stacked stk => stk -> StackedElt stk
Lk.top StackedVarLookup subst
s) CHRWaitForVarSet (StackedElt (StackedVarLookup subst))
w x
x))
      forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> b -> a -> c
flip forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (forall subst k.
StackedVarLookup subst
-> CHRWaitForVarSet (StackedElt (StackedVarLookup subst))
-> CHRMatchEnv k
-> CHRMatcherState subst k
mkCHRMatcherState StackedVarLookup subst
s forall a. Set a
Set.empty CHRMatchEnv (VarLookupKey subst)
menv)
      forall a b. (a -> b) -> a -> b
$ CHRMatcher subst x
mtch

-- | Run a CHRMatcher
chrmatcherRun :: (CHREmptySubstitution subst) => CHRMatcher subst () -> CHRMatchEnv (VarLookupKey subst) -> subst -> Maybe (subst, CHRWaitForVarSet subst)
chrmatcherRun :: forall subst.
CHREmptySubstitution subst =>
CHRMatcher subst ()
-> CHRMatchEnv (VarLookupKey subst)
-> subst
-> Maybe (subst, CHRWaitForVarSet subst)
chrmatcherRun CHRMatcher subst ()
mtch CHRMatchEnv (VarLookupKey subst)
menv subst
s = forall subst r x.
CHREmptySubstitution subst =>
(CHRMatcherFailure -> r)
-> (subst -> CHRWaitForVarSet subst -> x -> r)
-> CHRMatcher subst x
-> CHRMatchEnv (VarLookupKey subst)
-> StackedVarLookup subst
-> r
chrmatcherRun' (forall a b. a -> b -> a
const forall a. Maybe a
Nothing) (\subst
s CHRWaitForVarSet subst
w ()
_ -> forall a. a -> Maybe a
Just (subst
s,CHRWaitForVarSet subst
w)) CHRMatcher subst ()
mtch CHRMatchEnv (VarLookupKey subst)
menv (forall stk. Stacked stk => StackedElt stk -> stk -> stk
Lk.push forall subst. CHREmptySubstitution subst => subst
chrEmptySubst forall a b. (a -> b) -> a -> b
$ forall stk. Stacked stk => StackedElt stk -> stk
Lk.lifts subst
s) -- (StackedVarLookup [chrEmptySubst,s])

-------------------------------------------------------------------------------------------
--- CHRMatcher API, part II
-------------------------------------------------------------------------------------------

chrMatchSubst :: CHRMatcher subst (StackedVarLookup subst)
chrMatchSubst :: forall subst. CHRMatcher subst (StackedVarLookup subst)
chrMatchSubst = forall f (m :: * -> *) o. MonadState f m => (f :-> o) -> m o
getl forall {f :: * -> *} {a} {b} {c}.
Functor f =>
(a -> f a) -> (a, b, c) -> f (a, b, c)
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 :: forall subst k v.
(LookupApply subst subst, Lookup subst k v, k ~ VarLookupKey subst,
 v ~ VarLookupVal subst) =>
k -> v -> CHRMatcher subst ()
chrMatchBind k
k v
v = forall {f :: * -> *} {a} {b} {c}.
Functor f =>
(a -> f a) -> (a, b, c) -> f (a, b, c)
chrmatcherstateVarLookup forall f (m :: * -> *) o.
MonadState f m =>
(f :-> o) -> (o -> o) -> m ()
=$: ((forall c k v. Lookup c k v => k -> v -> c
Lk.singleton k
k v
v :: subst) forall l1 l2. LookupApply l1 l2 => l1 -> l2 -> l2
`Lk.apply`)
{-# INLINE chrMatchBind #-}

chrMatchWait :: (Ord k, k ~ VarLookupKey subst) => k -> CHRMatcher subst ()
chrMatchWait :: forall k subst.
(Ord k, k ~ VarLookupKey subst) =>
k -> CHRMatcher subst ()
chrMatchWait k
k = forall subst.
(CHRWaitForVarSet subst -> CHRWaitForVarSet subst)
-> CHRMatcher subst ()
chrMatchModifyWait (forall a. Ord a => a -> Set a -> Set a
Set.insert k
k)
{-# INLINE chrMatchWait #-}

chrMatchSuccess :: CHRMatcher subst ()
chrMatchSuccess :: forall subst. CHRMatcher subst ()
chrMatchSuccess = forall (m :: * -> *) a. Monad m => a -> m a
return ()
{-# INLINE chrMatchSuccess #-}

-- | Normal CHRMatcher failure
chrMatchFail :: CHRMatcher subst a
chrMatchFail :: forall subst a. CHRMatcher subst a
chrMatchFail = forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError CHRMatcherFailure
CHRMatcherFailure
{-# INLINE chrMatchFail #-}

-- | CHRMatcher failure because a variable binding is missing
chrMatchFailNoBinding :: CHRMatcher subst a
chrMatchFailNoBinding :: forall subst a. CHRMatcher subst a
chrMatchFailNoBinding = forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError CHRMatcherFailure
CHRMatcherFailure_NoBinding
{-# INLINE chrMatchFailNoBinding #-}

chrMatchSucces :: CHRMatcher subst ()
chrMatchSucces :: forall subst. CHRMatcher subst ()
chrMatchSucces = forall (m :: * -> *) a. Monad m => a -> m a
return ()
{-# INLINE chrMatchSucces #-}

chrMatchModifyWait :: (CHRWaitForVarSet subst -> CHRWaitForVarSet subst) -> CHRMatcher subst ()
chrMatchModifyWait :: forall subst.
(CHRWaitForVarSet subst -> CHRWaitForVarSet subst)
-> CHRMatcher subst ()
chrMatchModifyWait Set (VarLookupKey subst) -> Set (VarLookupKey subst)
f =
  -- modify (\st -> st {_chrmatcherstateWaitForVarSet = f $ _chrmatcherstateWaitForVarSet st})
  -- (chrmatcherstateWaitForVarSet =$:)
  forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\(StackedVarLookup subst
s,Set (VarLookupKey subst)
w,CHRMatchEnv (VarLookupKey subst)
e) -> (StackedVarLookup subst
s,Set (VarLookupKey subst) -> Set (VarLookupKey subst)
f Set (VarLookupKey subst)
w,CHRMatchEnv (VarLookupKey subst)
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 :: forall env x subst.
CHRMatchable env x subst =>
Bool -> env -> x -> x -> CHRMatcher subst ()
chrMatchAndWaitToM Bool
wait env
env x
x1 x
x2 = forall env x subst.
CHRMatchable env x subst =>
CHRMatchHow -> env -> x -> x -> CHRMatcher subst ()
chrUnifyM (if Bool
wait then CHRMatchHow
CHRMatchHow_MatchAndWait else CHRMatchHow
CHRMatchHow_Match) env
env x
x1 x
x2

-------------------------------------------------------------------------------------------
--- CHRMatchable: instances
-------------------------------------------------------------------------------------------

-- TBD: move to other file...
instance {-# OVERLAPPABLE #-} Ord (ExtrValVarKey ()) => VarExtractable () where
  varFreeSet :: () -> Set (ExtrValVarKey ())
varFreeSet ()
_ = forall a. Set a
Set.empty

instance {-# OVERLAPPABLE #-} (Ord (ExtrValVarKey ()), CHREmptySubstitution subst, LookupApply subst subst, VarLookupKey subst ~ ExtrValVarKey ()) => CHRMatchable env () subst where
  chrUnifyM :: CHRMatchHow -> env -> () -> () -> CHRMatcher subst ()
chrUnifyM CHRMatchHow
_ env
_ ()
_ ()
_ = forall subst. CHRMatcher subst ()
chrMatchSuccess

-------------------------------------------------------------------------------------------
--- Prio: instances
-------------------------------------------------------------------------------------------

instance Show Prio where
  show :: Prio -> String
show = forall a. Show a => a -> String
show forall b c a. (b -> c) -> (a -> b) -> a -> c
. Prio -> Word32
unPrio

instance PP Prio where
  pp :: Prio -> PP_Doc
pp = forall a. PP a => a -> PP_Doc
pp forall b c a. (b -> c) -> (a -> b) -> a -> c
. Prio -> Word32
unPrio

-------------------------------------------------------------------------------------------
--- CHRPrioEvaluatable: instances
-------------------------------------------------------------------------------------------

type instance CHRPrioEvaluatableVal () = Prio