Commit 83b74fbd authored by Sylvain Dailler's avatar Sylvain Dailler
Browse files

P718-014 Adding a label stop_intros into introduce_premises

We need to stop the transformation intro_premises to introduce variables
past a label. This allows us to keep variables in the goal (for counterex
generation) and be able to retrieve them as counterexamples.

* transform/
  changed vc_term_info so that it is not mutable anymore
  (do_intro): Removing the passing records to the do_intros calls which
may prevent us from seeing last vc_model
  (do_intro_vc_vars): adding a reference to keep the location of the vc

* transform/
  (intros): When encountering stop_intro label, the function should
stop introducing.
parent 87581293
......@@ -33,11 +33,11 @@ let model_trace_regexp = Str.regexp "model_trace:"
(* Information about the term that triggers VC. *)
type vc_term_info = {
mutable vc_inside : bool;
vc_inside : bool;
(* true if the term that triggers VC is currently processed *)
mutable vc_loc : Loc.position option;
vc_loc : Loc.position option;
(* the position of the term that triggers VC *)
mutable vc_pre_or_post : bool;
vc_pre_or_post : bool;
(* true if VC was generated for precondition or postcondition *)
......@@ -50,26 +50,23 @@ let label_starts_with regexp l =
let get_label labels regexp =
Slab.choose (Slab.filter (label_starts_with regexp) labels)
let is_model_vc_label l = if l = model_vc_label || l = model_vc_post_label then true
else false
let is_model_vc_label l = l = model_vc_label || l = model_vc_post_label
let check_enter_vc_term t info =
let check_enter_vc_term t info vc_loc =
(* Check whether the term that triggers VC is entered.
If it is entered, extract the location of the term and if the VC is
postcondition or precondition of a function, extract the name of
the corresponding function.
if Slab.exists is_model_vc_label t.t_label then begin
info.vc_inside <- true;
info.vc_loc <- t.t_loc;
info.vc_pre_or_post <- Slab.mem model_vc_post_label t.t_label;
let check_exit_vc_term t info =
(* Check whether the term triggering VC is exited. *)
if Slab.exists is_model_vc_label t.t_label then begin
info.vc_inside <- false;
if Slab.exists is_model_vc_label t.t_label then
vc_loc := t.t_loc;
{ vc_inside = true;
vc_loc = t.t_loc;
vc_pre_or_post = Slab.mem model_vc_post_label t.t_label}
let add_old lab_str =
......@@ -101,9 +98,11 @@ let model_trace_for_postcondition ~labels =
with Not_found ->
let rec do_intro info t =
check_enter_vc_term t info;
let is_counterexample_label l = l = model_label || l = model_projected_label
let rec do_intro info vc_loc t =
let info = check_enter_vc_term t info vc_loc in
let do_intro = do_intro info vc_loc in
let defs = match t.t_node with
| Tapp (ls, tl) ->
......@@ -117,8 +116,6 @@ let rec do_intro info t =
If the variable should be in counterexample, introduce new constant
in location loc with all labels necessary for collecting the it for
counterexample and make it equal to the variable *)
let is_counterexample_label l = if
l = model_label || l = model_projected_label then true else false in
if Slab.exists is_counterexample_label ls.ls_name.id_label then
let const_label = if info.vc_pre_or_post then
model_trace_for_postcondition ~labels:ls.ls_name.id_label
......@@ -135,35 +132,35 @@ let rec do_intro info t =
| _ ->
(fun defs term ->
List.append defs (do_intro info term))
List.append defs (do_intro term))
| Tbinop (_, f1, f2) ->
List.append (do_intro info f1) (do_intro info f2)
List.append (do_intro f1) (do_intro f2)
| Tquant (_, fq) ->
let _, _, f = t_open_quant fq in
do_intro info f
do_intro f
| Tlet (t, tb) ->
let _, f = t_open_bound tb in
List.append (do_intro info t) (do_intro info f)
List.append (do_intro t) (do_intro f)
| Tnot f ->
do_intro info f
do_intro f
| Tif (f1, f2, f3) ->
(List.append (do_intro info f1) (do_intro info f2))
(do_intro info f3)
(List.append (do_intro f1) (do_intro f2))
(do_intro f3)
| Tcase (t, _) ->
do_intro info t
do_intro t
(* todo: handle the second argument of Tcase *)
| _ -> [] in
check_exit_vc_term t info;
(* check_exit_vc_term t info; *)
let do_intro_vc_vars_counterexmp info pr f =
List.append (do_intro info f) [(create_prop_decl Pgoal pr f)]
let do_intro_vc_vars_counterexmp info vc_loc pr f =
List.append (do_intro info vc_loc f) [(create_prop_decl Pgoal pr f)]
let intro_vc_vars_counterexmp2 task =
let info = {
......@@ -171,14 +168,15 @@ let intro_vc_vars_counterexmp2 task =
vc_loc = None;
vc_pre_or_post = false;
} in
let vc_loc = ref None in
(* Do introduction and find location of term triggering VC *)
let do_intro_trans = Trans.goal (do_intro_vc_vars_counterexmp info) in
let do_intro_trans = Trans.goal (do_intro_vc_vars_counterexmp info vc_loc) in
let task = (Trans.apply do_intro_trans) task in
(* Pass meta with location of the term triggering VC to printer *)
let vc_loc_meta = Theory.lookup_meta "vc_location" in
let g,task = Task.task_separate_goal task in
let pos_str = match info.vc_loc with
let pos_str = match !vc_loc with
| None -> ""
| Some loc ->
let (file, line, col1, col2) = Loc.get loc in
......@@ -20,7 +20,11 @@ open Ty
open Term
open Decl
let rec intros pr f = match f.t_node with
let stop_intro = Ident.create_label "stop_intro"
let rec intros pr f =
if Slab.mem stop_intro f.t_label then [create_prop_decl Pgoal pr f] else
match f.t_node with
| Tbinop (Timplies,{ t_node = Tbinop (Tor,f2,{ t_node = Ttrue }) },_)
when Slab.mem Term.asym_label f2.t_label ->
[create_prop_decl Pgoal pr f]
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