Commit 99f12932 authored by Sylvain Dailler's avatar Sylvain Dailler
Browse files

Improve displaying of human readable counterexample.

parent 4cbabcdb
...@@ -279,20 +279,20 @@ let print_float_human fmt f = ...@@ -279,20 +279,20 @@ let print_float_human fmt f =
| Float_hexa(s,f) -> fprintf fmt "%s (%g)" s f | Float_hexa(s,f) -> fprintf fmt "%s (%g)" s f
let rec print_array_human fmt (arr: model_array) = let rec print_array_human fmt (arr: model_array) =
fprintf fmt "("; fprintf fmt "@[(";
List.iter (fun e -> List.iter (fun e ->
fprintf fmt "%s => %a," e.arr_index_key print_model_value_human e.arr_index_value) fprintf fmt "@[%s =>@ %a,@]" e.arr_index_key print_model_value_human e.arr_index_value)
arr.arr_indices; arr.arr_indices;
fprintf fmt "others => %a)" print_model_value_human arr.arr_others fprintf fmt "@[others =>@ %a@])@]" print_model_value_human arr.arr_others
and print_record_human fmt r = and print_record_human fmt r =
fprintf fmt "%a" fprintf fmt "@[%a@]"
(Pp.print_list_delim ~start:Pp.lbrace ~stop:Pp.rbrace ~sep:Pp.semi (Pp.print_list_delim ~start:Pp.lbrace ~stop:Pp.rbrace ~sep:Pp.semi
(fun fmt (f, v) -> fprintf fmt "%s = %a" f print_model_value_human v)) r (fun fmt (f, v) -> fprintf fmt "@[%s =@ %a@]" f print_model_value_human v)) r
and print_proj_human fmt p = and print_proj_human fmt p =
let s, v = p in let s, v = p in
fprintf fmt "%s %a" fprintf fmt "@[{%s =>@ %a}@]"
s print_model_value_human v s print_model_value_human v
and print_model_value_human fmt (v: model_value) = and print_model_value_human fmt (v: model_value) =
...@@ -302,8 +302,10 @@ and print_model_value_human fmt (v: model_value) = ...@@ -302,8 +302,10 @@ and print_model_value_human fmt (v: model_value) =
| Fraction (s1, s2) -> fprintf fmt "%s" (s1 ^ "/" ^ s2) | Fraction (s1, s2) -> fprintf fmt "%s" (s1 ^ "/" ^ s2)
| Float f -> print_float_human fmt f | Float f -> print_float_human fmt f
| Boolean b -> fprintf fmt "%b" b | Boolean b -> fprintf fmt "%b" b
| Apply (s, []) ->
fprintf fmt "%s" s
| Apply (s, lt) -> | Apply (s, lt) ->
fprintf fmt "(%s %a)" s (Pp.print_list Pp.space print_model_value_human) lt fprintf fmt "@[(%s@ %a)@]" s (Pp.print_list Pp.space print_model_value_human) lt
| Array arr -> print_array_human fmt arr | Array arr -> print_array_human fmt arr
| Record r -> print_record_human fmt r | Record r -> print_record_human fmt r
| Proj p -> print_proj_human fmt p | Proj p -> print_proj_human fmt p
......
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