diff --git a/plugins/extraction/java.ml b/plugins/extraction/java.ml index ae82cb830e66..6dfc3ea6427a 100644 --- a/plugins/extraction/java.ml +++ b/plugins/extraction/java.ml @@ -25,7 +25,10 @@ let keywords = "catch"; "extends"; "int"; "short"; "try"; "char"; "final"; "interface"; "static"; "void"; "class"; "finally"; "long"; "strictfp"; "volatile"; - "const"; "float"; "native"; "super"; "while"; "_" ] + "const"; "float"; "native"; "super"; "while"; "_"; + (* not Java keywords, but names of the generated [class Main] helpers: + reserve them so extracted identifiers get renamed instead of clashing *) + "let"; "error"; "__"; "__dummy" ] Id.Set.empty let pp_comment s = str "// " ++ s ++ fnl () @@ -83,8 +86,10 @@ let pp_type table vl t = pp_tuple pp_rec l ++ spc () ++ pp_global table Type r | Tarr (t1,t2) -> str "Function<" ++ pp_rec t1 ++ str ", " ++ pp_rec t2++ str ">" - | Tdummy _ -> str "__" - | Tunknown -> str "__" + (* Both stand for "no informative type here"; [Object] is the weakest + valid Java type. A finer strategy (generics) is future work. *) + | Tdummy _ -> str "Object" + | Tunknown -> str "Object" in hov 0 (pp_rec t) @@ -144,9 +149,13 @@ let rec pp_expr table env args = expected result type for the generic return. *) str "error" ++ paren (pp_java_string s) | MLdummy _ -> - 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. *) + (* [__()] is a generic method, so each occurrence is target-typed by + its context. Applied arguments are dropped, as in the OCaml + backend: extracted code is pure, and self-application of the dummy + only yields the dummy again, so skipping the arguments cannot + change the result. (Emitting the application would not compile + anyway: a receiver position is not a poly context.) *) + str "__()" | MLmagic a -> pp_expr table env [] a | MLaxiom s -> @@ -424,6 +433,20 @@ let pp_struct table = fnl() ++ fnl() ++ str "static A error(String msg) { throw new RuntimeException(msg); }" ++ fnl() ++ fnl() ++ + (* The dummy value replacing erased logical content ([MLdummy]). It is + passed around and may even be applied at runtime, so it must be a + benign value, never a throwing expression: self-application returns + the value itself (same trick as the OCaml backend's [__]). *) + str "static final Function __dummy = new Function() {" ++ + fnl() ++ + str " public Object apply(Object x) { return this; }" ++ + fnl() ++ + str "};" ++ + fnl() ++ fnl() ++ + str "@SuppressWarnings(\"unchecked\")" ++ + fnl() ++ + str "static A __() { return (A) __dummy; }" ++ + 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 4611d5573632..71ded3604e5f 100755 --- a/test-suite/misc/java-extraction.sh +++ b/test-suite/misc/java-extraction.sh @@ -9,3 +9,4 @@ self_dir=$(CDPATH= cd -- "$(dirname -- "$0")" && pwd) "$self_dir/java-extraction/run-case.sh" match_default "$self_dir/java-extraction/run-case.sh" absurd_match "$self_dir/java-extraction/run-case.sh" axiom +"$self_dir/java-extraction/run-case.sh" mldummy diff --git a/test-suite/misc/java-extraction/absurd_match/java_absurd_match.java.expected b/test-suite/misc/java-extraction/absurd_match/java_absurd_match.java.expected index ca00ee59de90..ff2058c97160 100644 --- a/test-suite/misc/java-extraction/absurd_match/java_absurd_match.java.expected +++ b/test-suite/misc/java-extraction/absurd_match/java_absurd_match.java.expected @@ -6,6 +6,13 @@ static B let(A val, Function cont) { return cont.apply(val); } static A error(String msg) { throw new RuntimeException(msg); } +static final Function __dummy = new Function() { + public Object apply(Object x) { return this; } +}; + +@SuppressWarnings("unchecked") +static A __() { return (A) __dummy; } + public interface empty {} public interface result {} public static class Ok implements result { diff --git a/test-suite/misc/java-extraction/axiom/java_axiom.java.expected b/test-suite/misc/java-extraction/axiom/java_axiom.java.expected index 7c71bbea7992..de9f1d1eebde 100644 --- a/test-suite/misc/java-extraction/axiom/java_axiom.java.expected +++ b/test-suite/misc/java-extraction/axiom/java_axiom.java.expected @@ -6,6 +6,13 @@ static B let(A val, Function cont) { return cont.apply(val); } static A error(String msg) { throw new RuntimeException(msg); } +static final Function __dummy = new Function() { + public Object apply(Object x) { return this; } +}; + +@SuppressWarnings("unchecked") +static A __() { return (A) __dummy; } + public interface value {} public static class A implements value { 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 d9dbee39c35a..f047b9cd5be2 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 @@ -6,6 +6,13 @@ static B let(A val, Function cont) { return cont.apply(val); } static A error(String msg) { throw new RuntimeException(msg); } +static final Function __dummy = new Function() { + public Object apply(Object x) { return this; } +}; + +@SuppressWarnings("unchecked") +static A __() { return (A) __dummy; } + public interface nat {} public static class O implements nat { 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 4dc893768203..a163e453c2c4 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 @@ -6,6 +6,13 @@ static B let(A val, Function cont) { return cont.apply(val); } static A error(String msg) { throw new RuntimeException(msg); } +static final Function __dummy = new Function() { + public Object apply(Object x) { return this; } +}; + +@SuppressWarnings("unchecked") +static A __() { return (A) __dummy; } + 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 f9016cb2e9df..9c86bb569ff3 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 @@ -6,6 +6,13 @@ static B let(A val, Function cont) { return cont.apply(val); } static A error(String msg) { throw new RuntimeException(msg); } +static final Function __dummy = new Function() { + public Object apply(Object x) { return this; } +}; + +@SuppressWarnings("unchecked") +static A __() { return (A) __dummy; } + public interface nat {} public static class O implements nat { 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 index a2f3229d7218..7bcdd41a38cf 100644 --- 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 @@ -6,6 +6,13 @@ static B let(A val, Function cont) { return cont.apply(val); } static A error(String msg) { throw new RuntimeException(msg); } +static final Function __dummy = new Function() { + public Object apply(Object x) { return this; } +}; + +@SuppressWarnings("unchecked") +static A __() { return (A) __dummy; } + public interface color {} public static class Red implements color { 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 index c13a3d81fda2..b3ca150248fd 100644 --- 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 @@ -6,6 +6,13 @@ static B let(A val, Function cont) { return cont.apply(val); } static A error(String msg) { throw new RuntimeException(msg); } +static final Function __dummy = new Function() { + public Object apply(Object x) { return this; } +}; + +@SuppressWarnings("unchecked") +static A __() { return (A) __dummy; } + public interface color {} public static class Red implements color { diff --git a/test-suite/misc/java-extraction/mldummy.v b/test-suite/misc/java-extraction/mldummy.v new file mode 100644 index 000000000000..c37c6be18602 --- /dev/null +++ b/test-suite/misc/java-extraction/mldummy.v @@ -0,0 +1,14 @@ +Require Corelib.extraction.Extraction. + +Extraction Language Java. +Set Extraction Output Directory "misc/java-extraction/_generated/mldummy". + +(* Logical (Prop) constants survive extraction as [MLdummy] when extracted + directly: they must become a benign value, not a throwing expression. *) + +Definition tt_prop : True := I. + +Definition both : True /\ True := conj I I. + +Extraction "java_mldummy.java" + tt_prop both. diff --git a/test-suite/misc/java-extraction/mldummy/DriverMldummy.java b/test-suite/misc/java-extraction/mldummy/DriverMldummy.java new file mode 100644 index 000000000000..867172656f65 --- /dev/null +++ b/test-suite/misc/java-extraction/mldummy/DriverMldummy.java @@ -0,0 +1,21 @@ +import java.util.function.Function; + +public class DriverMldummy { + public static void main(String[] args) { + // Erased logical content becomes the benign dummy value: touching it must + // not throw (unlike an unrealized axiom), and it must survive being + // treated as a function, since extracted code may pass it around and + // apply it. + if (Main.tt_prop == null) { + throw new AssertionError("expected tt_prop to be a benign value but was null"); + } + if (Main.both == null) { + throw new AssertionError("expected both to be a benign value but was null"); + } + @SuppressWarnings("unchecked") + Function f = (Function) Main.tt_prop; + if (f.apply(null) != Main.tt_prop) { + throw new AssertionError("expected the dummy to be self-applicable"); + } + } +} diff --git a/test-suite/misc/java-extraction/mldummy/java_mldummy.java.expected b/test-suite/misc/java-extraction/mldummy/java_mldummy.java.expected new file mode 100644 index 000000000000..efbdb64645b3 --- /dev/null +++ b/test-suite/misc/java-extraction/mldummy/java_mldummy.java.expected @@ -0,0 +1,20 @@ +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); } + +static final Function __dummy = new Function() { + public Object apply(Object x) { return this; } +}; + +@SuppressWarnings("unchecked") +static A __() { return (A) __dummy; } + +static Object tt_prop = __(); + +static Object both = __(); + +}