tct-2.0.1: A Complexity Analyser for Term Rewrite Systems

Portabilityunportable
Stabilityunstable
MaintainerMartin Avanzini <martin.avanzini@uibk.ac.at>
Safe HaskellSafe-Infered

Tct.Method.TCombinator

Contents

Description

This module implements all transformation combinators.

Synopsis

Timeout

data TimeoutProof t

Constructors

NoTimeout (ProofOf t) 
TimedOut Int 

Timed

timed :: Transformer t => TheTransformer t -> TheTransformer (Timed t)

The transformer timed t behaves like t but additionally measures the execution time.

data TimedProof t

Constructors

TimedProof 

Fields

tpCpu :: Double
 
tpWall :: Double
 
tpProof :: ProofOf t
 

Try

try :: Transformer t => TheTransformer t -> TheTransformer (Try t)

The transformer try t behaves like t but succeeds even if t fails. When t fails the input problem is returned.

force :: Transformer t => TheTransformer t -> TheTransformer (Try t)

The transformer force t behaves like t but fails always whenever no progress is achieved.

data Try t

Constructors

Try Bool t 

data TryProof t

Constructors

TryProof Bool (ProofOf t) 

Composition

(>>>) :: (Transformer t1, Transformer t2) => TheTransformer t1 -> TheTransformer t2 -> TheTransformer SomeTransformation

The transformer t1 >>> t2 first transforms using t1, resulting subproblems are transformed using t2.

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

The transformer exhaustively t applies t repeatedly until t fails. exhaustively t == t >>> try (exhaustively t).

data t1 :>>>: t2

Constructors

(TheTransformer t1) :>>>: (TheTransformer t2) 

data ComposeProof t1 t2

Constructors

ComposeProof (Result t1) (Maybe (Enumeration (Result t2))) 

Choice

(<>) :: (Transformer t1, Transformer t2) => TheTransformer t1 -> TheTransformer t2 -> TheTransformer SomeTransformation

The transformer t1 <> t2 transforms the input using t1 if successfull, otherwise t2 is applied.

(<||>) :: (Transformer t1, Transformer t2) => TheTransformer t1 -> TheTransformer t2 -> TheTransformer SomeTransformation

The transformer t1 <||> t2 applies the transformations t1 and t2 in parallel, using the result of whichever transformation succeeds first.

data t1 :<>: t2

Constructors

Choice 

Instances

data ChoiceProof t1 t2

Constructors

ChoiceOne (Result t1) 
ChoiceTwo (Result t2) 
ChoiceSeq (Result t1) (Result t2) 

WithProblem

ID

idtrans :: TheTransformer Id

Identity transformation.

data Unique a

Constructors

One a 
Two a 

Instances