Emit valid Java for MLexn and MLaxiom (#6) by cedretaber · Pull Request #13 · proof-ninja/rocq

cedretaber · 2026-07-15T18:40:15Z

概要

issue #6(および優先度再評価レポートの No.4 前半 + No.9 前半 + No.12)への対応です。

MLexn / MLaxiom は現在 OCaml バックエンドのコピーのまま (error "absurd case") という Java として不正な出力を生成していました。両者は「実行が到達してはいけない場所」を表すので、#11 で導入した class Main の汎用ヘルパー error()(この合流を見越して命名)への合流が正しい意味論です。

変更内容

MLexn → error("absurd case") などの有効な Java 式(適用引数は従来どおり捨てる: error() は適用前に throw するので健全。.apply を付けると receiver 位置は poly context でないため型推論が壊れる)
MLaxiom → error("AXIOM TO BE REALIZED (axiom.mystery)")
pp_java_string 新設: Java 文字列リテラル用エスケープ(Pp.qs は OCaml 用エスケープなので不可)
Pcons(深いパターン) → user_err による抽出時の明示エラー。従来はサブパターンを無視して位置束縛するため「黙って間違った Java」を生成し得ました。main extraction に構築箇所がない effectively-dead 構文(レポート No.12)なので実装せずエラー化が正解です
MLuint/MLfloat/MLstring/MLparray → user_err(レポート No.9 前半)。従来は Haskell の Prelude.error をコピーした不正 Java を出力していました

MLdummy を本 PR に含めなかった理由

Issue / レポートは「共通の式位置 fail ヘルパーで MLexn/MLaxiom/MLdummy の3構文すべてを解決する」という処方ですが、MLdummy にはこの処方が当てはまりません。

MLdummy は Prop 消去の跡地に残るプレースホルダで、正常実行中に引き回され・適用までされる無害な値です。他バックエンドの実装がこれを裏付けます:

OCaml: let __ = let rec f _ = Obj.repr f in Obj.repr f(適用すると自分を返す値)
Scheme: (define __ (lambda (_) __))(同上)
Haskell: __ = Prelude.error "..."(エラーだが遅延評価なので触れない限り無害)

Java は正格評価かつ static フィールドは即時初期化なので、MLdummy を throw 式にすると Prop を使うほぼすべてのプログラムがクラスロード時に死にます(現状のコンパイルエラーより発見しにくい壊れ方への悪化)。正しい対応は OCaml/Scheme 型の「適用可能で自分を返す値」を定義することで、型整合(レポート No.5)・キャスト戦略(No.8)・条件付きプリアンブル出力(他バックエンドの usf.mldummy 相当)を含む設計タスクになるため、専用の PR に分離しました。本 PR では str "__" のまま据え置き、TODO コメントで経緯を明記しています。

テスト

新規2ケース(sh test-suite/misc/java-extraction.sh で全6ケース PASS、既存 golden への diff なし):

absurd_match: 空帰納型への match(→ MLexn "absurd case")。driver で実行時に素の RuntimeException("absurd case")(偶発的な例外でない)ことを検証。なお、パラメータを直接 absurd match すると未使用引数がダミー束縛 _ として抽出され、_ をラムダ引数に使えるのは JDK 22+ のため CI で javac が通らない恐れがあります。コンストラクタ2つの型で包んで absurd match を分岐内に置く形にし、.v にコメントで理由を残しています
axiom: 未実現 axiom(→ MLaxiom)。static 初期化子が throw するため、driver は ExceptionInInitializerError を catch して cause が RuntimeException("AXIOM TO BE REALIZED (axiom.mystery)") であることを検証

user_err 経路(primitives / Pcons)は「抽出が失敗すること」を期待するケースをハーネスがサポートしていないため自動テスト化していません(ハーネス拡張は別タスク)。primitives は手動確認済みです:

$ rocq c prim_uint.v   # Definition x := 42%uint63.
Error: Cannot handle primitive integers in Java yet.

🤖 Generated with Claude Code

MLexn and MLaxiom were printed OCaml-style ((error "...")), which is not valid Java. Both mark places execution must never reach, so route them to the existing generic error() helper in class Main, with a proper Java string literal escaper (Pp.qs escapes for OCaml, not Java). Constructs the main extraction pipeline never produces, or that we refuse to extract for now, become explicit extraction-time errors instead of invalid Java output: deep Pcons patterns (previously bound fields positionally while silently ignoring the sub-patterns) and the four primitive constructs MLuint/MLfloat/MLstring/MLparray (previously emitted Haskell's Prelude.error). MLdummy is intentionally left as-is: it is a benign placeholder produced by Prop erasure that is passed around and applied at runtime, so unlike MLexn/MLaxiom it must not become a throwing expression. Making it valid Java needs a self-returning applicable value plus type-strategy decisions, and is deferred to a dedicated PR. New scripted test cases: absurd_match (empty-inductive match reaches the explicit "absurd case" error at runtime) and axiom (an unrealized axiom fails class initialization with the AXIOM TO BE REALIZED message). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

cedretaber · 2026-07-15T19:25:59Z

+Extraction Language Java.
+Set Extraction Output Directory "misc/java-extraction/_generated/absurd_match".
+
+Inductive empty : Set := .


これ有効な Rocq コードなんだ 👀

cedretaber · 2026-07-15T19:29:00Z

+Definition from_shape (s : shape) : result :=
+  match s with
+  | Leaf => Ok
+  | Wrap e => match e with end


match は全てのコンストラクタを網羅していないといけないけど、 empty 型はコンストラクタが0個なので、これで有効な match 式になる。
そして爆発律によってあらゆる型になれる（ ex falso quodlibet ）。

cedretaber · 2026-07-15T19:31:52Z

+   is not a valid lambda parameter name on every supported JDK. *)
+Inductive shape :=
+| Leaf : shape
+| Wrap : empty -> shape.


empty 型にはコンストラクタが無いから、 Rocq の世界では、そもそも Wrap は作れないはず。

cedretaber · 2026-07-15T19:32:36Z

+
+    // A [match] on an empty inductive type has no branches; reaching it must
+    // raise the explicit absurd-case error, not an accidental exception.
+    Main.shape absurd = new Main.Wrap(new Main.empty() {});


Rocq の世界では存在しないものを、テストのために、 Java の世界で無理矢理作り出す。

cedretaber · 2026-07-15T19:33:35Z

+        str "__" (* TODO: define a benign applicable [__] value (separate PR);
+                    an [MLdummy] is passed around and applied at runtime, so
+                    it must NOT become a throwing expression. *)


別 RP で対応予定。

cedretaber · 2026-07-15T19:34:33Z

    | MLexn s ->
-        (* An [MLexn] may be applied, but I don't really care. *)
-        paren (str "error " ++ qs s)
+        (* Applied arguments are dropped: [error] throws before any
+           application could happen, and the surrounding context supplies the
+           expected result type for the generic return. *)
+        str "error" ++ paren (pp_java_string s)


コード上は出現するが到達不可能。
（テストを見るとどういう場合に出てくるか分かりやすいかも。）

cedretaber · 2026-07-15T19:38:43Z

+let pp_gen_pat table = function
+  | Pusual r -> pp_global_name table Cons r


Pusual 以外出てこないはずなのでかなり簡素化できている。

hiroshi-cl · 2026-07-15T23:08:16Z

+  let buf = Buffer.create (String.length s + 2) in
+  Buffer.add_char buf '"';
+  String.iter (fun c -> match c with
+    | '"'  -> Buffer.add_string buf "\\\""


Buffer.add_charありそうだからそれを使ったほうが素直そう

確かに、下手にエスケープして見辛くなるよりそちらの方がいいかも？

{||} リテラル使ってエスケープ不要にしました。

hiroshi-cl · 2026-07-15T23:12:05Z

+    | c when Char.code c < 0x20 ->
+        Buffer.add_string buf (Printf.sprintf "\\u%04x" (Char.code c))
+    | c -> Buffer.add_char buf c) s;
+  Buffer.add_char buf '"';


こっちはadd_char

Review feedback on #13: the double-escaped OCaml literals ("\\\"", "\\n", ...) needed mental unescaping to see the Java escape sequence they emit. With {|...|} quoted strings the source shows the emitted sequence verbatim. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

cedretaber self-assigned this Jul 15, 2026

cedretaber requested a review from hiroshi-cl July 15, 2026 19:09

cedretaber marked this pull request as ready for review July 15, 2026 19:09

cedretaber commented Jul 15, 2026

View reviewed changes

hiroshi-cl reviewed Jul 15, 2026

View reviewed changes

cedretaber mentioned this pull request Jul 16, 2026

4. MLexn/MLaxiom/MLdummy を有効なJavaとして生成する #17

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Emit valid Java for MLexn and MLaxiom (#6)#13

Emit valid Java for MLexn and MLaxiom (#6)#13
cedretaber wants to merge 2 commits into
java_extractionfrom
feat/java-exn-axiom

cedretaber commented Jul 15, 2026

Uh oh!

cedretaber Jul 15, 2026

Uh oh!

cedretaber Jul 15, 2026

Uh oh!

cedretaber Jul 15, 2026

Uh oh!

cedretaber Jul 15, 2026

Uh oh!

cedretaber Jul 15, 2026

Uh oh!

cedretaber Jul 15, 2026

Uh oh!

cedretaber Jul 15, 2026

Uh oh!

hiroshi-cl Jul 15, 2026

Uh oh!

cedretaber Jul 16, 2026

Uh oh!

cedretaber Jul 16, 2026

Uh oh!

hiroshi-cl Jul 15, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

		let pp_gen_pat table = function
		\| Pusual r -> pp_global_name table Cons r

Uh oh!

Conversation

cedretaber commented Jul 15, 2026

概要

変更内容

MLdummy を本 PR に含めなかった理由

テスト

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants