Dependencies
============

ocaml (possibly with ocamllex and ocamlyacc)


Compiling the program
=====================

To compile:
  $ make

Running the program
===================

The program reads recursive definitions from standard input and checks if they
pass the size-change termination criterion.
To end the input (and check the definitions), press Control-d.

To read definitions from a file, use
  $ ./sct < file

It is possible to change the value of bound B with
  $ ./sct -B 3
and to change the value of bound D with
  $ ./sct -D 4

For example, we get the original SCT with depth of values with
  $ ./sct -B 1 -D 0 -collapse_analysis
or simply with
  $ ./sct -original_SCT


It is possible to ask the program to print various information. Use
  $ ./sct -v <n>
where n is 1, 2, 3, 4, 5 or 6.


Syntax of recursive definitions
===============================

Recursive definitions are written with a very simple syntax definitions.
The aim was to make parsing and static analysis as simple as possible.
All the examples from the papers are given in the "examples" subdirectory.


Each line (clause) of a recursive definition is of the form

  function_name  pattern*  =  body

where a "pattern" is a Caml (deep) pattern matching and "body" uses only
applications, constructors, tuples, variables from the patterns and other
function names.

Here is, for example, the Ackermann function:

ackermann Z[] Z[] = S[Z[]]
ackermann Z[] S[n] = S[S[n]]
ackermann S[m] Z[] = ackermann m S[Z[]]
ackermann S[m] S[n] = ackermann m (ackermann S[m] n)


The points to note are
  - each clause of the definition must be on a single line
  - all constructors require square brackets
  - the global environment of the definitions is empty
  - no type checking is done, only termination checking

Several examples are given in the "examples" directory.