tct-2.0.1: A Complexity Analyser for Term Rewrite Systems

MaintainerMartin Avanzini <>
Safe HaskellSafe-Infered







In this section we describe the configuration of TcT, both influencing the command line interface (cf. Tct.CommandLine) and the interactive interface (cf. Tct.Interactive).

The command line interface supports various flags that govern the behaviour of TcT. Besides basic options given on the command line, TcT can be configured by modifying the configuration file. The configuration file is a Haskell source file that resides in


by default, and defines the actual binary that is run each time TcT is called. Thus the full expressiveness of Haskell is available, as a downside, it requires also a working Haskell environment.

A minimal configuration is generated automatically on the first run of TcT. This initial configuration constitutes of a set of convenient imports, the IO action main together with a configuration record Config.

>>> cat ${HOME}/.tct/tct.hs
import Prelude hiding (fail, uncurry)
import Tct.Configuration
import Tct.Interactive
import Tct.Instances
import qualified Tct.Instances as Instance
import qualified Tct.Processors as Processor
import qualified Termlib.Repl as TR
config :: Config
config = defaultConfig
main :: IO ()
main = tct config

Notably, the body of the default configuration contains two definitions.

config :: Config
This definition defines the configuration of TcT, as explained below. The definition is mandatory if you want to run the interactive interface, cf. Tct.Interactive.
main :: IO ()
This is the main program. Specifying the main program is mandatory for using the command line interface as explained in Tct.CommandLine.

The default configuration imports following modules:

This module. It defines the defaultConfig, and operators to modify it.
This module exposes the functionality of the interactive mode.
This module defines operations for constructing (instances of) processors, together with many combinators.
This module exports all processors implemented in TcT. These are useful, in the interactive mode, cf. the action apply.
This module gives access to the term rewriting library.

defaultConfig :: Config

This is the default configuration of TcT.

tct :: Config -> IO ()

This runs TcT with the given configuration. Use defaultConfig for running TcT with the default configuration.

The Configuration Record

The configuration record passed in main allows one to predefine various flags of TcT, but most importantly, through the field strategies it allows the modification of the list of strategies that can be employed. Note that option specified at the command line overwrite the ones supplied in the config file.

data Config

Configuration of TcT.




strategies :: [Strategy]

This field can be extended by custom strategies.

allProcessors :: AnyProcessor

This fields holds the processor available in TcT.

makeProcessor :: Problem -> AnyProcessor -> ErroneousIO (InstanceOf SomeProcessor)

This field can be used to govern how a processor is determined for the loaded problem if no processor is supplied at the command line. The second parameter refers to the list of available processors.

recompile :: Bool

This flag determines if the configuration file should be dynamically reloaded.

configDir :: ErroneousIO FilePath

This field specifies the configuration dir. It defaults to '${HOME}/.tct'.

outputMode :: OutputMode

This field specifies the output mode under which proofs are displayed. It defaults to proof output.

logFile :: Maybe FilePath

This field may be used to specify a log-file, showing extended output concerning applications of processors.

getSolver :: ErroneousIO SatSolver

This field can be used to specify an alternative SAT solver. Per default, TcT searches for executables minisat or minisat2 in '${PATH}'.

version :: String

This field can be used to modify the version.

putProof :: Proof SomeProcessor -> PPMode -> IO ()

This field can be overwritten in order to govern how a proof is displayed.

putError :: TCTError -> IO ()

This field can be overwritten in order to govern how an error message is displayed.

putWarning :: TCTWarning -> IO ()

This field can be overwritten in order to govern how a warning is displayed.

timeoutAfter :: Maybe Int

This field can be used to set an optional timeout, in seconds.

problemFile :: FilePath

This field holds the file name of the input problem.

interactiveShowProofs :: Bool

When this flag is True, interactive mode will print proofs after execution of commands.

listStrategies :: Maybe (Maybe String)

Modified by command line option '--list', cf. Tct.CommandLine.

answerType :: Maybe AnswerType

Modified by command line option '--answer', cf. Tct.CommandLine.

showHelp :: Bool

Modified by command line option '--help', cf. Tct.CommandLine.

showVersion :: Bool

Modified by command line option '--version', cf. Tct.CommandLine.

interactive :: Bool

Modified by command line option '--interactive', cf. Tct.CommandLine.

errorMsg :: [String]

This field holds error messages from dynamic recompilation.

Adding Strategies to TcT

Strategies are added by overwriting the field strategies with a list of strategy declarations, of the form

 code ::: strategy name [parameter-declaration]

Here code refers to a value that defines the actual processor, name the name of the strategy, and the last component is used to indicate the arguments of the defined strategy.

The following depicts a modified configuration that defines two new strategies, called matrices and withDP. Observe that one can use both transformations and processors, optionally parameterised as governed by the parameter-declaration, as code.

 config :: Config
 config = defaultConfig { strategies = strategies } where
   strategies = [ matrices ::: strategy "matrices" ( optional naturalArg "start" (Nat 1) :+: naturalArg )
                , withDP   ::: strategy "withDP" ]
 matrices (Nat start :+: Nat n) = 
   fastest [ matrix ` withDimension ` d | d <- [start..start+n] ] where
 withDP = 
   (timeout 5 dps <> dts)
   >>> try (exhaustively partitionIndependent)
   >>> try cleanSuffix
   >>> try usableRules where 
     dps = dependencyPairs >>> try usableRules >>> wgOnUsable
     dts = dependencyTuples
     wgOnUsable = weightgap ` wgOn ` WgOnTrs }

Consider the first strategy declaration that defines a strategy matrices [:start <nat>] <nat>. The declaration indicates that this strategy takes two parameters, the left and respectively right argument to the operator :+:. In general, the infix operator :+: can be used to combine an arbitrary sequence of parameters. In the declaration above, the defined strategy expects two natural numbers, as indicated by the constructor naturalArg. The first parameter is declared as an optional parameter called start, whose default value is given as 1. The parameters are provided to the code of matrices. Using the supplied parameters start and n, the code evaluates to a processor that searches for n different matrix interpretations of increasing dimension in parallel. Along with other processors and combinators, both matrix and fastest from the module Tct.Instances.

The second strategy declaration above declares a transformation called withDP. Transformations generate from the input problem a possibly empty set of sub-problems, in a complexity preserving manner. For every transformation t and processor p, one can use the processor t >>| p which first applies transformation t and then proceeds according to /p on all resulting sub-problems. Strategy declarations perform such a lifting of transformation implicitly, the declaration of withDP for instance results in a strategy withDP <processor.

Parameter Declarations

Values of type Arg a can be used to define single parameters, and can be combined with :+: to create a parameter list. Note that the type variable a accounts for the type of the defined parameter, and must be an instance of ParsableArgument. In Section 'Tct.Configuration#primdecls' below we provide various instances.

data Arg t

This datatype captures the description of a single argument.




name :: String

The name of the argument.

description :: String

Optional description for the argument.

defaultValue :: Domain t

A possible default value, if the argument is optional.

isOptional_ :: Bool

Indicates wether the argument is optional.

Constructor for Arg a with sensible defaults.

arg :: Arg t

Constructor for description of arguments of type t.

data a :+: b

This operator constructs tuples of arguments.


a :+: b 


optional :: Arg t -> String -> Domain t -> Arg t

Constructor for description of optional arguments of type t. The following describes an optional argument dimension with default value 2.

>>> optional naturalArg "dimension" 2


boolArg :: Arg Bool

Boolean argument, which is parsed as either On or Off.

naturalArg :: Arg Nat

Natural argument

processorArg :: Arg Processor

Processor argument

type EnumArg a = Arg (EnumOf a)

This can be used to lift instances of Typeable, Show, Enum and Bounded to arguments. Suppose you have a datatype like the following.

>>> data MyType = A | B | C deriving (Typeable, Show, Enum, Bounded)

An argument description for an element of type MyType is then given by

>>> arg :: EnumArg MyType

type AssocArg a = Arg (Assoc a)

Construct an argument from an associated list, by declaring a datatype an instance of AssocArgument. Use as follows:

>>> instance AssocArgument MyType where
     assoc _ = [("nameA", valueA), ("nameB", valueB)...]

Then one can use a declaration

>>> arg :: AssocArg MyType

which will parse valueA as nameA, valueB as nameB, and so on.

class AssocArgument a where

Instances of this class can be parsed by means of the defined method assoc.


assoc :: Phantom a -> [(String, a)]

The resulting list associates names to elements, and should be finite. An element is parsed by parsing its name.

Argument that can additionally be none.

maybeArg :: Arg a -> Arg (Maybe a)

Argument, that additionally parses as none.

listArg :: Arg a -> Arg [a]

A list of arguments.