summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2022-01-27 22:04:35 +0100
committerSon Ho2022-01-27 22:04:35 +0100
commit6070002cbc97a46b8c060a8ac58c0602a1fbf660 (patch)
tree032ad997592ef80fd3e84608f05e93e5c12caddb
parent8f397cd1c8b187ce1cc7e3ed8522b123496c9157 (diff)
Move some definitions from SymbolicToPure to PureToExtract
Diffstat (limited to '')
-rw-r--r--src/Logging.ml3
-rw-r--r--src/PureToExtract.ml103
-rw-r--r--src/SymbolicToPure.ml88
-rw-r--r--src/main.ml2
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.