wip: compilable java extract

[hiroshi-cl]

とりあえず雑にclaude codeにコンパイルだけはできるようにしてもらった

問題	修正
import java.util.function.Function; が未出力	preamble で import だけ出力するよう変更
class Main { } が閉じられない	pp_struct 側でクラスの開閉と let ヘルパを出力
コンストラクタに new がない（S(...) → new S(...)）	MLcons の (* str "new " ++ *) を有効化
パターン束縛変数が未定義プレースホルダ（__S_n'_dot_S0）になる	pp_one_pat を書き換え、let(((S)scrutinee).S0, n$ -> body) 形式でフィールドアクセスを生成
識別子に ' が残り Java で不正	MLrel・MLletin・pp_fix を Id.print → pr_id（'→$ 変換）に変更
再帰フィールド初期化子の自己参照エラー	Dfix をフィールド宣言 + インスタンス初期化ブロック { add = ...; mul = ...; } に分離

[hiroshi-cl]

Codex によるレビュー結果

1. 変更の概要

差分は主に以下を修正しています。

• Function の import と Main クラスの閉じ括弧を正しく生成。
• ローカル識別子中の ' を $ に変換。
• コンストラクタ式に new を追加。
• MLfix の代入に欠けていた = を追加。
• パターン変数をコンストラクタのフィールドから let で束縛。
• Dfix を「フィールド宣言」と「初期化ブロック」に分離。

---

2. 各変更の正しさの検証

preamble / pp_struct

• OCaml型: Pp.t の連結として正しい。
• MiniML: 出力の外枠だけなので意味への影響はない。
• Java: Function の import が追加され、Main の } も生成されるため正しい。Main が非 public なのでファイル名と一致しなくても問題ない。

pr_id の適用

• OCaml型: Id.print と同様に Pp.t を返すため正しい。
• MiniML: 名前の表記だけを変え、束縛関係は変えない。
• Java: Rocq由来の ' は Java 識別子に使えないため、$ への変換は必須の修正。

コンストラクタへの new

• OCaml型: 正しい。
• MiniML: MLcons を新しいコンストラクタ値の生成として表現しており妥当。
• Java: クラスのコンストラクタ呼び出しには new が必要なので必須の修正。

MLfix の =

• OCaml型: 正しい。
• Java: 以前の fi expr は無効だったため、fi = expr 自体は正しい修正。ただし MLfix 全体の出力形式には後述の未解決問題がある。

パターン変数の束縛

• OCaml型: ids' は Id.t list、wrapped は Pp.t となり整合している。
• MiniML: push_vars (List.rev_map id_of_mlid ids) によって ids'[j] がフィールド j の名前になるため、env' で生成した本体と各フィールド束縛は一致する。List.fold_right により field 0 が外側になり、Java では field 0、1、…の順に評価される。
• Java: ((Constr) exp).Constr_j と let(value, x -> body) は有効であり、生成例の let(((S)n).S0, n$ -> ...) も妥当。

Dfix

• OCaml型: rv、defs、ty の対応を添字で扱っており、Dfix の配列長不変条件の下では正しい。
• MiniML: 全フィールドを宣言してから各定義を代入するため、再帰参照可能な環境を作るという意図に合う。
• Java: f = ...f... をフィールド宣言時初期化からインスタンス初期化ブロックへ移すことで、illegal self-reference を回避できる。相互再帰についても全宣言が初期化ブロックより前にあるため名前解決上は正しい。

---

3. 残っている問題・考慮漏れのエッジケース

🔴 重要: case の被検査式が複数回評価される

exp は各 instanceof と各フィールド参照で再出力される。複数フィールドを持つコンストラクタでは同じ式を何度も評価することになる。純粋で決定的な MiniML 式なら問題ないが、custom extraction や外部関数に副作用がある場合、MiniML の「scrutinee を一度評価する」意味を保存しない。case 全体の前で scrutinee を一度 let 束縛する修正が必要。

🔴 重要: MLfix は依然として一般的な Java 式ではない

最初の定義には var がなく、出力全体が「宣言・文・最後の式」の並びである。Java にはこの形式のブロック式がないため、MLfix がラムダ本体や引数位置に現れるとコンパイルできない可能性が高い。今回の = 追加だけでは一般のローカル fix を処理できない。

🟡 中: 一般パターンに対応していない

pp_gen_pat を捨てて全束縛変数をトップレベルの Constr_j に割り当てているため、Pcons の深いパターンではネストしたフィールド位置を表現できない。Pwild や Prel も未対応のままである。

🟡 中: 最終分岐の型検査を省略している

最後の分岐は無条件にキャストして本体を実行する。通常の網羅的な Pusual 分岐では成立するが、非網羅的・一般パターン・将来の分岐変換では ClassCastException になり得る。

🟢 低: 複数ファイルを同時コンパイルできない

すべての出力が同一パッケージの class Main を定義するため、各ファイルを個別にコンパイルすることは可能でも、javac *.java では duplicate class エラーになる。ファイル単位の固有クラス名が必要。