Expr: always add a "decrease" precondition to a rec_rsym

This is the most sensible way to recognize that we are looking
at a recursive function call, and we need that in Vc, even if there
is no actual variant to check, in order to rename the oldies in Eexec.

src/mlw/expr.ml

@@ -1074,8 +1074,7 @@ and rec_fixp dl =
     if cty_ghost d.c_cty && not (rs_ghost s) then Loc.errorm
       "Expr.let_rec: ghost status mismatch";
     let c = c_cty_ghostify (rs_ghost s) d in
-    let c = if List.length c.cty_pre < List.length s.rs_cty.cty_pre
-            then cty_add_pre [List.hd s.rs_cty.cty_pre] c else c in
+    let c = cty_add_pre [List.hd s.rs_cty.cty_pre] c in
     if eff_equal c.cty_effect s.rs_cty.cty_effect &&
        mask_equal c.cty_mask s.rs_cty.cty_mask then sm, (s,d)
     else let n = rs_dup s c in Mrs.add s n sm, (n,d) in
@@ -1122,13 +1121,10 @@ let let_rec fdl =
        c.cty_args = []
     then invalid_arg "Expr.let_rec";
     (* prepare the extra "decrease" precondition *)
-    let pre = match varl with
-      | [] -> c.cty_pre
-      | _::_ ->
-          let tl = List.map fst varl in
-          let id = id_fresh ("DECR " ^ s.rs_name.id_string) in
-          let ps = create_psymbol id (List.map t_type tl) in
-          ps_app ps tl :: c.cty_pre in
+    let decr_tl = List.map fst varl in
+    let decr_id = id_fresh ("DECR " ^ s.rs_name.id_string) in
+    let decr_ps = create_psymbol decr_id (List.map t_type decr_tl) in
+    let pre = ps_app decr_ps decr_tl :: c.cty_pre in
     (* create the clean rsymbol *)
     let id = id_clone s.rs_name in
     let c = create_cty ~mask:c.cty_mask c.cty_args pre
@@ -1148,8 +1144,7 @@ let let_rec fdl =
   LDrec rdl, rdl
 
 let ls_decr_of_rec_defn = function
-  | { rec_rsym = {rs_cty = {cty_pre = {t_node = Tapp (ls,_)}::_}};
-      rec_varl = _::_ } -> Some ls
+  | { rec_rsym = {rs_cty = {cty_pre = {t_node = Tapp (ls,_)}::_}} } -> Some ls
   | _ -> None
 
 (* pretty-pringting *)

src/mlw/pmodule.ml

@@ -830,8 +830,8 @@ and clone_let_defn cl sm ld = match ld with
         ~ghost:(rs_ghost s) ~kind:(rs_kind s) c' in
       sm_save_rs cl sm s s', ld
   | LDrec rdl ->
-      let conv_rs mrs {rec_rsym = {rs_name = id} as rs; rec_varl = varl} =
-        let cty = clone_cty cl sm ~drop_decr:(varl <> []) rs.rs_cty in
+      let conv_rs mrs {rec_rsym = {rs_name = id} as rs} =
+        let cty = clone_cty cl sm ~drop_decr:true rs.rs_cty in
         let rs' = create_rsymbol (id_clone id) ~ghost:(rs_ghost rs) cty in
         Mrs.add rs rs' mrs, rs' in
       let mrs, rsyml = Lists.map_fold_left conv_rs sm.sm_rs rdl in

src/mlw/vc.ml

@@ -233,6 +233,7 @@ let decrease_def env loc old_t t =
   else decrease_alg env loc old_t t
 
 let decrease env loc lab expl olds news =
+  if olds = [] && news = [] then t_true else
   let rec decr olds news = match olds, news with
     | (old_t, Some old_r)::olds, (t, Some r)::news
       when oty_equal old_t.t_ty t.t_ty && ls_equal old_r r ->
@@ -774,11 +775,9 @@ let rec k_expr env lps e res xmap =
         let init = wp_of_inv None lab expl_loop_init invl in
         let prev = sp_of_inv None lab expl_loop_init invl in
         let keep = wp_of_inv None lab expl_loop_keep invl in
-        let keep, oldies =
-          if varl = [] then keep, Mpv.empty else
-          let oldies, ovarl = oldify_variant varl in
-          let d = decrease env loc lab expl_loop_vari ovarl varl in
-          wp_and d keep, oldies in
+        let oldies, ovarl = oldify_variant varl in
+        let decr = decrease env loc lab expl_loop_vari ovarl varl in
+        let keep = wp_and decr keep in
         let iinv = inv_of_loop env e.e_loc invl varl in
         let j = List.fold_right assert_inv iinv (Kstop init) in
         let k = List.fold_right assert_inv iinv (Kstop keep) in
@@ -873,7 +872,6 @@ and k_rec env lps rdl =
   let k_rd {rec_fun = c; rec_varl = varl} =
     let e = match c.c_node with
       | Cfun e -> e | _ -> assert false in
-    if varl = [] then k_fun env lps c.c_cty e else
     (* store in lps our variant at the entry point
        and the list of well-founded orderings
        for each function in the let-rec block *)