Commit c61edffe authored by Sylvain Dailler's avatar Sylvain Dailler

Allow having a function that adapts counterexamples after parsing.

parent 8ab7b281
......@@ -284,7 +284,7 @@ let convert_to_model_element name t =
let value = convert_to_model_value t in
Model_parser.create_model_element ~name ~value ()
let apply_to_record (list_records: (string list) Mstr.t) (t: term) =
let default_apply_to_record (list_records: (string list) Mstr.t) (t: term) =
let rec array_apply_to_record (a: array) =
match a with
......@@ -325,6 +325,16 @@ let apply_to_record (list_records: (string list) Mstr.t) (t: term) =
in
apply_to_record t
let apply_to_records_ref = ref None
let register_apply_to_records f =
apply_to_records_ref := Some f
let apply_to_record list_records t =
match !apply_to_records_ref with
| None -> default_apply_to_record list_records t
| Some f -> f list_records t
let definition_apply_to_record list_records d =
match d with
| Function (lt, t) ->
......
......@@ -13,6 +13,17 @@
val print_table:
Smt2_model_defs.correspondence_table -> unit
(* This allows registering a transformation of counterexamples terms. It allows
to convert Apply(s, t) into appropriate counterexample datatypes. For
example, an unconstrained array that was translated from an high-level
language to a why3 record can be recognized in this function and be
translated back to an array (based on the name of its fields.
This function has the information of the records that were saved.
*)
val register_apply_to_records:
((string list) Stdlib.Mstr.t -> Smt2_model_defs.term -> Smt2_model_defs.term) ->
unit
(* From the table generated by the parser, build a list of model_element *)
val create_list:
Stdlib.Sstr.t -> ((string * string) list) Stdlib.Mstr.t -> Smt2_model_defs.correspondence_table ->
......
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