had some fun writing an IsabelleHOL backend

(do not actually use this, most things are broken, and the primitives
lib barely exists and is simply incorrect. But it is enough to create
syntax-correct Isabelle code for relatively simply rust code, as long
as it does not contain any uses of traits)

1 files changed, 32 insertions, 7 deletions

diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 672fb22f..afd3420e 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -692,6 +692,9 @@ let export_functions_group (fmt : Format.formatter) (config : gen_config)
               | HOL4 ->
                   raise
                     (Failure "HOL4 doesn't have decreases/termination clauses")
+              | IsabelleHOL ->
+                  raise
+                    (Failure "HOL4 doesn't have decreases/termination clauses")
           in
           extract_decrease f.f;
           List.iter extract_decrease f.loops)
@@ -886,7 +889,7 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (fi : extract_file_info)
   | Lean ->
       Printf.fprintf out "-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS\n";
       Printf.fprintf out "-- [%s]%s\n" fi.rust_module_name fi.custom_msg
-  | Coq | FStar | HOL4 ->
+  | Coq | FStar | HOL4 | IsabelleHOL ->
       Printf.fprintf out
         "(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)\n";
       Printf.fprintf out "(** [%s]%s *)\n" fi.rust_module_name fi.custom_msg);
@@ -968,7 +971,23 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (fi : extract_file_info)
         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" fi.module_name);
+      Printf.fprintf out "val _ = new_theory \"%s\"\n\n" fi.module_name
+  | IsabelleHOL ->
+      Printf.fprintf out "theory \"%s\" imports\n" fi.module_name;
+      (* Add the custom imports and includes *)
+      let imports =
+        "Aeneas.Primitives"
+        :: "HOL-Library.Datatype_Records"
+        :: fi.custom_imports @ fi.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 ^ "\"") imports in
+      if imports <> [] then
+        let imports = String.concat "\n  " imports in
+        Printf.fprintf out "  %s\n" imports
+      else Printf.fprintf out "\n";
+      Printf.fprintf out "begin\n\n"
+      (* Initialize the theory *)
+  );
   (* From now onwards, we use the formatter *)
   (* Set the margin *)
   Format.pp_set_margin fmt 80;
@@ -988,7 +1007,8 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (fi : extract_file_info)
   | FStar -> ()
   | Lean -> if fi.in_namespace then Printf.fprintf out "end %s\n" fi.namespace
   | HOL4 -> Printf.fprintf out "val _ = export_theory ()\n"
-  | Coq -> Printf.fprintf out "End %s.\n" fi.module_name);
+  | Coq -> Printf.fprintf out "End %s.\n" fi.module_name
+  | IsabelleHOL -> Printf.fprintf out "end");
 
   (* Some logging *)
   if !Errors.error_list <> [] then
@@ -1148,7 +1168,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
         (* We use the raw crate name for the namespaces *)
         let namespace =
           match Config.backend () with
-          | FStar | Coq | HOL4 -> crate.name
+          | FStar | Coq | HOL4 | IsabelleHOL -> crate.name
           | Lean -> crate.name
         in
         (* Concatenate *)
@@ -1189,6 +1209,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
       | Coq -> Some ("/backends/coq/Primitives.v", "Primitives.v")
       | Lean -> None
       | HOL4 -> None
+      | IsabelleHOL -> None
     in
     match primitives_src_dest with
     | None -> ()
@@ -1223,6 +1244,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
     | Coq -> "_"
     | Lean -> "."
     | HOL4 -> "_"
+    | IsabelleHOL -> "."
   in
   let file_delimiter =
     if Config.backend () = Lean then "/" else module_delimiter
@@ -1234,6 +1256,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
     | Coq -> ".v"
     | Lean -> ".lean"
     | HOL4 -> "Script.sml"
+    | IsabelleHOL -> ".thy"
   in
   (* File extension for the opaque module *)
   let opaque_ext =
@@ -1242,6 +1265,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
     | Coq -> ".v"
     | Lean -> ".lean"
     | HOL4 -> "Script.sml"
+    | IsabelleHOL -> ".thy"
   in
 
   (* Extract one or several files, depending on the configuration *)
@@ -1284,7 +1308,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
            match Config.backend () with
            | FStar ->
                ("TypesExternal", "TypesExternal", ": external type declarations")
-           | HOL4 | Coq | Lean ->
+           | HOL4 | Coq | Lean | IsabelleHOL ->
                ( (* The name of the file we generate *)
                  "TypesExternal_Template",
                  (* The name of the file that will be imported by the Types
@@ -1339,6 +1363,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
        | Coq -> ".v"
        | Lean -> ".lean"
        | HOL4 -> "Script.sml"
+       | IsabelleHOL -> ".thy"
      in
      let types_filename =
        extract_filebasename ^ file_delimiter ^ "Types" ^ types_filename_ext
@@ -1410,7 +1435,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
                ( "FunsExternal",
                  "FunsExternal",
                  ": external function declarations" )
-           | HOL4 | Coq | Lean ->
+           | HOL4 | Coq | Lean | IsabelleHOL ->
                ( (* The name of the file we generate *)
                  "FunsExternal_Template",
                  (* The name of the file that will be imported by the Funs
@@ -1530,7 +1555,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
 
   (* Generate the build file *)
   match Config.backend () with
-  | Coq | FStar | HOL4 ->
+  | Coq | FStar | HOL4 | IsabelleHOL ->
       ()
       (* 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