prevent warning non_conservative_extension when cloning

src/core/theory.ml

@@ -399,6 +399,8 @@ let add_symbol_pr uc pr = add_symbol add_pr pr.pr_name pr uc
 
 let create_decl d = mk_tdecl (Decl d)
 
+let print_id fmt id = Format.fprintf fmt "%s" id.id_string
+
 let warn_dubious_axiom uc k p syms =
   match k with
   | Plemma | Pgoal -> ()
@@ -412,7 +414,8 @@ let warn_dubious_axiom uc k p syms =
           | _ -> ())
         syms;
       Warning.emit ?loc:p.id_loc
-        "axiom %s does not contain any local abstract symbol" p.id_string
+        "@[axiom %s does not contain any local abstract symbol@ (contains: @[%a@])@]" p.id_string
+        (Pp.print_list Pp.comma print_id) (Sid.elements syms)
     with Exit -> ()
 
 let lab_w_non_conservative_extension_no =
@@ -421,7 +424,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 uc d =
+let add_decl ?(warn=true) uc d =
   let uc = add_tdecl uc (create_decl d) in
   match d.d_node with
   | Dtype ts  ->
@@ -449,19 +452,19 @@ let add_decl uc d =
         List.fold_left add uc la in
       List.fold_left add_ind uc dl
   | Dprop (k,pr,_) ->
-      if should_be_conservative uc.uc_name &&
+      if warn && 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_symbol_pr uc pr
 
 (** Declaration constructors + add_decl *)
 
-let add_ty_decl uc ts = add_decl uc (create_ty_decl ts)
-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 uc k p f = add_decl uc (create_prop_decl k p f)
+let add_ty_decl uc ts = add_decl ~warn:false uc (create_ty_decl ts)
+let add_data_decl uc dl = add_decl ~warn:false uc (create_data_decl dl)
+let add_param_decl uc ls = add_decl ~warn:false uc (create_param_decl ls)
+let add_logic_decl uc dl = add_decl ~warn:false uc (create_logic_decl dl)
+let add_ind_decl uc s dl = add_decl ~warn:false 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)
 
 (** Use *)
 
@@ -885,7 +888,7 @@ let add_decl_with_tuples uc d =
     | None -> s in
   let ixs = Sid.fold add ids Sint.empty in
   let add n uc = use_export uc (tuple_theory n) in
-  add_decl (Sint.fold add ixs uc) d
+  add_decl ~warn:false (Sint.fold add ixs uc) d
 
 (* Exception reporting *)
 

src/core/theory.mli

@@ -154,14 +154,14 @@ val restore_path : ident -> string list * string * string list
 
 val create_decl : decl -> tdecl
 
-val add_decl : theory_uc -> decl -> theory_uc
+val add_decl : ?warn:bool -> 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 : theory_uc -> prop_kind -> prsymbol -> term -> theory_uc
+val add_prop_decl : ?warn:bool -> theory_uc -> prop_kind -> prsymbol -> term -> theory_uc
 
 val lab_w_non_conservative_extension_no : Ident.label
 

src/mlw/pmodule.ml

@@ -286,9 +286,9 @@ let add_pdecl_no_logic uc d =
   | PDexn xs -> add_symbol add_xs xs.xs_name xs uc
   | PDpure -> uc
 
-let add_pdecl_raw uc d =
+let add_pdecl_raw ?(warn=true) uc d =
   let uc = add_pdecl_no_logic uc d in
-  let th = List.fold_left add_decl uc.muc_theory d.pd_pure in
+  let th = List.fold_left (add_decl ~warn) uc.muc_theory d.pd_pure in
   { uc with muc_theory = th }
 
 (** {2 Builtin symbols} *)
@@ -329,7 +329,7 @@ let unit_module =
   let td = create_alias_decl (id_fresh "unit") [] ity_unit in
   let d,metas = create_type_decl [td] in
   assert (metas = []);
-  close_module (add_pdecl_raw uc d)
+  close_module (add_pdecl_raw ~warn:false uc d)
 
 let create_module env ?(path=[]) n =
   let m = empty_module env n path in
@@ -345,14 +345,14 @@ let add_use uc d = Sid.fold (fun id uc ->
   | Some n -> use_export uc (tuple_module n)
   | None -> uc) (Mid.set_diff d.pd_syms uc.muc_known) uc
 
-let add_pdecl ~vc uc d =
+let add_pdecl ?(warn=true) ~vc uc d =
   let uc = add_use uc d in
   let dl = if vc then Vc.vc uc.muc_env uc.muc_known d else [] in
   (* verification conditions must not add additional dependencies
      on built-in theories like TupleN or HighOrd. Also, we expect
      int.Int or any other library theory to be in the context:
      importing them automatically seems to be too invasive. *)
-  add_pdecl_raw (List.fold_left add_pdecl_raw uc dl) d
+  add_pdecl_raw ~warn (List.fold_left (add_pdecl_raw ~warn) uc dl) d
 
 (** {2 Cloning} *)
 
@@ -527,7 +527,7 @@ let clone_decl inst cl uc d = match d.d_node with
       uc
   | Dparam ls ->
       let d = create_param_decl (clone_ls cl ls) in
-      add_pdecl ~vc:false uc (create_pure_decl d)
+      add_pdecl ~warn:false ~vc:false uc (create_pure_decl d)
   | Dlogic ldl ->
       List.iter (fun (ls,_) ->
         if Mls.mem ls inst.mi_ls then raise (CannotInstantiate ls.ls_name);
@@ -535,7 +535,7 @@ let clone_decl inst cl uc d = match d.d_node with
       let get_logic (_,ld) =
         Opt.get (ls_defn_of_axiom (clone_fmla cl (ls_defn_axiom ld))) in
       let d = create_logic_decl (List.map get_logic ldl) in
-      add_pdecl ~vc:false uc (create_pure_decl d)
+      add_pdecl ~warn:false ~vc:false uc (create_pure_decl d)
   | Dind (s, idl) ->
       let lls = List.map (fun (ls,_) ->
         if Mls.mem ls inst.mi_ls then raise (CannotInstantiate ls.ls_name);
@@ -547,7 +547,7 @@ let clone_decl inst cl uc d = match d.d_node with
         pr', clone_fmla cl f in
       let get_ind ls (_,la) = ls, List.map get_case la in
       let d = create_ind_decl s (List.map2 get_ind lls idl) in
-      add_pdecl ~vc:false uc (create_pure_decl d)
+      add_pdecl ~warn:false ~vc:false uc (create_pure_decl d)
   | Dprop (k,pr,f) ->
       let skip, k' = match k, Mpr.find_opt pr inst.mi_pk with
         | Pgoal, _ -> true, Pgoal
@@ -559,7 +559,7 @@ let clone_decl inst cl uc d = match d.d_node with
       let pr' = create_prsymbol (id_clone pr.pr_name) in
       cl.pr_table <- Mpr.add pr pr' cl.pr_table;
       let d = create_prop_decl k' pr' (clone_fmla cl f) in
-      add_pdecl ~vc:false uc (create_pure_decl d)
+      add_pdecl ~warn:false ~vc:false uc (create_pure_decl d)
 
 let cl_save_ls cl s s' =
   cl.ls_table <- Mls.add_new (CannotInstantiate s.ls_name) s s' cl.ls_table
@@ -929,7 +929,7 @@ let add_vc uc (its, f) =
   let label = Slab.singleton (Ident.create_label ("expl:VC for " ^ nm)) in
   let pr = create_prsymbol (id_fresh ~label ?loc ("VC " ^ nm)) in
   let d = create_pure_decl (create_prop_decl Pgoal pr f) in
-  add_pdecl ~vc:false uc d
+  add_pdecl ~warn:false ~vc:false uc d
 
 let clone_pdecl inst cl uc d = match d.pd_node with
   | PDtype tdl ->
@@ -938,7 +938,7 @@ let clone_pdecl inst cl uc d = match d.pd_node with
         let d,metas = create_type_decl tdl in
       List.fold_left
         (fun uc (m,a) -> add_meta uc m a)
-        (add_pdecl ~vc:false uc d)
+        (add_pdecl ~warn:false ~vc:false uc d)
         metas
   | PDlet (LDsym (rs, c)) when Mrs.mem rs inst.mi_rs ->
       (* refine only [val] symbols *)
@@ -967,7 +967,7 @@ let clone_pdecl inst cl uc d = match d.pd_node with
       (* FIXME check effects of cexp/ld wrt rs *)
       (* FIXME add correspondance for "let lemma" to cl.pr_table *)
       let dl = Vc.vc uc.muc_env uc.muc_known (create_let_decl ld) in
-      List.fold_left add_pdecl_raw uc dl
+      List.fold_left (add_pdecl_raw ~warn:false) uc dl
   | PDlet ld ->
       begin match ld with
         | LDvar ({pv_vs=vs}, _) when Mvs.mem vs inst.mi_pv ->
@@ -990,7 +990,7 @@ let clone_pdecl inst cl uc d = match d.pd_node with
       cl.rn_table <- Mreg.set_union cl.rn_table frz;
       let sm, ld = clone_let_defn cl (sm_of_cl cl) ld in
       cl.pv_table <- sm.sm_pv; cl.rs_table <- sm.sm_rs;
-      add_pdecl ~vc:false uc (create_let_decl ld)
+      add_pdecl ~warn:false ~vc:false uc (create_let_decl ld)
   | PDexn ({xs_name = id} as xs) when Mxs.mem xs inst.mi_xs ->
       let xs' = Mxs.find xs inst.mi_xs in
       begin try let ity = clone_ity cl xs.xs_ity in
@@ -1004,7 +1004,7 @@ let clone_pdecl inst cl uc d = match d.pd_node with
       let ity = clone_ity cl xs.xs_ity in
       let xs' = create_xsymbol id ~mask:xs.xs_mask ity in
       cl.xs_table <- Mxs.add xs xs' cl.xs_table;
-      add_pdecl ~vc:false uc (create_exn_decl xs')
+      add_pdecl ~warn:false ~vc:false uc (create_exn_decl xs')
   | PDpure ->
       List.fold_left (clone_decl inst cl) uc d.pd_pure
 

src/mlw/pmodule.mli

@@ -117,7 +117,7 @@ val add_meta : pmodule_uc -> meta -> meta_arg list -> pmodule_uc
 
 (** {2 Program decls} *)
 
-val add_pdecl : vc:bool -> pmodule_uc -> pdecl -> pmodule_uc
+val add_pdecl : ?warn:bool -> vc:bool -> pmodule_uc -> pdecl -> pmodule_uc
 (** [add_pdecl ~vc m d] adds declaration [d] in module [m].
     If [vc] is [true], VC is computed and added to [m]. *)
 

theories/floating_point.why

@@ -104,7 +104,7 @@ theory GenFloat
 
   predicate no_overflow (m:mode) (x:real) = abs (round m x) <= max
 
-  axiom Bounded_real_no_overflow "W:non_conservative_extension:N":
+  axiom Bounded_real_no_overflow :
     forall m:mode, x:real. abs x <= max -> no_overflow m x
 
   axiom Round_monotonic :

theories/ieee_float.why

@@ -285,10 +285,10 @@ theory GenericFloat
 
   axiom eq_refl: forall x. is_finite x -> x .= x
 
-  axiom eq_sym "W:non_conservative_extension:N" :
+  axiom eq_sym :
     forall x y. x .= y -> y .= x
 
-  axiom eq_trans "W:non_conservative_extension:N":
+  axiom eq_trans :
     forall x y z. x .= y -> y .= z -> x .= z
 
   axiom eq_zero: zeroF .= (.- zeroF)