ATS：使用定理证明进行编程/安装和操作 ATS 编译器

安装 ATS

注意：这些说明已在 Ubuntu Linux 上测试过，其他发行版可能需要进行修改。

在 Linux 上，第一步是 下载当前 ATS 编译器 ATS/Anairiats 的稳定版本。文件名应类似于“ats-lang-anairiats-x.x.x.tar.gz”，其中“x.x.x”代表版本号。然后您可以将其安装到 /usr/share/atshome/ 或您主目录下的某个目录中。

安装到 /usr/share/atshome/

打开终端并调用

sudo tar xvzf ats-lang-anairiats-x.x.x.tar.gz /

现在将此添加到环境中

ATSHOME=/usr/share/atshome
export ATSHOME
ATSHOMERELOC=ATS-x.x.x
export ATSHOMERELOC
PATH=$ATSHOME/bin:$PATH
export PATH

安装到主目录

如果您选择安装到其他目录，例如 ~/FOO，请先解压缩到某个临时目录

tar xvzf ats-lang-anairiats-x.x.x.tar.gz /tmp

然后将 /tmp/usr/share/atshome 移动到 ~/FOO

mv /tmp/usr/share/atshome ~/FOO

然后将以下内容添加到 ~/.bashrc

ATSHOME=~/FOO/atshome
export ATSHOME
ATSHOMERELOC=ATS-x.x.x
export ATSHOMERELOC
PATH=$ATSHOME/bin:$PATH
export PATH

需要解释这两个环境变量的含义。两者都假定不为空。

• ATSHOME 是 ATS 安装目录的绝对路径
• ATSHOMERELOC 是已安装 ATS 编译器的版本，用于在生成的代码中进行名称混淆

第一个程序

为了测试，请在您喜欢的文本编辑器中写入以下内容

implement main () = print "hello, world!\n"

并将其保存到名为 hello.dats 的文件中。然后请发出以下命令行

atscc -o hello hello.dats

如果一切顺利，那么 ./hello 就是一个新生成的可执行文件，当执行时，它应该将字符串“Hello, world!”和一个换行符打印到控制台上。

文件扩展名

您将感兴趣的两种主要文件类型

• 包含模块接口的文件，扩展名为 .sats（第一个字母来自“statics”）
• 包含接口实现的文件，扩展名为 .dats（第一个字母来自“dynamics”）

“statics”和“dynamics”的含义将在后面解释。