As in C, a funciton in ATS may also take an indefinite number of arguments. Let us use the function printf in ATS, which corresponds to the function of the same name in C, as an example to explain this feature.
The type of printf is given as follows:
fun printf : {ts:types} (printf_c ts, ts) -> void
We use printf_c for a type constructor that forms types for format
strings (in C) when applied to lists of types. For instance,
printf_c(char, double, int) is a type for format strings that require
a character, a double, and an integer to be supplied. Given
a character c, a double d and an integer i,
@(c, d, i) is an argument of types (char, double, int),
and the following expression is well-typed in ATS:
printf ("c = %c and d = %f and i = %i", @(c, d, i))
The type of the format string
"c = %c and d = %f and i = %i" is computed to be
printf_c (char, double, int)
and then @(c, d, i) is checked to be of the type
(char, double, int). Note that a format string must be a constant
in order for its type to be computed during typechecking.
As an example, we present as follows a program that prints out a multiplication table for single digits:
#define N 9
implement main (argc, argv) = loop1 (0) where {
// [loop1] and [loop2] are verified to be terminating based on the supplied metrics
// [.< N-i, 0 >.] is a termination metric
// Ignore it if you have not learned this feature yet
fun loop1 {i:nat | i <= N} .< N-i, 0 >. (i: int i): void =
if i < N then loop2 (i+1, 0) else ()
// end of [loop1]
// [.< N-i, N+1-j >.] is a termination metric
// Ignore it if you have notlearned this feature yet
and loop2 {i,j:nat | i <= N; j <= i} .< N-i, i-j+1 >. (i: int i, j: int j): void =
if j < i then begin
if (j > 0) then print '\t';
printf ("%1d*%1d=%2.2d", @(j+1, i, (j+1) * i));
loop2 (i, j+1)
end else begin
print_newline (); loop1 (i)
end // end of [if]
// end of [loop2]
} // end of [main]
The following text is the output of the program:
1*1=01 1*2=02 2*2=04 1*3=03 2*3=06 3*3=09 1*4=04 2*4=08 3*4=12 4*4=16 1*5=05 2*5=10 3*5=15 4*5=20 5*5=25 1*6=06 2*6=12 3*6=18 4*6=24 5*6=30 6*6=36 1*7=07 2*7=14 3*7=21 4*7=28 5*7=35 6*7=42 7*7=49 1*8=08 2*8=16 3*8=24 4*8=32 5*8=40 6*8=48 7*8=56 8*8=64 1*9=09 2*9=18 3*9=27 4*9=36 5*9=45 6*9=54 7*9=63 8*9=72 9*9=81
The code used for illustration is available here.