CHR.Types

CHR TreeTrie based solver shared internals, for all solvers

Documentation

class (CHREmptySubstitution subst, LookupApply subst subst, VarExtractable x, VarLookupKey subst ~ ExtrValVarKey x) => CHRMatchable env x 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.

Instances

(Ord (ExtrValVarKey ()), CHREmptySubstitution subst, LookupApply subst subst, VarLookupKey subst ~ ExtrValVarKey ()) => CHRMatchable env () subst

Defined in CHR.Types.Core

Methods

chrMatchTo :: env -> subst -> () -> () -> Maybe subst

chrUnify :: CHRMatchHow -> CHRMatchEnv (VarLookupKey subst) -> env -> subst -> () -> () -> Maybe subst

chrMatchToM :: env -> () -> () -> CHRMatcher subst ()

chrUnifyM :: CHRMatchHow -> env -> () -> () -> CHRMatcher subst ()

chrBuiltinSolveM :: env -> () -> CHRMatcher subst ()

CHRMatchable env x subst => CHRMatchable env (Maybe x) subst

Defined in CHR.Types.Core

Methods

chrMatchTo :: env -> subst -> Maybe x -> Maybe x -> Maybe subst

chrUnify :: CHRMatchHow -> CHRMatchEnv (VarLookupKey subst) -> env -> subst -> Maybe x -> Maybe x -> Maybe subst

chrMatchToM :: env -> Maybe x -> Maybe x -> CHRMatcher subst ()

chrUnifyM :: CHRMatchHow -> env -> Maybe x -> Maybe x -> CHRMatcher subst ()

chrBuiltinSolveM :: env -> Maybe x -> CHRMatcher subst ()

CHRMatchable env x subst => CHRMatchable env [x] subst

Defined in CHR.Types.Core

Methods

chrMatchTo :: env -> subst -> [x] -> [x] -> Maybe subst

chrUnify :: CHRMatchHow -> CHRMatchEnv (VarLookupKey subst) -> env -> subst -> [x] -> [x] -> Maybe subst

chrMatchToM :: env -> [x] -> [x] -> CHRMatcher subst ()

chrUnifyM :: CHRMatchHow -> env -> [x] -> [x] -> CHRMatcher subst ()

chrBuiltinSolveM :: env -> [x] -> CHRMatcher subst ()

type family CHRMatchableKey subst :: *

The key of a substitution

Instances

type CHRMatchableKey (StackedVarLookup subst)

Defined in CHR.Types.Core

type CHRMatchableKey (StackedVarLookup subst) = CHRMatchableKey subst

class CHREmptySubstitution subst

Capability to yield an empty substitution.

Minimal complete definition

chrEmptySubst

class IsConstraint c

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

Alias API for backtrack priority requirements

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

Alias API for priority requirements

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

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

Alias API for constraint requirements

data Prio

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

Instances

Bounded Prio

Defined in CHR.Types.Core

Methods

minBound :: Prio

maxBound :: Prio

Enum Prio

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

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

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

Defined in CHR.Types.Core

Methods

toRational :: Prio -> Rational

Show Prio

Defined in CHR.Types.Core

Methods

showsPrec :: Int -> Prio -> ShowS

show :: Prio -> String

showList :: [Prio] -> ShowS

PP Prio

Defined in CHR.Types.Core

Methods

pp :: Prio -> PP_Doc

ppList :: [Prio] -> PP_Doc

Eq Prio

Defined in CHR.Types.Core

Methods

(==) :: Prio -> Prio -> Bool

(/=) :: Prio -> Prio -> Bool

Ord Prio

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

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

Minimal complete definition

chrPrioLift

type family CHRPrioEvaluatableVal p :: *

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

Instances

type CHRPrioEvaluatableVal ()

Defined in CHR.Types.Core

type CHRPrioEvaluatableVal () = Prio

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

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)

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

Failure of CHRMatcher

type NmToVarMp = HashMap String IVar

type IVar = Key

emptyNmToVarMp :: NmToVarMp

type family TrTrKey x

Instances

type TrTrKey (Maybe x)

Defined in CHR.Data.TreeTrie

type TrTrKey (Maybe x) = TrTrKey x

type TrTrKey [x]

Defined in CHR.Data.TreeTrie

type TrTrKey [x] = TrTrKey x

type TrTrKey (Work' k c)

Defined in CHR.Types

type TrTrKey (Work' k c) = TrTrKey c

type TrTrKey (Rule cnstr guard bprio prio)

Defined in CHR.Types.Rule

type TrTrKey (Rule cnstr guard bprio prio) = TrTrKey cnstr

type CHRKey v = Key (TrTrKey v)

Convenience alias for key into CHR store

type WorkTime = Int

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

initWorkTime :: WorkTime

data Work' k c

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

Show (Work' k c)

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)

Defined in CHR.Types

Methods

pp :: Work' k c -> PP_Doc

ppList :: [Work' k c] -> PP_Doc

type TrTrKey (Work' k c)

Defined in CHR.Types

type TrTrKey (Work' k c) = TrTrKey c

type Work c = Work' (WorkKey c) c

data SolveStep' c r s

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

Show (SolveStep' c r s)

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)

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]

emptySolveTrace :: SolveTrace' c r s

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