CHR.Types.Core

Documentation

class IsConstraint c where

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

Minimal complete definition

Nothing

Methods

cnstrRequiresSolve :: c -> Bool

Requires solving? Or is just a residue...

cnstrSolvesVia :: c -> ConstraintSolvesVia

data ConstraintSolvesVia

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

Instances

Enum ConstraintSolvesVia

Defined in CHR.Types.Core

Methods

succ :: ConstraintSolvesVia -> ConstraintSolvesVia

pred :: ConstraintSolvesVia -> ConstraintSolvesVia

toEnum :: Int -> ConstraintSolvesVia

fromEnum :: ConstraintSolvesVia -> Int

enumFrom :: ConstraintSolvesVia -> [ConstraintSolvesVia]

enumFromThen :: ConstraintSolvesVia -> ConstraintSolvesVia -> [ConstraintSolvesVia]

enumFromTo :: ConstraintSolvesVia -> ConstraintSolvesVia -> [ConstraintSolvesVia]

enumFromThenTo :: ConstraintSolvesVia -> ConstraintSolvesVia -> ConstraintSolvesVia -> [ConstraintSolvesVia]

Show ConstraintSolvesVia

Defined in CHR.Types.Core

Methods

showsPrec :: Int -> ConstraintSolvesVia -> ShowS

show :: ConstraintSolvesVia -> String

showList :: [ConstraintSolvesVia] -> ShowS

PP ConstraintSolvesVia

Defined in CHR.Types.Core

Methods

pp :: ConstraintSolvesVia -> PP_Doc

ppList :: [ConstraintSolvesVia] -> PP_Doc

Eq ConstraintSolvesVia

Defined in CHR.Types.Core

Methods

(==) :: ConstraintSolvesVia -> ConstraintSolvesVia -> Bool

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

Ord ConstraintSolvesVia

Defined in CHR.Types.Core

Methods

compare :: ConstraintSolvesVia -> ConstraintSolvesVia -> Ordering

(<) :: ConstraintSolvesVia -> ConstraintSolvesVia -> Bool

(<=) :: ConstraintSolvesVia -> ConstraintSolvesVia -> Bool

(>) :: ConstraintSolvesVia -> ConstraintSolvesVia -> Bool

(>=) :: ConstraintSolvesVia -> ConstraintSolvesVia -> Bool

max :: ConstraintSolvesVia -> ConstraintSolvesVia -> ConstraintSolvesVia

min :: ConstraintSolvesVia -> ConstraintSolvesVia -> ConstraintSolvesVia

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

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

Alias API for guard requirements

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

Alias API for priority requirements

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

Alias API for backtrack priority requirements

class CHREmptySubstitution subst where

Capability to yield an empty substitution.

Methods

chrEmptySubst :: subst

data CHRMatcherFailure

Failure of CHRMatcher

Constructors

CHRMatcherFailure

CHRMatcherFailure_NoBinding

absence of binding

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

chrmatcherRun' :: CHREmptySubstitution subst => (CHRMatcherFailure -> r) -> (subst -> CHRWaitForVarSet subst -> x -> r) -> CHRMatcher subst x -> CHRMatchEnv (VarLookupKey subst) -> StackedVarLookup subst -> r

Run a CHRMatcher

chrmatcherRun :: CHREmptySubstitution subst => CHRMatcher subst () -> CHRMatchEnv (VarLookupKey subst) -> subst -> Maybe (subst, CHRWaitForVarSet subst)

Run a CHRMatcher

chrmatcherstateEnv :: Functor f => (c -> f c) -> (a, b, c) -> f (a, b, c)

chrmatcherstateVarLookup :: Functor f => (a -> f a) -> (a, b, c) -> f (a, b, c)

chrMatchResolveCompareAndContinue

Arguments

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

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)

chrMatchBind :: forall subst k v. (LookupApply subst subst, Lookup subst k v, k ~ VarLookupKey subst, v ~ VarLookupVal subst) => k -> v -> CHRMatcher subst ()

chrMatchFail :: CHRMatcher subst a

Normal CHRMatcher failure

chrMatchFailNoBinding :: CHRMatcher subst a

CHRMatcher failure because a variable binding is missing

chrMatchSuccess :: CHRMatcher subst ()

chrMatchWait :: (Ord k, k ~ VarLookupKey subst) => k -> CHRMatcher subst ()

chrMatchSucces :: CHRMatcher subst ()

data CHRMatchEnv k

Context/environment required for matching itself

Constructors

CHRMatchEnv

Fields

• chrmatchenvMetaMayBind :: !(k -> Bool)

emptyCHRMatchEnv :: CHRMatchEnv x

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

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

One-directional (1st to 2nd x) unify

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

One-directional (1st to 2nd x) unify

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

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

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

Solve a constraint which is categorized as ConstraintSolvesVia_Solve

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

data CHRMatchHow

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

Eq CHRMatchHow

Defined in CHR.Types.Core

Methods

(==) :: CHRMatchHow -> CHRMatchHow -> Bool

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

Ord CHRMatchHow

Defined in CHR.Types.Core

Methods

compare :: CHRMatchHow -> CHRMatchHow -> Ordering

(<) :: CHRMatchHow -> CHRMatchHow -> Bool

(<=) :: CHRMatchHow -> CHRMatchHow -> Bool

(>) :: CHRMatchHow -> CHRMatchHow -> Bool

(>=) :: CHRMatchHow -> CHRMatchHow -> Bool

max :: CHRMatchHow -> CHRMatchHow -> CHRMatchHow

min :: CHRMatchHow -> CHRMatchHow -> CHRMatchHow

chrMatchAndWaitToM :: CHRMatchable env x subst => Bool -> env -> x -> x -> CHRMatcher subst ()

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)

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

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

Methods

chrCheck :: env -> subst -> x -> Maybe subst

chrCheckM :: env -> x -> CHRMatcher subst ()

newtype Prio

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

Constructors

Prio

Fields

• unPrio :: Word32

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 where

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

Minimal complete definition

chrPrioLift

Methods

chrPrioEval :: env -> subst -> x -> CHRPrioEvaluatableVal x

Reduce to a prio representation

chrPrioCompare :: env -> (subst, x) -> (subst, x) -> Ordering

Compare priorities

chrPrioLift :: proxy env -> proxy subst -> CHRPrioEvaluatableVal x -> x

Lift prio val into prio

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

data CHRTrOpt

Constructors

CHRTrOpt_Lookup

trie query

CHRTrOpt_Stats

various stats

Instances

Show CHRTrOpt

Defined in CHR.Types.Core

Methods

showsPrec :: Int -> CHRTrOpt -> ShowS

show :: CHRTrOpt -> String

showList :: [CHRTrOpt] -> ShowS

Eq CHRTrOpt

Defined in CHR.Types.Core

Methods

(==) :: CHRTrOpt -> CHRTrOpt -> Bool

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

Ord CHRTrOpt

Defined in CHR.Types.Core

Methods

compare :: CHRTrOpt -> CHRTrOpt -> Ordering

(<) :: CHRTrOpt -> CHRTrOpt -> Bool

(<=) :: CHRTrOpt -> CHRTrOpt -> Bool

(>) :: CHRTrOpt -> CHRTrOpt -> Bool

(>=) :: CHRTrOpt -> CHRTrOpt -> Bool

max :: CHRTrOpt -> CHRTrOpt -> CHRTrOpt

min :: CHRTrOpt -> CHRTrOpt -> CHRTrOpt

type IVar = Key

type VarToNmMp = IntMap String

emptyVarToNmMp :: VarToNmMp

type NmToVarMp = HashMap String IVar

emptyNmToVarMp :: NmToVarMp

Orphan instances

Ord (ExtrValVarKey ()) => VarExtractable ()

Methods

varFree :: () -> [ExtrValVarKey ()]

varFreeSet :: () -> Set (ExtrValVarKey ())