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 #