twee-lib-2.4.2: An equational theorem prover

Twee.Join

Description

Tactics for joining critical pairs.

# Documentation

data Config Source #

Constructors

 Config Fields

step1 :: (Function f, Has a (Rule f)) => Config -> (Index f (Equation f), Index f (Rule f)) -> RuleIndex f a -> CriticalPair f -> Maybe (CriticalPair f) Source #

step2 :: (Function f, Has a (Rule f)) => Config -> (Index f (Equation f), Index f (Rule f)) -> RuleIndex f a -> CriticalPair f -> Maybe (CriticalPair f) Source #

step3 :: (Function f, Has a (Rule f)) => Config -> (Index f (Equation f), Index f (Rule f)) -> RuleIndex f a -> CriticalPair f -> Maybe (CriticalPair f) Source #

allSteps :: (Function f, Has a (Rule f)) => Config -> (Index f (Equation f), Index f (Rule f)) -> RuleIndex f a -> CriticalPair f -> Maybe (CriticalPair f) Source #

joinWith :: (Function f, Has a (Rule f)) => Config -> (Index f (Equation f), Index f (Rule f)) -> RuleIndex f a -> (Term f -> Term f -> Reduction f) -> CriticalPair f -> Maybe (CriticalPair f) Source #

subsumed :: (Has a (Rule f), Function f) => (Index f (Equation f), Index f (Rule f)) -> RuleIndex f a -> Equation f -> Bool Source #

subsumed1 :: Has a (Rule f) => Index f (Equation f) -> RuleIndex f a -> Equation f -> Bool Source #

groundJoin :: (Function f, Has a (Rule f)) => Config -> (Index f (Equation f), Index f (Rule f)) -> RuleIndex f a -> [Branch f] -> CriticalPair f -> Either (Model f) (Maybe (CriticalPair f), [CriticalPair f]) Source #

groundJoinFrom :: (Function f, Has a (Rule f)) => Config -> (Index f (Equation f), Index f (Rule f)) -> RuleIndex f a -> Model f -> [Branch f] -> CriticalPair f -> Either (Model f) (Maybe (CriticalPair f), [CriticalPair f]) Source #

groundJoinFromMaybe :: (Function f, Has a (Rule f)) => Config -> (Index f (Equation f), Index f (Rule f)) -> RuleIndex f a -> Maybe (Model f) -> [Branch f] -> CriticalPair f -> Either (Model f) (Maybe (CriticalPair f), [CriticalPair f]) Source #

optimise :: (a -> [a]) -> (a -> Bool) -> a -> a Source #