prevent new transformation split_intros_goal_wp from removing too many variables

the variables labelled with "model" are kept, so as to produce better
counterexamples

also: declaration of labels grouped together in Ident module

src/core/ident.ml

@@ -42,82 +42,6 @@ let lab_equal : label -> label -> bool = (==)
 let lab_hash lab = lab.lab_tag
 let lab_compare l1 l2 = Pervasives.compare l1.lab_tag l2.lab_tag
 
-(* functions for working with counterexample model labels *)
-
-let model_proj_label = create_label "model_projected"
-let model_label = create_label "model"
-
-let remove_model_labels ~labels =
-  Slab.filter (fun l -> (l <> model_label) && (l <> model_proj_label) ) labels
-
-let is_model_trace_label label =
-  Strings.has_prefix "model_trace:" label.lab_string
-
-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 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
-  with Not_found -> labels
-
-let append_to_model_element_name ~labels ~to_append =
-  let trans lab_str =
-    let splitted = Strings.bounded_split '@' lab_str 2 in
-    match splitted with
-    | [before; after] -> before ^ to_append ^ "@" ^ after
-    | _ -> lab_str^to_append in
-  transform_model_trace_label labels trans
-
-let append_to_model_trace_label ~labels ~to_append =
-    let trans lab_str = lab_str ^ to_append in
-    transform_model_trace_label labels trans
-
-let get_model_element_name ~labels =
-  let trace_label = get_model_trace_label ~labels in
-  let splitted1 = Strings.bounded_split ':' trace_label.lab_string 2 in
-  match splitted1 with
-  | [_; content] ->
-    begin
-      let splitted2 = Strings.bounded_split '@' content 2 in
-      match splitted2 with
-      | [el_name; _] -> el_name
-      | [el_name] -> el_name
-      | _ -> raise Not_found
-    end;
-  | [_] -> ""
-  | _ -> assert false
-
-let get_model_trace_string ~labels =
-  let tl = get_model_trace_label ~labels in
-  let splitted = Strings.bounded_split ':' tl.lab_string 2 in
-  match splitted with
-  | [_; t_str] -> t_str
-  | _ -> ""
-
-(* Functions for working with ITP labels *)
-
-let is_name_label label =
-  Strings.has_prefix "name:" label.lab_string
-
-let get_name_label ~labels =
-  try Some (Slab.choose (Slab.filter is_name_label labels))
-  with Not_found -> None
-
-let get_element_name ~labels =
-  match get_name_label ~labels with
-  | None -> None
-  | Some name_label ->
-    let splitted1 = Strings.bounded_split ':' name_label.lab_string 2 in
-    let correct_word = Str.regexp "^\\([A-Za-z]+\\)\\([A-Za-z0-9_']*\\)$" in
-    match splitted1 with
-    | ["name"; content] when Str.string_match correct_word content 0 ->
-        Some content
-    | _ -> None
-
 (** Naming convention *)
 
 let infix  s = "infix "  ^ s
@@ -270,21 +194,6 @@ let id_unique printer ?(sanitizer = same) id =
     Hid.replace printer.values id name;
     name
 
-let id_unique_label printer ?(sanitizer = same) id =
-  try
-    Hid.find printer.values id
-  with Not_found ->
-    let labels = id.id_label in
-    let name =
-      match (get_element_name ~labels) with
-      | Some x -> x
-      | None -> printer.sanitizer id.id_string
-    in
-    let name = sanitizer name in
-    let name = find_unique printer.indices name in
-    Hid.replace printer.values id name;
-    name
-
 let string_unique printer s = find_unique printer.indices s
 
 let forget_id printer id =
@@ -345,3 +254,99 @@ let sanitizer' head rest last n =
   String.concat "" (List.rev !lst)
 
 let sanitizer head rest n = sanitizer' head rest rest n
+
+
+
+(** {2 functions for working with counterexample model labels} *)
+
+let model_label = create_label "model"
+
+let has_model_label id = Slab.mem model_label id.id_label
+
+let model_proj_label = create_label "model_projected"
+
+let remove_model_labels ~labels =
+  Slab.filter (fun l -> (l <> model_label) && (l <> model_proj_label) ) labels
+
+let is_model_trace_label label =
+  Strings.has_prefix "model_trace:" label.lab_string
+
+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 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
+  with Not_found -> labels
+
+let append_to_model_element_name ~labels ~to_append =
+  let trans lab_str =
+    let splitted = Strings.bounded_split '@' lab_str 2 in
+    match splitted with
+    | [before; after] -> before ^ to_append ^ "@" ^ after
+    | _ -> lab_str^to_append in
+  transform_model_trace_label labels trans
+
+let append_to_model_trace_label ~labels ~to_append =
+    let trans lab_str = lab_str ^ to_append in
+    transform_model_trace_label labels trans
+
+let get_model_element_name ~labels =
+  let trace_label = get_model_trace_label ~labels in
+  let splitted1 = Strings.bounded_split ':' trace_label.lab_string 2 in
+  match splitted1 with
+  | [_; content] ->
+    begin
+      let splitted2 = Strings.bounded_split '@' content 2 in
+      match splitted2 with
+      | [el_name; _] -> el_name
+      | [el_name] -> el_name
+      | _ -> raise Not_found
+    end;
+  | [_] -> ""
+  | _ -> assert false
+
+let get_model_trace_string ~labels =
+  let tl = get_model_trace_label ~labels in
+  let splitted = Strings.bounded_split ':' tl.lab_string 2 in
+  match splitted with
+  | [_; t_str] -> t_str
+  | _ -> ""
+
+(* Functions for working with ITP labels *)
+
+let is_name_label label =
+  Strings.has_prefix "name:" label.lab_string
+
+let get_name_label ~labels =
+  try Some (Slab.choose (Slab.filter is_name_label labels))
+  with Not_found -> None
+
+let get_element_name ~labels =
+  match get_name_label ~labels with
+  | None -> None
+  | Some name_label ->
+    let splitted1 = Strings.bounded_split ':' name_label.lab_string 2 in
+    let correct_word = Str.regexp "^\\([A-Za-z]+\\)\\([A-Za-z0-9_']*\\)$" in
+    match splitted1 with
+    | ["name"; content] when Str.string_match correct_word content 0 ->
+        Some content
+    | _ -> None
+
+let id_unique_label printer ?(sanitizer = same) id =
+  try
+    Hid.find printer.values id
+  with Not_found ->
+    let labels = id.id_label in
+    let name =
+      match (get_element_name ~labels) with
+      | Some x -> x
+      | None -> printer.sanitizer id.id_string
+    in
+    let name = sanitizer name in
+    let name = find_unique printer.indices name in
+    Hid.replace printer.values id name;
+    name

src/core/ident.mli

@@ -27,39 +27,6 @@ val lab_hash : label -> int
 
 val create_label : string -> label
 
-(* functions for working with counterexample model labels *)
-
-val remove_model_labels : labels : Slab.t -> Slab.t
-(** Returns a copy of labels without labels ["model"] and ["model_projected"]. *)
-
-val append_to_model_trace_label : labels : Slab.t ->
-  to_append : string ->
-  Slab.t
-(** The returned set of labels will contain the same set of labels
-    as argument labels except that a label of the form ["model_trace:*"]
-    will be ["model_trace:*to_append"]. *)
-
-val append_to_model_element_name : labels : Slab.t ->
-  to_append : string ->
-  Slab.t
-(** The returned set of labels will contain the same set of labels
-    as argument labels except that a label of the form ["model_trace:*@*"]
-    will be ["model_trace:*to_append@*"]. *)
-
-val get_model_element_name : labels : Slab.t -> string
-(** If labels contain a label of the form ["model_trace:name@*"],
-    return ["name"].
-    Throws [Not_found] if there is no label of the form ["model_trace:*"]. *)
-
-val get_model_trace_string : labels : Slab.t -> string
-(** If labels contain a label of the form ["model_trace:mt_string"],
-    return ["mt_string"].
-    Throws [Not_found] if there is no label of the form ["model_trace:*"]. *)
-
-val get_model_trace_label : labels : Slab.t -> Slab.elt
-(** Return a label of the form ["model_trace:*"].
-    Throws [Not_found] if there is no such label. *)
-
 (** {2 Naming convention } *)
 
 val infix: string -> string
@@ -135,11 +102,6 @@ val id_unique :
 (** use ident_printer to generate a unique name for ident
     an optional sanitizer is applied over the printer's sanitizer *)
 
-val id_unique_label :
-  ident_printer -> ?sanitizer : (string -> string) -> ident -> string
-(** Do the same as id_unique except that it tries first to
-   use the "name:" label to generate the name instead of id.id_string *)
-
 val string_unique : ident_printer -> string -> string
 (** Uniquify string *)
 
@@ -168,3 +130,50 @@ val char_to_alnum : char -> string
 val char_to_lalnum : char -> string
 val char_to_alnumus : char -> string
 val char_to_lalnumus : char -> string
+
+
+(** {2 Name handling for ITP} *)
+
+val id_unique_label :
+  ident_printer -> ?sanitizer : (string -> string) -> ident -> string
+(** Do the same as id_unique except that it tries first to
+   use the "name:" label to generate the name instead of id.id_string *)
+
+
+
+(** {2 labels for handling counterexamples} *)
+
+val model_label: label
+
+val has_model_label: ident -> bool
+
+val remove_model_labels : labels : Slab.t -> Slab.t
+(** Returns a copy of labels without labels ["model"] and ["model_projected"]. *)
+
+val append_to_model_trace_label : labels : Slab.t ->
+  to_append : string ->
+  Slab.t
+(** The returned set of labels will contain the same set of labels
+    as argument labels except that a label of the form ["model_trace:*"]
+    will be ["model_trace:*to_append"]. *)
+
+val append_to_model_element_name : labels : Slab.t ->
+  to_append : string ->
+  Slab.t
+(** The returned set of labels will contain the same set of labels
+    as argument labels except that a label of the form ["model_trace:*@*"]
+    will be ["model_trace:*to_append@*"]. *)
+
+val get_model_element_name : labels : Slab.t -> string
+(** If labels contain a label of the form ["model_trace:name@*"],
+    return ["name"].
+    Throws [Not_found] if there is no label of the form ["model_trace:*"]. *)
+
+val get_model_trace_string : labels : Slab.t -> string
+(** If labels contain a label of the form ["model_trace:mt_string"],
+    return ["mt_string"].
+    Throws [Not_found] if there is no label of the form ["model_trace:*"]. *)
+
+val get_model_trace_label : labels : Slab.t -> Slab.elt
+(** Return a label of the form ["model_trace:*"].
+    Throws [Not_found] if there is no such label. *)

src/printer/cntexmp_printer.ml

@@ -71,8 +71,10 @@ let get_label labels regexp =
 let print_label fmt l =
   fprintf fmt "\"%s\"" l.lab_string
 
+(* already in Ident
 let model_label = Ident.create_label "model"
   (* This label identifies terms that should be in counter-example. *)
+ *)
 let model_vc_term_label = Ident.create_label "model_vc"
   (* This label identifies the term that triggers the VC. *)
 let model_projection = Ident.create_label "model_projection"

src/printer/cntexmp_printer.mli

@@ -40,8 +40,6 @@ val get_label: unit Ident.Mlab.t -> Str.regexp -> Ident.label
 
 val print_label: Format.formatter -> Ident.label -> unit
 
-val model_label: Ident.label
-
 val model_projection: Ident.label
 
 val model_vc_term_label: Ident.label

src/transform/eliminate_inductive.ml

@@ -40,7 +40,9 @@ let inv acc (ps,al) =
   let tl = List.map t_var vl in
   let hd = ps_app ps tl in
   let dj = Lists.map_join_left (exi tl) t_or al in
-  let hsdj = Simplify_formula.fmla_remove_quant (t_implies hd dj) in
+  let hsdj =
+    Simplify_formula.fmla_remove_quant ~keep_model_vars:false (t_implies hd dj)
+  in
   let ax = t_forall_close vl [] hsdj in
   let nm = id_derive (ps.ls_name.id_string ^ "_inversion") ps.ls_name in
   create_prop_decl Paxiom (create_prsymbol nm) ax :: acc

src/transform/intro_projections_counterexmp.ml

@@ -63,7 +63,8 @@ let debug_decl decl =
 *)
 
 (* Label for terms that should be in counterexample *)
-let model_label = Ident.create_label "model"
+(* already in Ident
+   let model_label = Ident.create_label "model" *)
 (* Label for terms that should be projected in counterexample *)
 let model_proj_label = Ident.create_label "model_projected"
 

src/transform/intro_vc_vars_counterexmp.ml

@@ -22,8 +22,10 @@ let meta_vc_location =
   Theory.register_meta_excl "vc_location" [Theory.MTstring]
   ~desc:"Location@ of@ the@ term@ that@ triggers@ vc@ in@ the@ form@ file:line:col."
 
-let model_label = Ident.create_label "model"
+(* let model_label = Ident.create_label "model"
+  already in Ident
   (* Identifies terms that should be in counterexample and should not be projected. *)
+ *)
 let model_projected_label = Ident.create_label "model_projected"
   (* Identifies terms that should be in counterexample and should be projected. *)
 let model_vc_label = Ident.create_label "model_vc"

src/transform/introduction.ml

@@ -108,7 +108,7 @@ let () = Trans.register_transform
 
 
 let simplify_intros =
-  Trans.compose Simplify_formula.simplify_trivial_quantification introduce_premises
+  Trans.compose Simplify_formula.simplify_trivial_wp_quantification introduce_premises
 
 let split_intros_goal_wp =
   Trans.compose_l Split_goal.split_goal_right (Trans.singleton simplify_intros)
@@ -124,7 +124,7 @@ let () = Trans.register_transform_l
            ~desc:"The@ recommended@ splitting@ transformation@ to@ apply@ on@ VCs@ generated@ by@ WP@ (split_goal_right@ followed@ by@ simplify_trivial_quantifications@ followed@ by@ introduce_premises)."
 
 let () = Trans.register_transform_l
-           "split_intros_intros_all_wp" split_intros_all_wp
+           "split_intros_all_wp" split_intros_all_wp
            ~desc:"Same@ as@ split_intros_goal_wp,@ but@ also@ split@ premises."
 
 let () = Trans.register_transform

src/transform/simplify_formula.ml

@@ -108,10 +108,13 @@ let rec equ_simp f = t_label_copy f (match f.t_node with
        t_equ_simp (equ_simp f1) (equ_simp f2)
   | _ -> t_map equ_simp f)
 
-let rec fmla_quant sign f = function
+let rec fmla_quant ~keep_model_vars sign f = function
   | [] -> [], f
   | vs::l ->
-      let vsl, f = fmla_quant sign f l in
+     let vsl, f = fmla_quant ~keep_model_vars sign f l in
+     if keep_model_vars && has_model_label vs.vs_name then
+       vs::vsl, f
+     else
       try
         fmla_find_subst (Svs.singleton vs) vs sign f;
         vs::vsl, f
@@ -119,7 +122,7 @@ let rec fmla_quant sign f = function
         let f = t_subst_single vs t f in
         vsl, equ_simp f
 
-let rec fmla_remove_quant f =
+let rec fmla_remove_quant ~keep_model_vars f =
   match f.t_node with
     | Tquant (k,fb) ->
         let vsl,trl,f',close = t_open_quant_cb fb in
@@ -128,10 +131,10 @@ let rec fmla_remove_quant f =
           else
             let sign = match k with
               | Tforall -> false | Texists -> true in
-            let vsl, f' = fmla_quant sign f' vsl in
-            let f' = fmla_remove_quant f' in
+            let vsl, f' = fmla_quant ~keep_model_vars sign f' vsl in
+            let f' = fmla_remove_quant ~keep_model_vars f' in
             t_quant k (close vsl [] f')
-    | _ -> Term.t_map fmla_remove_quant f
+    | _ -> Term.t_map (fmla_remove_quant ~keep_model_vars) f
 
 (*let fmla_remove_quant f =
   Format.eprintf "@[<hov>%a =>|@\n" Pretty.print_fmla f;
@@ -142,7 +145,10 @@ let rec fmla_remove_quant f =
 *)
 
 let simplify_trivial_quantification =
-  Trans.rewrite fmla_remove_quant None
+  Trans.rewrite (fmla_remove_quant ~keep_model_vars:false) None
+
+let simplify_trivial_wp_quantification =
+  Trans.rewrite (fmla_remove_quant ~keep_model_vars:true) None
 
 let () = Trans.register_transform
   "simplify_trivial_quantification" simplify_trivial_quantification
@@ -152,7 +158,9 @@ let () = Trans.register_transform
      - @[transform \\forall x. x <> y \\/ F@ into F[y/x].@]@]"
 
 let simplify_trivial_quantification_in_goal =
-  Trans.goal (fun pr f -> [create_prop_decl Pgoal pr (fmla_remove_quant f)])
+  Trans.goal
+    (fun pr f ->
+     [create_prop_decl Pgoal pr (fmla_remove_quant ~keep_model_vars:false f)])
 
 let () = Trans.register_transform
   "simplify_trivial_quantification_in_goal"

src/transform/simplify_formula.mli

@@ -14,12 +14,20 @@ val fmla_simpl : Term.term -> Term.term
 val simplify_formula :  Task.task Trans.trans
 val simplify_formula_and_task :  Task.task list Trans.trans
 
-val fmla_remove_quant : Term.term -> Term.term
+val fmla_remove_quant : keep_model_vars:bool -> Term.term -> Term.term
 (** transforms \exists x. x == y /\ F into F[y/x]
-    and \forall x. x <> y \/ F into F[y/x] *)
+    and \forall x. x <> y \/ F into F[y/x]
+
+    if [keep_model_vars] is true, then variables that hold a label for
+    counterexamples are always kept.
+ *)
 
 val simplify_trivial_quantification : Task.task Trans.trans
 
+val simplify_trivial_wp_quantification : Task.task Trans.trans
+(** same as [simplify_trivial_quantification] but keep variables that
+    hold a counterexample label *)
+
 val fmla_cond_subst: (Term.term -> Term.term -> bool) -> Term.term -> Term.term
 (** given a formula [f] containing some equality or disequality [t1] ?= [t2]
     such that [filter t1 t2] (resp [filter t2 t1]) evaluates to true,