Move some definitions from SymbolicToPure to PureToExtract

4 files changed, 108 insertions, 88 deletions

diff --git a/src/Logging.ml b/src/Logging.ml
index 23bf672d..ad600adc 100644
--- a/src/Logging.ml
+++ b/src/Logging.ml
@@ -15,6 +15,9 @@ let translate_log = L.get_logger "MainLogger.Translate"
 (** Logger for SymbolicToPure *)
 let symbolic_to_pure_log = L.get_logger "MainLogger.SymbolicToPure"
 
+(** Logger for PureToExtract *)
+let pure_to_extract_log = L.get_logger "MainLogger.PureToExtract"
+
 (** Logger for Interpreter *)
 let interpreter_log = L.get_logger "MainLogger.Interpreter"
 
diff --git a/src/PureToExtract.ml b/src/PureToExtract.ml
new file mode 100644
index 00000000..4b7b5ad8
--- /dev/null
+++ b/src/PureToExtract.ml
@@ -0,0 +1,103 @@
+(** This module is used to transform the pure ASTs to ASTs ready for extraction *)
+
+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
+
+(** 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
+
+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
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index e4fdebff..14bbc63f 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -15,92 +15,6 @@ module PP = PrintPure
 (** The local logger *)
 let log = L.symbolic_to_pure_log
 
-(** TODO: move this, it is not useful for symbolic -> pure *)
-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
-
-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
-
 (* TODO: move *)
 let mk_place_from_var (v : var) : place = { var = v.id; projection = [] }
 
@@ -373,7 +287,7 @@ let translate_type_def_kind (kind : T.type_def_kind) : type_def_kind =
 let translate_type_def (def : T.type_def) : type_def =
   (* Translate *)
   let def_id = def.T.def_id in
-  let name = translate_type_name def in
+  let name = def.name in
   (* Can't translate types with regions for now *)
   assert (def.region_params = []);
   let type_params = def.type_params in
diff --git a/src/main.ml b/src/main.ml
index a4de3d7a..1f996c2b 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -6,7 +6,7 @@ module A = CfimAst
 module I = Interpreter
 module EL = Easy_logging.Logging
 module TA = TypesAnalysis
-module P = Pure
+open PureToExtract
 
 (* This is necessary to have a backtrace when raising exceptions - for some
  * reason, the -g option doesn't work.