Merge pull request #233 from AeneasVerif/son/borrow-check

Add a `-borrow-check` option

1 files changed, 22 insertions, 20 deletions

diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 0f887ec8..2bc9bb25 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -31,8 +31,9 @@ let translate_function_to_symbolics (trans_ctx : trans_ctx) (fdef : fun_decl) :
   | None -> None
   | Some _ ->
       (* Evaluate *)
-      let inputs, symb = evaluate_function_symbolic trans_ctx fdef in
-      Some (inputs, symb)
+      let synthesize = true in
+      let inputs, symb = evaluate_function_symbolic synthesize trans_ctx fdef in
+      Some (inputs, Option.get symb)
 
 (** Translate a function, by generating its forward and backward translations.
 
@@ -665,7 +666,7 @@ let export_functions_group (fmt : Format.formatter) (config : gen_config)
           let extract_decrease decl =
             let has_decr_clause = has_decreases_clause decl in
             if has_decr_clause then
-              match !Config.backend with
+              match Config.backend () with
               | Lean ->
                   Extract.extract_template_lean_termination_and_decreasing ctx
                     fmt decl
@@ -864,7 +865,7 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (fi : extract_file_info)
    * internal count is consistent with the state of the file.
    *)
   (* Create the header *)
-  (match !Config.backend with
+  (match Config.backend () with
   | 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
@@ -873,7 +874,7 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (fi : extract_file_info)
         "(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)\n";
       Printf.fprintf out "(** [%s]%s *)\n" fi.rust_module_name fi.custom_msg);
   (* Generate the imports *)
-  (match !Config.backend with
+  (match Config.backend () with
   | FStar ->
       Printf.fprintf out "module %s\n" fi.module_name;
       Printf.fprintf out "open Primitives\n";
@@ -957,7 +958,7 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (fi : extract_file_info)
   Format.pp_print_newline fmt ();
 
   (* Close the module *)
-  (match !Config.backend with
+  (match Config.backend () with
   | FStar -> ()
   | Lean -> if fi.in_namespace then Printf.fprintf out "end %s\n" fi.namespace
   | HOL4 -> Printf.fprintf out "val _ = export_theory ()\n"
@@ -1039,7 +1040,8 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
       trans_ctx;
       names_maps;
       indent_incr = 2;
-      use_dep_ite = !Config.backend = Lean && !Config.extract_decreases_clauses;
+      use_dep_ite =
+        Config.backend () = Lean && !Config.extract_decreases_clauses;
       trait_decl_id = None (* None by default *);
       is_provided_method = false (* false by default *);
       trans_trait_decls;
@@ -1113,13 +1115,13 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
         (* Convert the case *)
         let crate_name = StringUtils.to_camel_case basename in
         let crate_name =
-          if !Config.backend = HOL4 then
+          if Config.backend () = HOL4 then
             StringUtils.lowercase_first_letter crate_name
           else crate_name
         in
         (* We use the raw crate name for the namespaces *)
         let namespace =
-          match !Config.backend with
+          match Config.backend () with
           | FStar | Coq | HOL4 -> crate.name
           | Lean -> crate.name
         in
@@ -1144,7 +1146,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
 
   (* Lean reflects the module hierarchy within the filesystem, so we need to
      create more directories *)
-  if !Config.backend = Lean then (
+  if Config.backend () = Lean then (
     let ( ^^ ) = Filename.concat in
     if !Config.split_files then mkdir_if (dest_dir ^^ crate_name);
     if needs_clauses_module then (
@@ -1156,7 +1158,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
     (* Retrieve the executable's directory *)
     let exe_dir = Filename.dirname Sys.argv.(0) in
     let primitives_src_dest =
-      match !Config.backend with
+      match Config.backend () with
       | FStar -> Some ("/backends/fstar/Primitives.fst", "Primitives.fst")
       | Coq -> Some ("/backends/coq/Primitives.v", "Primitives.v")
       | Lean -> None
@@ -1190,18 +1192,18 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
 
   (* Extract the file(s) *)
   let module_delimiter =
-    match !Config.backend with
+    match Config.backend () with
     | FStar -> "."
     | Coq -> "_"
     | Lean -> "."
     | HOL4 -> "_"
   in
   let file_delimiter =
-    if !Config.backend = Lean then "/" else module_delimiter
+    if Config.backend () = Lean then "/" else module_delimiter
   in
   (* File extension for the "regular" modules *)
   let ext =
-    match !Config.backend with
+    match Config.backend () with
     | FStar -> ".fst"
     | Coq -> ".v"
     | Lean -> ".lean"
@@ -1209,7 +1211,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
   in
   (* File extension for the opaque module *)
   let opaque_ext =
-    match !Config.backend with
+    match Config.backend () with
     | FStar -> ".fsti"
     | Coq -> ".v"
     | Lean -> ".lean"
@@ -1253,7 +1255,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
             For the other backends, we generate a template file as a model
             for the file the user has to provide. *)
          let module_suffix, opaque_imported_suffix, custom_msg =
-           match !Config.backend with
+           match Config.backend () with
            | FStar ->
                ("TypesExternal", "TypesExternal", ": external type declarations")
            | HOL4 | Coq | Lean ->
@@ -1306,7 +1308,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
 
      (* Extract the non opaque types *)
      let types_filename_ext =
-       match !Config.backend with
+       match Config.backend () with
        | FStar -> ".fst"
        | Coq -> ".v"
        | Lean -> ".lean"
@@ -1377,7 +1379,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
             For the other backends, we generate a template file as a model
             for the file the user has to provide. *)
          let module_suffix, opaque_imported_suffix, custom_msg =
-           match !Config.backend with
+           match Config.backend () with
            | FStar ->
                ( "FunsExternal",
                  "FunsExternal",
@@ -1445,7 +1447,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
      let clauses_module =
        if needs_clauses_module then
          let clauses_submodule =
-           if !Config.backend = Lean then module_delimiter ^ "Clauses" else ""
+           if Config.backend () = Lean then module_delimiter ^ "Clauses" else ""
          in
          [ crate_name ^ clauses_submodule ^ module_delimiter ^ "Clauses" ]
        else []
@@ -1501,7 +1503,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
      extract_file gen_config ctx file_info);
 
   (* Generate the build file *)
-  match !Config.backend with
+  match Config.backend () with
   | Coq | FStar | HOL4 ->
       ()
       (* Nothing to do - TODO: we might want to generate the _CoqProject file for Coq.