6

Coq から抽出された Ocaml コードには、(場合によっては)次のように定義された型__と関数が含まれています。__

type __ = Obj.t
let __ = let rec f _ = Obj.repr f in Obj.repr f

ドキュメントによると、過去にはそのような型は として定義されていたunit(したがって、 と見なす__ことができた) が、 typeの値が type の値に適用される()(まれな) ケースが存在します。____

__は OCaml のモジュールの文書化されていない関数を使用しますが、Obj定義されているのは本質的にすべての引数 (その数に関係なく) を食べる完全にポリモーフィックな関数のようです。

__を削除できず、このタイプの値が同じタイプの値に適用されるケースに関するドキュメントはありますか? ） 視点？

4

1 に答える 1

3

READMEで引用されている参考文献は、消去の問題の概要を示しています。具体的には、このレポートとこの記事の両方で、型スキーマと CIC 用語の論理部分がどのように消去されるか、およびなぜ__ x = __. 問題は__、それ自体に適用される可能性があるということではなく、何にでも適用される可能性があるということです。

残念ながら、この行動が病的でない場合に重要であるかどうかはまったく明らかではありません. そこに与えられた動機は、任意のCoq 用語を抽出できるようにすることであり、ドキュメントには、実際の観点から本当に興味深いケースについては言及されていません。3で与えられた例はこれです:

Definition foo (X : Type) (f : nat -> X) (g : X -> nat) := g (f 0).
Definition bar := foo True (fun _ => I).

を実行Recursive Extraction bar.すると、次の結果が得られます。

type __ = Obj.t
let __ = let rec f _ = Obj.repr f in Obj.repr f

type nat =
| O
| S of nat

(** val foo : (nat -> 'a1) -> ('a1 -> nat) -> nat **)

let foo f g =
  g (f O)

(** val bar : (__ -> nat) -> nat **)

let bar =
  foo (Obj.magic __)

fooは でポリモーフィックであるためType、アプリケーションの本体を単純化する方法はありませんf O。計算コンテンツが含まれる可能性があるからです。ただし、Propは のサブタイプであるためType、 にfooも適用できます。Trueこれは で発生しbarます。barしたがって、 を減らそうとすると、__に適用されることになりOます。

この特定のケースは、完全にインライン化できるため、あまり興味深いものではありませんfoo。

let bar g =
  g __

Trueは何にも適用できないため、法的な Coq 用語に対応する場合、gその__引数も何にも適用されないため、安全に使用できます__ = ()(私は信じています)。ただし、消去された用語をさらに適用できるかどうかを事前に知ることができない場合があり、これが__必要性の一般的な定義になります。たとえば、ファイルの末尾近くにあるこちらFunの例を確認してください。

于 2013-04-07T21:13:58.817 に答える