summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/PureToExtract.ml138
1 files changed, 116 insertions, 22 deletions
diff --git a/src/PureToExtract.ml b/src/PureToExtract.ml
index 6a1bcc2a..b563ba15 100644
--- a/src/PureToExtract.ml
+++ b/src/PureToExtract.ml
@@ -211,11 +211,27 @@ type names_map = {
}
(** The names map stores the mappings from names to identifiers and vice-versa.
- We use it for lookups (during the translation) and to check for name clashes.
+ We use it for lookups (during the translation) and to check for name clashes.
+
+ [id_to_string] is for debugging.
*)
-let names_map_add (id : id) (name : string) (nm : names_map) : names_map =
- (* Sanity check: no clashes *)
+let names_map_add (id_to_string : id -> string) (id : id) (name : string)
+ (nm : names_map) : names_map =
+ (* Check if there is a clash *)
+ (match StringMap.find_opt name nm.name_to_id with
+ | None -> () (* Ok *)
+ | Some clash ->
+ (* There is a clash: print a nice debugging message for the user *)
+ let id1 = "\n- " ^ id_to_string clash in
+ let id2 = "\n- " ^ id_to_string id in
+ let err =
+ "Name clash detected: the following identifiers are bound to the same \
+ name \"" ^ name ^ "\":" ^ id1 ^ id2
+ in
+ log#serror err;
+ failwith err);
+ (* Sanity check *)
assert (not (StringSet.mem name nm.names_set));
(* Insert *)
let id_to_name = IdMap.add id name nm.id_to_name in
@@ -223,22 +239,23 @@ let names_map_add (id : id) (name : string) (nm : names_map) : names_map =
let names_set = StringSet.add name nm.names_set in
{ id_to_name; name_to_id; names_set }
-let names_map_add_assumed_type (id : assumed_ty) (name : string)
- (nm : names_map) : names_map =
- names_map_add (TypeId (Assumed id)) name nm
-
-let names_map_add_assumed_struct (id : assumed_ty) (name : string)
- (nm : names_map) : names_map =
- names_map_add (StructId (Assumed id)) name nm
+let names_map_add_assumed_type (id_to_string : id -> string) (id : assumed_ty)
+ (name : string) (nm : names_map) : names_map =
+ names_map_add id_to_string (TypeId (Assumed id)) name nm
-let names_map_add_assumed_variant (id : assumed_ty) (variant_id : VariantId.id)
+let names_map_add_assumed_struct (id_to_string : id -> string) (id : assumed_ty)
(name : string) (nm : names_map) : names_map =
- names_map_add (VariantId (Assumed id, variant_id)) name nm
+ names_map_add id_to_string (StructId (Assumed id)) name nm
+
+let names_map_add_assumed_variant (id_to_string : id -> string)
+ (id : assumed_ty) (variant_id : VariantId.id) (name : string)
+ (nm : names_map) : names_map =
+ names_map_add id_to_string (VariantId (Assumed id, variant_id)) name nm
-let names_map_add_assumed_function (fid : A.assumed_fun_id)
- (rg_id : RegionGroupId.id option) (name : string) (nm : names_map) :
- names_map =
- names_map_add (FunId (A.Assumed fid, rg_id)) name nm
+let names_map_add_assumed_function (id_to_string : id -> string)
+ (fid : A.assumed_fun_id) (rg_id : RegionGroupId.id option) (name : string)
+ (nm : names_map) : names_map =
+ names_map_add id_to_string (FunId (A.Assumed fid, rg_id)) name nm
(** Make a (variable) basename unique (by adding an index).
@@ -271,8 +288,79 @@ type extraction_ctx = {
*)
let ctx_add (id : id) (name : string) (ctx : extraction_ctx) : extraction_ctx =
- (* TODO : nice debugging message if collision *)
- let names_map = names_map_add id name ctx.names_map in
+ (* The id_to_string function to print nice debugging messages if there are
+ * collisions *)
+ let id_to_string (id : id) : string =
+ let fun_defs = ctx.trans_ctx.fun_context.fun_defs in
+ let type_defs = ctx.trans_ctx.type_context.type_defs in
+ (* TODO: factorize the pretty-printing with what is in PrintPure *)
+ let get_type_name (id : type_id) : string =
+ match id with
+ | AdtId id ->
+ let def = TypeDefId.Map.find id type_defs in
+ Print.name_to_string def.name
+ | Assumed aty -> show_assumed_ty aty
+ | Tuple -> failwith "Unreachable"
+ in
+ match id with
+ | FunId (fid, rg_id) ->
+ let fun_name =
+ match fid with
+ | A.Local fid ->
+ Print.name_to_string (FunDefId.Map.find fid fun_defs).name
+ | A.Assumed aid -> A.show_assumed_fun_id aid
+ in
+ let fun_kind =
+ match rg_id with
+ | None -> "forward"
+ | Some rg_id -> "backward " ^ RegionGroupId.to_string rg_id
+ in
+ "fun name (" ^ fun_kind ^ "): " ^ fun_name
+ | TypeId id -> "type name: " ^ get_type_name id
+ | StructId id -> "struct constructor of: " ^ get_type_name id
+ | VariantId (id, variant_id) ->
+ let variant_name =
+ match id with
+ | Tuple -> failwith "Unreachable"
+ | Assumed Result ->
+ if variant_id = result_return_id then "@result::Return"
+ else if variant_id = result_fail_id then "@result::Fail"
+ else failwith "Unreachable"
+ | AdtId id -> (
+ let def = TypeDefId.Map.find id type_defs in
+ match def.kind with
+ | Struct _ -> failwith "Unreachable"
+ | Enum variants ->
+ let variant = VariantId.nth variants variant_id in
+ Print.name_to_string def.name ^ "::" ^ variant.variant_name)
+ in
+ "variant name: " ^ variant_name
+ | FieldId (id, field_id) ->
+ let field_name =
+ match id with
+ | Tuple -> failwith "Unreachable"
+ | Assumed Result -> failwith "Unreachable"
+ | AdtId id -> (
+ let def = TypeDefId.Map.find id type_defs in
+ match def.kind with
+ | Enum _ -> failwith "Unreachable"
+ | Struct fields ->
+ let field = FieldId.nth fields field_id in
+ let field_name =
+ match field.field_name with
+ | None -> FieldId.to_string field_id
+ | Some name -> name
+ in
+ Print.name_to_string def.name ^ "." ^ field_name)
+ in
+ "field name: " ^ field_name
+ | UnknownId -> "keyword"
+ | TypeVarId _ | VarId _ ->
+ (* We should never get there: we add indices to make sure variable
+ * names are unique *)
+ failwith "Unreachable"
+ in
+ let names_map = names_map_add id_to_string id name ctx.names_map in
{ ctx with names_map }
let ctx_get (id : id) (ctx : extraction_ctx) : string =
@@ -435,6 +523,10 @@ let initialize_names_map (init : names_map_init) : names_map =
* to check collisions. *)
let id_to_name = IdMap.empty in
let nm = { id_to_name; name_to_id; names_set } in
+ (* For debugging - we are creating bindings for assumed types and functions, so
+ * it is ok if we simply use the "show" function (those aren't simply identified
+ * by numbers) *)
+ let id_to_string = show_id in
(* Then we add:
* - the assumed types
* - the assumed struct constructors
@@ -443,24 +535,26 @@ let initialize_names_map (init : names_map_init) : names_map =
*)
let nm =
List.fold_left
- (fun nm (type_id, name) -> names_map_add_assumed_type type_id name nm)
+ (fun nm (type_id, name) ->
+ names_map_add_assumed_type id_to_string type_id name nm)
nm init.assumed_adts
in
let nm =
List.fold_left
- (fun nm (type_id, name) -> names_map_add_assumed_struct type_id name nm)
+ (fun nm (type_id, name) ->
+ names_map_add_assumed_struct id_to_string type_id name nm)
nm init.assumed_structs
in
let nm =
List.fold_left
(fun nm (type_id, variant_id, name) ->
- names_map_add_assumed_variant type_id variant_id name nm)
+ names_map_add_assumed_variant id_to_string type_id variant_id name nm)
nm init.assumed_variants
in
let nm =
List.fold_left
(fun nm (fun_id, rg_id, name) ->
- names_map_add_assumed_function fun_id rg_id name nm)
+ names_map_add_assumed_function id_to_string fun_id rg_id name nm)
nm init.assumed_functions
in
(* Return *)