WIP: Extract local MLfix as valid Java expressions via fixK helpers

plugins/extraction/java.ml

@@ -83,6 +83,15 @@ let pp_abst st idlist = match idlist with (* may need cast, "(Function<S, T>)(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 "<A1, R>"
+    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 <A1, R> Function<A1, R> fix0(Function<Function<A1, R>, Function<A1, R>> 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 <A, B> B let(A val, Function<A, B> 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;
-}
+}

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
 

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

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

@@ -24,9 +24,9 @@ public static class S implements nat {
 static Function<nat, Function<nat, nat>> 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<nat, nat> double0 = n -> add.apply(n).apply(n)
 static Function<nat, Function<nat, nat>> 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));
 
 }

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

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

@@ -44,21 +44,23 @@ static Function<natlist, Function<natlist, natlist>>
 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<natlist, natlist> 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())))))))
 ;
 }
 

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.

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