Twee.Join

Tactics for joining critical pairs.

Documentation

data Config

Constructors

Config

Fields

• cfg_ground_join :: !Bool
• cfg_use_connectedness :: !Bool
• cfg_set_join :: !Bool

defaultConfig :: Config

joinCriticalPair :: (Function f, Has a (Rule f), Has a (Lemma f)) => Config -> Index f (Equation f) -> RuleIndex f a -> Maybe (Model f) -> CriticalPair f -> Either (CriticalPair f, Model f) (Maybe (CriticalPair f), [CriticalPair f])

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

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

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

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

joinWith :: (Has a (Rule f), Has a (Lemma f)) => Index f (Equation f) -> RuleIndex f a -> (Term f -> Term f -> Resulting f) -> CriticalPair f -> Maybe (CriticalPair f)

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

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

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

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

valid :: Function f => Model f -> Reduction f -> Bool

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