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:
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]
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 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 simplest way to compile the two files acker.dats and test_acker.dats is to issue the following command-line:
The generated excutable test_acker is in the current working directory. The compilation can also be performed separately as is demonstrated below: 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:
Suppose that this single file is given the name acker3.dats. Then the testing code can be written as follows: 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).