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

Tct.Processor.Transformations

Contents

Using Transformations
- Lifting to Processors
Defining new Transformations
- Transformation Result
- Transformation Proof
Existential Quantification
Subsumed Processor
Misc

Description

This module gives the infrastructure for transformation processors. Transformation processors transform an input problem into zero or more subproblems, reflecting the complexity of the input problem. Transformations abort if the input problem cannot be simplified. Use try to continue with the input problem.

Synopsis

Using Transformations

data TheTransformer t

This datatype defines a specific instance of a transformation.

Constructors

TheTransformer
Fields transformation :: t The Transformation. transformationArgs :: Domains (ArgumentsOf t) Arguments of the transformation.

Instances

HasUsableArgs (TheTransformer WeightGap)
HasCBits (TheTransformer WeightGap)
HasBits (TheTransformer WeightGap)
HasDegree (TheTransformer WeightGap)
Processor a => Decomposing (TheTransformer (Decompose a))
HasCertBy (TheTransformer WeightGap)
HasDimension (TheTransformer WeightGap)
(Transformer t, ParsableArguments (ArgumentsOf t)) => Describe (TheTransformer t)
Transformer t => Apply (TheTransformer t)
Transformer trans => AsStrategy (TheTransformer trans) ConstantDeclaration
Transformer t => WithProblem (TheTransformer t) (TheTransformer (WithProblem t))
Transformer t => Timed (TheTransformer t) (TheTransformer (Timed t))
Transformer t => TimesOut (TheTransformer t) (TheTransformer (Timeout t))
Transformer t => EQuantified (TheTransformer t) (TheTransformer SomeTransformation)
(ParsableArguments args, Transformer trans, ~ * ds (Domains args)) => AsStrategy (ds -> TheTransformer trans) (FunctionDeclaration args)

Lifting to Processors

(>>|) :: (Processor sub, Transformer t) => TheTransformer t -> InstanceOf sub -> TransformationInstance t sub

The processor t >>| p first applies the transformation t. If this succeeds, the processor p is applied on the resulting subproblems. Otherwise t >>| p fails.

(>>||) :: (Processor sub, Transformer t) => TheTransformer t -> InstanceOf sub -> TransformationInstance t sub

Like >>| but resulting subproblems are solved in parallel by the given processor.

Defining new Transformations

In order to define a new transformation, define an instance of Transformer and TransformationProof. Use withArgs for providing an instance constructor, compare Tct.instances. Use transformationProcessor to lift the defined transformation to a processor.

class (Arguments (ArgumentsOf t), TransformationProof t) => Transformer t where

The main class a transformation implements.

Associated Types

type ArgumentsOf t

Arguments of the transformation, cf. Tct.Processor.Args.

type ProofOf t

Proof type of the transformation.

Methods

name :: t -> String

Unique name.

description :: t -> [String]

Description of the transformation.

arguments :: t -> ArgumentsOf t

Description of the arguments, cf. module Tct.Processor.Args.

instanceName :: TheTransformer t -> String

Optional name specific to instances. Defaults to the transformation name.

transform :: SolverM m => TheTransformer t -> Problem -> m (Result t)

This is the main method of a transformation. Given a concrete instance, it translates a complexity problem into a Result.

continue :: TheTransformer t -> Bool

If True, then the processor will pretend that the input problem was simplified, independent on the result of transform. This is used for implementing transformation Try, and should not be defined.

Instances

Transformer SomeTransformation
Transformer Id
Transformer InnermostRuleRemoval
Transformer ToInnermost
Transformer Uncurry
Transformer WeightGap
Transformer UR
Transformer DPs
Transformer RemoveInapplicable
Transformer Trivial
Transformer SimpRHS
Transformer RemoveWeakSuffix
Transformer RemoveHead
Transformer PathAnalysis
Transformer t => Transformer (WithProblem t)
Transformer t => Transformer (Timeout t)
Transformer t => Transformer (Timed t)
Transformer t => Transformer (Try t)
Processor p => Transformer (Decompose p)
Processor p => Transformer (SimpPE p)
(Transformer t1, Transformer t2) => Transformer (:<>: t1 t2)
(Transformer t1, Transformer t2) => Transformer (:>>>: t1 t2)
(Processor p1, Processor p2) => Transformer (DecomposeDG p1 p2)

class TransformationProof t where

Every transformer needs to implement this class. Minimal definition: answer and pprintTProof.

Methods

answer :: Processor sub => Proof t sub -> Answer

Construct an Answer from the Proof.

tproofToXml :: Transformer t => TheTransformer t -> Problem -> ProofOf t -> (String, [XmlContent])

Construct an Xml-node from a transformation proof. The default implementation wraps the pretty-printed output in a proofdata node

proofToXml :: (Transformer t, Processor sub) => Proof t sub -> XmlContent

pprintTProof :: TheTransformer t -> Problem -> ProofOf t -> PPMode -> Doc

Pretty print the transformation proof.

pprintProof :: (Transformer t, Processor sub) => Proof t sub -> PPMode -> Doc

Pretty printer of the Proof. A default implementation is given.

normalisedProof :: (Transformer t, Processor sub) => Proof t sub -> Proof SomeTransformation SomeProcessor

Instances

TransformationProof SomeTransformation
TransformationProof Id
TransformationProof InnermostRuleRemoval
TransformationProof ToInnermost
TransformationProof Uncurry
TransformationProof WeightGap
TransformationProof UR
TransformationProof DPs
TransformationProof RemoveInapplicable
TransformationProof Trivial
TransformationProof SimpRHS
TransformationProof RemoveWeakSuffix
TransformationProof RemoveHead
TransformationProof PathAnalysis
Transformer t => TransformationProof (WithProblem t)
(Transformer t, TransformationProof t) => TransformationProof (Timeout t)
(Transformer t, TransformationProof t) => TransformationProof (Timed t)
(Transformer t, TransformationProof t) => TransformationProof (Try t)
Processor p => TransformationProof (Decompose p)
Processor p => TransformationProof (SimpPE p)
(Transformer t1, Transformer t2) => TransformationProof (:<>: t1 t2)
(TransformationProof t1, Transformer t1, Transformer t2) => TransformationProof (:>>>: t1 t2)
(Processor p1, Processor p2) => TransformationProof (DecomposeDG p1 p2)

data Transformation t sub

Provides a lifting from Transformer to Processor.

Constructors

Transformation t

Instances

(Transformer t, Processor sub) => Processor (Transformation t sub)
(Transformer t, ParsableArguments (ArgumentsOf t)) => Describe (Transformation t AnyProcessor)
(ParsableArguments (ArgumentsOf t), Transformer t) => Apply (Transformation t sub)

withArgs :: Transformer t => Transformation t sub -> Domains (ArgumentsOf t) -> TheTransformer t

Constructor for instances.

modifyArguments :: Transformer t => (Domains (ArgumentsOf t) -> Domains (ArgumentsOf t)) -> TheTransformer t -> TheTransformer t

Modify parameters of instance

transformationProcessor :: (Arguments (ArgumentsOf t), ParsableArguments (ArgumentsOf t), Transformer t) => t -> StdProcessor (Transformation t sub)

Lifts transformations to standard processors.

Transformation Result

data Result t

Result type for a transformation.

Constructors

NoProgress (ProofOf t)	The transformation did not simplify the problem.
Progress (ProofOf t) (Enumeration Problem)	The transformation resulted in the given subproblems.

proofFromResult :: Result t -> ProofOf t

subProblemsFromResult :: Result r -> Enumeration Problem

isProgressResult :: Result r -> Bool

mapResult :: (ProofOf t1 -> ProofOf t2) -> Result t1 -> Result t2

sanitiseResult :: Result t1 -> Result t1

Transformation Proof

data Proof t sub

This is the proof of a transformation lifted to a processor.

Constructors

Proof
Fields transformationResult :: Result t The `Result` generated by the transformation inputProblem :: Problem The input problem appliedTransformer :: TheTransformer t The instance of the applied transformation appliedSubprocessor :: InstanceOf sub The instance of the applied subprocessor subProofs :: Enumeration (Proof sub) An enumeration of the subproofs

Instances

(Transformer t, Processor sub) => ComplexityProof (Proof t sub)

subProblems :: Proof t sub -> Enumeration Problem

findProof :: Numbering a => a -> Proof t sub -> Maybe (Proof sub)

transformationProof :: Proof t sub -> ProofOf t

answerFromSubProof :: Processor sub => Proof t sub -> Answer

If the proof contains exactly one subproblem, return the computed certificate of this problem. Otherwise, return MaybeAnswer.

Existential Quantification

data SomeTransformation

Constructors

forall t . Transformer t => SomeTransformation t (Domains (ArgumentsOf t))

Instances

Transformer SomeTransformation
TransformationProof SomeTransformation
Transformer t => EQuantified (TheTransformer t) (TheTransformer SomeTransformation)

data SomeTransProof

Constructors

forall t . (Transformer t, TransformationProof t) => SomeTransProof (TheTransformer t) (ProofOf t)

someTransformation :: Transformer t => TheTransformer t -> TheTransformer SomeTransformation

someProof :: (Transformer t, Processor sub) => Proof t sub -> Proof SomeTransformation SomeProcessor

Subsumed Processor

The following utilities are used only internally.

liftMS :: Maybe Problem -> Proof proc -> Proof (Subsumed proc)

mkSubsumed :: InstanceOf proc -> InstanceOf (Subsumed proc)

Misc

transformerToXml :: Transformer t => TheTransformer t -> XmlContent

thenApply :: (Processor sub, Transformer t) => TheTransformer t -> InstanceOf sub -> TransformationInstance t sub