diff --git a/plugins/extraction/java.ml b/plugins/extraction/java.ml index f85a23e361c6..ae82cb830e66 100644 --- a/plugins/extraction/java.ml +++ b/plugins/extraction/java.ml @@ -40,6 +40,26 @@ let preamble _ _ comment _ _ = let comma = fun _ -> str ", " let paren = pp_par true +(* Prints [s] as a Java string literal. [Pp.qs] escapes for OCaml, whose + conventions differ from Java's (e.g. decimal [\255] escapes). + Note: [\uXXXX] escapes are translated before Java lexes the file (JLS 3.3), + so line terminators, quotes and backslashes must be handled by the explicit + cases below and never reach the [\u] fallback. *) +let pp_java_string s = + let buf = Buffer.create (String.length s + 2) in + Buffer.add_char buf '"'; + String.iter (fun c -> match c with + | '"' -> Buffer.add_string buf {|\"|} + | '\\' -> Buffer.add_string buf {|\\|} + | '\n' -> Buffer.add_string buf {|\n|} + | '\r' -> Buffer.add_string buf {|\r|} + | '\t' -> Buffer.add_string buf {|\t|} + | c when Char.code c < 0x20 -> + Buffer.add_string buf (Printf.sprintf {|\u%04x|} (Char.code c)) + | c -> Buffer.add_char buf c) s; + Buffer.add_char buf '"'; + str (Buffer.contents buf) + let pp_global table k r = if is_inline_custom r then str (find_custom r) @@ -83,14 +103,9 @@ let pp_abst st idlist = match idlist with (* may need cast, "(Function)(x let pp_letin x def body = (* let(def, x -> body), where [let] is a defined function *) hv 0 (hv 0 (str "let" ++ paren (def ++ str ", " ++ x ++ str " ->" ++ spc() ++ hov 0 body))) -let pp_ids_pat table ids env = function - | Pwild -> str "_" - | Prel n -> Id.print (get_db_name n env) - | _ -> assert false - -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) +let pp_gen_pat table = function + | Pusual r -> pp_global_name table Cons r + | Pcons _ -> user_err Pp.(str "Cannot handle deep patterns in Java yet.") | Ptuple _ -> user_err Pp.(str "Cannot handle tuple patterns in Java yet.") | Pwild | Prel _ -> assert false (* catch-all: handled in pp_pat_branches *) @@ -124,21 +139,22 @@ let rec pp_expr table env args = let ids',env' = push_vars (List.rev (Array.to_list ids)) env in pp_fix table env' i (Array.of_list (List.rev ids'),defs) args | MLexn s -> - (* An [MLexn] may be applied, but I don't really care. *) - paren (str "error " ++ qs s) + (* Applied arguments are dropped: [error] throws before any + application could happen, and the surrounding context supplies the + expected result type for the generic return. *) + str "error" ++ paren (pp_java_string s) | MLdummy _ -> - str "__" (* An [MLdummy] may be applied, but I don't really care. *) + 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. *) | MLmagic a -> pp_expr table env [] a - | MLaxiom s -> paren (str "error \"AXIOM TO BE REALIZED (" ++ str s ++ str ")\"") - | MLuint _ -> - paren (str "Prelude.error \"EXTRACTION OF UINT NOT IMPLEMENTED\"") - | MLfloat _ -> - paren (str "Prelude.error \"EXTRACTION OF FLOAT NOT IMPLEMENTED\"") - | MLstring _ -> - paren (str "Prelude.error \"EXTRACTION OF STRING NOT IMPLEMENTED\"") - | MLparray _ -> - paren (str "Prelude.error \"EXTRACTION OF PARRAY NOT IMPLEMENTED\"") + | MLaxiom s -> + str "error" ++ paren (pp_java_string ("AXIOM TO BE REALIZED (" ^ s ^ ")")) + | MLuint _ -> user_err Pp.(str "Cannot handle primitive integers in Java yet.") + | MLfloat _ -> user_err Pp.(str "Cannot handle primitive floats in Java yet.") + | MLstring _ -> user_err Pp.(str "Cannot handle primitive strings in Java yet.") + | MLparray _ -> user_err Pp.(str "Cannot handle persistent arrays in Java yet.") and pp_fix table env i (ids,bl) args = prvect_with_sep @@ -155,7 +171,7 @@ and pp_one_pat table env exp (ids,p,t) = let n = List.length ids in let ids', env' = push_vars (List.rev_map id_of_mlid ids) env in let ids_field = List.rev ids' in - let constr, _instance = pp_gen_pat table (List.map id_of_mlid ids) env p in + let constr = pp_gen_pat table p in let body = pp_expr table env' [] t in let cast_exp = paren (paren (str constr) ++ exp) in let wrapped = List.fold_right diff --git a/test-suite/misc/java-extraction.sh b/test-suite/misc/java-extraction.sh index 5c8fd005d842..4611d5573632 100755 --- a/test-suite/misc/java-extraction.sh +++ b/test-suite/misc/java-extraction.sh @@ -7,3 +7,5 @@ self_dir=$(CDPATH= cd -- "$(dirname -- "$0")" && pwd) "$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 +"$self_dir/java-extraction/run-case.sh" absurd_match +"$self_dir/java-extraction/run-case.sh" axiom diff --git a/test-suite/misc/java-extraction/absurd_match.v b/test-suite/misc/java-extraction/absurd_match.v new file mode 100644 index 000000000000..e2a69ea83f22 --- /dev/null +++ b/test-suite/misc/java-extraction/absurd_match.v @@ -0,0 +1,27 @@ +Require Corelib.extraction.Extraction. + +Extraction Language Java. +Set Extraction Output Directory "misc/java-extraction/_generated/absurd_match". + +Inductive empty : Set := . + +Inductive result := +| Ok : result +| Ng : result. + +(* [shape] wraps [empty] so that the extracted lambda still uses its + parameter: matching a parameter directly against an empty inductive would + leave the parameter unused and extract it as the dummy binder [_], which + is not a valid lambda parameter name on every supported JDK. *) +Inductive shape := +| Leaf : shape +| Wrap : empty -> shape. + +Definition from_shape (s : shape) : result := + match s with + | Leaf => Ok + | Wrap e => match e with end + end. + +Extraction "java_absurd_match.java" + from_shape. diff --git a/test-suite/misc/java-extraction/absurd_match/DriverAbsurdMatch.java b/test-suite/misc/java-extraction/absurd_match/DriverAbsurdMatch.java new file mode 100644 index 000000000000..a22c6c34be5b --- /dev/null +++ b/test-suite/misc/java-extraction/absurd_match/DriverAbsurdMatch.java @@ -0,0 +1,23 @@ +public class DriverAbsurdMatch { + public static void main(String[] args) { + Main.result normal = Main.from_shape.apply(new Main.Leaf()); + if (!Main.Ok.class.equals(normal.getClass())) { + throw new AssertionError("expected Ok but got " + normal.getClass().getName()); + } + + // A [match] on an empty inductive type has no branches; reaching it must + // raise the explicit absurd-case error, not an accidental exception. + Main.shape absurd = new Main.Wrap(new Main.empty() {}); + try { + Main.from_shape.apply(absurd); + throw new AssertionError("expected an absurd-case failure but from_shape 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 (!"absurd case".equals(e.getMessage())) { + throw new AssertionError("unexpected absurd-case message: " + e.getMessage(), e); + } + } + } +} 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 new file mode 100644 index 000000000000..ca00ee59de90 --- /dev/null +++ b/test-suite/misc/java-extraction/absurd_match/java_absurd_match.java.expected @@ -0,0 +1,48 @@ +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 empty {} +public interface result {} +public static class Ok implements result { + + Ok() { + } + + } + +public static class Ng implements result { + + Ng() { + } + + } + +public interface shape {} +public static class Leaf implements shape { + + Leaf() { + } + + } + +public static class Wrap implements shape { + final empty Wrap0; + + Wrap(empty Wrap0) { + this.Wrap0 = Wrap0; + } + + } + +static Function from_shape = s -> + (s instanceof Leaf) ? new Ok() + : (s instanceof Wrap) ? error("absurd case") + : error("non-exhaustive match") + ; + +} diff --git a/test-suite/misc/java-extraction/axiom.v b/test-suite/misc/java-extraction/axiom.v new file mode 100644 index 000000000000..688f0df29397 --- /dev/null +++ b/test-suite/misc/java-extraction/axiom.v @@ -0,0 +1,13 @@ +Require Corelib.extraction.Extraction. + +Extraction Language Java. +Set Extraction Output Directory "misc/java-extraction/_generated/axiom". + +Inductive value := +| A : value +| B : value. + +Axiom mystery : value. + +Extraction "java_axiom.java" + mystery. diff --git a/test-suite/misc/java-extraction/axiom/DriverAxiom.java b/test-suite/misc/java-extraction/axiom/DriverAxiom.java new file mode 100644 index 000000000000..1f83f2366e13 --- /dev/null +++ b/test-suite/misc/java-extraction/axiom/DriverAxiom.java @@ -0,0 +1,18 @@ +public class DriverAxiom { + public static void main(String[] args) { + // An unrealized axiom extracts to a throwing static field initializer, so + // the first touch of the Main class fails its static initialization. + try { + Main.mystery.getClass(); + throw new AssertionError("expected class initialization to fail but mystery was usable"); + } catch (ExceptionInInitializerError e) { + Throwable cause = e.getCause(); + if (cause == null || !RuntimeException.class.equals(cause.getClass())) { + throw new AssertionError("expected a plain RuntimeException cause but got " + cause, e); + } + if (!"AXIOM TO BE REALIZED (axiom.mystery)".equals(cause.getMessage())) { + throw new AssertionError("unexpected axiom message: " + cause.getMessage(), e); + } + } + } +} diff --git a/test-suite/misc/java-extraction/axiom/java_axiom.java.expected b/test-suite/misc/java-extraction/axiom/java_axiom.java.expected new file mode 100644 index 000000000000..7c71bbea7992 --- /dev/null +++ b/test-suite/misc/java-extraction/axiom/java_axiom.java.expected @@ -0,0 +1,26 @@ +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 value {} +public static class A implements value { + + A() { + } + + } + +public static class B implements value { + + B() { + } + + } + +static value mystery = error("AXIOM TO BE REALIZED (axiom.mystery)"); + +}