Safe Haskell | None |
---|---|
Language | Haskell2010 |
Documentation
Twee | |
|
Eq a => Eq (Modelled a) Source # | |
Ord a => Ord (Modelled a) Source # | |
(Show a, Show (ConstantOf a)) => Show (Modelled a) Source # | |
(PrettyTerm (ConstantOf a), Pretty a) => Pretty (Modelled a) Source # | |
Symbolic a => Symbolic (Modelled a) Source # | |
Rated a => Rated (Modelled a) Source # | |
type ConstantOf (Modelled a) Source # | |
reduceCP :: Function f => Twee f -> JoinStage -> (Term f -> Term f) -> Critical (Equation f) -> Either JoinReason (Critical (Equation f)) Source #
data JoinReason Source #
normaliseCPQuickly :: Function f => Twee f -> Critical (Equation f) -> Either JoinReason (Critical (Equation f)) Source #
normaliseCPReducing :: Function f => Twee f -> Critical (Equation f) -> Either JoinReason (Critical (Equation f)) Source #
normaliseCP :: Function f => Twee f -> Critical (Equation f) -> Either JoinReason (Critical (Equation f)) Source #
consider :: Function f => Int -> Label -> Label -> Critical (Equation f) -> State (Twee f) Bool Source #
groundJoin :: Function f => Twee f -> [Branch f] -> Critical (Equation f) -> Either (Model f) [Critical (Equation f)] Source #
data Simplification f Source #
Show f => Show (Simplification f) Source # | |
(Numbered f, PrettyTerm f) => Pretty (Simplification f) Source # | |
reduceWith :: Function f => Twee f -> Label -> Rule f -> Modelled (Critical (Rule f)) -> Maybe (Simplification f) Source #
simplifyRule :: Function f => Label -> Model f -> Modelled (Critical (Rule f)) -> State (Twee f) () Source #
noCritInfo :: Function f => CritInfo f Source #
data CancellationRule f Source #
CancellationRule | |
|
Show (CancellationRule f) Source # | |
(Numbered f, PrettyTerm f) => Pretty (CancellationRule f) Source # | |
Symbolic (CancellationRule f) Source # | |
type ConstantOf (CancellationRule f) Source # | |
toCancellationRule :: Function f => Twee f -> Rule f -> Maybe (CancellationRule f) Source #
Critical | |
|
Eq a => Eq (Critical a) Source # | |
Ord a => Ord (Critical a) Source # | |
(Show a, Show (ConstantOf a)) => Show (Critical a) Source # | |
(PrettyTerm (ConstantOf a), Pretty a) => Pretty (Critical a) Source # | |
Symbolic a => Symbolic (Critical a) Source # | |
Rated a => Rated (Critical a) Source # | |
type ConstantOf (Critical a) Source # | |
passiveCount :: Passive f -> Int Source #
criticalPairs :: Function f => Twee f -> Label -> Label -> Rule f -> [Labelled (Critical (Equation f))] Source #
criticalPairs1 :: Function f => Twee f -> [Int] -> Rule f -> [Labelled (Rule f)] -> [Labelled (Critical (Equation f))] Source #
queueCP :: Function f => (Passive f -> State (Twee f) ()) -> (Equation f -> Bool) -> Label -> Label -> Critical (Equation f) -> State (Twee f) () Source #
queueCPs :: (Function f, Ord a) => (Passive f -> State (Twee f) ()) -> Label -> Label -> (Label -> a) -> Labelled (Rule f) -> State (Twee f) () Source #
queueCPsSplit :: Function f => (Passive f -> State (Twee f) ()) -> Label -> Label -> Labelled (Rule f) -> State (Twee f) () Source #
toCP :: Function f => Twee f -> Label -> Label -> (Equation f -> Bool) -> Critical (Equation f) -> Maybe (CP f) Source #
bestCancellation :: Function f => Twee f -> (Equation f -> Bool) -> Equation f -> (Int, Equation f) Source #
cancellations :: Function f => Twee f -> (Equation f -> Bool) -> Equation f -> [Equation f] Source #
NewRule (Rule f) | |
ExtraRule (Rule f) | |
NewCP (Passive f) | |
Reduce (Simplification f) (Rule f) | |
Consider (Critical (Equation f)) | |
Joined (Critical (Equation f)) JoinReason | |
Delay (Critical (Equation f)) | |
Cancel (Critical (Equation f)) (Equation f) | |
Discharge (Critical (Equation f)) (Model f) | |
NormaliseCPs (Twee f) |