Introduction to Programming in ATS:
PrevChapter 7. ModularityNext

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 is for a dynamic one. A static file is often referred to as a SATS-file, and it usually contains interface declarations for functions and values, datatype declarations, type definitions, etc. The primary purpose of a SATS-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 one should not 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 during typechecking. Essentially, statically loading a file means to put the content of the file in a namespace that can be accessed by the following code. 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, a constructor (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 us write the following code: 

//
#include
"share/atspre_staload.hats"
//
staload "acker.sats"
dynload "acker.dats"

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

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 two files acker.dats and test_acker.dats is to issue the following command-line: 


atscc -o test_acker acker.dats test_acker.dats

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


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

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

If we want to, we can also merge acker.sats and acker.dats into a single file of the following content: 

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

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]

Suppose that this single file is given the name acker3.dats. Then the testing code can be written as follows: 

//
#include
"share/atspre_staload.hats"
//
staload "acker3.dats"
dynload "acker3.dats"

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

Note that it is perfectly fine for a dynamic ATS file to be statically loaded. Actually, a static ATS file is really just a special case of dynamic ATS file in which there is no implementation (of either functions or values).

PrevHomeNext
ModularityUpGeneric Template Implementation