私は現在vellvmを使用しており、その上で変換を開発しています。私はcoq初心者です。
これはアトムの実装です：http： //www.cis.upenn.edu/~plclub/popl08-tutorial/code/coqdoc/Atom.html
vellvmでは、たとえば、アトムはIDおよびラベルとして使用されます。
1つのllvm変換にコードのブロックを挿入したいので、そのために「atom」タイプのラベルを付ける必要があります。Atomラベルを作成するにはどうすればよいですか？
私の質問をもう少し一般的に言えば：1）なぜ誰かがAtomを使いたいのですか？2）どうすれば構築できますか？3）このように構成すると、コード内でアトムが異なる方法で使用される可能性があることを考慮して問題が発生しますか？
ありがとう！
編集：IDとラベルのコード
Definition id := atom. (*r identities *)
Definition l := atom. (*r labels *)
（ChargueraudとAydemirによって）指摘したファイルを見ると、アトムタイプは、物に名前を付けるために使用できるすべてのタイプを表すために使用されていることがわかります。
新しいアトムを作成するには、関数atom_fresh_for_listを使用する必要があります。この関数のタイプは、任意のアトムを返すだけでなく、取得したアトムが引数として指定したリストに存在しないことの証明も返すことを示しています。これが新しいものを作成する方法です。古いものをすべてリストに入れ、それを引数として関数atom_fresh_for_listを呼び出します。その結果、タイプ{x：atom|の値を取得します。...}。これは正確にはアトムではありません。より多くの情報を持つアトムです。次のように書くことで、アトムを手に入れることができます。
let（v、h）：= atom_fresh_for_list ...in..。
次に、2番目の「...」で変数vにアトムが含まれているため、それを使用できます。このアトムが新しいアトムであることを証明する必要がある場合は、他の変数hを使用できます。
イヴ
イブは部分的に答えることができましたが、原子を構築する方法の例がありません. projT1 を使用する必要があります。このためのコードは次のとおりです。
Definition an_atom : atom := (projT1 (atom_fresh_for_list nil)).
nil は任意のリストです。