Make good progress on generating code for HOL4

8 files changed, 1217 insertions, 487 deletions

diff --git a/compiler/Config.ml b/compiler/Config.ml
index 15818938..ce9b0e0c 100644
--- a/compiler/Config.ml
+++ b/compiler/Config.ml
@@ -3,9 +3,9 @@
 (** {1 Backend choice} *)
 
 (** The choice of backend *)
-type backend = FStar | Coq | Lean
+type backend = FStar | Coq | Lean | HOL4
 
-let backend_names = [ "fstar"; "coq"; "lean" ]
+let backend_names = [ "fstar"; "coq"; "lean"; "hol4" ]
 
 (** Utility to compute the backend from an input parameter *)
 let backend_of_string (b : string) : backend option =
@@ -13,6 +13,7 @@ let backend_of_string (b : string) : backend option =
   | "fstar" -> Some FStar
   | "coq" -> Some Coq
   | "lean" -> Some Lean
+  | "hol4" -> Some HOL4
   | _ -> None
 
 let opt_backend : backend option ref = ref None
diff --git a/compiler/Driver.ml b/compiler/Driver.ml
index d8418278..2ff9e295 100644
--- a/compiler/Driver.ml
+++ b/compiler/Driver.ml
@@ -158,6 +158,11 @@ let () =
         if !use_fuel then (
           log#error "The Lean backend doesn't support the -use-fuel option";
           fail ())
+    | HOL4 ->
+        (* We don't support fuel for the HOL4 backend *)
+        if !use_fuel then (
+          log#error "The HOL4 backend doesn't support the -use-fuel option";
+          fail ())
   in
 
   (* Retrieve and check the filename *)
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 03c256ec..0decbff1 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -16,7 +16,7 @@ module F = Format
 let int_name (int_ty : integer_type) =
   let isize, usize, i_format, u_format =
     match !backend with
-    | FStar | Coq ->
+    | FStar | Coq | HOL4 ->
         ("isize", "usize", format_of_string "i%d", format_of_string "u%d")
     | Lean -> ("Isize", "Usize", format_of_string "I%d", format_of_string "U%d")
   in
@@ -37,14 +37,15 @@ let int_name (int_ty : integer_type) =
 (** Small helper to compute the name of a unary operation *)
 let unop_name (unop : unop) : string =
   match unop with
-  | Not -> ( match !backend with FStar | Lean -> "not" | Coq -> "negb")
+  | Not -> (
+      match !backend with FStar | Lean -> "not" | Coq -> "negb" | HOL4 -> "~")
   | Neg (int_ty : integer_type) -> (
       match !backend with Lean -> "-" | _ -> int_name int_ty ^ "_neg")
   | Cast _ -> raise (Failure "Unsupported")
 
 (** Small helper to compute the name of a binary operation (note that many
     binary operations like "less than" are extracted to primitive operations,
-    like [<].
+    like [<]).
  *)
 let named_binop_name (binop : E.binop) (int_ty : integer_type) : string =
   let binop =
@@ -54,12 +55,16 @@ let named_binop_name (binop : E.binop) (int_ty : integer_type) : string =
     | Add -> "add"
     | Sub -> "sub"
     | Mul -> "mul"
+    | Lt -> "lt"
+    | Le -> "le"
+    | Ge -> "ge"
+    | Gt -> "gt"
     | _ -> raise (Failure "Unreachable")
   in
   (* Remark: the Lean case is actually not used *)
   match !backend with
   | Lean -> int_name int_ty ^ "." ^ binop
-  | FStar | Coq -> int_name int_ty ^ "_" ^ binop
+  | FStar | Coq | HOL4 -> int_name int_ty ^ "_" ^ binop
 
 (** A list of keywords/identifiers used by the backend and with which we
     want to check collision.
@@ -185,6 +190,28 @@ let keywords () =
           "with";
           "opaque_defs";
         ]
+    | HOL4 ->
+        [
+          "Axiom";
+          "case";
+          "Definition";
+          "else";
+          "End";
+          "fix";
+          "fix_exec";
+          "fn";
+          "fun";
+          "if";
+          "in";
+          "int";
+          "Inductive";
+          "let";
+          "of";
+          "Proof";
+          "QED";
+          "then";
+          "Theorem";
+        ]
   in
   List.concat [ named_unops; named_binops; misc ]
 
@@ -215,6 +242,15 @@ let assumed_adts () : (assumed_ty * string) list =
           (Fuel, "nat");
           (Option, "option");
           (Vec, "vec");
+        ]
+    | HOL4 ->
+        [
+          (State, "state");
+          (Result, "result");
+          (Error, "error");
+          (Fuel, "num");
+          (Option, "OPTION");
+          (Vec, "vec");
         ])
 
 let assumed_structs : (assumed_ty * string) list = []
@@ -253,6 +289,16 @@ let assumed_variants () : (assumed_ty * VariantId.id * string) list =
         (Option, option_some_id, "some");
         (Option, option_none_id, "none");
       ]
+  | HOL4 ->
+      [
+        (Result, result_return_id, "Return");
+        (Result, result_fail_id, "Fail");
+        (Error, error_failure_id, "Failure");
+        (* No Fuel::Zero on purpose *)
+        (* No Fuel::Succ on purpose *)
+        (Option, option_some_id, "SOME");
+        (Option, option_none_id, "NONE");
+      ]
 
 let assumed_llbc_functions :
     (A.assumed_fun_id * T.RegionGroupId.id option * string) list =
@@ -288,6 +334,9 @@ let assumed_pure_functions () : (pure_assumed_fun_id * string) list =
   | Lean ->
       (* We don't provide [FuelDecrease] and [FuelEqZero] on purpose *)
       [ (Return, "return"); (Fail, "fail_"); (Assert, "massert") ]
+  | HOL4 ->
+      (* We don't provide [FuelDecrease] and [FuelEqZero] on purpose *)
+      [ (Return, "return"); (Fail, "fail"); (Assert, "massert") ]
 
 let names_map_init () : names_map_init =
   {
@@ -310,37 +359,60 @@ let extract_unop (extract_expr : bool -> texpression -> unit)
       F.pp_print_space fmt ();
       extract_expr true arg;
       if inside then F.pp_print_string fmt ")"
-  | Cast (src, tgt) ->
-      (* The source type is an implicit parameter *)
-      if inside then F.pp_print_string fmt "(";
-      let cast_str =
-        match !backend with
-        | Coq | FStar -> "scalar_cast"
-        | Lean -> (* TODO: I8.cast, I16.cast, etc.*) "Scalar.cast"
-      in
-      F.pp_print_string fmt cast_str;
-      F.pp_print_space fmt ();
-      if !backend <> Lean then (
-        F.pp_print_string fmt
-          (StringUtils.capitalize_first_letter
-             (PrintPure.integer_type_to_string src));
-        F.pp_print_space fmt ());
-      if !backend = Lean then F.pp_print_string fmt ("." ^ int_name tgt)
-      else
-        F.pp_print_string fmt
-          (StringUtils.capitalize_first_letter
-             (PrintPure.integer_type_to_string tgt));
-      F.pp_print_space fmt ();
-      extract_expr true arg;
-      if inside then F.pp_print_string fmt ")"
+  | Cast (src, tgt) -> (
+      (* HOL4 has a special treatment: because it doesn't support dependent
+         types, we don't have a specific operator for the cast *)
+      match !backend with
+      | HOL4 ->
+          (* Casting, say, an u32 to an i32 would be done as follows:
+             {[
+               mk_i32 (u32_to_int x)
+             ]}
+          *)
+          if inside then F.pp_print_string fmt "(";
+          F.pp_print_string fmt ("mk_" ^ int_name tgt);
+          F.pp_print_space fmt ();
+          F.pp_print_string fmt "(";
+          F.pp_print_string fmt (int_name src ^ "_to_int");
+          F.pp_print_space fmt ();
+          extract_expr true arg;
+          F.pp_print_string fmt ")";
+          if inside then F.pp_print_string fmt ")"
+      | FStar | Coq | Lean ->
+          (* Rem.: the source type is an implicit parameter *)
+          if inside then F.pp_print_string fmt "(";
+          let cast_str =
+            match !backend with
+            | Coq | FStar -> "scalar_cast"
+            | Lean -> (* TODO: I8.cast, I16.cast, etc.*) "Scalar.cast"
+            | HOL4 -> raise (Failure "Unreachable")
+          in
+          F.pp_print_string fmt cast_str;
+          F.pp_print_space fmt ();
+          if !backend <> Lean then (
+            F.pp_print_string fmt
+              (StringUtils.capitalize_first_letter
+                 (PrintPure.integer_type_to_string src));
+            F.pp_print_space fmt ());
+          if !backend = Lean then F.pp_print_string fmt ("." ^ int_name tgt)
+          else
+            F.pp_print_string fmt
+              (StringUtils.capitalize_first_letter
+                 (PrintPure.integer_type_to_string tgt));
+          F.pp_print_space fmt ();
+          extract_expr true arg;
+          if inside then F.pp_print_string fmt ")")
 
+(** [extract_expr] : the boolean argument is [inside] *)
 let extract_binop (extract_expr : bool -> texpression -> unit)
     (fmt : F.formatter) (inside : bool) (binop : E.binop)
     (int_ty : integer_type) (arg0 : texpression) (arg1 : texpression) : unit =
   if inside then F.pp_print_string fmt "(";
   (* Some binary operations have a special notation depending on the backend *)
   (match (!backend, binop) with
-  | _, (Eq | Lt | Le | Ne | Ge | Gt) | Lean, (Div | Rem | Add | Sub | Mul) ->
+  | HOL4, (Eq | Ne)
+  | (FStar | Coq | Lean), (Eq | Lt | Le | Ne | Ge | Gt)
+  | Lean, (Div | Rem | Add | Sub | Mul) ->
       let binop =
         match binop with
         | Eq -> "="
@@ -357,87 +429,99 @@ let extract_binop (extract_expr : bool -> texpression -> unit)
         | _ -> raise (Failure "Unreachable")
       in
       let binop =
-        match !backend with FStar | Lean -> binop | Coq -> "s" ^ binop
+        match !backend with FStar | Lean | HOL4 -> binop | Coq -> "s" ^ binop
       in
       extract_expr false arg0;
       F.pp_print_space fmt ();
       F.pp_print_string fmt binop;
       F.pp_print_space fmt ();
       extract_expr false arg1
-  | _, (Div | Rem | Add | Sub | Mul) ->
+  | _, (Lt | Le | Ge | Gt | Div | Rem | Add | Sub | Mul) ->
       let binop = named_binop_name binop int_ty in
       F.pp_print_string fmt binop;
       F.pp_print_space fmt ();
-      extract_expr false arg0;
+      extract_expr true arg0;
       F.pp_print_space fmt ();
-      extract_expr false arg1
+      extract_expr true arg1
   | _, (BitXor | BitAnd | BitOr | Shl | Shr) -> raise Unimplemented);
   if inside then F.pp_print_string fmt ")"
 
 let type_decl_kind_to_qualif (kind : decl_kind)
-    (type_kind : type_decl_kind option) : string =
+    (type_kind : type_decl_kind option) : string option =
   match !backend with
   | FStar -> (
       match kind with
-      | SingleNonRec -> "type"
-      | SingleRec -> "type"
-      | MutRecFirst -> "type"
-      | MutRecInner -> "and"
-      | MutRecLast -> "and"
-      | Assumed -> "assume type"
-      | Declared -> "val")
+      | SingleNonRec -> Some "type"
+      | SingleRec -> Some "type"
+      | MutRecFirst -> Some "type"
+      | MutRecInner -> Some "and"
+      | MutRecLast -> Some "and"
+      | Assumed -> Some "assume type"
+      | Declared -> Some "val")
   | Coq -> (
       match (kind, type_kind) with
-      | SingleNonRec, Some Enum -> "Inductive"
-      | SingleNonRec, Some Struct -> "Record"
-      | (SingleRec | MutRecFirst), Some _ -> "Inductive"
+      | SingleNonRec, Some Enum -> Some "Inductive"
+      | SingleNonRec, Some Struct -> Some "Record"
+      | (SingleRec | MutRecFirst), Some _ -> Some "Inductive"
       | (MutRecInner | MutRecLast), Some _ ->
           (* Coq doesn't support groups of mutually recursive definitions which mix
            * records and inducties: we convert everything to records if this happens
            *)
-          "with"
-      | (Assumed | Declared), None -> "Axiom"
+          Some "with"
+      | (Assumed | Declared), None -> Some "Axiom"
       | _ -> raise (Failure "Unexpected"))
   | Lean -> (
       match kind with
       | SingleNonRec ->
-          if type_kind = Some Struct then "structure" else "inductive"
-      | SingleRec -> "inductive"
-      | MutRecFirst -> "mutual inductive"
-      | MutRecInner -> "inductive"
-      | MutRecLast -> "inductive" (* TODO: need to print end afterwards *)
-      | Assumed -> "axiom"
-      | Declared -> "axiom")
-
-let fun_decl_kind_to_qualif (kind : decl_kind) =
+          if type_kind = Some Struct then Some "structure" else Some "inductive"
+      | SingleRec -> Some "inductive"
+      | MutRecFirst -> Some "inductive"
+      | MutRecInner -> Some "inductive"
+      | MutRecLast -> Some "inductive"
+      | Assumed -> Some "axiom"
+      | Declared -> Some "axiom")
+  | HOL4 -> None
+
+let fun_decl_kind_to_qualif (kind : decl_kind) : string option =
   match !backend with
   | FStar -> (
       match kind with
-      | SingleNonRec -> "let"
-      | SingleRec -> "let rec"
-      | MutRecFirst -> "let rec"
-      | MutRecInner -> "and"
-      | MutRecLast -> "and"
-      | Assumed -> "assume val"
-      | Declared -> "val")
+      | SingleNonRec -> Some "let"
+      | SingleRec -> Some "let rec"
+      | MutRecFirst -> Some "let rec"
+      | MutRecInner -> Some "and"
+      | MutRecLast -> Some "and"
+      | Assumed -> Some "assume val"
+      | Declared -> Some "val")
   | Coq -> (
       match kind with
-      | SingleNonRec -> "Definition"
-      | SingleRec -> "Fixpoint"
-      | MutRecFirst -> "Fixpoint"
-      | MutRecInner -> "with"
-      | MutRecLast -> "with"
-      | Assumed -> "Axiom"
-      | Declared -> "Axiom")
+      | SingleNonRec -> Some "Definition"
+      | SingleRec -> Some "Fixpoint"
+      | MutRecFirst -> Some "Fixpoint"
+      | MutRecInner -> Some "with"
+      | MutRecLast -> Some "with"
+      | Assumed -> Some "Axiom"
+      | Declared -> Some "Axiom")
   | Lean -> (
       match kind with
-      | SingleNonRec -> "def"
-      | SingleRec -> "def"
-      | MutRecFirst -> "mutual def"
-      | MutRecInner -> "def"
-      | MutRecLast -> "def" (* TODO: need to print end afterwards *)
-      | Assumed -> "axiom"
-      | Declared -> "axiom")
+      | SingleNonRec -> Some "def"
+      | SingleRec -> Some "def"
+      | MutRecFirst -> Some "mutual def"
+      | MutRecInner -> Some "def"
+      | MutRecLast -> Some "def"
+      | Assumed -> Some "axiom"
+      | Declared -> Some "axiom")
+  | HOL4 -> None
+
+(** The type of types.
+
+    TODO: move inside the formatter?
+ *)
+let type_keyword () =
+  match !backend with
+  | FStar -> "Type0"
+  | Coq | Lean -> "Type"
+  | HOL4 -> raise (Failure "Unexpected")
 
 (**
    [ctx]: we use the context to lookup type definitions, to retrieve type names.
@@ -514,7 +598,7 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
     let name = List.map to_snake_case name in
     let name = String.concat "_" name in
     match !backend with
-    | FStar | Lean -> name
+    | FStar | Lean | HOL4 -> name
     | Coq -> capitalize_first_letter name
   in
   let type_name name = type_name_to_snake_case name ^ "_t" in
@@ -533,7 +617,9 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
   in
   let struct_constructor (basename : name) : string =
     let tname = type_name basename in
-    let prefix = match !backend with FStar -> "Mk" | Lean | Coq -> "mk" in
+    let prefix =
+      match !backend with FStar -> "Mk" | Lean | Coq | HOL4 -> "mk"
+    in
     prefix ^ tname
   in
   let get_fun_name = get_name in
@@ -569,7 +655,7 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
       match !Config.backend with
       | FStar -> "_decreases"
       | Lean -> "_terminates"
-      | Coq -> raise (Failure "Unexpected")
+      | Coq | HOL4 -> raise (Failure "Unexpected")
     in
     (* Concatenate *)
     fname ^ lp_suffix ^ suffix
@@ -583,14 +669,16 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
     let suffix =
       match !Config.backend with
       | Lean -> "_decreases"
-      | FStar | Coq -> raise (Failure "Unexpected")
+      | FStar | Coq | HOL4 -> raise (Failure "Unexpected")
     in
     (* Concatenate *)
     fname ^ lp_suffix ^ suffix
   in
 
   let opaque_pre () =
-    match !Config.backend with FStar | Coq -> "" | Lean -> "opaque_defs."
+    match !Config.backend with
+    | FStar | Coq | HOL4 -> ""
+    | Lean -> "opaque_defs."
   in
 
   let var_basename (_varset : StringSet.t) (basename : string option) (ty : ty)
@@ -637,7 +725,7 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
             (* TODO: use "t" also for F* *)
             match !backend with
             | FStar -> "x" (* lacking inspiration here... *)
-            | Coq | Lean -> "t" (* lacking inspiration here... *))
+            | Coq | Lean | HOL4 -> "t" (* lacking inspiration here... *))
         | Bool -> "b"
         | Char -> "c"
         | Integer _ -> "i"
@@ -651,6 +739,9 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
     | FStar ->
         (* This is *not* a no-op: this removes the capital letter *)
         to_snake_case basename
+    | HOL4 ->
+        (* In HOL4, type variable names must start with "'" *)
+        "'" ^ to_snake_case basename
     | Coq | Lean -> basename
   in
   let append_index (basename : string) (i : int) : string =
@@ -663,14 +754,24 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
     | Scalar sv -> (
         match !backend with
         | FStar -> F.pp_print_string fmt (Z.to_string sv.PV.value)
-        | Coq ->
-            if inside then F.pp_print_string fmt "(";
+        | Coq | HOL4 ->
+            let print_brackets = inside && !backend = HOL4 in
+            if print_brackets then F.pp_print_string fmt "(";
+            (match !backend with
+            | Coq -> ()
+            | HOL4 ->
+                F.pp_print_string fmt ("int_to_" ^ int_name sv.PV.int_ty);
+                F.pp_print_space fmt ()
+            | _ -> raise (Failure "Unreachable"));
             (* We need to add parentheses if the value is negative *)
             if sv.PV.value >= Z.of_int 0 then
               F.pp_print_string fmt (Z.to_string sv.PV.value)
             else F.pp_print_string fmt ("(" ^ Z.to_string sv.PV.value ^ ")");
-            F.pp_print_string fmt ("%" ^ int_name sv.PV.int_ty);
-            if inside then F.pp_print_string fmt ")"
+            (match !backend with
+            | Coq -> F.pp_print_string fmt ("%" ^ int_name sv.PV.int_ty)
+            | HOL4 -> ()
+            | _ -> raise (Failure "Unreachable"));
+            if print_brackets then F.pp_print_string fmt ")"
         | Lean ->
             F.pp_print_string fmt "(";
             F.pp_print_string fmt (int_name sv.int_ty);
@@ -694,6 +795,9 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
         F.pp_print_string fmt b
     | Char c -> (
         match !backend with
+        | HOL4 ->
+            (* [#"a"] is a notation for [CHR 97] (97 is the ASCII code for 'a') *)
+            F.pp_print_string fmt ("#\"" ^ String.make 1 c ^ "\"")
         | FStar | Lean -> F.pp_print_string fmt ("'" ^ String.make 1 c ^ "'")
         | Coq ->
             if inside then F.pp_print_string fmt "(";
@@ -750,32 +854,183 @@ let mk_formatter_and_names_map (ctx : trans_ctx) (crate_name : string)
   let names_map = initialize_names_map fmt (names_map_init ()) in
   (fmt, names_map)
 
+let is_single_opaque_fun_decl_group (dg : Pure.fun_decl list) : bool =
+  match dg with [ d ] -> d.body = None | _ -> false
+
+let is_single_opaque_type_decl_group (dg : Pure.type_decl list) : bool =
+  match dg with [ d ] -> d.kind = Opaque | _ -> false
+
+let is_empty_record_type_decl (d : Pure.type_decl) : bool = d.kind = Struct []
+
+let is_empty_record_type_decl_group (dg : Pure.type_decl list) : bool =
+  match dg with [ d ] -> is_empty_record_type_decl d | _ -> false
+
 (** In some provers, groups of definitions must be delimited.
 
     - in Coq, *every* group (including singletons) must end with "."
     - in Lean, groups of mutually recursive definitions must end with "end"
+    - in HOL4 (in most situations) the whole group must be within a `Define` command
+
+    Calls to {!extract_fun_decl} should be inserted between calls to
+    {!start_fun_decl_group} and {!end_fun_decl_group}.
+
+    TODO: maybe those [{start/end}_decl_group] functions are not that much a good
+    idea and we should merge them with the corresponding [extract_decl] functions.
  *)
-let print_decl_end_delimiter (fmt : F.formatter) (kind : decl_kind) =
-  if !backend = Coq && decl_is_last_from_group kind then (
-    F.pp_print_cut fmt ();
-    F.pp_print_string fmt ".")
-  else if !backend = Lean && kind = MutRecLast then (
-    F.pp_print_cut fmt ();
-    F.pp_print_string fmt "end")
+let start_fun_decl_group (ctx : extraction_ctx) (fmt : F.formatter)
+    (is_rec : bool) (dg : Pure.fun_decl list) =
+  match !backend with
+  | FStar | Coq | Lean -> ()
+  | HOL4 ->
+      (* In HOL4, opaque functions have a special treatment *)
+      if is_single_opaque_fun_decl_group dg then ()
+      else
+        let with_opaque_pre = false in
+        let compute_fun_def_name (def : Pure.fun_decl) : string =
+          ctx_get_local_function with_opaque_pre def.def_id def.loop_id
+            def.back_id ctx
+          ^ "_def"
+        in
+        let names = List.map compute_fun_def_name dg in
+        (* Add a break before *)
+        F.pp_print_break fmt 0 0;
+        (* Open the box for the delimiters *)
+        F.pp_open_vbox fmt 0;
+        (* Open the box for the definitions themselves *)
+        F.pp_open_vbox fmt ctx.indent_incr;
+        (* Print the delimiters *)
+        if is_rec then
+          F.pp_print_string fmt
+            ("val [" ^ String.concat ", " names ^ "] = DefineDiv ‘")
+        else (
+          assert (List.length names = 1);
+          let name = List.hd names in
+          F.pp_print_string fmt ("val " ^ name ^ " = Define ‘"));
+        F.pp_print_cut fmt ()
+
+(** See {!start_fun_decl_group}. *)
+let end_fun_decl_group (fmt : F.formatter) (is_rec : bool)
+    (dg : Pure.fun_decl list) =
+  match !backend with
+  | FStar -> ()
+  | Coq ->
+      (* For aesthetic reasons, we print the Coq end group delimiter directly
+         in {!extract_fun_decl}. *)
+      ()
+  | Lean ->
+      (* We must add the "end" keyword to groups of mutually recursive functions *)
+      if is_rec && List.length dg > 1 then (
+        F.pp_print_cut fmt ();
+        F.pp_print_string fmt "end";
+        (* Add breaks to insert new lines between definitions *)
+        F.pp_print_break fmt 0 0)
+      else ()
+  | HOL4 ->
+      (* In HOL4, opaque functions have a special treatment *)
+      if is_single_opaque_fun_decl_group dg then ()
+      else (
+        (* Close the box for the definitions *)
+        F.pp_close_box fmt ();
+        (* Print the end delimiter *)
+        F.pp_print_cut fmt ();
+        F.pp_print_string fmt "’";
+        (* Close the box for the delimiters *)
+        F.pp_close_box fmt ();
+        (* Add breaks to insert new lines between definitions *)
+        F.pp_print_break fmt 0 0)
 
-let unit_name () = match !backend with Lean -> "Unit" | Coq | FStar -> "unit"
+(** See {!start_fun_decl_group}: similar usage, but for the type declarations. *)
+let start_type_decl_group (ctx : extraction_ctx) (fmt : F.formatter)
+    (is_rec : bool) (dg : Pure.type_decl list) =
+  match !backend with
+  | FStar | Coq -> ()
+  | Lean ->
+      if is_rec && List.length dg > 1 then (
+        F.pp_print_space fmt ();
+        F.pp_print_string fmt "mutual";
+        F.pp_print_space fmt ())
+  | HOL4 ->
+      (* In HOL4, opaque types and empty records have a special treatment *)
+      if
+        is_single_opaque_type_decl_group dg
+        || is_empty_record_type_decl_group dg
+      then ()
+      else (
+        (* Add a break before *)
+        F.pp_print_break fmt 0 0;
+        (* Open the box for the delimiters *)
+        F.pp_open_vbox fmt 0;
+        (* Open the box for the definitions themselves *)
+        F.pp_open_vbox fmt ctx.indent_incr;
+        (* Print the delimiters *)
+        F.pp_print_string fmt "Datatype:";
+        F.pp_print_cut fmt ())
+
+(** See {!start_fun_decl_group}. *)
+let end_type_decl_group (fmt : F.formatter) (is_rec : bool)
+    (dg : Pure.type_decl list) =
+  match !backend with
+  | FStar -> ()
+  | Coq ->
+      (* For aesthetic reasons, we print the Coq end group delimiter directly
+         in {!extract_fun_decl}. *)
+      ()
+  | Lean ->
+      (* We must add the "end" keyword to groups of mutually recursive functions *)
+      if is_rec && List.length dg > 1 then (
+        F.pp_print_cut fmt ();
+        F.pp_print_string fmt "end";
+        (* Add breaks to insert new lines between definitions *)
+        F.pp_print_break fmt 0 0)
+      else ()
+  | HOL4 ->
+      (* In HOL4, opaque types and empty records have a special treatment *)
+      if
+        is_single_opaque_type_decl_group dg
+        || is_empty_record_type_decl_group dg
+      then ()
+      else (
+        (* Close the box for the definitions *)
+        F.pp_close_box fmt ();
+        (* Print the end delimiter *)
+        F.pp_print_cut fmt ();
+        F.pp_print_string fmt "End";
+        (* Close the box for the delimiters *)
+        F.pp_close_box fmt ();
+        (* Add breaks to insert new lines between definitions *)
+        F.pp_print_break fmt 0 0)
+
+let unit_name () =
+  match !backend with Lean -> "Unit" | Coq | FStar | HOL4 -> "unit"
 
 (** [inside] constrols whether we should add parentheses or not around type
     applications (if [true] we add parentheses).
+
+    [no_params_tys]: for all the types inside this set, do not print the type parameters.
+    This is used for HOL4. As polymorphism is uniform in HOL4, printing the
+    type parameters in the recursive definitions is useless (and actually
+    forbidden).
+
+    For instance, where in F* we would write:
+    {[
+      type list a = | Nil : list a | Cons : a -> list a -> list a
+    ]}
+
+    In HOL4 we would simply write:
+    {[
+      Datatype:
+        list = Nil 'a | Cons 'a list
+      End
+    ]}
  *)
-let rec extract_ty (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
-    (ty : ty) : unit =
-  let extract_rec = extract_ty ctx fmt in
+let rec extract_ty (ctx : extraction_ctx) (fmt : F.formatter)
+    (no_params_tys : TypeDeclId.Set.t) (inside : bool) (ty : ty) : unit =
+  let extract_rec = extract_ty ctx fmt no_params_tys in
   match ty with
   | Adt (type_id, tys) -> (
       match type_id with
       | Tuple ->
-          (* This is a bit annoying, but in F*/Coq [()] is not the unit type:
+          (* This is a bit annoying, but in F*/Coq/HOL4 [()] is not the unit type:
            * we have to write [unit]... *)
           if tys = [] then F.pp_print_string fmt (unit_name ())
           else (
@@ -784,23 +1039,54 @@ let rec extract_ty (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
               (fun () ->
                 F.pp_print_space fmt ();
                 let product =
-                  match !backend with FStar -> "&" | Coq -> "*" | Lean -> "×"
+                  match !backend with
+                  | FStar -> "&"
+                  | Coq -> "*"
+                  | Lean -> "×"
+                  | HOL4 -> "#"
                 in
                 F.pp_print_string fmt product;
                 F.pp_print_space fmt ())
               (extract_rec true) tys;
             F.pp_print_string fmt ")")
-      | AdtId _ | Assumed _ ->
-          let print_paren = inside && tys <> [] in
-          if print_paren then F.pp_print_string fmt "(";
-          (* TODO: for now, only the opaque *functions* are extracted in the
-             opaque module. The opaque *types* are assumed. *)
+      | AdtId _ | Assumed _ -> (
+          (* HOL4 behaves differently. Where in Coq/FStar/Lean we would write:
+             `tree a b`
+
+             In HOL4 we would write:
+             `('a, 'b) tree`
+          *)
           let with_opaque_pre = false in
-          F.pp_print_string fmt (ctx_get_type with_opaque_pre type_id ctx);
-          if tys <> [] then F.pp_print_space fmt ();
-          Collections.List.iter_link (F.pp_print_space fmt) (extract_rec true)
-            tys;
-          if print_paren then F.pp_print_string fmt ")")
+          match !backend with
+          | FStar | Coq | Lean ->
+              let print_paren = inside && tys <> [] in
+              if print_paren then F.pp_print_string fmt "(";
+              (* TODO: for now, only the opaque *functions* are extracted in the
+                 opaque module. The opaque *types* are assumed. *)
+              F.pp_print_string fmt (ctx_get_type with_opaque_pre type_id ctx);
+              if tys <> [] then (
+                F.pp_print_space fmt ();
+                Collections.List.iter_link (F.pp_print_space fmt)
+                  (extract_rec true) tys);
+              if print_paren then F.pp_print_string fmt ")"
+          | HOL4 ->
+              let print_tys =
+                match type_id with
+                | AdtId id -> not (TypeDeclId.Set.mem id no_params_tys)
+                | Assumed _ -> true
+                | _ -> raise (Failure "Unreachable")
+              in
+              if tys <> [] && print_tys then (
+                let print_paren = List.length tys > 1 in
+                if print_paren then F.pp_print_string fmt "(";
+                Collections.List.iter_link
+                  (fun () ->
+                    F.pp_print_string fmt ",";
+                    F.pp_print_space fmt ())
+                  (extract_rec true) tys;
+                if print_paren then F.pp_print_string fmt ")";
+                F.pp_print_space fmt ());
+              F.pp_print_string fmt (ctx_get_type with_opaque_pre type_id ctx)))
   | TypeVar vid -> F.pp_print_string fmt (ctx_get_type_var vid ctx)
   | Bool -> F.pp_print_string fmt ctx.fmt.bool_name
   | Char -> F.pp_print_string fmt ctx.fmt.char_name
@@ -855,18 +1141,20 @@ let extract_type_decl_register_names (ctx : extraction_ctx) (def : type_decl) :
 
 (** Print the variants *)
 let extract_type_decl_variant (ctx : extraction_ctx) (fmt : F.formatter)
-    (type_name : string) (type_params : string list) (cons_name : string)
-    (fields : field list) : unit =
+    (type_decl_group : TypeDeclId.Set.t) (type_name : string)
+    (type_params : string list) (cons_name : string) (fields : field list) :
+    unit =
   F.pp_print_space fmt ();
   (* variant box *)
   F.pp_open_hvbox fmt ctx.indent_incr;
   (* [| Cons :]
    * Note that we really don't want any break above so we print everything
    * at once. *)
-  F.pp_print_string fmt ("| " ^ cons_name ^ " :");
-  F.pp_print_space fmt ();
+  let opt_colon = if !backend <> HOL4 then " :" else "" in
+  F.pp_print_string fmt ("| " ^ cons_name ^ opt_colon);
   let print_field (fid : FieldId.id) (f : field) (ctx : extraction_ctx) :
       extraction_ctx =
+    F.pp_print_space fmt ();
     (* Open the field box *)
     F.pp_open_box fmt ctx.indent_incr;
     (* Print the field names, if the backend accepts it.
@@ -888,16 +1176,17 @@ let extract_type_decl_variant (ctx : extraction_ctx) (fmt : F.formatter)
               F.pp_print_string fmt (field_name ^ " :");
               F.pp_print_space fmt ();
               ctx)
-      | Coq | Lean -> ctx
+      | Coq | Lean | HOL4 -> ctx
     in
     (* Print the field type *)
-    extract_ty ctx fmt false f.field_ty;
-    (* Print the arrow [->]*)
-    F.pp_print_space fmt ();
-    F.pp_print_string fmt "->";
+    let inside = !backend = HOL4 in
+    extract_ty ctx fmt type_decl_group inside f.field_ty;
+    (* Print the arrow [->] *)
+    if !backend <> HOL4 then (
+      F.pp_print_space fmt ();
+      F.pp_print_string fmt "->");
     (* Close the field box *)
     F.pp_close_box fmt ();
-    F.pp_print_space fmt ();
     (* Return *)
     ctx
   in
@@ -907,21 +1196,23 @@ let extract_type_decl_variant (ctx : extraction_ctx) (fmt : F.formatter)
     List.fold_left (fun ctx (fid, f) -> print_field fid f ctx) ctx fields
   in
   (* Print the final type *)
-  F.pp_open_hovbox fmt 0;
-  F.pp_print_string fmt type_name;
-  List.iter
-    (fun type_param ->
-      F.pp_print_space fmt ();
-      F.pp_print_string fmt type_param)
-    type_params;
-  F.pp_close_box fmt ();
+  if !backend <> HOL4 then (
+    F.pp_print_space fmt ();
+    F.pp_open_hovbox fmt 0;
+    F.pp_print_string fmt type_name;
+    List.iter
+      (fun type_param ->
+        F.pp_print_space fmt ();
+        F.pp_print_string fmt type_param)
+      type_params;
+    F.pp_close_box fmt ());
   (* Close the variant box *)
   F.pp_close_box fmt ()
 
 (* TODO: we don' need the [def_name] paramter: it can be retrieved from the context *)
 let extract_type_decl_enum_body (ctx : extraction_ctx) (fmt : F.formatter)
-    (def : type_decl) (def_name : string) (type_params : string list)
-    (variants : variant list) : unit =
+    (type_decl_group : TypeDeclId.Set.t) (def : type_decl) (def_name : string)
+    (type_params : string list) (variants : variant list) : unit =
   (* We want to generate a definition which looks like this (taking F* as example):
      {[
        type list a = | Cons : a -> list a -> list a | Nil : list a
@@ -959,15 +1250,16 @@ let extract_type_decl_enum_body (ctx : extraction_ctx) (fmt : F.formatter)
        id (in the case of Lean) *)
     let cons_name = ctx.fmt.variant_name def.name v.variant_name in
     let fields = v.fields in
-    extract_type_decl_variant ctx fmt def_name type_params cons_name fields
+    extract_type_decl_variant ctx fmt type_decl_group def_name type_params
+      cons_name fields
   in
   (* Print the variants *)
   let variants = VariantId.mapi (fun vid v -> (vid, v)) variants in
   List.iter (fun (vid, v) -> print_variant vid v) variants
 
 let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter)
-    (kind : decl_kind) (def : type_decl) (type_params : string list)
-    (fields : field list) : unit =
+    (type_decl_group : TypeDeclId.Set.t) (kind : decl_kind) (def : type_decl)
+    (type_params : string list) (fields : field list) : unit =
   (* We want to generate a definition which looks like this (taking F* as example):
      {[
        type t = { x : int; y : bool; }
@@ -1007,6 +1299,20 @@ let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter)
      expanded which introduces let bindings of the form: [let RecordCons ... = x in ...].
      As a consequence, we never use the record projectors (unless we reconstruct
      them in the micro passes of course).
+
+     HOL4:
+     =====
+     Type definitions are written as follows:
+     {[
+       Datatype:
+         tree =
+           TLeaf 'a
+         | TNode node ;
+
+         node =
+           Node (tree list)
+       End
+     ]}
   *)
   (* Note that we already printed: [type t =] *)
   let is_rec = decl_is_from_rec_group kind in
@@ -1026,12 +1332,15 @@ let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter)
         F.pp_print_string fmt
           (ctx_get_struct with_opaque_pre (AdtId def.def_id) ctx);
         F.pp_print_string fmt " ");
-      if !backend <> Lean then F.pp_print_string fmt "{";
+      (match !backend with
+      | Lean -> ()
+      | FStar | Coq -> F.pp_print_string fmt "{"
+      | HOL4 -> F.pp_print_string fmt "<|");
       F.pp_print_break fmt 1 ctx.indent_incr;
       (* The body itself *)
       (* Open a box for the body *)
       (match !backend with
-      | Coq | FStar -> F.pp_open_hvbox fmt 0
+      | Coq | FStar | HOL4 -> F.pp_open_hvbox fmt 0
       | Lean -> F.pp_open_vbox fmt 0);
       (* Print the fields *)
       let print_field (field_id : FieldId.id) (f : field) : unit =
@@ -1042,7 +1351,7 @@ let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter)
         F.pp_print_space fmt ();
         F.pp_print_string fmt ":";
         F.pp_print_space fmt ();
-        extract_ty ctx fmt false f.field_ty;
+        extract_ty ctx fmt type_decl_group false f.field_ty;
         if !backend <> Lean then F.pp_print_string fmt ";";
         (* Close the box for the field *)
         F.pp_close_box fmt ()
@@ -1053,9 +1362,14 @@ let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter)
         fields;
       (* Close the box for the body *)
       F.pp_close_box fmt ();
-      if !backend <> Lean then (
-        F.pp_print_space fmt ();
-        F.pp_print_string fmt "}"))
+      match !backend with
+      | Lean -> ()
+      | FStar | Coq ->
+          F.pp_print_space fmt ();
+          F.pp_print_string fmt "}"
+      | HOL4 ->
+          F.pp_print_space fmt ();
+          F.pp_print_string fmt "|>")
     else (
       (* We extract for Coq or Lean, and we have a recursive record, or a record in
          a group of mutually recursive types: we extract it as an inductive type *)
@@ -1063,14 +1377,15 @@ let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter)
       let with_opaque_pre = false in
       let cons_name = ctx_get_struct with_opaque_pre (AdtId def.def_id) ctx in
       let def_name = ctx_get_local_type with_opaque_pre def.def_id ctx in
-      extract_type_decl_variant ctx fmt def_name type_params cons_name fields)
+      extract_type_decl_variant ctx fmt type_decl_group def_name type_params
+        cons_name fields)
   in
   ()
 
 (** Extract a nestable, muti-line comment *)
 let extract_comment (fmt : F.formatter) (s : string) : unit =
   match !backend with
-  | Coq | FStar ->
+  | Coq | FStar | HOL4 ->
       F.pp_print_string fmt "(** ";
       F.pp_print_string fmt s;
       F.pp_print_string fmt " *)"
@@ -1081,16 +1396,16 @@ let extract_comment (fmt : F.formatter) (s : string) : unit =
 
 (** Extract a type declaration.
 
-    Note that all the names used for extraction should already have been
-    registered.
+    This function is for all type declarations and all backends **at the exception**
+    of opaque (assumed/declared) types format4 HOL4.
+
+    See {!extract_type_decl}.
  *)
-let extract_type_decl (ctx : extraction_ctx) (fmt : F.formatter)
-    (kind : decl_kind) (def : type_decl) : unit =
-  let extract_body =
-    match kind with
-    | SingleNonRec | SingleRec | MutRecFirst | MutRecInner | MutRecLast -> true
-    | Assumed | Declared -> false
-  in
+let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
+    (type_decl_group : TypeDeclId.Set.t) (kind : decl_kind) (def : type_decl)
+    (extract_body : bool) : unit =
+  (* Sanity check *)
+  assert (extract_body || !backend <> HOL4);
   let type_kind =
     if extract_body then
       match def.kind with
@@ -1114,7 +1429,8 @@ let extract_type_decl (ctx : extraction_ctx) (fmt : F.formatter)
    * body translation (they are not top-level) *)
   let ctx_body, type_params = ctx_add_type_params def.type_params ctx in
   (* Add a break before *)
-  F.pp_print_break fmt 0 0;
+  if !backend <> HOL4 || not (decl_is_first_from_group kind) then
+    F.pp_print_break fmt 0 0;
   (* Print a comment to link the extracted type to its original rust definition *)
   extract_comment fmt ("[" ^ Print.name_to_string def.name ^ "]");
   F.pp_print_break fmt 0 0;
@@ -1122,18 +1438,17 @@ let extract_type_decl (ctx : extraction_ctx) (fmt : F.formatter)
    * one line. Note however that in the case of Lean line breaks are important
    * for parsing: we thus use a hovbox. *)
   (match !backend with
-  | Coq | FStar -> F.pp_open_hvbox fmt 0
+  | Coq | FStar | HOL4 -> F.pp_open_hvbox fmt 0
   | Lean -> F.pp_open_vbox fmt 0);
   (* Open a box for "type TYPE_NAME (TYPE_PARAMS) =" *)
   F.pp_open_hovbox fmt ctx.indent_incr;
   (* > "type TYPE_NAME" *)
   let qualif = ctx.fmt.type_decl_kind_to_qualif kind type_kind in
-  F.pp_print_string fmt (qualif ^ " " ^ def_name);
+  (match qualif with
+  | Some qualif -> F.pp_print_string fmt (qualif ^ " " ^ def_name)
+  | None -> F.pp_print_string fmt def_name);
   (* Print the type parameters *)
-  let type_keyword =
-    match !backend with FStar -> "Type0" | Coq | Lean -> "Type"
-  in
-  if def.type_params <> [] then (
+  if def.type_params <> [] && !backend <> HOL4 then (
     if use_forall then (
       F.pp_print_space fmt ();
       F.pp_print_string fmt ":";
@@ -1149,7 +1464,7 @@ let extract_type_decl (ctx : extraction_ctx) (fmt : F.formatter)
       def.type_params;
     F.pp_print_string fmt ":";
     F.pp_print_space fmt ();
-    F.pp_print_string fmt (type_keyword ^ ")"));
+    F.pp_print_string fmt (type_keyword () ^ ")"));
   (* Print the "=" if we extract the body*)
   if extract_body then (
     F.pp_print_space fmt ();
@@ -1160,32 +1475,107 @@ let extract_type_decl (ctx : extraction_ctx) (fmt : F.formatter)
       | Lean ->
           if type_kind = Some Struct && kind = SingleNonRec then "where"
           else ":="
+      | HOL4 -> "="
     in
     F.pp_print_string fmt eq)
   else (
-    (* Otherwise print ": Type" *)
+    (* Otherwise print ": Type", unless it is the HOL4 backend (in
+       which case we declare the type with `new_type`) *)
     if use_forall then F.pp_print_string fmt ","
     else (
       F.pp_print_space fmt ();
       F.pp_print_string fmt ":");
     F.pp_print_space fmt ();
-    F.pp_print_string fmt type_keyword);
+    F.pp_print_string fmt (type_keyword ()));
   (* Close the box for "type TYPE_NAME (TYPE_PARAMS) =" *)
   F.pp_close_box fmt ();
   (if extract_body then
-   match def.kind with
-   | Struct fields ->
-       extract_type_decl_struct_body ctx_body fmt kind def type_params fields
-   | Enum variants ->
-       extract_type_decl_enum_body ctx_body fmt def def_name type_params
-         variants
-   | Opaque -> raise (Failure "Unreachable"));
-  (* If Coq: end the definition with a "." *)
-  print_decl_end_delimiter fmt kind;
+     match def.kind with
+     | Struct fields ->
+         extract_type_decl_struct_body ctx_body fmt type_decl_group kind def
+           type_params fields
+     | Enum variants ->
+         extract_type_decl_enum_body ctx_body fmt type_decl_group def def_name
+           type_params variants
+     | Opaque -> raise (Failure "Unreachable"));
+  (* Add the definition end delimiter *)
+  if !backend = HOL4 && decl_is_not_last_from_group kind then (
+    F.pp_print_space fmt ();
+    F.pp_print_string fmt ";")
+  else if !backend = Coq && decl_is_last_from_group kind then (
+    (* This is actually an end of group delimiter. For aesthetic reasons
+       we print it here instead of in {!end_type_decl_group}. *)
+    F.pp_print_cut fmt ();
+    F.pp_print_string fmt ".");
   (* Close the box for the definition *)
   F.pp_close_box fmt ();
   (* Add breaks to insert new lines between definitions *)
-  F.pp_print_break fmt 0 0
+  if !backend <> HOL4 || decl_is_not_last_from_group kind then
+    F.pp_print_break fmt 0 0
+
+(** Extract an opaque type declaration to HOL4.
+
+    Remark (SH): having to treat this specific case separately is very annoying,
+    but I could not find a better way.
+ *)
+let extract_type_decl_hol4_opaque (ctx : extraction_ctx) (fmt : F.formatter)
+    (def : type_decl) : unit =
+  (* Retrieve the definition name *)
+  let with_opaque_pre = false in
+  let def_name = ctx_get_local_type with_opaque_pre def.def_id ctx in
+  (* Count the number of parameters *)
+  let num_params = List.length def.type_params in
+  (* Generate the declaration *)
+  F.pp_print_space fmt ();
+  F.pp_print_string fmt
+    ("val _ = new_type (\"" ^ def_name ^ ", " ^ string_of_int num_params ^ ")");
+  F.pp_print_space fmt ()
+
+(** Extract an empty record type declaration to HOL4.
+
+    Empty records are not supported in HOL4, so we extract them as type
+    abbreviations to the unit type.
+
+    Remark (SH): having to treat this specific case separately is very annoying,
+    but I could not find a better way.
+ *)
+let extract_type_decl_hol4_empty_record (ctx : extraction_ctx)
+    (fmt : F.formatter) (def : type_decl) : unit =
+  (* Retrieve the definition name *)
+  let with_opaque_pre = false in
+  let def_name = ctx_get_local_type with_opaque_pre def.def_id ctx in
+  (* Sanity check *)
+  assert (def.type_params = []);
+  (* Generate the declaration *)
+  F.pp_print_space fmt ();
+  F.pp_print_string fmt ("Type " ^ def_name ^ " = “: unit”");
+  F.pp_print_space fmt ()
+
+(** Extract a type declaration.
+
+    Note that all the names used for extraction should already have been
+    registered.
+
+    This function should be inserted between calls to {!start_type_decl_group}
+    and {!end_type_decl_group}.
+ *)
+let extract_type_decl (ctx : extraction_ctx) (fmt : F.formatter)
+    (type_decl_group : TypeDeclId.Set.t) (kind : decl_kind) (def : type_decl) :
+    unit =
+  let extract_body =
+    match kind with
+    | SingleNonRec | SingleRec | MutRecFirst | MutRecInner | MutRecLast -> true
+    | Assumed | Declared -> false
+  in
+  if extract_body then
+    if !backend = HOL4 && is_empty_record_type_decl def then
+      extract_type_decl_hol4_empty_record ctx fmt def
+    else extract_type_decl_gen ctx fmt type_decl_group kind def extract_body
+  else
+    match !backend with
+    | FStar | Coq | Lean ->
+        extract_type_decl_gen ctx fmt type_decl_group kind def extract_body
+    | HOL4 -> extract_type_decl_hol4_opaque ctx fmt def
 
 (** Auxiliary function.
 
@@ -1370,7 +1760,9 @@ let extract_type_decl_record_field_projectors (ctx : extraction_ctx)
           (* Close the inner box projector *)
           F.pp_close_box fmt ();
           (* If Coq: end the definition with a "." *)
-          print_decl_end_delimiter fmt kind;
+          if !backend = Coq then (
+            F.pp_print_cut fmt ();
+            F.pp_print_string fmt ".");
           (* Close the outer box projector  *)
           F.pp_close_box fmt ();
           (* Add breaks to insert new lines between definitions *)
@@ -1401,7 +1793,9 @@ let extract_type_decl_record_field_projectors (ctx : extraction_ctx)
           (* Close the inner box projector *)
           F.pp_close_box fmt ();
           (* If Coq: end the definition with a "." *)
-          print_decl_end_delimiter fmt kind;
+          if !backend = Coq then (
+            F.pp_print_cut fmt ();
+            F.pp_print_string fmt ".");
           (* Close the outer box projector  *)
           F.pp_close_box fmt ();
           (* Add breaks to insert new lines between definitions *)
@@ -1424,7 +1818,7 @@ let extract_type_decl_record_field_projectors (ctx : extraction_ctx)
 let extract_type_decl_extra_info (ctx : extraction_ctx) (fmt : F.formatter)
     (kind : decl_kind) (decl : type_decl) : unit =
   match !backend with
-  | FStar | Lean -> ()
+  | FStar | Lean | HOL4 -> ()
   | Coq ->
       extract_type_decl_coq_arguments ctx fmt kind decl;
       extract_type_decl_record_field_projectors ctx fmt kind decl
@@ -1448,7 +1842,7 @@ let extract_state_type (fmt : F.formatter) (ctx : extraction_ctx)
       match !backend with
       | Coq -> "Axiom"
       | Lean -> "axiom"
-      | FStar -> raise (Failure "Unexpected")
+      | FStar | HOL4 -> raise (Failure "Unexpected")
     in
     F.pp_print_string fmt axiom;
     F.pp_print_space fmt ();
@@ -1475,6 +1869,8 @@ let extract_state_type (fmt : F.formatter) (ctx : extraction_ctx)
           F.pp_print_string fmt ":";
           F.pp_print_space fmt ();
           F.pp_print_string fmt "Type0"
+      | HOL4 ->
+          F.pp_print_string fmt ("val _ = new_type (" ^ state_name ^ ", 0)")
       | Coq | Lean -> print_axiom ())
   | Declared -> (
       match !backend with
@@ -1486,12 +1882,24 @@ let extract_state_type (fmt : F.formatter) (ctx : extraction_ctx)
           F.pp_print_string fmt ":";
           F.pp_print_space fmt ();
           F.pp_print_string fmt "Type0"
+      | HOL4 ->
+          F.pp_print_string fmt ("val _ = new_type (" ^ state_name ^ ", 0)")
       | Coq | Lean -> print_axiom ()));
   (* Close the box for the definition *)
   F.pp_close_box fmt ();
   (* Add breaks to insert new lines between definitions *)
   F.pp_print_break fmt 0 0
 
+(** In some provers like HOL4, we don't print the type parameters when calling
+    functions (and the polymorphism is uniform...).
+
+    TODO: we may want to check that the polymorphism is indeed uniform when
+    generating code for such backends, and print at least a warning to the
+    user when it is not the case.
+ *)
+let print_fun_type_params () : bool =
+  match !backend with FStar | Coq | Lean -> true | HOL4 -> false
+
 (** Compute the names for all the pure functions generated from a rust function
     (forward function and backward functions).
  *)
@@ -1507,6 +1915,7 @@ let extract_fun_decl_register_names (ctx : extraction_ctx) (keep_fwd : bool)
       (* Add the decreases proof for Lean only *)
       match !Config.backend with
       | Coq | FStar -> ctx
+      | HOL4 -> raise (Failure "Unexpected")
       | Lean -> ctx_add_decreases_proof def ctx
     else ctx
   in
@@ -1729,12 +2138,13 @@ and extract_function_call (ctx : extraction_ctx) (fmt : F.formatter)
       let with_opaque_pre = ctx.use_opaque_pre in
       let fun_name = ctx_get_function with_opaque_pre fun_id ctx in
       F.pp_print_string fmt fun_name;
-      (* Print the type parameters *)
-      List.iter
-        (fun ty ->
-          F.pp_print_space fmt ();
-          extract_ty ctx fmt true ty)
-        type_args;
+      (* Print the type parameters, if the backend is not HOL4 *)
+      if !backend <> HOL4 then
+        List.iter
+          (fun ty ->
+            F.pp_print_space fmt ();
+            extract_ty ctx fmt TypeDeclId.Set.empty true ty)
+          type_args;
       (* Print the arguments *)
       List.iter
         (fun ve ->
@@ -1787,9 +2197,8 @@ and extract_field_projector (ctx : extraction_ctx) (fmt : F.formatter)
       F.pp_print_string fmt ".";
       (* If in Coq, the field projection has to be parenthesized *)
       (match !backend with
-      | FStar -> F.pp_print_string fmt field_name
-      | Coq -> F.pp_print_string fmt ("(" ^ field_name ^ ")")
-      | Lean -> F.pp_print_string fmt field_name);
+      | FStar | Lean | HOL4 -> F.pp_print_string fmt field_name
+      | Coq -> F.pp_print_string fmt ("(" ^ field_name ^ ")"));
       (* Close the box *)
       F.pp_close_box fmt ()
   | arg :: args ->
@@ -1843,7 +2252,6 @@ and extract_lets (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
       (re : texpression) : extraction_ctx =
     (* Open a box for the let-binding *)
     F.pp_open_hovbox fmt ctx.indent_incr;
-    let is_fstar_monadic = monadic && !backend = FStar in
     let ctx =
       (* There are two cases:
        * - do we use a notation like [x <-- y;]
@@ -1861,7 +2269,7 @@ and extract_lets (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
         let arrow =
           match !backend with
           | Coq -> "<-"
-          | FStar | Lean -> failwith "impossible"
+          | FStar | Lean | HOL4 -> raise (Failure "impossible")
         in
         F.pp_print_string fmt arrow;
         F.pp_print_space fmt ();
@@ -1869,24 +2277,42 @@ and extract_lets (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
         F.pp_print_string fmt ";";
         ctx)
       else (
-        F.pp_print_string fmt (if is_fstar_monadic then "let*" else "let");
-        F.pp_print_space fmt ();
+        (* Print the "let" *)
+        if monadic then
+          match !backend with
+          | FStar ->
+              F.pp_print_string fmt "let*";
+              F.pp_print_space fmt ()
+          | Coq | Lean ->
+              F.pp_print_string fmt "let";
+              F.pp_print_space fmt ()
+          | HOL4 -> ()
+        else (
+          F.pp_print_string fmt "let";
+          F.pp_print_space fmt ());
         let ctx = extract_typed_pattern ctx fmt true lv in
         F.pp_print_space fmt ();
         let eq =
           match !backend with
           | FStar -> "="
           | Coq -> ":="
-          (* TODO: switch to ⟵ once issues are fixed *)
-          | Lean -> if monadic then "←" else ":="
+          | Lean ->
+              (* TODO: switch to ⟵ once issues are fixed *)
+              if monadic then "←" else ":="
+          | HOL4 -> if monadic then "<-" else "="
         in
         F.pp_print_string fmt eq;
         F.pp_print_space fmt ();
         extract_texpression ctx fmt false re;
-        (* In Lean, monadic let-bindings don't require to end with "in" *)
-        if !backend <> Lean then (
-          F.pp_print_space fmt ();
-          F.pp_print_string fmt "in");
+        (* End the monadic let-binding *)
+        (match !backend with
+        | Lean ->
+            (* In Lean, monadic let-bindings don't require to end with anything *)
+            ()
+        | Coq | FStar ->
+            F.pp_print_space fmt ();
+            F.pp_print_string fmt "in"
+        | HOL4 -> F.pp_print_string fmt ";");
         ctx)
     in
     (* Close the box for the let-binding *)
@@ -1896,10 +2322,10 @@ and extract_lets (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
     ctx
   in
   let exists_monadic = List.exists (fun (m, _, _) -> m) lets in
-  (* If Lean, we rely on monadic blocks, so we insert a do and open a new box
+  (* If Lean and HOL4, we rely on monadic blocks, so we insert a do and open a new box
      immediately *)
-  if !backend = Lean && exists_monadic then (
-    F.pp_open_vbox fmt ctx.indent_incr;
+  if (!backend = Lean || !backend = HOL4) && exists_monadic then (
+    F.pp_open_vbox fmt (if !backend = Lean then ctx.indent_incr else 0);
     F.pp_print_string fmt "do";
     F.pp_print_space fmt ());
   let ctx =
@@ -1913,23 +2339,29 @@ and extract_lets (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
   extract_texpression ctx fmt false next_e;
   (* Close the box for the next expression *)
   F.pp_close_box fmt ();
-  (* do-box (Lean only) *)
-  if !backend = Lean && exists_monadic then F.pp_close_box fmt ();
+
+  (* do-box (Lean and HOL4 only) *)
+  if (!backend = Lean || !backend = HOL4) && exists_monadic then (
+    if !backend = HOL4 then (
+      F.pp_print_space fmt ();
+      F.pp_print_string fmt "od");
+    F.pp_close_box fmt ());
   (* Close parentheses *)
   if inside && !backend <> Lean then F.pp_print_string fmt ")";
   (* Close the box for the whole expression *)
   F.pp_close_box fmt ()
 
-and extract_Switch (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
+and extract_Switch (ctx : extraction_ctx) (fmt : F.formatter) (_inside : bool)
     (scrut : texpression) (body : switch_body) : unit =
+  (* Remark: we don't use the [inside] parameter because we extract matches in
+     a conservative manner: we always make sure they are parenthesized/delimited
+     with keywords such as [end] *)
   (* Open a box for the whole expression.
 
      In the case of Lean, we rely on indentation to delimit the end of the
      branches, and need to insert line breaks: we thus use a vbox.
   *)
   if !Config.backend = Lean then F.pp_open_vbox fmt 0 else F.pp_open_hvbox fmt 0;
-  (* Open parentheses *)
-  if inside then F.pp_print_string fmt "(";
   (* Extract the switch *)
   (match body with
   | If (e_then, e_else) ->
@@ -1961,7 +2393,7 @@ and extract_Switch (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
                 F.pp_print_space fmt ();
                 F.pp_print_string fmt "begin";
                 F.pp_print_space fmt
-            | Coq | Lean ->
+            | Coq | Lean | HOL4 ->
                 F.pp_print_space fmt ();
                 F.pp_print_string fmt "(";
                 F.pp_print_cut fmt)
@@ -1978,18 +2410,18 @@ and extract_Switch (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
         F.pp_close_box fmt ();
         (* Close the parenthesized expression *)
         (if parenth then
-         match !backend with
-         | FStar ->
-             F.pp_print_space fmt ();
-             F.pp_print_string fmt "end"
-         | Coq | Lean -> F.pp_print_string fmt ")");
+           match !backend with
+           | FStar ->
+               F.pp_print_space fmt ();
+               F.pp_print_string fmt "end"
+           | Coq | Lean | HOL4 -> F.pp_print_string fmt ")");
         (* Close the box for the then/else+branch *)
         F.pp_close_box fmt ()
       in
 
       extract_branch true e_then;
       extract_branch false e_else
-  | Match branches ->
+  | Match branches -> (
       (* Open a box for the [match ... with] *)
       F.pp_open_hovbox fmt ctx.indent_incr;
       (* Print the [match ... with] *)
@@ -1998,13 +2430,19 @@ and extract_Switch (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
         | FStar -> "begin match"
         | Coq -> "match"
         | Lean -> "match h:"
+        | HOL4 ->
+            (* We're being extra safe in the case of HOL4 *)
+            "(case"
       in
       F.pp_print_string fmt match_begin;
       F.pp_print_space fmt ();
       let scrut_inside = PureUtils.texpression_requires_parentheses scrut in
       extract_texpression ctx fmt scrut_inside scrut;
       F.pp_print_space fmt ();
-      F.pp_print_string fmt "with";
+      let match_scrut_end =
+        match !backend with FStar | Coq | Lean -> "with" | HOL4 -> "of"
+      in
+      F.pp_print_string fmt match_scrut_end;
       (* Close the box for the [match ... with] *)
       F.pp_close_box fmt ();
 
@@ -2020,7 +2458,9 @@ and extract_Switch (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
         F.pp_print_space fmt ();
         let ctx = extract_typed_pattern ctx fmt false br.pat in
         F.pp_print_space fmt ();
-        let arrow = match !backend with FStar -> "->" | Coq | Lean -> "=>" in
+        let arrow =
+          match !backend with FStar -> "->" | Coq | Lean | HOL4 -> "=>"
+        in
         F.pp_print_string fmt arrow;
         (* Close the box for the pattern *)
         F.pp_close_box fmt ();
@@ -2037,58 +2477,89 @@ and extract_Switch (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
 
       List.iter extract_branch branches;
 
-      (* End the match - we rely on indentation in Lean *)
-      if !backend <> Lean then (
-        F.pp_print_space fmt ();
-        F.pp_print_string fmt "end"));
-  (* Close parentheses *)
-  if inside then F.pp_print_string fmt ")";
+      (* End the match *)
+      match !backend with
+      | Lean -> (*We rely on indentation in Lean *) ()
+      | FStar | Coq ->
+          F.pp_print_space fmt ();
+          F.pp_print_string fmt "end"
+      | HOL4 -> F.pp_print_string fmt ")"));
   (* Close the box for the whole expression *)
   F.pp_close_box fmt ()
 
 and extract_StructUpdate (ctx : extraction_ctx) (fmt : F.formatter)
-    (_inside : bool) (supd : struct_update) : unit =
+    (inside : bool) (supd : struct_update) : unit =
   (* We can't update a subset of the fields in Coq (i.e., we can do
      [{| x:= 3; y := 4 |}], but there is no syntax for [{| s with x := 3 |}]) *)
   assert (!backend <> Coq || supd.init = None);
-  F.pp_open_hvbox fmt 0;
-  F.pp_open_hvbox fmt ctx.indent_incr;
-  let lb, rb =
-    match !backend with Lean | FStar -> ("{", "}") | Coq -> ("{|", "|}")
+  (* In the case of HOL4, records with no fields are not supported and are
+     thus extracted to unit. We need to check that by looking up the definition *)
+  let extract_as_unit =
+    if !backend = HOL4 then
+      let d =
+        TypeDeclId.Map.find supd.struct_id ctx.trans_ctx.type_context.type_decls
+      in
+      d.kind = Struct []
+    else false
   in
-  F.pp_print_string fmt lb;
-  F.pp_print_space fmt ();
-  F.pp_open_hvbox fmt ctx.indent_incr;
-  if supd.init <> None then (
-    let var_name = ctx_get_var (Option.get supd.init) ctx in
-    F.pp_print_string fmt var_name;
-    F.pp_print_space fmt ();
-    F.pp_print_string fmt "with";
-    F.pp_print_space fmt ());
-  F.pp_open_hvbox fmt 0;
-  let delimiter = match !backend with Lean -> "," | Coq | FStar -> ";" in
-  let assign = match !backend with Coq | Lean -> ":=" | FStar -> "=" in
-  Collections.List.iter_link
-    (fun () ->
-      F.pp_print_string fmt delimiter;
-      F.pp_print_space fmt ())
-    (fun (fid, fe) ->
-      F.pp_open_hvbox fmt ctx.indent_incr;
-      let f = ctx_get_field (AdtId supd.struct_id) fid ctx in
-      F.pp_print_string fmt f;
-      F.pp_print_string fmt (" " ^ assign);
+  if extract_as_unit then
+    (* Remark: this is only valid for HOL4 (for instance the Coq unit value is [tt]) *)
+    F.pp_print_string fmt "()"
+  else (
+    F.pp_open_hvbox fmt 0;
+    F.pp_open_hvbox fmt ctx.indent_incr;
+    let lb, rb =
+      match !backend with
+      | Lean | FStar -> (Some "{", Some "}")
+      | Coq -> (Some "{|", Some "|}")
+      | HOL4 -> (None, None)
+    in
+    (match lb with
+    | Some lb ->
+        F.pp_print_string fmt lb;
+        F.pp_print_space fmt ()
+    | None -> ());
+    let need_paren = inside && !backend = HOL4 in
+    if need_paren then F.pp_print_string fmt "(";
+    F.pp_open_hvbox fmt ctx.indent_incr;
+    if supd.init <> None then (
+      let var_name = ctx_get_var (Option.get supd.init) ctx in
+      F.pp_print_string fmt var_name;
       F.pp_print_space fmt ();
-      F.pp_open_hvbox fmt ctx.indent_incr;
-      extract_texpression ctx fmt true fe;
-      F.pp_close_box fmt ();
-      F.pp_close_box fmt ())
-    supd.updates;
-  F.pp_close_box fmt ();
-  F.pp_close_box fmt ();
-  F.pp_close_box fmt ();
-  F.pp_print_space fmt ();
-  F.pp_print_string fmt rb;
-  F.pp_close_box fmt ()
+      F.pp_print_string fmt "with";
+      F.pp_print_space fmt ());
+    F.pp_open_hvbox fmt 0;
+    let delimiter =
+      match !backend with Lean -> "," | Coq | FStar | HOL4 -> ";"
+    in
+    let assign =
+      match !backend with Coq | Lean | HOL4 -> ":=" | FStar -> "="
+    in
+    Collections.List.iter_link
+      (fun () ->
+        F.pp_print_string fmt delimiter;
+        F.pp_print_space fmt ())
+      (fun (fid, fe) ->
+        F.pp_open_hvbox fmt ctx.indent_incr;
+        let f = ctx_get_field (AdtId supd.struct_id) fid ctx in
+        F.pp_print_string fmt f;
+        F.pp_print_string fmt (" " ^ assign);
+        F.pp_print_space fmt ();
+        F.pp_open_hvbox fmt ctx.indent_incr;
+        extract_texpression ctx fmt true fe;
+        F.pp_close_box fmt ();
+        F.pp_close_box fmt ())
+      supd.updates;
+    F.pp_close_box fmt ();
+    F.pp_close_box fmt ();
+    F.pp_close_box fmt ();
+    if need_paren then F.pp_print_string fmt ")";
+    (match rb with
+    | Some rb ->
+        F.pp_print_space fmt ();
+        F.pp_print_string fmt rb
+    | None -> ());
+    F.pp_close_box fmt ())
 
 (** Insert a space, if necessary *)
 let insert_req_space (fmt : F.formatter) (space : bool ref) : unit =
@@ -2098,17 +2569,27 @@ let insert_req_space (fmt : F.formatter) (space : bool ref) : unit =
 
     We return two contexts:
     - the context augmented with bindings for the type parameters
-    - the previous context augmented with bindings for the input values
+    - the context augmented with bindings for the type parameters *and*
+      bindings for the input values
+
+    TODO: do we really need the first one? We should probably always use
+    the second one.
+    It comes from the fact that when we print the input values for the
+    decrease clause, we introduce bindings in the context (because we print
+    patterns, not the variables). We should figure a cleaner way.
  *)
 let extract_fun_parameters (space : bool ref) (ctx : extraction_ctx)
     (fmt : F.formatter) (def : fun_decl) : extraction_ctx * extraction_ctx =
   (* Add the type parameters - note that we need those bindings only for the
    * body translation (they are not top-level) *)
   let ctx, _ = ctx_add_type_params def.signature.type_params ctx in
-  (* Print the parameters - rk.: we should have filtered the functions
+  (* Print the parameters - rem.: we should have filtered the functions
    * with no input parameters *)
-  (* The type parameters *)
-  if def.signature.type_params <> [] then (
+  (* The type parameters.
+
+     Note that in HOL4 we don't print the type parameters.
+  *)
+  if def.signature.type_params <> [] && !backend <> HOL4 then (
     (* Open a box for the type parameters *)
     F.pp_open_hovbox fmt 0;
     insert_req_space fmt space;
@@ -2122,7 +2603,10 @@ let extract_fun_parameters (space : bool ref) (ctx : extraction_ctx)
     F.pp_print_string fmt ":";
     F.pp_print_space fmt ();
     let type_keyword =
-      match !backend with FStar -> "Type0" | Coq | Lean -> "Type"
+      match !backend with
+      | FStar -> "Type0"
+      | Coq | Lean -> "Type"
+      | HOL4 -> raise (Failure "Unreachable")
     in
     F.pp_print_string fmt (type_keyword ^ ")");
     (* Close the box for the type parameters *)
@@ -2142,7 +2626,7 @@ let extract_fun_parameters (space : bool ref) (ctx : extraction_ctx)
             F.pp_print_space fmt ();
             F.pp_print_string fmt ":";
             F.pp_print_space fmt ();
-            extract_ty ctx fmt false lv.ty;
+            extract_ty ctx fmt TypeDeclId.Set.empty false lv.ty;
             F.pp_print_string fmt ")";
             (* Close the box for the input parameters *)
             F.pp_close_box fmt ();
@@ -2161,7 +2645,7 @@ let extract_fun_input_parameters_types (ctx : extraction_ctx)
     (fmt : F.formatter) (def : fun_decl) : unit =
   let extract_param (ty : ty) : unit =
     let inside = false in
-    extract_ty ctx fmt inside ty;
+    extract_ty ctx fmt TypeDeclId.Set.empty inside ty;
     F.pp_print_space fmt ();
     F.pp_print_string fmt "->";
     F.pp_print_space fmt ()
@@ -2171,7 +2655,9 @@ let extract_fun_input_parameters_types (ctx : extraction_ctx)
 let assert_backend_supports_decreases_clauses () =
   match !backend with
   | FStar | Lean -> ()
-  | _ -> failwith "decreases clauses only supported for the Lean & F* backends"
+  | _ ->
+      raise
+        (Failure "decreases clauses only supported for the Lean & F* backends")
 
 (** Extract a decreases clause function template body.
 
@@ -2346,14 +2832,12 @@ let extract_template_lean_termination_and_decreasing (ctx : extraction_ctx)
 
 (** Extract a function declaration.
 
-    Note that all the names used for extraction should already have been
-    registered.
+    This function is for all function declarations and all backends **at the exception**
+    of opaque (assumed/declared) functions for HOL4.
 
-    We take the definition of the forward translation as parameter (which is
-    equal to the definition to extract, if we extract a forward function) because
-    it is useful for the decrease clause.
+    See {!extract_fun_decl}.
  *)
-let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
+let extract_fun_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
     (kind : decl_kind) (has_decreases_clause : bool) (def : fun_decl) : unit =
   assert (not def.is_global_decl_body);
   (* Retrieve the function name *)
@@ -2363,7 +2847,8 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
       ctx
   in
   (* Add a break before *)
-  F.pp_print_break fmt 0 0;
+  if !backend <> HOL4 || not (decl_is_first_from_group kind) then
+    F.pp_print_break fmt 0 0;
   (* Print a comment to link the extracted type to its original rust definition *)
   extract_comment fmt ("[" ^ Print.fun_name_to_string def.basename ^ "]");
   F.pp_print_space fmt ();
@@ -2371,6 +2856,9 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
    * one line and indents are correct *)
   F.pp_open_hvbox fmt 0;
   F.pp_open_vbox fmt ctx.indent_incr;
+  (* For HOL4: we may need to put parentheses around the definition *)
+  let parenthesize = !backend = HOL4 && decl_is_not_last_from_group kind in
+  if parenthesize then F.pp_print_string fmt "(";
   (* Open a box for "let FUN_NAME (PARAMS) : EFFECT =" *)
   F.pp_open_hovbox fmt ctx.indent_incr;
   (* > "let FUN_NAME" *)
@@ -2382,12 +2870,16 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
   *)
   let is_opaque_coq = !backend = Coq && is_opaque in
   let use_forall = is_opaque_coq && def.signature.type_params <> [] in
-  (* *)
-  let qualif = ctx.fmt.fun_decl_kind_to_qualif kind in
-  (* For Lean: we generate a record of assumed functions *)
-  if not (!backend = Lean && (kind = Assumed || kind = Declared)) then (
-    F.pp_print_string fmt qualif;
-    F.pp_print_space fmt ());
+  (* Print the qualifier ("assume", etc.).
+
+     For Lean: we generate a record of assumed functions *)
+  (if not (!backend = Lean && (kind = Assumed || kind = Declared)) then
+     let qualif = ctx.fmt.fun_decl_kind_to_qualif kind in
+     match qualif with
+     | Some qualif ->
+         F.pp_print_string fmt qualif;
+         F.pp_print_space fmt ()
+     | None -> ());
   F.pp_print_string fmt def_name;
   F.pp_print_space fmt ();
   if use_forall then (
@@ -2428,7 +2920,8 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
       if !backend = FStar then (
         F.pp_print_string fmt "Tot";
         F.pp_print_space fmt ()));
-    extract_ty ctx fmt has_decreases_clause def.signature.output;
+    extract_ty ctx fmt TypeDeclId.Set.empty has_decreases_clause
+      def.signature.output;
     (* Close the box for the return type *)
     F.pp_close_box fmt ();
     (* Print the decrease clause - rk.: a function with a decreases clause
@@ -2468,6 +2961,8 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
         in
         Collections.List.prefix num_fwd_inputs all_inputs
       in
+      (* TODO: we should probably print the input variables, not the typed
+         patterns *)
       let _ =
         List.fold_left
           (fun ctx (lv : typed_pattern) ->
@@ -2487,7 +2982,7 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
   (* Print the "=" *)
   if not is_opaque then (
     F.pp_print_space fmt ();
-    let eq = match !backend with FStar -> "=" | Coq | Lean -> ":=" in
+    let eq = match !backend with FStar | HOL4 -> "=" | Coq | Lean -> ":=" in
     F.pp_print_string fmt eq);
   (* Close the box for "(PARAMS) : EFFECT =" *)
   F.pp_close_box fmt ();
@@ -2569,17 +3064,82 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
     F.pp_close_box fmt ();
     (* Close the box for the [decreasing by ...] *)
     F.pp_close_box fmt ());
-  (* Add the definition group end delimiter *)
-  print_decl_end_delimiter fmt kind;
+  (* Close the parentheses *)
+  if parenthesize then F.pp_print_string fmt ")";
+  (* Add the definition end delimiter *)
+  if !backend = HOL4 && decl_is_not_last_from_group kind then (
+    F.pp_print_space fmt ();
+    F.pp_print_string fmt "/\\")
+  else if !backend = Coq && decl_is_last_from_group kind then (
+    (* This is actually an end of group delimiter. For aesthetic reasons
+       we print it here instead of in {!end_fun_decl_group}. *)
+    F.pp_print_cut fmt ();
+    F.pp_print_string fmt ".");
   (* Close the outer box for the definition *)
   F.pp_close_box fmt ();
   (* Add breaks to insert new lines between definitions *)
-  F.pp_print_break fmt 0 0
+  if !backend <> HOL4 || decl_is_not_last_from_group kind then
+    F.pp_print_break fmt 0 0
+
+(** Extract an opaque function declaration to HOL4.
+
+    Remark (SH): having to treat this specific case separately is very annoying,
+    but I could not find a better way.
+ *)
+let extract_fun_decl_hol4_opaque (ctx : extraction_ctx) (fmt : F.formatter)
+    (def : fun_decl) : unit =
+  (* Retrieve the definition name *)
+  let with_opaque_pre = false in
+  let def_name =
+    ctx_get_local_function with_opaque_pre def.def_id None None ctx
+  in
+  (* Add the type parameters - note that we need those bindings only for the
+   * generation of the type (they are not top-level) *)
+  let ctx, _ = ctx_add_type_params def.signature.type_params ctx in
+  (* Open a box for the whole definition *)
+  F.pp_open_hovbox fmt ctx.indent_incr;
+  (* Generate: `val _ = new_constant ("...",` *)
+  F.pp_print_string fmt ("val _ = new_constant (\"" ^ def_name ^ ", ");
+  (* Open a box for the type *)
+  F.pp_open_hvbox fmt 0;
+  (* Generate the type *)
+  extract_fun_input_parameters_types ctx fmt def;
+  extract_ty ctx fmt TypeDeclId.Set.empty false def.signature.output;
+  (* Close the box for the type *)
+  F.pp_close_box fmt ();
+  (* Close the parenthesis opened for the inputs of `new_constant` *)
+  F.pp_print_string fmt ")";
+  (* Close the box for the definition *)
+  F.pp_close_box fmt ()
+
+(** Extract a function declaration.
+
+    Note that all the names used for extraction should already have been
+    registered.
+
+    We take the definition of the forward translation as parameter (which is
+    equal to the definition to extract, if we extract a forward function) because
+    it is useful for the decrease clause.
+
+    This function should be inserted between calls to {!start_fun_decl_group}
+    and {!end_fun_decl_group}.
+ *)
+let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
+    (kind : decl_kind) (has_decreases_clause : bool) (def : fun_decl) : unit =
+  assert (not def.is_global_decl_body);
+  (* We treat HOL4 opaque functions in a specific manner *)
+  if !backend = HOL4 && Option.is_none def.body then
+    extract_fun_decl_hol4_opaque ctx fmt def
+  else extract_fun_decl_gen ctx fmt kind has_decreases_clause def
 
 (** Extract a global declaration body of the shape "QUALIF NAME : TYPE = BODY"
-    with a custom body extractor
+    with a custom body extractor.
+
+    We introduce this helper because every (non opaque) global declaration gets
+    extracted to two declarations, and we can actually factor out the generation
+    of those declarations. See {!extract_global_decl} for more explanations.
  *)
-let extract_global_decl_body (ctx : extraction_ctx) (fmt : F.formatter)
+let extract_global_decl_body_gen (ctx : extraction_ctx) (fmt : F.formatter)
     (kind : decl_kind) (name : string) (ty : ty)
     (extract_body : (F.formatter -> unit) Option.t) : unit =
   let is_opaque = Option.is_none extract_body in
@@ -2591,8 +3151,11 @@ let extract_global_decl_body (ctx : extraction_ctx) (fmt : F.formatter)
   (* Open "QUALIF NAME : TYPE =" box (depth=1) *)
   F.pp_open_hovbox fmt ctx.indent_incr;
   (* Print "QUALIF NAME " *)
-  F.pp_print_string fmt (ctx.fmt.fun_decl_kind_to_qualif kind);
-  F.pp_print_space fmt ();
+  (match ctx.fmt.fun_decl_kind_to_qualif kind with
+  | Some qualif ->
+      F.pp_print_string fmt qualif;
+      F.pp_print_space fmt ()
+  | None -> ());
   F.pp_print_string fmt name;
   F.pp_print_space fmt ();
 
@@ -2605,14 +3168,14 @@ let extract_global_decl_body (ctx : extraction_ctx) (fmt : F.formatter)
   (* Open "TYPE" box (depth=3) *)
   F.pp_open_hovbox fmt ctx.indent_incr;
   (* Print "TYPE" *)
-  extract_ty ctx fmt false ty;
+  extract_ty ctx fmt TypeDeclId.Set.empty false ty;
   (* Close "TYPE" box (depth=3) *)
   F.pp_close_box fmt ();
 
   if not is_opaque then (
     (* Print " =" *)
     F.pp_print_space fmt ();
-    let eq = match !backend with FStar -> "=" | Coq | Lean -> ":=" in
+    let eq = match !backend with FStar | HOL4 -> "=" | Coq | Lean -> ":=" in
     F.pp_print_string fmt eq);
   (* Close ": TYPE =" box (depth=2) *)
   F.pp_close_box fmt ();
@@ -2632,22 +3195,52 @@ let extract_global_decl_body (ctx : extraction_ctx) (fmt : F.formatter)
   F.pp_close_box fmt ();
 
   (* Coq: add a "." *)
-  print_decl_end_delimiter fmt Declared;
+  if !backend = Coq then (
+    F.pp_print_cut fmt ();
+    F.pp_print_string fmt ".");
 
   (* Close the outer definition box (depth=0) *)
   F.pp_close_box fmt ()
 
+(** Extract an opaque global declaration for HOL4.
+
+    Remark (SH): having to treat this specific case separately is very annoying,
+    but I could not find a better way.
+ *)
+let extract_global_decl_hol4_opaque (ctx : extraction_ctx) (fmt : F.formatter)
+    (name : string) (ty : ty) : unit =
+  (* Open the definition boxe (depth=0) *)
+  F.pp_open_hvbox fmt ctx.indent_incr;
+  (* [val ..._def = new_constant ("...",] *)
+  F.pp_open_hovbox fmt 0;
+  F.pp_print_string fmt
+    ("val " ^ name ^ "_def = new_constant (\"" ^ name ^ "\", ");
+  F.pp_close_box fmt ();
+  (* Print the type *)
+  F.pp_open_hovbox fmt 0;
+  extract_ty ctx fmt TypeDeclId.Set.empty false ty;
+  F.pp_close_box fmt ();
+  (* Close the definition boxe *) F.pp_close_box fmt ()
+
 (** Extract a global declaration.
 
-    We generate the body which computes the global value separately from the
+    We generate the body which *computes* the global value separately from the
     value declaration itself.
 
     For example in Rust,
     [static X: u32 = 3;]
 
     will be translated to the following F*:
-    [let x_body : result u32 = Return 3]
-    [let x_c : u32 = eval_global x_body]
+    [let x_body : result u32 = Return 3] (* this has type [result u32] *)
+    [let x_c : u32 = eval_global x_body] (* this has type [u32] (no [result]!) *)
+
+    This function generates the two declarations.
+
+    Remark: because global declaration groups are always singletons (i.e.,
+    there are no groups of mutually recursive global declarations), this function
+    doesn't need to be called between calls to functions of the shape
+    [{start,end}_gloabl_decl_group], contrary to {!extract_type_decl}
+    and {!extract_fun_decl}.
  *)
 let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter)
     (global : A.global_decl) (body : fun_decl) (interface : bool) : unit =
@@ -2677,13 +3270,19 @@ let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter)
   in
   match body.body with
   | None ->
+      (* No body: only generate a [val x_c : u32] declaration *)
       let kind = if interface then Declared else Assumed in
-      extract_global_decl_body ctx fmt kind decl_name decl_ty None
+      if !backend = HOL4 then
+        extract_global_decl_hol4_opaque ctx fmt decl_name decl_ty
+      else extract_global_decl_body_gen ctx fmt kind decl_name decl_ty None
   | Some body ->
-      extract_global_decl_body ctx fmt SingleNonRec body_name body_ty
+      (* There is a body *)
+      (* Generate: [let x_body : result u32 = Return 3] *)
+      extract_global_decl_body_gen ctx fmt SingleNonRec body_name body_ty
         (Some (fun fmt -> extract_texpression ctx fmt false body.body));
       F.pp_print_break fmt 0 0;
-      extract_global_decl_body ctx fmt SingleNonRec decl_name decl_ty
+      (* Generate: [let x_c : u32 = eval_global x_body] *)
+      extract_global_decl_body_gen ctx fmt SingleNonRec decl_name decl_ty
         (Some
            (fun fmt ->
              let body =
@@ -2691,6 +3290,7 @@ let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter)
                | FStar -> "eval_global " ^ body_name
                | Lean -> "eval_global " ^ body_name ^ " (by simp)"
                | Coq -> body_name ^ "%global"
+               | HOL4 -> "get_return_value " ^ body_name
              in
              F.pp_print_string fmt body));
       (* Add a break to insert lines between declarations *)
@@ -2790,7 +3390,22 @@ let extract_unit_test_if_unit_fun (ctx : extraction_ctx) (fmt : F.formatter)
         F.pp_print_string fmt "==";
         F.pp_print_space fmt ();
         let success = ctx_get_variant (Assumed Result) result_return_id ctx in
-        F.pp_print_string fmt ("." ^ success ^ " ())"));
+        F.pp_print_string fmt ("." ^ success ^ " ())")
+    | HOL4 ->
+        F.pp_print_string fmt "val _ = assert_return (";
+        F.pp_print_string fmt "“";
+        (* Note that if the function is opaque, the unit test will fail
+           because the normalizer will get stuck *)
+        let with_opaque_pre = ctx.use_opaque_pre in
+        let fun_name =
+          ctx_get_local_function with_opaque_pre def.def_id def.loop_id
+            def.back_id ctx
+        in
+        F.pp_print_string fmt fun_name;
+        if sg.inputs <> [] then (
+          F.pp_print_space fmt ();
+          F.pp_print_string fmt "()");
+        F.pp_print_string fmt "”)");
     (* Close the box for the test *)
     F.pp_close_box fmt ();
     (* Add a break after *)
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index 81bdd202..0a5d7df2 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -98,6 +98,19 @@ let decl_is_from_mut_rec_group (kind : decl_kind) : bool =
   | SingleNonRec | SingleRec | Assumed | Declared -> false
   | MutRecFirst | MutRecInner | MutRecLast -> true
 
+let decl_is_first_from_group (kind : decl_kind) : bool =
+  match kind with
+  | SingleNonRec | SingleRec | MutRecFirst | Assumed | Declared -> true
+  | MutRecLast | MutRecInner -> false
+
+(** Return [true] if the declaration is not the last from its group of declarations.
+
+    We need this because in some provers (e.g., HOL4), we need to delimit
+    the inner declarations (with `/\` for instance).
+ *)
+let decl_is_not_last_from_group (kind : decl_kind) : bool =
+  not (decl_is_last_from_group kind)
+
 (* TODO: this should a module we give to a functor! *)
 
 type type_decl_kind = Enum | Struct
@@ -118,15 +131,20 @@ type formatter = {
   char_name : string;
   int_name : integer_type -> string;
   str_name : string;
-  type_decl_kind_to_qualif : decl_kind -> type_decl_kind option -> string;
+  type_decl_kind_to_qualif :
+    decl_kind -> type_decl_kind option -> string option;
       (** Compute the qualified for a type definition/declaration.
 
           For instance: "type", "and", etc.
+
+          Remark: can return [None] for some backends like HOL4.
        *)
-  fun_decl_kind_to_qualif : decl_kind -> string;
+  fun_decl_kind_to_qualif : decl_kind -> string option;
       (** Compute the qualified for a function definition/declaration.
 
           For instance: "let", "let rec", "and", etc.
+
+          Remark: can return [None] for some backends like HOL4.
        *)
   field_name : name -> FieldId.id -> string option -> string;
       (** Inputs:
diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml
index 1f5d1ed8..9b768f3b 100644
--- a/compiler/PureUtils.ml
+++ b/compiler/PureUtils.ml
@@ -169,7 +169,7 @@ let rec let_group_requires_parentheses (e : texpression) : bool =
 let texpression_requires_parentheses e =
   match !Config.backend with
   | FStar | Lean -> false
-  | Coq -> let_group_requires_parentheses e
+  | Coq | HOL4 -> let_group_requires_parentheses e
 
 let is_var (e : texpression) : bool =
   match e.e with Var _ -> true | _ -> false
diff --git a/compiler/StringUtils.ml b/compiler/StringUtils.ml
index 0fd46136..161df27b 100644
--- a/compiler/StringUtils.ml
+++ b/compiler/StringUtils.ml
@@ -96,6 +96,11 @@ let capitalize_first_letter (s : string) : string =
   let s = match s with [] -> s | c :: s' -> uppercase_ascii c :: s' in
   string_of_chars s
 
+let lowercase_first_letter (s : string) : string =
+  let s = string_to_chars s in
+  let s = match s with [] -> s | c :: s' -> lowercase_ascii c :: s' in
+  string_of_chars s
+
 (** Unit tests *)
 let _ =
   assert (to_camel_case "hello_world" = "HelloWorld");
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 5252495d..5dc8664a 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -2642,7 +2642,7 @@ let wrap_in_match_fuel (fuel0 : VarId.id) (fuel : VarId.id) (body : texpression)
       let match_ty = body.ty in
       let match_e = Switch (fuel0, Match [ fail_branch; success_branch ]) in
       { e = match_e; ty = match_ty }
-  | Lean ->
+  | Lean | HOL4 ->
       (* We should have checked the command line arguments before *)
       raise (Failure "Unexpected")
 
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 409fc5d3..709b54a4 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -407,10 +407,9 @@ let module_has_opaque_decls (ctx : gen_ctx) : bool * bool =
     the declaration, if both booleans are [true]).
  *)
 let export_type (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx)
-    (kind : ExtractBase.decl_kind) (id : Pure.TypeDeclId.id)
-    (extract_decl : bool) (extract_extra_info : bool) : unit =
-  (* Retrieve the declaration *)
-  let def = Pure.TypeDeclId.Map.find id ctx.trans_types in
+    (type_decl_group : Pure.TypeDeclId.Set.t) (kind : ExtractBase.decl_kind)
+    (def : Pure.type_decl) (extract_decl : bool) (extract_extra_info : bool) :
+    unit =
   (* Update the kind, if the type is opaque *)
   let is_opaque, kind =
     match def.kind with
@@ -427,7 +426,8 @@ let export_type (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx)
     (is_opaque && config.extract_opaque)
     || ((not is_opaque) && config.extract_transparent)
   then (
-    if extract_decl then Extract.extract_type_decl ctx.extract_ctx fmt kind def;
+    if extract_decl then
+      Extract.extract_type_decl ctx.extract_ctx fmt type_decl_group kind def;
     if extract_extra_info then
       Extract.extract_type_decl_extra_info ctx.extract_ctx fmt kind def)
 
@@ -438,9 +438,11 @@ let export_type (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx)
  *)
 let export_types_group (fmt : Format.formatter) (config : gen_config)
     (ctx : gen_ctx) (is_rec : bool) (ids : Pure.TypeDeclId.id list) : unit =
+  assert (ids <> []);
   let export_type = export_type fmt config ctx in
-  let export_type_decl kind id = export_type kind id true false in
-  let export_type_extra_info kind id = export_type kind id false true in
+  let ids_set = Pure.TypeDeclId.Set.of_list ids in
+  let export_type_decl kind id = export_type ids_set kind id true false in
+  let export_type_extra_info kind id = export_type ids_set kind id false true in
 
   (* Rem.: we shouldn't have (mutually) recursive opaque types *)
   let num_decls = List.length ids in
@@ -452,22 +454,51 @@ let export_types_group (fmt : Format.formatter) (config : gen_config)
     else if i = num_decls - 1 then ExtractBase.MutRecLast
     else ExtractBase.MutRecInner
   in
-  (* Extract the type declarations *)
+
+  (* Retrieve the declarations *)
+  let defs =
+    List.map (fun id -> Pure.TypeDeclId.Map.find id ctx.trans_types) ids
+  in
+
+  (* Extract the type declarations.
+
+     Because some declaration groups are delimited, we wrap the declarations
+     between [{start,end}_type_decl_group].
+
+     Ex.:
+     ====
+     When targeting HOL4, the calls to [{start,end}_type_decl_group] would generate
+     the [Datatype] and [End] delimiters in the snippet of code below:
+
+     {[
+       Datatype:
+         tree =
+           TLeaf 'a
+         | TNode node ;
+
+         node =
+           Node (tree list)
+       End
+     ]}
+  *)
+  Extract.start_type_decl_group ctx.extract_ctx fmt is_rec defs;
   List.iteri
-    (fun i id ->
+    (fun i def ->
       let kind = kind_from_index i in
-      export_type_decl kind id)
-    ids;
+      export_type_decl kind def)
+    defs;
+  Extract.end_type_decl_group fmt is_rec defs;
+
   (* Export the extra information (ex.: [Arguments] instructions in Coq) *)
   List.iteri
-    (fun i id ->
+    (fun i def ->
       let kind = kind_from_index i in
-      export_type_extra_info kind id)
-    ids
+      export_type_extra_info kind def)
+    defs
 
 (** Export a global declaration.
 
-    TODO: check correct behaviour with opaque globals.
+    TODO: check correct behavior with opaque globals.
  *)
 let export_global (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx)
     (id : A.GlobalDeclId.id) : unit =
@@ -485,6 +516,11 @@ let export_global (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx)
     && (((not is_opaque) && config.extract_transparent)
        || (is_opaque && config.extract_opaque))
   then
+    (* We don't wrap global declaration groups between calls to functions
+       [{start, end}_global_decl_group] (which don't exist): global declaration
+       groups are always singletons, so the [extract_global_decl] function
+       takes care of generating the delimiters.
+    *)
     Extract.extract_global_decl ctx.extract_ctx fmt global body config.interface
 
 (** Utility.
@@ -519,6 +555,20 @@ let export_functions_group_scc (fmt : Format.formatter) (config : gen_config)
   let is_mut_rec = List.length decls > 1 in
   assert ((not is_mut_rec) || is_rec);
   let decls_length = List.length decls in
+  (* We open and close the declaration group with [{start, end}_fun_decl_group].
+
+     Some backends require the groups to be delimited. For instance, if we target
+     HOL4, the calls to [{start, end}_fun_decl_group] would generate the
+     [val ... = Define `] and [`] delimiters in the snippet of code below:
+
+     {[
+       val ... = Define `
+         (even (i : num) : bool result = if i = 0 then Return T else odd (i - 1)) /\
+         (odd (i : num) : bool result = if i = 0 then Return F else even (i - 1))
+       `
+     ]}
+  *)
+  Extract.start_fun_decl_group ctx.extract_ctx fmt is_rec decls;
   List.iteri
     (fun i def ->
       let is_opaque = Option.is_none def.Pure.body in
@@ -545,7 +595,8 @@ let export_functions_group_scc (fmt : Format.formatter) (config : gen_config)
         ((not is_opaque) && config.extract_transparent)
         || (is_opaque && config.extract_opaque)
       then Extract.extract_fun_decl ctx.extract_ctx fmt kind has_decr_clause def)
-    decls
+    decls;
+  Extract.end_fun_decl_group fmt is_rec decls
 
 (** Export a group of function declarations.
 
@@ -586,6 +637,9 @@ let export_functions_group (fmt : Format.formatter) (config : gen_config)
                   fmt decl
             | Coq ->
                 raise (Failure "Coq doesn't have decreases/termination clauses")
+            | HOL4 ->
+                raise
+                  (Failure "HOL4 doesn't have decreases/termination clauses")
         in
         extract_decrease fwd;
         List.iter extract_decrease loop_fwds)
@@ -610,14 +664,14 @@ let export_functions_group (fmt : Format.formatter) (config : gen_config)
 
   (* Extract the function definitions *)
   (if config.extract_fun_decls then
-   (* Group the mutually recursive definitions *)
-   let subgroups = ReorderDecls.group_reorder_fun_decls decls in
+     (* Group the mutually recursive definitions *)
+     let subgroups = ReorderDecls.group_reorder_fun_decls decls in
 
-   (* Extract the subgroups *)
-   let export_subgroup (is_rec : bool) (decls : Pure.fun_decl list) : unit =
-     export_functions_group_scc fmt config ctx is_rec decls
-   in
-   List.iter (fun (is_rec, decls) -> export_subgroup is_rec decls) subgroups);
+     (* Extract the subgroups *)
+     let export_subgroup (is_rec : bool) (decls : Pure.fun_decl list) : unit =
+       export_functions_group_scc fmt config ctx is_rec decls
+     in
+     List.iter (fun (is_rec, decls) -> export_subgroup is_rec decls) subgroups);
 
   (* Insert unit tests if necessary *)
   if config.test_trans_unit_functions then
@@ -733,7 +787,7 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (filename : string)
   | Lean ->
       Printf.fprintf out "-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS\n";
       Printf.fprintf out "-- [%s]%s\n" rust_module_name custom_msg
-  | Coq | FStar ->
+  | Coq | FStar | HOL4 ->
       Printf.fprintf out
         "(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)\n";
       Printf.fprintf out "(** [%s]%s *)\n" rust_module_name custom_msg);
@@ -769,7 +823,17 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (filename : string)
       (* Add the custom imports *)
       List.iter (fun m -> Printf.fprintf out "import %s\n" m) custom_imports;
       (* Add the custom includes *)
-      List.iter (fun m -> Printf.fprintf out "import %s\n" m) custom_includes);
+      List.iter (fun m -> Printf.fprintf out "import %s\n" m) custom_includes
+  | HOL4 ->
+      Printf.fprintf out "open primitivesLib divDefLib\n";
+      (* Add the custom imports and includes *)
+      let imports = custom_imports @ custom_includes in
+      if imports <> [] then
+        let imports = String.concat " " imports in
+        Printf.fprintf out "open %s\n\n" imports
+      else Printf.fprintf out "\n";
+      (* Initialize the theory *)
+      Printf.fprintf out "val _ = new_theory \"%s\"\n\n" module_name);
   (* From now onwards, we use the formatter *)
   (* Set the margin *)
   Format.pp_set_margin fmt 80;
@@ -787,6 +851,7 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (filename : string)
   (* Close the module *)
   (match !Config.backend with
   | FStar | Lean -> ()
+  | HOL4 -> Printf.fprintf out "val _ = export_theory \"%s\"\n" module_name
   | Coq -> Printf.fprintf out "End %s .\n" module_name);
 
   (* Some logging *)
@@ -807,7 +872,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
   let variant_concatenate_type_name =
     (* For Lean, we exploit the fact that the variant name should always be
        prefixed with the type name to prevent collisions *)
-    match !Config.backend with Coq | FStar -> true | Lean -> false
+    match !Config.backend with Coq | FStar | HOL4 -> true | Lean -> false
   in
   let mk_formatter_and_names_map = Extract.mk_formatter_and_names_map in
   let fmt, names_map =
@@ -896,6 +961,11 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
         let basename = Filename.basename filename in
         (* Convert the case *)
         let module_name = StringUtils.to_camel_case basename in
+        let module_name =
+          if !Config.backend = HOL4 then
+            StringUtils.lowercase_first_letter module_name
+          else module_name
+        in
         (* Concatenate *)
         (module_name, Filename.concat dest_dir module_name)
   in
@@ -938,30 +1008,34 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
       assert !Config.split_files;
       mkdir_if (dest_dir ^^ module_name ^^ "Clauses")));
 
-  (* Copy the "Primitives" file *)
+  (* Copy the "Primitives" file, if necessary *)
   let _ =
     (* Retrieve the executable's directory *)
     let exe_dir = Filename.dirname Sys.argv.(0) in
-    let primitives_src, primitives_destname =
+    let primitives_src_dest =
       match !Config.backend with
-      | Config.FStar -> ("/backends/fstar/Primitives.fst", "Primitives.fst")
-      | Config.Coq -> ("/backends/coq/Primitives.v", "Primitives.v")
-      | Config.Lean -> ("/backends/lean/Primitives.lean", "Base/Primitives.lean")
+      | FStar -> Some ("/backends/fstar/Primitives.fst", "Primitives.fst")
+      | Coq -> Some ("/backends/coq/Primitives.v", "Primitives.v")
+      | Lean -> Some ("/backends/lean/Primitives.lean", "Base/Primitives.lean")
+      | HOL4 -> None
     in
-    let src = open_in (exe_dir ^ primitives_src) in
-    let tgt_filename = Filename.concat dest_dir primitives_destname in
-    let tgt = open_out tgt_filename in
-    (* Very annoying: I couldn't find a "cp" function in the OCaml libraries... *)
-    try
-      while true do
-        (* We copy line by line *)
-        let line = input_line src in
-        Printf.fprintf tgt "%s\n" line
-      done
-    with End_of_file ->
-      close_in src;
-      close_out tgt;
-      log#linfo (lazy ("Copied:    " ^ tgt_filename))
+    match primitives_src_dest with
+    | None -> ()
+    | Some (primitives_src, primitives_destname) -> (
+        let src = open_in (exe_dir ^ primitives_src) in
+        let tgt_filename = Filename.concat dest_dir primitives_destname in
+        let tgt = open_out tgt_filename in
+        (* Very annoying: I couldn't find a "cp" function in the OCaml libraries... *)
+        try
+          while true do
+            (* We copy line by line *)
+            let line = input_line src in
+            Printf.fprintf tgt "%s\n" line
+          done
+        with End_of_file ->
+          close_in src;
+          close_out tgt;
+          log#linfo (lazy ("Copied:    " ^ tgt_filename)))
   in
 
   (* Extract the file(s) *)
@@ -976,14 +1050,22 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
   in
 
   let module_delimiter =
-    match !Config.backend with FStar -> "." | Coq -> "_" | Lean -> "."
+    match !Config.backend with
+    | FStar -> "."
+    | Coq -> "_"
+    | Lean -> "."
+    | HOL4 -> "_"
   in
   let file_delimiter =
     if !Config.backend = Lean then "/" else module_delimiter
   in
   (* File extension for the "regular" modules *)
   let ext =
-    match !Config.backend with FStar -> ".fst" | Coq -> ".v" | Lean -> ".lean"
+    match !Config.backend with
+    | FStar -> ".fst"
+    | Coq -> ".v"
+    | Lean -> ".lean"
+    | HOL4 -> "Script.sml"
   in
   (* File extension for the opaque module *)
   let opaque_ext =
@@ -991,161 +1073,165 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) :
     | FStar -> ".fsti"
     | Coq -> ".v"
     | Lean -> ".lean"
+    | HOL4 -> "Script.sml"
   in
 
   (* Extract one or several files, depending on the configuration *)
   (if !Config.split_files then (
-   let base_gen_config =
-     {
-       extract_types = false;
-       extract_decreases_clauses = !Config.extract_decreases_clauses;
-       extract_template_decreases_clauses = false;
-       extract_fun_decls = false;
-       extract_transparent = true;
-       extract_opaque = false;
-       extract_state_type = false;
-       extract_globals = false;
-       interface = false;
-       test_trans_unit_functions = false;
-     }
-   in
-
-   (* Check if there are opaque types and functions - in which case we need
-    * to split *)
-   let has_opaque_types, has_opaque_funs = module_has_opaque_decls gen_ctx in
-   let has_opaque_types = has_opaque_types || !Config.use_state in
-
-   (* Extract the types *)
-   (* If there are opaque types, we extract in an interface *)
-   let types_filename_ext =
-     match !Config.backend with
-     | FStar -> if has_opaque_types then ".fsti" else ".fst"
-     | Coq -> ".v"
-     | Lean -> ".lean"
-   in
-   let types_filename =
-     extract_filebasename ^ file_delimiter ^ "Types" ^ types_filename_ext
-   in
-   let types_module = module_name ^ module_delimiter ^ "Types" in
-   let types_config =
-     {
-       base_gen_config with
-       extract_types = true;
-       extract_opaque = true;
-       extract_state_type = !Config.use_state;
-       interface = has_opaque_types;
-     }
-   in
-   extract_file types_config gen_ctx types_filename crate.A.name types_module
-     ": type definitions" [] [];
-
-   (* Extract the template clauses *)
-   (if needs_clauses_module && !Config.extract_template_decreases_clauses then
-    let template_clauses_filename =
-      extract_filebasename ^ file_delimiter ^ "Clauses" ^ file_delimiter
-      ^ "Template" ^ ext
-    in
-    let template_clauses_module =
-      module_name ^ module_delimiter ^ "Clauses" ^ module_delimiter ^ "Template"
-    in
-    let template_clauses_config =
-      { base_gen_config with extract_template_decreases_clauses = true }
-    in
-    extract_file template_clauses_config gen_ctx template_clauses_filename
-      crate.A.name template_clauses_module
-      ": templates for the decreases clauses" [ types_module ] []);
-
-   (* Extract the opaque functions, if needed *)
-   let opaque_funs_module =
-     if has_opaque_funs then (
-       let opaque_filename =
-         extract_filebasename ^ file_delimiter ^ "Opaque" ^ opaque_ext
-       in
-       let opaque_module = module_name ^ module_delimiter ^ "Opaque" in
-       let opaque_imported_module =
-         (* In the case of Lean, we declare an interface (a record) containing
-            the opaque definitions, and we leave it to the user to provide an
-            instance of this module.
-
-            TODO: do the same for Coq.
-            TODO: do the same for the type definitions.
-         *)
-         if !Config.backend = Lean then
-           module_name ^ module_delimiter ^ "ExternalFuns"
-         else opaque_module
-       in
-       let opaque_config =
-         {
-           base_gen_config with
-           extract_fun_decls = true;
-           extract_transparent = false;
-           extract_opaque = true;
-           interface = true;
-         }
-       in
-       let gen_ctx =
-         {
-           gen_ctx with
-           extract_ctx = { gen_ctx.extract_ctx with use_opaque_pre = false };
-         }
-       in
-       extract_file opaque_config gen_ctx opaque_filename crate.A.name
-         opaque_module ": opaque function definitions" [] [ types_module ];
-       [ opaque_imported_module ])
-     else []
-   in
-
-   (* Extract the functions *)
-   let fun_filename = extract_filebasename ^ file_delimiter ^ "Funs" ^ ext in
-   let fun_module = module_name ^ module_delimiter ^ "Funs" in
-   let fun_config =
-     {
-       base_gen_config with
-       extract_fun_decls = true;
-       extract_globals = true;
-       test_trans_unit_functions = !Config.test_trans_unit_functions;
-     }
-   in
-   let clauses_module =
-     if needs_clauses_module then
-       let clauses_submodule =
-         if !Config.backend = Lean then module_delimiter ^ "Clauses" else ""
-       in
-       [ module_name ^ clauses_submodule ^ module_delimiter ^ "Clauses" ]
-     else []
-   in
-   extract_file fun_config gen_ctx fun_filename crate.A.name fun_module
-     ": function definitions" []
-     ([ types_module ] @ opaque_funs_module @ clauses_module))
-  else
-    let gen_config =
-      {
-        extract_types = true;
-        extract_decreases_clauses = !Config.extract_decreases_clauses;
-        extract_template_decreases_clauses =
-          !Config.extract_template_decreases_clauses;
-        extract_fun_decls = true;
-        extract_transparent = true;
-        extract_opaque = true;
-        extract_state_type = !Config.use_state;
-        extract_globals = true;
-        interface = false;
-        test_trans_unit_functions = !Config.test_trans_unit_functions;
-      }
-    in
-    (* Add the extension for F* *)
-    let extract_filename = extract_filebasename ^ ext in
-    extract_file gen_config gen_ctx extract_filename crate.A.name module_name ""
-      [] []);
+     let base_gen_config =
+       {
+         extract_types = false;
+         extract_decreases_clauses = !Config.extract_decreases_clauses;
+         extract_template_decreases_clauses = false;
+         extract_fun_decls = false;
+         extract_transparent = true;
+         extract_opaque = false;
+         extract_state_type = false;
+         extract_globals = false;
+         interface = false;
+         test_trans_unit_functions = false;
+       }
+     in
+
+     (* Check if there are opaque types and functions - in which case we need
+      * to split *)
+     let has_opaque_types, has_opaque_funs = module_has_opaque_decls gen_ctx in
+     let has_opaque_types = has_opaque_types || !Config.use_state in
+
+     (* Extract the types *)
+     (* If there are opaque types, we extract in an interface *)
+     let types_filename_ext =
+       match !Config.backend with
+       | FStar -> if has_opaque_types then ".fsti" else ".fst"
+       | Coq -> ".v"
+       | Lean -> ".lean"
+       | HOL4 -> "Script.sml"
+     in
+     let types_filename =
+       extract_filebasename ^ file_delimiter ^ "Types" ^ types_filename_ext
+     in
+     let types_module = module_name ^ module_delimiter ^ "Types" in
+     let types_config =
+       {
+         base_gen_config with
+         extract_types = true;
+         extract_opaque = true;
+         extract_state_type = !Config.use_state;
+         interface = has_opaque_types;
+       }
+     in
+     extract_file types_config gen_ctx types_filename crate.A.name types_module
+       ": type definitions" [] [];
+
+     (* Extract the template clauses *)
+     (if needs_clauses_module && !Config.extract_template_decreases_clauses then
+        let template_clauses_filename =
+          extract_filebasename ^ file_delimiter ^ "Clauses" ^ file_delimiter
+          ^ "Template" ^ ext
+        in
+        let template_clauses_module =
+          module_name ^ module_delimiter ^ "Clauses" ^ module_delimiter
+          ^ "Template"
+        in
+        let template_clauses_config =
+          { base_gen_config with extract_template_decreases_clauses = true }
+        in
+        extract_file template_clauses_config gen_ctx template_clauses_filename
+          crate.A.name template_clauses_module
+          ": templates for the decreases clauses" [ types_module ] []);
+
+     (* Extract the opaque functions, if needed *)
+     let opaque_funs_module =
+       if has_opaque_funs then (
+         let opaque_filename =
+           extract_filebasename ^ file_delimiter ^ "Opaque" ^ opaque_ext
+         in
+         let opaque_module = module_name ^ module_delimiter ^ "Opaque" in
+         let opaque_imported_module =
+           (* In the case of Lean, we declare an interface (a record) containing
+              the opaque definitions, and we leave it to the user to provide an
+              instance of this module.
+
+              TODO: do the same for Coq.
+              TODO: do the same for the type definitions.
+           *)
+           if !Config.backend = Lean then
+             module_name ^ module_delimiter ^ "ExternalFuns"
+           else opaque_module
+         in
+         let opaque_config =
+           {
+             base_gen_config with
+             extract_fun_decls = true;
+             extract_transparent = false;
+             extract_opaque = true;
+             interface = true;
+           }
+         in
+         let gen_ctx =
+           {
+             gen_ctx with
+             extract_ctx = { gen_ctx.extract_ctx with use_opaque_pre = false };
+           }
+         in
+         extract_file opaque_config gen_ctx opaque_filename crate.A.name
+           opaque_module ": opaque function definitions" [] [ types_module ];
+         [ opaque_imported_module ])
+       else []
+     in
+
+     (* Extract the functions *)
+     let fun_filename = extract_filebasename ^ file_delimiter ^ "Funs" ^ ext in
+     let fun_module = module_name ^ module_delimiter ^ "Funs" in
+     let fun_config =
+       {
+         base_gen_config with
+         extract_fun_decls = true;
+         extract_globals = true;
+         test_trans_unit_functions = !Config.test_trans_unit_functions;
+       }
+     in
+     let clauses_module =
+       if needs_clauses_module then
+         let clauses_submodule =
+           if !Config.backend = Lean then module_delimiter ^ "Clauses" else ""
+         in
+         [ module_name ^ clauses_submodule ^ module_delimiter ^ "Clauses" ]
+       else []
+     in
+     extract_file fun_config gen_ctx fun_filename crate.A.name fun_module
+       ": function definitions" []
+       ([ types_module ] @ opaque_funs_module @ clauses_module))
+   else
+     let gen_config =
+       {
+         extract_types = true;
+         extract_decreases_clauses = !Config.extract_decreases_clauses;
+         extract_template_decreases_clauses =
+           !Config.extract_template_decreases_clauses;
+         extract_fun_decls = true;
+         extract_transparent = true;
+         extract_opaque = true;
+         extract_state_type = !Config.use_state;
+         extract_globals = true;
+         interface = false;
+         test_trans_unit_functions = !Config.test_trans_unit_functions;
+       }
+     in
+     (* Add the extension for F* *)
+     let extract_filename = extract_filebasename ^ ext in
+     extract_file gen_config gen_ctx extract_filename crate.A.name module_name
+       "" [] []);
 
   (* Generate the build file *)
   match !Config.backend with
-  | Coq | FStar ->
+  | Coq | FStar | HOL4 ->
       ()
       (* Nothing to do - TODO: we might want to generate the _CoqProject file for Coq.
          But then we can't modify it if we want to add more files for the proofs
          for instance. But we might want to put the proofs elsewhere anyway.
          Remark: there is the same problem for Lean actually.
+         Maybe generate it if the user asks for it?
       *)
   | Lean ->
       (*