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

 ${HOME}/.tct/tct.hs

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
#!/usr/bin/runhaskell
.
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:

Tct.Configuration

This module. It defines the defaultConfig, and operators to modify it.

Tct.Interactive

This module exposes the functionality of the interactive mode.

Tct.Instances

This module defines operations for constructing (instances of) processors, together with many combinators.

Tct.Processors

This module exports all processors implemented in TcT. These are useful, in the interactive mode, cf. the action apply.

Termlib.Repl

This module gives access to the term rewriting library.

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.

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.

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.

Constructor for Arg a with sensible defaults.

Argument that can additionally be none.