Printf-like Functions

The printf function in C is variadic, that is, the arity of the function is indefinite. In ATS, there is a function of the same name that is essentially the counterpart of the printf function in C.

The following interface is assigned to printf in ATS:

fun printf {ts:types} (fmt: printf_c ts, arg: ts): void

We use printf_c for a type constructor that takes a list of types to form a type for format strings (in C). 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 () = let
  fun loop1
    {i:nat | i <= N}
    (i: int i): void =
    if i < N then loop2 (i+1, 0) else ()
  // end of [loop1]
  and loop2
    {i,j:nat | i <= N; j <= i}
    (i: int i, j: int j): void =
    if j < i then let
      val () = if (j > 0) then print '	'
      val () = printf ("%1d*%1d=%2.2d", @(j+1, i, (j+1) * i))
    in
      loop2 (i, j+1)
    end else let
      val () = print_newline () in loop1 (i)
    end // end of [if]
  // end of [loop2]
in
  loop1 (0)
end // end of [main]

This programs generates the following expected output:


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

Please find a few other functions declared in prelude/SATS/printf.sats that are similar to printf.