Commit b25b6a72 authored by David Hauzar's avatar David Hauzar
Browse files

Traceability for record field names in counterexamples.

In wp, eval_match is used to replace record fields with simple variables
of the same type. Originally, all labels from the variable that field
was accessed were copied to new variables representing fields of this
variable. Therefore also "model_trace:var_name" label was copied and thus
the field had name "var_name" in the counterexample.

This commit solves this problem by appending names of the fields to
"model_trace:*" label of new variables representing record fields.
parent a330453c
...@@ -53,7 +53,7 @@ module M ...@@ -53,7 +53,7 @@ module M
(*** In all cases, records are decomposed using match eval ***) (*** In all cases, records are decomposed using match eval ***)
type r = {f "field_f" :int; g:bool} type r = {f "model_trace:field_f" :int; g:bool}
(* Projection functions *) (* Projection functions *)
function projf_r_f "model_trace:.f" (x : r) : int function projf_r_f "model_trace:.f" (x : r) : int
......
...@@ -603,4 +603,3 @@ let () = Exn_printer.register ...@@ -603,4 +603,3 @@ let () = Exn_printer.register
fprintf fmt "Cannot prove the termination of %a" print_ls ls fprintf fmt "Cannot prove the termination of %a" print_ls ls
| _ -> raise exn | _ -> raise exn
end end
...@@ -64,4 +64,3 @@ val print_task : formatter -> task -> unit ...@@ -64,4 +64,3 @@ val print_task : formatter -> task -> unit
val print_theory : formatter -> theory -> unit val print_theory : formatter -> theory -> unit
val print_namespace : formatter -> string -> theory -> unit val print_namespace : formatter -> string -> theory -> unit
...@@ -61,10 +61,24 @@ let rec add_quant kn (vl,tl,f) v = ...@@ -61,10 +61,24 @@ let rec add_quant kn (vl,tl,f) v =
| _ -> [] | _ -> []
in in
match cl with match cl with
| [ls,_] -> | [ls,pjl] ->
let s = ty_match Mtv.empty (Opt.get ls.ls_value) ty in let s = ty_match Mtv.empty (Opt.get ls.ls_value) ty in
let mk_v ty = create_vsymbol (id_clone v.vs_name) (ty_inst s ty) in let mk_v ty pj =
let nvl = List.map mk_v ls.ls_args in (* The name of the field corresponding to the variable that is created *)
let field_name = begin match pj with
| Some pj_ls ->
begin
try
Ident.get_model_element_name ~labels:pj_ls.ls_name.id_label
with Not_found -> pj_ls.ls_name.id_string
end
| _ -> ""
end in
let label = Ident.append_to_model_element_name
~labels:v.vs_name.id_label ~to_append:("." ^ field_name) in
create_vsymbol (id_clone ~label v.vs_name) (ty_inst s ty) in
let nvl = List.map2 mk_v ls.ls_args pjl in
let t = fs_app ls (List.map t_var nvl) ty in let t = fs_app ls (List.map t_var nvl) ty in
let f = t_let_close_simp v t f in let f = t_let_close_simp v t f in
let tl = tr_map (t_subst_single v t) tl in let tl = tr_map (t_subst_single v t) tl in
...@@ -114,7 +128,7 @@ let eval_match ~inline kn t = ...@@ -114,7 +128,7 @@ let eval_match ~inline kn t =
let rec eval stop env t = let rec eval stop env t =
let stop = stop || Slab.mem Split_goal.stop_split t.t_label in let stop = stop || Slab.mem Split_goal.stop_split t.t_label in
let eval = eval stop in let eval = eval stop in
t_label_copy t (match t.t_node with match t.t_node with
| Tapp (ls, [t1;t2]) when ls_equal ls ps_equ -> | Tapp (ls, [t1;t2]) when ls_equal ls ps_equ ->
cs_equ kn env (eval env t1) (eval env t2) cs_equ kn env (eval env t1) (eval env t2)
| Tapp (ls, [t1]) when is_projection kn ls -> | Tapp (ls, [t1]) when is_projection kn ls ->
...@@ -142,7 +156,7 @@ let eval_match ~inline kn t = ...@@ -142,7 +156,7 @@ let eval_match ~inline kn t =
else List.fold_left (add_quant kn) ([],tl,f) vl in else List.fold_left (add_quant kn) ([],tl,f) vl in
t_quant_simp q (close (List.rev vl) tl (eval env f)) 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 in
eval false Mvs.empty t 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