diff --git a/src/kernel_internals/typing/rmtmps.ml b/src/kernel_internals/typing/rmtmps.ml
index 3b3eaadd34889a78bfab20890733789dd0e0e407..160f27ea9dc56848e41658d3ba06084c20865827 100644
--- a/src/kernel_internals/typing/rmtmps.ml
+++ b/src/kernel_internals/typing/rmtmps.ml
@@ -861,7 +861,7 @@ let removeUnmarked isRoot ast reachable_tbl =
begin
try
let kf = Globals.Functions.get vi in
- Kernel.debug ~dkey "GFunDecl: %a@." Kernel_function.pretty_code kf
+ Kernel.debug ~dkey "GFunDecl: %a@." Kernel_function.pretty kf
with Not_found ->
Kernel.debug ~dkey
"GFunDecl: %a (no associated kernel function)@."
diff --git a/src/kernel_services/abstract_interp/abstract_interp.ml b/src/kernel_services/abstract_interp/abstract_interp.ml
index 31de26b07b835d03c23d07fc916ecd04baf279a0..0569d8fe257e55f6c88fe4d94ddaba55feeaca44 100644
--- a/src/kernel_services/abstract_interp/abstract_interp.ml
+++ b/src/kernel_services/abstract_interp/abstract_interp.ml
@@ -222,7 +222,6 @@ module Make_Generic_Lattice_Set
let hash = hash
let rehash = Datatype.identity
let copy = Datatype.undefined
- let internal_pretty_code = Datatype.undefined
let pretty = pretty
let varname = Datatype.undefined
let mem_project = Datatype.never_any_project
@@ -364,7 +363,6 @@ module Make_Lattice_Base (V:Lattice_Value):(Lattice_Base with type l = V.t) = st
let hash = hash
let rehash = Datatype.identity
let copy = Datatype.undefined
- let internal_pretty_code = Datatype.undefined
let pretty = pretty
let varname = Datatype.undefined
let mem_project = Datatype.never_any_project
@@ -517,8 +515,7 @@ module Bool = struct
let rehash = Datatype.identity
let copy = Datatype.identity
let pretty = pretty
- let internal_pretty_code = Datatype.undefined
- let varname = Datatype.undefined
+ let varname = Datatype.undefined
let mem_project = Datatype.never_any_project
end) :
Datatype.S with type t := t)
@@ -677,8 +674,7 @@ struct
let hash = hash
let rehash = Datatype.identity
let copy = Datatype.undefined
- let internal_pretty_code = Datatype.undefined
- let pretty = pretty
+ let pretty = pretty
let varname = Datatype.undefined
let mem_project = Datatype.never_any_project
end) :
@@ -777,7 +773,6 @@ struct
let hash = hash
let rehash = Datatype.identity
let copy = Datatype.undefined
- let internal_pretty_code = Datatype.undefined
let pretty = pretty
let varname = Datatype.undefined
let mem_project = Datatype.never_any_project
@@ -947,7 +942,6 @@ struct
let hash = hash
let rehash = Datatype.undefined
let copy = Datatype.undefined
- let internal_pretty_code = Datatype.undefined
let pretty = pretty
let varname = Datatype.undefined
let mem_project = Datatype.never_any_project
diff --git a/src/kernel_services/abstract_interp/base.ml b/src/kernel_services/abstract_interp/base.ml
index 2ebe0f3efa129c9d60576ec84dd1b4d5d105eb40..4734eef370604d213ef841ba76e96ba3a4994843 100644
--- a/src/kernel_services/abstract_interp/base.ml
+++ b/src/kernel_services/abstract_interp/base.ml
@@ -99,7 +99,6 @@ module Validity = Datatype.Make
let pretty = pretty_validity
let mem_project = Datatype.never_any_project
- let internal_pretty_code = Datatype.pp_fail
let rehash = Datatype.identity
let copy (x:t) = x
let varname _ = "v"
@@ -450,7 +449,6 @@ module Base = struct
let pretty = pretty
let hash = hash
let mem_project = Datatype.never_any_project
- let internal_pretty_code = Datatype.pp_fail
let rehash = Datatype.identity
let copy = Datatype.undefined
let varname = Datatype.undefined
diff --git a/src/kernel_services/abstract_interp/int_Base.ml b/src/kernel_services/abstract_interp/int_Base.ml
index 2aab074ee278371a381fbfc68e825606eef557bc..f75a06568c36414d32a66364e708112c3caf33a7 100644
--- a/src/kernel_services/abstract_interp/int_Base.ml
+++ b/src/kernel_services/abstract_interp/int_Base.ml
@@ -55,7 +55,6 @@ include Datatype.Make
let hash = hash
let rehash = Datatype.identity
let copy = Extlib.id
- let internal_pretty_code = Datatype.undefined
let pretty = pretty
let varname = Datatype.undefined
let mem_project = Datatype.never_any_project
diff --git a/src/kernel_services/abstract_interp/int_interval.ml b/src/kernel_services/abstract_interp/int_interval.ml
index f1eb54dada1209a83225a2b0b5017fb34e7be71b..4900196abcd0e8828504e03535e43c56706dc600 100644
--- a/src/kernel_services/abstract_interp/int_interval.ml
+++ b/src/kernel_services/abstract_interp/int_interval.ml
@@ -94,7 +94,6 @@ include Datatype.Make_with_collections
let hash = hash
let pretty = pretty
let rehash = Datatype.identity
- let internal_pretty_code = Datatype.pp_fail
let mem_project = Datatype.never_any_project
let copy = Datatype.undefined
let varname = Datatype.undefined
diff --git a/src/kernel_services/abstract_interp/int_set.ml b/src/kernel_services/abstract_interp/int_set.ml
index 1d5a7fad690e76287ed21e296371fcd9b25df308..e1fe0de05909a39dee7f02dc70400cae957fa131 100644
--- a/src/kernel_services/abstract_interp/int_set.ml
+++ b/src/kernel_services/abstract_interp/int_set.ml
@@ -130,7 +130,6 @@ include Datatype.Make_with_collections
let hash = hash
let pretty = pretty
let rehash x = x
- let internal_pretty_code = Datatype.pp_fail
let mem_project = Datatype.never_any_project
let copy = Datatype.undefined
let varname = Datatype.undefined
diff --git a/src/kernel_services/abstract_interp/int_val.ml b/src/kernel_services/abstract_interp/int_val.ml
index 8fb7cf1b226f052663ef9f58979897e86792d1da..424ba043ea0e9dad37f038eba0104cf0d3742c8b 100644
--- a/src/kernel_services/abstract_interp/int_val.ml
+++ b/src/kernel_services/abstract_interp/int_val.ml
@@ -75,7 +75,6 @@ include Datatype.Make_with_collections
let hash = hash
let pretty = pretty
let rehash x = x
- let internal_pretty_code = Datatype.pp_fail
let mem_project = Datatype.never_any_project
let copy = Datatype.undefined
let varname = Datatype.undefined
diff --git a/src/kernel_services/abstract_interp/ival.ml b/src/kernel_services/abstract_interp/ival.ml
index 2384610cb9f8af4512699f51a1cbc2421bf6f758..233c6f19fc22e47eee46b6fe9aa80b35af9a682a 100644
--- a/src/kernel_services/abstract_interp/ival.ml
+++ b/src/kernel_services/abstract_interp/ival.ml
@@ -824,7 +824,6 @@ include (
let hash = hash
let pretty = pretty
let rehash = rehash
- let internal_pretty_code = Datatype.pp_fail
let mem_project = Datatype.never_any_project
let copy = Datatype.undefined
let varname = Datatype.undefined
diff --git a/src/kernel_services/abstract_interp/lmap.ml b/src/kernel_services/abstract_interp/lmap.ml
index afe85f50c5b901176bd733b5884258627c85ea3e..483210b38356b616ed5fdcd9d54d873c75edcd97 100644
--- a/src/kernel_services/abstract_interp/lmap.ml
+++ b/src/kernel_services/abstract_interp/lmap.ml
@@ -591,7 +591,6 @@ struct
let compare = compare
let hash = hash
let pretty = pretty
- let internal_pretty_code = Datatype.undefined
let rehash = Datatype.identity
let copy = Datatype.undefined
let varname = Datatype.undefined
diff --git a/src/kernel_services/abstract_interp/lmap_bitwise.ml b/src/kernel_services/abstract_interp/lmap_bitwise.ml
index ee6e25cad0d1d230c328933d10ed64192b07ae5e..72515172d0ec47b7300de80ba4825aab8e7fc521 100644
--- a/src/kernel_services/abstract_interp/lmap_bitwise.ml
+++ b/src/kernel_services/abstract_interp/lmap_bitwise.ml
@@ -238,7 +238,6 @@ struct
let equal = equal
let compare = compare
let pretty = pretty
- let internal_pretty_code = Datatype.undefined
let rehash = Datatype.identity
let copy = Datatype.undefined
let varname = Datatype.undefined
diff --git a/src/kernel_services/abstract_interp/map_lattice.ml b/src/kernel_services/abstract_interp/map_lattice.ml
index 28d864d5708fe0c885895909eb9cd45193c83429..0d0d31d9e90fe234611f8378f0d1b77bb50640d8 100644
--- a/src/kernel_services/abstract_interp/map_lattice.ml
+++ b/src/kernel_services/abstract_interp/map_lattice.ml
@@ -498,7 +498,6 @@ module Make_MapSet_Lattice
let hash = hash
let rehash = Datatype.identity
let copy = Datatype.undefined
- let internal_pretty_code = Datatype.pp_fail
let pretty = pretty
let mem_project = Datatype.never_any_project
let varname = Datatype.undefined
diff --git a/src/kernel_services/abstract_interp/offsetmap.ml b/src/kernel_services/abstract_interp/offsetmap.ml
index 98a53b5f61d76d9e3d6b63eb55c9e7a11188c812..0bc43658600ab137d32f6681a8031bea49dee8be 100644
--- a/src/kernel_services/abstract_interp/offsetmap.ml
+++ b/src/kernel_services/abstract_interp/offsetmap.ml
@@ -229,7 +229,6 @@ module Make (V : module type of Offsetmap_lattice_with_isotropy) = struct
let compare = compare
let rehash x = !rehash_ref x
let copy = Datatype.undefined
- let internal_pretty_code = Datatype.undefined
let pretty = pretty
let varname = Datatype.undefined
let mem_project = Datatype.never_any_project
@@ -2461,7 +2460,6 @@ module Int_Intervals = struct
let mem_project = Datatype.never_any_project
let varname _ = "i"
- let internal_pretty_code = Datatype.undefined
let copy = Datatype.undefined
end)
diff --git a/src/kernel_services/abstract_interp/origin.ml b/src/kernel_services/abstract_interp/origin.ml
index c31e62808d56c7b8072205110d01fd31041f417f..c6cdb0fd21cf0f3aae1c36136d824b9fd4b3c2dc 100644
--- a/src/kernel_services/abstract_interp/origin.ml
+++ b/src/kernel_services/abstract_interp/origin.ml
@@ -135,7 +135,6 @@ include Datatype.Make
let hash = hash
let rehash = Datatype.undefined
let copy = Datatype.undefined
- let internal_pretty_code = Datatype.undefined
let pretty = pretty
let varname = Datatype.undefined
let mem_project = Datatype.never_any_project
diff --git a/src/kernel_services/ast_data/alarms.ml b/src/kernel_services/ast_data/alarms.ml
index ce0c8902d6ff10d013c553f57e394948600fe0bd..3ccb9304cb3ac6e9e2608c82530878deba39d769 100644
--- a/src/kernel_services/ast_data/alarms.ml
+++ b/src/kernel_services/ast_data/alarms.ml
@@ -308,7 +308,6 @@ module D =
| Invalid_bool lv ->
Format.fprintf fmt "Invalid_bool(@[%a@])" Lval.pretty lv
- let internal_pretty_code = Datatype.undefined
let copy = Datatype.undefined
let mem_project = Datatype.never_any_project
end)
diff --git a/src/kernel_services/ast_data/globals.ml b/src/kernel_services/ast_data/globals.ml
index cc79e169f7a5eec485c4d144ac0dad50bbf343c3..06f17de617ad1c311b46ac76127c933f0f423cd4 100644
--- a/src/kernel_services/ast_data/globals.ml
+++ b/src/kernel_services/ast_data/globals.ml
@@ -91,17 +91,6 @@ module Vars = struct
let get_astinfo vi = !get_astinfo_ref vi
- let pp_varinfo p fmt v =
- let name, loc = get_astinfo v in
- let pp fmt =
- Format.fprintf fmt "@[<hv 2>Globals.Vars.find_from_astinfo@;%S@;%a@]"
- name
- (Cil_datatype.Localisation.internal_pretty_code Type.Call) loc
- in
- Type.par p Type.Call fmt pp
-
- let () = Varinfo.internal_pretty_code_ref := pp_varinfo
-
let iter_globals f l =
let treat_global = function
| GVar(vi,init,_) -> f vi init
diff --git a/src/kernel_services/ast_data/property_status.ml b/src/kernel_services/ast_data/property_status.ml
index 552171036e72d27253e46c4999b8122a5dd54f35..ba440a42ed53764e29cbef756fd3fed480d6cbe2 100644
--- a/src/kernel_services/ast_data/property_status.ml
+++ b/src/kernel_services/ast_data/property_status.ml
@@ -80,9 +80,7 @@ module Emitter_with_properties =
let copy = Datatype.undefined
let pretty fmt e = Usable_emitter.pretty fmt e.emitter
- let internal_pretty_code = Datatype.undefined
- let varname _ = assert false (* unused while [internal_pretty_code]
- unimplemented *)
+ let varname _ = assert false
let mem_project = Datatype.never_any_project
end)
diff --git a/src/kernel_services/ast_queries/ast_diff.ml b/src/kernel_services/ast_queries/ast_diff.ml
index c7551b0733be41b396abf71790e09045a5c16ef7..96a1eb0a076324d4cc1aab1eaaa1ef039b7df6da 100644
--- a/src/kernel_services/ast_queries/ast_diff.ml
+++ b/src/kernel_services/ast_queries/ast_diff.ml
@@ -59,11 +59,6 @@ struct
let map f = function
| `Same x -> `Same (f x)
| `Not_present -> `Not_present
- let mk_internal_pretty_code pp prec fmt = function
- | `Not_present -> Format.pp_print_string fmt "`Not_present"
- | `Same x ->
- let pp fmt = Format.fprintf fmt "`Same %a" (pp Type.Call) x in
- Type.par prec Call fmt pp
let mk_pretty pp fmt = function
| `Not_present -> Format.pp_print_string fmt "N/A"
| `Same x -> Format.fprintf fmt " => %a" pp x
@@ -111,12 +106,6 @@ let compare_pc pc1 pc2 =
| _, `Callees_changed -> 1
| `Callees_spec_changed, `Callees_spec_changed -> 0
-let string_of_pc = function
- | `Spec_changed -> "Spec_changed"
- | `Body_changed -> "Body_changed"
- | `Callees_changed -> "Callees_changed"
- | `Callees_spec_changed -> "Callees_spec_changed"
-
let pretty_pc fmt =
let open Format in
function
@@ -163,16 +152,6 @@ struct
| `Partial(x,pc) -> `Partial(f x,pc)
| (#correspondance as x) -> Correspondance_input.map f x
- let mk_internal_pretty_code pp prec fmt = function
- | `Partial (x,flags) ->
- let pp fmt =
- Format.fprintf fmt "`Partial (%a,%s)"
- (pp Type.Call) x (string_of_pc flags)
- in
- Type.par prec Call fmt pp
- | #correspondance as x ->
- Correspondance_input.mk_internal_pretty_code pp prec fmt x
-
let mk_pretty pp fmt = function
| `Partial(x,flags) ->
Format.fprintf fmt "-> %a %a" pp x pretty_pc flags
diff --git a/src/kernel_services/ast_queries/cil_builtins.ml b/src/kernel_services/ast_queries/cil_builtins.ml
index 4d0545f91f3f05c0e4251f395a25a5748f373bbe..8d224fd39bfe2b10a8ebd9de8b1b5185bc06b440 100644
--- a/src/kernel_services/ast_queries/cil_builtins.ml
+++ b/src/kernel_services/ast_queries/cil_builtins.ml
@@ -160,7 +160,6 @@ module Builtin_template = struct
let hash b = Datatype.String.hash b.name
let equal b1 b2 = b1.name = b2.name
let copy = Datatype.identity
- let internal_pretty_code = Datatype.undefined
let pretty fmt b =
Format.fprintf fmt "%s %s(%a%s)"
b.rettype b.name
diff --git a/src/kernel_services/ast_queries/cil_datatype.ml b/src/kernel_services/ast_queries/cil_datatype.ml
index 31b139bdd6bd451ebf2f4fedcb10d11c8cb89481..3e9dfcb0c49d6a360967825c6dcff5f712e16064 100644
--- a/src/kernel_services/ast_queries/cil_datatype.ml
+++ b/src/kernel_services/ast_queries/cil_datatype.ml
@@ -48,7 +48,6 @@ module Make
type t
val name: string
val reprs: t list
- val internal_pretty_code: Type.precedence -> Format.formatter -> t -> unit
val pretty: Format.formatter -> t -> unit
val varname: t -> string
end) =
@@ -69,7 +68,6 @@ module Make_with_collections
val reprs: t list
val compare: t -> t -> int
val equal: t -> t -> bool
- val internal_pretty_code: Type.precedence -> Format.formatter -> t -> unit
val pretty: Format.formatter -> t -> unit
val varname: t -> string
val hash: t -> int
@@ -161,7 +159,6 @@ module Cabs_file = struct
let reprs = [ Datatype.Filepath.dummy, [];
Datatype.Filepath.dummy, [ true, Cabs.GLOBANNOT [] ] ]
let varname (s, _) = "cabs_" ^ (Filepath.Normalized.to_pretty_string s)
- let internal_pretty_code = Datatype.undefined
let pretty fmt cabs = !pretty_ref fmt cabs
end)
end
@@ -199,7 +196,6 @@ module Position = struct
let hash = Hashtbl.hash
let copy = Datatype.identity
let equal: t -> t -> bool = ( = )
- let internal_pretty_code = Datatype.undefined
let pretty = Filepath.pp_pos
let varname _ = "pos"
end)
@@ -224,7 +220,6 @@ module Location = struct
let hash (b, _e) = Hashtbl.hash (b.Filepath.pos_path, b.Filepath.pos_lnum)
let copy = Datatype.identity (* immutable strings *)
let equal : t -> t -> bool = ( = )
- let internal_pretty_code = Datatype.undefined
let pretty fmt loc = !pretty_ref fmt loc
let varname _ = "loc"
end)
@@ -274,7 +269,6 @@ module Instr = struct
type t = instr
let name = "Instr"
let reprs = List.map (fun l -> Skip l) Location.reprs
- let internal_pretty_code = Datatype.undefined
let pretty fmt x = !pretty_ref fmt x
let varname = Datatype.undefined
end)
@@ -321,13 +315,6 @@ module Stmt_Id = struct
let hash t1 = t1.sid
let equal t1 t2 = t1.sid = t2.sid
let copy = Datatype.undefined
- let internal_pretty_code p_caller fmt s =
- let pp fmt =
- Format.fprintf fmt
- "@[<hv 2>fst@;@[<hv 2>(Kernel_function.find_from_sid@;%d)@]@]"
- s.sid
- in
- Type.par p_caller Type.Call fmt pp
let pretty fmt s = !pretty_ref fmt s
let varname _ = "stmt"
end)
@@ -378,15 +365,6 @@ module Kinstr = struct
| Kglobal -> 1 lsl 29
| Kstmt s -> s.sid
let copy = Datatype.undefined
- let internal_pretty_code p fmt = function
- | Kglobal ->
- Format.fprintf fmt "Kglobal"
- | Kstmt s ->
- let pp fmt =
- Format.fprintf fmt "@[<hv 2>Kstmt@;%a@]"
- (Stmt.internal_pretty_code Type.Call) s
- in
- Type.par p Type.Call fmt pp
let pretty fmt = function
| Kglobal ->
Format.fprintf fmt "Kglobal"
@@ -617,7 +595,6 @@ module Attribute=struct
let hash = hash_attribute config
let equal = Datatype.from_compare
let copy = Datatype.undefined
- let internal_pretty_code = Datatype.undefined
let pretty fmt t = !pretty_ref fmt t
let varname = Datatype.undefined
end)
@@ -642,7 +619,6 @@ struct
let hash = hash_type M.config
let equal = Datatype.from_compare
let copy = Datatype.undefined
- let internal_pretty_code = Datatype.undefined
let pretty fmt t = !pretty_typ_ref fmt t
let varname = Datatype.undefined
end)
@@ -736,7 +712,6 @@ module Label = struct
let name = "Label"
let reprs =
[ Label("", Location.unknown, false); Default Location.unknown ]
- let internal_pretty_code = Datatype.undefined
let pretty fmt l = !pretty_ref fmt l
let varname = Datatype.undefined
let hash = function
@@ -767,7 +742,6 @@ end
module Varinfo_Id = struct
let pretty_ref = ref (fun _ _ -> assert false)
- let internal_pretty_code_ref = ref (fun _ _ _ -> assert false)
let dummy =
{ vname = "";
vorig_name = "";
@@ -798,7 +772,6 @@ module Varinfo_Id = struct
let hash v = v.vid
let equal v1 v2 = v1.vid = v2.vid
let copy = Datatype.undefined
- let internal_pretty_code p fmt v = !internal_pretty_code_ref p fmt v
let pretty fmt v = !pretty_ref fmt v
let varname v = "vi_" ^ v.vorig_name
end)
@@ -835,7 +808,6 @@ module Compinfo = struct
let hash v = Hashtbl.hash v.ckey
let equal v1 v2 = v1.ckey = v2.ckey
let copy = Datatype.undefined
- let internal_pretty_code = Datatype.undefined
let pretty fmt f = !pretty_ref fmt f
let varname = Datatype.undefined
end)
@@ -878,7 +850,6 @@ module Fieldinfo = struct
let hash f1 = Hashtbl.hash (fid f1)
let equal f1 f2 = (fid f1) = (fid f2)
let copy = Datatype.undefined
- let internal_pretty_code = Datatype.undefined
let pretty fmt f = !pretty_ref fmt f
let varname = Datatype.undefined
end)
@@ -1155,7 +1126,6 @@ module Block = struct
let reprs =
[{battrs=[]; blocals=Varinfo.reprs; bstatics = [];
bstmts=Stmt.reprs; bscoping=true}]
- let internal_pretty_code = Datatype.undefined
let pretty fmt b = !pretty_ref fmt b
let varname = Datatype.undefined
end)
@@ -1224,7 +1194,6 @@ module Lval = struct
let equal = equal_lval
let hash = hash_lval
let copy = Datatype.undefined
- let internal_pretty_code = Datatype.undefined
let pretty fmt x = !pretty_ref fmt x
let varname _ = "lv"
end)
@@ -1240,7 +1209,6 @@ module LvalStructEq_input = struct
let equal = Datatype.from_compare
let hash = StructEq.hash_lval 13598
let copy = Datatype.undefined
- let internal_pretty_code = Datatype.undefined
let pretty fmt x = !Lval.pretty_ref fmt x
let varname _ = "lv"
end
@@ -1260,7 +1228,6 @@ module Offset = struct
let equal = equal_offset
let hash = hash_offset
let copy = Datatype.undefined
- let internal_pretty_code = Datatype.undefined
let pretty fmt x = !pretty_ref fmt x
let varname _ = "offs"
end)
@@ -1276,7 +1243,6 @@ module OffsetStructEq_input = struct
let equal = Datatype.from_compare
let hash = StructEq.hash_offset 75489
let copy = Datatype.undefined
- let internal_pretty_code = Datatype.undefined
let pretty fmt x = !Offset.pretty_ref fmt x
let varname _ = "offs"
end
@@ -1311,7 +1277,6 @@ module Logic_var = struct
let hash v = v.lv_id
let equal v1 v2 = v1.lv_id = v2.lv_id
let copy = Datatype.undefined
- let internal_pretty_code = Datatype.undefined
let pretty fmt t = !pretty_ref fmt t
let varname _ = "logic_var"
end)
@@ -1333,7 +1298,6 @@ module Builtin_logic_info = struct
let hash i = Hashtbl.hash i.bl_name
let equal i1 i2 = i1.bl_name = i2.bl_name
let copy = Datatype.identity (* works only if an AST is never modified *)
- let internal_pretty_code = Datatype.undefined
let pretty fmt li = !pretty_ref fmt li
let varname = Datatype.undefined
end)
@@ -1351,7 +1315,6 @@ module Logic_type_info = struct
let equal t1 t2 = t1.lt_name = t2.lt_name
let hash t = Hashtbl.hash t.lt_name
let copy = Datatype.identity (* works only if an AST is never modified *)
- let internal_pretty_code = Datatype.undefined
let pretty fmt lt = !pretty_ref fmt lt
let varname = Datatype.undefined
end)
@@ -1371,7 +1334,6 @@ module Logic_ctor_info = struct
let equal t1 t2 = t1.ctor_name = t2.ctor_name
let hash t = Hashtbl.hash t.ctor_name
let copy = Datatype.identity (* works only if an AST is never modified *)
- let internal_pretty_code = Datatype.undefined
let pretty fmt c = !pretty_ref fmt c
let varname = Datatype.undefined
end)
@@ -1386,7 +1348,6 @@ module Initinfo = struct
let reprs =
{ init = None } ::
List.map (fun t -> { init = Some (CompoundInit(t, [])) }) Typ.reprs
- let internal_pretty_code = Datatype.undefined
let pretty fmt i = !pretty_ref fmt i
let varname = Datatype.undefined
end)
@@ -1412,7 +1373,6 @@ module Logic_info = struct
let equal i1 i2 = Logic_var.equal i1.l_var_info i2.l_var_info
let hash i = Logic_var.hash i.l_var_info
let copy = Datatype.undefined
- let internal_pretty_code = Datatype.undefined
let pretty fmt li = !pretty_ref fmt li
let varname _ = "logic_varinfo"
end)
@@ -1497,7 +1457,6 @@ module Logic_info_structural = struct
let equal = Datatype.from_compare
let hash i = Logic_var.hash i.l_var_info
let copy = Datatype.undefined
- let internal_pretty_code = Datatype.undefined
let pretty fmt li = !Logic_info.pretty_ref fmt li
let varname _ = "logic_varinfo"
end)
@@ -2084,7 +2043,6 @@ module Logic_constant = struct
let equal = Datatype.from_compare
let hash = hash_logic_constant
let copy = Datatype.undefined
- let internal_pretty_code = Datatype.undefined
let pretty fmt lc = !pretty_ref fmt lc
let varname _ = "lconst"
end)
@@ -2108,7 +2066,6 @@ module Term = struct
let equal = Datatype.from_compare
let copy = Datatype.undefined
let hash = hash_fct hash_term
- let internal_pretty_code = Datatype.undefined
let pretty fmt t = !pretty_ref fmt t
let varname _ = "term"
end)
@@ -2128,7 +2085,6 @@ module Identified_term = struct
(* NB: Term.copy itself is undefined. *)
{ it_id = x.it_id; it_content = Term.copy x.it_content }
let hash x = x.it_id
- let internal_pretty_code = Datatype.undefined
let pretty fmt t = !pretty_ref fmt t
let varname _ = "id_term"
end)
@@ -2153,7 +2109,6 @@ module Term_lhost = struct
let equal = Datatype.from_compare
let hash = hash_fct hash_tlhost
let copy = Datatype.undefined
- let internal_pretty_code = Datatype.undefined
let pretty fmt h = !pretty_ref fmt h
let varname = Datatype.undefined
end)
@@ -2170,7 +2125,6 @@ module Term_offset = struct
let equal = Datatype.from_compare
let hash = hash_fct hash_toffset
let copy = Datatype.undefined
- let internal_pretty_code = Datatype.undefined
let pretty fmt t_o = !pretty_ref fmt t_o
let varname = Datatype.undefined
end)
@@ -2198,7 +2152,6 @@ module Logic_label = struct
let equal = Datatype.from_compare
let copy = Datatype.undefined
let hash = hash_label
- let internal_pretty_code = Datatype.undefined
let pretty fmt l = !pretty_ref fmt l
let varname _ = "logic_label"
end)
@@ -2219,7 +2172,6 @@ module Logic_real = struct
11 * Datatype.String.hash r.r_literal
let equal r1 r2 = compare r1 r2 = 0
let copy = Datatype.undefined
- let internal_pretty_code = Datatype.undefined
let pretty fmt t = !pretty_ref fmt t
let varname _ = "logic_real"
end)
@@ -2232,7 +2184,6 @@ module Global_annotation = struct
type t = global_annotation
let name = "Global_annotation"
let reprs = List.map (fun l -> Daxiomatic ("", [],[], l)) Location.reprs
- let internal_pretty_code = Datatype.undefined
let pretty fmt v = !pretty_ref fmt v
let varname = Datatype.undefined
@@ -2323,7 +2274,6 @@ module Global = struct
type t = global
let name = "Global"
let reprs = [ GText "" ]
- let internal_pretty_code = Datatype.undefined
let pretty fmt v = !pretty_ref fmt v
let varname = Datatype.undefined
@@ -2479,11 +2429,6 @@ module Kf = struct
!set_formal_decls v args;
x
let get_name_kf kf = (vi kf).Cil_types.vname
- let internal_pretty_code p_caller fmt kf =
- Type.par p_caller Type.Call fmt
- (fun fmt ->
- Format.fprintf fmt "@[<hv 2>Globals.Functions.find_by_name@;%S@]"
- (get_name_kf kf))
let pretty fmt kf = Varinfo.pretty fmt (vi kf)
let mem_project = Datatype.never_any_project
let varname kf = "kf_" ^ (get_name_kf kf)
@@ -2506,7 +2451,6 @@ module Code_annotation = struct
let equal x y = x.annot_id = y.annot_id
let compare x y = Datatype.Int.compare x.annot_id y.annot_id
let copy = Datatype.undefined
- let internal_pretty_code = Datatype.undefined
let pretty fmt ca = !pretty_ref fmt ca
let varname _ = "code_annot"
end)
@@ -2530,7 +2474,6 @@ module Predicate = struct
[ { pred_name = [ "" ];
pred_loc = Location.unknown;
pred_content = Pfalse } ]
- let internal_pretty_code = Datatype.undefined
let pretty fmt x = !pretty_ref fmt x
let varname _ = "p"
end)
@@ -2544,7 +2487,6 @@ module Toplevel_predicate = struct
let name = "Toplevel_predicate"
let reprs =
[ { tp_statement = List.hd Predicate.reprs; tp_kind = Assert }]
- let internal_pretty_code = Datatype.undefined
let pretty fmt x = !pretty_ref fmt x
let varname _ = "p"
end)
@@ -2562,7 +2504,6 @@ module Identified_predicate = struct
let equal x y = x.ip_id = y.ip_id
let copy = Datatype.undefined
let hash x = x.ip_id
- let internal_pretty_code = Datatype.undefined
let pretty fmt x = !pretty_ref fmt x
let varname _ = "id_predyes"
end)
@@ -2582,7 +2523,6 @@ module PredicateStructEq = struct
let equal = Datatype.from_compare
let copy = Datatype.undefined
let hash = hash_fct hash_predicate
- let internal_pretty_code = Datatype.undefined
let pretty fmt x = !pretty_ref fmt x
let varname _ = "p"
end)
@@ -2659,7 +2599,6 @@ module Fundec = struct
let rehash = Datatype.identity
let copy = Datatype.undefined
let pretty fmt f = !pretty_ref fmt f
- let internal_pretty_code = Datatype.undefined
let mem_project = Datatype.never_any_project
end)
end
@@ -2676,7 +2615,6 @@ module Lexpr = Make
type t = lexpr
let name = "Lexpr"
let reprs = [ { lexpr_node = PLvar ""; lexpr_loc = Location.unknown } ]
- let internal_pretty_code = Datatype.undefined
let pretty = Datatype.undefined (* TODO *)
let varname = Datatype.undefined
end)
@@ -2692,19 +2630,6 @@ module Localisation =
type t = localisation
let name = "Localisation"
let reprs = [ VGlobal ]
- let internal_pretty_code p_caller fmt loc =
- let pp s kf =
- Type.par p_caller Type.Call fmt
- (fun fmt ->
- Format.fprintf fmt "@[<hv 2>%s@;%a@]"
- s
- (Kf.internal_pretty_code Type.Call)
- kf)
- in
- match loc with
- | VGlobal -> Format.fprintf fmt "Cil_types.VGlobal"
- | VLocal kf -> pp "Cil_types.VLocal" kf
- | VFormal kf -> pp "Cil_types.VFormal" kf
let mem_project = Datatype.never_any_project
end)
diff --git a/src/kernel_services/ast_queries/cil_datatype.mli b/src/kernel_services/ast_queries/cil_datatype.mli
index 807648fbb378e86a9e0df39f6810bc800242db47..24b5ade1d02c6bc13cc4e58d6adf54b10db44c99 100644
--- a/src/kernel_services/ast_queries/cil_datatype.mli
+++ b/src/kernel_services/ast_queries/cil_datatype.mli
@@ -269,8 +269,6 @@ module Varinfo: sig
end
val dummy: t
(**/**)
- val internal_pretty_code_ref:
- (Type.precedence -> Format.formatter -> t -> unit) ref
end
module Kf: sig
diff --git a/src/kernel_services/ast_queries/file.ml b/src/kernel_services/ast_queries/file.ml
index 42bd47dd87081990a51d1cf9f77de7a0828f62eb..b3fa4fca000d301cbed097f3017df518d490e658 100644
--- a/src/kernel_services/ast_queries/file.ml
+++ b/src/kernel_services/ast_queries/file.ml
@@ -27,12 +27,6 @@ open Cil_datatype
type cpp_opt_kind = Gnu | Not_gnu | Unknown
-let pretty_cpp_opt_kind fmt =
- function
- | Gnu -> Format.pp_print_string fmt "Gnu"
- | Not_gnu -> Format.pp_print_string fmt "Not_gnu"
- | Unknown -> Format.pp_print_string fmt "Unknown"
-
type file =
| NeedCPP of
Filepath.Normalized.t (* Filename of the [.c] to preprocess. *)
@@ -62,22 +56,6 @@ module D =
let structural_descr = Structural_descr.t_abstract
let mem_project = Datatype.never_any_project
let copy = Datatype.identity (* immutable strings *)
- let internal_pretty_code p_caller fmt t =
- let pp fmt = match t with
- | NoCPP s ->
- Format.fprintf fmt "@[File.NoCPP %a@]" Filepath.Normalized.pretty s
- | External (f,p) ->
- Format.fprintf fmt "@[File.External (%a,%S)@]"
- Filepath.Normalized.pretty f p
- | NeedCPP (f,cmd,extra,kind) ->
- Format.fprintf
- fmt "@[File.NeedCPP (%a,%S,%S,%a)@]"
- Filepath.Normalized.pretty f
- cmd
- (String.concat " " extra)
- pretty_cpp_opt_kind kind
- in
- Type.par p_caller Type.Call fmt pp
end)
include D
diff --git a/src/kernel_services/cmdline_parameters/typed_parameter.ml b/src/kernel_services/cmdline_parameters/typed_parameter.ml
index b875e86a8eb7dc94a283f42cbcce934da6730568..8a9e8f585ace764499020dc00dd1b4cacc7a9989 100644
--- a/src/kernel_services/cmdline_parameters/typed_parameter.ml
+++ b/src/kernel_services/cmdline_parameters/typed_parameter.ml
@@ -67,9 +67,7 @@ include
let hash x = Datatype.String.hash x.name
let copy x = x (* The representation of the parameter is immutable *)
let pretty fmt x = Format.pp_print_string fmt x.name
- let internal_pretty_code = Datatype.undefined
let varname _ = assert false
- (* unused if internal_pretty_code undefined *)
let mem_project = Datatype.never_any_project
end)
diff --git a/src/kernel_services/plugin_entry_points/emitter.ml b/src/kernel_services/plugin_entry_points/emitter.ml
index 43d4b82ef8d8a26eec2b40b0bc2bb48636354b04..fd379811e4179e1a7888fe5bcd48d4428ee8d8a5 100644
--- a/src/kernel_services/plugin_entry_points/emitter.ml
+++ b/src/kernel_services/plugin_entry_points/emitter.ml
@@ -103,9 +103,7 @@ module D =
let hash x = Datatype.String.hash x.name
let copy x = x (* strings are immutable here *)
let pretty fmt x = Format.pp_print_string fmt x.name
- let internal_pretty_code = Datatype.undefined
- let varname _ = assert false (* unused while [internal_pretty_code]
- unimplemented *)
+ let varname _ = assert false
let mem_project = Datatype.never_any_project
end)
@@ -149,9 +147,7 @@ module Usable_emitter = struct
Format.fprintf fmt "%s (v%d)" name x.version
else
Format.pp_print_string fmt name
- let internal_pretty_code = Datatype.undefined
- let varname _ = assert false (* unused while [internal_pretty_code]
- unimplemented *)
+ let varname _ = assert false
let mem_project = Datatype.never_any_project
end)
diff --git a/src/libraries/datatype/datatype.ml b/src/libraries/datatype/datatype.ml
index 0db6b38c6c5659189e009ccf723ca23329f88d65..9ae247627dfe4ff5c72df5e9944242d883eb78e4 100644
--- a/src/libraries/datatype/datatype.ml
+++ b/src/libraries/datatype/datatype.ml
@@ -29,8 +29,6 @@ type 'a t =
compare: 'a -> 'a -> int;
hash: 'a -> int;
copy: 'a -> 'a;
- internal_pretty_code: Type.precedence -> Format.formatter -> 'a -> unit;
- pretty_code: Format.formatter -> 'a -> unit;
pretty: Format.formatter -> 'a -> unit;
varname: 'a -> string;
mem_project: (Project_skeleton.t -> bool) -> 'a -> bool }
@@ -51,8 +49,6 @@ module type S_no_copy = sig
val equal: t -> t -> bool
val compare: t -> t -> int
val hash: t -> int
- val pretty_code: Format.formatter -> t -> unit
- val internal_pretty_code: Type.precedence -> Format.formatter -> t -> unit
val pretty: Format.formatter -> t -> unit
val varname: t -> string
val mem_project: (Project_skeleton.t -> bool) -> t -> bool
@@ -82,9 +78,6 @@ let equal ty = (internal_info "equal" ty).equal
let compare ty = (internal_info "compare" ty).compare
let hash ty = (internal_info "hash" ty).hash
let copy ty = (internal_info "copy" ty).copy
-let internal_pretty_code ty =
- (internal_info "internal_pretty_code" ty).internal_pretty_code
-let pretty_code ty = (internal_info "pretty_code" ty).pretty_code
let pretty ty = (internal_info "pretty" ty).pretty
let varname ty = (internal_info "varname" ty).varname
let mem_project ty = (internal_info "mem_project" ty).mem_project
@@ -99,8 +92,6 @@ let undefined _ = assert false
let identity x = x
let never_any_project _ _ = false
let from_compare _ _ = assert false
-let from_pretty_code _ _ = assert false
-let pp_fail _ _ _ = assert false
module type Undefined = sig
val structural_descr: Structural_descr.t
@@ -109,7 +100,6 @@ module type Undefined = sig
val hash: 'a -> int
val rehash: 'a -> 'a
val copy: 'a -> 'a
- val internal_pretty_code: Type.precedence -> Format.formatter -> 'a -> unit
val pretty: Format.formatter -> 'a -> unit
val varname: 'a -> string
val mem_project: (Project_skeleton.t -> bool) -> 'a -> bool
@@ -120,7 +110,6 @@ module Partial_undefined = struct
let compare = undefined
let hash = undefined
let copy = undefined
- let internal_pretty_code = undefined
let pretty = undefined
let varname = undefined
let mem_project = undefined
@@ -168,7 +157,6 @@ module Build
val hash: t -> int
val rehash: t -> t
val copy: t -> t
- val internal_pretty_code: Type.precedence -> Format.formatter -> t -> unit
val pretty: Format.formatter -> t -> unit
val varname: t -> string
val mem_project: (Project_skeleton.t -> bool) -> t -> bool
@@ -186,24 +174,8 @@ struct
let hash = T.hash
let rehash = T.rehash
let copy = T.copy
- let internal_pretty_code = T.internal_pretty_code
-
- let pretty_code =
- if T.internal_pretty_code == undefined then undefined
- else if T.internal_pretty_code == pp_fail then pp_fail Type.NoPar
- else fun fmt x ->
- (* Format.printf "pretty code %s@." name;*)
- let buf = Buffer.create 17 in
- let buffmt = Format.formatter_of_buffer buf in
- Format.fprintf buffmt "%a@?" (T.internal_pretty_code Type.NoPar) x;
- let f =
- Scanf.format_from_string (String.escaped (Buffer.contents buf)) ""
- in
- Format.fprintf fmt f
- let pretty =
- if T.pretty == from_pretty_code then pretty_code
- else T.pretty
+ let pretty = T.pretty
let varname =
if T.varname == undefined then undefined
@@ -216,8 +188,6 @@ struct
compare = compare;
hash = hash;
copy = copy;
- internal_pretty_code = internal_pretty_code;
- pretty_code = pretty_code;
pretty = pretty;
varname = varname;
mem_project = mem_project }
@@ -261,7 +231,6 @@ module type Make_input = sig
val compare: t -> t -> int
val hash: t -> int
val copy: t -> t
- val internal_pretty_code: Type.precedence -> Format.formatter -> t -> unit
val pretty: Format.formatter -> t -> unit
val varname: t -> string
val mem_project: (Project_skeleton.t -> bool) -> t -> bool
@@ -353,10 +322,6 @@ module type Polymorphic2_input = sig
('a -> 'a -> int) -> ('b -> 'b -> int) -> ('a, 'b) t -> ('a, 'b) t -> int
val mk_hash: ('a -> int) -> ('b -> int) -> ('a, 'b) t -> int
val map: ('a -> 'a) -> ('b -> 'b) -> ('a, 'b) t -> ('a, 'b) t
- val mk_internal_pretty_code:
- (Type.precedence -> Format.formatter -> 'a -> unit) ->
- (Type.precedence -> Format.formatter -> 'b -> unit) ->
- Type.precedence -> Format.formatter -> ('a, 'b) t -> unit
val mk_pretty:
(Format.formatter -> 'a -> unit) -> (Format.formatter -> 'b -> unit) ->
Format.formatter -> ('a, 'b) t -> unit
@@ -423,12 +388,6 @@ module Polymorphic2(P: Polymorphic2_input) = struct
else*) P.map f1 f2
in
build mk T1.copy T2.copy
- let internal_pretty_code =
- let mk f1 f2 =
- if f1 == pp_fail || f2 == pp_fail then pp_fail
- else fun p fmt x -> P.mk_internal_pretty_code f1 f2 p fmt x
- in
- build mk T1.internal_pretty_code T2.internal_pretty_code
let pretty = build P.mk_pretty T1.pretty T2.pretty
let varname = build P.mk_varname T1.varname T2.varname
let mem_project =
@@ -475,11 +434,6 @@ module Polymorphic3
('a -> int) -> ('b -> int) -> ('c -> int) -> ('a, 'b, 'c) t -> int
val map:
('a -> 'a) -> ('b -> 'b) -> ('c -> 'c) -> ('a, 'b, 'c) t -> ('a, 'b, 'c) t
- val mk_internal_pretty_code:
- (Type.precedence -> Format.formatter -> 'a -> unit) ->
- (Type.precedence -> Format.formatter -> 'b -> unit) ->
- (Type.precedence -> Format.formatter -> 'c -> unit) ->
- Type.precedence -> Format.formatter -> ('a, 'b, 'c) t -> unit
val mk_pretty:
(Format.formatter -> 'a -> unit) ->
(Format.formatter -> 'b -> unit) ->
@@ -554,15 +508,6 @@ struct
else*) P.map f1 f2 f3
in
build mk T1.copy T2.copy T3.copy
- let internal_pretty_code =
- let mk f1 f2 f3 =
- if f1 == pp_fail || f2 == pp_fail || f3 == pp_fail then pp_fail
- else fun p fmt x -> P.mk_internal_pretty_code f1 f2 f3 p fmt x
- in
- build mk
- T1.internal_pretty_code
- T2.internal_pretty_code
- T3.internal_pretty_code
let pretty = build P.mk_pretty T1.pretty T2.pretty T3.pretty
let varname = build P.mk_varname T1.varname T2.varname T3.varname
let mem_project =
@@ -619,12 +564,6 @@ module Polymorphic4
val map:
('a -> 'a) -> ('b -> 'b) -> ('c -> 'c) -> ('d -> 'd) ->
('a, 'b, 'c, 'd) t -> ('a, 'b, 'c, 'd) t
- val mk_internal_pretty_code:
- (Type.precedence -> Format.formatter -> 'a -> unit) ->
- (Type.precedence -> Format.formatter -> 'b -> unit) ->
- (Type.precedence -> Format.formatter -> 'c -> unit) ->
- (Type.precedence -> Format.formatter -> 'd -> unit) ->
- Type.precedence -> Format.formatter -> ('a, 'b, 'c, 'd) t -> unit
val mk_pretty:
(Format.formatter -> 'a -> unit) ->
(Format.formatter -> 'b -> unit) ->
@@ -704,17 +643,6 @@ struct
else*) P.map f1 f2 f3 f4
in
build mk T1.copy T2.copy T3.copy T4.copy
- let internal_pretty_code =
- let mk f1 f2 f3 f4 =
- if f1 == pp_fail || f2 == pp_fail || f3 == pp_fail || f4 == pp_fail
- then pp_fail
- else fun p fmt x -> P.mk_internal_pretty_code f1 f2 f3 f4 p fmt x
- in
- build mk
- T1.internal_pretty_code
- T2.internal_pretty_code
- T3.internal_pretty_code
- T4.internal_pretty_code
let pretty = build P.mk_pretty T1.pretty T2.pretty T3.pretty T4.pretty
let varname =
build P.mk_varname T1.varname T2.varname T3.varname T4.varname
@@ -763,15 +691,9 @@ module Pair_arg = struct
if x == y then 0 else let n = f1 x1 y1 in if n = 0 then f2 x2 y2 else n
let mk_hash f1 f2 (x1,x2) = f1 x1 + 1351 * f2 x2
let map f1 f2 (x1,x2) = f1 x1, f2 x2
- let mk_internal_pretty_code f1 f2 p fmt (x1, x2) =
- let pp fmt =
- Format.fprintf
- fmt "@[<hv 2>%a,@;%a@]" (f1 Type.Tuple) x1 (f2 Type.Tuple) x2
- in
- Type.par p Type.Tuple fmt pp
- let mk_pretty f1 f2 fmt p =
- Format.fprintf fmt "@[%a@]" (* Type.par put the parenthesis *)
- (mk_internal_pretty_code (fun _ -> f1) (fun _ -> f2) Type.Basic) p
+ let mk_pretty f1 f2 fmt (x1, x2) =
+ let pp fmt = Format.fprintf fmt "@[<hv 2>%a,@;%a@]" f1 x1 f2 x2 in
+ Type.par Type.Basic Type.Tuple fmt pp
let mk_varname = undefined
let mk_mem_project mem1 mem2 f (x1, x2) = mem1 f x1 && mem2 f x2
end
@@ -819,9 +741,7 @@ let pair (type typ1) (type typ2) (ty1: typ1 Type.t) (ty2: typ2 Type.t) =
let compare = compare X.ty
let hash = hash X.ty
let copy = copy X.ty
- let internal_pretty_code = internal_pretty_code X.ty
- let pretty_code = pretty_code X.ty
- let pretty = from_pretty_code
+ let pretty = pretty X.ty
let varname = varname ty
let mem_project = mem_project X.ty
end
@@ -848,7 +768,6 @@ struct
let hash = undefined
let rehash = undefined
let copy = undefined
- let internal_pretty_code = undefined
let pretty = undefined
let varname _ = "f"
let mem_project = never_any_project
@@ -890,9 +809,6 @@ module type Polymorphic_input = sig
val mk_compare: ('a -> 'a -> int) -> 'a t -> 'a t -> int
val mk_hash: ('a -> int) -> 'a t -> int
val map: ('a -> 'a) -> 'a t -> 'a t
- val mk_internal_pretty_code:
- (Type.precedence -> Format.formatter -> 'a -> unit) ->
- Type.precedence -> Format.formatter -> 'a t -> unit
val mk_pretty:
(Format.formatter -> 'a -> unit) -> Format.formatter -> 'a t -> unit
val mk_varname: ('a -> string) -> 'a t -> string
@@ -958,13 +874,6 @@ module Polymorphic_gen(P: Polymorphic_input) = struct
(*if f == identity then identity else*)
fun x -> P.map X.copy x
let rehash = R.rehash
-
- let internal_pretty_code =
- let mk f =
- if f == pp_fail then pp_fail
- else fun p fmt x -> P.mk_internal_pretty_code f p fmt x
- in
- build mk X.internal_pretty_code
let pretty = build P.mk_pretty X.pretty
let varname = build P.mk_varname X.varname
let mem_project =
@@ -1014,11 +923,9 @@ module Poly_ref =
let mk_compare f x y = if x == y then 0 else f !x !y
let mk_hash f x = f !x
let map f x = ref (f !x)
- let mk_internal_pretty_code f p fmt x =
- let pp fmt = Format.fprintf fmt "@[<hv 2>ref@;%a@]" (f Type.Call) !x in
- Type.par p Type.Call fmt pp
let mk_pretty f fmt x =
- mk_internal_pretty_code (fun _ -> f) Type.Basic fmt x
+ let pp fmt = Format.fprintf fmt "@[<hv 2>ref@;%a@]" f !x in
+ Type.par Type.Basic Type.Call fmt pp
let mk_varname = undefined
let mk_mem_project mem f x = mem f !x
end)
@@ -1038,9 +945,7 @@ let t_ref (type typ) (ty: typ Type.t) =
let compare = compare ty
let hash = hash ty
let copy = copy ty
- let internal_pretty_code = internal_pretty_code ty
- let pretty_code = pretty_code ty
- let pretty = from_pretty_code
+ let pretty = pretty ty
let varname = varname ty
let mem_project = mem_project ty
end)
@@ -1073,15 +978,13 @@ module Poly_option =
| Some x, Some y -> f x y
let mk_hash f = function None -> 0 | Some x -> f x
let map f = function None -> None | Some x -> Some (f x)
- let mk_internal_pretty_code f p fmt = function
+ let mk_pretty f fmt = function
| None -> Format.fprintf fmt "None"
| Some x ->
let pp fmt =
- Format.fprintf fmt "@[<hv 2>Some@;%a@]" (f Type.Call) x
+ Format.fprintf fmt "@[<hv 2>Some@;%a@]" f x
in
- Type.par p Type.Call fmt pp
- let mk_pretty f fmt x =
- mk_internal_pretty_code (fun _ -> f) Type.Basic fmt x
+ Type.par Type.Basic Type.Call fmt pp
let mk_varname = undefined
let mk_mem_project mem f = function None -> false | Some x -> mem f x
end)
@@ -1102,9 +1005,7 @@ let option (type typ) (ty: typ Type.t) =
let compare = compare ty
let hash = hash ty
let copy = copy ty
- let internal_pretty_code = internal_pretty_code ty
- let pretty_code = pretty_code ty
- let pretty = from_pretty_code
+ let pretty = pretty ty
let varname = varname ty
let mem_project = mem_project ty
end)
@@ -1146,20 +1047,18 @@ module Poly_list =
(0,1) l)
with Too_long n -> n
let map = List.map
- let mk_internal_pretty_code f p fmt l =
+ let mk_pretty f fmt l =
let pp fmt =
Format.fprintf fmt "@[<hv 2>[ %t ]@]"
(fun fmt ->
let rec print fmt = function
| [] -> ()
- | [ x ] -> Format.fprintf fmt "%a" (f Type.List) x
- | x :: l -> Format.fprintf fmt "%a;@;%a" (f Type.List) x print l
+ | [ x ] -> Format.fprintf fmt "%a" f x
+ | x :: l -> Format.fprintf fmt "%a;@;%a" f x print l
in
print fmt l)
in
- Type.par p Type.Basic fmt pp (* Never enclose lists in parentheses *)
- let mk_pretty f fmt x =
- mk_internal_pretty_code (fun _ -> f) Type.Basic fmt x
+ Type.par Type.Basic Type.Basic fmt pp (* Never enclose lists in parentheses *)
let mk_varname = undefined
let mk_mem_project mem f = List.exists (mem f)
end)
@@ -1180,9 +1079,7 @@ let list (type typ) (ty: typ Type.t) =
let compare = compare ty
let hash = hash ty
let copy = copy ty
- let internal_pretty_code = internal_pretty_code ty
- let pretty_code = pretty_code ty
- let pretty = from_pretty_code
+ let pretty = pretty ty
let varname = varname ty
let mem_project = mem_project ty
end)
@@ -1234,21 +1131,19 @@ module Poly_array =
!acc
;;
let map = Array.map
- let mk_internal_pretty_code f p fmt a =
+ let mk_pretty f fmt a =
let pp fmt =
Format.fprintf fmt "@[<hv 2>[| %t |]@]"
(fun fmt ->
let length = Array.length a in
match length with
| 0 -> ()
- | _ -> (Format.fprintf fmt "%a" (f Type.List) a.(0);
+ | _ -> (Format.fprintf fmt "%a" f a.(0);
for i = 1 to (length - 1) do
- Format.fprintf fmt ";@;%a" (f Type.List) a.(i)
+ Format.fprintf fmt ";@;%a" f a.(i)
done))
in
- Type.par p Type.Basic fmt pp (* Never enclose arrays in parentheses *)
- let mk_pretty f fmt x =
- mk_internal_pretty_code (fun _ -> f) Type.Basic fmt x
+ Type.par Type.Basic Type.Basic fmt pp (* Never enclose arrays in parentheses *)
let mk_varname = undefined
let mk_mem_project mem f a =
try
@@ -1274,9 +1169,7 @@ let array (type typ) (ty: typ Type.t) =
let compare = compare ty
let hash = hash ty
let copy = copy ty
- let internal_pretty_code = internal_pretty_code ty
- let pretty_code = pretty_code ty
- let pretty = from_pretty_code
+ let pretty = pretty ty
let varname = varname ty
let mem_project = mem_project ty
end)
@@ -1304,7 +1197,6 @@ module Poly_queue =
let mk_compare = undefined
let mk_hash = undefined
let map = undefined
- let mk_internal_pretty_code = undefined
let mk_pretty = undefined
let mk_varname = undefined
let mk_mem_project mem f q =
@@ -1327,9 +1219,7 @@ let queue (type typ) (ty: typ Type.t) =
let compare = compare ty
let hash = hash ty
let copy = copy ty
- let internal_pretty_code = internal_pretty_code ty
- let pretty_code = pretty_code ty
- let pretty = from_pretty_code
+ let pretty = pretty ty
let varname = varname ty
let mem_project = mem_project ty
end)
@@ -1375,27 +1265,6 @@ struct
(* if E.copy == identity then identity
else*) fun s -> S.fold (fun x -> S.add (E.copy x)) s S.empty
- let internal_pretty_code p_caller fmt s =
- if is_empty s then
- Format.fprintf fmt "%s.empty" Info.module_name
- else
- let pp fmt =
- if S.cardinal s = 1 then
- Format.fprintf fmt "@[<hv 2>%s.singleton@;%a@]"
- Info.module_name
- (E.internal_pretty_code Type.Call)
- (Caml_list.hd (S.elements s))
- else
- Format.fprintf fmt
- "@[<hv 2>List.fold_left@;\
- (fun acc s -> %s.add s acc)@;%s.empty@;%a@]"
- Info.module_name
- Info.module_name
- (let module L = List(E) in L.internal_pretty_code Type.Call)
- (S.elements s)
- in
- Type.par p_caller Type.Call fmt pp
-
let pretty fmt s =
let pp_elt pp fmt v =
Format.fprintf fmt "@[%a@]" pp v
@@ -1424,8 +1293,6 @@ struct
let equal = P.equal
let compare = P.compare
let hash = P.hash
- let internal_pretty_code = P.internal_pretty_code
- let pretty_code = P.pretty_code
let pretty = P.pretty
let varname = P.varname
let mem_project = P.mem_project
@@ -1459,28 +1326,6 @@ struct
let mk_equal = M.equal
let mk_hash = undefined
let map = M.map
- let mk_internal_pretty_code = undefined
- (*f_value p_caller fmt map =
- (* [JS 2011/04/01] untested code! *)
- let pp_empty fmt = Format.fprintf fmt "%s.empty" Info.module_name in
- if M.is_empty map then
- Type.par p_caller Type.Basic fmt pp_empty
- else
- let pp fmt =
- Format.fprintf
- fmt "@[<hv 2>@[<hv 2>let map =@;%t@;<1 -2>in@]" pp_empty;
- M.iter
- (fun k v ->
- Format.fprintf
- fmt
- "@[<hv 2>let map =@;%s.add@;@[<hv 2>map@;%a@;%a@]@;<1 -2>in@]"
- Info.module_name
- (Key.internal_pretty_code Type.Call) k
- (f_value Type.Call) v)
- map;
- Format.fprintf fmt "@[map@]@]"
- in
- Type.par p_caller Type.Call fmt pp*)
let mk_pretty f_value fmt map =
Format.fprintf fmt "@[{{ ";
M.iter
@@ -1570,8 +1415,7 @@ struct
let h2 = H.create (H.length tbl) (* may be very memory-consuming *) in
H.iter (fun k v -> H.add h2 k v) h;
h2
- let mk_internal_pretty_code = undefined
- let mk_pretty = from_pretty_code
+ let mk_pretty = undefined
let mk_varname = undefined
let mk_mem_project =
if Key.mem_project == undefined then undefined
@@ -1624,7 +1468,6 @@ struct
let descr = Descr.of_type ty
let packed_descr = Descr.pack descr
let reprs = Type.reprs ty
- let pretty_code = undefined
end)
in M.ty
@@ -1748,8 +1591,6 @@ struct
let hash = FCHashtbl.hash
let rehash = identity
let copy = X.copy
- let internal_pretty_code =
- if X.pretty == undefined then undefined else fun _ -> X.pretty
let pretty = X.pretty
let varname = X.varname
let mem_project = never_any_project
@@ -1900,7 +1741,6 @@ module Formatter =
let hash = undefined
let rehash = undefined
let copy = undefined
- let internal_pretty_code = undefined
let pretty = undefined
let varname _ = "fmt"
let mem_project = never_any_project
@@ -1919,14 +1759,6 @@ module Integer =
let hash = Integer.hash
let rehash = identity
let copy = identity
- let internal_pretty_code par fmt n =
- let pp fmt =
- Format.fprintf
- fmt
- "Integer.of_string %S"
- (Integer.to_string n)
- in
- Type.par par Type.Call fmt pp
(* TODO: this should take into account kernel's option -big-ints-hex *)
let pretty = Integer.pretty
let varname _ = "integer_n"
@@ -1977,20 +1809,11 @@ module Triple_arg = struct
else n
let mk_hash f1 f2 f3 (x1,x2,x3) = f1 x1 + 1351 * f2 x2 + 257 * f3 x3
let map f1 f2 f3 (x1,x2,x3) = f1 x1, f2 x2, f3 x3
- let mk_internal_pretty_code f1 f2 f3 p fmt (x1, x2, x3) =
+ let mk_pretty f1 f2 f3 fmt (x1, x2, x3) =
let pp fmt =
- Format.fprintf
- fmt "@[<hv 2>%a,@;%a,@;%a@]"
- (f1 Type.Tuple) x1
- (f2 Type.Tuple) x2
- (f3 Type.Tuple) x3
+ Format.fprintf fmt "@[<hv 2>%a,@;%a,@;%a@]" f1 x1 f2 x2 f3 x3
in
- Type.par p Type.Tuple fmt pp
- let mk_pretty f1 f2 f3 fmt p =
- Format.fprintf fmt "@[(%a)@]"
- (mk_internal_pretty_code
- (fun _ -> f1) (fun _ -> f2) (fun _ -> f3) Type.Basic)
- p
+ Type.par Type.Basic Type.Tuple fmt pp
let mk_varname = undefined
let mk_mem_project mem1 mem2 mem3 f (x1, x2, x3) =
mem1 f x1 && mem2 f x2 && mem3 f x3
@@ -2042,9 +1865,7 @@ let triple
let compare = compare X.ty
let hash = hash X.ty
let copy = copy X.ty
- let internal_pretty_code = internal_pretty_code X.ty
- let pretty_code = pretty_code X.ty
- let pretty = from_pretty_code
+ let pretty = pretty X.ty
let varname = varname ty
let mem_project = mem_project X.ty
end
@@ -2086,21 +1907,11 @@ module Quadruple_arg = struct
let mk_hash f1 f2 f3 f4 (x1,x2,x3,x4) =
f1 x1 + 1351 * f2 x2 + 257 * f3 x3 + 997 * f4 x4
let map f1 f2 f3 f4 (x1,x2,x3,x4) = f1 x1, f2 x2, f3 x3, f4 x4
- let mk_internal_pretty_code f1 f2 f3 f4 p fmt (x1, x2, x3, x4) =
+ let mk_pretty f1 f2 f3 f4 fmt (x1, x2, x3, x4) =
let pp fmt =
- Format.fprintf
- fmt "@[<hv 2>%a,@;%a,@;%a,@;%a@]"
- (f1 Type.Tuple) x1
- (f2 Type.Tuple) x2
- (f3 Type.Tuple) x3
- (f4 Type.Tuple) x4
+ Format.fprintf fmt "@[<hv 2>%a,@;%a,@;%a,@;%a@]" f1 x1 f2 x2 f3 x3 f4 x4
in
- Type.par p Type.Tuple fmt pp
- let mk_pretty f1 f2 f3 f4 fmt p =
- Format.fprintf fmt "@[(%a)@]"
- (mk_internal_pretty_code
- (fun _ -> f1) (fun _ -> f2) (fun _ -> f3) (fun _ -> f4) Type.Basic)
- p
+ Type.par Type.Basic Type.Tuple fmt pp
let mk_varname = undefined
let mk_mem_project mem1 mem2 mem3 mem4 f (x1, x2, x3, x4) =
mem1 f x1 && mem2 f x2 && mem3 f x3 && mem4 f x4
@@ -2157,9 +1968,7 @@ let quadruple
let compare = compare X.ty
let hash = hash X.ty
let copy = copy X.ty
- let internal_pretty_code = internal_pretty_code X.ty
- let pretty_code = pretty_code X.ty
- let pretty = from_pretty_code
+ let pretty = pretty X.ty
let varname = varname ty
let mem_project = mem_project X.ty
end
diff --git a/src/libraries/datatype/datatype.mli b/src/libraries/datatype/datatype.mli
index fb520585b8f4155b5c48fc2210699e5c7f033c87..057a592dff5fbc54bf93733e866cd5a111591c47 100644
--- a/src/libraries/datatype/datatype.mli
+++ b/src/libraries/datatype/datatype.mli
@@ -36,8 +36,6 @@ type 'a t = private
compare: 'a -> 'a -> int;
hash: 'a -> int;
copy: 'a -> 'a;
- internal_pretty_code: Type.precedence -> Format.formatter -> 'a -> unit;
- pretty_code: Format.formatter -> 'a -> unit;
pretty: Format.formatter -> 'a -> unit;
varname: 'a -> string;
mem_project: (Project_skeleton.t -> bool) -> 'a -> bool }
@@ -74,14 +72,6 @@ module type S_no_copy = sig
val hash: t -> int
(** Hash function: same spec than [Hashtbl.hash]. *)
- val pretty_code: Format.formatter -> t -> unit
- (** Pretty print each value in an ML-like style: the result must be a valid
- OCaml expression. Only useful for journalisation. *)
-
- val internal_pretty_code: Type.precedence -> Format.formatter -> t -> unit
- (** Same spec than [pretty_code], but must take care of the precedence of the
- context in order to put parenthesis if required. See {!Type.par}. *)
-
val pretty: Format.formatter -> t -> unit
(** Pretty print each value in an user-friendly way. *)
@@ -111,9 +101,6 @@ val equal: 'a Type.t -> 'a -> 'a -> bool
val compare: 'a Type.t -> 'a -> 'a -> int
val hash: 'a Type.t -> 'a -> int
val copy: 'a Type.t -> 'a -> 'a
-val internal_pretty_code:
- 'a Type.t -> Type.precedence -> Format.formatter -> 'a -> unit
-val pretty_code: 'a Type.t -> Format.formatter -> 'a -> unit
val pretty: 'a Type.t -> Format.formatter -> 'a -> unit
val varname: 'a Type.t -> 'a -> string
val mem_project: 'a Type.t -> (Project_skeleton.t -> bool) -> 'a -> bool
@@ -135,20 +122,11 @@ val from_compare: 'a -> 'a -> bool
(** Must be used for [equal] in order to implement it by [compare x y = 0]
(with your own [compare] function). *)
-val from_pretty_code: Format.formatter -> 'a -> unit
-(** Must be used for [pretty] in order to implement it by [pretty_code]
- provided by the datatype from your own [internal_pretty_code] function. *)
-
val never_any_project: (Project_skeleton.t -> bool) -> 'a -> bool
(** Must be used for [mem_project] if values of your type does never contain
any project.
@plugin development guide *)
-val pp_fail: Type.precedence -> Format.formatter -> 'a -> unit
-(** Must be used for [internal_pretty_code] if this pretty-printer must
- fail only when called.
- @plugin development guide *)
-
(** Sub-signature of {!S}.
@plugin development guide *)
module type Undefined = sig
@@ -158,7 +136,6 @@ module type Undefined = sig
val hash: 'a -> int
val rehash: 'a -> 'a
val copy: 'a -> 'a
- val internal_pretty_code: Type.precedence -> Format.formatter -> 'a -> unit
val pretty: Format.formatter -> 'a -> unit
val varname: 'a -> string
val mem_project: (Project_skeleton.t -> bool) -> 'a -> bool
@@ -215,7 +192,6 @@ module type Make_input = sig
val compare: t -> t -> int
val hash: t -> int
val copy: t -> t
- val internal_pretty_code: Type.precedence -> Format.formatter -> t -> unit
val pretty: Format.formatter -> t -> unit
val varname: t -> string
val mem_project: (Project_skeleton.t -> bool) -> t -> bool
@@ -374,9 +350,6 @@ module Polymorphic
val mk_compare: ('a -> 'a -> int) -> 'a t -> 'a t -> int
val mk_hash: ('a -> int) -> 'a t -> int
val map: ('a -> 'a) -> 'a t -> 'a t
- val mk_internal_pretty_code:
- (Type.precedence -> Format.formatter -> 'a -> unit) ->
- Type.precedence -> Format.formatter -> 'a t -> unit
val mk_pretty:
(Format.formatter -> 'a -> unit) -> Format.formatter -> 'a t -> unit
val mk_varname: ('a -> string) -> 'a t -> string
@@ -404,10 +377,6 @@ module Polymorphic2
('a -> 'a -> int) -> ('b -> 'b -> int) -> ('a, 'b) t -> ('a, 'b) t -> int
val mk_hash: ('a -> int) -> ('b -> int) -> ('a, 'b) t -> int
val map: ('a -> 'a) -> ('b -> 'b) -> ('a, 'b) t -> ('a, 'b) t
- val mk_internal_pretty_code:
- (Type.precedence -> Format.formatter -> 'a -> unit) ->
- (Type.precedence -> Format.formatter -> 'b -> unit) ->
- Type.precedence -> Format.formatter -> ('a, 'b) t -> unit
val mk_pretty:
(Format.formatter -> 'a -> unit) -> (Format.formatter -> 'b -> unit) ->
Format.formatter -> ('a, 'b) t -> unit
@@ -443,11 +412,6 @@ module Polymorphic3
('a -> int) -> ('b -> int) -> ('c -> int) -> ('a, 'b, 'c) t -> int
val map:
('a -> 'a) -> ('b -> 'b) -> ('c -> 'c) -> ('a, 'b, 'c) t -> ('a, 'b, 'c) t
- val mk_internal_pretty_code:
- (Type.precedence -> Format.formatter -> 'a -> unit) ->
- (Type.precedence -> Format.formatter -> 'b -> unit) ->
- (Type.precedence -> Format.formatter -> 'c -> unit) ->
- Type.precedence -> Format.formatter -> ('a, 'b, 'c) t -> unit
val mk_pretty:
(Format.formatter -> 'a -> unit) ->
(Format.formatter -> 'b -> unit) ->
@@ -493,12 +457,6 @@ module Polymorphic4
val map:
('a -> 'a) -> ('b -> 'b) -> ('c -> 'c) -> ('d -> 'd) ->
('a, 'b, 'c, 'd) t -> ('a, 'b, 'c, 'd) t
- val mk_internal_pretty_code:
- (Type.precedence -> Format.formatter -> 'a -> unit) ->
- (Type.precedence -> Format.formatter -> 'b -> unit) ->
- (Type.precedence -> Format.formatter -> 'c -> unit) ->
- (Type.precedence -> Format.formatter -> 'd -> unit) ->
- Type.precedence -> Format.formatter -> ('a, 'b, 'c, 'd) t -> unit
val mk_pretty:
(Format.formatter -> 'a -> unit) ->
(Format.formatter -> 'b -> unit) ->
diff --git a/src/libraries/project/project.ml b/src/libraries/project/project.ml
index 6038ec5acf3fa7150d43d61485fda483000263ac..0d47edbedc46ba14b6c969458e9d61f5d9bac06d 100644
--- a/src/libraries/project/project.ml
+++ b/src/libraries/project/project.ml
@@ -51,12 +51,6 @@ module D =
let hash p = p.pid
let rehash x = !rehash_ref x
let copy = Datatype.undefined
- let internal_pretty_code p_caller fmt p =
- let pp f =
- Format.fprintf
- f "@[<hv 2>Project.from_unique_name@;%S@]" p.unique_name
- in
- Type.par p_caller Type.Call fmt pp
let pretty fmt p = Format.fprintf fmt "project %S" p.unique_name
let varname p = "p_" ^ p.name
let mem_project f x = f x
diff --git a/src/libraries/project/state.ml b/src/libraries/project/state.ml
index c714007a60e0bc233cdcb00a4653c4661e4f3a64..0ad6eafe40dfdc63b244ec978ba02893fea76f9c 100644
--- a/src/libraries/project/state.ml
+++ b/src/libraries/project/state.ml
@@ -104,11 +104,6 @@ include Datatype.Make_with_collections
let hash x = Hashtbl.hash x.unique_name
let copy = Datatype.undefined
let rehash = Datatype.undefined
- let internal_pretty_code p_caller fmt s =
- let pp fmt =
- Format.fprintf fmt "@[<hv 2>State.get@;%S@]" s.unique_name
- in
- Type.par p_caller Type.Call fmt pp
let pretty fmt s = Format.fprintf fmt "state %S" s.unique_name
let varname = Datatype.undefined
let mem_project = Datatype.never_any_project
diff --git a/src/libraries/project/state_selection.ml b/src/libraries/project/state_selection.ml
index 1b47451c304629169556911d8dfe05cb382a6880..b24af0f01b80dca77c9a2099ab4ba78a72e6ba22 100644
--- a/src/libraries/project/state_selection.ml
+++ b/src/libraries/project/state_selection.ml
@@ -84,26 +84,6 @@ include Datatype.Make
type t = state_selection
let name = "State_selection"
let reprs = [ full; empty; singleton State.dummy ]
- let internal_pretty_code p_caller fmt (s, _) = match s with
- | Full -> Format.fprintf fmt "@[State_selection.full@]"
- | Subset sel ->
- match Selection.fold_vertex (fun s acc -> s :: acc) sel [] with
- | [] -> Format.fprintf fmt "@[State_selection.empty@]"
- | [ s ] ->
- let pp fmt =
- Format.fprintf fmt "@[<hv 2>State_selection.singleton@;%a@]"
- (State.internal_pretty_code Type.Call)
- s
- in
- Type.par p_caller Type.Call fmt pp
- | l ->
- let module D = Datatype.List(State) in
- let pp fmt =
- Format.fprintf fmt "@[<hv 2>State_selection.of_list@;%a@]"
- (D.internal_pretty_code Type.Call)
- l
- in
- Type.par p_caller Type.Call fmt pp
end)
let transitive_closure next_vertices s =
diff --git a/src/libraries/utils/hptmap.ml b/src/libraries/utils/hptmap.ml
index 2a29fcb5437f90b027183178cc4279b67ca55df2..d1e5ef01cfc800320c04d84a656d92693ad617be 100644
--- a/src/libraries/utils/hptmap.ml
+++ b/src/libraries/utils/hptmap.ml
@@ -680,7 +680,6 @@ struct
else fun x -> !rehash_ref x
let copy = Datatype.undefined
- let internal_pretty_code = Datatype.pp_fail
let pretty = pretty
let varname = Datatype.undefined
let mem_project = Datatype.never_any_project
diff --git a/src/libraries/utils/rangemap.ml b/src/libraries/utils/rangemap.ml
index 867f43b8443c24d327c065a841f9373a0b700318..a6bd7aa47447265271c9cea525bbb715ef557870 100644
--- a/src/libraries/utils/rangemap.ml
+++ b/src/libraries/utils/rangemap.ml
@@ -533,7 +533,6 @@ module Make(Ord: Datatype.S)(Value: Value) = struct
create l x d r
in aux
- let internal_pretty_code = Datatype.undefined
let pretty = Datatype.undefined
let varname = Datatype.undefined
let mem_project =
diff --git a/src/plugins/aorai/data_for_aorai.ml b/src/plugins/aorai/data_for_aorai.ml
index 2fb166151250623148259f3b087a508891f3ef4c..f0ec1a3c1b9f8cc3da2a9238e9fc88dea54b797a 100644
--- a/src/plugins/aorai/data_for_aorai.ml
+++ b/src/plugins/aorai/data_for_aorai.ml
@@ -45,10 +45,8 @@ module Aorai_state =
let rehash = Datatype.identity
let compare x y = Datatype.Int.compare x.nums y.nums
let copy = Datatype.identity
- let internal_pretty_code = Datatype.undefined
let pretty fmt x = Format.fprintf fmt "state_%d" x.nums
- let varname _ =
- assert false (* unused while internal_pretty_code is undefined *)
+ let varname _ = assert false
let mem_project = Datatype.never_any_project
end
)
@@ -67,7 +65,6 @@ module Aorai_typed_trans =
let rehash = Datatype.identity
let compare x y = Datatype.Int.compare x.numt y.numt
let copy = Datatype.identity
- let internal_pretty_code = Datatype.undefined
let pretty = Promelaoutput.Typed.print_transition
let varname _ = assert false
let mem_project = Datatype.never_any_project
@@ -1815,7 +1812,6 @@ module Range = Datatype.Make_with_collections
Bounded(Datatype.Int.copy c1, Cil_datatype.Term.copy c2)
| Unbounded c1 -> Unbounded (Datatype.Int.copy c1)
| Unknown -> Unknown
- let internal_pretty_code _ = Datatype.from_pretty_code
let pretty fmt = function
| Fixed c1 -> Format.fprintf fmt "%d" c1
| Interval (c1,c2) ->
diff --git a/src/plugins/obfuscator/obfuscator_kind.ml b/src/plugins/obfuscator/obfuscator_kind.ml
index 4cf3258f806d50e1e1d39be7292142a129296d32..c6902760336c482f5c103dafd3dd78173382c2fd 100644
--- a/src/plugins/obfuscator/obfuscator_kind.ml
+++ b/src/plugins/obfuscator/obfuscator_kind.ml
@@ -86,7 +86,6 @@ include Datatype.Make_with_collections
let equal (k1:k) k2 = k1 = k2
let compare (k1:k) k2 = Stdlib.compare k1 k2
let varname _ = "k"
- let internal_pretty_code = Datatype.undefined
let copy = Datatype.identity
let structural_descr = Structural_descr.t_abstract
let rehash = Datatype.identity
diff --git a/src/plugins/pdg_types/pdgTypes.ml b/src/plugins/pdg_types/pdgTypes.ml
index afbaaced4783c835beed71eb744ce1d972674fdd..89cbb18c701df356e5399c9990666c50707db0ed 100644
--- a/src/plugins/pdg_types/pdgTypes.ml
+++ b/src/plugins/pdg_types/pdgTypes.ml
@@ -80,7 +80,6 @@ end
let pretty = print_id
let rehash = Datatype.identity
let copy = Datatype.undefined
- let internal_pretty_code = Datatype.undefined
let varname = Datatype.undefined
let mem_project = Datatype.never_any_project
end)
diff --git a/src/plugins/slicing/slicingTypes.ml b/src/plugins/slicing/slicingTypes.ml
index f7aec3942446d5c1085b06b1c40b82f132023dbb..74a31d69012701e846df5255bd61c40a36ef231a 100644
--- a/src/plugins/slicing/slicingTypes.ml
+++ b/src/plugins/slicing/slicingTypes.ml
@@ -90,7 +90,6 @@ module Sl_project =
type t = sl_project
let reprs = [ SlicingInternals.dummy_project ]
let name = "SlicingTypes.Sl_project"
- let internal_pretty_code = pp_sl_project
let varname _s = "sl_project_"
let mem_project = Datatype.never_any_project
end)
@@ -113,7 +112,7 @@ let pp_sl_fct_slice p_caller fmt ff =
let pp fmt =
Format.fprintf fmt
"@[<hv 2>!Db.Slicing.Slice.from_num_id@;%a@;%d@]"
- (Kernel_function.internal_pretty_code Type.Call)
+ Kernel_function.pretty
ff.SlicingInternals.ff_fct.SlicingInternals.fi_kf
ff.SlicingInternals.ff_id
in
@@ -127,13 +126,12 @@ module Sl_fct_slice =
type t = fct_slice
let name = "SlicingTypes.Sl_fct_slice"
let reprs = [ dummy_fct_slice ]
- let internal_pretty_code = pp_sl_fct_slice
let mem_project = Datatype.never_any_project
end)
let dyn_sl_fct_slice = Sl_fct_slice.ty
-let pp_sl_mark p fmt m =
+let pp_sl_mark fmt m =
let pp = match m.SlicingInternals.m1, m.SlicingInternals.m2 with
| SlicingInternals.Spare, _ -> None
| _, SlicingInternals.Spare -> None
@@ -163,7 +161,7 @@ let pp_sl_mark p fmt m =
fun fmt ->
Format.fprintf fmt "@[<hv 2>SlicingInternals.create_sl_mark@;~m1:%a@;~m2:%a@]"
pp m.SlicingInternals.m1 pp m.SlicingInternals.m2
- in Type.par p Type.Call fmt pp
+ in pp fmt
module Sl_mark =
Datatype.Make_with_collections
@@ -177,8 +175,7 @@ module Sl_mark =
let hash = Hashtbl.hash
let copy = Datatype.undefined
let rehash = Datatype.undefined
- let internal_pretty_code = pp_sl_mark
- let pretty = Datatype.from_pretty_code
+ let pretty = pp_sl_mark
let mem_project = Datatype.never_any_project
let varname = Datatype.undefined
end)
diff --git a/src/plugins/slicing/slicingTypes.mli b/src/plugins/slicing/slicingTypes.mli
index fa1b7086ea0894379223e283aeebab93f1db5a51..fdf1db12067f758f993a76fb8e6d2a52f47e2879 100644
--- a/src/plugins/slicing/slicingTypes.mli
+++ b/src/plugins/slicing/slicingTypes.mli
@@ -80,9 +80,6 @@ module Sl_fct_slice : Datatype.S with type t = SlicingInternals.fct_slice
val dyn_sl_fct_slice : Sl_fct_slice.t Type.t
-val pp_sl_mark :
- Type.precedence -> Format.formatter -> SlicingInternals.pdg_mark -> unit
-
module Sl_mark : Datatype.S_with_collections with
type t = SlicingInternals.pdg_mark
diff --git a/src/plugins/value/partitioning/split_strategy.ml b/src/plugins/value/partitioning/split_strategy.ml
index 33b8e743fd5d16fa920731f70e1ad17d317a23be..c99e49e1754ef8734e1c0c41bcc0121070da8a3d 100644
--- a/src/plugins/value/partitioning/split_strategy.ml
+++ b/src/plugins/value/partitioning/split_strategy.ml
@@ -57,7 +57,6 @@ include
| SplitEqList l ->
List.fold_left (fun acc i -> acc * 13 + 57 * Int.hash i) 1 l
let copy = Datatype.identity
- let internal_pretty_code = Datatype.undefined
let pretty fmt = function
| NoSplit -> Format.pp_print_string fmt "no split"
| SplitAuto -> Format.pp_print_string fmt "auto split"
diff --git a/src/plugins/value/values/offsm_value.ml b/src/plugins/value/values/offsm_value.ml
index 51399e2b4ac008502951e6f7ef380ed865846fab..4408fd246315f1c962ab9ca2082117b80583a4a7 100644
--- a/src/plugins/value/values/offsm_value.ml
+++ b/src/plugins/value/values/offsm_value.ml
@@ -372,7 +372,6 @@ module Datatype_Offsm_or_top = Datatype.Make_with_collections(struct
| Top -> 7895
| O o -> V_Offsetmap.hash o
let copy = Datatype.undefined
- let internal_pretty_code = Datatype.undefined
let pretty fmt = function
| Top -> Format.pp_print_string fmt "TopO"
| O o -> Format.fprintf fmt "O @[%a@]" V_Offsetmap.pretty o
diff --git a/src/plugins/value_types/cvalue.ml b/src/plugins/value_types/cvalue.ml
index 61fc238db742832bc5ad2a2a42e13f2acd0cfbb8..e1fc93ee85a0f9a53603e027839f68a585f03a9d 100644
--- a/src/plugins/value_types/cvalue.ml
+++ b/src/plugins/value_types/cvalue.ml
@@ -857,7 +857,6 @@ module V_Or_Uninitialized = struct
let copy = Datatype.undefined
let rehash = Datatype.identity
let pretty = pretty
- let internal_pretty_code = Datatype.undefined
let varname = Datatype.undefined
let mem_project = Datatype.never_any_project
end)
diff --git a/src/plugins/value_types/function_Froms.ml b/src/plugins/value_types/function_Froms.ml
index dae6e569a3daee127b6787b0e120a77e630df317..00d0cfa6ad486c2052c0d3deccc68804d7075df8 100644
--- a/src/plugins/value_types/function_Froms.ml
+++ b/src/plugins/value_types/function_Froms.ml
@@ -59,7 +59,6 @@ struct
let mem_project = Datatype.never_any_project
let varname _ = "da"
- let internal_pretty_code = Datatype.undefined
let copy = Datatype.undefined
end)
@@ -180,7 +179,6 @@ module DepsOrUnassigned = struct
let mem_project = Datatype.never_any_project
let varname _ = "d"
- let internal_pretty_code = Datatype.undefined
let copy = Datatype.undefined
end)
@@ -625,7 +623,6 @@ include Datatype.Make
let compare = Datatype.undefined
let equal = equal
let pretty = pretty
- let internal_pretty_code = Datatype.undefined
let rehash = Datatype.identity
let copy = Datatype.undefined
let varname = Datatype.undefined
diff --git a/src/plugins/wp/Lang.ml b/src/plugins/wp/Lang.ml
index 7869f466d863f94344ca26fb4337f80d7d76551e..bf35e910cd26b721b40d38a5100f0118a4d0852b 100644
--- a/src/plugins/wp/Lang.ml
+++ b/src/plugins/wp/Lang.ml
@@ -684,7 +684,6 @@ struct
let copy _old = QZERO.create ()
let varname = Datatype.undefined
let pretty = Datatype.undefined
- let internal_pretty_code = Datatype.undefined
let mem_project _ _ = false
end)
diff --git a/src/plugins/wp/ctypes.ml b/src/plugins/wp/ctypes.ml
index 8a6ede3e75a66dd8af63d1a1a707833f5b853c3c..befde6664008ca58bcf8b9f20465631294c59169 100644
--- a/src/plugins/wp/ctypes.ml
+++ b/src/plugins/wp/ctypes.ml
@@ -582,7 +582,6 @@ module C_object = Datatype.Make(struct
let copy = Datatype.Undefined.copy
- let internal_pretty_code = Datatype.Undefined.internal_pretty_code
let mem_project = Datatype.Undefined.mem_project
let varname _ = "co"
diff --git a/src/plugins/wp/wpPropId.ml b/src/plugins/wp/wpPropId.ml
index b11a73f320de7ae2c6d42da2e0ea491449ab13d0..ec12ebe8695b4e50e4084c767b18c02d0425c2a6 100644
--- a/src/plugins/wp/wpPropId.ml
+++ b/src/plugins/wp/wpPropId.ml
@@ -260,7 +260,6 @@ module PropIdRaw =
let copy = Datatype.undefined
let rehash = Datatype.identity
- let internal_pretty_code = Datatype.undefined
let pretty = Datatype.undefined
let mem_project = Datatype.never_any_project
let varname = Datatype.undefined