From 1110b3da85e93ba0755a665edd5b8c986c54cef0 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 26 Oct 2023 16:15:35 +0200
Subject: Make minor modifications and update the array test for F*

---
 compiler/Driver.ml         |  4 +++-
 compiler/ExtractBase.ml    | 22 ++++++++++------------
 compiler/ExtractBuiltin.ml |  5 ++++-
 3 files changed, 17 insertions(+), 14 deletions(-)

(limited to 'compiler')

diff --git a/compiler/Driver.ml b/compiler/Driver.ml
index 3b9ea4d1..b660b5a5 100644
--- a/compiler/Driver.ml
+++ b/compiler/Driver.ml
@@ -162,7 +162,9 @@ let () =
     | FStar ->
         (* Some patterns are not supported *)
         decompose_monadic_let_bindings := false;
-        decompose_nested_let_patterns := false
+        decompose_nested_let_patterns := false;
+        (* F* can disambiguate the field names *)
+        record_fields_short_names := true
     | Coq ->
         (* Some patterns are not supported *)
         decompose_monadic_let_bindings := true;
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index 8f71116c..6faa40b2 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -1332,22 +1332,20 @@ let default_fun_suffix (num_loops : int) (loop_id : LoopId.id option)
   let rg_suff =
     (* TODO: make all the backends match what is done for Lean *)
     match rg with
-    | None -> (
-        match !Config.backend with
-        | FStar | Coq | HOL4 -> "_fwd"
-        | Lean ->
-            (* In order to avoid name conflicts:
-             * - if the forward is eliminated, we add the suffix "_fwd" (it won't be used)
-             * - otherwise, no suffix (because the backward functions will have a suffix)
-             *)
-            if num_backs = 1 && not keep_fwd then "_fwd" else "")
+    | None ->
+        if
+          (* In order to avoid name conflicts:
+           * - if the forward is eliminated, we add the suffix "_fwd" (it won't be used)
+           * - otherwise, no suffix (because the backward functions will have a suffix)
+           *)
+          num_backs = 1 && not keep_fwd
+        then "_fwd"
+        else ""
     | Some rg ->
         assert (num_region_groups > 0 && num_backs > 0);
         if num_backs = 1 then
           (* Exactly one backward function *)
-          match !Config.backend with
-          | FStar | Coq | HOL4 -> if not keep_fwd then "_fwd_back" else "_back"
-          | Lean -> if not keep_fwd then "" else "_back"
+          if not keep_fwd then "" else "_back"
         else if
           (* Several region groups/backward functions:
              - if all the regions in the group have names, we use those names
diff --git a/compiler/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml
index 2dbacce3..c6bde9c2 100644
--- a/compiler/ExtractBuiltin.ml
+++ b/compiler/ExtractBuiltin.ml
@@ -149,7 +149,10 @@ let builtin_types () : builtin_type_info list =
           let fields =
             List.map
               (fun (rname, name) ->
-                (rname, backend_choice (extract_name ^ name) name))
+                ( rname,
+                  match !backend with
+                  | FStar | Lean -> name
+                  | Coq | HOL4 -> extract_name ^ "_" ^ name ))
               fields
           in
           let constructor = mk_struct_constructor extract_name in
-- 
cgit v1.2.3