Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
Tactics for joining critical pairs.
Documentation
joinCriticalPair :: (Function f, Has a (Rule f)) => Config -> (Index f (Equation f), Index f (Rule f)) -> RuleIndex f a -> Maybe (Model f) -> CriticalPair f -> Either (CriticalPair f, Model f) (Maybe (CriticalPair f), [CriticalPair f]) Source #
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 #
checkOrder :: Function f => 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 #
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 #