ats - 如何从 ATS2 中的主函数读入和访问参数？

Question

这是一项常见的基本任务，因此最好了解执行此操作的适当方法。 C++ 中的类似程序可能如下所示 ( ref ):

#include <iostream>
using namespace std;

int main(int argc, char** argv)
{

    for (int i = 0; i < argc; ++i)
        cout << argv[i] << "\n";

    return 0;
}

在此示例中，我们打印出命令行上的每个参数。因此，运行像 ./main.exe asdf 1234 bob 这样的编程会给出:

./main.exe 
asdf 
1234 
bob

Answer 1

这与 C 语言中的同类程序非常相似，但在约束和线性类型方面存在一些差异。一旦设置好，约束就很简单:

(*
Run patscc -o hello hello.dats
*)

#include "share/atspre_staload.hats"

implement main0{n}
(argc, argv): void = {

  fun echoArgs{i:nat | i < n}
  (ii: int(i), argv: !argv(n)): void = {
    val () = println!("arg ", ii, " is ", argv[ii])
    val () = if ii + 1 < argc then echoArgs(ii + 1, argv) 
  }

  val () = echoArgs(0, argv)
}

由于我们需要访问 argv 的内容，因此我们必须通过提供线性相关类型 !argv(n) 来更改其 View 类型的 View ； ! corresponds到 linear logic 中爆炸表明该类型的值在函数调用后仍然可用； (n) 仅表示 argv 是大小为 n 的字符串数组。我们必须保证数组的索引i小于数组的大小n。