Commit 0c4709dc authored by MARCHE Claude's avatar MARCHE Claude

remove unused and useless functions

parent 481ecc4f
......@@ -560,12 +560,6 @@ let print_model ?(me_name_trans = why_name_trans)
fmt
model = print_model ~print_attrs ~me_name_trans ~print_model_value fmt model
let model_to_string
~print_attrs
?(me_name_trans = why_name_trans)
model =
Format.asprintf "%a" (print_model ~print_attrs ~me_name_trans) model
let get_model_file model filename =
try
StringMap.find filename model
......@@ -578,30 +572,6 @@ let get_elements model_file line_number =
with Not_found ->
[]
(* TODO unused
let print_model_vc_term
~print_attrs
?(me_name_trans = why_name_trans)
?(sep = "\n")
fmt
model =
if not (is_model_empty model) then
match model.vc_term_loc with
| None -> fprintf fmt "error: cannot get location of the check"
| Some pos ->
let (filename, line_number, _, _) = Loc.get pos in
let model_file = get_model_file model.model_files filename in
let model_elements = get_elements model_file line_number in
print_model_elements ~print_attrs ~sep print_model_value me_name_trans fmt model_elements
let model_vc_term_to_string
~print_attrs
?(me_name_trans = why_name_trans)
?(sep = "\n")
model =
Format.asprintf "%a" (print_model_vc_term ~print_attrs ~me_name_trans ~sep) model
*)
let get_padding line =
try
let r = Str.regexp " *" in
......@@ -815,12 +785,6 @@ let print_model_json
fmt
model_files_bindings
let model_to_string_json
?(me_name_trans = why_name_trans)
?(vc_line_trans = (fun i -> string_of_int i))
model =
asprintf "%a" (print_model_json ~me_name_trans ~vc_line_trans) model
(*
***************************************************************
......
......@@ -171,42 +171,6 @@ val print_model_human :
*)
val model_to_string :
print_attrs:bool ->
?me_name_trans:(model_element_name -> string) ->
model ->
string
(** See print_model *)
(* TODO probably deprecated.
val print_model_vc_term :
print_attrs:bool ->
?me_name_trans: (model_element_name -> string) ->
?sep: string ->
Format.formatter ->
model ->
unit
(** Prints counter-example model elements related to term that
triggers VC.
@param sep separator of counter-example model elements
@param me_name_trans see print_model
@model the counter-example model.
*)
val model_vc_term_to_string :
print_attrs:bool ->
?me_name_trans: (model_element_name -> string) ->
?sep: string ->
model ->
string
(** Gets string with counter-example model elements related to term that
triggers VC.
See print_model_vc_term
*)
*)
val print_model_json :
?me_name_trans:(model_element_name -> string) ->
?vc_line_trans:(int -> string) ->
......@@ -266,13 +230,6 @@ val print_model_json :
}
*)
val model_to_string_json :
?me_name_trans:(model_element_name -> string) ->
?vc_line_trans:(int -> string) ->
model ->
string
(** See print_model_json *)
val interleave_with_source :
print_attrs:bool ->
?start_comment:string ->
......
......@@ -200,8 +200,8 @@ let craft_efficient_re l =
Str.regexp s
let debug_print_model ~print_attrs model =
let model_str = Model_parser.model_to_string ~print_attrs model in
Debug.dprintf debug "Call_provers: %s@." model_str
Debug.dprintf debug "Call_provers: %a@."
(Model_parser.print_model ?me_name_trans:None ~print_attrs) model
type answer_or_model = Answer of prover_answer | Model of string
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment