Check pattern conformance in all MLcase branches (#6)

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 <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); }" ++
+    fnl() ++ fnl() ++
     prlist_strict pp_sel structure ++
     str "}" ++ fnl()
 

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

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

@@ -4,6 +4,8 @@ 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); }
+
 public interface nat {}
 public static class O implements nat {
 
@@ -25,8 +27,8 @@ static Function<nat, Function<nat, nat>> 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<nat, Function<nat, nat>> 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")
 ;
 }
 

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

@@ -4,6 +4,8 @@ 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); }
+
 public interface nat {}
 public static class O implements nat {
 

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

@@ -4,6 +4,8 @@ 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); }
+
 public interface nat {}
 public static class O implements nat {
 
@@ -45,20 +47,21 @@ 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")
 ;
 }
 
 static Function<natlist, natlist> 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")
 ;
 }
 

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.

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);
+  }
+}

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

@@ -0,0 +1,42 @@
+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); }
+
+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<color, color> default_to_red = c ->
+  (c instanceof Red) ? new Green()
+  : new Red()
+  ;
+
+static Function<color, color> normalize = c ->
+  let(default_to_red.apply(c), scrutinee ->
+  (scrutinee instanceof Red) ? new Green()
+  : let(scrutinee, x -> x))
+  ;
+
+}

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.

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);
+      }
+    }
+  }
+}

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

@@ -0,0 +1,38 @@
+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); }
+
+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<color, color> rotate = c ->
+  (c instanceof Red) ? new Green()
+  : (c instanceof Green) ? new Blue()
+  : (c instanceof Blue) ? new Red()
+  : error("non-exhaustive match")
+  ;
+
+}