The Program Entry Point: mainats

There are two special functions of the name main_void and main_argc_argv that are given the following interfaces:

fun main_void (): void = "mainats"
overload main with main_void

fun main_argc_argv {n:int | n >= 1}
  (argc: int n, argv: &(@[string][n])): void = "mainats"
overload main with main_argc_argv

The symbol main is overloaded with both of these functions. In addition, the C-name mainats is assigned to both of them. When a function in ATS is translated into one in C, the C-name of the function, if ever assgined, is used to refer to its translation in C.

The interface for main_argc_argv indicates that the function takes as its arguments an integer argc greater than 0 and an array argv of size argc in which each element is a string, and returns no value. The syntax argv: &(@[string][n] means that argv is a call-by-reference argument. If we followed the like of syntax in C++, then this would be written as something like &argv: @[string][n].

To turn ATS source code into an executable, the function is required to be present in the C code translated from the ATS code (as it is called within the main function in C). Normally, this means that either main_void or main_argc_argv needs to be implemented in the ATS code (that is to be turned into an executable). However, in certain situations, it may make sense to implement mainats in C directly. Note that the interface for mainats in C is:

extern ats_void_type mainats (ats_int_type, ats_ptr_type) ;

where ats_void_type, ats_int_type and ats_ptr_type are just aliases for void, int and void*, respectively.

As an example, the following ATS program echos onto the standard output the given command line:

main (argc, argv) = let
  fun loop {n,i:nat | i <= n} // [loop] is tail-recursive
    (i: int i, argc: int n, argv: &(@[string][n])): void =
    if i < argc then begin
      if i > 0 then print (' '); print argv.[i]; loop (i+1, argc, argv)
    end // end of [if]
  // end of [loop]
  loop (0, argc, argv); print_newline ()
end // end of [main]

If mainats needs to be implemented in C, the proof function main_dummy should be implemented as follows:

implement main_dummy () = ()

This implementation is solely for telling the ATS compiler that mainats is expected to be implemented in C directly so that the compiler can generate proper code to handle the situation. As an example, I present as follows a typical scenario in GTK+ programming, where the function gtk_init needs to be called to modify the arguments passed from the given command line:

// some function implemented in ATS
extern fun main_work // implemented elsewhere
  {n:pos} (argc: int n, argv: &(@[string][n])): void = "main_work"
// end of [main_work]

// %{^ : the embedded C code is placed at the top
extern ats_void_type mainats (ats_int_type, ats_ptr_type) ;
%} // end of [%{^]

implement main_dummy () = () // indicating [mainats] being implemented in C

// %{$ : the embedded C code is placed at the bottom
mainats (
  ats_int_type argc, ats_ptr_type argv
) {
  gtk_init ((int*)&argc, (char ***)&argv) ; main_work (argc, argv) ; return ;
} /* end of [mainats] */

%} // end of [%{$]