From f50ea7cdb7f49c402cee0e53b6819efa6ef7fcb3 Mon Sep 17 00:00:00 2001 From: Hiroshi Yamaguchi Date: Thu, 9 Jul 2026 02:15:12 +0900 Subject: [PATCH] Extract local MLfix as valid Java expressions via fixK helpers MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The Java backend printed local MLfix as a statement sequence (var f = ...; ...; f.apply(args)), which is invalid in expression positions (lambda bodies, let RHS, function arguments). Every other MiniML construct already prints as an expression. Encode a local fix applied to K arguments as a call to a generated generic helper fixK(gen, a1, ..., aK) that ties recursion by method self-reference, so no cell arrays, unchecked casts, definite-assignment or effectively-final issues arise. Argument types ground A1..AK bottom-up and R is grounded by the target type of the expression position. Helpers are emitted on demand per arity next to the let helper (fix0 for unapplied fixes implies fix1). Mutual fixpoint groups are eliminated before printing by a Bekić rewrite (unmutualize) into nested single fixes, using mlutil's permut_rels and gen_subst (now exported). Supporting changes needed for javac type inference: - Inline let-bound fix heads into their use sites (a fixK call in the targetless let() argument position would infer Object). - Upcast constructor expressions to their inductive interface, ((natlist) new Cons(...)), to avoid over-specialized inference such as A2 := Nil; skipped for custom inductives. Expected outputs regenerated accordingly. - Fix MLmagic and MLcase dropping the application args accumulator. Known limitations: fixK calls in positions without a target type infer R = Object (e.g. a fix application result bound by let); helper names fixN can collide with user identifiers (same caveat as let); parameterized inductives get raw-type casts. Tests: local_fix (single recursion, applied K=2 and reused let-bound fix) and local_fix_mutual (mutual even/odd, K=0 elim-last and K=1 elim-first paths), each with a runtime driver. Co-Authored-By: Claude Fable 5 --- plugins/extraction/java.ml | 129 ++++++++++++++---- plugins/extraction/mlutil.mli | 2 + test-suite/misc/java-extraction.sh | 2 + .../java_arithmetic_demo.java.expected | 12 +- .../java_constants_demo.java.expected | 4 +- .../java_list_reverse.java.expected | 10 +- test-suite/misc/java-extraction/local_fix.v | 27 ++++ .../local_fix/DriverLocalFix.java | 55 ++++++++ .../local_fix/java_local_fix.java.expected | 75 ++++++++++ .../misc/java-extraction/local_fix_mutual.v | 37 +++++ .../local_fix_mutual/DriverParity.java | 44 ++++++ .../java_local_fix_mutual.java.expected | 71 ++++++++++ 12 files changed, 431 insertions(+), 37 deletions(-) create mode 100644 test-suite/misc/java-extraction/local_fix.v create mode 100644 test-suite/misc/java-extraction/local_fix/DriverLocalFix.java create mode 100644 test-suite/misc/java-extraction/local_fix/java_local_fix.java.expected create mode 100644 test-suite/misc/java-extraction/local_fix_mutual.v create mode 100644 test-suite/misc/java-extraction/local_fix_mutual/DriverParity.java create mode 100644 test-suite/misc/java-extraction/local_fix_mutual/java_local_fix_mutual.java.expected 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))))) + ; + +}