Commit ad0217fa authored by Sylvain Dailler's avatar Sylvain Dailler

ce: Adapt counterexamples for API uses

one field record optim: Default name of the record field is taken when an
empty model_trace is provided.
Add a registered function allowing removal of some record values before
displaying to the user.
parent 5ac4f862
...@@ -438,6 +438,7 @@ let compute_model_trace_field pj d = ...@@ -438,6 +438,7 @@ let compute_model_trace_field pj d =
| Some pj -> | Some pj ->
let name = get_model_trace_string let name = get_model_trace_string
~name:pj.id_string ~attrs:pj.id_attrs in ~name:pj.id_string ~attrs:pj.id_attrs in
let name = if name = "" then pj.id_string else name in
let attr = "field:" ^ (string_of_int d) ^ ":" ^ name in let attr = "field:" ^ (string_of_int d) ^ ":" ^ name in
Sattr.singleton (create_attribute attr) Sattr.singleton (create_attribute attr)
......
...@@ -876,14 +876,16 @@ let internal_loc t = ...@@ -876,14 +876,16 @@ let internal_loc t =
| Tapp (ls, []) -> ls.ls_name.id_loc | Tapp (ls, []) -> ls.ls_name.id_loc
| _ -> None | _ -> None
let default_remove_field (v: model_value) = v
let remove_field_fun = ref None
let register_remove_field f =
remove_field_fun := Some f
let build_model_rec (raw_model: model_element list) (term_map: Term.term Mstr.t) (model: model_files) = let build_model_rec (raw_model: model_element list) (term_map: Term.term Mstr.t) (model: model_files) =
List.fold_left (fun model raw_element -> List.fold_left (fun model raw_element ->
let raw_element_name = raw_element.me_name.men_name in let raw_element_name = raw_element.me_name.men_name in
let raw_element_value =
replace_projection
(fun x -> (recover_name term_map x).men_name)
raw_element.me_value
in
try try
( (
let t = Mstr.find raw_element_name term_map in let t = Mstr.find raw_element_name term_map in
...@@ -894,9 +896,22 @@ let build_model_rec (raw_model: model_element list) (term_map: Term.term Mstr.t) ...@@ -894,9 +896,22 @@ let build_model_rec (raw_model: model_element list) (term_map: Term.term Mstr.t)
ls.ls_name.id_string, Sattr.union attrs ls.ls_name.id_attrs ls.ls_name.id_string, Sattr.union attrs ls.ls_name.id_attrs
| _ -> "", attrs | _ -> "", attrs
in in
(* Transform value flattened by eval_match (one field record) back to
records *)
let raw_element_value = readd_one_fields ~attrs raw_element.me_value in
(* Replace projections with their real name *)
let raw_element_value =
replace_projection
(fun x -> (recover_name term_map x).men_name)
raw_element_value
in
(* Remove some specific record field related to the front-end language.
This function is registered. *)
let raw_element_value =
Opt.get_def default_remove_field !remove_field_fun raw_element_value in
let model_element = { let model_element = {
me_name = construct_name (get_model_trace_string ~name ~attrs) attrs; me_name = construct_name (get_model_trace_string ~name ~attrs) attrs;
me_value = readd_one_fields ~attrs raw_element_value; me_value = raw_element_value;
me_location = t.t_loc; me_location = t.t_loc;
me_term = Some t; me_term = Some t;
} in } in
......
...@@ -347,6 +347,8 @@ type raw_model_parser = ...@@ -347,6 +347,8 @@ type raw_model_parser =
[mel]: collected model [mel]: collected model
*) *)
val register_remove_field: (model_value -> model_value) -> unit
val register_model_parser : desc:Pp.formatted -> string -> raw_model_parser -> unit val register_model_parser : desc:Pp.formatted -> string -> raw_model_parser -> unit
val lookup_model_parser : string -> model_parser val lookup_model_parser : string -> model_parser
......
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