Safe Haskell	Safe-Inferred
Language	Haskell2010

Twee.Rule

Contents

Description

Term rewriting.

Synopsis

data Rule f = Rule {
- orientation :: Orientation f
- rule_proof :: !(Proof f)
- lhs :: !(Term f)
- rhs :: !(Term f)
}
type RuleOf a = Rule (ConstantOf a)
ruleDerivation :: Rule f -> Derivation f
data Orientation f
- = Oriented
- | WeaklyOriented !(Fun f) [Term f]
- | Permutative [(Term f, Term f)]
- | Unoriented
oriented :: Orientation f -> Bool
unorient :: Rule f -> Equation f
orient :: Function f => Equation f -> Proof f -> Rule f
backwards :: Rule f -> Rule f
simplify :: (Function f, Has a (Rule f)) => Index f a -> Term f -> Term f
simplifyOutermost :: (Function f, Has a (Rule f)) => Index f a -> Term f -> Term f
simplifyInnermost :: (Function f, Has a (Rule f)) => Index f a -> Term f -> Term f
simpleRewrite :: (Function f, Has a (Rule f)) => Index f a -> Term f -> Maybe (Rule f, Subst f)
type Strategy f = Term f -> [Reduction f]
type Reduction f = [(Rule f, Subst f)]
trans :: Reduction f -> Reduction f -> Reduction f
result :: Term f -> Reduction f -> Term f
reductionProof :: Function f => Term f -> Reduction f -> Derivation f
ruleResult :: Term f -> (Rule f, Subst f) -> Term f
ruleProof :: Function f => Term f -> (Rule f, Subst f) -> Derivation f
normaliseWith :: Function f => (Term f -> Bool) -> Strategy f -> Term f -> Reduction f
normalForms :: Function f => Strategy f -> Map (Term f) (Reduction f) -> Map (Term f) (Term f, Reduction f)
successors :: Function f => Strategy f -> Map (Term f) (Reduction f) -> Map (Term f) (Term f, Reduction f)
successorsAndNormalForms :: Function f => Strategy f -> Map (Term f) (Reduction f) -> (Map (Term f) (Term f, Reduction f), Map (Term f) (Term f, Reduction f))
anywhere :: Strategy f -> Strategy f
anywhereOutermost :: Strategy f -> Strategy f
anywhereInnermost :: Strategy f -> Strategy f
rewrite :: (Function f, Has a (Rule f)) => (Rule f -> Subst f -> Bool) -> Index f a -> Strategy f
tryRule :: (Function f, Has a (Rule f)) => (Rule f -> Subst f -> Bool) -> a -> Strategy f
reducesWith :: Function f => (Term f -> Term f -> Bool) -> Rule f -> Subst f -> Bool
reduces :: Function f => Rule f -> Subst f -> Bool
reducesOriented :: Function f => Rule f -> Subst f -> Bool
reducesInModel :: Function f => Model f -> Rule f -> Subst f -> Bool
reducesSkolem :: Function f => Rule f -> Subst f -> Bool
type Reduction1 f = [(Rule f, Subst f, [Int])]
trans1 :: Reduction1 f -> Reduction1 f -> Reduction1 f
result1 :: HasCallStack => Term f -> Reduction1 f -> Term f
reductionProof1 :: Function f => Term f -> Reduction1 f -> Derivation f
ruleResult1 :: HasCallStack => Term f -> (Rule f, Subst f, [Int]) -> Term f
ruleProof1 :: Function f => Term f -> (Rule f, Subst f, [Int]) -> Derivation f
type Strategy1 f = Term f -> [(Rule f, Subst f, [Int])]
anywhere1 :: Strategy1 f -> Strategy1 f
basic :: Strategy f -> Strategy1 f
normaliseWith1 :: Function f => (Term f -> Bool) -> Strategy1 f -> Term f -> Reduction1 f
normaliseWith1Random :: Function f => (Term f -> Bool) -> Strategy1 f -> Term f -> Gen (Reduction1 f)
rematchReduction1 :: HasCallStack => Term f -> Reduction1 f -> Reduction1 f
data UNF f
- = UniqueNormalForm (Term f) (Reduction1 f)
- | HasCriticalPair (Rule f) (Rule f, Int) (ConfluenceFailure f)
data ConfluenceFailure f = ConfluenceFailure {
- cf_term :: Term f
- cf_left :: Reduction1 f
- cf_right :: Reduction1 f
- cf_orig_term :: Term f
- cf_orig_left :: Reduction1 f
}
cf_left_term :: ConfluenceFailure f -> Term f
cf_right_term :: ConfluenceFailure f -> Term f
hasUNFRetry :: Function f => Strategy1 f -> ConfluenceFailure f -> UNF f
hasUNFRandom :: Function f => Strategy1 f -> Term f -> Gen (UNF f)
hasUNFSimple :: Function f => Strategy1 f -> Term f -> Reduction1 f -> UNF f
hasUNF :: (HasCallStack, Function f) => Strategy1 f -> Term f -> Reduction1 f -> UNF f
decomposePath :: Term f -> [Int] -> (Var, [Int])
varPos :: Var -> Term f -> [Int]
track :: Rule f -> [Int] -> [Int] -> ([[Int]], [[Int]])

Rewrite rules.

data Rule f Source #

A rewrite rule.

Constructors

Rule
Fields orientation :: Orientation f Information about whether and how the rule is oriented. rule_proof :: !(Proof f) A proof that the rule holds. lhs :: !(Term f) The left-hand side of the rule. rhs :: !(Term f) The right-hand side of the rule.

Instances

Instances details

(Labelled f, Show f) => Show (Rule f) Source #
Instance details Defined in Twee.Rule Methods showsPrec :: Int -> Rule f -> ShowS # show :: Rule f -> String # showList :: [Rule f] -> ShowS #
Eq (Rule f) Source #
Instance details Defined in Twee.Rule Methods (==) :: Rule f -> Rule f -> Bool # (/=) :: Rule f -> Rule f -> Bool #
Ord (Rule f) Source #
Instance details Defined in Twee.Rule Methods compare :: Rule f -> Rule f -> Ordering # (<) :: Rule f -> Rule f -> Bool # (<=) :: Rule f -> Rule f -> Bool # (>) :: Rule f -> Rule f -> Bool # (>=) :: Rule f -> Rule f -> Bool # max :: Rule f -> Rule f -> Rule f # min :: Rule f -> Rule f -> Rule f #
(Labelled f, PrettyTerm f) => Pretty (Rule f) Source #
Instance details Defined in Twee.Rule Methods pPrintPrec :: PrettyLevel -> Rational -> Rule f -> Doc # pPrint :: Rule f -> Doc # pPrintList :: PrettyLevel -> [Rule f] -> Doc #
Symbolic (Rule f) Source #
Instance details Defined in Twee.Rule Associated Types type ConstantOf (Rule f) Source # Methods termsDL :: Rule f -> DList (TermListOf (Rule f)) Source # subst_ :: (Var -> BuilderOf (Rule f)) -> Rule f -> Rule f Source #
f ~ g => Has (Active f) (Rule g) Source #
Instance details Defined in Twee Methods the :: Active f -> Rule g Source #
f ~ g => Has (Rule f) (Rule g) Source #
Instance details Defined in Twee.Rule Methods the :: Rule f -> Rule g Source #
f ~ g => Has (Rule f) (Term g) Source #
Instance details Defined in Twee.Rule Methods the :: Rule f -> Term g Source #
type ConstantOf (Rule f) Source #
Instance details Defined in Twee.Rule type ConstantOf (Rule f) = f

type RuleOf a = Rule (ConstantOf a) Source #

ruleDerivation :: Rule f -> Derivation f Source #

data Orientation f Source #

A rule's orientation.

Oriented and WeaklyOriented rules are used only left-to-right. Permutative and Unoriented rules are used bidirectionally.

Constructors

Oriented	An oriented rule.
WeaklyOriented !(Fun f) [Term f]	A weakly oriented rule. The first argument is the minimal constant, the second argument is a list of terms which are weakly oriented in the rule. A rule with orientation `WeaklyOriented k ts` can be used unless all terms in `ts` are equal to `k`.
Permutative [(Term f, Term f)]	A permutative rule. A rule with orientation `Permutative ts` can be used if `map fst ts` is lexicographically greater than `map snd ts`.
Unoriented	An unoriented rule.

Instances

Instances details

(Labelled f, Show f) => Show (Orientation f) Source #
Instance details Defined in Twee.Rule Methods showsPrec :: Int -> Orientation f -> ShowS # show :: Orientation f -> String # showList :: [Orientation f] -> ShowS #
Eq (Orientation f) Source #
Instance details Defined in Twee.Rule Methods (==) :: Orientation f -> Orientation f -> Bool # (/=) :: Orientation f -> Orientation f -> Bool #
Ord (Orientation f) Source #
Instance details Defined in Twee.Rule Methods compare :: Orientation f -> Orientation f -> Ordering # (<) :: Orientation f -> Orientation f -> Bool # (<=) :: Orientation f -> Orientation f -> Bool # (>) :: Orientation f -> Orientation f -> Bool # (>=) :: Orientation f -> Orientation f -> Bool # max :: Orientation f -> Orientation f -> Orientation f # min :: Orientation f -> Orientation f -> Orientation f #
Symbolic (Orientation f) Source #
Instance details Defined in Twee.Rule Associated Types type ConstantOf (Orientation f) Source # Methods termsDL :: Orientation f -> DList (TermListOf (Orientation f)) Source # subst_ :: (Var -> BuilderOf (Orientation f)) -> Orientation f -> Orientation f Source #
type ConstantOf (Orientation f) Source #
Instance details Defined in Twee.Rule type ConstantOf (Orientation f) = f

oriented :: Orientation f -> Bool Source #

Is a rule oriented or weakly oriented?

unorient :: Rule f -> Equation f Source #

Turn a rule into an equation.

orient :: Function f => Equation f -> Proof f -> Rule f Source #

Turn an equation t :=: u into a rule t -> u by computing the orientation info (e.g. oriented, permutative or unoriented).

Crashes if either t < u, or there is a variable in u which is not in t. To avoid this problem, combine with split.

backwards :: Rule f -> Rule f Source #

Flip an unoriented rule so that it goes right-to-left.

Extra-fast rewriting, without proof output or unorientable rules.

simplify :: (Function f, Has a (Rule f)) => Index f a -> Term f -> Term f Source #

Compute the normal form of a term wrt only oriented rules.

simplifyOutermost :: (Function f, Has a (Rule f)) => Index f a -> Term f -> Term f Source #

Compute the normal form of a term wrt only oriented rules, using outermost reduction.

simplifyInnermost :: (Function f, Has a (Rule f)) => Index f a -> Term f -> Term f Source #

Compute the normal form of a term wrt only oriented rules, using innermost reduction.

simpleRewrite :: (Function f, Has a (Rule f)) => Index f a -> Term f -> Maybe (Rule f, Subst f) Source #

Find a simplification step that applies to a term.

Rewriting, with proof output.

type Strategy f = Term f -> [Reduction f] Source #

A strategy gives a set of possible reductions for a term.

type Reduction f = [(Rule f, Subst f)] Source #

A reduction proof is just a sequence of rewrite steps. In each rewrite step, all subterms that are exactly equal to the LHS of the rule are replaced by the RHS, i.e. the rewrite step is performed as a parallel rewrite without matching.

trans :: Reduction f -> Reduction f -> Reduction f Source #

Transitivity for reduction sequences.

result :: Term f -> Reduction f -> Term f Source #

Compute the final term resulting from a reduction, given the starting term.

reductionProof :: Function f => Term f -> Reduction f -> Derivation f Source #

Turn a reduction into a proof.

ruleResult :: Term f -> (Rule f, Subst f) -> Term f Source #

ruleProof :: Function f => Term f -> (Rule f, Subst f) -> Derivation f Source #

Normalisation.

normaliseWith :: Function f => (Term f -> Bool) -> Strategy f -> Term f -> Reduction f Source #

Normalise a term wrt a particular strategy.

normalForms :: Function f => Strategy f -> Map (Term f) (Reduction f) -> Map (Term f) (Term f, Reduction f) Source #

Compute all normal forms of a set of terms wrt a particular strategy.

successors :: Function f => Strategy f -> Map (Term f) (Reduction f) -> Map (Term f) (Term f, Reduction f) Source #

Compute all successors of a set of terms (a successor of a term t is a term u such that t ->* u).

successorsAndNormalForms :: Function f => Strategy f -> Map (Term f) (Reduction f) -> (Map (Term f) (Term f, Reduction f), Map (Term f) (Term f, Reduction f)) Source #

anywhere :: Strategy f -> Strategy f Source #

Apply a strategy anywhere in a term.

anywhereOutermost :: Strategy f -> Strategy f Source #

Apply a strategy anywhere in a term, preferring outermost reductions.

anywhereInnermost :: Strategy f -> Strategy f Source #

Apply a strategy anywhere in a term, preferring innermost reductions.

Basic strategies. These only apply at the root of the term.

rewrite :: (Function f, Has a (Rule f)) => (Rule f -> Subst f -> Bool) -> Index f a -> Strategy f Source #

A strategy which rewrites using an index.

tryRule :: (Function f, Has a (Rule f)) => (Rule f -> Subst f -> Bool) -> a -> Strategy f Source #

A strategy which applies one rule only.

reducesWith :: Function f => (Term f -> Term f -> Bool) -> Rule f -> Subst f -> Bool Source #

Check if a rule can be applied, given an ordering <= on terms.

reduces :: Function f => Rule f -> Subst f -> Bool Source #

Check if a rule can be applied normally.

reducesOriented :: Function f => Rule f -> Subst f -> Bool Source #

Check if a rule can be applied and is oriented.

reducesInModel :: Function f => Model f -> Rule f -> Subst f -> Bool Source #

Check if a rule can be applied in a particular model.

reducesSkolem :: Function f => Rule f -> Subst f -> Bool Source #

Check if a rule can be applied to the Skolemised version of a term.

Rewriting that performs only a single step at a time (not in parallel).

type Reduction1 f = [(Rule f, Subst f, [Int])] Source #

A reduction proof is a sequence of rewrite steps, stored as a list. Each rewrite step is coded as a rule, a substitution and a path to be rewritten.

trans1 :: Reduction1 f -> Reduction1 f -> Reduction1 f Source #

Transitivity for reduction sequences.

result1 :: HasCallStack => Term f -> Reduction1 f -> Term f Source #

Compute the final term resulting from a reduction, given the starting term.

reductionProof1 :: Function f => Term f -> Reduction1 f -> Derivation f Source #

Turn a reduction into a proof.

ruleResult1 :: HasCallStack => Term f -> (Rule f, Subst f, [Int]) -> Term f Source #

ruleProof1 :: Function f => Term f -> (Rule f, Subst f, [Int]) -> Derivation f Source #

type Strategy1 f = Term f -> [(Rule f, Subst f, [Int])] Source #

A strategy gives a set of possible reductions for a term.

anywhere1 :: Strategy1 f -> Strategy1 f Source #

Apply a strategy anywhere in a term.

basic :: Strategy f -> Strategy1 f Source #

Apply a basic strategy to a term.

normaliseWith1 :: Function f => (Term f -> Bool) -> Strategy1 f -> Term f -> Reduction1 f Source #

Normalise a term wrt a particular strategy.

normaliseWith1Random :: Function f => (Term f -> Bool) -> Strategy1 f -> Term f -> Gen (Reduction1 f) Source #

Normalise a term wrt a particular strategy, picking random rewrites at every step.

rematchReduction1 :: HasCallStack => Term f -> Reduction1 f -> Reduction1 f Source #

Testing whether a term has a unique normal form.

data UNF f Source #

Constructors

UniqueNormalForm (Term f) (Reduction1 f)
HasCriticalPair (Rule f) (Rule f, Int) (ConfluenceFailure f)

Instances

Instances details

Semigroup (UNF f) Source #
Instance details Defined in Twee.Rule Methods (<>) :: UNF f -> UNF f -> UNF f # sconcat :: NonEmpty (UNF f) -> UNF f # stimes :: Integral b => b -> UNF f -> UNF f #
Function f => Pretty (UNF f) Source #
Instance details Defined in Twee.Rule Methods pPrintPrec :: PrettyLevel -> Rational -> UNF f -> Doc # pPrint :: UNF f -> Doc # pPrintList :: PrettyLevel -> [UNF f] -> Doc #

data ConfluenceFailure f Source #

Constructors

ConfluenceFailure
Fields cf_term :: Term f cf_left :: Reduction1 f cf_right :: Reduction1 f cf_orig_term :: Term f cf_orig_left :: Reduction1 f

cf_left_term :: ConfluenceFailure f -> Term f Source #

cf_right_term :: ConfluenceFailure f -> Term f Source #

hasUNFRetry :: Function f => Strategy1 f -> ConfluenceFailure f -> UNF f Source #

hasUNFRandom :: Function f => Strategy1 f -> Term f -> Gen (UNF f) Source #

hasUNFSimple :: Function f => Strategy1 f -> Term f -> Reduction1 f -> UNF f Source #

hasUNF :: (HasCallStack, Function f) => Strategy1 f -> Term f -> Reduction1 f -> UNF f Source #

decomposePath :: Term f -> [Int] -> (Var, [Int]) Source #

varPos :: Var -> Term f -> [Int] Source #

track :: Rule f -> [Int] -> [Int] -> ([[Int]], [[Int]]) Source #