Commit f951a6b3 authored by David Hauzar's avatar David Hauzar

Passing terms corresponding to counter-example elelements in counter-example model.

parent 753e8d0d
......@@ -71,14 +71,16 @@ print_model_value fmt value =
type model_element = {
me_name : string;
me_value : model_value;
me_location : Loc.position option;
me_location : Loc.position option;
me_term : Term.term option;
}
let create_model_element ~name ~value ~location =
let create_model_element ~name ~value ?location ?term () =
{
me_name = name;
me_value = value;
me_location = location;
me_term = term;
}
let print_location fmt m_element =
......
......@@ -53,19 +53,25 @@ type model_element = {
(** Counter-example value for the element. *)
me_location : Loc.position option;
(** Source-code location of the element. *)
me_term : Term.term option;
(** Why term corresponding to the element. *)
}
val create_model_element :
name : string ->
value : model_value ->
location : Loc.position option ->
?location : Loc.position ->
?term : Term.term ->
unit ->
model_element
(** Creates a counter-example model element.
@param name : the name of the source-code element
@param value : counter-example value for the element
@param location : source-code location of the element *)
@param location : source-code location of the element
@param term : why term corresponding to the element *)
val print_model : Format.formatter -> model_element list -> unit
......
......@@ -52,11 +52,11 @@ let rec update_element_names_and_locations raw_model terms updated_model =
match raw_model with
| [] -> updated_model
| model_element::raw_strings_tail ->
let (element_name, element_location, terms_tail) = match terms with
| [] -> (model_element.me_name, None, [])
| term::t_tail -> ((get_element_name term model_element.me_name), term.t_loc, t_tail) in
let (element_name, element_location, element_term, terms_tail) = match terms with
| [] -> (model_element.me_name, None, None, [])
| term::t_tail -> ((get_element_name term model_element.me_name), term.t_loc, Some term, t_tail) in
let new_model_element = create_model_element
~name:element_name ~value:model_element.me_value ~location:element_location in
~name:element_name ~value:model_element.me_value ?location:element_location ?term:element_term () in
let updated_model = updated_model @ [new_model_element] in
update_element_names_and_locations raw_strings_tail terms_tail updated_model
......
......@@ -21,7 +21,7 @@ output:
pairs:
| possible_space { [] }
| possible_space LPAREN term SPACE value RPAREN pairs
{ (Model_parser.create_model_element ~name:$3 ~value:$5 ~location:None)::$7 }
{ (Model_parser.create_model_element ~name:$3 ~value:$5 ())::$7 }
possible_space:
| { "" }
......
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