1 files changed, 209 insertions, 81 deletions

diff --git a/src/PureToExtract.ml b/src/PureToExtract.ml
index 4b7b5ad8..b9f5a9a1 100644
--- a/src/PureToExtract.ml
+++ b/src/PureToExtract.ml
@@ -1,103 +1,231 @@
-(** This module is used to transform the pure ASTs to ASTs ready for extraction *)
+(** This module is used to extract the pure ASTs to various theorem provers.
+    It defines utilities and helpers to make the work as easy as possible:
+    we try to factorize as much as possible the different extractions to the
+    backends we target.
+ *)
 
 open Errors
 open Pure
-open CfimAstUtils
-module Id = Identifiers
-module T = Types
-module V = Values
-module E = Expressions
-module A = CfimAst
-module M = Modules
-module S = SymbolicAst
-module TA = TypesAnalysis
-module L = Logging
-module PP = PrintPure
+open TranslateCore
+module C = Contexts
+module RegionVarId = T.RegionVarId
 
 (** The local logger *)
 let log = L.pure_to_extract_log
 
-type name =
-  | FunName of A.FunDefId.id * T.RegionVarId.id option
-  | TypeName of T.TypeDefId.id
-[@@deriving show, ord]
-
-let name_to_string (n : name) : string = show_name n
+type extraction_ctx = {
+  type_context : C.type_context;
+  fun_context : C.fun_context;
+}
+(** Extraction context.
 
-module NameOrderedType = struct
-  type t = name
-
-  let compare = compare_name
+    Note that the extraction context contains information coming from the
+    CFIM AST (not only the pure AST). This is useful for naming, for instance:
+    we use the region information to generate the names of the backward
+    functions, etc.
+ *)
 
-  let to_string = name_to_string
+(** 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]
 
-  let pp_t = pp_name
+type region_group_info = {
+  id : RegionGroupId.id;
+      (** The id of the region group.
+          Note that a simple way of generating unique names for backward
+          functions is to use the region group ids.
+       *)
+  region_names : string option list;
+      (** The names of the region variables included in this group.
+          Note that names are not always available...
+       *)
+}
 
-  let show_t = show_name
-end
+type name = Identifiers.name
 
-module NameMap = Collections.MakeMapInj (NameOrderedType) (Id.NameOrderedType)
-(** Notice that we use the *injective* map to map identifiers to names.
+type name_formatter = {
+  bool_name : string;
+  char_name : string;
+  int_name : integer_type -> string;
+  str_name : string;
+  type_name : name -> string;  (** Provided a basename, compute a type name. *)
+  fun_name : A.fun_id -> name -> int -> region_group_info option -> string;
+      (** Inputs:
+          - function id: this is especially useful to identify whether the
+            function is an assumed function or a local function
+          - function basename
+          - number of region groups
+          - region group information in case of a backward function
+            (`None` if forward function)
+       *)
+  var_basename : name -> string;
+      (** Generates a variable basename.
 
-    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 once the formatter generated a basename, we add an index
+          if necessary to prevent name clashes.
+       *)
+}
+(** A name formatter's role is to come up with name suggestions.
+    For instance, provided some information about a function (its basename,
+    information about the region group, etc.) it should come up with an
+    appropriate name for the forward/backward function.
     
-    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.
+    It can of course apply many transformations, like changing to camel case/
+    snake case, adding prefixes/suffixes, etc.
  *)
 
-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
+let compute_type_def_name (fmt : name_formatter) (def : type_def) : string =
+  fmt.type_name def.name
+
+(** A helper function: generates a function suffix from a region group
+    information.
+    TODO: move all those helpers.
+*)
+let default_fun_suffix (num_region_groups : int) (rg : region_group_info option)
+    : string =
   (* 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"
+     - [rg] is `Some`: this is a forward function:
+       - if there are no region groups (i.e., no backward functions) we don't
+         add any suffix
+       - if there are region gruops, we add "_fwd"
+     - [rg] is `None`: this is a backward function:
+       - this function has one region group: 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
+  match rg with
+  | None -> if num_region_groups = 0 then "" else "_fwd"
+  | Some rg ->
+      assert (num_region_groups > 0);
+      if num_region_groups = 1 then (* Exactly one backward function *)
+        "_back"
+      else if
+        (* Several region groups/backward functions:
+           - if all the regions in the group have names, we use those names
+           - otherwise we use an index
+        *)
+        List.for_all Option.is_some rg.region_names
+      then
+        (* Concatenate the region names *)
+        "_back" ^ String.concat "" (List.map Option.get rg.region_names)
+      else (* Use the region index *)
+        "_back" ^ RegionGroupId.to_string rg.id
+
+(** Extract information from a function, and give this information to a
+    [name_formatter] to generate a function's name.
+    
+    Note that we need region information coming from CFIM (when generating
+    the name for a backward function, we try to use the names of the regions
+    to 
+ *)
+let compute_fun_def_name (ctx : extraction_ctx) (fmt : name_formatter)
+    (fun_id : A.fun_id) (rg_id : RegionGroupId.id option) : string =
+  (* Lookup the function CFIM signature (we need the region information) *)
+  let sg = CfimAstUtils.lookup_fun_sig fun_id ctx.fun_context.fun_defs in
+  let basename = CfimAstUtils.lookup_fun_name fun_id ctx.fun_context.fun_defs in
+  (* Compute the regions information *)
+  let num_region_groups = List.length sg.regions_hierarchy in
+  let rg_info =
+    match rg_id with
+    | None -> None
+    | Some rg_id ->
+        let rg = RegionGroupId.nth sg.regions_hierarchy rg_id in
+        let regions =
+          List.map (fun rid -> RegionVarId.nth sg.region_params rid) rg.regions
+        in
+        let region_names =
+          List.map (fun (r : T.region_var) -> r.name) regions
+        in
+        Some { id = rg.id; region_names }
   in
-  add_to_last fdef.name
+  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
+  (** 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
+*)