From a781ea75c1860c76c5577faa57efcdb0db910612 Mon Sep 17 00:00:00 2001
From: Escherichia
Date: Fri, 29 Mar 2024 10:56:52 +0100
Subject: Added meta information to names_map_id field in names_map type

---
 compiler/ExtractBase.ml | 45 +++++++++++++++++++++++----------------------
 1 file changed, 23 insertions(+), 22 deletions(-)

(limited to 'compiler')

diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index 74ac9e32..96f816cb 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -237,7 +237,7 @@ module IdSet = Collections.MakeSet (IdOrderedType)
   *)
 type names_map = {
   id_to_name : string IdMap.t;
-  name_to_id : id StringMap.t;
+  name_to_id : (id * Meta.meta option) StringMap.t;
       (** The name to id map is used to look for name clashes, and generate nice
           debugging messages: if there is a name clash, it is useful to know
           precisely which identifiers are mapped to the same name...
@@ -253,8 +253,8 @@ let empty_names_map : names_map =
   }
 
 (** Small helper to report name collision *)
-let report_name_collision (id_to_string : id -> string) (id1 : id) (id2 : id)
-    (name : string) : unit =
+let report_name_collision (id_to_string : id -> string)
+    (id1, meta : id * Meta.meta option) (id2 : id) (name : string) : unit =
   let id1 = "\n- " ^ id_to_string id1 in
   let id2 = "\n- " ^ id_to_string id2 in
   let err =
@@ -263,9 +263,10 @@ let report_name_collision (id_to_string : id -> string) (id1 : id) (id2 : id)
     ^ "\nYou may want to rename some of your definitions, or report an issue."
   in
   (* If we fail hard on errors, raise an exception *)
-  save_error __FILE__ __LINE__ None err
+  save_error __FILE__ __LINE__ meta err
 
-let names_map_get_id_from_name (name : string) (nm : names_map) : id option =
+let names_map_get_id_from_name (name : string) (nm : names_map) :
+    (id * Meta.meta option) option =
   StringMap.find_opt name nm.name_to_id
 
 let names_map_check_collision (id_to_string : id -> string) (id : id)
@@ -277,15 +278,15 @@ let names_map_check_collision (id_to_string : id -> string) (id : id)
       report_name_collision id_to_string clash id name
 
 (** Insert bindings in a names map without checking for collisions *)
-let names_map_add_unchecked (id : id) (name : string) (nm : names_map) :
+let names_map_add_unchecked (id, meta : id * Meta.meta option) (name : string) (nm : names_map) :
     names_map =
   (* Insert *)
   let id_to_name = IdMap.add id name nm.id_to_name in
-  let name_to_id = StringMap.add name id nm.name_to_id in
+  let name_to_id= StringMap.add name (id, meta) nm.name_to_id in
   let names_set = StringSet.add name nm.names_set in
   { id_to_name; name_to_id; names_set }
 
-let names_map_add (id_to_string : id -> string) (id : id) (name : string)
+let names_map_add (id_to_string : id -> string) (id, meta : id * meta option) (name : string)
     (nm : names_map) : names_map =
   (* Check if there is a clash *)
   names_map_check_collision id_to_string id name nm;
@@ -296,9 +297,9 @@ let names_map_add (id_to_string : id -> string) (id : id) (name : string)
        ^ ":\nThe chosen name is already in the names set: " ^ name
      in
      (* If we fail hard on errors, raise an exception *)
-     save_error __FILE__ __LINE__ None err);
+     save_error __FILE__ __LINE__ meta err);
   (* Insert *)
-  names_map_add_unchecked id name nm
+  names_map_add_unchecked (id, meta) name nm
 
 (** The unsafe names map stores mappings from identifiers to names which might
     collide. For some backends and some names, it might be acceptable to have
@@ -384,7 +385,7 @@ let allow_collisions (id : id) : bool =
 
 (** The [id_to_string] function to print nice debugging messages if there are
     collisions *)
-let names_maps_add (id_to_string : id -> string) (id : id) (name : string)
+let names_maps_add (meta : Meta.meta option) (id_to_string : id -> string) (id : id) (name : string)
     (nm : names_maps) : names_maps =
   (* We do not use the same name map if we allow/disallow collisions.
      We notably use it for field names: some backends like Lean can use the
@@ -415,10 +416,10 @@ let names_maps_add (id_to_string : id -> string) (id : id) (name : string)
     *)
     let strict_names_map =
       if strict_collisions id then
-        names_map_add id_to_string id name nm.strict_names_map
+        names_map_add id_to_string (id, meta) name nm.strict_names_map
       else nm.strict_names_map
     in
-    let names_map = names_map_add id_to_string id name nm.names_map in
+    let names_map = names_map_add id_to_string (id, meta) name nm.names_map in
     { nm with strict_names_map; names_map }
 
 (** The [id_to_string] function to print nice debugging messages if there are
@@ -468,20 +469,20 @@ type names_map_init = {
 
 let names_maps_add_assumed_type (id_to_string : id -> string) (id : assumed_ty)
     (name : string) (nm : names_maps) : names_maps =
-  names_maps_add id_to_string (TypeId (TAssumed id)) name nm
+  names_maps_add None id_to_string (TypeId (TAssumed id)) name nm
 
 let names_maps_add_assumed_struct (id_to_string : id -> string)
     (id : assumed_ty) (name : string) (nm : names_maps) : names_maps =
-  names_maps_add id_to_string (StructId (TAssumed id)) name nm
+  names_maps_add None id_to_string (StructId (TAssumed id)) name nm
 
 let names_maps_add_assumed_variant (id_to_string : id -> string)
     (id : assumed_ty) (variant_id : VariantId.id) (name : string)
     (nm : names_maps) : names_maps =
-  names_maps_add id_to_string (VariantId (TAssumed id, variant_id)) name nm
+  names_maps_add None id_to_string (VariantId (TAssumed id, variant_id)) name nm
 
-let names_maps_add_function (id_to_string : id -> string) (fid : fun_id)
+let names_maps_add_function (id_to_string : id -> string) (fid, meta : fun_id * meta option)
     (name : string) (nm : names_maps) : names_maps =
-  names_maps_add id_to_string (FunId fid) name nm
+  names_maps_add meta id_to_string (FunId fid) name nm
 
 let bool_name () = if !backend = Lean then "Bool" else "bool"
 let char_name () = if !backend = Lean then "Char" else "char"
@@ -659,7 +660,7 @@ let id_to_string (meta : Meta.meta option) (id : id) (ctx : extraction_ctx) :
 let ctx_add (meta : Meta.meta) (id : id) (name : string) (ctx : extraction_ctx)
     : extraction_ctx =
   let id_to_string (id : id) : string = id_to_string (Some meta) id ctx in
-  let names_maps = names_maps_add id_to_string id name ctx.names_maps in
+  let names_maps = names_maps_add (Some meta) id_to_string id name ctx.names_maps in
   { ctx with names_maps }
 
 let ctx_get (meta : Meta.meta option) (id : id) (ctx : extraction_ctx) : string
@@ -1125,7 +1126,7 @@ let initialize_names_maps () : names_maps =
         (* There is duplication in the keywords so we don't check the collisions
            while registering them (what is important is that there are no collisions
            between keywords and user-defined identifiers) *)
-        names_map_add_unchecked UnknownId name nm)
+        names_map_add_unchecked (UnknownId, None) name nm)
       strict_names_map keywords
   in
   let nm = { names_map; unsafe_names_map; strict_names_map } in
@@ -1155,9 +1156,9 @@ let initialize_names_maps () : names_maps =
   in
   let assumed_functions =
     List.map
-      (fun (fid, name) -> (FromLlbc (Pure.FunId (FAssumed fid), None), name))
+      (fun (fid, name) -> ((FromLlbc (Pure.FunId (FAssumed fid), None), None), name))
       init.assumed_llbc_functions
-    @ List.map (fun (fid, name) -> (Pure fid, name)) init.assumed_pure_functions
+    @ List.map (fun (fid, name) -> ((Pure fid, None), name)) init.assumed_pure_functions
   in
   let nm =
     List.fold_left
-- 
cgit v1.2.3


From a25f3bc7fe1dcddc952b4dcbb7b732bdf095197e Mon Sep 17 00:00:00 2001
From: Escherichia
Date: Wed, 3 Apr 2024 18:23:46 +0200
Subject: rebased branch

---
 compiler/ExtractBase.ml | 32 +++++++++++++++++++-------------
 1 file changed, 19 insertions(+), 13 deletions(-)

(limited to 'compiler')

diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index 96f816cb..34b5ad64 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -254,7 +254,7 @@ let empty_names_map : names_map =
 
 (** Small helper to report name collision *)
 let report_name_collision (id_to_string : id -> string)
-    (id1, meta : id * Meta.meta option) (id2 : id) (name : string) : unit =
+    ((id1, meta) : id * Meta.meta option) (id2 : id) (name : string) : unit =
   let id1 = "\n- " ^ id_to_string id1 in
   let id2 = "\n- " ^ id_to_string id2 in
   let err =
@@ -278,16 +278,16 @@ let names_map_check_collision (id_to_string : id -> string) (id : id)
       report_name_collision id_to_string clash id name
 
 (** Insert bindings in a names map without checking for collisions *)
-let names_map_add_unchecked (id, meta : id * Meta.meta option) (name : string) (nm : names_map) :
-    names_map =
+let names_map_add_unchecked ((id, meta) : id * Meta.meta option) (name : string)
+    (nm : names_map) : names_map =
   (* Insert *)
   let id_to_name = IdMap.add id name nm.id_to_name in
-  let name_to_id= StringMap.add name (id, meta) nm.name_to_id in
+  let name_to_id = StringMap.add name (id, meta) nm.name_to_id in
   let names_set = StringSet.add name nm.names_set in
   { id_to_name; name_to_id; names_set }
 
-let names_map_add (id_to_string : id -> string) (id, meta : id * meta option) (name : string)
-    (nm : names_map) : names_map =
+let names_map_add (id_to_string : id -> string) ((id, meta) : id * meta option)
+    (name : string) (nm : names_map) : names_map =
   (* Check if there is a clash *)
   names_map_check_collision id_to_string id name nm;
   (* Sanity check *)
@@ -385,8 +385,8 @@ let allow_collisions (id : id) : bool =
 
 (** The [id_to_string] function to print nice debugging messages if there are
     collisions *)
-let names_maps_add (meta : Meta.meta option) (id_to_string : id -> string) (id : id) (name : string)
-    (nm : names_maps) : names_maps =
+let names_maps_add (meta : Meta.meta option) (id_to_string : id -> string)
+    (id : id) (name : string) (nm : names_maps) : names_maps =
   (* We do not use the same name map if we allow/disallow collisions.
      We notably use it for field names: some backends like Lean can use the
      type information to disambiguate field projections.
@@ -480,8 +480,9 @@ let names_maps_add_assumed_variant (id_to_string : id -> string)
     (nm : names_maps) : names_maps =
   names_maps_add None id_to_string (VariantId (TAssumed id, variant_id)) name nm
 
-let names_maps_add_function (id_to_string : id -> string) (fid, meta : fun_id * meta option)
-    (name : string) (nm : names_maps) : names_maps =
+let names_maps_add_function (id_to_string : id -> string)
+    ((fid, meta) : fun_id * meta option) (name : string) (nm : names_maps) :
+    names_maps =
   names_maps_add meta id_to_string (FunId fid) name nm
 
 let bool_name () = if !backend = Lean then "Bool" else "bool"
@@ -660,7 +661,9 @@ let id_to_string (meta : Meta.meta option) (id : id) (ctx : extraction_ctx) :
 let ctx_add (meta : Meta.meta) (id : id) (name : string) (ctx : extraction_ctx)
     : extraction_ctx =
   let id_to_string (id : id) : string = id_to_string (Some meta) id ctx in
-  let names_maps = names_maps_add (Some meta) id_to_string id name ctx.names_maps in
+  let names_maps =
+    names_maps_add (Some meta) id_to_string id name ctx.names_maps
+  in
   { ctx with names_maps }
 
 let ctx_get (meta : Meta.meta option) (id : id) (ctx : extraction_ctx) : string
@@ -1156,9 +1159,12 @@ let initialize_names_maps () : names_maps =
   in
   let assumed_functions =
     List.map
-      (fun (fid, name) -> ((FromLlbc (Pure.FunId (FAssumed fid), None), None), name))
+      (fun (fid, name) ->
+        ((FromLlbc (Pure.FunId (FAssumed fid), None), None), name))
       init.assumed_llbc_functions
-    @ List.map (fun (fid, name) -> ((Pure fid, None), name)) init.assumed_pure_functions
+    @ List.map
+        (fun (fid, name) -> ((Pure fid, None), name))
+        init.assumed_pure_functions
   in
   let nm =
     List.fold_left
-- 
cgit v1.2.3


From 8a8f3ee2e444542112a3b0ea0b4e6283b1893aaa Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 4 Apr 2024 10:57:01 +0200
Subject: Make minor modifications

---
 compiler/ExtractBase.ml | 36 +++++++++++++++++++++---------------
 1 file changed, 21 insertions(+), 15 deletions(-)

(limited to 'compiler')

diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index 34b5ad64..451c2c41 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -254,28 +254,34 @@ let empty_names_map : names_map =
 
 (** Small helper to report name collision *)
 let report_name_collision (id_to_string : id -> string)
-    ((id1, meta) : id * Meta.meta option) (id2 : id) (name : string) : unit =
-  let id1 = "\n- " ^ id_to_string id1 in
-  let id2 = "\n- " ^ id_to_string id2 in
+    ((id1, meta1) : id * Meta.meta option) (id2 : id) (meta2 : Meta.meta option)
+    (name : string) : unit =
+  let meta_to_string (meta : Meta.meta option) =
+    match meta with
+    | None -> ""
+    | Some meta -> "\n  " ^ Errors.meta_to_string meta.span
+  in
+  let id1 = "\n- " ^ id_to_string id1 ^ meta_to_string meta1 in
+  let id2 = "\n- " ^ id_to_string id2 ^ meta_to_string meta2 in
   let err =
     "Name clash detected: the following identifiers are bound to the same name \
      \"" ^ name ^ "\":" ^ id1 ^ id2
     ^ "\nYou may want to rename some of your definitions, or report an issue."
   in
   (* If we fail hard on errors, raise an exception *)
-  save_error __FILE__ __LINE__ meta err
+  save_error __FILE__ __LINE__ meta1 err
 
 let names_map_get_id_from_name (name : string) (nm : names_map) :
     (id * Meta.meta option) option =
   StringMap.find_opt name nm.name_to_id
 
 let names_map_check_collision (id_to_string : id -> string) (id : id)
-    (name : string) (nm : names_map) : unit =
+    (meta : Meta.meta option) (name : string) (nm : names_map) : unit =
   match names_map_get_id_from_name name nm with
   | None -> () (* Ok *)
   | Some clash ->
       (* There is a clash: print a nice debugging message for the user *)
-      report_name_collision id_to_string clash id name
+      report_name_collision id_to_string clash id meta name
 
 (** Insert bindings in a names map without checking for collisions *)
 let names_map_add_unchecked ((id, meta) : id * Meta.meta option) (name : string)
@@ -289,7 +295,7 @@ let names_map_add_unchecked ((id, meta) : id * Meta.meta option) (name : string)
 let names_map_add (id_to_string : id -> string) ((id, meta) : id * meta option)
     (name : string) (nm : names_map) : names_map =
   (* Check if there is a clash *)
-  names_map_check_collision id_to_string id name nm;
+  names_map_check_collision id_to_string id meta name nm;
   (* Sanity check *)
   (if StringSet.mem name nm.names_set then
      let err =
@@ -385,8 +391,8 @@ let allow_collisions (id : id) : bool =
 
 (** The [id_to_string] function to print nice debugging messages if there are
     collisions *)
-let names_maps_add (meta : Meta.meta option) (id_to_string : id -> string)
-    (id : id) (name : string) (nm : names_maps) : names_maps =
+let names_maps_add (id_to_string : id -> string) (id : id)
+    (meta : Meta.meta option) (name : string) (nm : names_maps) : names_maps =
   (* We do not use the same name map if we allow/disallow collisions.
      We notably use it for field names: some backends like Lean can use the
      type information to disambiguate field projections.
@@ -401,7 +407,7 @@ let names_maps_add (meta : Meta.meta option) (id_to_string : id -> string)
   *)
   if allow_collisions id then (
     (* Check with the ids which are considered to be strict on collisions *)
-    names_map_check_collision id_to_string id name nm.strict_names_map;
+    names_map_check_collision id_to_string id meta name nm.strict_names_map;
     {
       nm with
       unsafe_names_map = unsafe_names_map_add id name nm.unsafe_names_map;
@@ -469,21 +475,21 @@ type names_map_init = {
 
 let names_maps_add_assumed_type (id_to_string : id -> string) (id : assumed_ty)
     (name : string) (nm : names_maps) : names_maps =
-  names_maps_add None id_to_string (TypeId (TAssumed id)) name nm
+  names_maps_add id_to_string (TypeId (TAssumed id)) None name nm
 
 let names_maps_add_assumed_struct (id_to_string : id -> string)
     (id : assumed_ty) (name : string) (nm : names_maps) : names_maps =
-  names_maps_add None id_to_string (StructId (TAssumed id)) name nm
+  names_maps_add id_to_string (StructId (TAssumed id)) None name nm
 
 let names_maps_add_assumed_variant (id_to_string : id -> string)
     (id : assumed_ty) (variant_id : VariantId.id) (name : string)
     (nm : names_maps) : names_maps =
-  names_maps_add None id_to_string (VariantId (TAssumed id, variant_id)) name nm
+  names_maps_add id_to_string (VariantId (TAssumed id, variant_id)) None name nm
 
 let names_maps_add_function (id_to_string : id -> string)
     ((fid, meta) : fun_id * meta option) (name : string) (nm : names_maps) :
     names_maps =
-  names_maps_add meta id_to_string (FunId fid) name nm
+  names_maps_add id_to_string (FunId fid) meta name nm
 
 let bool_name () = if !backend = Lean then "Bool" else "bool"
 let char_name () = if !backend = Lean then "Char" else "char"
@@ -662,7 +668,7 @@ let ctx_add (meta : Meta.meta) (id : id) (name : string) (ctx : extraction_ctx)
     : extraction_ctx =
   let id_to_string (id : id) : string = id_to_string (Some meta) id ctx in
   let names_maps =
-    names_maps_add (Some meta) id_to_string id name ctx.names_maps
+    names_maps_add id_to_string id (Some meta) name ctx.names_maps
   in
   { ctx with names_maps }
 
-- 
cgit v1.2.3


From eae7ce912c8bae44f98e1d489aba5618c0029bd2 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 4 Apr 2024 10:59:46 +0200
Subject: Make a minor modification

---
 compiler/ExtractBase.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'compiler')

diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index 451c2c41..d760ab1e 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -268,8 +268,10 @@ let report_name_collision (id_to_string : id -> string)
      \"" ^ name ^ "\":" ^ id1 ^ id2
     ^ "\nYou may want to rename some of your definitions, or report an issue."
   in
-  (* If we fail hard on errors, raise an exception *)
-  save_error __FILE__ __LINE__ meta1 err
+  (* If we fail hard on errors, raise an exception - we don't link this error
+     to any meta information because we already put the span information about
+     the two problematic definitions in the error message above. *)
+  save_error __FILE__ __LINE__ None err
 
 let names_map_get_id_from_name (name : string) (nm : names_map) :
     (id * Meta.meta option) option =
-- 
cgit v1.2.3


From f58161f23ccb4bff2080a7c63105d80777c33362 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 4 Apr 2024 11:00:23 +0200
Subject: Update a comment

---
 compiler/ExtractBase.ml | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

(limited to 'compiler')

diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index d760ab1e..f8d3cd96 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -268,9 +268,11 @@ let report_name_collision (id_to_string : id -> string)
      \"" ^ name ^ "\":" ^ id1 ^ id2
     ^ "\nYou may want to rename some of your definitions, or report an issue."
   in
-  (* If we fail hard on errors, raise an exception - we don't link this error
-     to any meta information because we already put the span information about
-     the two problematic definitions in the error message above. *)
+  (* Register the error.
+
+     We don't link this error to any meta information because we already put
+     the span information about the two problematic definitions in the error
+     message above. *)
   save_error __FILE__ __LINE__ None err
 
 let names_map_get_id_from_name (name : string) (nm : names_map) :
-- 
cgit v1.2.3


From 795e2107e305d425efdf6071b29f186cae83656b Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 4 Apr 2024 11:56:09 +0200
Subject: Update the names of the synthesized backward functions

---
 compiler/ExtractBase.ml    | 6 ++++--
 compiler/SymbolicToPure.ml | 9 +++++++++
 2 files changed, 13 insertions(+), 2 deletions(-)

(limited to 'compiler')

diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index 74ac9e32..0a7c8df2 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -1662,9 +1662,11 @@ let ctx_compute_var_basename (meta : Meta.meta) (ctx : extraction_ctx)
   in
   (* If there is a basename, we use it *)
   match basename with
-  | Some basename ->
+  | Some basename -> (
       (* This should be a no-op *)
-      to_snake_case basename
+      match !Config.backend with
+      | Lean -> basename
+      | FStar | Coq | HOL4 -> to_snake_case basename)
   | None -> (
       (* No basename: we use the first letter of the type *)
       match ty with
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 0c30f44c..7e970029 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -1502,6 +1502,15 @@ let fresh_back_vars_for_current_fun (ctx : bs_ctx)
         match ty with None -> None | Some ty -> Some (name, ty))
       back_vars
   in
+  (* If there is one backward function or less, we use the name "back"
+     (there is no point in using the lifetime name, and it makes the
+     code generation more stable) *)
+  let num_back_vars = List.length (List.filter_map (fun x -> x) back_vars) in
+  let back_vars =
+    if num_back_vars = 1 then
+      List.map (Option.map (fun (_, ty) -> (Some "back", ty))) back_vars
+    else back_vars
+  in
   fresh_opt_vars back_vars ctx
 
 (** IMPORTANT: do not use this one directly, but rather {!symbolic_value_to_texpression} *)
-- 
cgit v1.2.3


From bac38f94aacf4a0d621b0b2d2c423db9e0c6f175 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 4 Apr 2024 13:21:08 +0200
Subject: Improve the name of the backward functions further

---
 compiler/PureUtils.ml      | 11 ++++++++---
 compiler/SymbolicToPure.ml | 13 +++++++++++--
 2 files changed, 19 insertions(+), 5 deletions(-)

(limited to 'compiler')

diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml
index 4bc90872..6f44bb74 100644
--- a/compiler/PureUtils.ml
+++ b/compiler/PureUtils.ml
@@ -75,10 +75,15 @@ let inputs_info_is_wf (info : inputs_info) : bool =
 let fun_sig_info_is_wf (info : fun_sig_info) : bool =
   inputs_info_is_wf info.fwd_info
 
+let opt_dest_arrow_ty (ty : ty) : (ty * ty) option =
+  match ty with TArrow (arg_ty, ret_ty) -> Some (arg_ty, ret_ty) | _ -> None
+
+let is_arrow_ty (ty : ty) : bool = Option.is_some (opt_dest_arrow_ty ty)
+
 let dest_arrow_ty (meta : Meta.meta) (ty : ty) : ty * ty =
-  match ty with
-  | TArrow (arg_ty, ret_ty) -> (arg_ty, ret_ty)
-  | _ -> craise __FILE__ __LINE__ meta "Not an arrow type"
+  match opt_dest_arrow_ty ty with
+  | Some (arg_ty, ret_ty) -> (arg_ty, ret_ty)
+  | None -> craise __FILE__ __LINE__ meta "Not an arrow type"
 
 let compute_literal_type (cv : literal) : literal_type =
   match cv with
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 7e970029..67fd2c9b 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -1499,7 +1499,14 @@ let fresh_back_vars_for_current_fun (ctx : bs_ctx)
   let back_vars =
     List.map
       (fun (name, ty) ->
-        match ty with None -> None | Some ty -> Some (name, ty))
+        match ty with
+        | None -> None
+        | Some ty ->
+            (* If the type is not an arrow type, don't use the name "back"
+               (it is a backward function with no inputs, that is to say a
+               value) *)
+            let name = if is_arrow_ty ty then name else None in
+            Some (name, ty))
       back_vars
   in
   (* If there is one backward function or less, we use the name "back"
@@ -1508,7 +1515,9 @@ let fresh_back_vars_for_current_fun (ctx : bs_ctx)
   let num_back_vars = List.length (List.filter_map (fun x -> x) back_vars) in
   let back_vars =
     if num_back_vars = 1 then
-      List.map (Option.map (fun (_, ty) -> (Some "back", ty))) back_vars
+      List.map
+        (Option.map (fun (name, ty) -> (Option.map (fun _ -> "back") name, ty)))
+        back_vars
     else back_vars
   in
   fresh_opt_vars back_vars ctx
-- 
cgit v1.2.3


From ec7a1d3c94846a94481a487dd077efb6ddb108fe Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 4 Apr 2024 13:27:02 +0200
Subject: Make a minor update in SymbolicToPure

---
 compiler/SymbolicToPure.ml | 15 +++++++--------
 1 file changed, 7 insertions(+), 8 deletions(-)

(limited to 'compiler')

diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 67fd2c9b..5cd13072 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -2258,15 +2258,14 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) :
                  (fun ty ->
                    match ty with
                    | None -> None
-                   | Some (back_sg, ty) ->
-                       (* We insert a name for the variable only if the function
-                          can fail: if it can fail, it means the call returns a backward
-                          function. Otherwise, it directly returns the value given
-                          back by the backward function, which means we shouldn't
-                          give it a name like "back..." (it doesn't make sense) *)
+                   | Some (_back_sg, ty) ->
+                       (* We insert a name for the variable only if the type
+                          is an arrow type. If it is not, it means the backward
+                          function is degenerate (it takes no inputs) so it is
+                          not a function anymore but a value: it doesn't make
+                          sense to use a name like "back...". *)
                        let name =
-                         if back_sg.effect_info.can_fail then Some back_fun_name
-                         else None
+                         if is_arrow_ty ty then Some back_fun_name else None
                        in
                        Some (name, ty))
                  back_tys)
-- 
cgit v1.2.3