Commit 54acfb42 authored by David Hauzar's avatar David Hauzar

Printing counter-example model to json format.

parent c9a783fd
......@@ -141,7 +141,7 @@ LIBGENERATED = src/util/config.ml \
LIB_UTIL = config bigInt util opt lists strings \
extmap extset exthtbl weakhtbl \
hashcons stdlib exn_printer pp debug loc lexlib print_tree \
hashcons stdlib exn_printer pp json debug loc lexlib print_tree \
cmdline warning sysutil rc plugin bigInt number pqueue
LIB_CORE = ident ty term pattern decl theory \
......
......@@ -56,26 +56,29 @@ let array_add_element ~array ~index ~value =
arr_indices = arr_index::array.arr_indices;
}
let rec print_indices fmt indices =
let rec print_indices sanit_print fmt indices =
match indices with
| [] -> ()
| index::tail ->
fprintf fmt "; %d -> " index.arr_index_key;
print_model_value fmt index.arr_index_value;
print_indices fmt tail
print_model_value_sanit sanit_print fmt index.arr_index_value;
print_indices sanit_print fmt tail
and
print_array fmt arr =
print_array sanit_print fmt arr =
fprintf fmt "{others -> ";
print_model_value fmt arr.arr_others;
print_indices fmt arr.arr_indices;
print_model_value_sanit sanit_print fmt arr.arr_others;
print_indices sanit_print fmt arr.arr_indices;
fprintf fmt "}"
and
print_model_value fmt value =
print_model_value_sanit sanit_print fmt value =
(* Prints model value. *)
match value with
| Integer s -> fprintf fmt "%s" s
| Other s -> fprintf fmt "%s" s
| Array a -> print_array fmt a
| Integer s -> sanit_print fmt s
| Other s -> sanit_print fmt s
| Array a -> print_array sanit_print fmt a
let print_model_value fmt value =
print_model_value_sanit (fun fmt s -> fprintf fmt "%s" s) fmt value
(*
......@@ -168,13 +171,6 @@ let get_elements model_file line_number =
with Not_found ->
[]
let make_int_to_line_map lines =
let (map, _) = List.fold_left
(fun (map, num_line) line -> (IntMap.add num_line line map, num_line+1))
(IntMap.empty, 1)
lines in
map
let get_padding line =
try
let r = Str.regexp " *" in
......@@ -201,9 +197,7 @@ let interleave_line model_file (source_code, line_number) line =
let interleave_with_source model filename source_code =
try
let model_file = StringMap.find filename model in
(*let (_, model_file) = StringMap.choose model in*)
let lines = Str.split (Str.regexp "^") source_code in
(*let int_to_line_map = make_int_to_line_map lines in*)
let (source_code, _) = List.fold_left
(interleave_line model_file)
("", 1)
......@@ -211,7 +205,37 @@ let interleave_with_source model filename source_code =
source_code
with Not_found ->
source_code
(*
** Quering the model - json
*)
let print_model_value_to_json fmt me_value =
fprintf fmt "%a" (print_model_value_sanit Json.string) me_value
let print_model_element_json fmt me =
Json.print_json_field me.me_name print_model_value_to_json fmt me.me_value
let print_model_elements_json fmt model_elements =
Json.list print_model_element_json fmt model_elements
let print_model_elements_on_lines_json fmt model_file =
Json.map_bindings
(fun i -> string_of_int i)
print_model_elements_json
fmt
(IntMap.bindings model_file)
let print_model_json fmt model =
Json.map_bindings
(fun s -> s)
print_model_elements_on_lines_json
fmt
(StringMap.bindings model)
let model_to_string_json model =
print_model_json str_formatter model;
flush_str_formatter ()
(*
***************************************************************
......
......@@ -102,6 +102,10 @@ val print_model : Format.formatter -> model -> unit
val model_to_string : model -> string
val print_model_json : Format.formatter -> model -> unit
val model_to_string_json : model -> string
val interleave_with_source : model -> string -> string -> string
(*
......
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2015 -- INRIA - CNRS - Paris-Sud University *)
(* *)
(* This software is distributed under the terms of the GNU Lesser *)
(* General Public License version 2.1, with the special exception *)
(* on linking described in file LICENSE. *)
(* *)
(********************************************************************)
let string fmt s =
let b = Buffer.create (2 * String.length s) in
Buffer.add_char b '"';
for i = 0 to String.length s -1 do
match s.[i] with
| '"' -> Buffer.add_string b "\\\""
| '\\' -> Buffer.add_string b "\\\\"
| c -> Buffer.add_char b c
done;
Buffer.add_char b '"';
Format.fprintf fmt "%s" (Buffer.contents b)
let int fmt d = Format.fprintf fmt "%d" d
let bool fmt b = Format.fprintf fmt "%b" b
let print_json_field key value_pr fmt value =
Format.fprintf fmt "%a : %a " string key value_pr value
let list pr fmt l =
if l = [] then Format.fprintf fmt "[]"
else
Pp.print_list_delim ~start:Pp.lsquare ~stop:Pp.rsquare ~sep:Pp.comma
pr fmt l
let print_map_binding key_to_str value_pr fmt binding =
let (key, value) = binding in
print_json_field (key_to_str key) value_pr fmt value
let map_bindings key_to_str value_pr fmt map_bindings =
if map_bindings = [] then Format.fprintf fmt "{}"
else
Pp.print_list_delim ~start:Pp.lbrace ~stop:Pp.rbrace ~sep:Pp.comma
(print_map_binding key_to_str value_pr) fmt map_bindings
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2015 -- INRIA - CNRS - Paris-Sud University *)
(* *)
(* This software is distributed under the terms of the GNU Lesser *)
(* General Public License version 2.1, with the special exception *)
(* on linking described in file LICENSE. *)
(* *)
(********************************************************************)
val string : Format.formatter -> string -> unit
val int : Format.formatter -> int -> unit
val bool : Format.formatter -> bool -> unit
val list :
(Format.formatter -> 'a -> unit) -> Format.formatter -> 'a list -> unit
val map_bindings :
('a -> string) ->
(Format.formatter -> 'b -> unit) ->
Format.formatter ->
('a * 'b) list ->
unit
val print_json_field :
string -> (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a -> unit
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