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”的含義將在後面解釋。