summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/Assumed.ml9
-rw-r--r--src/CfimAst.ml1
-rw-r--r--src/CfimAstUtils.ml2
-rw-r--r--src/CfimOfJson.ml2
-rw-r--r--src/Identifiers.ml38
-rw-r--r--src/Names.ml39
-rw-r--r--src/Print.ml2
-rw-r--r--src/Pure.ml1
-rw-r--r--src/PureToExtract.ml22
-rw-r--r--src/Types.ml1
10 files changed, 63 insertions, 54 deletions
diff --git a/src/Assumed.ml b/src/Assumed.ml
index 38e539b4..2bf7cd7c 100644
--- a/src/Assumed.ml
+++ b/src/Assumed.ml
@@ -29,9 +29,10 @@
```
*)
+open Names
+open TypesUtils
module T = Types
module A = CfimAst
-open TypesUtils
module Sig = struct
(** A few utilities *)
@@ -227,7 +228,7 @@ module Sig = struct
let vec_index_mut_sig : A.fun_sig = vec_index_gen_sig true
end
-type assumed_info = A.assumed_fun_id * A.fun_sig * bool * Identifiers.name
+type assumed_info = A.assumed_fun_id * A.fun_sig * bool * name
(** The list of assumed functions and all their information:
- their signature
@@ -271,9 +272,9 @@ let get_assumed_sig (id : A.assumed_fun_id) : A.fun_sig =
let _, sg, _, _ = get_assumed_info id in
sg
-let get_assumed_name (id : A.assumed_fun_id) : Identifiers.fun_name =
+let get_assumed_name (id : A.assumed_fun_id) : fun_name =
let _, _, _, name = get_assumed_info id in
- Identifiers.Regular name
+ Regular name
let assumed_is_monadic (id : A.assumed_fun_id) : bool =
let _, _, b, _ = get_assumed_info id in
diff --git a/src/CfimAst.ml b/src/CfimAst.ml
index 279430df..f597cd27 100644
--- a/src/CfimAst.ml
+++ b/src/CfimAst.ml
@@ -1,4 +1,5 @@
open Identifiers
+open Names
open Types
open Values
open Expressions
diff --git a/src/CfimAstUtils.ml b/src/CfimAstUtils.ml
index c694d61b..57906143 100644
--- a/src/CfimAstUtils.ml
+++ b/src/CfimAstUtils.ml
@@ -26,7 +26,7 @@ let lookup_fun_sig (fun_id : fun_id) (fun_decls : fun_decl FunDeclId.Map.t) :
| Assumed aid -> Assumed.get_assumed_sig aid
let lookup_fun_name (fun_id : fun_id) (fun_decls : fun_decl FunDeclId.Map.t) :
- Identifiers.fun_name =
+ Names.fun_name =
match fun_id with
| Local id -> (FunDeclId.Map.find id fun_decls).name
| Assumed aid -> Assumed.get_assumed_name aid
diff --git a/src/CfimOfJson.ml b/src/CfimOfJson.ml
index e78b157a..d1108913 100644
--- a/src/CfimOfJson.ml
+++ b/src/CfimOfJson.ml
@@ -9,7 +9,7 @@
*)
open Yojson.Basic
-open Identifiers
+open Names
open OfJsonBasic
module T = Types
module V = Values
diff --git a/src/Identifiers.ml b/src/Identifiers.ml
index 31460dcd..eb2db3bd 100644
--- a/src/Identifiers.ml
+++ b/src/Identifiers.ml
@@ -171,41 +171,3 @@ module IdGen () : Id = struct
module Set = C.MakeSet (Ord)
module Map = C.MakeMap (Ord)
end
-
-type name = string list [@@deriving show, ord]
-(** A name such as: `std::collections::vector` (which would be represented as
- [["std"; "collections"; "vector"]]) *)
-
-(* TODO: remove? *)
-module NameOrderedType : C.OrderedType with type t = name = struct
- type t = name
-
- let compare = compare_name
-
- let to_string = String.concat "::"
-
- let pp_t = pp_name
-
- let show_t = show_name
-end
-
-module NameMap = C.MakeMap (NameOrderedType)
-module NameSet = C.MakeSet (NameOrderedType)
-
-type module_name = name [@@deriving show, ord]
-
-type type_name = name [@@deriving show, ord]
-
-module ImplId = IdGen ()
-
-(** A function name *)
-type fun_name =
- | Regular of name (** "Regular" function name *)
- | Impl of type_name * ImplId.id * string
- (** The function comes from an "impl" block.
-
- As we may have several "impl" blocks for one type, we need to use
- a block id to disambiguate the functions (in rustc, this identifier
- is called a "disambiguator").
- *)
-[@@deriving show, ord]
diff --git a/src/Names.ml b/src/Names.ml
new file mode 100644
index 00000000..fff98be9
--- /dev/null
+++ b/src/Names.ml
@@ -0,0 +1,39 @@
+open Identifiers
+
+type name = string list [@@deriving show, ord]
+(** A name such as: `std::collections::vector` (which would be represented as
+ [["std"; "collections"; "vector"]]) *)
+
+(* TODO: remove? *)
+module NameOrderedType : C.OrderedType with type t = name = struct
+ type t = name
+
+ let compare = compare_name
+
+ let to_string = String.concat "::"
+
+ let pp_t = pp_name
+
+ let show_t = show_name
+end
+
+module NameMap = C.MakeMap (NameOrderedType)
+module NameSet = C.MakeSet (NameOrderedType)
+
+type module_name = name [@@deriving show, ord]
+
+type type_name = name [@@deriving show, ord]
+
+module ImplId = IdGen ()
+
+(** A function name *)
+type fun_name =
+ | Regular of name (** "Regular" function name *)
+ | Impl of type_name * ImplId.id * string
+ (** The function comes from an "impl" block.
+
+ As we may have several "impl" blocks for one type, we need to use
+ a block id to disambiguate the functions (in rustc, this identifier
+ is called a "disambiguator").
+ *)
+[@@deriving show, ord]
diff --git a/src/Print.ml b/src/Print.ml
index 64351e3e..f8b8ff85 100644
--- a/src/Print.ml
+++ b/src/Print.ml
@@ -1,4 +1,4 @@
-open Identifiers
+open Names
module T = Types
module TU = TypesUtils
module V = Values
diff --git a/src/Pure.ml b/src/Pure.ml
index b1c8e254..bbbf72a6 100644
--- a/src/Pure.ml
+++ b/src/Pure.ml
@@ -1,4 +1,5 @@
open Identifiers
+open Names
module T = Types
module V = Values
module E = Expressions
diff --git a/src/PureToExtract.ml b/src/PureToExtract.ml
index 2c8a5a28..4db5d2c5 100644
--- a/src/PureToExtract.ml
+++ b/src/PureToExtract.ml
@@ -28,11 +28,11 @@ type region_group_info = {
module StringSet = Collections.MakeSet (Collections.OrderedString)
module StringMap = Collections.MakeMap (Collections.OrderedString)
-type name = Identifiers.name
+type name = Names.name
-type type_name = Identifiers.type_name
+type type_name = Names.type_name
-type fun_name = Identifiers.fun_name
+type fun_name = Names.fun_name
(* TODO: this should a module we give to a functor! *)
type formatter = {
@@ -526,7 +526,8 @@ let ctx_add_type_decl_struct (def : type_decl) (ctx : extraction_ctx) :
let ctx = ctx_add (StructId (AdtId def.def_id)) cons_name ctx in
(ctx, cons_name)
-let ctx_add_type_decl (def : type_decl) (ctx : extraction_ctx) : extraction_ctx =
+let ctx_add_type_decl (def : type_decl) (ctx : extraction_ctx) : extraction_ctx
+ =
let def_name = ctx.fmt.type_name def.name in
let ctx = ctx_add (TypeId (AdtId def.def_id)) def_name ctx in
ctx
@@ -549,8 +550,9 @@ let ctx_add_variant (def : type_decl) (variant_id : VariantId.id)
let ctx = ctx_add (VariantId (AdtId def.def_id, variant_id)) name ctx in
(ctx, name)
-let ctx_add_variants (def : type_decl) (variants : (VariantId.id * variant) list)
- (ctx : extraction_ctx) : extraction_ctx * string list =
+let ctx_add_variants (def : type_decl)
+ (variants : (VariantId.id * variant) list) (ctx : extraction_ctx) :
+ extraction_ctx * string list =
List.fold_left_map
(fun ctx (vid, v) -> ctx_add_variant def vid v ctx)
ctx variants
@@ -566,11 +568,13 @@ let ctx_add_decrases_clause (def : fun_decl) (ctx : extraction_ctx) :
let name = ctx.fmt.decreases_clause_name def.def_id def.basename in
ctx_add (DecreasesClauseId (A.Local def.def_id)) name ctx
-let ctx_add_fun_decl (trans_group : bool * pure_fun_translation) (def : fun_decl)
- (ctx : extraction_ctx) : extraction_ctx =
+let ctx_add_fun_decl (trans_group : bool * pure_fun_translation)
+ (def : fun_decl) (ctx : extraction_ctx) : extraction_ctx =
(* Lookup the CFIM def to compute the region group information *)
let def_id = def.def_id in
- let cfim_def = FunDeclId.Map.find def_id ctx.trans_ctx.fun_context.fun_decls in
+ let cfim_def =
+ FunDeclId.Map.find def_id ctx.trans_ctx.fun_context.fun_decls
+ in
let sg = cfim_def.signature in
let num_rgs = List.length sg.regions_hierarchy in
let keep_fwd, (_, backs) = trans_group in
diff --git a/src/Types.ml b/src/Types.ml
index 6393e0d8..013f511d 100644
--- a/src/Types.ml
+++ b/src/Types.ml
@@ -1,4 +1,5 @@
open Identifiers
+open Names
module TypeVarId = IdGen ()
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-24 16:54:17 +0000