From 5a39e6c08d428d774165e0ef3922ba8b75eee9e1 Mon Sep 17 00:00:00 2001 From: ppedrot Date: Mon, 28 Jan 2013 21:05:35 +0000 Subject: Uniformization of the "anomaly" command. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16165 85f007b7-540e-0410-9357-904b9bb8a0f7 --- library/assumptions.ml | 3 ++- library/declare.ml | 6 +++--- library/declaremods.ml | 34 +++++++++++++++++----------------- library/globnames.ml | 8 ++++---- library/goptions.ml | 6 +++--- library/impargs.ml | 10 +++++----- library/kindops.ml | 4 ++-- library/lib.ml | 12 ++++++------ library/libnames.ml | 2 +- library/libobject.ml | 16 ++++++++-------- library/library.ml | 6 +++--- library/nametab.ml | 4 ++-- library/summary.ml | 2 +- 13 files changed, 57 insertions(+), 56 deletions(-) (limited to 'library') 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 -- cgit v1.2.3