Commit 2c0a5748 authored by MARCHE Claude's avatar MARCHE Claude

Improved explanations and highlighting (contributed by Astraver project:

http://linuxtesting.org/astraver)
parent 4d2f0191
......@@ -17,34 +17,45 @@ open Term
let expl_regexp = Str.regexp "expl:\\(.*\\)"
let check_expl lab acc =
let lab = lab.Ident.lab_string in
if Str.string_match expl_regexp lab 0
then Some (Str.matched_group 1 lab)
else acc
let check_expl lab = Ident.Slab.fold check_expl lab None
let rec get_expl_fmla acc f =
if f.t_ty <> None then acc else
if Ident.Slab.mem Split_goal.stop_split f.Term.t_label then acc else
let res = check_expl f.Term.t_label in
if res = None then match f.t_node with
| Term.Ttrue | Term.Tfalse | Term.Tapp _ -> acc
| Term.Tbinop (Term.Timplies,_,f) -> get_expl_fmla acc f
| Term.Tlet _ | Term.Tcase _ | Term.Tquant (Term.Tforall, _) ->
Term.t_fold get_expl_fmla acc f
| _ -> raise Exit
else if acc = None then res else raise Exit
let get_expl_fmla f = try get_expl_fmla None f with Exit -> None
let collect_expls lab =
Ident.Slab.fold
(fun lab acc ->
let lab = lab.Ident.lab_string in
if Str.string_match expl_regexp lab 0
then Str.matched_group 1 lab :: acc
else acc)
lab
[]
let concat_expls = function
| [] -> None
| [l] -> Some l
| l :: ls -> Some (l ^ " (" ^ String.concat ". " ls ^ ")")
let rec get_expls_fmla acc f =
if f.t_ty <> None then acc
else if Ident.Slab.mem Split_goal.stop_split f.Term.t_label then acc
else
let res = collect_expls f.Term.t_label in
if res = [] then match f.t_node with
| Term.Ttrue | Term.Tfalse | Term.Tapp _ -> acc
| Term.Tbinop (Term.Timplies, _, f) -> get_expls_fmla acc f
| Term.Tlet _ | Term.Tcase _ | Term.Tquant (Term.Tforall, _) ->
Term.t_fold get_expls_fmla acc f
| _ -> raise Exit
else if acc = [] then res
else raise Exit
let get_expls_fmla f = try get_expls_fmla [] f with Exit -> []
let goal_expl_task ~root task =
let gid = (Task.task_goal task).Decl.pr_name in
let info =
let fmla = Task.task_goal_fmla task in
let res = get_expl_fmla fmla in
if res <> None || not root then res else check_expl gid.Ident.id_label
let res = get_expls_fmla (Task.task_goal_fmla task) in
concat_expls
(if res <> [] && not root
then res
else collect_expls gid.Ident.id_label)
in
gid, info, task
......
......@@ -137,11 +137,19 @@ let expl_loop_keep = Ident.create_label "expl:loop invariant preservation"
let expl_loopvar = Ident.create_label "expl:loop variant decrease"
let expl_variant = Ident.create_label "expl:variant decrease"
let rec wp_expl l f = match f.t_node with
| _ when Slab.mem Split_goal.stop_split f.t_label -> t_label_add l f
| Tbinop (Tand,f1,f2) -> t_label_copy f (t_and (wp_expl l f1) (wp_expl l f2))
| Teps _ -> t_label_add l f (* post-condition, push down later *)
| _ -> f
let lab_has_expl =
let expl_regexp = Str.regexp "expl:\\(.*\\)" in
Slab.exists
(fun l ->
Str.string_match expl_regexp l.lab_string 0)
let rec wp_expl l f =
if lab_has_expl f.t_label then f
else match f.t_node with
| _ when Slab.mem Split_goal.stop_split f.t_label -> t_label_add l f
| Tbinop (Tand,f1,f2) -> t_label_copy f (t_and (wp_expl l f1) (wp_expl l f2))
| Teps _ -> t_label_add l f (* post-condition, push down later *)
| _ -> f
let wp_and ~sym f1 f2 =
if sym then t_and_simp f1 f2 else t_and_asym_simp f1 f2
......@@ -946,14 +954,19 @@ let rec unabsurd f = match f.t_node with
let add_wp_decl km name f uc =
(* prepare a proposition symbol *)
let s = "WP_parameter " ^ name.id_string in
(* set a proper explanation *)
let n =
try let _,_,l = restore_path name in
String.concat "." l
with Not_found -> name.id_string
let label =
let label = name.id_label in
if lab_has_expl label then label
else
(* set a proper explanation *)
let n =
try let _, _, l = restore_path name in
String.concat "." l
with Not_found -> name.id_string
in
let lab = Ident.create_label ("expl:VC for " ^ n) in
Slab.add lab label
in
let lab = Ident.create_label ("expl:VC for " ^ n) in
let label = Slab.add lab name.id_label in
let id = id_fresh ~label ?loc:name.id_loc s in
let pr = create_prsymbol id in
(* prepare the VC formula *)
......
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