More projection functions for a single type.

Transformation intro_projections_counterexmp support more
projections for a single type Ty.ty. The projections can have a name
and this name is appended to the name of the function symbol or
predicate being projected.

This is useful for records - for record type, there can be a projection
for each element of the type and the name of the projection can be
the name of the element.

examples/tests/cvc4-models.mlw

@@ -3,12 +3,19 @@ module M
 
   use import int.Int
 
-  function projf (l : int) : int
+  function projf1 "model_trace:.projf1" (l : int) : int
   =
-  l+100
+  l+10
 
-  meta "inline : no" function projf
-  meta "model_projection" function projf
+  function projf2 "model_trace:projf2" (l : int) : int
+  =
+  l-10
+
+  meta "inline : no" function projf1
+  meta "model_projection" function projf1
+
+  meta "inline : no" function projf2
+  meta "model_projection" function projf2
 
   val y "model_projected" "model" "model_trace:y" :ref int
 

src/core/ident.ml

@@ -42,6 +42,51 @@ 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_trace_regexp = Str.regexp "model_trace:"
+
+let is_model_trace_label l =
+  try
+    ignore(Str.search_forward model_trace_regexp l.lab_string 0);
+    true
+  with Not_found -> false
+
+let transform_model_trace_label labels trans_fun =
+  try
+    let trace_label = Slab.choose (Slab.filter is_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 = Str.bounded_split (Str.regexp_string "@") 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 = Slab.choose (Slab.filter is_model_trace_label labels) in
+  let splitted1 = Str.bounded_split (Str.regexp_string ":") trace_label.lab_string 2 in
+  match splitted1 with
+  | [_; content] ->
+    begin
+      let splitted2 = Str.bounded_split (Str.regexp_string "@") content 2 in
+      match splitted2 with
+      | [el_name; _] -> el_name
+      | [el_name] -> el_name
+      | _ -> raise Not_found
+    end;
+  | _ -> assert false
+
+
 (** Identifiers *)
 
 type ident = {

src/core/ident.mli

@@ -27,6 +27,28 @@ val lab_hash : label -> int
 
 val create_label : string -> label
 
+(* functions for working with counterexample model labels *)
+
+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:name@context"
+    will be "model_trace:nameto_append@context."*)
+
+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 element name (there is no
+    label of the form "model_trace:+". *)
+
 (** {2 Identifiers} *)
 
 type ident = private {
@@ -107,4 +129,3 @@ val char_to_alnum : char -> string
 val char_to_lalnum : char -> string
 val char_to_alnumus : char -> string
 val char_to_lalnumus : char -> string
-

src/transform/intro_projections_counterexmp.ml

@@ -13,7 +13,7 @@ open Ident
 open Term
 open Decl
 
-(*
+
 (* Debugging functions *)
 let debug = Debug.register_info_flag "intro_projections_counterexmp"
   ~desc:"Print@ debugging@ messages@ about@ introducing@ projections@ for@ counterexamples."
@@ -30,7 +30,6 @@ let debug_decl decl =
   Pretty.print_decl Format.str_formatter decl;
   let s = Format.flush_str_formatter () in
   Debug.dprintf debug "Declaration %s @." s
-*)
 
 (* Label for terms that should be in counterexample *)
 let model_label = Ident.create_label "model"
@@ -69,13 +68,14 @@ let intro_proj_for_ls map_projs ls_projected =
   (* Returns list of declarations for projection of ls_projected
      if it has a  label "model_projected", otherwise returns [].
 
-     The declarations include:
+     There can be more projection functions for ls_projected. For
+     each projection function f the declarations include:
      - declaration of new constant with labels of ls_projected
        and label "model"
      - declaration of axiom saying that the new constant is equal to
        ls_projected projected by its projection function
 
-     The projection function for ls_declared is stored in map_projs
+     The projection functions for ls_declared are stored in map_projs
      with key ls_projected.ls_value
 
      @param map_projs maps types to projection function for these types
@@ -88,24 +88,31 @@ let intro_proj_for_ls map_projs ls_projected =
     match ls_projected.ls_value with
     | None -> []
     | Some ty_projected ->
-      (* t_proj is a term corresponding to
-         - ls_projected (the label symbol being projected) - if there is no
-	   projection function for its type
-         - application of projection function f to ls_projected  *)
-      let t_proj =
-	let t_projected = Term.t_app ls_projected [] ls_projected.ls_value in
-	try
-	  let f = Ty.Mty.find ty_projected map_projs in
-	  Term.t_app f [t_projected] f.ls_value
-	with Not_found -> t_projected in
-
-      (* introduce new constant c and axiom stating c = t_proj *)
-      let const_label = Slab.add model_label ls_projected.ls_name.id_label in
-      let const_loc = Opt.get ls_projected.ls_name.id_loc in
-      let const_name = ls_projected.ls_name.id_string^"_proj_constant" in
-      let axiom_name = ls_projected.ls_name.id_string^"_proj_axiom" in
-
-      intro_const_equal_to_term ~term:t_proj ~const_label ~const_loc ~const_name ~axiom_name
+      let introduce_constant t_proj proj_name =
+	  (* introduce new constant c and axiom stating c = t_proj  *)
+	  let const_label = Slab.add model_label ls_projected.ls_name.id_label in
+	  let const_label = append_to_model_element_name ~labels:const_label ~to_append:proj_name in
+	  let const_loc = Opt.get ls_projected.ls_name.id_loc in
+	  let const_name = ls_projected.ls_name.id_string^"_proj_constant_"^proj_name in
+	  let axiom_name = ls_projected.ls_name.id_string^"_proj_axiom_"^proj_name in
+	  intro_const_equal_to_term ~term:t_proj ~const_label ~const_loc ~const_name ~axiom_name in
+
+      let t_projected = Term.t_app ls_projected [] ls_projected.ls_value in
+      try
+	let fs = Ty.Mty.find ty_projected map_projs in
+	(* Introduce constant c for each projectin function f stating that c = f t_projected *)
+	List.fold_left
+	  (fun l f ->
+	    let proj_name =
+	      try
+		get_model_element_name ~labels:f.ls_name.id_label
+	      with Not_found -> "" in
+	    List.append l (introduce_constant (Term.t_app f [t_projected] f.ls_value) proj_name))
+	  []
+	  fs
+      with Not_found ->
+	(* There are no projection functions, introduce constant c and and axiom stating c = t_projected *)
+	introduce_constant t_projected ""
 
 let introduce_projs map_projs decl =
   match decl.d_node with
@@ -132,7 +139,13 @@ let build_projections_map projs =
   let build_map ls_proj proj_map =
     match ls_proj.ls_args with
     | [ty_proj_arg] ->
-      Ty.Mty.add ty_proj_arg ls_proj proj_map
+      let projs_for_ty =
+	try
+	  Ty.Mty.find ty_proj_arg proj_map
+	with Not_found -> []
+      in
+      let projs_for_ty = List.append projs_for_ty [ls_proj] in
+      Ty.Mty.add ty_proj_arg projs_for_ty proj_map
     | _ -> assert false
   in
   Sls.fold build_map projs Ty.Mty.empty
@@ -147,8 +160,8 @@ let intro_projections_counterexmp =
 
 let () = Trans.register_transform "intro_projections_counterexmp" intro_projections_counterexmp
   ~desc:"For@ each@ declared@ abstract@ function@ and@ predicate@ p@ with@ label@ model_projected@ \
-creates@ declaration@ of@ new@ constant@ c@ with@ label@ model@ and@ an@ axiom;@ if@ there@ exists@ \
-projection@ function@ f@ for@ p,@ the@ axiom@ is@ c = f p,@ otherwise@ it@ is@ c = p."
+and@ projectin@ funtion@ f@ for@ p@ creates@ declaration@ of@ new@ constant@ c@ with@ label@ model@ and@ an@ axiom@ \
+c = f p,@ if@ there@ is@ no@ projection@ function@ creates@ constant@ c@ and@ axiom@ c = p."
 
 (*
 Local Variables:

src/transform/intro_projections_counterexmp.mli

@@ -24,6 +24,18 @@ val intro_projections_counterexmp :  Task.task Trans.trans
     if f is tagged with meta "model_projection" and has a single argument
     of the same type as is the type of p.
 
+    Projections can be given names by labeling projection function by label
+    of the form "model_trace:proj_name".
+    If predicate p has has a label of the form "model_trace:p_name@*",
+    the constant will have a label of the form "model_trace:p_nameproj_name@*".
+    This is especially usefull when projetions are projecting record type
+    to its elements (there is one projection for every record element with
+    name ".record_element_name".
+
+    Note that in order this work, projection functions cannot be inlined.
+    If inlining transformation is performed, projection functions must
+    be marked with meta "inline : no".
+
     This transformation is needed in situations when we want to display not
     value of a variable, but value of a projection function applied to a variable.
     This is needed, e.g., in cases when the type of a variable is abstract.

src/util/util.ml

@@ -62,4 +62,3 @@ let anyd fold pr1 pr2 x =
 (* constant boolean function *)
 let ttrue _ = true
 let ffalse _ = false
-

src/whyml/mlw_wp.ml

@@ -285,23 +285,6 @@ let expl_loopvar = Slab.add Split_goal.stop_split (Slab.singleton expl_loopvar)
 
 (** Reconstruct pure values after writes *)
 
-let model_trace_regexp = Str.regexp "model_trace:"
-
-let is_model_trace_label l =
-  try
-    ignore(Str.search_forward model_trace_regexp l.lab_string 0);
-    true
-  with Not_found -> false
-
-(* Appends the string to_append to the label that begins with "model_trace:" *)
-let append_to_model_trace_label ~labels ~to_append =
-  try
-    let trace_label = Slab.choose (Slab.filter is_model_trace_label labels) in
-    let labels_without_trace = Slab.remove trace_label labels in
-    let new_trace_label = Ident.create_label (trace_label.lab_string^"@"^to_append) in
-    Slab.add new_trace_label labels_without_trace
-  with Not_found -> labels
-
 (* The counter-example model related data needed for creating new
    variable. *)
 type model_data = {
@@ -337,7 +320,7 @@ let create_model_data ?loc ?context_labels append_to_model_trace =
 
 let mk_var id ty md =
   let new_labels =
-    append_to_model_trace_label ~labels:id.id_label ~to_append:md.md_append_to_model_trace in
+    append_to_model_trace_label ~labels:id.id_label ~to_append:("@"^md.md_append_to_model_trace) in
 
   create_vsymbol (id_fresh ~label:new_labels ?loc:md.md_loc id.id_string) ty