235 issue

src/core/ident.ml

@@ -339,6 +339,8 @@ let sanitizer head rest n = sanitizer' head rest rest n
 
 (** {2 functions for working with counterexample attributes} *)
 
+let proxy_attr = create_attribute "mlw:proxy_symbol"
+
 let model_projected_attr = create_attribute "model_projected"
 let model_vc_attr = create_attribute "model_vc"
 let model_vc_post_attr = create_attribute "model_vc_post"

src/core/ident.mli

@@ -165,10 +165,11 @@ val id_unique_attr :
 (** Do the same as id_unique except that it tries first to use
     the "name:" attribute to generate the name instead of id.id_string *)
 
+val proxy_attr: attribute
+
 (** {2 Attributes for handling counterexamples} *)
 
 val model_projected_attr : attribute
-
 val model_vc_attr : attribute
 val model_vc_post_attr : attribute
 val model_vc_havoc_attr : attribute

src/mlw/compile.ml

@@ -642,7 +642,7 @@ module Transform = struct
     | Evar pv -> begin try Mpv.find pv subst, Spv.singleton pv
         with Not_found -> e, Spv.empty end
     | Elet (Lvar (pv, ({e_effect = eff1} as e1)), e2)
-      when Sattr.mem Expr.proxy_attr pv.pv_vs.vs_name.id_attrs &&
+      when Sattr.mem proxy_attr pv.pv_vs.vs_name.id_attrs &&
            eff_pure eff1 &&
            can_inline e1 e2 ->
         let e1, s1 = expr info subst e1 in

src/mlw/expr.ml

@@ -372,7 +372,6 @@ let e_attr_copy { e_attrs = attrs; e_loc = loc } e =
   let loc = if e.e_loc = None then loc else e.e_loc in
   { e with e_attrs = attrs; e_loc = loc }
 
-let proxy_attr = create_attribute "mlw:proxy_symbol"
 let proxy_attrs = Sattr.singleton proxy_attr
 
 let rec e_attr_push ?loc l e = match e.e_node with

src/mlw/expr.mli

@@ -258,8 +258,6 @@ val e_locate_effect : (effect -> bool) -> expr -> Loc.position option
 (** [e_locate_effect pr e] looks for a minimal sub-expression of
     [e] whose effect satisfies [pr] and returns its location *)
 
-val proxy_attr : attribute
-
 val e_rs_subst : rsymbol Mrs.t -> expr -> expr
 val c_rs_subst : rsymbol Mrs.t -> cexp -> cexp
 

src/transform/introduction.ml

@@ -293,7 +293,7 @@ let subst_filter ls =
 
 let simplify_intros =
   Trans.compose introduce_premises
-                (Subst.subst_filtered subst_filter)
+                (Subst.subst_filtered ~subst_to_proxy:false subst_filter)
 
 let split_vc =
   Trans.compose_l

src/transform/subst.ml

@@ -9,6 +9,7 @@
 (*                                                                  *)
 (********************************************************************)
 
+open Ident
 open Term
 open Decl
 open Theory
@@ -133,8 +134,8 @@ let apply_subst ((prs,sigma) : (Spr.t * term Mls.t)) (tdl:Theory.tdecl list) : T
                     aux (td::urg) rem tuc postponed
                 | exception (NoTerminationProof _) ->
                     let urg = List.fold_right (fun (ls,ld) urg ->
-                      let nm = ls.ls_name.Ident.id_string ^ "'def" in
-                      let pr = create_prsymbol (Ident.id_fresh nm) in
+                      let nm = ls.ls_name.id_string ^ "'def" in
+                      let pr = create_prsymbol (id_fresh nm) in
                       let f = ls_defn_axiom ld in
                       let d = create_prop_decl Paxiom pr f in
                       Theory.create_decl d :: urg) ld' urg
@@ -170,8 +171,15 @@ let rec occurs_in_term ls t =
   | Tapp(ls',[]) when ls_equal ls' ls -> true
   | _ -> t_any (occurs_in_term ls) t
 
-(* [find_equalities filter t] searches in task [t] for equalities of
-   the form constant = term or term = constant, where constant does
+(* [true] if [t] is exactly a proxy symbol *)
+let is_proxy t =
+  match t.t_node with
+  | Tapp (ls, []) ->
+      Sattr.exists (fun a -> attr_equal a proxy_attr) ls.ls_name.id_attrs
+  | _ -> false
+
+(* [find_equalities subst_to_proxy filter t] searches in task [t] for equalities
+   of the form constant = term or term = constant, where constant does
    not occur in the term.  That function returns first the set of
    prsymbols for the equalities found, and second a map from the
    lsymbols of the constant to the associated term. That map is
@@ -181,12 +189,15 @@ let rec occurs_in_term ls t =
    function applys a generic filter to the constants that can be taken
    into consideration.  if several equalities occur for the same
    constant, the first one is considered.
+   [subst_to_proxy]: If false, we don't register equalities which are a direct
+   substitution to a proxy variable (from a non-proxy variable).
  *)
-let find_equalities filter =
-  let valid ls =
+let find_equalities ~subst_to_proxy filter =
+  let valid ls t2 =
     ls.ls_args = [] && ls.ls_constr = 0 && ls.ls_value <> None &&
     List.for_all Ty.ty_closed (Ty.oty_cons ls.ls_args ls.ls_value) &&
-    filter ls
+    filter ls &&
+    (subst_to_proxy || is_proxy (t_app_infer ls []) || not (is_proxy t2))
   in
   let select ls t sigma =
     let () = Debug.dprintf debug_subst "selected: %a -> %a@."
@@ -206,7 +217,7 @@ let find_equalities filter =
              begin
                try match t1.t_node with
                | Tapp (ls, []) when
-                      valid ls &&
+                      valid ls t2 &&
                         not (Mls.mem ls sigma) ->
                   let t2' = subst_in_term sigma t2 in
                   if occurs_in_term ls t2' then raise Exit
@@ -215,7 +226,7 @@ let find_equalities filter =
                with Exit ->
                     match t2.t_node with
                     | Tapp (ls, []) when
-                           valid ls &&
+                           valid ls t1 &&
                              not (Mls.mem ls sigma) ->
                        let t1' = subst_in_term sigma t1 in
                        if occurs_in_term ls t1' then acc
@@ -227,8 +238,8 @@ let find_equalities filter =
      | Dlogic ld ->
         List.fold_left
           (fun ((prs,sigma) as acc) (ls,ld) ->
-           if valid ls && not (Mls.mem ls sigma) then
-             let _, t = open_ls_defn ld in
+           let _, t = open_ls_defn ld in
+           if valid ls t && not (Mls.mem ls sigma) then
              let t' = subst_in_term sigma t in
              if occurs_in_term ls t' then acc
              else (prs, select ls t' sigma)
@@ -244,11 +255,11 @@ let get_decls =
 let apply_subst x t =
   apply_subst x (List.rev (Trans.apply get_decls t))
 
-let subst_filtered filter =
-  Trans.bind (find_equalities filter)
+let subst_filtered ~subst_to_proxy filter =
+  Trans.bind (find_equalities ~subst_to_proxy filter)
              (fun x -> Trans.store (apply_subst x))
 
-let subst_all = subst_filtered (fun _ -> true)
+let subst_all = subst_filtered ~subst_to_proxy:false (fun _ -> true)
 
 let () =
   wrap_and_register ~desc:"substitutes with all equalities between a constant and a term"
@@ -263,7 +274,7 @@ let subst tl =
        | Tapp (ls, []) -> Sls.add ls acc
        | _ -> raise (Arg_trans "subst: %a is not a constant")) Sls.empty tl
   in
-  subst_filtered (fun ls -> Sls.mem ls to_subst)
+  subst_filtered ~subst_to_proxy:true (fun ls -> Sls.mem ls to_subst)
 
 let () =
   wrap_and_register ~desc:"substitutes with all equalities involving one of the given constants"

src/transform/subst.mli

@@ -9,7 +9,12 @@
 (*                                                                  *)
 (********************************************************************)
 
-val subst_filtered : (Term.lsymbol -> bool) -> Task.task Trans.trans
+val subst_filtered : subst_to_proxy:bool ->
+  (Term.lsymbol -> bool) -> Task.task Trans.trans
+(* [subst_filtered subst_to_proxy p]: substitute only lsymbol chosen by [p].
+   If [subst_to_proxy] is true, allow the substitution from normal symbols to
+   proxy symbols.
+*)
 
 val subst : Term.term list -> Task.task Trans.trans