Emit a benign dummy value for MLdummy (#14)

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> 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<Object, Object> __dummy = new Function<Object, Object>() {" ++
+    fnl() ++
+    str "  public Object apply(Object x) { return this; }" ++
+    fnl() ++
+    str "};" ++
+    fnl() ++ fnl() ++
+    str "@SuppressWarnings(\"unchecked\")" ++
+    fnl() ++
+    str "static <A> A __() { return (A) __dummy; }" ++
+    fnl() ++ fnl() ++
     prlist_strict pp_sel structure ++
     str "}" ++ fnl()
 

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

test-suite/misc/java-extraction/absurd_match/java_absurd_match.java.expected

@@ -6,6 +6,13 @@ static <A, B> B let(A val, Function<A, B> cont) { return cont.apply(val); }
 
 static <A> A error(String msg) { throw new RuntimeException(msg); }
 
+static final Function<Object, Object> __dummy = new Function<Object, Object>() {
+  public Object apply(Object x) { return this; }
+};
+
+@SuppressWarnings("unchecked")
+static <A> A __() { return (A) __dummy; }
+
 public interface empty {}
 public interface result {}
 public static class Ok implements result {

test-suite/misc/java-extraction/axiom/java_axiom.java.expected

@@ -6,6 +6,13 @@ static <A, B> B let(A val, Function<A, B> cont) { return cont.apply(val); }
 
 static <A> A error(String msg) { throw new RuntimeException(msg); }
 
+static final Function<Object, Object> __dummy = new Function<Object, Object>() {
+  public Object apply(Object x) { return this; }
+};
+
+@SuppressWarnings("unchecked")
+static <A> A __() { return (A) __dummy; }
+
 public interface value {}
 public static class A implements value {
 

test-suite/misc/java-extraction/basic_arithmetic/java_arithmetic_demo.java.expected

@@ -6,6 +6,13 @@ static <A, B> B let(A val, Function<A, B> cont) { return cont.apply(val); }
 
 static <A> A error(String msg) { throw new RuntimeException(msg); }
 
+static final Function<Object, Object> __dummy = new Function<Object, Object>() {
+  public Object apply(Object x) { return this; }
+};
+
+@SuppressWarnings("unchecked")
+static <A> A __() { return (A) __dummy; }
+
 public interface nat {}
 public static class O implements nat {
 

test-suite/misc/java-extraction/basic_arithmetic/java_constants_demo.java.expected

@@ -6,6 +6,13 @@ static <A, B> B let(A val, Function<A, B> cont) { return cont.apply(val); }
 
 static <A> A error(String msg) { throw new RuntimeException(msg); }
 
+static final Function<Object, Object> __dummy = new Function<Object, Object>() {
+  public Object apply(Object x) { return this; }
+};
+
+@SuppressWarnings("unchecked")
+static <A> A __() { return (A) __dummy; }
+
 public interface nat {}
 public static class O implements nat {
 

test-suite/misc/java-extraction/list_reverse/java_list_reverse.java.expected

@@ -6,6 +6,13 @@ static <A, B> B let(A val, Function<A, B> cont) { return cont.apply(val); }
 
 static <A> A error(String msg) { throw new RuntimeException(msg); }
 
+static final Function<Object, Object> __dummy = new Function<Object, Object>() {
+  public Object apply(Object x) { return this; }
+};
+
+@SuppressWarnings("unchecked")
+static <A> A __() { return (A) __dummy; }
+
 public interface nat {}
 public static class O implements nat {
 

test-suite/misc/java-extraction/match_default/java_match_default.java.expected

@@ -6,6 +6,13 @@ static <A, B> B let(A val, Function<A, B> cont) { return cont.apply(val); }
 
 static <A> A error(String msg) { throw new RuntimeException(msg); }
 
+static final Function<Object, Object> __dummy = new Function<Object, Object>() {
+  public Object apply(Object x) { return this; }
+};
+
+@SuppressWarnings("unchecked")
+static <A> A __() { return (A) __dummy; }
+
 public interface color {}
 public static class Red implements color {
 

test-suite/misc/java-extraction/match_failure/java_match_failure.java.expected

@@ -6,6 +6,13 @@ static <A, B> B let(A val, Function<A, B> cont) { return cont.apply(val); }
 
 static <A> A error(String msg) { throw new RuntimeException(msg); }
 
+static final Function<Object, Object> __dummy = new Function<Object, Object>() {
+  public Object apply(Object x) { return this; }
+};
+
+@SuppressWarnings("unchecked")
+static <A> A __() { return (A) __dummy; }
+
 public interface color {}
 public static class Red implements color {
 

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.

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<Object, Object> f = (Function<Object, Object>) Main.tt_prop;
+    if (f.apply(null) != Main.tt_prop) {
+      throw new AssertionError("expected the dummy to be self-applicable");
+    }
+  }
+}

test-suite/misc/java-extraction/mldummy/java_mldummy.java.expected

@@ -0,0 +1,20 @@
+import java.util.function.Function;
+
+class Main {
+
+static <A, B> B let(A val, Function<A, B> cont) { return cont.apply(val); }
+
+static <A> A error(String msg) { throw new RuntimeException(msg); }
+
+static final Function<Object, Object> __dummy = new Function<Object, Object>() {
+  public Object apply(Object x) { return this; }
+};
+
+@SuppressWarnings("unchecked")
+static <A> A __() { return (A) __dummy; }
+
+static Object tt_prop = __();
+
+static Object both = __();
+
+}