Portability	unportable
Stability	unstable
Maintainer	Martin Avanzini <martin.avanzini@uibk.ac.at>
Safe Haskell	Safe-Infered

Tct.Method.DP.Simplification

Contents

Remove Weak Suffixes
Remove Tails
Simplify Dependency Pair Right-Hand-Sides
Trivial DP Problems
Removing of InapplicableRules
Knowledge Propagation

Description

This module provides various fast transformations that simplify dependency pair problems.

Synopsis

Remove Weak Suffixes

removeWeakSuffix :: TheTransformer RemoveWeakSuffix

Removes trailing weak paths. A dependency pair is on a trailing weak path if it is from the weak components and all sucessors in the dependency graph are on trailing weak paths.

Only applicable on DP-problems as obtained by dependencyPairs or dependencyTuples. Also not applicable when strictTrs prob = Trs.empty.

data RemoveWeakSuffixProof

Constructors

RTProof
Fields removables :: [(NodeId, DGNode)] Tail Nodes of the dependency graph. cgraph :: CDG Employed congruence graph. graph :: DG Employed weak dependency graph. signature :: Signature variables :: Variables
RTError DPError

removeWeakSuffixProcessor :: Transformation RemoveWeakSuffix AnyProcessor

data RemoveWeakSuffix

Instances

Transformer RemoveWeakSuffix
TransformationProof RemoveWeakSuffix

Remove Tails

removeHeads :: TheTransformer RemoveHead

Removes unnecessary roots from the dependency graph.

data RemoveHeadProof

Constructors

RHProof
Fields rhRemoveds :: [(NodeId, DGNode)] rhGraph :: DG Employed weak dependency graph. rhSig :: Signature rhVars :: Variables
RHError DPError

removeHeadProcessor :: Transformation RemoveHead AnyProcessor

data RemoveHead

Instances

Transformer RemoveHead
TransformationProof RemoveHead

Simplify Dependency Pair Right-Hand-Sides

simpDPRHS :: TheTransformer SimpRHS

Simplifies right-hand sides of dependency pairs. Removes r_i from right-hand side c_n(r_1,...,r_n) if no instance of r_i can be rewritten.

Only applicable on DP-problems as obtained by dependencyPairs or dependencyTuples. Also not applicable when strictTrs prob = Trs.empty.

data SimpRHSProof

Constructors

SRHSProof
Fields srhsReplacedRules :: [Rule] Rules that could be simplified. srhsDG :: DG Employed dependency graph. srhsSig :: Signature srhsVars :: Variables
SRHSError DPError

simpDPRHSProcessor :: Transformation SimpRHS AnyProcessor

data SimpRHS

Instances

Transformer SimpRHS
TransformationProof SimpRHS

Trivial DP Problems

trivial :: TheTransformer Trivial

Checks whether the DP problem is trivial, i.e., does not contain any cycles.

Only applicable on DP-problems as obtained by dependencyPairs or dependencyTuples. Also not applicable when strictTrs prob = Trs.empty.

data TrivialProof

Constructors

TrivialProof
Fields trivialCDG :: CDG Employed congruence graph. trivialSig :: Signature trivialVars :: Variables
TrivialError DPError
TrivialFail

trivialProcessor :: Transformation Trivial AnyProcessor

data Trivial

Instances

Transformer Trivial
TransformationProof Trivial

Removing of InapplicableRules

removeInapplicable :: TheTransformer RemoveInapplicable

Removes inapplicable rules in DP deriviations.

Currently we check whether the left-hand side is non-basic, and there exists no incoming edge except from the same rule.

data RemoveInapplicableProof

Constructors

RemoveInapplicableProof
Fields riWDG :: DG Employed dependency graph. riInitials :: [NodeId] Nodes that start a dependency derivation riReachable :: [NodeId] Nodes reachable from initial nodes riSig :: Signature riVars :: Variables
RemoveInapplicableError DPError
RemoveInapplicableFail

removeInapplicableProcessor :: Transformation RemoveInapplicable AnyProcessor

data RemoveInapplicable

Instances

Transformer RemoveInapplicable
TransformationProof RemoveInapplicable

Knowledge Propagation

simpPE :: TheTransformer (SimpPE AnyProcessor)

Moves a strict dependency into the weak component if all predecessors in the dependency graph are strict and there is no edge from the rule to itself.

simpPEOn :: ExpressionSelector -> TheTransformer (SimpPE AnyProcessor)

withPEOn :: Processor p => InstanceOf p -> ExpressionSelector -> TheTransformer (SimpPE p)

data SimpPEProof p

Constructors

SimpPEProof
Fields skpDG :: DG skpSelections :: [SimpPESelection] skpSig :: Signature skpVars :: Variables
SimpPEPProof
Fields skpDG :: DG skpSig :: Signature skpPProof :: PartialProof (ProofOf p) skpPProc :: InstanceOf p skpSelections :: [SimpPESelection] skpVars :: Variables
SimpPEErr DPError

simpPEProcessor :: Transformation (SimpPE AnyProcessor) AnyProcessor

data SimpPE p

Instances

Processor p => Transformer (SimpPE p)
Processor p => TransformationProof (SimpPE p)