diff --git a/plugins/extraction/java.ml b/plugins/extraction/java.ml index 293d8a3dc4f8..02ca358fb309 100644 --- a/plugins/extraction/java.ml +++ b/plugins/extraction/java.ml @@ -83,6 +83,15 @@ 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 kn_of_ind r = let open GlobRef in match r.glob with + | IndRef (kn,_) -> MutInd.user kn + | _ -> assert false + +let get_ind r = let open GlobRef in match r.glob with + | IndRef _ -> r + | ConstructRef (ind,_) -> { glob = IndRef ind; inst = r.inst } + | _ -> assert false + let pp_ids_pat table ids env = function | Pwild -> str "_" | Prel n -> Id.print (get_db_name n env) @@ -95,6 +104,67 @@ let pp_gen_pat table ids env = function | Pwild -> "_", [] (* TODO *) | Prel n -> Id.to_string (get_db_name n env), [] +let fix_arities = ref Int.Set.empty + +let reset_fix_arities () = + fix_arities := Int.Set.empty + +let record_fix_arity k = + fix_arities := Int.Set.add k !fix_arities + +let rec is_fix_head = function + | MLfix _ -> true + | MLapp (f, _) -> is_fix_head f + | MLmagic a -> is_fix_head a + | _ -> false + +(* defs use Rel 1 = ids.(n-1), ..., Rel n = ids.(0). *) +let rec unmutualize i ids defs = + let n = Array.length ids in + if n <= 1 then (i, ids, defs) + else if i < n - 1 then + let inner = MLfix (0, [|ids.(n-1)|], [|defs.(n-1)|]) in + let defs' = Array.map (ast_subst inner) (Array.sub defs 0 (n-1)) in + unmutualize i (Array.sub ids 0 (n-1)) defs' + else + let inner = MLfix (0, [|ids.(0)|], [|permut_rels (n-1) 1 defs.(0)|]) in + let v = Array.init n + (fun j -> Some (if j < n-1 then MLrel (j+1) else inner)) + in + let defs' = Array.map (gen_subst v (-1)) (Array.sub defs 1 (n-1)) in + unmutualize (i-1) (Array.sub ids 1 (n-1)) defs' + +let pp_fix_helper k = + let tyvar i = str "A" ++ int i in + let arg i = str "a" ++ int i in + let xarg i = str "x" ++ int i in + let rec fn_type i = + if Int.equal i (k + 1) then str "R" + else str "Function<" ++ tyvar i ++ str ", " ++ fn_type (i+1) ++ str ">" + in + let type_params = + if Int.equal k 0 then str "" + else str "<" ++ prlist_with_sep comma tyvar (List.init k (fun i -> i+1)) ++ str ", R>" + in + let apply_args prefix = + prlist_strict (fun i -> str ".apply" ++ paren (prefix i)) (List.init k (fun i -> i+1)) + in + if Int.equal k 0 then + str "static Function fix0(Function, Function> gen) {" ++ fnl() ++ + str " return a1 -> fix1(gen, a1);" ++ fnl() ++ + str "}" ++ fnl2() + else + str "static " ++ type_params ++ spc() ++ str "R fix" ++ int k ++ + paren + (str "Function<" ++ fn_type 1 ++ str ", " ++ fn_type 1 ++ str "> gen, " ++ + prlist_with_sep comma (fun i -> tyvar i ++ spc() ++ arg i) (List.init k (fun i -> i+1))) ++ + str " {" ++ fnl() ++ + str " return gen.apply(" ++ + prlist_with_sep (fun () -> str " -> ") xarg (List.init k (fun i -> i+1)) ++ + str " -> fix" ++ int k ++ paren (str "gen, " ++ prlist_with_sep comma xarg (List.init k (fun i -> i+1))) ++ + str ")" ++ apply_args arg ++ str ";" ++ fnl() ++ + str "}" ++ fnl2() + let rec pp_expr table env args = let apply st = pp_app st args in function @@ -108,20 +178,26 @@ let rec pp_expr table env args = let fl,env' = push_vars (List.map id_of_mlid fl) env in apply (pp_abst (pp_expr table env' [] a') (List.rev fl)) | MLletin (id,a1,a2) -> - let i,env' = push_vars [id_of_mlid id] env in - let pp_id = pr_id (List.hd i) - and pp_a1 = pp_expr table env [] a1 - and pp_a2 = pp_expr table env' [] a2 in - hv 0 (apply (pp_letin pp_id pp_a1 pp_a2)) + if is_fix_head a1 then pp_expr table env args (ast_subst a1 a2) + else + let i,env' = push_vars [id_of_mlid id] env in + let pp_id = pr_id (List.hd i) + and pp_a1 = pp_expr table env [] a1 + and pp_a2 = pp_expr table env' [] a2 in + hv 0 (apply (pp_letin pp_id pp_a1 pp_a2)) | MLglob r -> apply (pp_global table Term r) | MLcons (_,r,args') -> (* [r] : a name of a constructor *) assert (List.is_empty args); - str "new " ++ pp_global table Cons r ++ paren (prlist_with_sep comma (pp_expr table env []) args') + let cons = str "new " ++ pp_global table Cons r ++ paren (prlist_with_sep comma (pp_expr table env []) args') in + let ind = get_ind r in + if is_custom ind || is_inline_custom ind then cons + else paren (paren (pp_global table Type ind) ++ spc () ++ cons) | MLtuple _ -> user_err Pp.(str "Cannot handle tuples in Java yet.") | MLcase (_,t, pv) -> - pp_pat table env t pv + apply (paren (pp_pat table env t pv)) | MLfix (i,ids,defs) -> + let i,ids,defs = unmutualize i ids defs in 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 -> @@ -130,7 +206,7 @@ let rec pp_expr table env args = | MLdummy _ -> str "__" (* An [MLdummy] may be applied, but I don't really care. *) | MLmagic a -> - pp_expr table env [] a + pp_expr table env args a | MLaxiom s -> paren (str "error \"AXIOM TO BE REALIZED (" ++ str s ++ str ")\"") | MLuint _ -> paren (str "Prelude.error \"EXTRACTION OF UINT NOT IMPLEMENTED\"") @@ -142,12 +218,17 @@ let rec pp_expr table env args = paren (str "Prelude.error \"EXTRACTION OF PARRAY NOT IMPLEMENTED\"") and pp_fix table env i (ids,bl) args = - prvect_with_sep - (fun () -> str ";" ++ fnl() ++ str "var ") - (fun (fi,ti) -> pr_id fi ++ str " = " ++ pp_expr table env [] ti) - (Array.map2 (fun id b -> (id,b)) ids bl) ++ - fnl () ++ - hov 2 (str ";" ++ fnl() ++ pp_app (pr_id ids.(i)) args) + assert (Array.length ids = 1); + assert (Array.length bl = 1); + assert (Int.equal i 0); + let k = List.length args in + record_fix_arity k; + str "fix" ++ int k ++ + paren + (pr_id ids.(0) ++ str " -> " ++ pp_expr table env [] bl.(0) ++ + (match args with + | [] -> mt () + | _ -> str ", " ++ prlist_with_sep comma identity args)) and pp_one_pat table env exp (ids,p,t) = (* push_vars after List.rev_map makes the head of ids' correspond to @@ -217,15 +298,6 @@ let pp_global_name table k r = str (Common.pp_global table k r) let pp_parameters l = (pp_boxed_tuple pp_tvar l ++ space_if (not (List.is_empty l))) -let kn_of_ind r = let open GlobRef in match r.glob with - | IndRef (kn,_) -> MutInd.user kn - | _ -> assert false - -let get_ind r = let open GlobRef in match r.glob with - | IndRef _ -> r - | ConstructRef (ind,_) -> { glob = IndRef ind; inst = r.inst } - | _ -> assert false - let pp_one_field table r i = function | Some r' -> pp_global_with_key table Term (kn_of_ind (get_ind r)) r' | None -> pp_global table Type (get_ind r) ++ str "__" ++ int i @@ -375,10 +447,17 @@ let pp_struct table = prlist_strict (fun e -> pp_structure_elem table e) sel end in fun structure -> + reset_fix_arities (); + let body = prlist_strict pp_sel structure in + let arities = + if Int.Set.mem 0 !fix_arities then Int.Set.add 1 !fix_arities + else !fix_arities + in str "class Main {" ++ fnl() ++ fnl() ++ str "static B let(A val, Function cont) { return cont.apply(val); }" ++ fnl() ++ fnl() ++ - prlist_strict pp_sel structure ++ + Int.Set.fold (fun k pp -> pp ++ pp_fix_helper k) arities (mt ()) ++ + body ++ str "}" ++ fnl() let file_naming state mp = file_of_modfile (State.get_table state) mp @@ -393,4 +472,4 @@ let java_descr = { sig_preamble = (fun _ _ _ _ _ -> mt ()); pp_sig = (fun _ _ -> mt ()); pp_decl = pp_decl; -} \ No newline at end of file +} diff --git a/plugins/extraction/mlutil.mli b/plugins/extraction/mlutil.mli index 7d15491c29a4..9290545872d9 100644 --- a/plugins/extraction/mlutil.mli +++ b/plugins/extraction/mlutil.mli @@ -108,7 +108,9 @@ val ast_occurs : int -> ml_ast -> bool val ast_occurs_itvl : int -> int -> ml_ast -> bool val ast_lift : int -> ml_ast -> ml_ast val ast_pop : ml_ast -> ml_ast +val permut_rels : int -> int -> ml_ast -> ml_ast val ast_subst : ml_ast -> ml_ast -> ml_ast +val gen_subst : ml_ast option array -> int -> ml_ast -> ml_ast val ast_glob_subst : ml_ast Refmap'.t -> ml_ast -> ml_ast diff --git a/test-suite/misc/java-extraction.sh b/test-suite/misc/java-extraction.sh index a8ee57d9283d..562d25e5e222 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" local_fix +"$self_dir/java-extraction/run-case.sh" local_fix_mutual 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..c886e583ac0d 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 @@ -24,9 +24,9 @@ public static class S implements nat { static Function> add; static { add = n -> m -> -(n instanceof O) ? m +((n instanceof O) ? m : // n instanceof S - let(((S)n).S0, n$ -> new S(add.apply(n$).apply(m))) + let(((S)n).S0, n$ -> ((nat) new S(add.apply(n$).apply(m))))) ; } @@ -36,14 +36,14 @@ static Function double0 = n -> add.apply(n).apply(n) static Function> mul; static { mul = n -> m -> -(n instanceof O) ? new O() +((n instanceof O) ? ((nat) new O()) : // n instanceof S - let(((S)n).S0, n$ -> add.apply(m).apply(mul.apply(n$).apply(m))) + let(((S)n).S0, n$ -> add.apply(m).apply(mul.apply(n$).apply(m)))) ; } -static nat two = new S(new S(new O())); +static nat two = ((nat) new S(((nat) new S(((nat) new O()))))); -static nat three = new S(two); +static nat three = ((nat) new S(two)); } 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..f5b59a2052cc 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 @@ -21,8 +21,8 @@ public static class S implements nat { } -static nat two = new S(new S(new O())); +static nat two = ((nat) new S(((nat) new S(((nat) new O()))))); -static nat three = new S(two); +static nat three = ((nat) new S(two)); } 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..852df6949056 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 @@ -44,21 +44,23 @@ static Function> app; static { app = l1 -> l2 -> -(l1 instanceof Nil) ? 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)))) + let(((Cons)l1).Cons1, xs -> + ((natlist) new Cons(x, app.apply(xs).apply(l2)))))) ; } static Function reverse; static { reverse = l -> -(l instanceof Nil) ? new Nil() +((l instanceof Nil) ? ((natlist) 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())))) + app.apply(reverse.apply(xs)).apply(((natlist) new Cons(x, ((natlist) + new Nil()))))))) ; } diff --git a/test-suite/misc/java-extraction/local_fix.v b/test-suite/misc/java-extraction/local_fix.v new file mode 100644 index 000000000000..4f6585c2ae42 --- /dev/null +++ b/test-suite/misc/java-extraction/local_fix.v @@ -0,0 +1,27 @@ +Require Corelib.extraction.Extraction. + +Extraction Language Java. +Set Extraction Output Directory "misc/java-extraction/_generated/local_fix". + +Inductive natlist := +| Nil : natlist +| Cons : nat -> natlist -> natlist. + +Definition rev_acc (l acc : natlist) : natlist := + let fix go l acc := + match l with + | Nil => acc + | Cons x xs => go xs (Cons x acc) + end + in go l Nil. + +Definition rev_pair (l : natlist) : natlist := + let fix go l acc := + match l with + | Nil => acc + | Cons x xs => go xs (Cons x acc) + end + in go (go l Nil) Nil. + +Extraction "java_local_fix.java" + rev_acc rev_pair. diff --git a/test-suite/misc/java-extraction/local_fix/DriverLocalFix.java b/test-suite/misc/java-extraction/local_fix/DriverLocalFix.java new file mode 100644 index 000000000000..2c75c8c7ec67 --- /dev/null +++ b/test-suite/misc/java-extraction/local_fix/DriverLocalFix.java @@ -0,0 +1,55 @@ +public class DriverLocalFix { + static Main.nat intToNat(int n) { + Main.nat r = new Main.O(); + for (int i = 0; i < n; i++) { + r = new Main.S(r); + } + return r; + } + + static int natToInt(Main.nat n) { + int i = 0; + while (n instanceof Main.S) { + i++; + n = ((Main.S) n).S0; + } + return i; + } + + static Main.natlist build(int... xs) { + Main.natlist l = new Main.Nil(); + for (int i = xs.length - 1; i >= 0; i--) { + l = new Main.Cons(intToNat(xs[i]), l); + } + return l; + } + + static String show(Main.natlist l) { + StringBuilder sb = new StringBuilder("["); + boolean first = true; + while (l instanceof Main.Cons) { + Main.Cons c = (Main.Cons) l; + if (!first) { + sb.append("; "); + } + sb.append(natToInt(c.Cons0)); + first = false; + l = c.Cons1; + } + sb.append("]"); + return sb.toString(); + } + + static void assertList(String expected, Main.natlist actual) { + String actualShown = show(actual); + if (!expected.equals(actualShown)) { + throw new AssertionError("expected " + expected + " but got " + actualShown); + } + } + + public static void main(String[] args) { + assertList("[3; 2; 1]", Main.rev_acc.apply(build(1, 2, 3)).apply(new Main.Nil())); + assertList("[]", Main.rev_acc.apply(build()).apply(new Main.Nil())); + assertList("[4; 5; 6]", Main.rev_pair.apply(build(4, 5, 6))); + } +} diff --git a/test-suite/misc/java-extraction/local_fix/java_local_fix.java.expected b/test-suite/misc/java-extraction/local_fix/java_local_fix.java.expected new file mode 100644 index 000000000000..78cb9030fe8b --- /dev/null +++ b/test-suite/misc/java-extraction/local_fix/java_local_fix.java.expected @@ -0,0 +1,75 @@ +import java.util.function.Function; + +class Main { + +static B let(A val, Function cont) { return cont.apply(val); } + +static +R fix2(Function>, Function>> gen, A1 +a1, A2 +a2) { + return gen.apply(x1 -> x2 -> fix2(gen, x1, x2)).apply(a1).apply(a2); +} + +public interface nat {} +public static class O implements nat { + + O() { + } + + } + +public static class S implements nat { + final nat S0; + + S(nat S0) { + this.S0 = S0; + } + + } + +public interface natlist {} +public static class Nil implements natlist { + + Nil() { + } + + } + +public static class Cons implements natlist { + final nat Cons0; + final natlist Cons1; + + Cons(nat Cons0, natlist Cons1) { + this.Cons0 = Cons0; + this.Cons1 = Cons1; + } + + } + +static Function> rev_acc = l -> _ -> + fix2(go -> l0 -> acc -> + ((l0 instanceof Nil) ? acc + : // l0 instanceof Cons + let(((Cons)l0).Cons0, x -> + let(((Cons)l0).Cons1, xs -> + go.apply(xs).apply(((natlist) new Cons(x, acc)))))) + , l, ((natlist) new Nil())) + ; + +static Function rev_pair = l -> fix2(go -> l0 -> acc -> + ((l0 instanceof Nil) ? acc + : // l0 instanceof Cons + let(((Cons)l0).Cons0, x -> + let(((Cons)l0).Cons1, xs -> + go.apply(xs).apply(((natlist) new Cons(x, acc)))))) + , fix2(go -> l0 -> acc -> + ((l0 instanceof Nil) ? acc + : // l0 instanceof Cons + let(((Cons)l0).Cons0, x -> + let(((Cons)l0).Cons1, xs -> + go.apply(xs).apply(((natlist) new Cons(x, acc)))))) + , l, ((natlist) new Nil())), ((natlist) new Nil())) + ; + +} diff --git a/test-suite/misc/java-extraction/local_fix_mutual.v b/test-suite/misc/java-extraction/local_fix_mutual.v new file mode 100644 index 000000000000..f971d10065fe --- /dev/null +++ b/test-suite/misc/java-extraction/local_fix_mutual.v @@ -0,0 +1,37 @@ +Require Corelib.extraction.Extraction. + +Extraction Language Java. +Set Extraction Output Directory "misc/java-extraction/_generated/local_fix_mutual". + +Inductive parity := +| Even : parity +| Odd : parity. + +Definition parity_of (n : nat) : parity := + (fix evenp (n : nat) : parity := + match n with + | O => Even + | S m => oddp m + end + with oddp (n : nat) : parity := + match n with + | O => Odd + | S m => evenp m + end + for evenp) n. + +Definition parity_of_succ (n : nat) : parity := + (fix evenp (n : nat) : parity := + match n with + | O => Even + | S m => oddp m + end + with oddp (n : nat) : parity := + match n with + | O => Odd + | S m => evenp m + end + for oddp) (S (S n)). + +Extraction "java_local_fix_mutual.java" + parity_of parity_of_succ. diff --git a/test-suite/misc/java-extraction/local_fix_mutual/DriverParity.java b/test-suite/misc/java-extraction/local_fix_mutual/DriverParity.java new file mode 100644 index 000000000000..1612f898ce42 --- /dev/null +++ b/test-suite/misc/java-extraction/local_fix_mutual/DriverParity.java @@ -0,0 +1,44 @@ +public class DriverParity { + static Main.nat intToNat(int n) { + Main.nat r = new Main.O(); + for (int i = 0; i < n; i++) { + r = new Main.S(r); + } + return r; + } + + static String show(Main.parity p) { + if (p instanceof Main.Even) { + return "Even"; + } + if (p instanceof Main.Odd) { + return "Odd"; + } + throw new AssertionError("unknown parity value"); + } + + static void assertParity(String expected, Main.parity actual) { + String actualShown = show(actual); + if (!expected.equals(actualShown)) { + throw new AssertionError("expected " + expected + " but got " + actualShown); + } + } + + static void assertSuccAgrees(int n) { + String expected = show(Main.parity_of.apply(intToNat(n + 1))); + String actual = show(Main.parity_of_succ.apply(intToNat(n))); + if (!expected.equals(actual)) { + throw new AssertionError("expected parity_of_succ " + n + " to be " + expected + " but got " + actual); + } + } + + public static void main(String[] args) { + assertParity("Even", Main.parity_of.apply(intToNat(0))); + assertParity("Odd", Main.parity_of.apply(intToNat(5))); + assertSuccAgrees(0); + assertSuccAgrees(1); + assertSuccAgrees(2); + assertSuccAgrees(3); + assertSuccAgrees(4); + } +} diff --git a/test-suite/misc/java-extraction/local_fix_mutual/java_local_fix_mutual.java.expected b/test-suite/misc/java-extraction/local_fix_mutual/java_local_fix_mutual.java.expected new file mode 100644 index 000000000000..847515b7f979 --- /dev/null +++ b/test-suite/misc/java-extraction/local_fix_mutual/java_local_fix_mutual.java.expected @@ -0,0 +1,71 @@ +import java.util.function.Function; + +class Main { + +static B let(A val, Function cont) { return cont.apply(val); } + +static Function fix0(Function, Function> gen) { + return a1 -> fix1(gen, a1); +} + +static R fix1(Function, Function> gen, A1 +a1) { + return gen.apply(x1 -> fix1(gen, x1)).apply(a1); +} + +public interface nat {} +public static class O implements nat { + + O() { + } + + } + +public static class S implements nat { + final nat S0; + + S(nat S0) { + this.S0 = S0; + } + + } + +public interface parity {} +public static class Even implements parity { + + Even() { + } + + } + +public static class Odd implements parity { + + Odd() { + } + + } + +static Function parity_of = fix0(evenp -> n -> + ((n instanceof O) ? ((parity) new Even()) + : // n instanceof S + let(((S)n).S0, m -> + fix1(oddp -> n0 -> + ((n0 instanceof O) ? ((parity) new Odd()) + : // n0 instanceof S + let(((S)n0).S0, m0 -> evenp.apply(m0))) + , m))) + ); + +static Function parity_of_succ = n -> fix1(oddp -> n0 -> + ((n0 instanceof O) ? ((parity) new Odd()) + : // n0 instanceof S + let(((S)n0).S0, m -> + fix1(evenp -> n1 -> + ((n1 instanceof O) ? ((parity) new Even()) + : // n1 instanceof S + let(((S)n1).S0, m0 -> oddp.apply(m0))) + , m))) + , ((nat) new S(((nat) new S(n))))) + ; + +}