Introduction to Programming in ATS:
<<< PreviousModularityNext >>>

Static and Dynamic ATS Files

The first letters in the ATS filename extensions sats and dats refer to the words static and dynamic, respectively. For instance, foo.sats is a name for a static file while bar.dats for a dynamic one. A static file usually contains interface declarations for functions and values, datatype declarations, type definitions, etc. The primary purpose of such a file is for allowing its content to be shared among various other ATS files, either static or dynamic.

Let us now go through a simple example to see a typical use of static files. Suppose that we want to implement the Ackermann's function, which is famous for being recursive but not primitive recursive. In a static file named acker.sats (or any other legal filename), we can declare the following function interface: 

fun acker (m: int, n: int): int

Please note that we cannot use the keyword extern when declaring an interface for either a function or a value in a static file. Then in a dynamic file named acker.dats (or any other legal filename), we can give the following implementation: 

staload "acker.sats"

implement
acker (m, n) =
  if m > 0 then
    if n > 0 then acker (m-1, acker (m, n-1))
    else acker (m-1, 1)
  else n+1
// end of [acker]

The keyword staload indicates to the ATS typechecker that the file following it is to be statically loaded. Essentially, statically loading a file means to put the content of the file in a namespace that can be accessed by the code that follows. It is important to note that static loading is different from plain file inclusion. The latter is also supported in ATS, and it is a feature I will cover elsewhere.

It is also possible to give the following implementation for the declared function acker: 

staload ACKER = "acker.sats"

implement $ACKER.acker
  (m, n) = acker (m, n) where {
  fun acker (m: int, n:int): int = 
    if m > 0 then
      if n > 0 then acker (m-1, acker (m, n-1))
      else acker (m-1, 1)
    else n+1
} // end of [$ACKER.acker]

In this case, the namespace for storing the content of the file acker.sats is given the name ACKER, and the prefix $ACKER. (the dollar sign followed by ACKER followed by the dot symbol) must be attached to any name that refers an entity (a function, a value, a datatype, the constructors associated with a datatype, a type definition, etc.) declared in acker.sats. When there are many static files to be loaded, it is often a good practice to assign names to the namespaces holding these files so that the original source of each declared entity can be readily tracked down.

In another file named test_acker.dats, let use write the following code: 

staload "acker.sats"
dynload "acker.dats"

implement
main () = () where {
//
// acker (3, 3) should return 61
//
  val () = assertloc (acker (3, 3) = 61)
} // end of [main]

The keyword dynload indicates to the ATS compiler to generate a call to the initializing function associated with the file acker.dats. This is mandatory as an error would otherwise be reported at link-time. Usually, calling the initializing function associated with a dynamic file is necessary only if there is a value implemented in the file. In this case, there is only a function implemented in acker.dats. If we include the following line somewhere inside acker.dats: 

#define ATS_DYNLOADFLAG 0 // no need for dynloading at run-time

then the line starting with the keyword dynload in test_acker.dats is no longer needed. The function assertloc verifies at run-time that its argument evaluates to the boolean value true. In the case where the argument evaluates to false, the function call aborts and a message is reported that contains the name of the file, which is test_acker.dats in this example, and the location at which the source code of the call is found in the file. If this sounds a bit confusing, please try to execute a program that contains a call to assertloc on false and you will see clearly what happens.

The simplest way to compile the three files acker.sats, acker.dats and test_acker.dats is to issue the following command-line: 


atscc -o test_acker acker.sats acker.dats test_acker.dats

The generate excutable test_acker is in the current working directory. The compilation can also be performed separately as is demonstrated below: 


atscc -c acker.sats
atscc -c acker.dats
atscc -c test_acker.dats
atscc -o test_acker acker_sats.o acker_dats.o test_acker_dats.o

This style of separate compilation works particularly well when it is employed by the make utility.

<<< PreviousHomeNext >>>
ModularityUpGeneric Template Implementation