Commit eaa386a9 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Warn when cloning a theory that does not contain any abstract symbol.

File "why3/modules/array.mlw", line 141, characters 2-26:
warning: cloned theory map.MapPermut does not contain any abstract symbol; it should be used instead

Note that warn_clone_not_abstract is not called from clone_export so that
the location of the declaration can be passed.
parent 34e01bba
......@@ -628,6 +628,22 @@ let cl_tdecl cl inst td = match td.td_node with
| Clone (th,sm) -> Clone (th, cl_smap cl sm)
| Meta (id,al) -> Meta (id, List.map (cl_marg cl) al)
let warn_clone_not_abstract loc th =
try
List.iter (fun d -> match d.td_node with
| Decl d ->
begin match d.d_node with
| Dtype { ts_def = None }
| Dparam _ -> raise Exit
| _ -> ()
end
| _ -> ()
) th.th_decls;
Warning.emit ~loc "cloned theory %a.%s does not contain any abstract symbol; it should be used instead"
(Pp.print_list (Pp.constant_string ".") Pp.string) th.th_path
th.th_name.id_string
with Exit -> ()
let clone_theory cl add_td acc th inst =
let add acc td =
let td =
......
......@@ -168,6 +168,8 @@ val create_inst :
lemma : prsymbol list ->
goal : prsymbol list -> th_inst
val warn_clone_not_abstract : Loc.position -> theory -> unit
val clone_theory : ('a -> tdecl -> 'a) -> 'a -> theory -> th_inst -> 'a
val clone_export : theory_uc -> theory -> th_inst -> theory_uc
......
......@@ -1185,7 +1185,9 @@ let add_use_clone env lenv th loc (use, subst) =
Glob.use (match use.use_theory with Qident x | Qdot (_,x) -> x.id_loc) t.th_name;
match subst with
| None -> use_export th t
| Some s -> clone_export th t (type_inst th t s)
| Some s ->
warn_clone_not_abstract loc t;
clone_export th t (type_inst th t s)
in
let use_or_clone th = match use.use_import with
| Some (import, use_as) ->
......
......@@ -1979,7 +1979,9 @@ let use_clone_pure lib mth uc loc (use,inst) =
(* use or clone *)
let uc = match inst with
| None -> Theory.use_export uc th
| Some inst -> Theory.clone_export uc th (Typing.type_inst uc th inst) in
| Some inst ->
Theory.warn_clone_not_abstract loc th;
Theory.clone_export uc th (Typing.type_inst uc th inst) in
(* close namespace, if any *)
match use.use_import with
| Some (import, _) -> Theory.close_namespace uc import
......@@ -2001,8 +2003,10 @@ let use_clone lib mmd mth uc loc (use,inst) =
| Module m, None -> use_export uc m
| Theory th, None -> use_export_theory uc th
| Module m, Some inst ->
Theory.warn_clone_not_abstract loc m.mod_theory;
clone_export uc m (Typing.type_inst (get_theory uc) m.mod_theory inst)
| Theory th, Some inst ->
Theory.warn_clone_not_abstract loc th;
clone_export_theory uc th (Typing.type_inst (get_theory uc) th inst) in
(* close namespace, if any *)
match use.use_import with
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment