The module system of ATS is largely infuenced by that of Modula-3, which is both simple and general as well as effective in supporting large scale programming.
In addition, ATS contains a component ATS/LF that supports a form of (interactive) theorem proving, where proofs are written as total functions. With this component, we can advocate a programming style that combines programming with theorem proving. Furthermore, we may use this component as a logical framework to encode various deduction systems and their (meta-)properties.
Once these requirements are met, you can readily install Geizella in 3 steps as described below:
tar -zvxf ATS.tar.gz
setenv ATSHOME FOO/ATS/
setenv PATH ${PATH}:${ATSHOME}/bin
make all
// compilation command: // atscc -o HelloWorld HelloWorld.dats implement main (argc, argv) = begin print ("Hello, world!"); print_newline () end
>> atscc -o HelloWorld HelloWorld.dats
<< Hello, world!
// [fun] declares a recursive function fun fact1 (x: int): int = if x > 0 then x * fact1 (x-1) else 1
// [fn] declares a non-recursive function; it is fine to replace [fn] with [fun] // [@(...)] is used in ATS to group arguments for functions of variable arguments fn fact1_usage (cmd: string): void = prerrf ("Usage: %s [integer]\n", @(cmd)) // print an error message implement main (argc, argv) = if argc >= 2 then let val n = int1_of argv.[1] // turning a string into an integer val res = fact1 n in printf ("factorial of %i = %i\n", @(n, res)) end else begin fact1_usage (argv.[0]); exit (1) end
// [a:viewt@ype] means that [a] can be a linear type of any size fun exit : {a:viewt@ype} int -> a
The entire code for this example is available here.
int -> type
typedef Int = [n:int] int n // type for integers
typedef Nat = [n:int | n >= 0] int n // type for natural numbers
The factorial function can be implemented as follows:
fun fact2 {n:nat} (x: int n): Nat = if x > 0 then x nmul fact2 (x-1) else 1
(Nat, Nat) -> Nat
// [fn] declares a non-recursive function // [@(...)] is used in ATS to group arguments for functions of variable arguments fn fact2_usage (cmd: string): void = prerrf ("Usage: %s [integer]\n", @(cmd)) // print an error message implement main (argc, argv) = if argc >= 2 then let val n = int1_of argv.[1] // turning a string into an integer val () = assert_errmsg (n >= 0, "The integer argument needs to be nonnegative.\n") val res = fact2 n in printf ("factorial of %i = %i\n", @(n, res)) end else begin fact2_usage (argv.[0]); exit (1) end
This page is maintained by Hongwei Xi. As always, your comments are welcome.