Emit a benign dummy value for MLdummy (#14)

[cedretaber]

#14 の一部。#17 の完了分です（MLexn/MLaxiom は #13 で対応済み、本 PR が残りの MLdummy)。

MLdummy が MLexn/MLaxiom と異なる理由

MLdummy は論理的内容（Prop）の消去跡に残る値です。MLexn/MLaxiom と違って「実行が到達してはいけない場所」ではなく、抽出後のコードが保持し、引き回し、場合によっては適用すらする正常な実行時値です。したがって throw する式にしてはいけません — さもないと Prop 由来の値に触れるプログラムがクラスロード時に死にます。

• OCaml バックエンドは良性の自己適用可能な値を使う: let __ = let rec f _ = Obj.repr f in Obj.repr f
• Haskell バックエンドの __ = Prelude.error "..." は遅延評価だから成立している
• Java は正格かつ静的型付けなので、「良性の実行時値」と「静的型付けの戦略」の両方が必要

実装

1. MLdummy は __() として出力 — generic メソッド呼び出しは poly expression なので、各出現箇所が文脈（代入・引数・三項演算子の枝など）からターゲット型付けされます。適用引数は OCaml バックエンド同様に破棄します: 抽出コードは純粋で、dummy の自己適用は dummy 自身を返すだけなので、結果に影響しません。
2. class Main にヘルパーを2つ追加（既存の error/let と同じく無条件出力。pp_struct は unsafe_needs を受け取れないため）:

   static final Function<Object, Object> __dummy = new Function<Object, Object>() {
     public Object apply(Object x) { return this; }
   };
   
   @SuppressWarnings("unchecked")
   static <A> A __() { return (A) __dummy; }

   自己適用すると自分自身が返ります — OCaml の __ と同じトリックです。
3. 型位置の Tdummy/Tunknown は Object として出力（従来は不正な Java となる __ を出力していた）。generics によるより精密な型付けは No.5 のスコープで、本 PR では扱いません。
4. keywords に let/error/__/__dummy を追加 — 同名の Coq 識別子が生成ヘルパーと衝突しないよう rename させます（ocaml.ml が __ を予約しているのと同じ流儀。let/error については既存の穴も同時に修正）。

テスト

新規ケース mldummy を追加: Prop 定数（tt_prop : True、both : True /\ True）を直接抽出すると static Object tt_prop = __(); が生成されます。driver では「値が non-null であること（axiom ケースと違いクラスロードで throw しない）」と「dummy が自己適用可能であること」を検証します。既存の golden はヘルパーブロック追加分のみの変更です。全7ケース PASS。

テストがトップレベル定数に限定される理由

「実行時に引数として渡される dummy」（OCaml 出力での konst __ x の形）は、多相関数を Prop で実体化した場合にしか発生しません。その場合は出力される型に Tvar が現れ、generics 未対応（No.5）の現状では Java がコンパイルできないため、テスト不能です。OCaml バックエンドをオラクルとして実験的に確認済み:

• 単相の関数・コンストラクタの Prop 引数は killing signature で完全に消去される（dummy は残らない）
• Extraction Implicit + 部分適用も eta 簡約されて単なる参照になる（dummy は出ない）

したがって「適用される dummy」のシナリオは generics 対応後に初めてテスト可能になります。ヘルパー側はその時に備えて既に良性・自己適用可能に作ってあります。

🤖 Generated with Claude Code

[cedretaber]

使う場合だけ出すようにするのが良さそうだけど、とりあえずは全部出しても良いか。

[cedretaber]

📝 私の理解

• Rocq の関数は証明や型を値と同じように引数として受け取ることができる
  • もちろん、これらはコンパイル時に解決されているはず
  • OCaml や Java に変換されるときに、これらの引数は消えるので、普通は問題にならない
• 問題は generics な引数で、使われ方によって証明・型・値などになる場合
  • その引数が値として利用される場合、その引数は OCaml や Java のコードにも残さないといけないので、単純に消せない
  • しかしこの引数が証明・型になる時、 OCaml や Java では全く無意味なものになる
  • この時に出てくるのが dummy である
• とはいえ、 Rocq のコンパイルが通っている段階で、この変数が「変な使い方」をされることはない
  • というか、実際は、型が Prop に属する場合、関数自体が最適化されて OCaml や Java に変換されたときは中身が消えたりするらしい
  • なので、 dummy は apply できるように作ってあるが、実際のコードでは、 apply されることはなさそう
  • じゃあなんで apply できて、自分自身を返すようになっているかというと、「念のため」らしい
    • ocaml.ml に An [MLdummy] may be applied, but I don't really care. というコメントがある
    • あと An [MLexn] may be applied, but I don't really care. というコメントもあるので、こっちも実際には apply されることはなさそう
  • 仮にコードが残ってしまった場合でも、動作を壊さないようになっているらしい
• で、この dummy が実際にコード中の引数などの位置に現れるには、 generics が必須なのだけど、現在の Java extraction は generics を取り扱えないので、検証不可能
  • テストについても、実際に dummy が出てくるようなコードは確認できていない

例:

Definition twice (A : Type) (f : A -> A) (x : A) : A := f (f x).
Definition weird : True := twice True (fun p => p) I.

というコードがあるとき、 weird は以下のように OCaml に変換される。

let weird = __

この weird は Prop なので、 OCaml 上では何の意味もなく、よって、全体が dummy にされてしまう。
Java への変換でも同じようにしていいはず。

[hiroshi-cl]

特にツッコミどころもなさそう