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..5c8fd005d842 100755 --- a/test-suite/misc/java-extraction.sh +++ b/test-suite/misc/java-extraction.sh @@ -5,3 +5,5 @@ 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/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_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)) + ; + +} 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") + ; + +}