Java extraction backend: 未対応タスク

[hiroshi-cl]

#6 In proof-ninja/rocq の作り直し

優先度: 高

実際の抽出で高頻度に発生し、かつ発生時にコンパイル不能な Java（もしくは重大な正しさの欠陥）を生む項目。

No.	項目	元の優先度	対応内容	発生頻度の実態
1	ローカル MLfix を有効なJava式にする	高	ラムダ本体・let右辺・関数引数など任意の式位置で使用可能な、単一・相互再帰対応のJavaエンコーディング（例: 即時実行ラムダやヘルパーメソッド化）を導入する	occasional。2つの経路がある: ①Gallinaの項中に直接書かれたfix/cofix式は無条件にMLfixになる（extraction.ml:743-746,988-994）。②トップレベルのDfixが「インライン化」された場合にdfix_to_mlfixでローカル化される（modutil.ml:260-274,293-301）。mlutil.ml:1571-1577のinline条件式はto_inline r(明示指定)の他にis_projection/is_recursor/manual_inline/inline_testの論理和だが、inline_test(:1528-1537)自体は「fixpointは自動インライン化しない」設計であり(optim_seが渡すfake_body = MLfix(0,[||],[||])のトリックもこれを担保する)、is_projection/is_recursorも通常Dfixブロックには該当しない。したがって相互再帰するDfixが実際にローカル化されるのは、事実上Extraction Inlineの明示指定、またはWf.Fix/Fix_F等コアライブラリのwell-founded recursionヘルパー(mlutil.ml:1545-1561のホワイトリスト、通常は単一再帰)が中心となる。相互再帰（idsが複数）が生じるのは主に①、またはユーザーが相互再帰FixpointにExtraction Inlineを明示指定した場合に限られ、通常のFixpoint f ... with g ...をトップレベルで書いただけでは発生しない（Dfixのまま）。出現時、現状は宣言・代入・式を式位置に直接並べるため必ず構文不正になる。
2	浅いパターン（Pusual/Prel/Pwild）の正しい処理	高	パターン構造から分岐条件・フィールド参照・変数束縛を生成し、位置番号による束縛をやめる。実際にはネスト/再帰は一切発生しないため「再帰的パターンマッチャー」は不要で、各分岐がPusual/Prel/Pwildのいずれか(常にフラットな1段)であるケースを網羅すればよい	extract_branch（extraction.ml:968）は常に固定でPusualを構築し、Pcons/Ptupleの構築箇所は存在しない。Prel/Pwildはmlutil.ml:1159-1171のfactor_branches最適化(複数分岐が同一コードを生成する場合に1本へ統合)でのみ後から生成される。この最適化(factor_branches)が発動する条件は「複数分岐が構文的に同一のコードへ簡約される」ことであり、Gallinaでワイルドカードを使っただけで自動的に保証されるわけではない。ただし、複数コンストラクタに対して同じ処理をする(ワイルドカードで束縛変数を使わない、あるいは同じ値を返す)典型的な書き方をした場合には現実によく起こりうる。
3	MLcase 全分岐のパターン適合性検査（チェックボックス再オープン要）	高	最終分岐も無条件キャストしない。分岐選択自体はml_branch arrayの要素数(通常は対象inductiveのコンストラクタ数と一致)から抽出時に静的に決まるため、本来は「全分岐にinstanceofを付ける」だけで足りる話であり、実行時に非網羅性を検出する仕組みは別問題として扱う	common。ただし出力自体はコンパイルは通る（構文ブロッカーではない）。Rocqのmatchは本来網羅的にコンパイルされ絶対分岐はMLexnで埋まるため通常は安全なケースが多いが、MLmagic由来の型不一致等と相互作用した場合にサイレントな誤り・素のClassCastExceptionを生みうる。issue自身が完了条件として明記しており、堅牢性/診断品質の観点で高を維持。
4	MLexn/MLaxiom/MLdummy を有効なJavaとして生成する	中	共通の式位置 fail ヘルパー（例外送出式）を導入し、3構文すべてをこのヘルパーで解決する	3構文で頻度は異なる。MLdummyはcommon: Prop消去で日常的に生成される(extraction.ml:777,839,1095,1148,1224-1225)。MLexnはoccasional: 実際の構築箇所は空match=絶対分岐(extraction.ml:933「absurd case」)と、未使用な相互再帰コンポーネントの占位(modutil.ml:393「UNUSED」)の2箇所のみで、MLdummyほど頻出しない。MLaxiomもoccasional〜rare: 本来のAxiom/Admitted由来の生成(extraction.ml:1137)は開発次第で、加えてEvar/Meta(未解決項)に対するフォールバック(extraction.ml:748「evar」)は完全なdevelopmentでは通常発生しないはずの経路。いずれにせよ現状 (error "...")/__/(error "AXIOM...") は未定義Javaで、MLdummyだけでも費用対効果が最も大きい項目。
5	Tvar/Tdummy/Tunknown を有効なJava型として生成する	中	'a 形式や __ をやめ、有効なジェネリクス型変数名（例: T1, T2…）または Object への一律消去のいずれかの方針を決めて生成する	occasional〜common。多相定義・型消去の残存で普通に出現する（extraction.ml:360-400,1027-1032,1074-1077,1124-1133）。現状は不正なJava型であり、出現する定義すべてがコンパイル不能になる。
6	Dtype を実装する	中	Scheme同様に型エイリアスを消去するか、対応するJava宣言（インタフェース等）を生成するかを決定する	occasional。実際の型シノニム定義（Definition foo := ...型）で発生する（extraction.ml:1124-1163）。現状は不正な type のみを出力しファイル全体が構文不正になる。
7	出力ファイルごとに固有のトップレベルクラス名を生成する	低	file_naming が返すモジュール由来のファイル名からクラス名を生成し、class Main 固定をやめる	複数ファイル抽出では常に発生し、issue自身の完了条件（javac *.java の同時成功）を直接ブロックする。修正コストは低く効果は最大級。
8	MLmagic の型安全性を整理する	低	Javaの静的型が食い違う場合にキャストを生成する。型戦略（Tvar系の消去方針）と合わせて設計する	occasional。needs_magic/mgu（mlutil.ml:116-142）がMLレベルの単純型同士の単一化に失敗した箇所（変数参照・定数適用・コンストラクタ適用、extraction.ml:736,821-855,893-919）で挿入される。依存型(添字付き帰納型・依存matchの戻り型・整礎再帰等)を使うコードで発生しやすく、nat/list/option中心の一階関数型コードではほぼ発生しない。注意: skip_typing()(mlutil.ml:133)はlang() == Schemeの場合のみ真であり、Schemeは単一化チェック自体を行わないため構造的にMLmagicが生成されない。Java(table.ml:675)はOCaml/Haskellと同じく単一化チェック対象であり、Schemeのような「構造的に発生しない」対象ではなく実際にMLmagicノードが生成されうる。

---

優先度: 中

発生時は対応が必要だが、**発生頻度が低い（rare-requires-opt-in）**か、内部処理専用で最終出力への到達が稀であるため、実装より先に「明示的な抽出エラーを出す」ことを優先し、実装自体は需要が出てから着手すればよい項目。

No.	項目	元の優先度	対応内容	発生頻度の実態
9	プリミティブ値（MLuint/MLfloat/MLstring/MLparray）の実装	中	まず現状の Prelude.error（不正Java）を明示的な抽出時エラーに置き換える（高優先のfailヘルパーで解決可）。実装（MLstring→String等）は需要が出てから	rare-requires-opt-in。構築箇所はInt/Float/String/Arrayという核項コンストラクタに対応する4行のみ(extraction.ml:760-768)で、Gallinaソースが実際にRocqのネイティブint63/float/string/arrayリテラルを含む場合にのみ生成される(通常はこれらのプリミティブ機能を導入した開発でのみ出現する)。本プロジェクトの .v ファイル（common/theories/Demo.v, variants/proof-ninja/theories/JavaExtractionDemo.v）はいずれも未使用と確認済み。
10	Coinductive の扱いを決める	中	現状の「Javaとして無効な説明文」を明示的な抽出エラーに置き換える。遅延評価（thunk）の実装は需要が出てから	rare-requires-opt-in。本プロジェクトの .v に CoInductive は存在しない。パリティ実装にはthunk/lazinessの設計が必要で相応のコストがかかる。
11	Tmeta/Tvar' の処理	中	assert false を診断可能なエラーメッセージに置き換える	推論フェーズ専用の内部値であり、他バックエンド（OCaml/Haskell/JSON）も同様にassertしている不変条件。最終出力への到達は基本的に想定されない。

---

優先度: 低

miniml.ml の型定義上は存在するが、実際の抽出パイプラインに構築箇所が一つも存在しない（effectively-dead）、または他バックエンドと同一方針で現状維持が妥当な項目。実装は不要で、到達時に明確なエラーを返す程度で十分。

No.	項目	元の優先度	対応内容	発生頻度の実態
12	Ptuple・ネストした Pcons パターン	高	到達時に明示的な抽出エラーを返すのみでよく、再帰的パターンマッチャーの実装は不要	effectively-dead。extraction.ml/mlutil.ml/modutil.ml のいずれにも構築箇所が存在しない。miniml.ml:170-174 自身が「main extraction では未使用、P.N. Tollitte の Relation Extraction プラグイン専用」と明記している。
13	MLtuple の実装	中	到達時に明示的な抽出エラーを返すのみでよい	effectively-dead。構築箇所がなく、通常の prod（ペア型）は普通の帰納型コンストラクタ（MLcons）として抽出される。
14	モジュール変換（MEstruct/MEfunctor/MEident/MEapply/SEmodtype）	低	assert false を診断可能なエラーに置き換える程度に留める	Haskell/Scheme/JSONも同一の「struct平坦化・他は破棄」方針。ident/apply は「extract_env で展開済みのはず」という上流の不変条件があり、到達は異常系。
15	Javaシグネチャ出力（pp_sig）の方針を決める	低	現状の「常に空」を明文化して方針として確定させる	Haskell/Scheme/JSONも同様に空のシグネチャを返しており、パリティ上の欠落ではない。