summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorEscherichia2024-03-29 10:56:52 +0100
committerEscherichia2024-04-03 18:20:25 +0200
commita781ea75c1860c76c5577faa57efcdb0db910612 (patch)
tree3b2aa289972d5246469a45da9aa37605f68f831c
parentebf2ba2fda2a5f8e0a63f4cb6761291c9b501fab (diff)
Added meta information to names_map_id field in names_map type
-rw-r--r--compiler/ExtractBase.ml45
1 files changed, 23 insertions, 22 deletions
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index 74ac9e32..96f816cb 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -237,7 +237,7 @@ module IdSet = Collections.MakeSet (IdOrderedType)
*)
type names_map = {
id_to_name : string IdMap.t;
- name_to_id : id StringMap.t;
+ name_to_id : (id * Meta.meta option) 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...
@@ -253,8 +253,8 @@ let empty_names_map : names_map =
}
(** Small helper to report name collision *)
-let report_name_collision (id_to_string : id -> string) (id1 : id) (id2 : id)
- (name : string) : unit =
+let report_name_collision (id_to_string : id -> string)
+ (id1, meta : id * Meta.meta option) (id2 : id) (name : string) : unit =
let id1 = "\n- " ^ id_to_string id1 in
let id2 = "\n- " ^ id_to_string id2 in
let err =
@@ -263,9 +263,10 @@ let report_name_collision (id_to_string : id -> string) (id1 : id) (id2 : id)
^ "\nYou may want to rename some of your definitions, or report an issue."
in
(* If we fail hard on errors, raise an exception *)
- save_error __FILE__ __LINE__ None err
+ save_error __FILE__ __LINE__ meta err
-let names_map_get_id_from_name (name : string) (nm : names_map) : id option =
+let names_map_get_id_from_name (name : string) (nm : names_map) :
+ (id * Meta.meta option) option =
StringMap.find_opt name nm.name_to_id
let names_map_check_collision (id_to_string : id -> string) (id : id)
@@ -277,15 +278,15 @@ let names_map_check_collision (id_to_string : id -> string) (id : id)
report_name_collision id_to_string clash id name
(** Insert bindings in a names map without checking for collisions *)
-let names_map_add_unchecked (id : id) (name : string) (nm : names_map) :
+let names_map_add_unchecked (id, meta : id * Meta.meta option) (name : string) (nm : names_map) :
names_map =
(* 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 name_to_id= StringMap.add name (id, meta) 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_add (id_to_string : id -> string) (id : id) (name : string)
+let names_map_add (id_to_string : id -> string) (id, meta : id * meta option) (name : string)
(nm : names_map) : names_map =
(* Check if there is a clash *)
names_map_check_collision id_to_string id name nm;
@@ -296,9 +297,9 @@ let names_map_add (id_to_string : id -> string) (id : id) (name : string)
^ ":\nThe chosen name is already in the names set: " ^ name
in
(* If we fail hard on errors, raise an exception *)
- save_error __FILE__ __LINE__ None err);
+ save_error __FILE__ __LINE__ meta err);
(* Insert *)
- names_map_add_unchecked id name nm
+ names_map_add_unchecked (id, meta) name nm
(** The unsafe names map stores mappings from identifiers to names which might
collide. For some backends and some names, it might be acceptable to have
@@ -384,7 +385,7 @@ let allow_collisions (id : id) : bool =
(** The [id_to_string] function to print nice debugging messages if there are
collisions *)
-let names_maps_add (id_to_string : id -> string) (id : id) (name : string)
+let names_maps_add (meta : Meta.meta option) (id_to_string : id -> string) (id : id) (name : string)
(nm : names_maps) : names_maps =
(* We do not use the same name map if we allow/disallow collisions.
We notably use it for field names: some backends like Lean can use the
@@ -415,10 +416,10 @@ let names_maps_add (id_to_string : id -> string) (id : id) (name : string)
*)
let strict_names_map =
if strict_collisions id then
- names_map_add id_to_string id name nm.strict_names_map
+ names_map_add id_to_string (id, meta) name nm.strict_names_map
else nm.strict_names_map
in
- let names_map = names_map_add id_to_string id name nm.names_map in
+ let names_map = names_map_add id_to_string (id, meta) name nm.names_map in
{ nm with strict_names_map; names_map }
(** The [id_to_string] function to print nice debugging messages if there are
@@ -468,20 +469,20 @@ type names_map_init = {
let names_maps_add_assumed_type (id_to_string : id -> string) (id : assumed_ty)
(name : string) (nm : names_maps) : names_maps =
- names_maps_add id_to_string (TypeId (TAssumed id)) name nm
+ names_maps_add None id_to_string (TypeId (TAssumed id)) name nm
let names_maps_add_assumed_struct (id_to_string : id -> string)
(id : assumed_ty) (name : string) (nm : names_maps) : names_maps =
- names_maps_add id_to_string (StructId (TAssumed id)) name nm
+ names_maps_add None id_to_string (StructId (TAssumed id)) name nm
let names_maps_add_assumed_variant (id_to_string : id -> string)
(id : assumed_ty) (variant_id : VariantId.id) (name : string)
(nm : names_maps) : names_maps =
- names_maps_add id_to_string (VariantId (TAssumed id, variant_id)) name nm
+ names_maps_add None id_to_string (VariantId (TAssumed id, variant_id)) name nm
-let names_maps_add_function (id_to_string : id -> string) (fid : fun_id)
+let names_maps_add_function (id_to_string : id -> string) (fid, meta : fun_id * meta option)
(name : string) (nm : names_maps) : names_maps =
- names_maps_add id_to_string (FunId fid) name nm
+ names_maps_add meta id_to_string (FunId fid) name nm
let bool_name () = if !backend = Lean then "Bool" else "bool"
let char_name () = if !backend = Lean then "Char" else "char"
@@ -659,7 +660,7 @@ let id_to_string (meta : Meta.meta option) (id : id) (ctx : extraction_ctx) :
let ctx_add (meta : Meta.meta) (id : id) (name : string) (ctx : extraction_ctx)
: extraction_ctx =
let id_to_string (id : id) : string = id_to_string (Some meta) id ctx in
- let names_maps = names_maps_add id_to_string id name ctx.names_maps in
+ let names_maps = names_maps_add (Some meta) id_to_string id name ctx.names_maps in
{ ctx with names_maps }
let ctx_get (meta : Meta.meta option) (id : id) (ctx : extraction_ctx) : string
@@ -1125,7 +1126,7 @@ let initialize_names_maps () : names_maps =
(* There is duplication in the keywords so we don't check the collisions
while registering them (what is important is that there are no collisions
between keywords and user-defined identifiers) *)
- names_map_add_unchecked UnknownId name nm)
+ names_map_add_unchecked (UnknownId, None) name nm)
strict_names_map keywords
in
let nm = { names_map; unsafe_names_map; strict_names_map } in
@@ -1155,9 +1156,9 @@ let initialize_names_maps () : names_maps =
in
let assumed_functions =
List.map
- (fun (fid, name) -> (FromLlbc (Pure.FunId (FAssumed fid), None), name))
+ (fun (fid, name) -> ((FromLlbc (Pure.FunId (FAssumed fid), None), None), name))
init.assumed_llbc_functions
- @ List.map (fun (fid, name) -> (Pure fid, name)) init.assumed_pure_functions
+ @ List.map (fun (fid, name) -> ((Pure fid, None), name)) init.assumed_pure_functions
in
let nm =
List.fold_left