| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
UHC.Util.CHR.Base
Description
Derived from work by Gerrit vd Geest, but with searching structures for predicates to avoid explosion of search space during resolution.
- class IsConstraint c where
- cnstrRequiresSolve :: c -> Bool
- cnstrSolvesVia :: c -> ConstraintSolvesVia
- data ConstraintSolvesVia
- class (CHRMatchable env c subst, VarExtractable c, VarUpdatable c subst, Typeable c, Serialize c, TTKeyable c, IsConstraint c, Ord c, Ord (TTKey c), PP c, PP (TTKey c)) => IsCHRConstraint env c subst
- class (CHRCheckable env g subst, VarExtractable g, VarUpdatable g subst, Typeable g, Serialize g, PP g) => IsCHRGuard env g subst
- class (CHRPrioEvaluatable env p subst, Typeable p, Serialize p, PP p) => IsCHRPrio env p subst
- class (IsCHRPrio env bp subst, CHRMatchable env bp subst, PP (CHRPrioEvaluatableVal bp)) => IsCHRBacktrackPrio env bp subst
- class CHREmptySubstitution subst where
- chrEmptySubst :: subst
- data CHRMatcherFailure
- type CHRMatcher subst = StateT (CHRMatcherState subst (VarLookupKey subst)) (Either CHRMatcherFailure)
- chrmatcherRun' :: CHREmptySubstitution subst => (CHRMatcherFailure -> r) -> (subst -> CHRWaitForVarSet subst -> x -> r) -> CHRMatcher subst x -> CHRMatchEnv (VarLookupKey subst) -> StackedVarLookup subst -> r
- chrmatcherRun :: CHREmptySubstitution subst => CHRMatcher subst () -> CHRMatchEnv (VarLookupKey subst) -> subst -> Maybe (subst, CHRWaitForVarSet subst)
- chrmatcherstateEnv :: ArrowApply arr => Lens arr ((a, b, c) -> (a, b, o)) (c -> o)
- chrmatcherstateVarLookup :: ArrowApply arr => Lens arr ((a, b, c) -> (o, b, c)) (a -> o)
- chrMatchResolveCompareAndContinue :: forall s. (VarLookup s, VarLookupCmb 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 ()
- chrMatchSubst :: CHRMatcher subst (StackedVarLookup subst)
- chrMatchBind :: forall subst k v. (VarLookupCmb subst subst, VarLookup subst, k ~ VarLookupKey subst, v ~ VarLookupVal subst) => k -> v -> CHRMatcher subst ()
- chrMatchFail :: CHRMatcher subst a
- chrMatchFailNoBinding :: CHRMatcher subst a
- chrMatchSuccess :: CHRMatcher subst ()
- chrMatchWait :: (Ord k, k ~ VarLookupKey subst) => k -> CHRMatcher subst ()
- chrMatchSucces :: CHRMatcher subst ()
- data CHRMatchEnv k = CHRMatchEnv {
- chrmatchenvMetaMayBind :: !(k -> Bool)
- emptyCHRMatchEnv :: CHRMatchEnv x
- class (CHREmptySubstitution subst, VarLookupCmb subst subst, VarExtractable x, VarLookupKey subst ~ ExtrValVarKey x) => CHRMatchable env x subst where
- 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 :: *
- data CHRMatchHow
- chrMatchAndWaitToM :: CHRMatchable env x subst => Bool -> env -> x -> x -> CHRMatcher subst ()
- type CHRWaitForVarSet s = Set (VarLookupKey s)
- class (CHREmptySubstitution subst, VarLookupCmb subst subst) => CHRCheckable env x subst where
- chrCheck :: env -> subst -> x -> Maybe subst
- chrCheckM :: env -> x -> CHRMatcher subst ()
- newtype Prio = Prio {}
- class (Ord (CHRPrioEvaluatableVal x), Bounded (CHRPrioEvaluatableVal x)) => CHRPrioEvaluatable env x subst | x -> env subst where
- chrPrioEval :: env -> subst -> x -> CHRPrioEvaluatableVal x
- chrPrioCompare :: env -> (subst, x) -> (subst, x) -> Ordering
- chrPrioLift :: CHRPrioEvaluatableVal x -> x
- type family CHRPrioEvaluatableVal p :: *
- data CHRTrOpt
Documentation
class IsConstraint c where Source
The things a constraints needs to be capable of in order to participate in solving
Minimal complete definition
Nothing
Methods
cnstrRequiresSolve :: c -> Bool Source
Requires solving? Or is just a residue...
cnstrSolvesVia :: c -> ConstraintSolvesVia Source
data ConstraintSolvesVia Source
Different ways of solving
Constructors
| 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 |
class (CHRMatchable env c subst, VarExtractable c, VarUpdatable c subst, Typeable c, Serialize c, TTKeyable c, IsConstraint c, Ord c, Ord (TTKey c), PP c, PP (TTKey c)) => IsCHRConstraint env c subst Source
(Class alias) API for constraint requirements
class (CHRCheckable env g subst, VarExtractable g, VarUpdatable g subst, Typeable g, Serialize g, PP g) => IsCHRGuard env g subst Source
(Class alias) API for guard requirements
class (CHRPrioEvaluatable env p subst, Typeable p, Serialize p, PP p) => IsCHRPrio env p subst Source
(Class alias) API for priority requirements
class (IsCHRPrio env bp subst, CHRMatchable env bp subst, PP (CHRPrioEvaluatableVal bp)) => IsCHRBacktrackPrio env bp subst Source
(Class alias) API for backtrack priority requirements
class CHREmptySubstitution subst where Source
Capability to yield an empty substitution.
Methods
chrEmptySubst :: subst Source
data CHRMatcherFailure Source
Failure of CHRMatcher
Constructors
| CHRMatcherFailure | |
| CHRMatcherFailure_NoBinding | absence of binding |
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 ())
chrmatcherRun' :: CHREmptySubstitution subst => (CHRMatcherFailure -> r) -> (subst -> CHRWaitForVarSet subst -> x -> r) -> CHRMatcher subst x -> CHRMatchEnv (VarLookupKey subst) -> StackedVarLookup subst -> r Source
Run a CHRMatcher
chrmatcherRun :: CHREmptySubstitution subst => CHRMatcher subst () -> CHRMatchEnv (VarLookupKey subst) -> subst -> Maybe (subst, CHRWaitForVarSet subst) Source
Run a CHRMatcher
chrmatcherstateEnv :: ArrowApply arr => Lens arr ((a, b, c) -> (a, b, o)) (c -> o) Source
chrmatcherstateVarLookup :: ArrowApply arr => Lens arr ((a, b, c) -> (o, b, c)) (a -> o) Source
chrMatchResolveCompareAndContinue Source
Arguments
| :: (VarLookup s, VarLookupCmb 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 () |
Do the resolution part of a comparison, continuing with a function which can assume variable resolution has been done for the terms being compared
chrMatchSubst :: CHRMatcher subst (StackedVarLookup subst) Source
chrMatchBind :: forall subst k v. (VarLookupCmb subst subst, VarLookup subst, k ~ VarLookupKey subst, v ~ VarLookupVal subst) => k -> v -> CHRMatcher subst () Source
chrMatchFail :: CHRMatcher subst a Source
Normal CHRMatcher failure
chrMatchFailNoBinding :: CHRMatcher subst a Source
CHRMatcher failure because a variable binding is missing
chrMatchSuccess :: CHRMatcher subst () Source
chrMatchWait :: (Ord k, k ~ VarLookupKey subst) => k -> CHRMatcher subst () Source
chrMatchSucces :: CHRMatcher subst () Source
data CHRMatchEnv k Source
Context/environment required for matching itself
Constructors
| CHRMatchEnv | |
Fields
| |
class (CHREmptySubstitution subst, VarLookupCmb subst subst, VarExtractable x, VarLookupKey subst ~ ExtrValVarKey x) => CHRMatchable env x subst where 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.
Minimal complete definition
Nothing
Methods
chrMatchTo :: env -> subst -> x -> x -> Maybe subst Source
One-directional (1st to 2nd x) unify
chrUnify :: CHRMatchHow -> CHRMatchEnv (VarLookupKey subst) -> env -> subst -> x -> x -> Maybe subst Source
One-directional (1st to 2nd x) unify
chrMatchToM :: env -> x -> x -> CHRMatcher subst () Source
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 () Source
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
chrBuiltinSolveM :: env -> x -> CHRMatcher subst () Source
Solve a constraint which is categorized as ConstraintSolvesVia_Solve
Instances
| (Ord (ExtrValVarKey ()), CHREmptySubstitution subst, VarLookupCmb subst subst, (~) * (VarLookupKey subst) (ExtrValVarKey ())) => CHRMatchable env () subst Source | |
| CHRMatchable env x subst => CHRMatchable env [x] subst Source | |
| CHRMatchable env x subst => CHRMatchable env (Maybe x) subst Source |
type family CHRMatchableKey subst :: * Source
The key of a substitution
Instances
| type CHRMatchableKey (StackedVarLookup subst) = CHRMatchableKey subst Source |
data CHRMatchHow Source
How to match, increasingly more binding is allowed
Constructors
| 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 |
Instances
chrMatchAndWaitToM :: CHRMatchable env x subst => Bool -> env -> x -> x -> CHRMatcher subst () Source
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
type CHRWaitForVarSet s = Set (VarLookupKey s) Source
class (CHREmptySubstitution subst, VarLookupCmb subst subst) => CHRCheckable env x subst where 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).
Minimal complete definition
Nothing
Separate priority type, where minBound represents lowest prio, and compare sorts from high to low prio (i.e. high compare low == LT)
class (Ord (CHRPrioEvaluatableVal x), Bounded (CHRPrioEvaluatableVal x)) => CHRPrioEvaluatable env x subst | x -> env subst where Source
A PrioEvaluatable participates in the reduction process to indicate the rule priority, higher prio takes precedence
Minimal complete definition
Methods
chrPrioEval :: env -> subst -> x -> CHRPrioEvaluatableVal x Source
Reduce to a prio representation
chrPrioCompare :: env -> (subst, x) -> (subst, x) -> Ordering Source
Compare priorities
chrPrioLift :: CHRPrioEvaluatableVal x -> x Source
Lift prio val into prio
type family CHRPrioEvaluatableVal p :: * Source
The type of value a prio representation evaluates to, must be Ord instance
Instances
| type CHRPrioEvaluatableVal () = Prio Source |