Commit f4a22d69 authored by David Hauzar's avatar David Hauzar

Prevent loosing labels while doing eval_match.

When eval_match creates new terms from original terms, all labels of
the original terms are copied to the new terms. The exception are
labels of the form "model_trace:*". These labels are not copied if both
original terms and new terms contain this label.
parent b25b6a72
......@@ -52,12 +52,12 @@ let is_model_trace_label label =
true
with Not_found -> false
let get_model_trace_label labels =
let get_model_trace_label ~labels =
Slab.choose (Slab.filter is_model_trace_label labels)
let transform_model_trace_label labels trans_fun =
try
let trace_label = get_model_trace_label labels in
let trace_label = get_model_trace_label ~labels in
let labels_without_trace = Slab.remove trace_label labels in
let new_trace_label = create_label (trans_fun trace_label.lab_string) in
Slab.add new_trace_label labels_without_trace
......@@ -76,7 +76,7 @@ let append_to_model_trace_label ~labels ~to_append =
transform_model_trace_label labels trans
let get_model_element_name ~labels =
let trace_label = get_model_trace_label labels in
let trace_label = get_model_trace_label ~labels in
let splitted1 = Str.bounded_split (Str.regexp_string ":") trace_label.lab_string 2 in
match splitted1 with
| [_; content] ->
......
......@@ -49,6 +49,10 @@ val get_model_element_name : labels : Slab.t -> string
Throws Not_found if there is no element name (there is no
label of the form "model_trace:+". *)
val get_model_trace_label : labels : Slab.t -> Slab.elt
(** Return label of the for "model_trace:*".
Throws Not_found if there is no such label.*)
(** {2 Identifiers} *)
type ident = private {
......
......@@ -69,10 +69,10 @@ let rec print_indices fmt indices =
print_indices fmt tail
and
print_array fmt arr =
fprintf fmt "[others -> ";
fprintf fmt "(others => ";
print_model_value fmt arr.arr_others;
print_indices fmt arr.arr_indices;
fprintf fmt "]"
fprintf fmt ")"
and
print_model_value_sanit sanit_print fmt value =
(* Prints model value. *)
......
......@@ -62,6 +62,7 @@ let rec add_quant kn (vl,tl,f) v =
in
match cl with
| [ls,pjl] ->
(* there is only one constructor *)
let s = ty_match Mtv.empty (Opt.get ls.ls_value) ty in
let mk_v ty pj =
(* The name of the field corresponding to the variable that is created *)
......@@ -128,7 +129,7 @@ let eval_match ~inline kn t =
let rec eval stop env t =
let stop = stop || Slab.mem Split_goal.stop_split t.t_label in
let eval = eval stop in
match t.t_node with
let t_eval_matched = (match t.t_node with
| Tapp (ls, [t1;t2]) when ls_equal ls ps_equ ->
cs_equ kn env (eval env t1) (eval env t2)
| Tapp (ls, [t1]) when is_projection kn ls ->
......@@ -156,7 +157,18 @@ let eval_match ~inline kn t =
else List.fold_left (add_quant kn) ([],tl,f) vl in
t_quant_simp q (close (List.rev vl) tl (eval env f))
| _ ->
t_map_simp (eval env) t
t_map_simp (eval env) t) in
(* Copy all labels of t to t_eval_matched except for "model_trace:*" label.
This label is not copied if both t and t_eval_matched contain it. *)
let t =
(try
let _ = Ident.get_model_trace_label ~labels:t_eval_matched.t_label in
let original_mt_label = Ident.get_model_trace_label ~labels:t.t_label in
(* If both t_eval_matched and t contain model_trace label, remove it *)
t_label_remove original_mt_label t
with Not_found -> t) in
t_label_copy t t_eval_matched
in
eval false Mvs.empty t
......
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