Uniformization of the "anomaly" command.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16165 85f007b7-540e-0410-9357-904b9bb8a0f7

13 files changed, 57 insertions, 56 deletions

diff --git a/library/assumptions.ml b/library/assumptions.ml
index 84e870499..cb0c99e5a 100644
--- a/library/assumptions.ml
+++ b/library/assumptions.ml
@@ -14,6 +14,7 @@
 (* Initial author: Arnaud Spiwack
    Module-traversing code: Pierre Letouzey *)
 
+open Pp
 open Errors
 open Util
 open Names
@@ -147,7 +148,7 @@ let lookup_constant_in_impl cst fallback =
        - The label has not been found in the structure. This is an error *)
     match fallback with
       | Some cb -> cb
-      | None -> anomaly ("Print Assumption: unknown constant "^string_of_con cst)
+      | None -> anomaly (str "Print Assumption: unknown constant " ++ pr_con cst)
 
 let lookup_constant cst =
   try
diff --git a/library/declare.ml b/library/declare.ml
index 5c1072843..27aecfe73 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -280,7 +280,7 @@ let inInductive : inductive_obj -> obj =
 let declare_mind isrecord mie =
   let id = match mie.mind_entry_inds with
     | ind::_ -> ind.mind_entry_typename
-    | [] -> anomaly "cannot declare an empty list of inductives" in
+    | [] -> anomaly (Pp.str "cannot declare an empty list of inductives") in
   let (sp,kn as oname) = add_leaf id (inInductive ([],mie)) in
   let mind = Global.mind_of_delta_kn kn in
   declare_mib_implicits mind;
@@ -294,7 +294,7 @@ let pr_rank i = pr_nth (i+1)
 
 let fixpoint_message indexes l =
   Flags.if_verbose msg_info (match l with
-  | [] -> anomaly "no recursive definition"
+  | [] -> anomaly (Pp.str "no recursive definition")
   | [id] -> pr_id id ++ str " is recursively defined" ++
       (match indexes with
 	 | Some [|i|] -> str " (decreasing on "++pr_rank i++str " argument)"
@@ -309,7 +309,7 @@ let fixpoint_message indexes l =
 
 let cofixpoint_message l =
   Flags.if_verbose msg_info (match l with
-  | [] -> anomaly "No corecursive definition."
+  | [] -> anomaly (Pp.str "No corecursive definition.")
   | [id] -> pr_id id ++ str " is corecursively defined"
   | l -> hov 0 (prlist_with_sep pr_comma pr_id l ++
                     spc () ++ str "are corecursively defined"))
diff --git a/library/declaremods.ml b/library/declaremods.ml
index 99704d1c0..61d6e0852 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -158,7 +158,7 @@ let mp_of_kn kn =
     if Dir_path.equal sec Dir_path.empty then
       MPdot (mp,l)
     else
-      anomaly ("Non-empty section in module name!" ^ string_of_kn kn)
+      anomaly (str "Non-empty section in module name!" ++ spc () ++ pr_kn kn)
 
 let dir_of_sp sp =
   let dir,id = repr_path sp in
@@ -310,7 +310,7 @@ let (in_module : substitutive_objects -> obj),
     subst_function = subst_module;
     classify_function = classify_module }
 
-let cache_keep _ = anomaly "This module should not be cached!"
+let cache_keep _ = anomaly (Pp.str "This module should not be cached!")
 
 let load_keep i ((sp,kn),seg) =
   let mp = mp_of_kn kn in
@@ -319,10 +319,10 @@ let load_keep i ((sp,kn),seg) =
       try
 	let prefix',objects = MPmap.find mp !modtab_objects in
 	  if not (eq_op prefix' prefix) then
-	    anomaly "Two different modules with the same path!";
+	    anomaly (Pp.str "Two different modules with the same path!");
 	  modtab_objects := MPmap.add mp (prefix,objects@seg) !modtab_objects;
       with
-	  Not_found -> anomaly "Keep objects before substitutive"
+	  Not_found -> anomaly (Pp.str "Keep objects before substitutive")
     end;
     load_objects i prefix seg
 
@@ -366,10 +366,10 @@ let cache_modtype ((sp,kn),(entry,modtypeobjs,sub_mty_l)) =
   let _ =
     match entry with
       | None ->
-	  anomaly "You must not recache interactive module types!"
+	  anomaly (Pp.str "You must not recache interactive module types!")
       | Some (mte,inl) ->
 	  if not (mp_eq mp (Global.add_modtype (basename sp) mte inl)) then
-	    anomaly "Kernel and Library names do not match"
+	    anomaly (Pp.str "Kernel and Library names do not match")
   in
 
   (* Using declare_modtype should lead here, where we check
@@ -433,11 +433,11 @@ let in_modtype : modtype_obj -> obj =
 
 let rec replace_module_object idl (mbids,mp,lib_stack) (mbids2,mp2,objs) mp1 =
   let () = match mbids with
-  | [] -> () | _ -> anomaly "Unexpected functor objects" in
+  | [] -> () | _ -> anomaly (Pp.str "Unexpected functor objects") in
   let rec replace_idl = function
     | _,[] -> []
     | id::idl,(id',obj)::tail when Id.equal id id' ->
-      if not (String.equal (object_tag obj) "MODULE") then anomaly "MODULE expected!";
+      if not (String.equal (object_tag obj) "MODULE") then anomaly (Pp.str "MODULE expected!");
       let substobjs = match idl with
       | [] ->
         let mp' = MPdot(mp, Label.of_id id) in
@@ -591,13 +591,13 @@ let end_module () =
 	    get_modtype_substobjs (Global.env()) mp inline mty in
 	  Some mp1,(mbids@mbids1,mp1,objs), [], []
       | Some (MSEfunctor _, _) ->
-	  anomaly "Funsig cannot be here..."
+	  anomaly (Pp.str "Funsig cannot be here...")
       | Some (MSEapply _ as mty, inline) ->
 	  let (mbids1,mp1,objs) =
 	    get_modtype_substobjs (Global.env()) mp inline mty in
 	  Some mp1,(mbids@mbids1,mp1,objs), [], []
   with
-	Not_found -> anomaly "Module objects not found..."
+	Not_found -> anomaly (Pp.str "Module objects not found...")
   in
     (* must be called after get_modtype_substobjs, because of possible
      dependencies on functor arguments *)
@@ -625,9 +625,9 @@ let end_module () =
   let newoname = Lib.add_leaves id objects in
 
     if not (eq_full_path (fst newoname) (fst oldoname)) then
-      anomaly "Names generated on start_ and end_module do not match";
+      anomaly (Pp.str "Names generated on start_ and end_module do not match");
     if not (mp_eq (mp_of_kn (snd newoname)) mp) then
-      anomaly "Kernel and Library names do not match";
+      anomaly (Pp.str "Kernel and Library names do not match");
 
     Lib.add_frozen_state () (* to prevent recaching *);
     mp
@@ -660,7 +660,7 @@ let register_library dir cenv objs digest =
   with Not_found ->
     let mp', values = Global.import cenv digest in
     if not (mp_eq mp mp') then
-      anomaly "Unexpected disk module name";
+      anomaly (Pp.str "Unexpected disk module name");
     let mp,substitute,keep = objs in
     let substobjs = [], mp, substitute in
     let modobjs = substobjs, keep, values in
@@ -748,10 +748,10 @@ let end_modtype () =
   in
   if not (eq_full_path (fst oname) (fst oldoname)) then
     anomaly
-      "Section paths generated on start_ and end_modtype do not match";
+      (str "Section paths generated on start_ and end_modtype do not match");
   if not (mp_eq (mp_of_kn (snd oname)) mp) then
     anomaly
-      "Kernel and Library names do not match";
+      (str "Kernel and Library names do not match");
 
   Lib.add_frozen_state ()(* to prevent recaching *);
   mp
@@ -837,7 +837,7 @@ let declare_module_ interp_modtype interp_modexpr id args res mexpr_o fs =
     match entry with
       | {mod_entry_type = Some mte} -> get_modtype_substobjs env mmp inl_res mte
       | {mod_entry_expr = Some mexpr} -> get_module_substobjs env mmp inl_expr mexpr
-      | _ -> anomaly "declare_module: No type, no body ..."
+      | _ -> anomaly ~label:"declare_module" (Pp.str "No type, no body ...")
   in
   let (mbids,mp_from,objs) = substobjs in
   (* Undo the simulated interactive building of the module *)
@@ -850,7 +850,7 @@ let declare_module_ interp_modtype interp_modexpr id args res mexpr_o fs =
   in (* PLTODO *)
   let mp_env,resolver = Global.add_module id entry inl in
 
-  if not (mp_eq mp_env mp) then anomaly "Kernel and Library names do not match";
+  if not (mp_eq mp_env mp) then anomaly (Pp.str "Kernel and Library names do not match");
 
   
   check_subtypes mp subs;
diff --git a/library/globnames.ml b/library/globnames.ml
index ea002ef58..06a8f823d 100644
--- a/library/globnames.ml
+++ b/library/globnames.ml
@@ -155,14 +155,14 @@ let decode_mind kn =
     if (Dir_path.repr sec_dir) = [] then
      (Dir_path.make (dir_of_mp mp)),Label.to_id l
     else
-      anomaly "Section part should be empty!"
+      anomaly (Pp.str "Section part should be empty!")
 
 let decode_con kn =
   let mp,sec_dir,l = repr_con kn in
     match mp,(Dir_path.repr sec_dir) with
 	MPfile dir,[] -> (dir,Label.to_id l)
-      | _ , [] -> anomaly "MPfile expected!"
-      | _ -> anomaly "Section part should be empty!"
+      | _ , [] -> anomaly (Pp.str "MPfile expected!")
+      | _ -> anomaly (Pp.str "Section part should be empty!")
 
 (* popping one level of section in global names *)
 
@@ -178,4 +178,4 @@ let pop_global_reference = function
   | ConstRef con -> ConstRef (pop_con con)
   | IndRef (kn,i) -> IndRef (pop_kn kn,i)
   | ConstructRef ((kn,i),j) -> ConstructRef ((pop_kn kn,i),j)
-  | VarRef id -> anomaly "VarRef not poppable"
+  | VarRef id -> anomaly (Pp.str "VarRef not poppable")
diff --git a/library/goptions.ml b/library/goptions.ml
index 550ded685..381b67726 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -269,15 +269,15 @@ type 'a write_function = 'a -> unit
 let declare_int_option =
   declare_option
     (fun v -> IntValue v)
-    (function IntValue v -> v | _ -> anomaly "async_option")
+    (function IntValue v -> v | _ -> anomaly (Pp.str "async_option"))
 let declare_bool_option =
   declare_option
     (fun v -> BoolValue v)
-    (function BoolValue v -> v | _ -> anomaly "async_option")
+    (function BoolValue v -> v | _ -> anomaly (Pp.str "async_option"))
 let declare_string_option =
   declare_option
     (fun v -> StringValue v)
-    (function StringValue v -> v | _ -> anomaly "async_option")
+    (function StringValue v -> v | _ -> anomaly (Pp.str "async_option"))
 
 (* 3- User accessible commands *)
 
diff --git a/library/impargs.ml b/library/impargs.ml
index e2abb0925..c8c1ab005 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -275,16 +275,16 @@ let is_status_implicit = function
   | _ -> true
 
 let name_of_implicit = function
-  | None -> anomaly "Not an implicit argument"
+  | None -> anomaly (Pp.str "Not an implicit argument")
   | Some (id,_,_) -> id
 
 let maximal_insertion_of = function
   | Some (_,_,(b,_)) -> b
-  | None -> anomaly "Not an implicit argument"
+  | None -> anomaly (Pp.str "Not an implicit argument")
 
 let force_inference_of = function
   | Some (_, _, (_, b)) -> b
-  | None -> anomaly "Not an implicit argument"
+  | None -> anomaly (Pp.str "Not an implicit argument")
 
 (* [in_ctx] means we know the expected type, [n] is the index of the argument *)
 let is_inferable_implicit in_ctx n = function
@@ -308,7 +308,7 @@ let positions_of_implicits (_,impls) =
 
 let rec prepare_implicits f = function
   | [] -> []
-  | (Anonymous, Some _)::_ -> anomaly "Unnamed implicit"
+  | (Anonymous, Some _)::_ -> anomaly (Pp.str "Unnamed implicit")
   | (Name id, Some imp)::imps ->
       let imps' = prepare_implicits f imps in
       Some (id,imp,(set_maximality imps' f.maximal,true)) :: imps'
@@ -476,7 +476,7 @@ let implicits_of_global ref =
       List.map2 (fun (t, il) rl -> t, List.map2 rename il rl) l rename_l
     with Not_found -> l
     | Invalid_argument _ ->
-        anomaly "renamings list and implicits list have different lenghts"
+        anomaly (Pp.str "renamings list and implicits list have different lenghts")
   with Not_found -> [DefaultImpArgs,[]]
 
 let cache_implicits_decl (ref,imps) =
diff --git a/library/kindops.ml b/library/kindops.ml
index 86e6e2fff..35aebc531 100644
--- a/library/kindops.ml
+++ b/library/kindops.ml
@@ -34,8 +34,8 @@ let string_of_definition_kind def =
   | Global, CanonicalStructure -> "Canonical Structure"
   | Global, Example -> "Example"
   | Local, (CanonicalStructure|Example) ->
-      Errors.anomaly "Unsupported local definition kind"
+      Errors.anomaly (Pp.str "Unsupported local definition kind")
   | Local, Instance -> "Instance"
   | Global, Instance -> "Global Instance"
   | _, (StructureComponent|Scheme|CoFixpoint|Fixpoint|IdentityCoercion|Method)
-      -> Errors.anomaly "Internal definition kind"
+      -> Errors.anomaly (Pp.str "Internal definition kind")
diff --git a/library/lib.ml b/library/lib.ml
index 0f2f480cb..01e24f6c7 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -350,15 +350,15 @@ let end_compilation dir =
     try match find_entry_p is_opening_lib with
       |	(oname, CompilingLibrary prefix) -> oname
       | _ -> assert false
-    with Not_found -> anomaly "No module declared"
+    with Not_found -> anomaly (Pp.str "No module declared")
   in
   let _ =
     match !comp_name with
-      | None -> anomaly "There should be a module name..."
+      | None -> anomaly (Pp.str "There should be a module name...")
       | Some m ->
 	  if not (Names.Dir_path.equal m dir) then anomaly
-	    ("The current open module has name "^ (Names.Dir_path.to_string m) ^
-	       " and not " ^ (Names.Dir_path.to_string m));
+	    (str "The current open module has name" ++ spc () ++ pr_dirpath m ++
+             spc () ++ str "and not" ++ spc () ++ pr_dirpath m);
   in
   let (after,mark,before) = split_lib_at_opening oname in
   comp_name := None;
@@ -521,7 +521,7 @@ let discharge_item ((sp,_ as oname),e) =
   | FrozenState _ -> None
   | ClosedSection _ | ClosedModule _ -> None
   | OpenedSection _ | OpenedModule _ | CompilingLibrary _ ->
-      anomaly "discharge_item"
+      anomaly (Pp.str "discharge_item")
 
 let close_section () =
   let oname,fs =
@@ -681,7 +681,7 @@ let remove_section_part ref =
   let dir,_ = repr_path sp in
   match ref with
   | VarRef id ->
-      anomaly "remove_section_part not supported on local variables"
+      anomaly (Pp.str "remove_section_part not supported on local variables")
   | _ ->
       if is_dirpath_prefix_of dir (cwd ()) then
         (* Not yet (fully) discharged *)
diff --git a/library/libnames.ml b/library/libnames.ml
index 7680e5248..902222431 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -22,7 +22,7 @@ let pop_dirpath_n n dir =
   Dir_path.make (List.skipn n (Dir_path.repr dir))
 
 let pop_dirpath p = match Dir_path.repr p with
-  | [] -> anomaly "dirpath_prefix: empty dirpath"
+  | [] -> anomaly (str "dirpath_prefix: empty dirpath")
   | _::l -> Dir_path.make l
 
 let is_dirpath_prefix_of d1 d2 =
diff --git a/library/libobject.ml b/library/libobject.ml
index 81f306a33..7cf286321 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -36,7 +36,7 @@ type 'a object_declaration = {
   discharge_function : object_name * 'a -> 'a option;
   rebuild_function : 'a -> 'a }
 
-let yell s = anomaly s
+let yell s = anomaly (Pp.str s)
 
 let default_object s = {
   object_name = s;
@@ -84,17 +84,17 @@ let declare_object_full odecl =
   let (infun,outfun) = Dyn.create na in
   let cacher (oname,lobj) =
     if String.equal (Dyn.tag lobj) na then odecl.cache_function (oname,outfun lobj)
-    else anomaly "somehow we got the wrong dynamic object in the cachefun"
+    else anomaly (Pp.str "somehow we got the wrong dynamic object in the cachefun")
   and loader i (oname,lobj) =
     if String.equal (Dyn.tag lobj) na then odecl.load_function i (oname,outfun lobj)
-    else anomaly "somehow we got the wrong dynamic object in the loadfun"
+    else anomaly (Pp.str "somehow we got the wrong dynamic object in the loadfun")
   and opener i (oname,lobj) =
     if String.equal (Dyn.tag lobj) na then odecl.open_function i (oname,outfun lobj)
-    else anomaly "somehow we got the wrong dynamic object in the openfun"
+    else anomaly (Pp.str "somehow we got the wrong dynamic object in the openfun")
   and substituter (sub,lobj) = 
     if String.equal (Dyn.tag lobj) na then 
       infun (odecl.subst_function (sub,outfun lobj))
-    else anomaly "somehow we got the wrong dynamic object in the substfun"
+    else anomaly (Pp.str "somehow we got the wrong dynamic object in the substfun")
   and classifier lobj =
     if String.equal (Dyn.tag lobj) na then
       match odecl.classify_function (outfun lobj) with
@@ -103,15 +103,15 @@ let declare_object_full odecl =
 	| Keep obj -> Keep (infun obj)
 	| Anticipate (obj) -> Anticipate (infun obj)
     else
-      anomaly "somehow we got the wrong dynamic object in the classifyfun"
+      anomaly (Pp.str "somehow we got the wrong dynamic object in the classifyfun")
   and discharge (oname,lobj) =
     if String.equal (Dyn.tag lobj) na then
       Option.map infun (odecl.discharge_function (oname,outfun lobj))
     else
-      anomaly "somehow we got the wrong dynamic object in the dischargefun"
+      anomaly (Pp.str "somehow we got the wrong dynamic object in the dischargefun")
   and rebuild lobj =
     if String.equal (Dyn.tag lobj) na then infun (odecl.rebuild_function (outfun lobj))
-    else anomaly "somehow we got the wrong dynamic object in the rebuildfun"
+    else anomaly (Pp.str "somehow we got the wrong dynamic object in the rebuildfun")
   in
   Hashtbl.add cache_tab na { dyn_cache_function = cacher;
 			     dyn_load_function = loader;
diff --git a/library/library.ml b/library/library.ml
index a944db45c..f68a058c2 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -33,7 +33,7 @@ let find_logical_path phys_dir =
   match paths with
   | [_,dir,_] -> dir
   | [] -> Nameops.default_root_prefix
-  | l -> anomaly ("Two logical paths are associated to "^phys_dir)
+  | l -> anomaly (str "Two logical paths are associated to" ++ spc () ++ str phys_dir)
 
 let is_in_load_paths phys_dir =
   let dir = CUnix.canonical_path_name phys_dir in
@@ -67,7 +67,7 @@ let add_load_path isroot (phys_path,coq_path) =
 	    end
       | [] ->
 	  load_paths := (phys_path,coq_path,isroot) :: !load_paths;
-      | _ -> anomaly ("Two logical paths are associated to "^phys_path)
+      | _ -> anomaly (str "Two logical paths are associated to" ++ spc () ++ str phys_path)
 
 let extend_path_with_dirpath p dir =
   List.fold_left Filename.concat p
@@ -669,7 +669,7 @@ let save_library_to dir f =
     let fn = Filename.dirname f'^"/"^Nativecode.mod_uid_of_dirpath dir in
     match Nativelibrary.compile_library dir ast lp fn with
       | 0 -> ()
-      | _ -> anomaly "Library compilation failure"
+      | _ -> anomaly (Pp.str "Library compilation failure")
     end
   with e ->
     msg_warning (str ("Removed file "^f')); close_out ch; Sys.remove f';
diff --git a/library/nametab.ml b/library/nametab.ml
index 46d8dcc3f..6829e9431 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -172,7 +172,7 @@ let rec push_exactly uname o level tree = function
 	  let ptab' = push_exactly uname o (level-1) mc path in
 	  mktree tree.path (ModIdmap.add modid ptab' tree.map)
   | [] ->
-      anomaly "Prefix longer than path! Impossible!"
+      anomaly (Pp.str "Prefix longer than path! Impossible!")
 
 
 let push visibility uname o tab =
@@ -312,7 +312,7 @@ struct
   let equal d1 d2 = Int.equal (Dir_path.compare d1 d2) 0
   let to_string = Dir_path.to_string
   let repr dir = match Dir_path.repr dir with
-    | [] -> anomaly "Empty dirpath"
+    | [] -> anomaly (Pp.str "Empty dirpath")
     | id :: l -> (id, l)
 end
 
diff --git a/library/summary.ml b/library/summary.ml
index a31f61c31..c6de35744 100644
--- a/library/summary.ml
+++ b/library/summary.ml
@@ -29,7 +29,7 @@ let internal_declare_summary sumname sdecl =
     init_function = dyn_init }
   in
   if Hashtbl.mem summaries sumname then
-    anomalylabstrm "Summary.declare_summary"
+    anomaly ~label:"Summary.declare_summary"
       (str "Cannot declare a summary twice: " ++ str sumname);
   Hashtbl.add summaries sumname ddecl