Safe Haskell	Safe-Inferred
Language	Haskell2010

CHR.Types

Description

CHR TreeTrie based solver shared internals, for all solvers

Synopsis

class (CHREmptySubstitution subst, LookupApply subst subst, VarExtractable x, VarLookupKey subst ~ ExtrValVarKey x) => CHRMatchable env x subst
type family CHRMatchableKey subst :: *
class CHREmptySubstitution subst
class IsConstraint c
type IsCHRBacktrackPrio env bp subst = (IsCHRPrio env bp subst, CHRMatchable env bp subst, PP (CHRPrioEvaluatableVal bp))
type IsCHRPrio env p subst = (CHRPrioEvaluatable env p subst, Typeable p, PP p)
type IsCHRGuard env g subst = (CHRCheckable env g subst, VarExtractable g, VarUpdatable g subst, Typeable g, PP g)
type IsCHRConstraint env c subst = (CHRMatchable env c subst, VarExtractable c, VarUpdatable c subst, Typeable c, TreeTrieKeyable c, IsConstraint c, Ord c, Ord (TrTrKey c), PP c, PP (TrTrKey c))
data Prio
class (Ord (CHRPrioEvaluatableVal x), Bounded (CHRPrioEvaluatableVal x)) => CHRPrioEvaluatable env x subst
type family CHRPrioEvaluatableVal p :: *
class (CHREmptySubstitution subst, LookupApply subst subst) => CHRCheckable env x subst
type CHRMatcher subst = StateT (CHRMatcherState subst (VarLookupKey subst)) (Either CHRMatcherFailure)
data CHRMatcherFailure
type NmToVarMp = HashMap String IVar
type IVar = Key
emptyNmToVarMp :: NmToVarMp
type family TrTrKey x
type CHRKey v = Key (TrTrKey v)
type WorkTime = Int
initWorkTime :: WorkTime
data Work' k c
- = Work {
  - workKey :: k
  - workCnstr :: !c
  - workTime :: WorkTime
  }
- | Work_Residue {
  - workCnstr :: !c
  }
- | Work_Solve {
  - workCnstr :: !c
  }
- | Work_Fail
type Work c = Work' (WorkKey c) c
data SolveStep' c r s
- = SolveStep {
  - stepChr :: r
  - stepSubst :: s
  - stepAlt :: Maybe [c]
  - stepNewTodo :: [c]
  - stepNewDone :: [c]
  }
- | SolveStats {
  - stepStats :: Map String PP_Doc
  }
- | SolveDbg {
  - stepPP :: PP_Doc
  }
type SolveTrace' c r s = [SolveStep' c r s]
emptySolveTrace :: SolveTrace' c r s
ppSolveTrace :: (PP r, PP c) => SolveTrace' c r s -> PP_Doc

Documentation

class (CHREmptySubstitution subst, LookupApply subst subst, VarExtractable x, VarLookupKey subst ~ ExtrValVarKey x) => CHRMatchable env x subst Source #

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.

Instances

Instances details

(Ord (ExtrValVarKey ()), CHREmptySubstitution subst, LookupApply subst subst, VarLookupKey subst ~ ExtrValVarKey ()) => CHRMatchable env () subst Source #
Instance details Defined in CHR.Types.Core Methods chrMatchTo :: env -> subst -> () -> () -> Maybe subst Source # chrUnify :: CHRMatchHow -> CHRMatchEnv (VarLookupKey subst) -> env -> subst -> () -> () -> Maybe subst Source # chrMatchToM :: env -> () -> () -> CHRMatcher subst () Source # chrUnifyM :: CHRMatchHow -> env -> () -> () -> CHRMatcher subst () Source # chrBuiltinSolveM :: env -> () -> CHRMatcher subst () Source #
CHRMatchable env x subst => CHRMatchable env (Maybe x) subst Source #
Instance details Defined in CHR.Types.Core Methods chrMatchTo :: env -> subst -> Maybe x -> Maybe x -> Maybe subst Source # chrUnify :: CHRMatchHow -> CHRMatchEnv (VarLookupKey subst) -> env -> subst -> Maybe x -> Maybe x -> Maybe subst Source # chrMatchToM :: env -> Maybe x -> Maybe x -> CHRMatcher subst () Source # chrUnifyM :: CHRMatchHow -> env -> Maybe x -> Maybe x -> CHRMatcher subst () Source # chrBuiltinSolveM :: env -> Maybe x -> CHRMatcher subst () Source #
CHRMatchable env x subst => CHRMatchable env [x] subst Source #
Instance details Defined in CHR.Types.Core Methods chrMatchTo :: env -> subst -> [x] -> [x] -> Maybe subst Source # chrUnify :: CHRMatchHow -> CHRMatchEnv (VarLookupKey subst) -> env -> subst -> [x] -> [x] -> Maybe subst Source # chrMatchToM :: env -> [x] -> [x] -> CHRMatcher subst () Source # chrUnifyM :: CHRMatchHow -> env -> [x] -> [x] -> CHRMatcher subst () Source # chrBuiltinSolveM :: env -> [x] -> CHRMatcher subst () Source #

type family CHRMatchableKey subst :: * Source #

The key of a substitution

Instances

Instances details

type CHRMatchableKey (StackedVarLookup subst) Source #
Instance details Defined in CHR.Types.Core type CHRMatchableKey (StackedVarLookup subst) = CHRMatchableKey subst

class CHREmptySubstitution subst Source #

Capability to yield an empty substitution.

Minimal complete definition

chrEmptySubst

class IsConstraint c Source #

The things a constraints needs to be capable of in order to participate in solving

type IsCHRBacktrackPrio env bp subst = (IsCHRPrio env bp subst, CHRMatchable env bp subst, PP (CHRPrioEvaluatableVal bp)) Source #

Alias API for backtrack priority requirements

type IsCHRPrio env p subst = (CHRPrioEvaluatable env p subst, Typeable p, PP p) Source #

Alias API for priority requirements

type IsCHRGuard env g subst = (CHRCheckable env g subst, VarExtractable g, VarUpdatable g subst, Typeable g, PP g) Source #

Alias API for guard requirements

type IsCHRConstraint env c subst = (CHRMatchable env c subst, VarExtractable c, VarUpdatable c subst, Typeable c, TreeTrieKeyable c, IsConstraint c, Ord c, Ord (TrTrKey c), PP c, PP (TrTrKey c)) Source #

Alias API for constraint requirements

data Prio Source #

Separate priority type, where minBound represents lowest prio, and compare sorts from high to low prio (i.e. high compare low == LT)

Instances

Instances details

Bounded Prio Source #
Instance details Defined in CHR.Types.Core Methods minBound :: Prio # maxBound :: Prio #
Enum Prio Source #
Instance details Defined in CHR.Types.Core Methods succ :: Prio -> Prio # pred :: Prio -> Prio # toEnum :: Int -> Prio # fromEnum :: Prio -> Int # enumFrom :: Prio -> [Prio] # enumFromThen :: Prio -> Prio -> [Prio] # enumFromTo :: Prio -> Prio -> [Prio] # enumFromThenTo :: Prio -> Prio -> Prio -> [Prio] #
Num Prio Source #
Instance details Defined in CHR.Types.Core Methods (+) :: Prio -> Prio -> Prio # (-) :: Prio -> Prio -> Prio # (*) :: Prio -> Prio -> Prio # negate :: Prio -> Prio # abs :: Prio -> Prio # signum :: Prio -> Prio # fromInteger :: Integer -> Prio #
Integral Prio Source #
Instance details Defined in CHR.Types.Core Methods quot :: Prio -> Prio -> Prio # rem :: Prio -> Prio -> Prio # div :: Prio -> Prio -> Prio # mod :: Prio -> Prio -> Prio # quotRem :: Prio -> Prio -> (Prio, Prio) # divMod :: Prio -> Prio -> (Prio, Prio) # toInteger :: Prio -> Integer #
Real Prio Source #
Instance details Defined in CHR.Types.Core Methods toRational :: Prio -> Rational #
Show Prio Source #
Instance details Defined in CHR.Types.Core Methods showsPrec :: Int -> Prio -> ShowS # show :: Prio -> String # showList :: [Prio] -> ShowS #
PP Prio Source #
Instance details Defined in CHR.Types.Core Methods pp :: Prio -> PP_Doc # ppList :: [Prio] -> PP_Doc #
Eq Prio Source #
Instance details Defined in CHR.Types.Core Methods (==) :: Prio -> Prio -> Bool # (/=) :: Prio -> Prio -> Bool #
Ord Prio Source #
Instance details Defined in CHR.Types.Core Methods compare :: Prio -> Prio -> Ordering # (<) :: Prio -> Prio -> Bool # (<=) :: Prio -> Prio -> Bool # (>) :: Prio -> Prio -> Bool # (>=) :: Prio -> Prio -> Bool # max :: Prio -> Prio -> Prio # min :: Prio -> Prio -> Prio #

class (Ord (CHRPrioEvaluatableVal x), Bounded (CHRPrioEvaluatableVal x)) => CHRPrioEvaluatable env x subst Source #

A PrioEvaluatable participates in the reduction process to indicate the rule priority, higher prio takes precedence

Minimal complete definition

chrPrioLift

type family CHRPrioEvaluatableVal p :: * Source #

The type of value a prio representation evaluates to, must be Ord instance

Instances

Instances details

type CHRPrioEvaluatableVal () Source #
Instance details Defined in CHR.Types.Core type CHRPrioEvaluatableVal () = Prio

class (CHREmptySubstitution subst, LookupApply subst subst) => CHRCheckable env x subst Source #

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

type CHRMatcher subst = StateT (CHRMatcherState subst (VarLookupKey subst)) (Either CHRMatcherFailure) Source #

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 ())

data CHRMatcherFailure Source #

Failure of CHRMatcher

type NmToVarMp = HashMap String IVar Source #

type IVar = Key Source #

emptyNmToVarMp :: NmToVarMp Source #

type family TrTrKey x #

Instances

Instances details

type TrTrKey (Maybe x)
Instance details Defined in CHR.Data.TreeTrie type TrTrKey (Maybe x) = TrTrKey x
type TrTrKey [x]
Instance details Defined in CHR.Data.TreeTrie type TrTrKey [x] = TrTrKey x
type TrTrKey (Work' k c) Source #
Instance details Defined in CHR.Types type TrTrKey (Work' k c) = TrTrKey c
type TrTrKey (Rule cnstr guard bprio prio) Source #
Instance details Defined in CHR.Types.Rule type TrTrKey (Rule cnstr guard bprio prio) = TrTrKey cnstr

type CHRKey v = Key (TrTrKey v) Source #

Convenience alias for key into CHR store

type WorkTime = Int Source #

All solver constraints are identified individually with a timestamp, also serving as its identification depending on the solver

initWorkTime :: WorkTime Source #

data Work' k c Source #

A chunk of work to do when solving, a constraint + sequence nr

Constructors

Work
Fields 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
Fields workCnstr :: !c the constraint to be reduced
Work_Solve
Fields workCnstr :: !c the constraint to be reduced
Work_Fail

Instances

Instances details

Show (Work' k c) Source #
Instance details Defined in CHR.Types Methods showsPrec :: Int -> Work' k c -> ShowS # show :: Work' k c -> String # showList :: [Work' k c] -> ShowS #
(PP k, PP c) => PP (Work' k c) Source #
Instance details Defined in CHR.Types Methods pp :: Work' k c -> PP_Doc # ppList :: [Work' k c] -> PP_Doc #
type TrTrKey (Work' k c) Source #
Instance details Defined in CHR.Types type TrTrKey (Work' k c) = TrTrKey c

type Work c = Work' (WorkKey c) c Source #

data SolveStep' c r s Source #

A trace step

Constructors

SolveStep
Fields stepChr :: r stepSubst :: s stepAlt :: Maybe [c] stepNewTodo :: [c] stepNewDone :: [c]
SolveStats
Fields stepStats :: Map String PP_Doc
SolveDbg
Fields stepPP :: PP_Doc

Instances

Instances details

Show (SolveStep' c r s) Source #
Instance details Defined in CHR.Types Methods showsPrec :: Int -> SolveStep' c r s -> ShowS # show :: SolveStep' c r s -> String # showList :: [SolveStep' c r s] -> ShowS #
(PP r, PP c) => PP (SolveStep' c r s) Source #
Instance details Defined in CHR.Types Methods pp :: SolveStep' c r s -> PP_Doc # ppList :: [SolveStep' c r s] -> PP_Doc #

type SolveTrace' c r s = [SolveStep' c r s] Source #

emptySolveTrace :: SolveTrace' c r s Source #

ppSolveTrace :: (PP r, PP c) => SolveTrace' c r s -> PP_Doc Source #