diff --git a/src/kernel_services/abstract_interp/abstract_interp.ml b/src/kernel_services/abstract_interp/abstract_interp.ml
index 80233cd3f3e65cb96fa2ec27a445615e30693a88..54f0b9b6f4ace4cc798ff1c91d06ab4dbcba9a32 100644
--- a/src/kernel_services/abstract_interp/abstract_interp.ml
+++ b/src/kernel_services/abstract_interp/abstract_interp.ml
@@ -246,7 +246,6 @@ module Make_Hashconsed_Lattice_Set
module O = Set
include Make_Generic_Lattice_Set (V) (Set)
- let () = Type.set_ml_name ty None
let intersects e1 e2 = match e1, e2 with
| _, Top | Top, _ -> true
diff --git a/src/kernel_services/abstract_interp/lmap.ml b/src/kernel_services/abstract_interp/lmap.ml
index 0f5c56a0959d97126f77f8d1a270c038a755aa21..2d563e9283949c51563d925b48e5d653d08446c5 100644
--- a/src/kernel_services/abstract_interp/lmap.ml
+++ b/src/kernel_services/abstract_interp/lmap.ml
@@ -595,7 +595,6 @@ struct
let copy = Datatype.undefined
let mem_project = Datatype.never_any_project
end)
- let () = Type.set_ml_name ty None
let top = Top
let bottom = Bottom
diff --git a/src/kernel_services/analysis/service_graph.ml b/src/kernel_services/analysis/service_graph.ml
index b383f6284702dce3bfee44a92719d3c0176f7993..6bc18ce04fa24137d293a077d60570fe105dcfef 100644
--- a/src/kernel_services/analysis/service_graph.ml
+++ b/src/kernel_services/analysis/service_graph.ml
@@ -93,7 +93,6 @@ struct
let reprs = [ M.create () ]
let mem_project = Datatype.never_any_project
end)
- let () = Type.set_ml_name Datatype.ty None
let add_labeled_edge g src l dst =
if mem_edge g src dst then begin
remove_edge g src dst;
diff --git a/src/kernel_services/ast_queries/cil_datatype.ml b/src/kernel_services/ast_queries/cil_datatype.ml
index 30cbd6c15099a9ee5debb9f76ad41b2356a58c37..86a73f05bbf5a5b007c1956b1479610fc768ea74 100644
--- a/src/kernel_services/ast_queries/cil_datatype.ml
+++ b/src/kernel_services/ast_queries/cil_datatype.ml
@@ -2456,7 +2456,6 @@ module Kf = struct
let pretty fmt kf = Varinfo.pretty fmt (vi kf)
let mem_project = Datatype.never_any_project
end)
- let () = Type.set_ml_name ty (Some "Kernel_function.ty")
end
diff --git a/src/libraries/datatype/datatype.ml b/src/libraries/datatype/datatype.ml
index 8dae3ee8845863d16cf056b3afe010dc63f141d0..608c29405556b58b5cf223a792c00aca7838e3d1 100644
--- a/src/libraries/datatype/datatype.ml
+++ b/src/libraries/datatype/datatype.ml
@@ -228,8 +228,7 @@ module Make(X: Make_input) = struct
module T = struct
include X
let name = if is_module_name X.name then X.name ^ ".t" else X.name
- let ml_name = if is_module_name X.name then Some (X.name ^ ".ty") else None
- let ty = Type.register ~name ~ml_name X.structural_descr X.reprs
+ let ty = Type.register ~name X.structural_descr X.reprs
end
include T
@@ -326,27 +325,6 @@ module Polymorphic2(P: Polymorphic2_input) = struct
include Type.Polymorphic2(P)
- (* cannot declare [name] locally in instantiate since it prevents OCaml
- generalization *)
- let name = !poly_name_ref
- let instantiate ty1 ty2 =
- let res, first = instantiate ty1 ty2 in
- if first && name <> "" then begin
- let ml_name =
- Format.asprintf
- "Datatype.%s %a %a"
- name
- (fun fmt ty -> Type.pp_ml_name ty Type.Call fmt)
- ty1
- (fun fmt ty -> Type.pp_ml_name ty Type.Call fmt)
- ty2
- in
- Type.set_ml_name res (Some ml_name)
- end;
- res, first
-
- let () = poly_name_ref := ""
-
module Make(T1: S)(T2: S) = struct
module T = struct
@@ -438,29 +416,6 @@ struct
include Type.Polymorphic3(P)
- (* cannot declare [name] locally in instantiate since it prevents OCaml
- generalization *)
- let name = !poly_name_ref
- let instantiate ty1 ty2 ty3 =
- let res, first = instantiate ty1 ty2 ty3 in
- if first && name <> "" then begin
- let ml_name =
- Format.asprintf
- "Datatype.%s %a %a %a"
- name
- (fun fmt ty -> Type.pp_ml_name ty Type.Call fmt)
- ty1
- (fun fmt ty -> Type.pp_ml_name ty Type.Call fmt)
- ty2
- (fun fmt ty -> Type.pp_ml_name ty Type.Call fmt)
- ty3
- in
- Type.set_ml_name res (Some ml_name)
- end;
- res, first
-
- let () = poly_name_ref := ""
-
module Make(T1: S)(T2: S)(T3: S) = struct
module T = struct
@@ -566,31 +521,6 @@ struct
include Type.Polymorphic4(P)
- (* cannot declare [name] locally in instantiate since it prevents OCaml
- generalization *)
- let name = !poly_name_ref
- let instantiate ty1 ty2 ty3 ty4 =
- let res, first = instantiate ty1 ty2 ty3 ty4 in
- if first && name <> "" then begin
- let ml_name =
- Format.asprintf
- "Datatype.%s %a %a %a %a"
- name
- (fun fmt ty -> Type.pp_ml_name ty Type.Call fmt)
- ty1
- (fun fmt ty -> Type.pp_ml_name ty Type.Call fmt)
- ty2
- (fun fmt ty -> Type.pp_ml_name ty Type.Call fmt)
- ty3
- (fun fmt ty -> Type.pp_ml_name ty Type.Call fmt)
- ty4
- in
- Type.set_ml_name res (Some ml_name)
- end;
- res, first
-
- let () = poly_name_ref := ""
-
module Make(T1: S)(T2: S)(T3: S)(T4: S) = struct
module T = struct
@@ -796,25 +726,6 @@ module Polymorphic_gen(P: Polymorphic_input) = struct
include Type.Polymorphic(P)
- (* cannot declare [name] locally in instantiate since it prevents OCaml
- generalization *)
- let name = !poly_name_ref
- let instantiate ty =
- let res, first = instantiate ty in
- if first && name <> "" then begin
- let ml_name =
- Format.asprintf
- "Datatype.%s %a"
- name
- (fun fmt ty -> Type.pp_ml_name ty Type.Call fmt)
- ty
- in
- Type.set_ml_name res (Some ml_name)
- end;
- res, first
-
- let () = poly_name_ref := ""
-
module Make_gen(X: S)(R: sig val rehash: X.t poly -> X.t poly end) = struct
module T = struct
@@ -1246,8 +1157,6 @@ struct
let nearest_elt_le x = S.find_last (fun y -> y <= x)
let nearest_elt_ge x = S.find_first (fun y -> y >= x)
- let () = Type.set_ml_name P.ty (Some (Info.module_name ^ ".ty"))
-
let ty = P.ty
let name = P.name
let descr = P.descr
@@ -1455,7 +1364,6 @@ module Weak(W: Sub_caml_weak_hashtbl)(D: S with type t = W.data) = struct
let name = "Weak(" ^ D.name ^ ")"
let reprs = let w = W.create 0 in Caml_list.iter (W.add w) D.reprs; [ w ]
end)
- let () = Type.set_ml_name ty None;
end
module Caml_weak_hashtbl(D: S) = struct
@@ -1575,8 +1483,6 @@ struct
end))
(struct let module_name = module_name end)
- let () = Type.set_ml_name ty (Some ("Datatype." ^ name))
-
end
module Unit =
diff --git a/src/libraries/datatype/type.ml b/src/libraries/datatype/type.ml
index 53c0534319946f58271420789f3f48d59972f97d..e3deb416ab0b988a8b1bc8703243820318c6588d 100644
--- a/src/libraries/datatype/type.ml
+++ b/src/libraries/datatype/type.ml
@@ -60,8 +60,7 @@ let par p_caller p_callee fmt pp =
type concrete_repr =
{ mutable name: string;
digest: Digest.t;
- structural_descr: Structural_descr.t;
- mutable pp_ml_name: precedence -> Format.formatter -> unit }
+ structural_descr: Structural_descr.t }
(* phantom type *)
type 'a t = concrete_repr
@@ -94,32 +93,8 @@ let embedded_types: concrete_repr Tbl.t = Tbl.create 7
(** {2 Main functions} *)
(* ****************************************************************************)
-let mk_dyn_pp name = function
- | None ->
- let pp fmt =
- let plugin_name = match Str.split (Str.regexp_string ".") name with
- | [] -> None
- | p :: _ -> Some p
- in
- match plugin_name with
- | None ->
- Format.fprintf fmt "(failwith \"%s is not a printable type name\")" name
- | Some p ->
- Format.fprintf fmt "%s.ty" p
- in
- (fun p fmt -> par p Basic fmt pp)
- | Some s ->
- let prec =
- try
- ignore (Str.search_forward (Str.regexp " ") name 0);
- Call
- with Not_found ->
- Basic
- in
- fun p fmt -> par p prec fmt (fun fmt -> Format.fprintf fmt "%s" s)
-
exception AlreadyExists of string
-let register ?(closure=false) ~name ~ml_name structural_descr reprs =
+let register ?(closure=false) ~name structural_descr reprs =
let error () =
invalid_arg ("Type.register: invalid reprs for type " ^ name)
in
@@ -132,7 +107,6 @@ let register ?(closure=false) ~name ~ml_name structural_descr reprs =
error ()
| _ ->
if Hashtbl.mem types name then raise (AlreadyExists name);
- let pp_ml_name = mk_dyn_pp name ml_name in
let digest = match structural_descr with
| Structural_descr.Unknown ->
(* unserializable type: weakest digest *)
@@ -144,8 +118,7 @@ let register ?(closure=false) ~name ~ml_name structural_descr reprs =
let ty =
{ name = name;
digest = digest;
- structural_descr = structural_descr;
- pp_ml_name = pp_ml_name }
+ structural_descr = structural_descr }
in
let full_ty = { ty = ty; reprs = List.map Obj.repr reprs } in
Hashtbl.add types name full_ty;
@@ -174,18 +147,12 @@ end
let name ty = ty.name
let structural_descr ty = ty.structural_descr
let digest ty = ty.digest
-let pp_ml_name ty = ty.pp_ml_name
-let ml_name ty = Format.asprintf "%t" (ty.pp_ml_name Basic)
let unsafe_reprs ty = (Hashtbl.find types ty.name).reprs
let reprs ty =
let l = try unsafe_reprs ty with Not_found -> assert false in
List.map Obj.obj l
-let set_ml_name ty ml_name =
- let pp = mk_dyn_pp ty.name ml_name in
- ty.pp_ml_name <- pp
-
let set_name ty name =
let full_ty = try Hashtbl.find types ty.name with Not_found -> assert false in
Hashtbl.remove types ty.name;
@@ -236,11 +203,6 @@ module Polymorphic(T: Polymorphic_input) = struct
type 'a poly = 'a T.t
- let ml_name from_ty =
- Format.asprintf "%s.instantiate %t"
- T.module_name
- (from_ty.pp_ml_name Call)
-
let instantiate (ty:'a t) =
try
Tbl.find ty, false
@@ -248,7 +210,6 @@ module Polymorphic(T: Polymorphic_input) = struct
let repr =
register
~name:(T.name ty)
- ~ml_name:(Some (ml_name ty))
(T.structural_descr ty.structural_descr)
(List.fold_left
(fun acc ty -> T.reprs ty @ acc) [] (unsafe_reprs ty))
@@ -298,13 +259,6 @@ module Polymorphic2(T: Polymorphic2_input) = struct
let memo_tbl : concrete_repr Concrete_pair.t = Concrete_pair.create 17
let instances : (concrete_repr * concrete_repr) Tbl.t = Tbl.create 17
- let ml_name from_ty1 from_ty2 =
- Format.asprintf
- "%s.instantiate %t %t"
- T.module_name
- (from_ty1.pp_ml_name Call)
- (from_ty2.pp_ml_name Call)
-
let instantiate a b =
let key = a, b in
try
@@ -323,7 +277,6 @@ module Polymorphic2(T: Polymorphic2_input) = struct
let ty =
register
~name:(T.name a b)
- ~ml_name:(Some (ml_name a b))
(T.structural_descr a.structural_descr b.structural_descr)
reprs
in
@@ -396,12 +349,6 @@ module Function = struct
(match label with None -> "" | Some l -> "~" ^ l ^ ":")
^ par_ty_name is_instance_of ty1 ^ " -> " ^ name ty2
- let ml_name label ty1 ty2 =
- Format.asprintf
- "Datatype.func%s %t %t"
- (match label with None -> "" | Some l -> " ~label:(" ^ l ^ ", None)")
- (ty1.pp_ml_name Call) (ty2.pp_ml_name Call)
-
let instantiate ?label (a:'a) (b:'b t): ('a, 'b) poly t * bool =
let l, o = match label with
| None -> None, None
@@ -420,7 +367,6 @@ module Function = struct
register
~closure:true
~name:(name l a b)
- ~ml_name:(Some (ml_name l a b))
Structural_descr.t_unknown
(List.map (fun r _ -> r) (unsafe_reprs b))
in
@@ -471,14 +417,6 @@ module Polymorphic3(T:Polymorphic3_input) = struct
: (concrete_repr * concrete_repr * concrete_repr) Tbl.t
= Tbl.create 17
- let ml_name from_ty1 from_ty2 from_ty3 =
- Format.asprintf
- "%s.instantiate %t %t %t"
- T.module_name
- (from_ty1.pp_ml_name Call)
- (from_ty2.pp_ml_name Call)
- (from_ty3.pp_ml_name Call)
-
let instantiate a b c =
let key = a, b, c in
try
@@ -501,7 +439,6 @@ module Polymorphic3(T:Polymorphic3_input) = struct
let ty =
register
~name:(T.name a b c)
- ~ml_name:(Some (ml_name a b c))
(T.structural_descr
a.structural_descr
b.structural_descr
@@ -569,15 +506,6 @@ module Polymorphic4(T:Polymorphic4_input) = struct
: (concrete_repr * concrete_repr * concrete_repr * concrete_repr) Tbl.t
= Tbl.create 17
- let ml_name from_ty1 from_ty2 from_ty3 from_ty4 =
- Format.asprintf
- "%s.instantiate %t %t %t %t"
- T.module_name
- (from_ty1.pp_ml_name Call)
- (from_ty2.pp_ml_name Call)
- (from_ty3.pp_ml_name Call)
- (from_ty4.pp_ml_name Call)
-
let instantiate a b c d =
let key = a, b, c, d in
try
@@ -604,7 +532,6 @@ module Polymorphic4(T:Polymorphic4_input) = struct
let ty =
register
~name:(T.name a b c d)
- ~ml_name:(Some (ml_name a b c d))
(T.structural_descr
a.structural_descr
b.structural_descr
diff --git a/src/libraries/datatype/type.mli b/src/libraries/datatype/type.mli
index cc2bd56a2cf27c09c04c1dc2256c602a4871ddd3..022ea2caf3769ef8716d5851d67d1f20b15315c6 100644
--- a/src/libraries/datatype/type.mli
+++ b/src/libraries/datatype/type.mli
@@ -87,7 +87,6 @@ exception AlreadyExists of string
val register:
?closure:bool ->
name:string ->
- ml_name:string option ->
Structural_descr.t ->
'a list ->
'a t
@@ -97,7 +96,6 @@ val register:
[closure] is true iff the type is a function type.
[name] is the name of the type. Must be a valid OCaml type name (eventually
prefixed by a module path).
- [ml_name] is the OCaml name of the registered type value.
@raise AlreadyExists if the given name is already used by another type.
@raise Invalid_argument if [reprs] is the empty list
*)
@@ -129,9 +127,6 @@ val get_embedded_type_names: 'a t -> string list
list"; "int" ].
@since Oxygen-20120901 *)
-val ml_name: 'a t -> string
-val pp_ml_name: 'a t -> precedence -> Format.formatter -> unit
-val set_ml_name: 'a t -> string option -> unit
val set_name: 'a t -> string -> unit
(** @since Neon-20140301 *)
diff --git a/src/libraries/utils/hptmap.ml b/src/libraries/utils/hptmap.ml
index 15a34cae3f11f18749e5ac1888fac60544bc10d7..2c8f4f4e14176d7657739a7edc41bb7e161bccaa 100644
--- a/src/libraries/utils/hptmap.ml
+++ b/src/libraries/utils/hptmap.ml
@@ -693,7 +693,6 @@ struct
let pretty = pretty
let mem_project = Datatype.never_any_project
end)
- let () = Type.set_ml_name D.ty None
include (D: Datatype.S_with_collections with type t := t)
module PatriciaHashconsTbl =
diff --git a/src/libraries/utils/rangemap.ml b/src/libraries/utils/rangemap.ml
index d59ee5c547bb5bcc7fcdf7356b342a92f22340b7..e18a9c532bcbf8068022f80384510382384fa7e9 100644
--- a/src/libraries/utils/rangemap.ml
+++ b/src/libraries/utils/rangemap.ml
@@ -541,7 +541,6 @@ module Make(Ord: Datatype.S)(Value: Value) = struct
else
(fun s -> exists (fun k v -> Ord.mem_project s k || Value.mem_project s v))
end)
- let () = Type.set_ml_name ty None
end
diff --git a/src/plugins/pdg/pdg_types/pdgTypes.ml b/src/plugins/pdg/pdg_types/pdgTypes.ml
index 34d941009fe2e49de79382480db80f8ac499a37c..f2acde6c9e7a469151803f752b4db5d69e4a7c57 100644
--- a/src/plugins/pdg/pdg_types/pdgTypes.ml
+++ b/src/plugins/pdg/pdg_types/pdgTypes.ml
@@ -481,7 +481,6 @@ module Pdg = struct
let name = "body"
let mem_project = Datatype.never_any_project
end)
- let () = Type.set_ml_name Body_datatype.ty None
include Datatype.Pair(Kernel_function)(Body_datatype)
diff --git a/src/plugins/wp/wpo.ml b/src/plugins/wp/wpo.ml
index f6675856d79f30fd95304d5dbc6eca807abbd189..8de7b05c26f07be8568e451a150425ae24d47921 100644
--- a/src/plugins/wp/wpo.ml
+++ b/src/plugins/wp/wpo.ml
@@ -398,8 +398,6 @@ module S =
po_formula = VC_Annot.repr ;
}]
end)
-(* to get a "reasonable" API doc: *)
-let () = Type.set_ml_name S.ty (Some "Wpo.po")
module WpoType = S
module ProverType =
@@ -410,8 +408,6 @@ module ProverType =
let name = "Wpo.prover"
let reprs = [ Qed ]
end)
-(* to get a "reasonable" API doc: *)
-let () = Type.set_ml_name ProverType.ty (Some "Wpo.prover")
module ResultType =
Datatype.Make
@@ -423,8 +419,6 @@ module ResultType =
List.map VCS.result
[ Valid ; Unknown ; Timeout ; Failed ]
end)
-(* to get a "reasonable" API doc *)
-let () = Type.set_ml_name ResultType.ty (Some "Wpo.result")
(* -------------------------------------------------------------------------- *)
(* --- Getters --- *)
diff --git a/tests/dynamic/abstract.ml b/tests/dynamic/abstract.ml
index f0a45ba0e7f428d6185895bdae134eb6078034f6..4492141344b458c19f7ceb7579169abf7b00d875 100644
--- a/tests/dynamic/abstract.ml
+++ b/tests/dynamic/abstract.ml
@@ -82,7 +82,7 @@ module B = struct
module T = Type.Abstract(struct let name = "A.t" end)
let ty = T.ty
let _ =
- Type.register ~ml_name:None ~name:"B.t" Structural_descr.t_unknown [ 0.0 ]
+ Type.register ~name:"B.t" Structural_descr.t_unknown [ 0.0 ]
module U = Type.Abstract(struct let name = "A.u" end)
let ty' = U.ty
let fut = Datatype.func Datatype.unit ty'
diff --git a/tests/dynamic/abstract2.ml b/tests/dynamic/abstract2.ml
index f3f0f72b3e4a76c0c8dd1369a12c864672381771..78b34089af4c5f0d551980f3453cfc4f2e8805c4 100644
--- a/tests/dynamic/abstract2.ml
+++ b/tests/dynamic/abstract2.ml
@@ -2,7 +2,7 @@
module AA : sig end = struct
type _t = string
let ty =
- Type.register ~name:"AA.t" ~ml_name:None Structural_descr.t_unknown [ "" ]
+ Type.register ~name:"AA.t" Structural_descr.t_unknown [ "" ]
let _mk =
Dynamic.register ~plugin:"AA" "mk"
(Datatype.func Datatype.unit ty)
@@ -12,7 +12,7 @@ end
module BB : sig end = struct
type _t = float
let ty =
- Type.register ~name:"BB.t" ~ml_name:None Structural_descr.t_unknown [ 1.0 ]
+ Type.register ~name:"BB.t" Structural_descr.t_unknown [ 1.0 ]
let _print =
Dynamic.register ~plugin:"BB" "print"
(Datatype.func ty Datatype.unit)