Portability | unportable |
---|---|
Stability | unstable |
Maintainer | Martin Avanzini <martin.avanzini@uibk.ac.at> |
Safe Haskell | Safe-Infered |
Rule selectors give a general method to select rules from a problem.
- data RuleSelector a = RuleSelector {}
- type RuleSetSelector = RuleSelector Ruleset
- selRules :: RuleSetSelector
- selDPs :: RuleSetSelector
- selStricts :: RuleSetSelector
- selWeaks :: RuleSetSelector
- selFromWDG :: (DG -> Ruleset) -> RuleSetSelector
- selFromCWDG :: (CDG -> Ruleset) -> RuleSetSelector
- selInverse :: RuleSetSelector -> RuleSetSelector
- selCombine :: (String -> String -> String) -> (Trs -> Trs -> Trs) -> RuleSetSelector -> RuleSetSelector -> RuleSetSelector
- selUnion :: RuleSetSelector -> RuleSetSelector -> RuleSetSelector
- selInter :: RuleSetSelector -> RuleSetSelector -> RuleSetSelector
- selFirstCongruence :: RuleSetSelector
- selFirstStrictCongruence :: RuleSetSelector
- selLeafCWDG :: RuleSetSelector
- selLeafWDG :: RuleSetSelector
- selIndependentSG :: RuleSetSelector
- selCycleIndependentSG :: RuleSetSelector
- selCloseForward :: RuleSetSelector -> RuleSetSelector
- selCloseBackward :: RuleSetSelector -> RuleSetSelector
- data SelectorExpression
- = SelectDP Rule
- | SelectTrs Rule
- | BigAnd [SelectorExpression]
- | BigOr [SelectorExpression]
- type ExpressionSelector = RuleSelector SelectorExpression
- selAnyOf :: RuleSetSelector -> ExpressionSelector
- selAllOf :: RuleSetSelector -> ExpressionSelector
- selAnd :: [ExpressionSelector] -> ExpressionSelector
- selOr :: [ExpressionSelector] -> ExpressionSelector
- rules :: SelectorExpression -> (Trs, Trs)
- selFirstAlternative :: ExpressionSelector -> ExpressionSelector
- onSelectedRequire :: Boolean a => SelectorExpression -> (Bool -> Rule -> a) -> a
Documentation
data RuleSelector a
This datatype is used to select a subset of rules recorded in a problem.
RuleSelector | |
|
RuleSet Selectors
type RuleSetSelector = RuleSelector Ruleset
Constructors
Select rewrite rules, i.e., non dependency pair rules.
Select dependency pairs.
Select strict rules.
Select strict rules.
selFromWDG :: (DG -> Ruleset) -> RuleSetSelector
Select from the dependency graph, using the given function. The first parameter should specify a short name for the rule-selector.
selFromCWDG :: (CDG -> Ruleset) -> RuleSetSelector
Select from the congruence dependency graph, using the given function. The first parameter should specify a short name for the rule-selector.
Combinators
selInverse :: RuleSetSelector -> RuleSetSelector
Inverses the selection.
selCombine :: (String -> String -> String) -> (Trs -> Trs -> Trs) -> RuleSetSelector -> RuleSetSelector -> RuleSetSelector
Combine two rule-selectors component-wise.
selUnion :: RuleSetSelector -> RuleSetSelector -> RuleSetSelector
Select union of selections of given rule-selectors.
selInter :: RuleSetSelector -> RuleSetSelector -> RuleSetSelector
Select intersection of selections of given rule-selectors.
Instances Based on DG Analysis
selFirstCongruence :: RuleSetSelector
Selects all rules from root-nodes in the congruence graph.
selFirstStrictCongruence :: RuleSetSelector
Selects all rules from nodes n
of the CWDG that satisfy
(i) the node n
references at least one strict rule, and (ii)
there is no node between a root of the CWDG and n
containing a strict rule.
Selector Expressions
data SelectorExpression
Defines a notion of selected rules, specified as monotone Boolean Formula.
SelectorExpressions
are used for instance in solvePartial
to determine
which rules should be oriented by a processor.
Boolean Selectors
selAnd :: [ExpressionSelector] -> ExpressionSelector
Conjunction
selOr :: [ExpressionSelector] -> ExpressionSelector
Disjunction
Misc
rules :: SelectorExpression -> (Trs, Trs)
returns the pair of dps and rules mentioned in a SelectorExpression
selFirstAlternative :: ExpressionSelector -> ExpressionSelector
Selects the first alternative from the given rule selector.
onSelectedRequire :: Boolean a => SelectorExpression -> (Bool -> Rule -> a) -> a