Make progress on PureToExtract

1 files changed, 93 insertions, 95 deletions

diff --git a/src/PureToExtract.ml b/src/PureToExtract.ml
index b9f5a9a1..d5fd4432 100644
--- a/src/PureToExtract.ml
+++ b/src/PureToExtract.ml
@@ -25,18 +25,6 @@ type extraction_ctx = {
     functions, etc.
  *)
 
-(** We use identifiers to look for name clashes *)
-type id =
-  | FunId of FunDefId.id * RegionGroupId.id option
-  | TypeId of TypeDefId.id
-  | VarId of VarId.id
-  | UnknownId
-      (** Used for stored various strings like keywords, definitions which
-          should always be in context, etc. and which can't be linked to one
-          of the above.
-       *)
-[@@deriving show, ord]
-
 type region_group_info = {
   id : RegionGroupId.id;
       (** The id of the region group.
@@ -49,6 +37,9 @@ type region_group_info = {
        *)
 }
 
+module StringSet = Collections.MakeSet (Collections.OrderedString)
+module StringMap = Collections.MakeMap (Collections.OrderedString)
+
 type name = Identifiers.name
 
 type name_formatter = {
@@ -66,11 +57,18 @@ type name_formatter = {
           - region group information in case of a backward function
             (`None` if forward function)
        *)
-  var_basename : name -> string;
+  var_basename : StringSet.t -> ty -> string;
       (** Generates a variable basename.
+      
+          Inputs:
+          - the set of names used in the context so far
+          - the type of the variable (can be useful for heuristics, in order
+            not to always use "x" for instance, whenever naming anonymous
+            variables)
 
           Note that once the formatter generated a basename, we add an index
-          if necessary to prevent name clashes.
+          if necessary to prevent name clashes: the burden of name clashes checks
+          is thus on the caller's side.
        *)
 }
 (** A name formatter's role is to come up with name suggestions.
@@ -148,84 +146,84 @@ let compute_fun_def_name (ctx : extraction_ctx) (fmt : name_formatter)
   in
   fmt.fun_name fun_id basename num_region_groups rg_info
 
-(*
-  let name_to_string (n : name) : string = show_name n
-
-  module NameOrderedType = struct
-    type t = name
-
-    let compare = compare_name
-
-    let to_string = name_to_string
-
-    let pp_t = pp_name
-
-    let show_t = show_name
-  end
-
-  module NameMap = Collections.MakeMapInj (NameOrderedType) (Id.NameOrderedType)
-  (** Notice that we use the *injective* map to map identifiers to names.
-
-      Of course, even if those names (which are string lists) don't collide,
-      when converting them to strings we can still introduce collisions: we
-      check that later.
-
-      Note that we use injective maps for sanity: though we write the name
-      generation with collision in mind, it is always good to have such checks.
-  *)*)
-
-(*let translate_fun_name (fdef : A.fun_def) (bid : T.RegionGroupId.id option) :
-      Id.name =
-    let sg = fdef.signature in
-    (* General function to generate a suffix for a region group
-     * (i.e., an abstraction)*)
-    let rg_to_string (rg : T.region_var_group) : string =
-      (* We are just a little bit smart:
-         - if there is exactly one region id in the region group and this region
-           has a name, we use this name
-         - otherwise, we use the region number (note that region names shouldn't
-           start with numbers)
-      *)
-      match rg.T.regions with
-      | [ rid ] -> (
-          let rvar = T.RegionVarId.nth sg.region_params rid in
-          match rvar.name with
-          | None -> T.RegionGroupId.to_string rg.T.id
-          | Some name -> name)
-      | _ -> T.RegionGroupId.to_string rg.T.id
-    in
-    (* There are several cases:
-       - this is a forward function: we add "_fwd"
-       - this is a backward function:
-         - this function has one backward function: we add "_back"
-         - this function has several backward function: we add "_back" and an
-           additional suffix to identify the precise backward function
-    *)
-    let suffix =
-      match bid with
-      | None -> "_fwd"
-      | Some bid -> (
-          match sg.regions_hierarchy with
-          | [] ->
-              failwith "Unreachable"
-              (* we can't get there if we ask for a back function *)
-          | [ _ ] ->
-              (* Exactly one backward function *)
-              "_back"
-          | _ ->
-              (* Several backward functions *)
-              let rg = T.RegionGroupId.nth sg.regions_hierarchy bid in
-              "_back" ^ rg_to_string rg)
-    in
-    (* Final name *)
-    let rec add_to_last (n : Id.name) : Id.name =
-      match n with
-      | [] -> failwith "Unreachable"
-      | [ x ] -> [ x ^ suffix ]
-      | x :: n -> x :: add_to_last n
-    in
-    add_to_last fdef.name
-
-  (** Generates a name for a type (simply reuses the name in the definition) *)
-  let translate_type_name (def : T.type_def) : Id.name = def.T.name
-*)
+(** We use identifiers to look for name clashes *)
+type id =
+  | FunId of A.fun_id * RegionGroupId.id option
+  | TypeId of type_id
+  | VarId of VarId.id
+  | UnknownId
+      (** Used for stored various strings like keywords, definitions which
+          should always be in context, etc. and which can't be linked to one
+          of the above.
+       *)
+[@@deriving show, ord]
+
+module IdOrderedType = struct
+  type t = id
+
+  let compare = compare_id
+
+  let to_string = show_id
+
+  let pp_t = pp_id
+
+  let show_t = show_id
+end
+
+module IdMap = Collections.MakeMap (IdOrderedType)
+
+type names_map = {
+  id_to_name : string IdMap.t;
+  name_to_id : id 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...
+       *)
+  names_set : StringSet.t;
+}
+(** The names map stores the mappings from names to identifiers and vice-versa.
+
+      We use it for lookups (during the translation) and to check for name clashes.
+  *)
+
+let names_map_add (id : id) (name : string) (nm : names_map) : names_map =
+  (* Sanity check: no clashes *)
+  assert (not (StringSet.mem name nm.names_set));
+  (* 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 names_set = StringSet.add name nm.names_set in
+  { id_to_name; name_to_id; names_set }
+
+let names_map_find (id : id) (nm : names_map) : string =
+  IdMap.find id nm.id_to_name
+
+let names_map_find_function (id : A.fun_id) (rg : RegionGroupId.id option)
+    (nm : names_map) : string =
+  names_map_find (FunId (id, rg)) nm
+
+let names_map_find_local_function (id : FunDefId.id)
+    (rg : RegionGroupId.id option) (nm : names_map) : string =
+  names_map_find_function (A.Local id) rg nm
+
+let names_map_find_type (id : type_id) (nm : names_map) : string =
+  assert (id <> Tuple);
+  names_map_find (TypeId id) nm
+
+let names_map_find_local_type (id : TypeDefId.id) (nm : names_map) : string =
+  names_map_find_type (AdtId id) nm
+
+(** Make a basename unique (by adding an index).
+
+    We do this in an inefficient manner (by testing all indices starting from
+    0) but it shouldn't be a bottleneck.
+    
+    [add_index]: concatenates a given index to the variable's basename.
+ *)
+let var_basename_to_unique (names_set : StringSet.t) (add_index : int -> string)
+    : string =
+  let rec gen (i : int) : string =
+    let s = add_index i in
+    if StringSet.mem s names_set then gen (i + 1) else s
+  in
+  gen 0