Check pattern conformance in all MLcase branches (#6)#11
Merged
Conversation
Every constructor branch, including the last one, is now guarded by an
instanceof test instead of casting the final branch unconditionally.
When no branch matches, the generated code calls a new error() helper in
class Main that throws an explicit RuntimeException("non-exhaustive
match"), so a value fitting no constructor no longer surfaces as an
accidental ClassCastException.
Top-level catch-all patterns are handled structurally: Pwild emits its
body as the default of the conditional chain, Prel binds the scrutinee
via let before the body, and Ptuple raises an explicit extraction error
instead of printing invalid Java.
Adds the match_failure test case, whose driver feeds an anonymous
subclass of the extracted interface into a match and asserts that the
failure is the explicit RuntimeException, not a ClassCastException.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
cedretaber
commented
Jul 8, 2026
Comment on lines
+216
to
+221
| let rec split acc = function | ||
| | [] -> List.rev acc, None | ||
| | b :: _ when is_catch_all b -> List.rev acc, Some b (* later branches are unreachable *) | ||
| | b :: rest -> split (b :: acc) rest | ||
| in | ||
| let tests, default = split [] (Array.to_list pv) in |
Author
There was a problem hiding this comment.
自前で split 関数を定義し、「検査のある節」と「デフォルト・フォールバック節」に分けている。
Pwild, Prel 以降は到達しないので無視している。
cedretaber
commented
Jul 8, 2026
| str "class Main {" ++ fnl() ++ fnl() ++ | ||
| str "static <A, B> B let(A val, Function<A, B> cont) { return cont.apply(val); }" ++ | ||
| fnl() ++ fnl() ++ | ||
| str "static <A> A error(String msg) { throw new RuntimeException(msg); }" ++ |
cedretaber
commented
Jul 8, 2026
| let tests, default = split [] (Array.to_list pv) in | ||
| let pp_default = match default with | ||
| | Some b -> pp_catch_all_pat table env scrut b | ||
| | None -> str "error(\"non-exhaustive match\")" |
Author
There was a problem hiding this comment.
パターンマッチの網羅性は Rocq 側で担保しているので、ここには基本的に来ないかも。
ただし、 Java 側の定義を呼び出す FFI を利用するとか、 magic を使うとかしていた場合、あり得るかも？
Self-review found that no test exercised the catch-all code paths: every existing golden match is fully constructor-enumerated, so pp_catch_all_pat was never executed. The new case covers both shapes: a Pwild default (shared branch body not using the matched value) and a Prel default (a compound scrutinee bound to a variable used by the branch body). The driver also documents that a catch-all absorbs values beyond the extracted constructors instead of raising a match failure. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
cedretaber
marked this pull request as ready for review
July 8, 2026 13:57
hiroshi-cl
reviewed
Jul 15, 2026
| | Ptuple l -> "not implemented pattern...", [] | ||
| | Pwild -> "_", [] (* TODO *) | ||
| | Prel n -> Id.to_string (get_db_name n env), [] | ||
| | Ptuple _ -> user_err Pp.(str "Cannot handle tuple patterns in Java yet.") |
hiroshi-cl
reviewed
Jul 15, 2026
Comment on lines
+8
to
+9
| "$self_dir/java-extraction/run-case.sh" match_failure | ||
| "$self_dir/java-extraction/run-case.sh" match_default |
hiroshi-cl
reviewed
Jul 15, 2026
| | Pwild -> "_", [] (* TODO *) | ||
| | Prel n -> Id.to_string (get_db_name n env), [] | ||
| | Ptuple _ -> user_err Pp.(str "Cannot handle tuple patterns in Java yet.") | ||
| | Pwild | Prel _ -> assert false (* catch-all: handled in pp_pat_branches *) |
hiroshi-cl
approved these changes
Jul 15, 2026
This was referenced Jul 15, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
概要
issue #6 の優先度「高」タスクのひとつ:
変更内容
plugins/extraction/java.mlinstanceof検査を付与。 従来は最終分岐だけコメント + 無条件キャストだったため、どのコンストラクタにも適合しない値で偶発的なClassCastExceptionが発生していた。Pwild/Prel)があればそれが default(以降の分岐は到達不能として打ち切り)error("non-exhaustive match")を生成class Mainに失敗ヘルパーを追加:static <A> A error(String msg) { throw new RuntimeException(msg); }— Java のthrowは文であり三項演算子チェーン内に書けないため。将来MLexn/MLaxiomの対応(優先度「中」)でも流用可能な名前にしてある。pp_catch_all_pat):Pwildは body をそのまま、Prelはlet(scrutinee, x -> body)で束縛。従来のPrelは壊れた出力(((x)scrut).x0相当)になり得た。Ptupleは不正な Java 文字列"not implemented pattern..."を出す代わりに明示的な抽出エラー(user_err)を投げる。生成コードの変化(list_reverse の例):
テスト
basic_arithmetic/list_reverse)の golden を再生成。driver は引き続き PASS。match_failureを追加(issue のテスト項目「非網羅 case の動作をテストする」に対応): 3 コンストラクタのcolor型とrotate関数を抽出し、driver がnew Main.color() {}(どのコンストラクタでもない匿名クラス値)を渡すと、ClassCastExceptionではなく素のRuntimeException("non-exhaustive match")が飛ぶことを検証(例外クラスの完全一致 + メッセージの両方をチェック)検証
sh test-suite/misc/java-extraction.shで全 3 ケース PASS(抽出 → golden diff → javac → driver 実行)をローカル確認済みCloses する項目: issue #6 のチェックリスト「
MLcaseの全分岐でパターン適合性を検査する」🤖 Generated with Claude Code