[WP] Cint simplifier is reusing e_subst API

src/plugins/wp/Cint.ml

@@ -1449,24 +1449,6 @@ let mask_simplifier =
       r
 
   end in
-  let unary_op e f rewrite a = (* requires [e==f a] *)
-    (* reuse the previous term when not rewritten *)
-    let a' = rewrite a in if a'==a then e else f a'
-  in
-  let bin_op e f rewrite a b = (* requires [e==f a b] *)
-    (* reuse the previous term when there is no rewriting *)
-    let a' = rewrite a and b' = rewrite b in
-    if a'==a && b'==b then e else f a' b'
-  in
-  let nary_op e es f rewrite xs = (* requires [e==f es] and [xs=map g es] *)
-    (* reuse the previous term when there is no rewriting *)
-    let modified = ref false in
-    let xs = List.map2 (fun e x ->
-        let x = rewrite x in
-        if not (x==e) then modified := true;
-        x) es xs
-    in if !modified then f xs else e
-  in
   let rewrite_cst ~highest ctx e = (* [r = rewrite ctx e] such that [ctx |- e = r] *)
     match F.repr e with
     | Kint _ -> e
@@ -1531,12 +1513,19 @@ let mask_simplifier =
         else e
     | _ -> e
   in
-  let rec rewrite ~highest ctx e = (* [r = rewrite ctx e] such that [ctx |- e = r] *)
-    let e =
+  let nary_op e f rewrite es = (* requires [e==f es] *)
+    (* reuse the previous term when there is no rewriting *)
+    let modified = ref false in
+    let xs = List.map (fun e ->
+        let x = rewrite e in
+        if not (x==e) then modified := true;
+        x) es
+    in if !modified then f xs else e
+  in
+  let rewrite ~highest ctx e = (* [r = rewrite ctx e] such that [ctx |- e = r] *)
+    let x =
       match F.repr e with
-      | Fun(f,xs) when f == f_land ->
-          let es = List.map (rewrite ~highest ctx) xs in
-          Wp_parameters.debug ~dkey "Rewrite AND %a@." Lang.F.pp_term e;
+      | Fun(f,es) when f == f_land ->
           let reduce unset x = match F.repr x with
             | Kint v -> F.e_zint (Integer.logand (Integer.lognot unset) v)
             | _ -> x
@@ -1549,21 +1538,12 @@ let mask_simplifier =
           let unset_mask = List.fold_left (collect ctx) Integer.zero es in
           if Integer.is_zero unset_mask then e
           else if Integer.equal unset_mask Integer.minus_one then e_zero
-          else nary_op e xs (F.e_fun f_land) (reduce unset_mask) es
-      | Fun(f,xs) -> (try
-                        nary_op e xs (F.e_fun ~result:(F.typeof e) f) (rewrite ~highest ctx) xs
-                      with _ -> e)
-      | Not a -> unary_op e e_not (rewrite ~highest ctx) a
-      | And es -> nary_op e es e_and (rewrite ~highest ctx) es
-      | Or es -> nary_op e es e_or (rewrite ~highest ctx) es
-      | Imply(xs, b) ->
-          let l = b::xs in
-          nary_op e l (function b::xs -> e_imply xs b | _ -> assert false) (rewrite ~highest ctx) l
-      | Eq (a, b) -> bin_op e e_eq (rewrite ~highest ctx) a b
-      | Leq (a, b) -> bin_op e e_leq (rewrite ~highest ctx) a b
-      | Lt (a, b) -> bin_op e e_lt (rewrite ~highest ctx) a b
+          else nary_op e (F.e_fun f_land) (reduce unset_mask) es
       | _ -> e
-    in rewrite_cst ~highest ctx e
+    in
+    let x = rewrite_cst ~highest ctx x in
+    if x == e then raise Not_found (* to try substitutions in the subterms *)
+    else x
 
   in
   object
@@ -1585,25 +1565,24 @@ let mask_simplifier =
     method equivalent_exp e =
       if Tmap.is_empty masks then e else
         (Wp_parameters.debug ~dkey "Rewrite Exp: %a@." Lang.F.pp_term e;
-         rewrite ~highest:true masks e)
+         Lang.e_subst (rewrite ~highest:true masks) e)
 
     method weaker_hyp p =
       if Tmap.is_empty masks then p else
         (Wp_parameters.debug ~dkey "Rewrite Hyp: %a@." Lang.F.pp_pred p;
-         F.p_bool (rewrite ~highest:false  masks (F.e_prop p)))
+         (* Does not rewrite [hyp] as much as possible.
+            Any way, contradiction may be found later when [hyp] will be assumed *)
+         Lang.p_subst (rewrite ~highest:false  masks) p)
 
     method equivalent_branch p =
       if Tmap.is_empty masks then p else
         (Wp_parameters.debug ~dkey "Rewrite Branch: %a@." Lang.F.pp_pred p;
-         (* Does not rewrite [hyp] as much as possible.
-            Any way, contradiction may be found later when [hyp] will be assumed *)
-         F.p_bool (rewrite ~highest:true masks (F.e_prop p))
-        )
+         Lang.p_subst (rewrite ~highest:true masks) p)
 
     method stronger_goal p =
       if Tmap.is_empty masks then p else
         (Wp_parameters.debug ~dkey "Rewrite Goal: %a@." Lang.F.pp_pred p;
-         F.p_bool (rewrite ~highest:true masks (F.e_prop p)))
+         Lang.p_subst (rewrite ~highest:true masks) p)
 
   end