Make progress on the HOL4 backend

2 files changed, 80 insertions, 39 deletions

diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 7e4aeab4..d624d9ca 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -249,7 +249,7 @@ let assumed_adts () : (assumed_ty * string) list =
           (Result, "result");
           (Error, "error");
           (Fuel, "num");
-          (Option, "OPTION");
+          (Option, "option");
           (Vec, "vec");
         ])
 
@@ -1532,7 +1532,7 @@ let extract_type_decl_hol4_opaque (ctx : extraction_ctx) (fmt : F.formatter)
   (* Generate the declaration *)
   F.pp_print_space fmt ();
   F.pp_print_string fmt
-    ("val _ = new_type (\"" ^ def_name ^ ", " ^ string_of_int num_params ^ ")");
+    ("val _ = new_type (\"" ^ def_name ^ "\", " ^ string_of_int num_params ^ ")");
   F.pp_print_space fmt ()
 
 (** Extract an empty record type declaration to HOL4.
@@ -1874,7 +1874,7 @@ let extract_state_type (fmt : F.formatter) (ctx : extraction_ctx)
           F.pp_print_space fmt ();
           F.pp_print_string fmt "Type0"
       | HOL4 ->
-          F.pp_print_string fmt ("val _ = new_type (" ^ state_name ^ ", 0)")
+          F.pp_print_string fmt ("val _ = new_type (\"" ^ state_name ^ "\", 0)")
       | Coq | Lean -> print_axiom ())
   | Declared -> (
       match !backend with
@@ -1887,7 +1887,7 @@ let extract_state_type (fmt : F.formatter) (ctx : extraction_ctx)
           F.pp_print_space fmt ();
           F.pp_print_string fmt "Type0"
       | HOL4 ->
-          F.pp_print_string fmt ("val _ = new_type (" ^ state_name ^ ", 0)")
+          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 ();
@@ -3158,26 +3158,34 @@ let extract_fun_decl_hol4_opaque (ctx : extraction_ctx) (fmt : F.formatter)
   (* 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
+    ctx_get_local_function with_opaque_pre def.def_id def.loop_id def.back_id
+      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
+  (* Add breaks to insert new lines between definitions *)
+  F.pp_print_break fmt 0 0;
   (* Open a box for the whole definition *)
-  F.pp_open_hovbox fmt ctx.indent_incr;
+  F.pp_open_hvbox fmt ctx.indent_incr;
   (* Generate: `val _ = new_constant ("...",` *)
-  F.pp_print_string fmt ("val _ = new_constant (\"" ^ def_name ^ ", ");
+  F.pp_print_string fmt ("val _ = new_constant (\"" ^ def_name ^ "\",");
+  F.pp_print_space fmt ();
   (* Open a box for the type *)
-  F.pp_open_hvbox fmt 0;
+  F.pp_open_hovbox fmt 0;
+  F.pp_print_string fmt "“:";
   (* 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_print_string fmt "”";
   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 ()
+  F.pp_close_box fmt ();
+  (* Add breaks to insert new lines between definitions *)
+  F.pp_print_break fmt 0 0
 
 (** Extract a function declaration.
 
@@ -3211,6 +3219,15 @@ let extract_global_decl_body_gen (ctx : extraction_ctx) (fmt : F.formatter)
     (extract_body : (F.formatter -> unit) Option.t) : unit =
   let is_opaque = Option.is_none extract_body in
 
+  (* HOL4: Definition wrapper *)
+  if !backend = HOL4 then (
+    (* Open a vertical box: we *must* break lines *)
+    F.pp_open_vbox fmt 0;
+    F.pp_print_string fmt ("Definition " ^ name ^ "_def:");
+    F.pp_print_space fmt ();
+    F.pp_open_vbox fmt ctx.indent_incr;
+    F.pp_print_string fmt (String.make ctx.indent_incr ' '));
+
   (* Open the definition boxes (depth=0) *)
   F.pp_open_hvbox fmt 0;
   F.pp_open_hvbox fmt ctx.indent_incr;
@@ -3267,7 +3284,14 @@ let extract_global_decl_body_gen (ctx : extraction_ctx) (fmt : F.formatter)
     F.pp_print_string fmt ".");
 
   (* Close the outer definition box (depth=0) *)
-  F.pp_close_box fmt ()
+  F.pp_close_box fmt ();
+
+  (* HOL4: Definition wrapper *)
+  if !backend = HOL4 then (
+    F.pp_close_box fmt ();
+    F.pp_print_space fmt ();
+    F.pp_print_string fmt "End";
+    F.pp_close_box fmt ())
 
 (** Extract an opaque global declaration for HOL4.
 
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 1107a123..75fc7fe9 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -567,36 +567,51 @@ let export_functions_group_scc (fmt : Format.formatter) (config : gen_config)
          (odd (i : num) : bool result = if i = 0 then Return F else even (i - 1))
        `
      ]}
+
+     TODO: in practice splitting the code this way doesn't work so well: merge
+     the start/end decl group functions with the extract_fun_decl function?
   *)
-  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
-      let kind =
-        if is_opaque then
-          if config.interface then ExtractBase.Declared else ExtractBase.Assumed
-        else if not is_rec then ExtractBase.SingleNonRec
-        else if is_mut_rec then
-          (* If the functions are mutually recursive, we need to distinguish:
-           * - the first of the group
-           * - the last of the group
-           * - the inner functions
-           *)
-          if i = 0 then ExtractBase.MutRecFirst
-          else if i = decls_length - 1 then ExtractBase.MutRecLast
-          else ExtractBase.MutRecInner
-        else ExtractBase.SingleRec
-      in
-      let has_decr_clause =
-        has_decreases_clause def && config.extract_decreases_clauses
-      in
-      (* Check if the definition needs to be filtered or not *)
-      if
-        ((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;
-  Extract.end_fun_decl_group fmt is_rec decls
+  (* Filter the definitions - we generate a list of continuations *)
+  let extract_defs =
+    List.mapi
+      (fun i def ->
+        let is_opaque = Option.is_none def.Pure.body in
+        let kind =
+          if is_opaque then
+            if config.interface then ExtractBase.Declared
+            else ExtractBase.Assumed
+          else if not is_rec then ExtractBase.SingleNonRec
+          else if is_mut_rec then
+            (* If the functions are mutually recursive, we need to distinguish:
+             * - the first of the group
+             * - the last of the group
+             * - the inner functions
+             *)
+            if i = 0 then ExtractBase.MutRecFirst
+            else if i = decls_length - 1 then ExtractBase.MutRecLast
+            else ExtractBase.MutRecInner
+          else ExtractBase.SingleRec
+        in
+        let has_decr_clause =
+          has_decreases_clause def && config.extract_decreases_clauses
+        in
+        (* Check if the definition needs to be filtered or not *)
+        if
+          ((not is_opaque) && config.extract_transparent)
+          || (is_opaque && config.extract_opaque)
+        then
+          Some
+            (fun () ->
+              Extract.extract_fun_decl ctx.extract_ctx fmt kind has_decr_clause
+                def)
+        else None)
+      decls
+  in
+  let extract_defs = List.filter_map (fun x -> x) extract_defs in
+  if extract_defs <> [] then (
+    Extract.start_fun_decl_group ctx.extract_ctx fmt is_rec decls;
+    List.iter (fun f -> f ()) extract_defs;
+    Extract.end_fun_decl_group fmt is_rec decls)
 
 (** Export a group of function declarations.
 
@@ -828,6 +843,8 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (filename : string)
       Printf.fprintf out "open primitivesLib divDefLib\n";
       (* Add the custom imports and includes *)
       let imports = custom_imports @ custom_includes in
+      (* The imports are a list of module names: we need to add a "Theory" suffix *)
+      let imports = List.map (fun s -> s ^ "Theory") imports in
       if imports <> [] then
         let imports = String.concat " " imports in
         Printf.fprintf out "open %s\n\n" imports