From c943f0fe97b434796437bf717bf44fb4cd5185ff Mon Sep 17 00:00:00 2001 From: cedretaber Date: Wed, 8 Jul 2026 21:53:47 +0900 Subject: [PATCH 1/2] Check pattern conformance in all MLcase branches (#6) 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 --- plugins/extraction/java.ml | 54 ++++++++++++++----- test-suite/misc/java-extraction.sh | 1 + .../java_arithmetic_demo.java.expected | 11 ++-- .../java_constants_demo.java.expected | 2 + .../java_list_reverse.java.expected | 17 +++--- .../misc/java-extraction/match_failure.v | 19 +++++++ .../match_failure/DriverMatchFailure.java | 29 ++++++++++ .../java_match_failure.java.expected | 38 +++++++++++++ 8 files changed, 148 insertions(+), 23 deletions(-) create mode 100644 test-suite/misc/java-extraction/match_failure.v create mode 100644 test-suite/misc/java-extraction/match_failure/DriverMatchFailure.java create mode 100644 test-suite/misc/java-extraction/match_failure/java_match_failure.java.expected diff --git a/plugins/extraction/java.ml b/plugins/extraction/java.ml index 293d8a3dc4f8..f85a23e361c6 100644 --- a/plugins/extraction/java.ml +++ b/plugins/extraction/java.ml @@ -91,9 +91,8 @@ let pp_ids_pat table ids env = function let pp_gen_pat table ids env = function | Pcons (r, l) -> pp_global_name table Cons r, (List.map (pp_ids_pat table ids env) l) | Pusual r -> pp_global_name table Cons r, (List.map Id.print ids) - | 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.") + | Pwild | Prel _ -> assert false (* catch-all: handled in pp_pat_branches *) let rec pp_expr table env args = let apply st = pp_app st args in @@ -175,9 +174,23 @@ and pp_one_pat table env exp (ids,p,t) = in str constr, wrapped -(* TODO: the last branch is cast unconditionally; a non-exhaustive match would - raise a bare ClassCastException instead of an explicit extraction error. *) -and pp_pat table env t pv = (* TODO : How about wildcard / Prel at top level? *) +(* A top-level [Pwild] or [Prel] matches unconditionally, so it cannot (and + need not) be tested with [instanceof]: its body is the default of the + conditional chain. [Prel] additionally binds the scrutinee to a variable. *) +and pp_catch_all_pat table env scrut (ids,p,t) = + match p with + | Pwild -> + assert (List.is_empty ids); + pp_expr table env [] t + | Prel _ -> + let ids', env' = push_vars (List.rev_map id_of_mlid ids) env in + let body = pp_expr table env' [] t in + (match ids' with + | [id] -> pp_letin (pr_id id) scrut body + | _ -> assert false) + | _ -> assert false + +and pp_pat table env t pv = let exp = pp_expr table env [] t in match t with | MLrel _ | MLglob _ -> @@ -194,13 +207,28 @@ and pp_pat table env t pv = (* TODO : How about wildcard / Prel at top level? *) let scrut = pr_id scrut_id in pp_letin scrut exp (pp_pat_branches table env scrut pv) +(* Every constructor branch (including the last one) is guarded by an + [instanceof] test; the chain ends with the first catch-all branch if any, + otherwise with an explicit match-failure so that a value fitting no branch + raises a clear error instead of an accidental ClassCastException. *) and pp_pat_branches table env scrut pv = - prvecti - (fun i x -> - let constr, body = pp_one_pat table env scrut x in - if Int.equal i (Array.length pv - 1) then hv 2 (pp_comment (scrut ++ str " instanceof " ++ constr) ++ body) - else hv 2 (paren (scrut ++ str " instanceof " ++ constr) ++ str " ? " ++ body) ++ fnl() ++ str ": ") - pv + let is_catch_all (_,p,_) = match p with Pwild | Prel _ -> true | _ -> false in + 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 + let pp_default = match default with + | Some b -> pp_catch_all_pat table env scrut b + | None -> str "error(\"non-exhaustive match\")" + in + prlist_strict + (fun b -> + let constr, body = pp_one_pat table env scrut b in + hv 2 (paren (scrut ++ str " instanceof " ++ constr) ++ str " ? " ++ body) ++ fnl() ++ str ": ") + tests ++ + hv 2 pp_default (* TODO : almost all of definitions below are from ocaml.ml *) let str_global_with_key table k key r = @@ -378,6 +406,8 @@ let pp_struct table = str "class Main {" ++ fnl() ++ fnl() ++ str "static B let(A val, Function cont) { return cont.apply(val); }" ++ fnl() ++ fnl() ++ + str "static A error(String msg) { throw new RuntimeException(msg); }" ++ + fnl() ++ fnl() ++ prlist_strict pp_sel structure ++ str "}" ++ fnl() diff --git a/test-suite/misc/java-extraction.sh b/test-suite/misc/java-extraction.sh index a8ee57d9283d..446adccb939a 100755 --- a/test-suite/misc/java-extraction.sh +++ b/test-suite/misc/java-extraction.sh @@ -5,3 +5,4 @@ self_dir=$(CDPATH= cd -- "$(dirname -- "$0")" && pwd) "$self_dir/java-extraction/run-case.sh" basic_arithmetic "$self_dir/java-extraction/run-case.sh" list_reverse +"$self_dir/java-extraction/run-case.sh" match_failure diff --git a/test-suite/misc/java-extraction/basic_arithmetic/java_arithmetic_demo.java.expected b/test-suite/misc/java-extraction/basic_arithmetic/java_arithmetic_demo.java.expected index e34a46c46025..d9dbee39c35a 100644 --- a/test-suite/misc/java-extraction/basic_arithmetic/java_arithmetic_demo.java.expected +++ b/test-suite/misc/java-extraction/basic_arithmetic/java_arithmetic_demo.java.expected @@ -4,6 +4,8 @@ class Main { static B let(A val, Function cont) { return cont.apply(val); } +static A error(String msg) { throw new RuntimeException(msg); } + public interface nat {} public static class O implements nat { @@ -25,8 +27,8 @@ static Function> add; static { add = n -> m -> (n instanceof O) ? m -: // n instanceof S - let(((S)n).S0, n$ -> new S(add.apply(n$).apply(m))) +: (n instanceof S) ? let(((S)n).S0, n$ -> new S(add.apply(n$).apply(m))) +: error("non-exhaustive match") ; } @@ -37,8 +39,9 @@ static Function> mul; static { mul = n -> m -> (n instanceof O) ? new O() -: // n instanceof S - let(((S)n).S0, n$ -> add.apply(m).apply(mul.apply(n$).apply(m))) +: (n instanceof S) ? let(((S)n).S0, n$ -> + add.apply(m).apply(mul.apply(n$).apply(m))) +: error("non-exhaustive match") ; } diff --git a/test-suite/misc/java-extraction/basic_arithmetic/java_constants_demo.java.expected b/test-suite/misc/java-extraction/basic_arithmetic/java_constants_demo.java.expected index 3267a034390b..4dc893768203 100644 --- a/test-suite/misc/java-extraction/basic_arithmetic/java_constants_demo.java.expected +++ b/test-suite/misc/java-extraction/basic_arithmetic/java_constants_demo.java.expected @@ -4,6 +4,8 @@ class Main { static B let(A val, Function cont) { return cont.apply(val); } +static A error(String msg) { throw new RuntimeException(msg); } + public interface nat {} public static class O implements nat { diff --git a/test-suite/misc/java-extraction/list_reverse/java_list_reverse.java.expected b/test-suite/misc/java-extraction/list_reverse/java_list_reverse.java.expected index 1cb7f3b5dfef..f9016cb2e9df 100644 --- a/test-suite/misc/java-extraction/list_reverse/java_list_reverse.java.expected +++ b/test-suite/misc/java-extraction/list_reverse/java_list_reverse.java.expected @@ -4,6 +4,8 @@ class Main { static B let(A val, Function cont) { return cont.apply(val); } +static A error(String msg) { throw new RuntimeException(msg); } + public interface nat {} public static class O implements nat { @@ -45,9 +47,10 @@ app; static { app = l1 -> l2 -> (l1 instanceof Nil) ? l2 -: // l1 instanceof Cons - let(((Cons)l1).Cons0, x -> - let(((Cons)l1).Cons1, xs -> new Cons(x, app.apply(xs).apply(l2)))) +: (l1 instanceof Cons) ? let(((Cons)l1).Cons0, x -> + let(((Cons)l1).Cons1, xs -> + new Cons(x, app.apply(xs).apply(l2)))) +: error("non-exhaustive match") ; } @@ -55,10 +58,10 @@ static Function reverse; static { reverse = l -> (l instanceof Nil) ? new Nil() -: // l instanceof Cons - let(((Cons)l).Cons0, x -> - let(((Cons)l).Cons1, xs -> - app.apply(reverse.apply(xs)).apply(new Cons(x, new Nil())))) +: (l instanceof Cons) ? let(((Cons)l).Cons0, x -> + let(((Cons)l).Cons1, xs -> + app.apply(reverse.apply(xs)).apply(new Cons(x, new Nil())))) +: error("non-exhaustive match") ; } diff --git a/test-suite/misc/java-extraction/match_failure.v b/test-suite/misc/java-extraction/match_failure.v new file mode 100644 index 000000000000..33f37075d769 --- /dev/null +++ b/test-suite/misc/java-extraction/match_failure.v @@ -0,0 +1,19 @@ +Require Corelib.extraction.Extraction. + +Extraction Language Java. +Set Extraction Output Directory "misc/java-extraction/_generated/match_failure". + +Inductive color := +| Red : color +| Green : color +| Blue : color. + +Definition rotate (c : color) : color := + match c with + | Red => Green + | Green => Blue + | Blue => Red + end. + +Extraction "java_match_failure.java" + rotate. diff --git a/test-suite/misc/java-extraction/match_failure/DriverMatchFailure.java b/test-suite/misc/java-extraction/match_failure/DriverMatchFailure.java new file mode 100644 index 000000000000..819dd4a3619e --- /dev/null +++ b/test-suite/misc/java-extraction/match_failure/DriverMatchFailure.java @@ -0,0 +1,29 @@ +public class DriverMatchFailure { + static void assertRotate(Main.color input, Class expected) { + Main.color actual = Main.rotate.apply(input); + if (!expected.equals(actual.getClass())) { + throw new AssertionError("expected " + expected.getName() + " but got " + actual.getClass().getName()); + } + } + + public static void main(String[] args) { + assertRotate(new Main.Red(), Main.Green.class); + assertRotate(new Main.Green(), Main.Blue.class); + assertRotate(new Main.Blue(), Main.Red.class); + + // A value that fits no constructor of the inductive type must raise the + // explicit match failure, not an accidental ClassCastException. + Main.color alien = new Main.color() {}; + try { + Main.rotate.apply(alien); + throw new AssertionError("expected a match failure but rotate returned normally"); + } catch (RuntimeException e) { + if (!RuntimeException.class.equals(e.getClass())) { + throw new AssertionError("expected a plain RuntimeException but got " + e.getClass().getName(), e); + } + if (!"non-exhaustive match".equals(e.getMessage())) { + throw new AssertionError("unexpected match failure message: " + e.getMessage(), e); + } + } + } +} diff --git a/test-suite/misc/java-extraction/match_failure/java_match_failure.java.expected b/test-suite/misc/java-extraction/match_failure/java_match_failure.java.expected new file mode 100644 index 000000000000..c13a3d81fda2 --- /dev/null +++ b/test-suite/misc/java-extraction/match_failure/java_match_failure.java.expected @@ -0,0 +1,38 @@ +import java.util.function.Function; + +class Main { + +static B let(A val, Function cont) { return cont.apply(val); } + +static A error(String msg) { throw new RuntimeException(msg); } + +public interface color {} +public static class Red implements color { + + Red() { + } + + } + +public static class Green implements color { + + Green() { + } + + } + +public static class Blue implements color { + + Blue() { + } + + } + +static Function rotate = c -> + (c instanceof Red) ? new Green() + : (c instanceof Green) ? new Blue() + : (c instanceof Blue) ? new Red() + : error("non-exhaustive match") + ; + +} From 520059cb5da6aac210bcf7752b20ddd8863b264e Mon Sep 17 00:00:00 2001 From: cedretaber Date: Wed, 8 Jul 2026 22:40:44 +0900 Subject: [PATCH 2/2] Add match_default test covering catch-all branches 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 --- test-suite/misc/java-extraction.sh | 1 + .../misc/java-extraction/match_default.v | 29 +++++++++++++ .../match_default/DriverMatchDefault.java | 27 ++++++++++++ .../java_match_default.java.expected | 42 +++++++++++++++++++ 4 files changed, 99 insertions(+) create mode 100644 test-suite/misc/java-extraction/match_default.v create mode 100644 test-suite/misc/java-extraction/match_default/DriverMatchDefault.java create mode 100644 test-suite/misc/java-extraction/match_default/java_match_default.java.expected diff --git a/test-suite/misc/java-extraction.sh b/test-suite/misc/java-extraction.sh index 446adccb939a..5c8fd005d842 100755 --- a/test-suite/misc/java-extraction.sh +++ b/test-suite/misc/java-extraction.sh @@ -6,3 +6,4 @@ self_dir=$(CDPATH= cd -- "$(dirname -- "$0")" && pwd) "$self_dir/java-extraction/run-case.sh" basic_arithmetic "$self_dir/java-extraction/run-case.sh" list_reverse "$self_dir/java-extraction/run-case.sh" match_failure +"$self_dir/java-extraction/run-case.sh" match_default diff --git a/test-suite/misc/java-extraction/match_default.v b/test-suite/misc/java-extraction/match_default.v new file mode 100644 index 000000000000..79e220ae477a --- /dev/null +++ b/test-suite/misc/java-extraction/match_default.v @@ -0,0 +1,29 @@ +Require Corelib.extraction.Extraction. + +Extraction Language Java. +Set Extraction Output Directory "misc/java-extraction/_generated/match_default". + +Inductive color := +| Red : color +| Green : color +| Blue : color. + +(* The shared default branch factorizes to a Pwild catch-all: its body does + not use the matched value. *) +Definition default_to_red (c : color) : color := + match c with + | Red => Green + | _ => Red + end. + +(* The scrutinee is a compound expression and the default branch uses the + matched value, so it factorizes to a Prel catch-all binding the scrutinee + to a variable. *) +Definition normalize (c : color) : color := + match default_to_red c with + | Red => Green + | other => other + end. + +Extraction "java_match_default.java" + default_to_red normalize. diff --git a/test-suite/misc/java-extraction/match_default/DriverMatchDefault.java b/test-suite/misc/java-extraction/match_default/DriverMatchDefault.java new file mode 100644 index 000000000000..a4ed5305de0b --- /dev/null +++ b/test-suite/misc/java-extraction/match_default/DriverMatchDefault.java @@ -0,0 +1,27 @@ +public class DriverMatchDefault { + static void assertColor(String label, Main.color actual, Class expected) { + if (!expected.equals(actual.getClass())) { + throw new AssertionError(label + ": expected " + expected.getName() + " but got " + actual.getClass().getName()); + } + } + + public static void main(String[] args) { + // default_to_red: Red => Green | _ => Red (Pwild catch-all) + assertColor("default_to_red(Red)", Main.default_to_red.apply(new Main.Red()), Main.Green.class); + assertColor("default_to_red(Green)", Main.default_to_red.apply(new Main.Green()), Main.Red.class); + assertColor("default_to_red(Blue)", Main.default_to_red.apply(new Main.Blue()), Main.Red.class); + + // normalize: match default_to_red c with Red => Green | other => other + // (Prel catch-all binding the compound scrutinee to a variable) + assertColor("normalize(Red)", Main.normalize.apply(new Main.Red()), Main.Green.class); + assertColor("normalize(Green)", Main.normalize.apply(new Main.Green()), Main.Green.class); + assertColor("normalize(Blue)", Main.normalize.apply(new Main.Blue()), Main.Green.class); + + // A catch-all branch matches values beyond the extracted constructors, so + // even a foreign implementer of the interface takes the default branch + // instead of raising a match failure. + Main.color alien = new Main.color() {}; + assertColor("default_to_red(alien)", Main.default_to_red.apply(alien), Main.Red.class); + assertColor("normalize(alien)", Main.normalize.apply(alien), Main.Green.class); + } +} diff --git a/test-suite/misc/java-extraction/match_default/java_match_default.java.expected b/test-suite/misc/java-extraction/match_default/java_match_default.java.expected new file mode 100644 index 000000000000..a2f3229d7218 --- /dev/null +++ b/test-suite/misc/java-extraction/match_default/java_match_default.java.expected @@ -0,0 +1,42 @@ +import java.util.function.Function; + +class Main { + +static B let(A val, Function cont) { return cont.apply(val); } + +static A error(String msg) { throw new RuntimeException(msg); } + +public interface color {} +public static class Red implements color { + + Red() { + } + + } + +public static class Green implements color { + + Green() { + } + + } + +public static class Blue implements color { + + Blue() { + } + + } + +static Function default_to_red = c -> + (c instanceof Red) ? new Green() + : new Red() + ; + +static Function normalize = c -> + let(default_to_red.apply(c), scrutinee -> + (scrutinee instanceof Red) ? new Green() + : let(scrutinee, x -> x)) + ; + +}