llvm - 在 Coq 中，为什么要使用 Atom 以及如何构建它？

Question

我目前正在使用 vellvm，对其进行转换。我是 coq 新手。

这是原子实现: http://www.cis.upenn.edu/~plclub/popl08-tutorial/code/coqdoc/Atom.html

例如，在 vellvm 中，原子用作 id 和标签。

我想在一个 llvm 转换中插入一段代码，为此我必须给出一个类型为“atom”的标签。如何构建 Atom 标签？

让我的问题更笼统一些:1) 为什么有人会想要使用 Atom？2)我怎样才能 build 一个？3) 如果我以这种方式构造，我是否会难以考虑原子在代码中的使用方式可能有所不同？

谢谢!

编辑:id 和标签的代码

Definition id := atom. (*r identities *) 
Definition l := atom. (*r labels *)

Answer 1

查看您指向的文件(由 Chargueraud 和 Aydemir 编写)，您了解到原子类型用于表示您可以用来为事物命名的任何类型。

应该使用函数 atom_fresh_for_list 来创建一个新原子。这个函数的类型表明它不仅返回一个任意原子，而且还证明你得到的原子不存在于你作为参数给出的列表中。这就是创建新对象的方式:将所有旧对象放入一个列表中，然后将其作为参数调用函数 atom_fresh_for_list。结果，您获得了类型为 {x : atom | ...}。这不完全是一个原子:它是一个具有更多信息的原子。您可以通过以下方式获取原子:

让 (v, h) := atom_fresh_for_list ... 在 ...

然后，在第二个“...”中，变量 v 包含原子，您可以使用它。如果你需要证明这个原子是一个新原子，那么你可以使用另一个变量 h。

伊夫