Mlw: axioms produced by create_let_decl should not provoke warnings

Also, remove the optional [warn] argument of Theory.add_decl:
clients should use appropriate labels to suppress warnings.

src/core/theory.ml

@@ -420,7 +420,7 @@ let lab_w_non_conservative_extension_no =
 let should_be_conservative id =
   not (Slab.mem lab_w_non_conservative_extension_no id.id_label)
 
-let add_decl ?(warn=true) uc d =
+let add_decl uc d =
   let uc = add_tdecl uc (create_decl d) in
   match d.d_node with
     | Dtype ts  -> add_symbol add_ts ts.ts_name ts uc
@@ -429,8 +429,8 @@ let add_decl ?(warn=true) uc d =
     | Dlogic dl -> List.fold_left add_logic uc dl
     | Dind (_, dl) -> List.fold_left add_ind uc dl
     | Dprop ((k,pr,_) as p) ->
-      if warn && should_be_conservative uc.uc_name &&
-           should_be_conservative pr.pr_name
+      if should_be_conservative uc.uc_name &&
+         should_be_conservative pr.pr_name
       then warn_dubious_axiom uc k pr.pr_name d.d_syms;
       add_prop uc p
 
@@ -441,8 +441,7 @@ let add_data_decl uc dl = add_decl uc (create_data_decl dl)
 let add_param_decl uc ls = add_decl uc (create_param_decl ls)
 let add_logic_decl uc dl = add_decl uc (create_logic_decl dl)
 let add_ind_decl uc s dl = add_decl uc (create_ind_decl s dl)
-let add_prop_decl ?warn uc k p f =
-  add_decl ?warn uc (create_prop_decl k p f)
+let add_prop_decl uc k p f = add_decl uc (create_prop_decl k p f)
 
 (** Use *)
 

src/core/theory.mli

@@ -149,15 +149,16 @@ val restore_path : ident -> string list * string * string list
 
 val create_decl : decl -> tdecl
 
-val add_decl : ?warn:bool -> theory_uc -> decl -> theory_uc
+val add_decl : theory_uc -> decl -> theory_uc
 
 val add_ty_decl : theory_uc -> tysymbol -> theory_uc
 val add_data_decl : theory_uc -> data_decl list -> theory_uc
 val add_param_decl : theory_uc -> lsymbol -> theory_uc
 val add_logic_decl : theory_uc -> logic_decl list -> theory_uc
 val add_ind_decl : theory_uc -> ind_sign -> ind_decl list -> theory_uc
-val add_prop_decl :
-  ?warn:bool -> theory_uc -> prop_kind -> prsymbol -> term -> theory_uc
+val add_prop_decl : theory_uc -> prop_kind -> prsymbol -> term -> theory_uc
+
+val lab_w_non_conservative_extension_no : Ident.label
 
 (** {2 Use} *)
 

src/mlw/pdecl.ml

@@ -353,6 +353,8 @@ let rec t_subst_fmla v t f = t_label_copy f (match f.t_node with
   | Tvar u when vs_equal u v -> t_if t t_bool_true t_bool_false
   | _ -> t_map (t_subst_fmla v t) f)
 
+let lab_w_nce_no = Slab.singleton Theory.lab_w_non_conservative_extension_no
+
 let create_let_decl ld =
   let conv_post t ql =
     let conv q = match t.t_ty with
@@ -360,6 +362,7 @@ let create_let_decl ld =
       | None -> let v,f = open_post q in
                 t_subst_fmla v t f in
     List.map conv ql in
+  let label = lab_w_nce_no in
   let cty_axiom id cty f axms =
     if t_equal f t_true then axms else
     (* we do not care about aliases for pure symbols *)
@@ -383,13 +386,13 @@ let create_let_decl ld =
               let fl = f :: conv_post (t_var v) ql in
               t_exists_close [v] [] (t_and_simp_l fl)
           | [] -> t_true in
-        abst, defn, cty_axiom (id_clone s.rs_name) cty f axms
+        abst, defn, cty_axiom (id_clone ~label s.rs_name) cty f axms
     | RLls ({ls_name = id} as ls) ->
         let vl = List.map (fun v -> v.pv_vs) cty.cty_args in
         let hd = t_app ls (List.map t_var vl) ls.ls_value in
         let f = t_and_simp_l (conv_post hd cty.cty_post) in
         let nm = id.id_string ^ "_spec" in
-        let axms = cty_axiom (id_derive nm id) cty f axms in
+        let axms = cty_axiom (id_derive ~label nm id) cty f axms in
         let c = if Mrs.is_empty sm then c else c_rs_subst sm c in
         begin match c.c_node with
         | Cany | Capp _ | Cpur _ ->
@@ -406,13 +409,13 @@ let create_let_decl ld =
                 abst, (ls, vl, f) :: defn, axms
             | Some f ->
                 let f = t_insert hd f and nm = id.id_string ^ "_def" in
-                let axms = cty_axiom (id_derive nm id) cty f axms in
+                let axms = cty_axiom (id_derive ~label nm id) cty f axms in
                 create_param_decl ls :: abst, defn, axms
             | None when cty.cty_post = [] ->
                 let axms = match post_of_expr hd e with
                   | Some f ->
                       let nm = id.id_string ^ "_def" in
-                      cty_axiom (id_derive nm id) cty f axms
+                      cty_axiom (id_derive ~label nm id) cty f axms
                   | None -> axms in
                 create_param_decl ls :: abst, defn, axms
             | None ->
@@ -446,7 +449,7 @@ let create_let_decl ld =
     let abst = List.map (fun (s,_) -> create_param_decl s) dl in
     let mk_ax ({ls_name = id} as s, vl, t) =
       let nm = id.id_string ^ "_def" in
-      let pr = create_prsymbol (id_derive nm id) in
+      let pr = create_prsymbol (id_derive ~label nm id) in
       let hd = t_app s (List.map t_var vl) t.t_ty in
       let ax = t_forall_close vl [] (t_insert hd t) in
       create_prop_decl Paxiom pr ax in

src/mlw/pmodule.ml

@@ -275,7 +275,7 @@ let add_pdecl_no_logic uc d =
 
 let add_pdecl uc d =
   let uc = add_pdecl_no_logic uc d in
-  let th = List.fold_left (add_decl ~warn:true) uc.muc_theory d.pd_pure in
+  let th = List.fold_left add_decl uc.muc_theory d.pd_pure in
   { uc with muc_theory = th }
 
 (** {2 Builtin symbols} *)