diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-01-28 21:05:35 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-01-28 21:05:35 +0000 |
| commit | 5a39e6c08d428d774165e0ef3922ba8b75eee9e1 (patch) | |
| tree | e035f490e2c748356df73342876b22cfcb3bc5a0 | |
| parent | 5e8824960f68f529869ac299b030282cc916ba2c (diff) | |
Uniformization of the "anomaly" command.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16165 85f007b7-540e-0410-9357-904b9bb8a0f7
128 files changed, 454 insertions, 441 deletions
diff --git a/checker/check.ml b/checker/check.ml index 49fe6d0ba..18640d9d4 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -153,7 +153,7 @@ let find_logical_path phys_dir = match List.filter2 (fun p d -> p = phys_dir) physical logical with | _,[dir] -> dir | _,[] -> default_root_prefix - | _,l -> anomaly ("Two logical paths are associated to "^phys_dir) + | _,l -> anomaly (Pp.str ("Two logical paths are associated to "^phys_dir)) let remove_load_path dir = let physical, logical = !load_paths in @@ -185,7 +185,7 @@ let add_load_path (phys_path,coq_path) = end | _,[] -> load_paths := (phys_path :: fst !load_paths, coq_path :: snd !load_paths) - | _ -> anomaly ("Two logical paths are associated to "^phys_path) + | _ -> anomaly (Pp.str ("Two logical paths are associated to "^phys_path)) let load_paths_of_dir_path dir = let physical, logical = !load_paths in diff --git a/checker/environ.ml b/checker/environ.ml index a0fac3492..0b475ad49 100644 --- a/checker/environ.ml +++ b/checker/environ.ml @@ -111,9 +111,11 @@ let add_constraints c env = let lookup_constant kn env = Cmap_env.find kn env.env_globals.env_constants +let anomaly s = anomaly (Pp.str s) + let add_constant kn cs env = if Cmap_env.mem kn env.env_globals.env_constants then - Printf.ksprintf anomaly "Constant %s is already defined" + Printf.ksprintf anomaly ("Constant %s is already defined") (string_of_con kn); let new_constants = Cmap_env.add kn cs env.env_globals.env_constants in @@ -155,7 +157,7 @@ let lookup_mind kn env = let add_mind kn mib env = if Mindmap_env.mem kn env.env_globals.env_inductives then - Printf.ksprintf anomaly "Inductive %s is already defined" + Printf.ksprintf anomaly ("Inductive %s is already defined") (string_of_mind kn); let new_inds = Mindmap_env.add kn mib env.env_globals.env_inductives in let kn1,kn2 = user_mind kn,canonical_mind kn in @@ -174,7 +176,7 @@ let add_mind kn mib env = let add_modtype ln mtb env = if MPmap.mem ln env.env_globals.env_modtypes then - Printf.ksprintf anomaly "Module type %s is already defined" + Printf.ksprintf anomaly ("Module type %s is already defined") (string_of_mp ln); let new_modtypes = MPmap.add ln mtb env.env_globals.env_modtypes in let new_globals = @@ -184,7 +186,7 @@ let add_modtype ln mtb env = let shallow_add_module mp mb env = if MPmap.mem mp env.env_globals.env_modules then - Printf.ksprintf anomaly "Module %s is already defined" + Printf.ksprintf anomaly ("Module %s is already defined") (string_of_mp mp); let new_mods = MPmap.add mp mb env.env_globals.env_modules in let new_globals = @@ -194,7 +196,7 @@ let shallow_add_module mp mb env = let shallow_remove_module mp env = if not (MPmap.mem mp env.env_globals.env_modules) then - Printf.ksprintf anomaly "Module %s is unknown" + Printf.ksprintf anomaly ("Module %s is unknown") (string_of_mp mp); let new_mods = MPmap.remove mp env.env_globals.env_modules in let new_globals = diff --git a/checker/indtypes.ml b/checker/indtypes.ml index 285be1bc9..8b56b5365 100644 --- a/checker/indtypes.ml +++ b/checker/indtypes.ml @@ -100,7 +100,7 @@ let rec sorts_of_constr_args env t = let env1 = push_rel (name,Some def,ty) env in sorts_of_constr_args env1 c | _ when is_constructor_head t -> [] - | _ -> anomaly "infos_and_sort: not a positive constructor" + | _ -> anomaly ~label:"infos_and_sort" (Pp.str "not a positive constructor") (* Prop and Set are small *) @@ -299,11 +299,11 @@ let failwith_non_pos n ntypes c = let failwith_non_pos_vect n ntypes v = Array.iter (failwith_non_pos n ntypes) v; - anomaly "failwith_non_pos_vect: some k in [n;n+ntypes-1] should occur" + anomaly ~label:"failwith_non_pos_vect" (Pp.str "some k in [n;n+ntypes-1] should occur") let failwith_non_pos_list n ntypes l = List.iter (failwith_non_pos n ntypes) l; - anomaly "failwith_non_pos_list: some k in [n;n+ntypes-1] should occur" + anomaly ~label:"failwith_non_pos_list" (Pp.str "some k in [n;n+ntypes-1] should occur") (* Conclusion of constructors: check the inductive type is called with the expected parameters *) diff --git a/checker/inductive.ml b/checker/inductive.ml index b04c77ad8..abc162af7 100644 --- a/checker/inductive.ml +++ b/checker/inductive.ml @@ -67,7 +67,7 @@ let constructor_instantiate mind mib c = let instantiate_params full t args sign = let fail () = - anomaly "instantiate_params: type, ctxt and args mismatch" in + anomaly ~label:"instantiate_params" (Pp.str "type, ctxt and args mismatch") in let (rem_args, subs, ty) = fold_rel_context (fun (_,copt,_) (largs,subs,ty) -> @@ -778,7 +778,7 @@ let check_one_fix renv recpos def = check_rec_call renv [] a; let renv' = push_var_renv renv (x,a) in check_nested_fix_body renv' (decr-1) recArgsDecrArg b - | _ -> anomaly "Not enough abstractions in fix body" + | _ -> anomaly (Pp.str "Not enough abstractions in fix body") in check_rec_call renv [] def @@ -792,7 +792,7 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) = or Array.length names <> nbfix or bodynum < 0 or bodynum >= nbfix - then anomaly "Ill-formed fix term"; + then anomaly (Pp.str "Ill-formed fix term"); let fixenv = push_rec_types recdef env in let raise_err env i err = error_ill_formed_rec_body env err names i in @@ -813,7 +813,7 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) = raise_err env i (RecursionNotOnInductiveType a) in (mind, (env', b)) else check_occur env' (n+1) b - else anomaly "check_one_fix: Bad occurrence of recursive call" + else anomaly ~label:"check_one_fix" (Pp.str "Bad occurrence of recursive call") | _ -> raise_err env i NotEnoughAbstractionInFixBody in check_occur fixenv 1 def in (* Do it on every fixpoint *) @@ -842,7 +842,7 @@ let check_fix env fix = Profile.profile3 cfkey check_fix env fix;; exception CoFixGuardError of env * guard_error let anomaly_ill_typed () = - anomaly "check_one_cofix: too many arguments applied to constructor" + anomaly ~label:"check_one_cofix" (Pp.str "too many arguments applied to constructor") let rec codomain_is_coind env c = let b = whd_betadeltaiota env c in diff --git a/checker/modops.ml b/checker/modops.ml index f9c52c2e9..6b7a9c7a1 100644 --- a/checker/modops.ml +++ b/checker/modops.ml @@ -90,7 +90,7 @@ and add_module mb env = | SEBstruct (sign) -> add_signature mp sign mb.mod_delta env | SEBfunctor _ -> env - | _ -> anomaly "Modops:the evaluation of the structure failed " + | _ -> anomaly ~label:"Modops" (Pp.str "the evaluation of the structure failed ") let strengthen_const mp_from l cb resolver = @@ -118,7 +118,7 @@ let rec strengthen_mod mp_from mp_to mb = (add_delta_resolver mb.mod_delta resolve_out)*); mod_retroknowledge = mb.mod_retroknowledge} | SEBfunctor _ -> mb - | _ -> anomaly "Modops:the evaluation of the structure failed " + | _ -> anomaly ~label:"Modops" (Pp.str "the evaluation of the structure failed ") and strengthen_sig mp_from sign mp_to resolver = match sign with @@ -152,7 +152,7 @@ let strengthen mtb mp = typ_delta = resolve_out(*add_delta_resolver mtb.typ_delta (add_mp_delta_resolver mtb.typ_mp mp resolve_out)*)} | SEBfunctor _ -> mtb - | _ -> anomaly "Modops:the evaluation of the structure failed " + | _ -> anomaly ~label:"Modops" (Pp.str "the evaluation of the structure failed ") let subst_and_strengthen mb mp = strengthen_mod mb.mod_mp mp (subst_module (map_mp mb.mod_mp mp) mb) diff --git a/checker/reduction.ml b/checker/reduction.ml index c2d5c261c..57e39f9ce 100644 --- a/checker/reduction.ml +++ b/checker/reduction.ml @@ -287,13 +287,13 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) = (* Eta-expansion on the fly *) | (FLambda _, _) -> if v1 <> [] then - anomaly "conversion was given unreduced term (FLambda)"; + anomaly (Pp.str "conversion was given unreduced term (FLambda)"); let (_,_ty1,bd1) = destFLambda mk_clos hd1 in eqappr univ CONV infos (el_lift lft1,(bd1,[])) (el_lift lft2,(hd2,eta_expand_stack v2)) | (_, FLambda _) -> if v2 <> [] then - anomaly "conversion was given unreduced term (FLambda)"; + anomaly (Pp.str "conversion was given unreduced term (FLambda)"); let (_,_ty2,bd2) = destFLambda mk_clos hd2 in eqappr univ CONV infos (el_lift lft1,(hd1,eta_expand_stack v1)) (el_lift lft2,(bd2,[])) @@ -398,7 +398,7 @@ let vm_conv = fconv let hnf_prod_app env t n = match whd_betadeltaiota env t with | Prod (_,_,b) -> subst1 n b - | _ -> anomaly "hnf_prod_app: Need a product" + | _ -> anomaly ~label:"hnf_prod_app" (Pp.str "Need a product") let hnf_prod_applist env t nl = List.fold_left (hnf_prod_app env) t nl diff --git a/checker/term.ml b/checker/term.ml index 6bafeda7f..e7e9c891b 100644 --- a/checker/term.ml +++ b/checker/term.ml @@ -441,7 +441,7 @@ let destArity = | LetIn (x,b,t,c) -> prodec_rec ((x,Some b,t)::l) c | Cast (c,_,_) -> prodec_rec l c | Sort s -> l,s - | _ -> anomaly "destArity: not an arity" + | _ -> anomaly ~label:"destArity" (Pp.str "not an arity") in prodec_rec [] diff --git a/checker/typeops.ml b/checker/typeops.ml index 129c242b9..07c7bc367 100644 --- a/checker/typeops.ml +++ b/checker/typeops.ml @@ -351,10 +351,10 @@ let rec execute env cstr = (* Partial proofs: unsupported by the kernel *) | Meta _ -> - anomaly "the kernel does not support metavariables" + anomaly (Pp.str "the kernel does not support metavariables") | Evar _ -> - anomaly "the kernel does not support existential variables" + anomaly (Pp.str "the kernel does not support existential variables") and execute_type env constr = let j = execute env constr in diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4 index c11ffddbf..4d9904694 100644 --- a/grammar/argextend.ml4 +++ b/grammar/argextend.ml4 @@ -261,8 +261,8 @@ let declare_vernac_argument loc s pr cl = (None, [(None, None, $rules$)]); Pptactic.declare_extra_genarg_pprule ($rawwit$, $pr_rules$) - ($globwit$, fun _ _ _ _ -> Errors.anomaly "vernac argument needs not globwit printer") - ($wit$, fun _ _ _ _ -> Errors.anomaly "vernac argument needs not wit printer") } + ($globwit$, fun _ _ _ _ -> Errors.anomaly (Pp.str "vernac argument needs not globwit printer")) + ($wit$, fun _ _ _ _ -> Errors.anomaly (Pp.str "vernac argument needs not wit printer")) } >> ] open Pcoq diff --git a/grammar/q_util.ml4 b/grammar/q_util.ml4 index eee84c38d..34f1cf6cb 100644 --- a/grammar/q_util.ml4 +++ b/grammar/q_util.ml4 @@ -59,6 +59,6 @@ let rec mlexpr_of_prod_entry_key = function | Pcoq.Aself -> <:expr< Pcoq.Aself >> | Pcoq.Anext -> <:expr< Pcoq.Anext >> | Pcoq.Atactic n -> <:expr< Pcoq.Atactic $mlexpr_of_int n$ >> - | Pcoq.Agram s -> Errors.anomaly "Agram not supported" + | Pcoq.Agram s -> Errors.anomaly (Pp.str "Agram not supported") | Pcoq.Aentry ("",s) -> <:expr< Pcoq.Agram (Pcoq.Gram.Entry.obj $lid:s$) >> | Pcoq.Aentry (u,s) -> <:expr< Pcoq.Aentry $str:u$ $str:s$ >> diff --git a/interp/constrextern.ml b/interp/constrextern.ml index e8e76809c..e2d40f23f 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -629,7 +629,7 @@ let rec extern inctx scopes vars r = | None :: q -> raise No_match | Some c :: q -> match locs with - | [] -> anomaly "projections corruption [Constrextern.extern]" + | [] -> anomaly (Pp.str "projections corruption [Constrextern.extern]") | (_, false) :: locs' -> (* we don't want to print locals *) ip q locs' args acc @@ -932,7 +932,7 @@ let rec glob_of_pat env = function let id = try match lookup_name_of_rel n env with | Name id -> id | Anonymous -> - anomaly "glob_constr_of_pattern: index to an anonymous variable" + anomaly ~label:"glob_constr_of_pattern" (Pp.str "index to an anonymous variable") with Not_found -> Id.of_string ("_UNBOUND_REL_"^(string_of_int n)) in GVar (loc,id) | PMeta None -> GHole (loc,Evar_kinds.InternalHole) @@ -960,7 +960,7 @@ let rec glob_of_pat env = function | _, Some ind -> let bl' = List.map (fun (i,n,c) -> (i,n,glob_of_pat env c)) bl in simple_cases_matrix_of_branches ind bl' - | _, None -> anomaly "PCase with some branches but unknown inductive" + | _, None -> anomaly (Pp.str "PCase with some branches but unknown inductive") in let mat = if info.cip_extensible then mat @ [any_any_branch] else mat in @@ -968,7 +968,7 @@ let rec glob_of_pat env = function | PMeta None, _, _ -> (Anonymous,None),None | _, Some ind, Some nargs -> return_type_of_predicate ind nargs (glob_of_pat env p) - | _ -> anomaly "PCase with non-trivial predicate but unknown inductive" + | _ -> anomaly (Pp.str "PCase with non-trivial predicate but unknown inductive") in GCases (loc,RegularStyle,rtn,[glob_of_pat env tm,indnames],mat) | PFix f -> Detyping.detype false [] env (mkFix f) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 79c67165d..2afd33bab 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -316,7 +316,7 @@ let rec it_mkGLambda loc2 env body = let build_impls = function |Implicit -> (function |Name id -> Some (id, Impargs.Manual, (true,true)) - |Anonymous -> anomaly "Anonymous implicit argument") + |Anonymous -> anomaly (Pp.str "Anonymous implicit argument")) |Explicit -> fun _ -> None let impls_type_list ?(args = []) = @@ -543,7 +543,7 @@ let subst_aconstr_in_glob_constr loc intern lvar subst infos c = (aux ((x,(a,(scopt,subscopes)))::terms,binderopt) subinfos iter)) (if lassoc then List.rev l else l) termin with Not_found -> - anomaly "Inconsistent substitution of recursive notation") + anomaly (Pp.str "Inconsistent substitution of recursive notation")) | NHole (Evar_kinds.BinderType (Name id as na)) -> let na = try snd (coerce_to_name (fst (List.assoc id terms))) @@ -562,7 +562,7 @@ let subst_aconstr_in_glob_constr loc intern lvar subst infos c = termin bl in make_letins letins res with Not_found -> - anomaly "Inconsistent substitution of recursive notation") + anomaly (Pp.str "Inconsistent substitution of recursive notation")) | NProd (Name id, NHole _, c') when option_mem_assoc id binderopt -> let (loc,(na,bk,t)),letins = snd (Option.get binderopt) in GProd (loc,na,bk,t,make_letins letins (aux subst' infos c')) @@ -855,7 +855,7 @@ let chop_params_pattern loc ind args with_letin = let find_constructor loc add_params ref = let cstr = (function ConstructRef cstr -> cstr |IndRef _ -> user_err_loc (loc,"find_constructor",str "There is an inductive name deep in a \"in\" clause.") - |_ -> anomaly "unexpected global_reference in pattern") ref in + |_ -> anomaly (Pp.str "unexpected global_reference in pattern")) ref in cstr, (function (ind,_ as c) -> match add_params with |Some nb_args -> let nb = if Int.equal nb_args (Inductiveops.constructor_nrealhyps c) then fst (Inductiveops.inductive_nargs ind) @@ -890,7 +890,7 @@ let sort_fields mode loc l completer = | [] -> (i, acc) | (Some name) :: b-> (match m with - | [] -> anomaly "Number of projections mismatch" + | [] -> anomaly (Pp.str "Number of projections mismatch") | (_, regular)::tm -> let boolean = not regular in begin match global_reference_of_reference refer with @@ -914,7 +914,7 @@ let sort_fields mode loc l completer = (record.Recordops.s_EXPECTEDPARAM, Qualid (loc, shortest_qualid_of_global Id.Set.empty (ConstructRef ind)), build_patt record.Recordops.s_PROJ record.Recordops.s_PROJKIND 1 (0,[])) - with Not_found -> anomaly "Environment corruption for records." + with Not_found -> anomaly (Pp.str "Environment corruption for records.") in (* now we want to have all fields of the pattern indexed by their place in the constructor *) @@ -1099,7 +1099,7 @@ let drop_notations_pattern looked_for = tmp_scope = scopt} a with Not_found -> if Id.equal id ldots_var then RCPatAtom (loc,Some id) else - anomaly ("Unbound pattern notation variable: "^(Id.to_string id)) + anomaly (str "Unbound pattern notation variable: " ++ Id.print id) end | NRef g -> ensure_kind top g; @@ -1122,7 +1122,7 @@ let drop_notations_pattern looked_for = subst_pat_iterator ldots_var t u) (if lassoc then List.rev l else l) termin with Not_found -> - anomaly "Inconsistent substitution of recursive notation") + anomaly (Pp.str "Inconsistent substitution of recursive notation")) | NHole _ -> let () = assert (List.is_empty args) in RCPatAtom (loc, None) @@ -1224,7 +1224,7 @@ let get_implicit_name n imps = let set_hole_implicit i b = function | GRef (loc,r) | GApp (_,GRef (loc,r),_) -> (loc,Evar_kinds.ImplicitArg (r,i,b)) | GVar (loc,id) -> (loc,Evar_kinds.ImplicitArg (VarRef id,i,b)) - | _ -> anomaly "Only refs have implicits" + | _ -> anomaly (Pp.str "Only refs have implicits") let exists_implicit_name id = List.exists (fun imp -> is_status_implicit imp && Id.equal id (name_of_implicit imp)) diff --git a/interp/coqlib.ml b/interp/coqlib.ml index a047a762b..92a268796 100644 --- a/interp/coqlib.ml +++ b/interp/coqlib.ml @@ -26,7 +26,7 @@ let make_dir l = Dir_path.make (List.map Id.of_string (List.rev l)) let find_reference locstr dir s = let sp = Libnames.make_path (make_dir dir) (Id.of_string s) in try global_of_extended_global (Nametab.extended_global_of_path sp) - with Not_found -> anomaly (locstr^": cannot find "^(string_of_path sp)) + with Not_found -> anomaly ~label:locstr (str "cannot find " ++ Libnames.pr_path sp) let coq_reference locstr dir s = find_reference locstr ("Coq"::dir) s let coq_constant locstr dir s = constr_of_global (coq_reference locstr dir s) @@ -50,12 +50,12 @@ let gen_constant_in_modules locstr dirs s = match these with | [x] -> constr_of_global x | [] -> - anomalylabstrm "" (str (locstr^": cannot find "^s^ + anomaly ~label:locstr (str ("cannot find "^s^ " in module"^(if List.length dirs > 1 then "s " else " ")) ++ prlist_with_sep pr_comma pr_dirpath dirs) | l -> - anomalylabstrm "" - (str (locstr^": found more than once object of name "^s^ + anomaly ~label:locstr + (str ("found more than once object of name "^s^ " in module"^(if List.length dirs > 1 then "s " else " ")) ++ prlist_with_sep pr_comma pr_dirpath dirs) @@ -183,7 +183,7 @@ let build_bool_type () = andb_prop = init_constant ["Datatypes"] "andb_prop"; andb_true_intro = init_constant ["Datatypes"] "andb_true_intro" } -let build_sigma_set () = anomaly "Use build_sigma_type" +let build_sigma_set () = anomaly (Pp.str "Use build_sigma_type") let build_sigma_type () = { proj1 = init_constant ["Specif"] "projT1"; @@ -369,7 +369,7 @@ let coq_eq_ref = lazy (init_reference ["Logic"] "eq") let coq_identity_ref = lazy (init_reference ["Datatypes"] "identity") let coq_jmeq_ref = lazy (gen_reference "Coqlib" ["Logic";"JMeq"] "JMeq") let coq_eq_true_ref = lazy (gen_reference "Coqlib" ["Init";"Datatypes"] "eq_true") -let coq_existS_ref = lazy (anomaly "use coq_existT_ref") +let coq_existS_ref = lazy (anomaly (Pp.str "use coq_existT_ref")) let coq_existT_ref = lazy (init_reference ["Specif"] "existT") let coq_exist_ref = lazy (init_reference ["Specif"] "exist") let coq_not_ref = lazy (init_reference ["Logic"] "not") diff --git a/interp/genarg.ml b/interp/genarg.ml index 382c38da3..a029a3b31 100644 --- a/interp/genarg.ml +++ b/interp/genarg.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Pp open Util open Glob_term open Constrexpr @@ -238,7 +239,7 @@ type ('a,'b) abstract_argument_type = argument_type let create_arg v s = if List.mem_assoc s !dyntab then - Errors.anomaly ("Genarg.create: already declared generic argument " ^ s); + Errors.anomaly ~label:"Genarg.create" (str ("already declared generic argument " ^ s)); let t = ExtraArgType s in dyntab := (s,Option.map (in_gen t) v) :: !dyntab; (t,t,t) diff --git a/interp/notation.ml b/interp/notation.ml index 39a664a64..ac71e1ebd 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -337,7 +337,7 @@ let rec find_without_delimiters find (ntn_scope,ntn) = function let declare_notation_level ntn level = if Gmap.mem ntn !notation_level_map then - anomaly ("Notation "^ntn^" is already assigned a level"); + anomaly (str "Notation " ++ str ntn ++ str " is already assigned a level"); notation_level_map := Gmap.add ntn level !notation_level_map let level_of_notation ntn = @@ -887,7 +887,7 @@ let declare_notation_printing_rule ntn unpl = let find_notation_printing_rule ntn = try Gmap.find ntn !printing_rules - with Not_found -> anomaly ("No printing rule found for "^ntn) + with Not_found -> anomaly (str "No printing rule found for " ++ str ntn) (**********************************************************************) (* Synchronisation with reset *) diff --git a/kernel/closure.ml b/kernel/closure.ml index 1630cff38..b22dd42e7 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -797,7 +797,7 @@ let rec drop_parameters depth n argstk = | [] -> (* we know that n < stack_args_size(argstk) (if well-typed term) *) if Int.equal n 0 then [] else anomaly - "ill-typed term: found a match on a partially applied constructor" + (Pp.str "ill-typed term: found a match on a partially applied constructor") | _ -> assert false (* strip_update_shift_app only produces Zapp and Zshift items *) diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 6c22db3a2..4fde7474b 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -26,7 +26,7 @@ open Environ type work_list = Id.t array Cmap.t * Id.t array Mindmap.t let pop_dirpath p = match Dir_path.repr p with - | [] -> anomaly "dirpath_prefix: empty dirpath" + | [] -> anomaly ~label:"dirpath_prefix" (Pp.str "empty dirpath") | _::l -> Dir_path.make l let pop_mind kn = diff --git a/kernel/environ.ml b/kernel/environ.ml index 27b7c76b4..a36e2dcf6 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -460,13 +460,13 @@ fun env field value -> match value with | Const kn -> retroknowledge add_int31_op env value 2 op kn - | _ -> anomaly "Environ.register: should be a constant" + | _ -> anomaly ~label:"Environ.register" (Pp.str "should be a constant") in let add_int31_unop_from_const op = match value with | Const kn -> retroknowledge add_int31_op env value 1 op kn - | _ -> anomaly "Environ.register: should be a constant" + | _ -> anomaly ~label:"Environ.register" (Pp.str "should be a constant") in (* subfunction which completes the function constr_of_int31 above by performing the actual retroknowledge operations *) @@ -481,9 +481,9 @@ fun env field value -> | Ind i31t -> Retroknowledge.add_vm_decompile_constant_info rk value (constr_of_int31 i31t i31bit_type) - | _ -> anomaly "Environ.register: should be an inductive type") - | _ -> anomaly "Environ.register: Int31Bits should be an inductive type") - | _ -> anomaly "Environ.register: add_int31_decompilation_from_type called with an abnormal field" + | _ -> anomaly ~label:"Environ.register" (Pp.str "should be an inductive type")) + | _ -> anomaly ~label:"Environ.register" (Pp.str "Int31Bits should be an inductive type")) + | _ -> anomaly ~label:"Environ.register" (Pp.str "add_int31_decompilation_from_type called with an abnormal field") in {env with retroknowledge = let retroknowledge_with_reactive_info = @@ -491,7 +491,7 @@ fun env field value -> | KInt31 (_, Int31Type) -> let i31c = match value with | Ind i31t -> (Construct (i31t, 1)) - | _ -> anomaly "Environ.register: should be an inductive type" + | _ -> anomaly ~label:"Environ.register" (Pp.str "should be an inductive type") in add_int31_decompilation_from_type (add_vm_before_match_info @@ -511,14 +511,14 @@ fun env field value -> | Const kn -> retroknowledge add_int31_op env value 3 Cbytecodes.Kdiv21int31 kn - | _ -> anomaly "Environ.register: should be a constant") + | _ -> anomaly ~label:"Environ.register" (Pp.str "should be a constant")) | KInt31 (_, Int31Div) -> add_int31_binop_from_const Cbytecodes.Kdivint31 | KInt31 (_, Int31AddMulDiv) -> (* this is a ternary operation *) (match value with | Const kn -> retroknowledge add_int31_op env value 3 Cbytecodes.Kaddmuldivint31 kn - | _ -> anomaly "Environ.register: should be a constant") + | _ -> anomaly ~label:"Environ.register" (Pp.str "should be a constant")) | KInt31 (_, Int31Compare) -> add_int31_binop_from_const Cbytecodes.Kcompareint31 | KInt31 (_, Int31Head0) -> add_int31_unop_from_const Cbytecodes.Khead0int31 | KInt31 (_, Int31Tail0) -> add_int31_unop_from_const Cbytecodes.Ktail0int31 diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 165af63cf..357a48080 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -180,7 +180,7 @@ let infer_constructor_packet env_ar_par params lc = conditions. *) let typecheck_inductive env mie = let () = match mie.mind_entry_inds with - | [] -> anomaly "empty inductive types declaration" + | [] -> anomaly (Pp.str "empty inductive types declaration") | _ -> () in (* Check unicity of names *) @@ -327,11 +327,11 @@ let failwith_non_pos n ntypes c = let failwith_non_pos_vect n ntypes v = Array.iter (failwith_non_pos n ntypes) v; - anomaly "failwith_non_pos_vect: some k in [n;n+ntypes-1] should occur" + anomaly ~label:"failwith_non_pos_vect" (Pp.str "some k in [n;n+ntypes-1] should occur") let failwith_non_pos_list n ntypes l = List.iter (failwith_non_pos n ntypes) l; - anomaly "failwith_non_pos_list: some k in [n;n+ntypes-1] should occur" + anomaly ~label:"failwith_non_pos_list" (Pp.str "some k in [n;n+ntypes-1] should occur") (* Check the inductive type is called with the expected parameters *) let check_correct_par (env,n,ntypes,_) hyps l largs = diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 740ac8c13..31d9f48ac 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -63,7 +63,7 @@ let constructor_instantiate mind mib c = let instantiate_params full t args sign = let fail () = - anomaly "instantiate_params: type, ctxt and args mismatch" in + anomaly ~label:"instantiate_params" (Pp.str "type, ctxt and args mismatch") in let (rem_args, subs, ty) = Sign.fold_rel_context (fun (_,copt,_) (largs,subs,ty) -> @@ -777,7 +777,7 @@ let check_one_fix renv recpos def = check_rec_call renv [] a; let renv' = push_var_renv renv (x,a) in check_nested_fix_body renv' (decr-1) recArgsDecrArg b - | _ -> anomaly "Not enough abstractions in fix body" + | _ -> anomaly (Pp.str "Not enough abstractions in fix body") in check_rec_call renv [] def @@ -793,7 +793,7 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) = || not (Int.equal (Array.length names) nbfix) || bodynum < 0 || bodynum >= nbfix - then anomaly "Ill-formed fix term"; + then anomaly (Pp.str "Ill-formed fix term"); let fixenv = push_rec_types recdef env in let vdefj = judgment_of_fixpoint recdef in let raise_err env i err = @@ -815,7 +815,7 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) = raise_err env i (RecursionNotOnInductiveType a) in (mind, (env', b)) else check_occur env' (n+1) b - else anomaly "check_one_fix: Bad occurrence of recursive call" + else anomaly ~label:"check_one_fix" (Pp.str "Bad occurrence of recursive call") | _ -> raise_err env i NotEnoughAbstractionInFixBody in check_occur fixenv 1 def in (* Do it on every fixpoint *) @@ -845,7 +845,7 @@ let check_fix env fix = Profile.profile3 cfkey check_fix env fix;; exception CoFixGuardError of env * guard_error let anomaly_ill_typed () = - anomaly "check_one_cofix: too many arguments applied to constructor" + anomaly ~label:"check_one_cofix" (Pp.str "too many arguments applied to constructor") let rec codomain_is_coind env c = let b = whd_betadeltaiota env c in diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index 0d29cf10b..b566dd8af 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -229,7 +229,7 @@ and check_with_mod env sign (idl,mp1) mp equiv = and translate_module env mp inl me = match me.mod_entry_expr, me.mod_entry_type with | None, None -> - anomaly "Mod_typing.translate_module: empty type and expr in module entry" + anomaly ~label:"Mod_typing.translate_module" (Pp.str "empty type and expr in module entry") | None, Some mte -> let mtb = translate_module_type env mp inl mte in { mod_mp = mp; diff --git a/kernel/modops.ml b/kernel/modops.ml index e13586689..e247a5712 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -244,7 +244,7 @@ let add_retroknowledge mp = (match e with | Const kn -> kind_of_term (mkConst kn) | Ind ind -> kind_of_term (mkInd ind) - | _ -> anomaly "Modops.add_retroknowledge: had to import an unsupported kind of term") + | _ -> anomaly ~label:"Modops.add_retroknowledge" (Pp.str "had to import an unsupported kind of term")) in fun lclrk env -> (* The order of the declaration matters, for instance (and it's at the @@ -278,7 +278,7 @@ and add_module mb env = add_retroknowledge mp mb.mod_retroknowledge (add_signature mp sign mb.mod_delta env) | SEBfunctor _ -> env - | _ -> anomaly "Modops:the evaluation of the structure failed " + | _ -> anomaly ~label:"Modops" (Pp.str "the evaluation of the structure failed ") let strengthen_const mp_from l cb resolver = match cb.const_body with @@ -308,7 +308,7 @@ let rec strengthen_mod mp_from mp_to mb = (add_delta_resolver mb.mod_delta resolve_out); mod_retroknowledge = mb.mod_retroknowledge} | SEBfunctor _ -> mb - | _ -> anomaly "Modops:the evaluation of the structure failed " + | _ -> anomaly ~label:"Modops" (Pp.str "the evaluation of the structure failed ") and strengthen_sig mp_from sign mp_to resolver = match sign with @@ -345,7 +345,7 @@ let strengthen mtb mp = typ_delta = add_delta_resolver mtb.typ_delta (add_mp_delta_resolver mtb.typ_mp mp resolve_out)} | SEBfunctor _ -> mtb - | _ -> anomaly "Modops:the evaluation of the structure failed " + | _ -> anomaly ~label:"Modops" (Pp.str "the evaluation of the structure failed ") let module_type_of_module mp mb = match mp with @@ -408,7 +408,7 @@ let rec strengthen_and_subst_mod subst_module subst (fun resolver subst-> subst_dom_codom_delta_resolver subst resolver) mb - | _ -> anomaly "Modops:the evaluation of the structure failed " + | _ -> anomaly ~label:"Modops" (Pp.str "the evaluation of the structure failed ") and strengthen_and_subst_struct str subst mp_alias mp_from mp_to alias incl resolver = @@ -518,7 +518,7 @@ let strengthen_and_subst_mb mb mp include_b = let subst = map_mp mb.mod_mp mp empty_delta_resolver in subst_module subst (fun resolver subst -> subst_dom_codom_delta_resolver subst resolver) mb - | _ -> anomaly "Modops:the evaluation of the structure failed " + | _ -> anomaly ~label:"Modops" (Pp.str "the evaluation of the structure failed ") let subst_modtype_and_resolver mtb mp = @@ -572,7 +572,7 @@ let rec collect_mbid l = function | SEBstruct str as s-> let str_clean = Util.List.smartmap (clean_struct l) str in if str_clean == str then s else SEBstruct(str_clean) - | _ -> anomaly "Modops:the evaluation of the structure failed " + | _ -> anomaly ~label:"Modops" (Pp.str "the evaluation of the structure failed ") let clean_bounded_mod_expr = function diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index 4e78d2bd4..6b9247476 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -112,32 +112,32 @@ type symbol = let get_value tbl i = match tbl.(i) with | SymbValue v -> v - | _ -> anomaly "get_value failed" + | _ -> anomaly (Pp.str "get_value failed") let get_sort tbl i = match tbl.(i) with | SymbSort s -> s - | _ -> anomaly "get_sort failed" + | _ -> anomaly (Pp.str "get_sort failed") let get_name tbl i = match tbl.(i) with | SymbName id -> id - | _ -> anomaly "get_name failed" + | _ -> anomaly (Pp.str "get_name failed") let get_const tbl i = match tbl.(i) with | SymbConst kn -> kn - | _ -> anomaly "get_const failed" + | _ -> anomaly (Pp.str "get_const failed") let get_match tbl i = match tbl.(i) with | SymbMatch case_info -> case_info - | _ -> anomaly "get_match failed" + | _ -> anomaly (Pp.str "get_match failed") let get_ind tbl i = match tbl.(i) with | SymbInd ind -> ind - | _ -> anomaly "get_ind failed" + | _ -> anomaly (Pp.str "get_ind failed") let symbols_list = ref ([] : symbol list) diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml index 4ba305660..1c931ab85 100644 --- a/kernel/nativeconv.ml +++ b/kernel/nativeconv.ml @@ -148,6 +148,6 @@ let native_conv pb env t1 t2 = (* TODO change 0 when we can have deBruijn *) conv_val pb 0 !rt1 !rt2 empty_constraint end - | _ -> anomaly "Compilation failure" + | _ -> anomaly (Pp.str "Compilation failure") let _ = set_nat_conv native_conv diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml index 86fe45bdc..09202f6a7 100644 --- a/kernel/nativelib.ml +++ b/kernel/nativelib.ml @@ -19,7 +19,7 @@ open Envars used by the native compiler. *) let get_load_paths = - ref (fun _ -> anomaly "get_load_paths not initialized" : unit -> string list) + ref (fun _ -> anomaly (Pp.str "get_load_paths not initialized") : unit -> string list) let open_header = ["Nativevalues"; "Nativecode"; @@ -85,7 +85,7 @@ let call_linker ~fatal prefix f upds = register_native_file prefix with | Dynlink.Error e -> let msg = "Dynlink error, " ^ Dynlink.error_message e in - if fatal then anomaly msg else Pp.msg_warning (Pp.str msg) + if fatal then anomaly (Pp.str msg) else Pp.msg_warning (Pp.str msg) | _ -> let msg = "Dynlink error" in - if fatal then anomaly msg else Pp.msg_warning (Pp.str msg)); + if fatal then anomaly (Pp.str msg) else Pp.msg_warning (Pp.str msg)); match upds with Some upds -> update_locations upds | _ -> () diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml index fc4255aaf..2f317ca96 100644 --- a/kernel/nativevalues.ml +++ b/kernel/nativevalues.ml @@ -195,7 +195,8 @@ let mk_block tag args = (* Two instances of dummy_value should not be pointer equal, otherwise comparing them as terms would succeed *) -let dummy_value : unit -> t = fun () _ -> anomaly "Evaluation failed" +let dummy_value : unit -> t = + fun () _ -> anomaly ~label:"native" (Pp.str "Evaluation failed") let cast_accu v = (Obj.magic v:accumulator) diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 6a7248749..7a14e57cc 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -133,7 +133,7 @@ let betazeta_appvect n c v = match kind_of_term t, stack with Lambda(_,_,c), arg::stacktl -> stacklam (n-1) (arg::env) c stacktl | LetIn(_,b,_,c), _ -> stacklam (n-1) (b::env) c stack - | _ -> anomaly "Not enough lambda/let's" in + | _ -> anomaly (Pp.str "Not enough lambda/let's") in stacklam n [] c (Array.to_list v) (********************************************************************) @@ -267,7 +267,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = (match kind_of_term a1, kind_of_term a2 with | (Sort s1, Sort s2) -> if not (is_empty_stack v1 && is_empty_stack v2) then - anomaly "conversion was given ill-typed terms (Sort)"; + anomaly (Pp.str "conversion was given ill-typed terms (Sort)"); sort_cmp cv_pb s1 s2 cuniv | (Meta n, Meta m) -> if Int.equal n m @@ -318,7 +318,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = (* Inconsistency: we tolerate that v1, v2 contain shift and update but we throw them away *) if not (is_empty_stack v1 && is_empty_stack v2) then - anomaly "conversion was given ill-typed terms (FLambda)"; + anomaly (Pp.str "conversion was given ill-typed terms (FLambda)"); let (_,ty1,bd1) = destFLambda mk_clos hd1 in let (_,ty2,bd2) = destFLambda mk_clos hd2 in let u1 = ccnv CONV l2r infos el1 el2 ty1 ty2 cuniv in @@ -326,7 +326,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = | (FProd (_,c1,c2), FProd (_,c'1,c'2)) -> if not (is_empty_stack v1 && is_empty_stack v2) then - anomaly "conversion was given ill-typed terms (FProd)"; + anomaly (Pp.str "conversion was given ill-typed terms (FProd)"); (* Luo's system *) let u1 = ccnv CONV l2r infos el1 el2 c1 c'1 cuniv in ccnv cv_pb l2r infos (el_lift el1) (el_lift el2) c2 c'2 u1 @@ -336,7 +336,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = let () = match v1 with | [] -> () | _ -> - anomaly "conversion was given unreduced term (FLambda)" + anomaly (Pp.str "conversion was given unreduced term (FLambda)") in let (_,_ty1,bd1) = destFLambda mk_clos hd1 in eqappr CONV l2r infos @@ -345,7 +345,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = let () = match v2 with | [] -> () | _ -> - anomaly "conversion was given unreduced term (FLambda)" + anomaly (Pp.str "conversion was given unreduced term (FLambda)") in let (_,_ty2,bd2) = destFLambda mk_clos hd2 in eqappr CONV l2r infos @@ -520,7 +520,7 @@ let conv env t1 t2 = let hnf_prod_app env t n = match kind_of_term (whd_betadeltaiota env t) with | Prod (_,_,b) -> subst1 n b - | _ -> anomaly "hnf_prod_app: Need a product" + | _ -> anomaly ~label:"hnf_prod_app" (Pp.str "Need a product") let hnf_prod_applist env t nl = List.fold_left (hnf_prod_app env) t nl diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index a8c850ecd..2e21a86ff 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -286,14 +286,14 @@ let add_constant dir l decl senv = let add_mind dir l mie senv = let () = match mie.mind_entry_inds with | [] -> - anomaly "empty inductive types declaration" + anomaly (Pp.str "empty inductive types declaration") (* this test is repeated by translate_mind *) | _ -> () in let id = (List.nth mie.mind_entry_inds 0).mind_entry_typename in if not (Label.equal l (Label.of_id id)) then - anomaly ("the label of inductive packet and its first inductive"^ - " type do not match"); + anomaly (Pp.str "the label of inductive packet and its first inductive \ + type do not match"); let kn = make_mind senv.modinfo.modpath dir l in let mib = translate_mind senv.env kn mie in let mib = match mib.mind_hyps with [] -> hcons_mind mib | _ -> mib in @@ -499,7 +499,7 @@ let end_module l restype senv = let add_module_parameter mbid mte inl senv = let () = match senv.revstruct, senv.loads with | [], _ :: _ | _ :: _, [] -> - anomaly "Cannot add a module parameter to a non empty module" + anomaly (Pp.str "Cannot add a module parameter to a non empty module") | _ -> () in let mtb = translate_module_type senv.env (MPbound mbid) inl mte in @@ -510,7 +510,7 @@ let add_module_parameter mbid mte inl senv = | STRUCT params -> STRUCT ((mbid,mtb) :: params) | SIG params -> SIG ((mbid,mtb) :: params) | _ -> - anomaly "Module parameters can only be added to modules or signatures" + anomaly (Pp.str "Module parameters can only be added to modules or signatures") in let resolver_of_param = match mtb.typ_expr with @@ -644,10 +644,10 @@ let is_empty senv = match senv.revstruct, senv.modinfo.variant with let start_library dir senv = if not (is_empty senv) then - anomaly "Safe_typing.start_library: environment should be empty"; + anomaly ~label:"Safe_typing.start_library" (Pp.str "environment should be empty"); let dir_path,l = match (Dir_path.repr dir) with - [] -> anomaly "Empty dirpath in Safe_typing.start_library" + [] -> anomaly (Pp.str "Empty dirpath in Safe_typing.start_library") | hd::tl -> Dir_path.make tl, Label.of_id hd in @@ -686,9 +686,9 @@ let export senv dir = match modinfo.variant with | LIBRARY dp -> if not (Dir_path.equal dir dp) then - anomaly "We are not exporting the right library!" + anomaly (Pp.str "We are not exporting the right library!") | _ -> - anomaly "We are not exporting the library" + anomaly (Pp.str "We are not exporting the library") end; (*if senv.modinfo.params <> [] || senv.modinfo.restype <> None then (* error_export_simple *) (); *) diff --git a/kernel/term.ml b/kernel/term.ml index e4657ce28..93e870015 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -407,7 +407,7 @@ let isConstruct c = match kind_of_term c with Construct _ -> true | _ -> false (* Destructs a term <p>Case c of lc1 | lc2 .. | lcn end *) let destCase c = match kind_of_term c with | Case (ci,p,c,v) -> (ci,p,c,v) - | _ -> anomaly "destCase" + | _ -> invalid_arg "destCase" let isCase c = match kind_of_term c with Case _ -> true | _ -> false @@ -1160,7 +1160,7 @@ let destArity = | LetIn (x,b,t,c) -> prodec_rec ((x,Some b,t)::l) c | Cast (c,_,_) -> prodec_rec l c | Sort s -> l,s - | _ -> anomaly "destArity: not an arity" + | _ -> anomaly ~label:"destArity" (Pp.str "not an arity") in prodec_rec [] diff --git a/kernel/typeops.ml b/kernel/typeops.ml index e61168200..efc7a4ee8 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -466,10 +466,10 @@ let rec execute env cstr cu = (* Partial proofs: unsupported by the kernel *) | Meta _ -> - anomaly "the kernel does not support metavariables" + anomaly (Pp.str "the kernel does not support metavariables") | Evar _ -> - anomaly "the kernel does not support existential variables" + anomaly (Pp.str "the kernel does not support existential variables") and execute_type env constr cu = let (j,cu1) = execute env constr cu in diff --git a/kernel/univ.ml b/kernel/univ.ml index 71b417624..cfb704932 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -143,8 +143,8 @@ let super = function | Atom u -> Max ([],[u]) | Max _ -> - anomaly ("Cannot take the successor of a non variable universe:\n"^ - "(maybe a bugged tactic)") + anomaly (str "Cannot take the successor of a non variable universe" ++ spc () ++ + str "(maybe a bugged tactic)") (* Returns the formal universe that is greater than the universes u and v. Used to type the products. *) @@ -224,8 +224,8 @@ let repr g u = let rec repr_rec u = let a = try UniverseLMap.find u g - with Not_found -> anomalylabstrm "Univ.repr" - (str"Universe " ++ pr_uni_level u ++ str" undefined") + with Not_found -> anomaly ~label:"Univ.repr" + (str "Universe" ++ spc () ++ pr_uni_level u ++ spc () ++ str "undefined") in match a with | Equiv v -> repr_rec v @@ -432,7 +432,7 @@ let check_eq g u v = (* TODO: remove elements of lt in le! *) compare_list (check_equal g) ule vle && compare_list (check_equal g) ult vlt - | _ -> anomaly "check_eq" (* not complete! (Atom(u) = Max([u],[]) *) + | _ -> anomaly (str "check_eq") (* not complete! (Atom(u) = Max([u],[]) *) let check_leq g u v = match u,v with @@ -440,7 +440,7 @@ let check_leq g u v = | Max(le,lt), Atom vl -> List.for_all (fun ul -> check_smaller g false ul vl) le && List.for_all (fun ul -> check_smaller g true ul vl) lt - | _ -> anomaly "check_leq" + | _ -> anomaly (str "check_leq") (** Enforcing new constraints : [setlt], [setleq], [merge], [merge_disc] *) @@ -483,7 +483,7 @@ let merge g arcu arcv = else (max_rank, old_max_rank, best_arc, arc::rest) in match between g arcu arcv with - | [] -> anomaly "Univ.between" + | [] -> anomaly (str "Univ.between") | arc::rest -> let (max_rank, old_max_rank, best_arc, rest) = List.fold_left best_ranked (arc.rank, min_int, arc, []) rest in @@ -540,7 +540,7 @@ let enforce_univ_leq u v g = | LT p -> error_inconsistency Le u v (List.rev p) | LE _ -> merge g arcv arcu | NLE -> fst (setleq g arcu arcv) - | EQ -> anomaly "Univ.compare" + | EQ -> anomaly (Pp.str "Univ.compare") (* enforc_univ_eq : UniverseLevel.t -> UniverseLevel.t -> unit *) (* enforc_univ_eq u v will force u=v if possible, will fail otherwise *) @@ -556,7 +556,7 @@ let enforce_univ_eq u v g = | LT p -> error_inconsistency Eq u v (List.rev p) | LE _ -> merge g arcv arcu | NLE -> merge_disc g arcu arcv - | EQ -> anomaly "Univ.compare") + | EQ -> anomaly (Pp.str "Univ.compare")) (* enforce_univ_lt u v will force u<v if possible, will fail otherwise *) let enforce_univ_lt u v g = @@ -569,7 +569,7 @@ let enforce_univ_lt u v g = | NLE -> (match compare_neq false g arcv arcu with NLE -> fst (setlt g arcu arcv) - | EQ -> anomaly "Univ.compare" + | EQ -> anomaly (Pp.str "Univ.compare") | (LE p|LT p) -> error_inconsistency Lt u v (List.rev p)) (* Constraints and sets of consrtaints. *) @@ -615,14 +615,14 @@ let enforce_leq u v c = | Max (gel,gtl), Atom v -> let d = List.fold_right (fun u -> constraint_add_leq u v) gel c in List.fold_right (fun u -> Constraint.add (u,Lt,v)) gtl d - | _ -> anomaly "A universe bound can only be a variable" + | _ -> anomaly (Pp.str "A universe bound can only be a variable") let enforce_eq u v c = match (u,v) with | Atom u, Atom v -> (* We discard trivial constraints like u=u *) if UniverseLevel.equal u v then c else Constraint.add (u,Eq,v) c - | _ -> anomaly "A universe comparison can only happen between variables" + | _ -> anomaly (Pp.str "A universe comparison can only happen between variables") let merge_constraints c g = Constraint.fold enforce_constraint c g @@ -876,7 +876,7 @@ let is_direct_sort_constraint s v = match s with let solve_constraints_system levels level_bounds = let levels = - Array.map (Option.map (function Atom u -> u | _ -> anomaly "expects Atom")) + Array.map (Option.map (function Atom u -> u | _ -> anomaly (Pp.str "expects Atom"))) levels in let v = Array.copy level_bounds in let nind = Array.length v in @@ -899,7 +899,7 @@ let subst_large_constraint u u' v = if is_direct_constraint u v then sup u' (remove_large_constraint u v) else v | _ -> - anomaly "expect a universe level" + anomaly (Pp.str "expect a universe level") let subst_large_constraints = List.fold_right (fun (u,u') -> subst_large_constraint u u') @@ -910,7 +910,7 @@ let no_upper_constraints u cst = let test (u1, _, _) = not (Int.equal (UniverseLevel.compare u1 u) 0) in Constraint.for_all test cst - | Max _ -> anomaly "no_upper_constraints" + | Max _ -> anomaly (Pp.str "no_upper_constraints") (* Is u mentionned in v (or equals to v) ? *) @@ -918,7 +918,7 @@ let univ_depends u v = match u, v with | Atom u, Atom v -> UniverseLevel.equal u v | Atom u, Max (gel,gtl) -> List.mem u gel || List.mem u gtl - | _ -> anomaly "univ_depends given a non-atomic 1st arg" + | _ -> anomaly (Pp.str "univ_depends given a non-atomic 1st arg") (* Pretty-printing *) diff --git a/kernel/vm.ml b/kernel/vm.ml index b6a39b042..c6491c479 100644 --- a/kernel/vm.ml +++ b/kernel/vm.ml @@ -222,7 +222,7 @@ let whd_val : values -> whd = | 1 -> Vfix(Obj.obj o, None) | 2 -> Vfix(Obj.obj (Obj.field o 1), Some (Obj.obj o)) | 3 -> Vatom_stk(Aid(RelKey(int_tcode (fun_code o) 1)), []) - | _ -> Errors.anomaly "Vm.whd : kind_of_closure does not work") + | _ -> Errors.anomaly ~label:"Vm.whd " (Pp.str "kind_of_closure does not work")) else Vconstr_block(Obj.obj o) diff --git a/lib/dyn.ml b/lib/dyn.ml index de5158b14..aec707123 100644 --- a/lib/dyn.ml +++ b/lib/dyn.ml @@ -16,7 +16,7 @@ let dyntab = ref ([] : string list) let create s = if List.mem s !dyntab then - anomaly ("Dyn.create: already declared dynamic " ^ s); + anomaly ~label:"Dyn.create" (Pp.str ("already declared dynamic " ^ s)); dyntab := s :: !dyntab; ((fun v -> (s,Obj.repr v)), (fun (s',rv) -> diff --git a/lib/errors.ml b/lib/errors.ml index d4d285a05..342ec1022 100644 --- a/lib/errors.ml +++ b/lib/errors.ml @@ -26,8 +26,12 @@ let anomaly_gen label pp = let bt = get_backtrace () in raise (Anomaly (label, pp, bt)) -let anomaly string = - anomaly_gen None (str string) +let anomaly ?loc ?label pp = + let bt = get_backtrace () in + match loc with + | None -> raise (Anomaly (label, pp, bt)) + | Some loc -> + Loc.raise loc (Anomaly (label, pp, bt)) let anomalylabstrm string pps = anomaly_gen (Some string) pps @@ -45,11 +49,6 @@ let alreadydeclared pps = raise (AlreadyDeclared(pps)) let todo s = prerr_string ("TODO: "^s^"\n") -(* raising located exceptions *) -let anomaly_loc (loc,s,strm) = - let bt = get_backtrace () in - Loc.raise loc (Anomaly (Some s, strm, bt)) - let user_err_loc (loc,s,strm) = Loc.raise loc (UserError (s,strm)) let invalid_arg_loc (loc,s) = Loc.raise loc (Invalid_argument s) diff --git a/lib/errors.mli b/lib/errors.mli index 0b2defa1a..00c39c2b3 100644 --- a/lib/errors.mli +++ b/lib/errors.mli @@ -19,9 +19,9 @@ open Pp val make_anomaly : ?label:string -> std_ppcmds -> exn (** Create an anomaly. *) -val anomaly : string -> 'a -val anomalylabstrm : string -> std_ppcmds -> 'a -val anomaly_loc : Loc.t * string * std_ppcmds -> 'a +val anomaly : ?loc:Loc.t -> ?label:string -> std_ppcmds -> 'a +(** Raise an anomaly, with an optional location and an optional + label identifying the anomaly. *) val is_anomaly : exn -> bool (** Check whether a given exception is an anomaly. *) 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 diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index 59768f5a6..4fc251edc 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -145,7 +145,7 @@ let make_cases_pattern_action Gram.action (fun (v:local_binder list list) -> make (env, envlist, true) tl) | (ETPattern | ETOther _) -> - anomaly "Unexpected entry of type cases pattern or other") + anomaly (Pp.str "Unexpected entry of type cases pattern or other")) | GramConstrListMark (n,b) :: tl -> (* Rebuild expansions of ConstrList *) let heads,env = List.chop n env in diff --git a/parsing/extrawit.ml b/parsing/extrawit.ml index 3e1c44e5a..b36e39079 100644 --- a/parsing/extrawit.ml +++ b/parsing/extrawit.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Pp open Genarg (* This file defines extra argument types *) @@ -28,7 +29,7 @@ let wit_tactic = function | 3 -> wit_tactic3 | 4 -> wit_tactic4 | 5 -> wit_tactic5 - | n -> Errors.anomaly ("Unavailable tactic level: "^string_of_int n) + | n -> Errors.anomaly (str "Unavailable tactic level:" ++ spc () ++ int n) let globwit_tactic = function | 0 -> globwit_tactic0 @@ -37,7 +38,7 @@ let globwit_tactic = function | 3 -> globwit_tactic3 | 4 -> globwit_tactic4 | 5 -> globwit_tactic5 - | n -> Errors.anomaly ("Unavailable tactic level: "^string_of_int n) + | n -> Errors.anomaly (str "Unavailable tactic level:" ++ spc () ++ int n) let rawwit_tactic = function | 0 -> rawwit_tactic0 @@ -46,7 +47,7 @@ let rawwit_tactic = function | 3 -> rawwit_tactic3 | 4 -> rawwit_tactic4 | 5 -> rawwit_tactic5 - | n -> Errors.anomaly ("Unavailable tactic level: "^string_of_int n) + | n -> Errors.anomaly (str "Unavailable tactic level:" ++ spc () ++ int n) let tactic_genarg_level s = if Int.equal (String.length s) 7 && String.sub s 0 6 = "tactic" then diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4 index 53ade7c2c..372f92eed 100644 --- a/parsing/g_xml.ml4 +++ b/parsing/g_xml.ml4 @@ -98,7 +98,7 @@ let global_of_cdata (loc,a) = Nametab.locate (uri_of_data a) let inductive_of_cdata a = match global_of_cdata a with | IndRef (kn,_) -> kn - | _ -> anomaly "XML parser: not an inductive" + | _ -> anomaly ~label:"XML parser" (str "not an inductive") let ltacref_of_cdata (loc,a) = (loc,locate_tactic (uri_of_data a)) diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index b7d2c844f..e66458ebe 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -117,7 +117,7 @@ struct let inGramObj rawwit = in_typed_entry (unquote rawwit) let outGramObj (a:'a raw_abstract_argument_type) o = if not (argument_type_eq (type_of_typed_entry o) (unquote a)) - then anomaly "outGramObj: wrong type"; + then anomaly ~label:"outGramObj" (str "wrong type"); (* downcast from grammar_object *) Obj.magic (object_of_typed_entry o) end @@ -209,7 +209,7 @@ let grammar_extend e reinit ext = let rec remove_grammars n = if n>0 then (match !camlp4_state with - | [] -> anomaly "Pcoq.remove_grammars: too many rules to remove" + | [] -> anomaly ~label:"Pcoq.remove_grammars" (Pp.str "too many rules to remove") | ByGrammar(g,reinit,ext)::t -> grammar_delete g (Option.map of_coq_assoc reinit) ext; camlp4_state := t; @@ -266,7 +266,7 @@ let get_univ s = try Hashtbl.find univ_tab s with Not_found -> - anomaly ("Unknown grammar universe: "^s) + anomaly (Pp.str ("Unknown grammar universe: "^s)) let get_entry (u, utab) s = Hashtbl.find utab s @@ -621,16 +621,16 @@ let compute_entry allow_create adjust forpat = function else weaken_entry Constr.operconstr), adjust (n,q), false | ETName -> weaken_entry Prim.name, None, false - | ETBinder true -> anomaly "Should occur only as part of BinderList" + | ETBinder true -> anomaly (Pp.str "Should occur only as part of BinderList") | ETBinder false -> weaken_entry Constr.binder, None, false | ETBinderList (true,tkl) -> let () = match tkl with [] -> () | _ -> assert false in weaken_entry Constr.open_binders, None, false - | ETBinderList (false,_) -> anomaly "List of entries cannot be registered." + | ETBinderList (false,_) -> anomaly (Pp.str "List of entries cannot be registered.") | ETBigint -> weaken_entry Prim.bigint, None, false | ETReference -> weaken_entry Constr.global, None, false | ETPattern -> weaken_entry Constr.pattern, None, false - | ETConstrList _ -> anomaly "List of entries cannot be registered." + | ETConstrList _ -> anomaly (Pp.str "List of entries cannot be registered.") | ETOther (u,n) -> let u = get_univ u in let e = diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index 21077ecc8..a85c80a79 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -51,7 +51,7 @@ module ST=struct let enter t sign st= if Hashtbl.mem st.toterm sign then - anomaly "enter: signature already entered" + anomaly ~label:"enter" (Pp.str "signature already entered") else Hashtbl.replace st.toterm sign t; Hashtbl.replace st.tosign t sign @@ -272,7 +272,7 @@ let find uf i= find_aux uf [] i let get_representative uf i= match uf.map.(i).clas with Rep r -> r - | _ -> anomaly "get_representative: not a representative" + | _ -> anomaly ~label:"get_representative" (Pp.str "not a representative") let find_pac uf i pac = PacMap.find pac (get_representative uf i).constructors @@ -280,7 +280,7 @@ let find_pac uf i pac = let get_constructor_info uf i= match uf.map.(i).term with Constructor cinfo->cinfo - | _ -> anomaly "get_constructor: not a constructor" + | _ -> anomaly ~label:"get_constructor" (Pp.str "not a constructor") let size uf i= (get_representative uf i).weight @@ -325,7 +325,7 @@ let term uf i=uf.map.(i).term let subterms uf i= match uf.map.(i).vertex with Node(j,k) -> (j,k) - | _ -> anomaly "subterms: not a node" + | _ -> anomaly ~label:"subterms" (Pp.str "not a node") let signature uf i= let j,k=subterms uf i in (find uf j,find uf k) @@ -402,7 +402,7 @@ let rec canonize_name c = let build_subst uf subst = Array.map (fun i -> try term uf i - with _ -> anomaly "incomplete matching") subst + with _ -> anomaly (Pp.str "incomplete matching")) subst let rec inst_pattern subst = function PVar i -> @@ -657,8 +657,8 @@ let process_constructor_mark t i rep pac state = {lhs=s1;rhs=s2;rule=Injection(s,opac,t,pac,n)} state.combine; f (n-1) q1 q2 - | _-> anomaly - "add_pacs : weird error in injection subterms merge" + | _-> anomaly ~label:"add_pacs" + (Pp.str "weird error in injection subterms merge") in f cinfo.ci_nhyps opac.args pac.args | Partial_applied | Partial _ -> add_pac rep pac t; @@ -750,7 +750,7 @@ let complete_one_class state i= let ct = app (term state.uf i) typ pac.arity in state.uf.epsilons <- pac :: state.uf.epsilons; ignore (add_term state ct) - | _ -> anomaly "wrong incomplete class" + | _ -> anomaly (Pp.str "wrong incomplete class") let complete state = Int.Set.iter (complete_one_class state) state.pa_classes @@ -890,7 +890,7 @@ let find_instances state = check_for_interrupt (); do_match state res pb_stack done; - anomaly "get out of here !" + anomaly (Pp.str "get out of here !") with Stack.Empty -> () in !res diff --git a/plugins/cc/ccproof.ml b/plugins/cc/ccproof.ml index 25c01f2bd..5244dcf17 100644 --- a/plugins/cc/ccproof.ml +++ b/plugins/cc/ccproof.ml @@ -47,7 +47,7 @@ let rec ptrans p1 p3= {p_lhs=p1.p_lhs; p_rhs=p3.p_rhs; p_rule=Trans (p1,p3)} - else anomaly "invalid cc transitivity" + else anomaly (Pp.str "invalid cc transitivity") let rec psym p = match p.p_rule with @@ -85,7 +85,7 @@ let rec nth_arg t n= if n>0 then nth_arg t1 (n-1) else t2 - | _ -> anomaly "nth_arg: not enough args" + | _ -> anomaly ~label:"nth_arg" (Pp.str "not enough args") let pinject p c n a = {p_lhs=nth_arg p.p_lhs (n-a); diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml index eb7d9e8e4..3cc0686ad 100644 --- a/plugins/decl_mode/decl_interp.ml +++ b/plugins/decl_mode/decl_interp.ml @@ -237,7 +237,7 @@ let rec deanonymize ids = let rec glob_of_pat = function - PatVar (loc,Anonymous) -> anomaly "Anonymous pattern variable" + PatVar (loc,Anonymous) -> anomaly (Pp.str "Anonymous pattern variable") | PatVar (loc,Name id) -> GVar (loc,id) | PatCstr(loc,((ind,_) as cstr),lpat,_) -> @@ -288,10 +288,10 @@ let bind_aliases patvars subst patt = let interp_pattern env pat_expr = let patvars,pats = Constrintern.intern_pattern env pat_expr in match pats with - [] -> anomaly "empty pattern list" + [] -> anomaly (Pp.str "empty pattern list") | [subst,patt] -> (patvars,bind_aliases patvars subst patt,patt) - | _ -> anomaly "undetected disjunctive pattern" + | _ -> anomaly (Pp.str "undetected disjunctive pattern") let rec match_args dest names constr = function [] -> [],names,substl names constr diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index a42e0cb3e..c25a150f4 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -177,7 +177,7 @@ let close_block bt pts = ET_Case_analysis -> error "\"end cases\" expected." | ET_Induction -> error "\"end induction\" expected." end - | _,_ -> anomaly "Lonely suppose on stack." + | _,_ -> anomaly (Pp.str "Lonely suppose on stack.") (* utility for suppose / suppose it is *) @@ -187,7 +187,7 @@ let close_previous_case pts = Proof.is_done pts then match get_top_stack pts with - Per (et,_,_,_) :: _ -> anomaly "Weird case occured ..." + Per (et,_,_,_) :: _ -> anomaly (Pp.str "Weird case occured ...") | Suppose_case :: Per (et,_,_,_) :: _ -> goto_current_focus (pts) | _ -> error "Not inside a proof per cases or induction." @@ -233,7 +233,7 @@ let prepare_goal items gls = filter_hyps (let keep = !tokeep in fun id -> Id.Set.mem id keep)] gls let my_automation_tac = ref - (fun gls -> anomaly "No automation registered") + (fun gls -> anomaly (Pp.str "No automation registered")) let register_automation_tac tac = my_automation_tac:= tac @@ -380,7 +380,7 @@ let concl_refiner metas body gls = let env = pf_env gls in let sort = family_of_sort (Typing.sort_of env evd concl) in let rec aux env avoid subst = function - [] -> anomaly "concl_refiner: cannot happen" + [] -> anomaly ~label:"concl_refiner" (Pp.str "cannot happen") | (n,typ)::rest -> let _A = subst_meta subst typ in let x = id_of_name_using_hdchar env _A Anonymous in @@ -896,7 +896,7 @@ let register_nodep_subcase id= function | EK_nodep -> clauses,Per(et,pi,EK_nodep,id::clauses)::s | EK_dep _ -> error "Do not mix \"suppose\" with \"suppose it is\"." end - | _ -> anomaly "wrong stack state" + | _ -> anomaly (Pp.str "wrong stack state") let suppose_tac hyps gls0 = let info = get_its_info gls0 in @@ -950,7 +950,7 @@ let rec add_branch ((id,_) as cpl) pats tree= match tree with End_patt cpl0 -> End_patt cpl0 (* this ensures precedence for overlapping patterns *) - | _ -> anomaly "tree is expected to end here" + | _ -> anomaly (Pp.str "tree is expected to end here") end | args::stack -> match args with @@ -959,7 +959,7 @@ let rec add_branch ((id,_) as cpl) pats tree= match tree with Close_patt t -> Close_patt (add_branch cpl stack t) - | _ -> anomaly "we should pop here" + | _ -> anomaly (Pp.str "we should pop here") end | (patt,rp) :: rest_args -> match patt with @@ -974,7 +974,7 @@ let rec add_branch ((id,_) as cpl) pats tree= (fun i bri -> append_branch cpl 1 (rest_args::stack) bri) tree - | _ -> anomaly "No pop/stop expected here" + | _ -> anomaly (Pp.str "No pop/stop expected here") end | PatCstr (_,(ind,cnum),args,nam) -> match tree with @@ -1002,7 +1002,7 @@ let rec add_branch ((id,_) as cpl) pats tree= (nargs::rest_args::stack) bri else bri in map_tree_rp rp (fun ids -> ids) mapi tree - | _ -> anomaly "No pop/stop expected here" + | _ -> anomaly (Pp.str "No pop/stop expected here") and append_branch ((id,_) as cpl) depth pats = function Some (ids,tree) -> Some (Id.Set.add id ids,append_tree cpl depth pats tree) @@ -1015,7 +1015,7 @@ and append_tree ((id,_) as cpl) depth pats tree = Close_patt (append_tree cpl (pred depth) pats t) | Skip_patt (ids,t) -> Skip_patt (Id.Set.add id ids,append_tree cpl depth pats t) - | End_patt _ -> anomaly "Premature end of branch" + | End_patt _ -> anomaly (Pp.str "Premature end of branch") | Split_patt (_,_,_) -> map_tree (Id.Set.add id) (fun i bri -> append_branch cpl (succ depth) pats bri) tree @@ -1105,7 +1105,7 @@ let case_tac params pat_info hyps gls0 = let et,per_info,ek,old_clauses,rest = match info.pm_stack with Per (et,pi,ek,old_clauses)::rest -> (et,pi,ek,old_clauses,rest) - | _ -> anomaly "wrong place for cases" in + | _ -> anomaly (Pp.str "wrong place for cases") in let clause = build_dep_clause params pat_info per_info hyps gls0 in let ninfo1 = {pm_stack=Suppose_case::info.pm_stack} in let nek = @@ -1130,7 +1130,7 @@ let initial_instance_stack ids : (_, _) instance_stack = List.map (fun id -> id,[None,[]]) ids let push_one_arg arg = function - [] -> anomaly "impossible" + [] -> anomaly (Pp.str "impossible") | (head,args) :: ctx -> ((head,(arg::args)) :: ctx) @@ -1148,7 +1148,7 @@ let push_head c ids stacks = let pop_one (id,stack) = let nstack= match stack with - [] -> anomaly "impossible" + [] -> anomaly (Pp.str "impossible") | [c] as l -> l | (Some head,args)::(head0,args0)::ctx -> let arg = applist (head,(List.rev args)) in @@ -1195,7 +1195,7 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls = (applist (mkVar id, List.append param_metas (List.rev_append br_args hyp_metas)))) gls - | _ -> anomaly "wrong stack size" + | _ -> anomaly (Pp.str "wrong stack size") end | Split_patt (ids,ind,br), casee::next_objs -> let (mind,oind) as spec = Global.lookup_inductive ind in @@ -1262,11 +1262,11 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls = (refine case_term) (Array.mapi branch_tac br) gls | Split_patt (_, _, _) , [] -> - anomaly "execute_cases : Nothing to split" + anomaly ~label:"execute_cases " (Pp.str "Nothing to split") | Skip_patt _ , [] -> - anomaly "execute_cases : Nothing to skip" + anomaly ~label:"execute_cases " (Pp.str "Nothing to skip") | End_patt (_,_) , _ :: _ -> - anomaly "execute_cases : End of branch with garbage left" + anomaly ~label:"execute_cases " (Pp.str "End of branch with garbage left") let understand_my_constr c gls = let env = pf_env gls in @@ -1289,14 +1289,14 @@ let end_tac et2 gls = let et1,pi,ek,clauses = match info.pm_stack with Suppose_case::_ -> - anomaly "This case should already be trapped" + anomaly (Pp.str "This case should already be trapped") | Claim::_ -> error "\"end claim\" expected." | Focus_claim::_ -> error "\"end focus\" expected." | Per(et',pi,ek,clauses)::_ -> (et',pi,ek,clauses) | [] -> - anomaly "This case should already be trapped" in + anomaly (Pp.str "This case should already be trapped") in let et = if et1 <> et2 then match et1 with @@ -1394,7 +1394,7 @@ let rec do_proof_instr_gen _thus _then instr = | Psuppose hyps -> suppose_tac hyps | Pcase (params,pat_info,hyps) -> case_tac params pat_info hyps | Pend (B_elim et) -> end_tac et - | Pend _ -> anomaly "Not applicable" + | Pend _ -> anomaly (Pp.str "Not applicable") | Pescape -> escape_tac let eval_instr {instr=instr} = @@ -1443,7 +1443,7 @@ let rec postprocess pts instr = with Type_errors.TypeError(env, Type_errors.IllFormedRecBody(_,_,_,_,_)) -> - anomaly "\"end induction\" generated an ill-formed fixpoint" + anomaly (Pp.str "\"end induction\" generated an ill-formed fixpoint") end | Pend _ -> goto_current_focus_or_top (pts) diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4 index c2b286f1b..0b7e94fa0 100644 --- a/plugins/decl_mode/g_decl_mode.ml4 +++ b/plugins/decl_mode/g_decl_mode.ml4 @@ -44,15 +44,15 @@ let pr_open_subgoals () = *) let pr_proof_instr instr = - Errors.anomaly "Cannot print a proof_instr" + Errors.anomaly (Pp.str "Cannot print a proof_instr") (* arnaud: Il nous faut quelque chose de type extr_genarg_printer si on veut aller dans cette direction Ppdecl_proof.pr_proof_instr (Global.env()) instr *) let pr_raw_proof_instr instr = - Errors.anomaly "Cannot print a raw proof_instr" + Errors.anomaly (Pp.str "Cannot print a raw proof_instr") let pr_glob_proof_instr instr = - Errors.anomaly "Cannot print a non-interpreted proof_instr" + Errors.anomaly (Pp.str "Cannot print a non-interpreted proof_instr") let interp_proof_instr _ { Evd.it = gl ; sigma = sigma }= Decl_interp.interp_proof_instr diff --git a/plugins/decl_mode/ppdecl_proof.ml b/plugins/decl_mode/ppdecl_proof.ml index 01f32e4a3..7f63c4200 100644 --- a/plugins/decl_mode/ppdecl_proof.ml +++ b/plugins/decl_mode/ppdecl_proof.ml @@ -75,7 +75,7 @@ and print_vars pconstr gtyp env sep _be _have vars = begin let nenv = match st.st_label with - Anonymous -> anomaly "anonymous variable" + Anonymous -> anomaly (Pp.str "anonymous variable") | Name id -> Environ.push_named (id,None,st.st_it) env in let pr_sep = if sep then pr_comma () else mt () in spc() ++ pr_sep ++ @@ -173,14 +173,14 @@ let rec pr_bare_proof_instr _then _thus env = function str "per" ++ spc () ++ pr_elim_type et ++ spc () ++ pr_casee env c | Pend (B_elim et) -> str "end" ++ spc () ++ pr_elim_type et - | _ -> anomaly "unprintable instruction" + | _ -> anomaly (Pp.str "unprintable instruction") let pr_emph = function 0 -> str " " | 1 -> str "* " | 2 -> str "** " | 3 -> str "*** " - | _ -> anomaly "unknown emphasis" + | _ -> anomaly (Pp.str "unknown emphasis") let pr_proof_instr env instr = pr_emph instr.emph ++ spc () ++ diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 7f5ad4f66..85b9bde71 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -348,7 +348,7 @@ and extract_seb env mp all = function | SEBstruct (msb) -> let env' = Modops.add_signature mp msb empty_delta_resolver env in MEstruct (mp,extract_sfb env' mp all msb) - | SEBwith (_,_) -> anomaly "Not available yet" + | SEBwith (_,_) -> anomaly (Pp.str "Not available yet") and extract_module env mp all mb = (* A module has an empty [mod_expr] when : diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml index 43a08657b..eb166675e 100644 --- a/plugins/extraction/modutil.ml +++ b/plugins/extraction/modutil.ml @@ -19,7 +19,7 @@ open Mlutil let rec msid_of_mt = function | MTident mp -> mp | MTwith(mt,_)-> msid_of_mt mt - | _ -> anomaly "Extraction:the With operator isn't applied to a name" + | _ -> anomaly ~label:"extraction" (Pp.str "the With operator isn't applied to a name") (*s Apply some functions upon all [ml_decl] and [ml_spec] found in a [ml_structure]. *) @@ -226,7 +226,7 @@ let get_decl_in_structure r struc = | _ -> error_not_visible r in go ll sel with Not_found -> - anomaly "reference not found in extracted structure" + anomaly (Pp.str "reference not found in extracted structure") (*s Optimization of a [ml_structure]. *) diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 74728f412..51946871f 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -242,7 +242,7 @@ let safe_basename_of_global r = let last_chance r = try Nametab.basename_of_global r with Not_found -> - anomaly "Inductive object unknown to extraction and not globally visible" + anomaly (Pp.str "Inductive object unknown to extraction and not globally visible") in match r with | ConstRef kn -> Label.to_id (con_label kn) diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index c7a582a0e..d39c6167b 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -75,7 +75,7 @@ let match_one_quantified_hyp setref seq lf= Left(Lforall(i,dom,triv))|Right(Rexists(i,dom,triv))-> if do_sequent setref triv lf.id seq i dom lf.atoms then setref:=IS.add ((Phantom dom),lf.id) !setref - | _ ->anomaly "can't happen" + | _ -> anomaly (Pp.str "can't happen") let give_instances lf seq= let setref=ref IS.empty in @@ -125,7 +125,7 @@ let mk_open_instance id gl m t= GLambda(loc,name,k,_,t0)-> let t1=raux (n-1) t0 in GLambda(loc,name,k,GHole (Loc.ghost,Evar_kinds.BinderType name),t1) - | _-> anomaly "can't happen" in + | _-> anomaly (Pp.str "can't happen") in let ntt=try Pretyping.understand evmap env (raux m rawt) with _ -> diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml index 7acabaaa4..c812deaf5 100644 --- a/plugins/firstorder/rules.ml +++ b/plugins/firstorder/rules.ml @@ -32,7 +32,7 @@ let wrap n b continue seq gls= let rec aux i nc ctx= if i<=0 then seq else match nc with - []->anomaly "Not the expected number of hyps" + []->anomaly (Pp.str "Not the expected number of hyps") | ((id,_,typ) as nd)::q-> if occur_var env id (pf_concl gls) || List.exists (occur_var_in_decl env id) ctx then diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 9c895e6a9..450b3ef40 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -310,7 +310,7 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type = (fun i (end_of_type,ctxt_size,witness_fun) ((x',b',t') as decl) -> try let witness = Int.Map.find i sub in - if b' <> None then anomaly "can not redefine a rel!"; + if b' <> None then anomaly (Pp.str "can not redefine a rel!"); (Termops.pop end_of_type,ctxt_size,mkLetIn(x',witness,t',witness_fun)) with Not_found -> (mkProd_or_LetIn decl end_of_type, ctxt_size + 1, mkLambda_or_LetIn decl witness_fun) @@ -396,7 +396,7 @@ let rewrite_until_var arg_num eq_ids : tactic = then tclIDTAC g else match eq_ids with - | [] -> anomaly "Cannot find a way to prove recursive property"; + | [] -> anomaly (Pp.str "Cannot find a way to prove recursive property"); | eq_id::eq_ids -> tclTHEN (tclTRY (Equality.rewriteRL (mkVar eq_id))) @@ -604,7 +604,7 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos = observe (str "cannot compute new term value : " ++ pr_gls g' ++ fnl () ++ str "last hyp is" ++ pr_lconstr_env (pf_env g') new_term_value_eq ); - anomaly "cannot compute new term value" + anomaly (Pp.str "cannot compute new term value") in let fun_body = mkLambda(Anonymous, @@ -830,7 +830,7 @@ let build_proof h_reduce_with_zeta Locusops.onConcl; build_proof do_finalize new_infos ] g - | Rel _ -> anomaly "Free var in goal conclusion !" + | Rel _ -> anomaly (Pp.str "Free var in goal conclusion !") and build_proof do_finalize dyn_infos g = (* observe (str "proving with "++Printer.pr_lconstr dyn_infos.info++ str " on goal " ++ pr_gls g); *) observe_tac_stream (str "build_proof with " ++ Printer.pr_lconstr dyn_infos.info ) (build_proof_aux do_finalize dyn_infos) g @@ -1014,7 +1014,7 @@ let do_replace params rec_arg_num rev_args_id f fun_num all_funs g = {finfos with equation_lemma = Some (match Nametab.locate (qualid_of_ident equation_lemma_id) with ConstRef c -> c - | _ -> Errors.anomaly "Not a constant" + | _ -> Errors.anomaly (Pp.str "Not a constant") ) } | _ -> () @@ -1208,7 +1208,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams : else h_mutual_fix this_fix_info.name (this_fix_info.idx + 1) other_fix_infos - | _ -> anomaly "Not a valid information" + | _ -> anomaly (Pp.str "Not a valid information") in let first_tac : tactic = (* every operations until fix creations *) tclTHENSEQ @@ -1223,7 +1223,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams : let ctxt,pte_app = (decompose_prod_assum (pf_concl gl)) in let pte,pte_args = (decompose_app pte_app) in try - let pte = try destVar pte with _ -> anomaly "Property is not a variable" in + let pte = try destVar pte with _ -> anomaly (Pp.str "Property is not a variable") in let fix_info = Id.Map.find pte ptes_to_fix in let nb_args = fix_info.nb_realargs in tclTHENSEQ @@ -1364,7 +1364,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams : let prove_with_tcc tcc_lemma_constr eqs : tactic = match !tcc_lemma_constr with - | None -> anomaly "No tcc proof !!" + | None -> anomaly (Pp.str "No tcc proof !!") | Some lemma -> fun gls -> (* let hid = next_ident_away_in_goal h_id (pf_ids_of_hyps gls) in *) @@ -1562,7 +1562,7 @@ let prove_principle_for_gen let args_ids = List.map (fun (na,_,_) -> Nameops.out_name na) princ_info.args in let lemma = match !tcc_lemma_ref with - | None -> anomaly ( "No tcc proof !!") + | None -> anomaly (str "No tcc proof !!") | Some lemma -> lemma in (* let rec list_diff del_list check_list = *) diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 700beaff5..9916ed95a 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -48,7 +48,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = let id = Namegen.next_ident_away x avoid in Hashtbl.add tbl id x; (Name id,v,t)::(change_predicates_names (id::avoid) predicates) - | (Anonymous,_,_)::_ -> anomaly "Anonymous property binder " + | (Anonymous,_,_)::_ -> anomaly (Pp.str "Anonymous property binder ") in let avoid = (Termops.ids_of_context env_with_params ) in let princ_type_info = @@ -395,7 +395,7 @@ let get_funs_constant mp dp = let const = make_con mp dp (Label.of_id id) in const,i | Anonymous -> - anomaly "Anonymous fix" + anomaly (Pp.str "Anonymous fix") ) na | _ -> [|const,0|] @@ -505,7 +505,7 @@ let make_scheme (fas : (constant*glob_sort) list) : Entries.definition_entry lis let first_type,other_princ_types = match l_schemes with s::l_schemes -> s,l_schemes - | _ -> anomaly "" + | _ -> anomaly (Pp.str "") in let (_,(const,_,_)) = try diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 8acd24c88..9ec935cfd 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1092,7 +1092,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = new_b, Id.Set.remove id (Id.Set.filter not_free_in_t id_to_exclude) else GProd(Loc.ghost,n,k,t,new_b),Id.Set.filter not_free_in_t id_to_exclude - | _ -> anomaly "Should not have an anonymous function here" + | _ -> anomaly (Pp.str "Should not have an anonymous function here") (* We have renamed all the anonymous functions during alpha_renaming phase *) end diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index a74ae84e2..868bf58c9 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -532,7 +532,7 @@ let rec are_unifiable_aux = function else let eqs' = try ((List.combine cpl1 cpl2)@eqs) - with _ -> anomaly "are_unifiable_aux" + with _ -> anomaly (Pp.str "are_unifiable_aux") in are_unifiable_aux eqs' @@ -554,7 +554,7 @@ let rec eq_cases_pattern_aux = function else let eqs' = try ((List.combine cpl1 cpl2)@eqs) - with _ -> anomaly "eq_cases_pattern_aux" + with _ -> anomaly (Pp.str "eq_cases_pattern_aux") in eq_cases_pattern_aux eqs' | _ -> raise NotUnifiable diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 6c3b009f8..850234c3b 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -641,7 +641,7 @@ let rec add_args id new_args b = CAppExpl(Loc.ghost,(None,r),new_args) | _ -> b end - | CFix _ | CCoFix _ -> anomaly "add_args : todo" + | CFix _ | CCoFix _ -> anomaly ~label:"add_args " (Pp.str "todo") | CProdN(loc,nal,b1) -> CProdN(loc, List.map (fun (nal,k,b2) -> (nal,k,add_args id new_args b2)) nal, @@ -692,10 +692,10 @@ let rec add_args id new_args b = CRecord (loc, (match w with Some w -> Some (add_args id new_args w) | _ -> None), List.map (fun (e,o) -> e, add_args id new_args o) pars) - | CNotation _ -> anomaly "add_args : CNotation" - | CGeneralization _ -> anomaly "add_args : CGeneralization" + | CNotation _ -> anomaly ~label:"add_args " (Pp.str "CNotation") + | CGeneralization _ -> anomaly ~label:"add_args " (Pp.str "CGeneralization") | CPrim _ -> b - | CDelimiters _ -> anomaly "add_args : CDelimiters" + | CDelimiters _ -> anomaly ~label:"add_args " (Pp.str "CDelimiters") exception Stop of Constrexpr.constr_expr @@ -736,7 +736,7 @@ let rec chop_n_arrow n t = chop_n_arrow new_n t' with Stop t -> t end - | _ -> anomaly "Not enough products" + | _ -> anomaly (Pp.str "Not enough products") let rec get_args b t : Constrexpr.local_binder list * diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index dfbfdce3a..a041205bf 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -389,7 +389,7 @@ let _ = let find_or_none id = try Some - (match Nametab.locate (qualid_of_ident id) with ConstRef c -> c | _ -> Errors.anomaly "Not a constant" + (match Nametab.locate (qualid_of_ident id) with ConstRef c -> c | _ -> Errors.anomaly (Pp.str "Not a constant") ) with Not_found -> None @@ -417,7 +417,7 @@ let add_Function is_general f = and prop_lemma = find_or_none (Nameops.add_suffix f_id "_ind") and graph_ind = match Nametab.locate (qualid_of_ident (mk_rel_id f_id)) - with | IndRef ind -> ind | _ -> Errors.anomaly "Not an inductive" + with | IndRef ind -> ind | _ -> Errors.anomaly (Pp.str "Not an inductive") in let finfos = { function_constant = f; diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index eed421159..a061cfaca 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -112,7 +112,7 @@ let generate_type g_to_f f graph i = let ctxt,_ = decompose_prod_assum graph_arity in let fun_ctxt,res_type = match ctxt with - | [] | [_] -> anomaly "Not a valid context" + | [] | [_] -> anomaly (Pp.str "Not a valid context") | (_,_,res_type)::fun_ctxt -> fun_ctxt,res_type in let rec args_from_decl i accu = function @@ -277,7 +277,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem (fun (_,pat) acc -> match pat with | Genarg.IntroIdentifier id -> Id.Set.add id acc - | _ -> anomaly "Not an identifier" + | _ -> anomaly (Pp.str "Not an identifier") ) (List.nth intro_pats (pred i)) Id.Set.empty @@ -316,7 +316,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem (fun (_,pat) acc -> match pat with | IntroIdentifier id -> id::acc - | _ -> anomaly "Not an identifier" + | _ -> anomaly (Pp.str "Not an identifier") ) (List.nth intro_pats (pred i)) [] @@ -423,7 +423,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem Array.map (fun (_,(ctxt,concl)) -> match ctxt with - | [] | [_] | [_;_] -> anomaly "bad context" + | [] | [_] | [_;_] -> anomaly (Pp.str "bad context") | hres::res::(x,_,t)::ctxt -> Termops.it_mkLambda_or_LetIn (Termops.it_mkProd_or_LetIn concl [hres;res]) @@ -488,7 +488,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem Array.map (fun (_,(ctxt,concl)) -> match ctxt with - | [] | [_] | [_;_] -> anomaly "bad context" + | [] | [_] | [_;_] -> anomaly (Pp.str "bad context") | hres::res::(x,_,t)::ctxt -> Termops.it_mkLambda_or_LetIn (Termops.it_mkProd_or_LetIn concl [hres;res]) @@ -541,7 +541,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem (fun (_,pat) acc -> match pat with | Genarg.IntroIdentifier id -> Id.Set.add id acc - | _ -> anomaly "Not an identifier" + | _ -> anomaly (Pp.str "Not an identifier") ) (List.nth intro_pats (pred i)) Id.Set.empty @@ -935,7 +935,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = then let eq_lemma = try Option.get (infos).equation_lemma - with Option.IsNone -> anomaly "Cannot find equation lemma" + with Option.IsNone -> anomaly (Pp.str "Cannot find equation lemma") in tclTHENSEQ[ tclMAP h_intro ids; @@ -1146,7 +1146,7 @@ let revert_graph kn post_tac hid g = let info = try find_Function_of_graph ind' with Not_found -> (* The graphs are mutually recursive but we cannot find one of them !*) - anomaly "Cannot retrieve infos about a mutual block" + anomaly (Pp.str "Cannot retrieve infos about a mutual block") in (* if we can find a completeness lemma for this function then we can come back to the functional form. If not, we do nothing diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 4b87a9b9c..8816d960f 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -73,8 +73,8 @@ let def_of_const t = | Some c -> Declarations.force c | _ -> assert false) with _ -> - anomaly ("Cannot find definition of constant "^ - (Id.to_string (Label.to_id (con_label sp)))) + anomaly (str "Cannot find definition of constant " ++ + (Id.print (Label.to_id (con_label sp)))) ) |_ -> assert false @@ -91,7 +91,7 @@ let constant sl s = (Id.of_string s)));; let const_of_ref = function ConstRef kn -> kn - | _ -> anomaly "ConstRef expected" + | _ -> anomaly (Pp.str "ConstRef expected") let nf_zeta env = @@ -426,7 +426,7 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) = travel jinfo new_continuation_tac {expr_info with info = b; is_final=false} end - | Rel _ -> anomaly "Free var in goal conclusion !" + | Rel _ -> anomaly (Pp.str "Free var in goal conclusion !") | Prod _ -> begin try @@ -1115,7 +1115,7 @@ let whole_start (concl_tac:tactic) nb_args is_mes func input_type relation rec_a let f_id = match f_name with | Name f_id -> next_ident_away_in_goal f_id ids - | Anonymous -> anomaly "Anonymous function" + | Anonymous -> anomaly (Pp.str "Anonymous function") in let n_names_types,_ = decompose_lam_n nb_args body1 in let n_ids,ids = @@ -1125,7 +1125,7 @@ let whole_start (concl_tac:tactic) nb_args is_mes func input_type relation rec_a | Name id -> let n_id = next_ident_away_in_goal id ids in n_id::n_ids,n_id::ids - | _ -> anomaly "anonymous argument" + | _ -> anomaly (Pp.str "anonymous argument") ) ([],(f_id::ids)) n_names_types @@ -1249,7 +1249,7 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_ | Some s -> s | None -> try (add_suffix current_proof_name "_subproof") - with _ -> anomaly "open_new_goal with an unamed theorem" + with _ -> anomaly (Pp.str "open_new_goal with an unamed theorem") in let sign = initialize_named_context_for_proof () in let na = next_global_ident_away name [] in @@ -1261,7 +1261,7 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_ let na_global = Nametab.global na_ref in match na_global with ConstRef c -> is_opaque_constant c - | _ -> anomaly "equation_lemma: not a constant" + | _ -> anomaly ~label:"equation_lemma" (Pp.str "not a constant") in let lemma = mkConst (Lib.make_con na) in ref_ := Some lemma ; @@ -1405,7 +1405,7 @@ let (com_eqn : int -> Id.t -> let opacity = match terminate_ref with | ConstRef c -> is_opaque_constant c - | _ -> anomaly "terminate_lemma: not a constant" + | _ -> anomaly ~label:"terminate_lemma" (Pp.str "not a constant") in let (evmap, env) = Lemmas.get_current_context() in let f_constr = constr_of_global f_ref in @@ -1499,7 +1499,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num begin if do_observe () then msg_debug (str "Cannot create equation Lemma " ++ Errors.print e) - else anomaly "Cannot create equation Lemma" + else anomaly (Pp.str "Cannot create equation Lemma") ; true end @@ -1533,7 +1533,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num with e -> begin (try ignore (Backtrack.backto previous_label) with _ -> ()); - (* anomaly "Cannot create termination Lemma" *) + (* anomaly (Pp.str "Cannot create termination Lemma") *) raise e end diff --git a/plugins/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.ml4 index eb713f251..a17c62eba 100644 --- a/plugins/micromega/g_micromega.ml4 +++ b/plugins/micromega/g_micromega.ml4 @@ -20,7 +20,7 @@ open Errors open Misctypes let out_arg = function - | ArgVar _ -> anomaly "Unevaluated or_var variable" + | ArgVar _ -> anomaly (Pp.str "Unevaluated or_var variable") | ArgArg x -> x TACTIC EXTEND PsatzZ diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 851516945..c4961654d 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -318,7 +318,7 @@ let coq_iff = lazy (constant "iff") let evaluable_ref_of_constr s c = match kind_of_term (Lazy.force c) with | Const kn when Tacred.is_evaluable (Global.env()) (EvalConstRef kn) -> EvalConstRef kn - | _ -> anomaly ("Coq_omega: "^s^" is not an evaluable constant") + | _ -> anomaly ~label:"Coq_omega" (Pp.str (s^" is not an evaluable constant")) let sp_Zsucc = lazy (evaluable_ref_of_constr "Z.succ" coq_Zsucc) let sp_Zpred = lazy (evaluable_ref_of_constr "Z.pred" coq_Zpred) @@ -578,7 +578,7 @@ let compile name kind = let id = new_id () in tag_hypothesis name id; {kind = kind; body = List.rev accu; constant = n; id = id} - | _ -> anomaly "compile_equation" + | _ -> anomaly (Pp.str "compile_equation") in loop [] diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml index 4238037e7..2c41b95f3 100644 --- a/plugins/quote/quote.ml +++ b/plugins/quote/quote.ml @@ -410,7 +410,7 @@ let quote_terms ivs lc gl = | None -> begin match ivs.constant_lhs with | Some c_lhs -> Termops.subst_meta [1, c] c_lhs - | None -> anomaly "invalid inversion scheme for quote" + | None -> anomaly (Pp.str "invalid inversion scheme for quote") end | Some var_lhs -> begin match ivs.constant_lhs with diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml index 5cb97d4bd..1b9afb7c7 100644 --- a/plugins/rtauto/proof_search.ml +++ b/plugins/rtauto/proof_search.ml @@ -122,7 +122,7 @@ let add_step s sub = | SI_Or_r,[p] -> I_Or_r p | SE_Or i,[p1;p2] -> E_Or(i,p1,p2) | SD_Or i,[p] -> D_Or(i,p) - | _,_ -> anomaly "add_step: wrong arity" + | _,_ -> anomaly ~label:"add_step" (Pp.str "wrong arity") type 'a with_deps = {dep_it:'a; @@ -144,7 +144,7 @@ type state = let project = function Complete prf -> prf - | Incomplete (_,_) -> anomaly "not a successful state" + | Incomplete (_,_) -> anomaly (Pp.str "not a successful state") let pop n prf = let nprf= @@ -338,7 +338,7 @@ let search_norev seq= (Arrow(f2,f3))) f1; add_hyp (embed nseq) f3]):: !goals - | _ -> anomaly "search_no_rev: can't happen" in + | _ -> anomaly ~label:"search_no_rev" (Pp.str "can't happen") in Int.Map.iter add_one seq.norev_hyps; List.rev !goals @@ -363,7 +363,7 @@ let search_in_rev_hyps seq= | Arrow (Disjunct (f1,f2),f0) -> [make_step (SD_Or(i)), [add_hyp (add_hyp (embed nseq) (Arrow(f1,f0))) (Arrow (f2,f0))]] - | _ -> anomaly "search_in_rev_hyps: can't happen" + | _ -> anomaly ~label:"search_in_rev_hyps" (Pp.str "can't happen") with Not_found -> search_norev seq @@ -441,7 +441,7 @@ let branching = function | _::next -> s_info.nd_branching<-s_info.nd_branching+List.length next in List.map (append stack) successors - | Complete prf -> anomaly "already succeeded" + | Complete prf -> anomaly (Pp.str "already succeeded") open Pp diff --git a/plugins/xml/acic2Xml.ml4 b/plugins/xml/acic2Xml.ml4 index 34bb1d51f..9d3a10dba 100644 --- a/plugins/xml/acic2Xml.ml4 +++ b/plugins/xml/acic2Xml.ml4 @@ -21,7 +21,7 @@ let typesdtdname = "http://mowgli.cs.unibo.it/dtd/cictypes.dtd";; let rec find_last_id = function - [] -> Errors.anomaly "find_last_id: empty list" + [] -> Errors.anomaly ~label:"find_last_id" (Pp.str "empty list") | [id,_,_] -> id | _::tl -> find_last_id tl ;; diff --git a/plugins/xml/cic2acic.ml b/plugins/xml/cic2acic.ml index 4a8436d76..2772779d4 100644 --- a/plugins/xml/cic2acic.ml +++ b/plugins/xml/cic2acic.ml @@ -12,6 +12,8 @@ (* http://helm.cs.unibo.it *) (************************************************************************) +open Pp + (* Utility Functions *) exception TwoModulesWhoseDirPathIsOneAPrefixOfTheOther;; @@ -162,7 +164,7 @@ let family_of_term ty = match Term.kind_of_term ty with Term.Sort s -> Coq_sort (Term.family_of_sort s) | Term.Const _ -> CProp (* I could check that the constant is CProp *) - | _ -> Errors.anomaly "family_of_term" + | _ -> Errors.anomaly (Pp.str "family_of_term") ;; module CPropRetyping = @@ -177,7 +179,7 @@ module CPropRetyping = | h::rest -> match T.kind_of_term (DoubleTypeInference.whd_betadeltaiotacprop env sigma typ) with | T.Prod (na,c1,c2) -> subst_type env sigma (T.subst1 h c2) rest - | _ -> Errors.anomaly "Non-functional construction" + | _ -> Errors.anomaly (Pp.str "Non-functional construction") let sort_of_atomic_type env sigma ft args = @@ -193,7 +195,7 @@ let typeur sigma metamap = match Term.kind_of_term cstr with | T.Meta n -> (try T.strip_outer_cast (List.assoc n metamap) - with Not_found -> Errors.anomaly "type_of: this is not a well-typed term") + with Not_found -> Errors.anomaly ~label:"type_of" (Pp.str "this is not a well-typed term")) | T.Rel n -> let (_,_,ty) = Environ.lookup_rel n env in T.lift n ty @@ -202,7 +204,7 @@ let typeur sigma metamap = let (_,_,ty) = Environ.lookup_named id env in ty with Not_found -> - Errors.anomaly ("type_of: variable "^(Names.Id.to_string id)^" unbound")) + Errors.anomaly ~label:"type_of" (str "variable " ++ Names.Id.print id ++ str " unbound")) | T.Const c -> let cb = Environ.lookup_constant c env in Typeops.type_of_constant_type env (cb.Declarations.const_type) @@ -212,7 +214,7 @@ let typeur sigma metamap = | T.Case (_,p,c,lf) -> let Inductiveops.IndType(_,realargs) = try Inductiveops.find_rectype env sigma (type_of env c) - with Not_found -> Errors.anomaly "type_of: Bad recursive type" in + with Not_found -> Errors.anomaly ~label:"type_of" (Pp.str "Bad recursive type") in let t = Reductionops.whd_beta sigma (T.applist (p, realargs)) in (match Term.kind_of_term (DoubleTypeInference.whd_betadeltaiotacprop env sigma (type_of env t)) with | T.Prod _ -> Reductionops.whd_beta sigma (T.applist (t, [c])) @@ -253,7 +255,7 @@ let typeur sigma metamap = | _, (CProp as s) -> s) | T.App(f,args) -> sort_of_atomic_type env sigma (type_of env f) args | T.Lambda _ | T.Fix _ | T.Construct _ -> - Errors.anomaly "sort_of: Not a type (1)" + Errors.anomaly ~label:"sort_of" (Pp.str "Not a type (1)") | _ -> outsort env sigma (type_of env t) and sort_family_of env t = @@ -265,7 +267,7 @@ let typeur sigma metamap = | T.App(f,args) -> sort_of_atomic_type env sigma (type_of env f) args | T.Lambda _ | T.Fix _ | T.Construct _ -> - Errors.anomaly "sort_of: Not a type (1)" + Errors.anomaly ~label:"sort_of" (Pp.str "Not a type (1)") | _ -> outsort env sigma (type_of env t) in type_of, sort_of, sort_family_of @@ -514,7 +516,7 @@ print_endline "PASSATO" ; flush stdout ; add_inner_type fresh_id'' ; A.AEvar (fresh_id'', n, Array.to_list (Array.map (aux' env idrefs) l)) - | T.Meta _ -> Errors.anomaly "Meta met during exporting to XML" + | T.Meta _ -> Errors.anomaly (Pp.str "Meta met during exporting to XML") | T.Sort s -> A.ASort (fresh_id'', s) | T.Cast (v,_, t) -> Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml index e16f9dd19..479b04228 100644 --- a/plugins/xml/xmlcommand.ml +++ b/plugins/xml/xmlcommand.ml @@ -289,7 +289,7 @@ let kind_of_variable id = | IsAssumption Conjectural -> "VARIABLE","Conjecture" | IsDefinition Definition -> "VARIABLE","LocalDefinition" | IsProof _ -> "VARIABLE","LocalFact" - | _ -> Errors.anomaly "Unsupported variable kind" + | _ -> Errors.anomaly (Pp.str "Unsupported variable kind") ;; let kind_of_constant kn = @@ -423,7 +423,7 @@ let print_ref qid fn = (* pretty prints via Xml.pp the proof in progress on dest *) let show_pftreestate internal fn (kind,pftst) id = if true then - Errors.anomaly "Xmlcommand.show_pftreestate is not supported in this version." + Errors.anomaly (Pp.str "Xmlcommand.show_pftreestate is not supported in this version.") let show fn = let pftst = Pfedit.get_pftreestate () in @@ -519,7 +519,7 @@ let _ = let options = " --html -s --body-only --no-index --latin1 --raw-comments" in let command cmd = if Sys.command cmd <> 0 then - Errors.anomaly ("Error executing \"" ^ cmd ^ "\"") + Errors.anomaly (Pp.str ("Error executing \"" ^ cmd ^ "\"")) in command (coqdoc^options^" -o "^fn^".xml "^fn^".v"); command ("rm "^fn^".v "^fn^".glob"); diff --git a/pretyping/cases.ml b/pretyping/cases.ml index bcf4b9e4a..ce8e296ba 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Pp open Errors open Util open Names @@ -64,7 +65,7 @@ let error_needs_inversion env x t = let rec list_try_compile f = function | [a] -> f a - | [] -> anomaly "try_find_f" + | [] -> anomaly (str "try_find_f") | h::t -> try f h with UserError _ | TypeError _ | PretypeError _ | PatternMatchingError _ @@ -149,9 +150,9 @@ let feed_history arg = function | Continuation (n, l, h) when n>=1 -> Continuation (n-1, arg :: l, h) | Continuation (n, _, _) -> - anomaly ("Bad number of expected remaining patterns: "^(string_of_int n)) + anomaly (str "Bad number of expected remaining patterns: " ++ int n) | Result _ -> - anomaly "Exhausted pattern history" + anomaly (Pp.str "Exhausted pattern history") (* This is for non exhaustive error message *) @@ -177,7 +178,7 @@ let pop_history_pattern = function | Continuation (0, l, MakeConstructor (pci, rh)) -> feed_history (PatCstr (Loc.ghost,pci,List.rev l,Anonymous)) rh | _ -> - anomaly "Constructor not yet filled with its arguments" + anomaly (Pp.str "Constructor not yet filled with its arguments") let pop_history h = feed_history (PatVar (Loc.ghost, Anonymous)) h @@ -403,7 +404,7 @@ let lift_tomatch_type n = liftn_tomatch_type n 1 let current_pattern eqn = match eqn.patterns with | pat::_ -> pat - | [] -> anomaly "Empty list of patterns" + | [] -> anomaly (Pp.str "Empty list of patterns") let alias_of_pat = function | PatVar (_,name) -> name @@ -415,7 +416,7 @@ let remove_current_pattern eqn = { eqn with patterns = pats; alias_stack = alias_of_pat pat :: eqn.alias_stack } - | [] -> anomaly "Empty list of patterns" + | [] -> anomaly (Pp.str "Empty list of patterns") let push_current_pattern (cur,ty) eqn = match eqn.patterns with @@ -424,7 +425,7 @@ let push_current_pattern (cur,ty) eqn = { eqn with rhs = { eqn.rhs with rhs_env = rhs_env }; patterns = pats } - | [] -> anomaly "Empty list of patterns" + | [] -> anomaly (Pp.str "Empty list of patterns") let prepend_pattern tms eqn = {eqn with patterns = tms@eqn.patterns } @@ -606,7 +607,7 @@ let replace_tomatch n c = | Pushed ((b,tm),l,na) :: rest -> let b = replace_term n c depth b in let tm = map_tomatch_type (replace_term n c depth) tm in - List.iter (fun i -> if Int.equal i (n + depth) then anomaly "replace_tomatch") l; + List.iter (fun i -> if Int.equal i (n + depth) then anomaly (Pp.str "replace_tomatch")) l; Pushed ((b,tm),l,na) :: replrec depth rest | Alias (na,b,d) :: rest -> (* [b] is out of replacement scope *) @@ -835,7 +836,7 @@ let specialize_predicate_var (cur,typ,dep) tms ccl = (*****************************************************************************) let generalize_predicate (names,na) ny d tms ccl = let () = match na with - | Anonymous -> anomaly "Undetected dependency" + | Anonymous -> anomaly (Pp.str "Undetected dependency") | _ -> () in let p = List.length names + 1 in let ccl = lift_predicate 1 ccl tms in @@ -1697,7 +1698,7 @@ let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign = if not (eq_ind ind ind') then user_err_loc (loc,"",str "Wrong inductive type."); if not (Int.equal nrealargs_ctxt (List.length realnal)) then - anomaly "Ill-formed 'in' clause in cases"; + anomaly (Pp.str "Ill-formed 'in' clause in cases"); List.rev realnal | None -> List.make nrealargs_ctxt Anonymous in (na,None,build_dependent_inductive env0 indf') diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index b398a5693..f933bf1d3 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -42,7 +42,7 @@ let apply_coercion_args env argl funj = | Prod (_,c1,c2) -> (* Typage garanti par l'appel à app_coercion*) apply_rec (h::acc) (subst1 h c2) restl - | _ -> anomaly "apply_coercion_args" + | _ -> anomaly (Pp.str "apply_coercion_args") in apply_rec [] funj.uj_type argl @@ -334,7 +334,7 @@ let apply_coercion env sigma p hj typ_cl = jres), jres.uj_type) (hj,typ_cl) p) - with _ -> anomaly "apply_coercion" + with _ -> anomaly (Pp.str "apply_coercion") let inh_app_fun env evd j = let t = whd_betadeltaiota env evd j.uj_type in diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 2db867fc5..be3817d5e 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -375,7 +375,7 @@ type binder_kind = BProd | BLambda | BLetIn (**********************************************************************) (* Main detyping function *) -let detype_anonymous = ref (fun loc n -> anomaly "detype: index to an anonymous variable") +let detype_anonymous = ref (fun loc n -> anomaly ~label:"detype" (Pp.str "index to an anonymous variable")) let set_detype_anonymous f = detype_anonymous := f let rec detype (isgoal:bool) avoid env t = diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 2184d44d3..52ef44672 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -657,7 +657,7 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = let filter = List.map2 (&&) filter filter' in (id,t,c,ty,evs,filter,occs) :: make_subst (ctxt',l,occsl) | [], [], [] -> [] - | _ -> anomaly "Signature, instance and occurrences list do not match" in + | _ -> anomaly (Pp.str "Signature, instance and occurrences list do not match") in let rec set_holes evdref rhs = function | (id,_,c,cty,evsref,filter,occs)::subst -> diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index c2ba6d957..f4f373754 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -853,7 +853,7 @@ let make_projectable_subst aliases sigma evi args = cstrs) | _ -> (rest,Id.Map.add id [a,normalize_alias_opt aliases a,id] all,cstrs)) - | _ -> anomaly "Instance does not match its signature") + | _ -> anomaly (Pp.str "Instance does not match its signature")) sign (Array.rev_to_list args,Id.Map.empty,Constrmap.empty) in (full_subst,cstr_subst) @@ -862,7 +862,7 @@ let make_pure_subst evi args = (fun (id,b,c) (args,l) -> match args with | a::rest -> (rest, (id,a)::l) - | _ -> anomaly "Instance does not match its signature") + | _ -> anomaly (Pp.str "Instance does not match its signature")) (evar_filtered_context evi) (Array.rev_to_list args,[])) (*------------------------------------* @@ -1036,7 +1036,7 @@ let rec find_projectable_vars with_evars aliases sigma y subst = | _ -> subst' end | [] -> subst' - | _ -> anomaly "More than one non var in aliases class of evar instance" + | _ -> anomaly (Pp.str "More than one non var in aliases class of evar instance") else subst' in Id.Map.fold is_projectable subst [] @@ -1883,7 +1883,7 @@ let undefined_evars_of_term evd t = (try match (Evd.find evd n).evar_body with | Evar_empty -> Int.Set.add n acc | Evar_defined c -> evrec acc c - with Not_found -> anomaly "undefined_evars_of_term: evar not found") + with Not_found -> anomaly ~label:"undefined_evars_of_term" (Pp.str "evar not found")) | _ -> fold_constr evrec acc c in evrec Int.Set.empty t diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 4c18aec19..a6049d0cf 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -92,7 +92,7 @@ let make_evar_instance sign args = | (id,_,_) :: sign, c::args when isVarId id c -> instrec (sign,args) | (id,_,_) :: sign, c::args -> (id,c) :: instrec (sign,args) | [],[] -> [] - | [],_ | _,[] -> anomaly "Signature and its instance do not match" + | [],_ | _,[] -> anomaly (Pp.str "Signature and its instance do not match") in instrec (sign,args) @@ -157,7 +157,7 @@ module EvarInfoMap = struct with Not_found -> try ExistentialMap.find evk def with Not_found -> - anomaly "Evd.define: cannot define undeclared evar" in + anomaly ~label:"Evd.define" (Pp.str "cannot define undeclared evar") in let newinfo = { oldinfo with evar_body = Evar_defined body } in @@ -165,7 +165,7 @@ module EvarInfoMap = struct | Evar_empty -> (ExistentialMap.add evk newinfo def,ExistentialMap.remove evk undef) | _ -> - anomaly "Evd.define: cannot define an evar twice" + anomaly ~label:"Evd.define" (Pp.str "cannot define an evar twice") let is_evar = mem @@ -181,7 +181,7 @@ module EvarInfoMap = struct let info = try find sigma n with Not_found -> - anomaly ("Evar "^(string_of_existential n)^" was not declared") in + anomaly (str "Evar " ++ str (string_of_existential n) ++ str " was not declared") in let hyps = evar_filtered_context info in instantiate_evar hyps info.evar_concl (Array.to_list args) @@ -611,7 +611,7 @@ let try_meta_fvalue evd mv = let meta_fvalue evd mv = try try_meta_fvalue evd mv - with Not_found -> anomaly "meta_fvalue: meta has no value" + with Not_found -> anomaly ~label:"meta_fvalue" (Pp.str "meta has no value") let meta_value evd mv = (fst (try_meta_fvalue evd mv)).rebus @@ -631,14 +631,14 @@ let meta_assign mv (v,pb) evd = | Cltyp(na,ty) -> { evd with metas = Metamap.add mv (Clval(na,(mk_freelisted v,pb),ty)) evd.metas } - | _ -> anomaly "meta_assign: already defined" + | _ -> anomaly ~label:"meta_assign" (Pp.str "already defined") let meta_reassign mv (v,pb) evd = match Metamap.find mv evd.metas with | Clval(na,_,ty) -> { evd with metas = Metamap.add mv (Clval(na,(mk_freelisted v,pb),ty)) evd.metas } - | _ -> anomaly "meta_reassign: not yet defined" + | _ -> anomaly ~label:"meta_reassign" (Pp.str "not yet defined") (* If the meta is defined then forget its name *) let meta_name evd mv = diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index 9c08a8bf6..60b708f5b 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -245,7 +245,7 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs = process_constr (push_rel d env) (i+1) (lift 1 f) (cprest,rest)) | [],[] -> f - | _,[] | [],_ -> anomaly "process_constr" + | _,[] | [],_ -> anomaly (Pp.str "process_constr") in process_constr env 0 f (List.rev cstr.cs_args, recargs) @@ -473,7 +473,7 @@ let modify_sort_scheme sort = else mkLambda (n, t, drec (npar-1) c) | LetIn (n,b,t,c) -> mkLetIn (n,b,t,drec npar c) - | _ -> anomaly "modify_sort_scheme: wrong elimination type" + | _ -> anomaly ~label:"modify_sort_scheme" (Pp.str "wrong elimination type") in drec @@ -492,7 +492,7 @@ let weaken_sort_scheme sort npars term = mkProd (n, t, c'), mkLambda (n, t, term') | LetIn (n,b,t,c) -> let c',term' = drec np c in mkLetIn (n,b,t,c'), mkLetIn (n,b,t,term') - | _ -> anomaly "weaken_sort_scheme: wrong elimination type" + | _ -> anomaly ~label:"weaken_sort_scheme" (Pp.str "wrong elimination type") in drec npars @@ -532,7 +532,7 @@ let build_mutual_induction_scheme env sigma = function in let _ = check_arities listdepkind in mis_make_indrec env sigma listdepkind mib - | _ -> anomaly "build_induction_scheme expects a non empty list of inductive types" + | _ -> anomaly (Pp.str "build_induction_scheme expects a non empty list of inductive types") let build_induction_scheme env sigma ind dep kind = let (mib,mip) = lookup_mind_specif env ind in diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index d2aaea9fa..3880dfd4e 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -206,13 +206,13 @@ let instantiate_params t args sign = | ((_,None,_)::ctxt,a::args) -> (match kind_of_term t with | Prod(_,_,t) -> inst (a::s) t (ctxt,args) - | _ -> anomaly"instantiate_params: type, ctxt and args mismatch") + | _ -> anomaly ~label:"instantiate_params" (Pp.str "type, ctxt and args mismatch")) | ((_,(Some b),_)::ctxt,args) -> (match kind_of_term t with | LetIn(_,_,_,t) -> inst ((substl s b)::s) t (ctxt,args) - | _ -> anomaly"instantiate_params: type, ctxt and args mismatch") + | _ -> anomaly ~label:"instantiate_params" (Pp.str "type, ctxt and args mismatch")) | _, [] -> substl s t - | _ -> anomaly"instantiate_params: type, ctxt and args mismatch" + | _ -> anomaly ~label:"instantiate_params" (Pp.str "type, ctxt and args mismatch") in inst [] t (List.rev sign,args) let get_constructor (ind,mib,mip,params) j = @@ -248,7 +248,7 @@ let instantiate_context sign args = | (_,None,_)::sign, a::args -> aux (a::subst) (sign,args) | (_,Some b,_)::sign, args -> aux (substl subst b::subst) (sign,args) | [], [] -> subst - | _ -> anomaly "Signature/instance mismatch in inductive family" + | _ -> anomaly (Pp.str "Signature/instance mismatch in inductive family") in aux [] (List.rev sign,args) let get_arity env (ind,params) = @@ -385,7 +385,7 @@ let is_predicate_explicitly_dep env pred arsign = | Name _ -> true end - | _ -> anomaly "Non eta-expanded dep-expanded \"match\" predicate" + | _ -> anomaly (Pp.str "Non eta-expanded dep-expanded \"match\" predicate") in srec env pred arsign diff --git a/pretyping/matching.ml b/pretyping/matching.ml index dfc52295d..e25312e41 100644 --- a/pretyping/matching.ml +++ b/pretyping/matching.ml @@ -100,7 +100,7 @@ let extract_bound_vars = | (n :: l, (na1, na2, _) :: stk) when Int.equal k n -> begin match na1, na2 with | Name id1, Name _ -> list_insert id1 (aux (k + 1) (l, stk)) - | Name _, Anonymous -> anomaly "Unnamed bound variable" + | Name _, Anonymous -> anomaly (Pp.str "Unnamed bound variable") | Anonymous, _ -> raise PatternMatchingFailure end | (l, _ :: stk) -> aux (k + 1) (l, stk) diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index 84ad8e3dd..0ecbfdbb4 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -5,6 +5,7 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Pp open Errors open Term open Environ @@ -124,7 +125,7 @@ let type_of_sort s = let type_of_var env id = try let (_,_,ty) = lookup_named id env in ty with Not_found -> - anomaly ("type_of_var: variable "^(string_of_id id)^" unbound") + anomaly ~label:"type_of_var" (str "variable " ++ Id.print id ++ str " unbound") let sort_of_product env domsort rangsort = match (domsort, rangsort) with @@ -344,4 +345,4 @@ let native_norm env c ty = let time_info = Format.sprintf "Evaluation done in %.5f@." (t1 -. t0) in if !Flags.debug then Pp.msg_debug (Pp.str time_info); nf_val env !Nativelib.rt1 ty - | _ -> anomaly "Compilation failure" + | _ -> anomaly (Pp.str "Compilation failure") diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index c1e91ca2f..ef0869fe6 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -108,14 +108,14 @@ let rec head_pattern_bound t = -> raise BoundPattern (* Perhaps they were arguments, but we don't beta-reduce *) | PLambda _ -> raise BoundPattern - | PCoFix _ -> anomaly "head_pattern_bound: not a type" + | PCoFix _ -> anomaly ~label:"head_pattern_bound" (Pp.str "not a type") let head_of_constr_reference c = match kind_of_term c with | Const sp -> ConstRef sp | Construct sp -> ConstructRef sp | Ind sp -> IndRef sp | Var id -> VarRef id - | _ -> anomaly "Not a rigid reference" + | _ -> anomaly (Pp.str "Not a rigid reference") let pattern_of_constr sigma t = let ctx = ref [] in diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index fe03cae8c..bcabf1cd9 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -686,7 +686,7 @@ and pretype_type valcon env evdref lvar = function | Sort s -> s | Evar ev when is_Type (existential_type sigma ev) -> evd_comb1 (define_evar_as_sort) evdref ev - | _ -> anomaly "Found a type constraint which is not a type" + | _ -> anomaly (Pp.str "Found a type constraint which is not a type") in { utj_val = v; utj_type = s } diff --git a/pretyping/program.ml b/pretyping/program.ml index d2e22f71e..43175e80c 100644 --- a/pretyping/program.ml +++ b/pretyping/program.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Pp open Errors open Util open Names @@ -16,7 +17,8 @@ let make_dir l = Dir_path.make (List.map Id.of_string (List.rev l)) let find_reference locstr dir s = let sp = Libnames.make_path (make_dir dir) (Id.of_string s) in try Nametab.global_of_path sp - with Not_found -> anomaly (locstr^": cannot find "^(Libnames.string_of_path sp)) + with Not_found -> + anomaly ~label:locstr (Pp.str "cannot find" ++ spc () ++ Libnames.pr_path sp) let coq_reference locstr dir s = find_reference locstr ("Coq"::dir) s let coq_constant locstr dir s = Globnames.constr_of_global (coq_reference locstr dir s) diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 6ec5ab9b4..7359b2e2a 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -813,7 +813,7 @@ let instance sigma s c = let hnf_prod_app env sigma t n = match kind_of_term (whd_betadeltaiota env sigma t) with | Prod (_,_,b) -> subst1 n b - | _ -> anomaly "hnf_prod_app: Need a product" + | _ -> anomaly ~label:"hnf_prod_app" (Pp.str "Need a product") let hnf_prod_appvect env sigma t nl = Array.fold_left (hnf_prod_app env sigma) t nl @@ -824,7 +824,7 @@ let hnf_prod_applist env sigma t nl = let hnf_lam_app env sigma t n = match kind_of_term (whd_betadeltaiota env sigma t) with | Lambda (_,_,b) -> subst1 n b - | _ -> anomaly "hnf_lam_app: Need an abstraction" + | _ -> anomaly ~label:"hnf_lam_app" (Pp.str "Need an abstraction") let hnf_lam_appvect env sigma t nl = Array.fold_left (hnf_lam_app env sigma) t nl diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index beb0be32f..b01e30bac 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Pp open Errors open Util open Term @@ -22,7 +23,7 @@ let rec subst_type env sigma typ = function | h::rest -> match kind_of_term (whd_betadeltaiota env sigma typ) with | Prod (na,c1,c2) -> subst_type env sigma (subst1 h c2) rest - | _ -> anomaly "Non-functional construction" + | _ -> anomaly (str "Non-functional construction") (* Si ft est le type d'un terme f, lequel est appliqué à args, *) (* [sort_of_atomic_ty] calcule ft[args] qui doit être une sorte *) @@ -40,7 +41,7 @@ let sort_of_atomic_type env sigma ft args = let type_of_var env id = try let (_,_,ty) = lookup_named id env in ty with Not_found -> - anomaly ("type_of: variable "^(Id.to_string id)^" unbound") + anomaly ~label:"type_of" (str "variable " ++ Id.print id ++ str " unbound") let is_impredicative_set env = match Environ.engagement env with | Some ImpredicativeSet -> true @@ -51,7 +52,7 @@ let retype ?(polyprop=true) sigma = match kind_of_term cstr with | Meta n -> (try strip_outer_cast (Evd.meta_ftype sigma n).Evd.rebus - with Not_found -> anomaly ("type_of: unknown meta " ^ string_of_int n)) + with Not_found -> anomaly ~label:"type_of" (str "unknown meta " ++ int n)) | Rel n -> let (_,_,ty) = lookup_rel n env in lift n ty @@ -63,7 +64,7 @@ let retype ?(polyprop=true) sigma = | Case (_,p,c,lf) -> let Inductiveops.IndType(_,realargs) = try Inductiveops.find_rectype env sigma (type_of env c) - with Not_found -> anomaly "type_of: Bad recursive type" in + with Not_found -> anomaly ~label:"type_of" (str "Bad recursive type") in let t = whd_beta sigma (applist (p, realargs)) in (match kind_of_term (whd_betadeltaiota env sigma (type_of env t)) with | Prod _ -> whd_beta sigma (applist (t, [c])) @@ -104,7 +105,7 @@ let retype ?(polyprop=true) sigma = sort_of_atomic_type env sigma t args | App(f,args) -> sort_of_atomic_type env sigma (type_of env f) args | Lambda _ | Fix _ | Construct _ -> - anomaly "sort_of: Not a type (1)" + anomaly ~label:"sort_of" (str "Not a type (1)") | _ -> decomp_sort env sigma (type_of env t) and sort_family_of env t = @@ -122,7 +123,7 @@ let retype ?(polyprop=true) sigma = | App(f,args) -> family_of_sort (sort_of_atomic_type env sigma (type_of env f) args) | Lambda _ | Fix _ | Construct _ -> - anomaly "sort_of: Not a type (1)" + anomaly ~label:"sort_of" (str "Not a type (1)") | _ -> family_of_sort (decomp_sort env sigma (type_of env t)) and type_of_global_reference_knowing_parameters env c args = @@ -132,11 +133,11 @@ let retype ?(polyprop=true) sigma = let (_,mip) = lookup_mind_specif env ind in (try Inductive.type_of_inductive_knowing_parameters ~polyprop env mip argtyps - with Reduction.NotArity -> anomaly "type_of: Not an arity") + with Reduction.NotArity -> anomaly ~label:"type_of" (str "Not an arity")) | Const cst -> let t = constant_type env cst in (try Typeops.type_of_constant_knowing_parameters env t argtyps - with Reduction.NotArity -> anomaly "type_of: Not an arity") + with Reduction.NotArity -> anomaly ~label:"type_of" (str "Not an arity")) | Var id -> type_of_var env id | Construct cstr -> type_of_constructor env cstr | _ -> assert false diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index b265d636e..47c382c2e 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -99,7 +99,7 @@ let destEvalRef c = match kind_of_term c with | Var id -> EvalVar id | Rel n -> EvalRel n | Evar ev -> EvalEvar ev - | _ -> anomaly "Not an unfoldable reference" + | _ -> anomaly (Pp.str "Not an unfoldable reference") let reference_opt_value sigma env = function | EvalConst cst -> constant_opt_value env cst @@ -288,7 +288,7 @@ let compute_consteval_mutual_fix sigma env ref = (* Forget all \'s and args and do as if we had started with c' *) let ref = destEvalRef c' in (match reference_opt_value sigma env ref with - | None -> anomaly "Should have been trapped by compute_direct" + | None -> anomaly (Pp.str "Should have been trapped by compute_direct") | Some c -> srec env (minarg-nargs) [] ref c) | _ -> (* Should not occur *) NotAnElimination in diff --git a/pretyping/termops.ml b/pretyping/termops.ml index 70843c7a9..d10289820 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -211,7 +211,7 @@ let push_named_rec_types (lna,typarray,_) env = (fun i na t -> match na with | Name id -> (id, None, lift i t) - | Anonymous -> anomaly "Fix declarations must be named") + | Anonymous -> anomaly (Pp.str "Fix declarations must be named")) lna typarray in Array.fold_left (fun e assum -> push_named assum e) env ctxt @@ -275,7 +275,7 @@ let rec drop_extra_implicit_args c = match kind_of_term c with (* Get the last arg of an application *) let last_arg c = match kind_of_term c with | App (f,cl) -> Array.last cl - | _ -> anomaly "last_arg" + | _ -> anomaly (Pp.str "last_arg") (* Get the last arg of an application *) let decompose_app_vect c = @@ -974,7 +974,7 @@ let rec eta_reduce_head c = (match kind_of_term (eta_reduce_head c') with | App (f,cl) -> let lastn = (Array.length cl) - 1 in - if lastn < 1 then anomaly "application without arguments" + if lastn < 1 then anomaly (Pp.str "application without arguments") else (match kind_of_term cl.(lastn) with | Rel 1 -> @@ -1043,7 +1043,7 @@ let adjust_subst_to_rel_context sign l = | (_,Some c,_)::sign', args' -> aux (substl (List.rev subst) c :: subst) sign' args' | [], [] -> List.rev subst - | _ -> anomaly "Instance and signature do not match" + | _ -> anomaly (Pp.str "Instance and signature do not match") in aux [] (List.rev sign) l let fold_named_context_both_sides f l ~init = List.fold_right_and_left f l init @@ -1093,7 +1093,7 @@ let context_chop k ctx = | (0, l2) -> (List.rev acc, l2) | (n, ((_,Some _,_ as h)::t)) -> chop_aux (h::acc) (n, t) | (n, (h::t)) -> chop_aux (h::acc) (pred n, t) - | (_, []) -> anomaly "context_chop" + | (_, []) -> anomaly (Pp.str "context_chop") in chop_aux [] (k,ctx) (* Do not skip let-in's *) diff --git a/pretyping/typing.ml b/pretyping/typing.ml index bff9bb499..0f9100e79 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Pp open Errors open Util open Term @@ -21,7 +22,7 @@ open Arguments_renaming let meta_type evd mv = let ty = try Evd.meta_ftype evd mv - with Not_found -> anomaly ("unknown meta ?"^Nameops.string_of_meta mv) in + with Not_found -> anomaly (str "unknown meta ?" ++ str (Nameops.string_of_meta mv)) in meta_instance evd ty let constant_type_knowing_parameters env cst jl = diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 87025b4d2..3a67a13ab 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -633,7 +633,7 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag (list_of_app_stack ts) (list_of_app_stack ts1) with |Some substn -> unirec_rec curenvnb pb b false substn c1 (applist (c,(List.rev ks))) - |None -> anomaly "As expected, solve_canonical_projection breaks the term too much" + |None -> anomaly (Pp.str "As expected, solve_canonical_projection breaks the term too much") in let evd = sigma in if (if occur_meta_or_undefined_evar evd m || occur_meta_or_undefined_evar evd n diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 9f6715a7d..4c0771aef 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -123,7 +123,7 @@ let pr_expl_args pr (a,expl) = match expl with | None -> pr (lapp,L) a | Some (_,ExplByPos (n,_id)) -> - anomaly("Explicitation by position not implemented") + anomaly (Pp.str "Explicitation by position not implemented") | Some (_,ExplByName id) -> str "(" ++ pr_id id ++ str ":=" ++ pr ltop a ++ str ")" @@ -242,7 +242,7 @@ let pr_binder many pr (nal,k,t) = hov 1 (str "`" ++ (surround_impl b' (pr_lident (loc,id) ++ str " : " ++ (if t' then str "!" else mt()) ++ pr t))) - |_ -> anomaly "List of generalized binders have alwais one element." + |_ -> anomaly (Pp.str "List of generalized binders have alwais one element.") end | Default b -> match t with @@ -305,7 +305,7 @@ let split_lambda = function | CLambdaN (loc,[[na],bk,t],c) -> (na,t,c) | CLambdaN (loc,([na],bk,t)::bl,c) -> (na,t,CLambdaN(loc,bl,c)) | CLambdaN (loc,(na::nal,bk,t)::bl,c) -> (na,t,CLambdaN(loc,(nal,bk,t)::bl,c)) - | _ -> anomaly "ill-formed fixpoint body" + | _ -> anomaly (Pp.str "ill-formed fixpoint body") let rename na na' t c = match (na,na') with @@ -318,7 +318,7 @@ let split_product na' = function | CProdN (loc,([na],bk,t)::bl,c) -> rename na na' t (CProdN(loc,bl,c)) | CProdN (loc,(na::nal,bk,t)::bl,c) -> rename na na' t (CProdN(loc,(nal,bk,t)::bl,c)) - | _ -> anomaly "ill-formed fixpoint body" + | _ -> anomaly (Pp.str "ill-formed fixpoint body") let rec split_fix n typ def = if Int.equal n 0 then ([],typ,def) @@ -363,7 +363,7 @@ let pr_cofixdecl pr prd dangling_with_for ((_,id),bl,t,c) = pr_recursive_decl pr prd dangling_with_for id bl (mt()) t c let pr_recursive pr_decl id = function - | [] -> anomaly "(co)fixpoint with no definition" + | [] -> anomaly (Pp.str "(co)fixpoint with no definition") | [d1] -> pr_decl false d1 | dl -> prlist_with_sep (fun () -> fnl() ++ str "with ") diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 5a5396875..14fae2612 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -502,7 +502,7 @@ let pr_let_clauses recflag pr = function hv 0 (pr_let_clause (if recflag then "let rec " else "let ") pr hd ++ prlist (fun t -> spc () ++ pr_let_clause "with " pr t) tl) - | [] -> anomaly "LetIn must declare at least one binding" + | [] -> anomaly (Pp.str "LetIn must declare at least one binding") let pr_seq_body pr tl = hv 0 (str "[ " ++ diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index b78e73e48..c04b99c5d 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -151,7 +151,7 @@ let pr_section_locality local = let pr_explanation (e,b,f) = let a = match e with - | ExplByPos (n,_) -> anomaly "No more supported" + | ExplByPos (n,_) -> anomaly (Pp.str "No more supported") | ExplByName id -> pr_id id in let a = if f then str"!" ++ a else a in if b then str "[" ++ a ++ str "]" else a @@ -336,7 +336,7 @@ let pr_assumption_token many = function str (if many then "Parameters" else "Parameter") | (Global,Conjectural) -> str"Conjecture" | (Local,Conjectural) -> - anomaly "Don't know how to beautify a local conjecture" + anomaly (Pp.str "Don't know how to beautify a local conjecture") let pr_params pr_c (xl,(c,t)) = hov 2 (prlist_with_sep sep pr_lident xl ++ spc() ++ @@ -963,7 +963,7 @@ and pr_extend s cl = match rl with | Egramml.GramTerminal s :: rl -> str s, rl, cl | Egramml.GramNonTerminal _ :: rl -> pr_arg (List.hd cl), rl, List.tl cl - | [] -> anomaly "Empty entry" in + | [] -> anomaly (Pp.str "Empty entry") in let (pp,_) = List.fold_left (fun (strm,args) pi -> diff --git a/printing/printmod.ml b/printing/printmod.ml index 2b0f458c1..5980dae0c 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -203,7 +203,7 @@ let rec print_modexpr env mp locals mexpr = match mexpr with | SEBapply _ -> let lapp = flatten_app mexpr [] in hov 3 (str"(" ++ prlist_with_sep spc (print_modpath locals) lapp ++ str")") - | SEBwith (_,_)-> anomaly "Not available yet" + | SEBwith (_,_)-> anomaly (Pp.str "Not available yet") let rec printable_body dir = diff --git a/proofs/clenv.ml b/proofs/clenv.ml index ebb1cbcd4..158f8e94f 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -167,7 +167,7 @@ let error_incompatible_inst clenv mv = (str "An incompatible instantiation has already been found for " ++ pr_id id) | _ -> - anomaly "clenv_assign: non dependent metavar already assigned" + anomaly ~label:"clenv_assign" (Pp.str "non dependent metavar already assigned") (* TODO: replace by clenv_unify (mkMeta mv) rhs ? *) let clenv_assign mv rhs clenv = @@ -421,7 +421,7 @@ let error_already_defined b = (str "Binder name \"" ++ pr_id id ++ str"\" already defined with incompatible value.") | AnonHyp n -> - anomalylabstrm "" + anomaly (str "Position " ++ int n ++ str" already defined.") let clenv_unify_binding_type clenv c t u = diff --git a/proofs/goal.ml b/proofs/goal.ml index 38e536ba2..a9aa4fa59 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -63,7 +63,7 @@ let rec advance sigma g = let v = match evi.Evd.evar_body with | Evd.Evar_defined c -> c - | _ -> Errors.anomaly "Some goal is marked as 'cleared' but is uninstantiated" + | _ -> Errors.anomaly (Pp.str "Some goal is marked as 'cleared' but is uninstantiated") in let (e,_) = Term.destEvar v in let g' = { g with content = e } in diff --git a/proofs/logic.ml b/proofs/logic.ml index 45ef3efad..2f88c79a7 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -386,7 +386,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm = | _ -> if occur_meta trm then - anomaly "refiner called with a meta in non app/case subterm"; + anomaly (Pp.str "refiner called with a meta in non app/case subterm"); let t'ty = goal_type_of env sigma trm in check_conv_leq_goal env sigma trm t'ty conclty; @@ -434,7 +434,7 @@ and mk_hdgoals sigma goal goalacc trm = | _ -> if !check && occur_meta trm then - anomaly "refine called with a dependent meta"; + anomaly (Pp.str "refine called with a dependent meta"); goalacc, goal_type_of env sigma trm, sigma, trm and mk_arggoals sigma goal goalacc funty = function @@ -457,7 +457,7 @@ and mk_casegoals sigma goal goalacc p c = let (acc'',pt,sigma,p') = mk_hdgoals sigma goal acc' p in let indspec = try Tacred.find_hnf_rectype env sigma ct - with Not_found -> anomaly "mk_casegoals" in + with Not_found -> anomaly (Pp.str "mk_casegoals") in let (lbrty,conclty) = type_case_branches_with_names env indspec p c in (acc'',lbrty,conclty,sigma,p',c') diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index ad334e91c..ef92e8e42 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -64,7 +64,7 @@ let cook_proof hook = hook prf; match Proof_global.close_proof () with | (i,([e],cg,str,h)) -> (i,(e,cg,str,h)) - | _ -> Errors.anomaly "Pfedit.cook_proof: more than one proof term." + | _ -> Errors.anomaly ~label:"Pfedit.cook_proof" (Pp.str "more than one proof term.") let xml_cook_proof = ref (fun _ -> ()) let set_xml_cook_proof f = xml_cook_proof := f @@ -113,7 +113,7 @@ let get_current_goal_context () = let current_proof_statement () = match Proof_global.V82.get_current_initial_conclusions () with | (id,([concl],strength,hook)) -> id,strength,concl,hook - | _ -> Errors.anomaly "Pfedit.current_proof_statement: more than one statement" + | _ -> Errors.anomaly ~label:"Pfedit.current_proof_statement" (Pp.str "more than one statement") let solve_nth ?(with_end_tac=false) gi tac = try diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index b57ee2118..828da8688 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -170,7 +170,7 @@ let decl_red_expr s e = end let out_arg = function - | ArgVar _ -> anomaly "Unevaluated or_var variable" + | ArgVar _ -> anomaly (Pp.str "Unevaluated or_var variable") | ArgArg x -> x let out_with_occurrences (occs,c) = diff --git a/tactics/auto.ml b/tactics/auto.ml index f251b4f85..0ab86cb04 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -557,7 +557,7 @@ let make_resolve_hyp env sigma (hname,_,htyp) = (mkVar hname, htyp)] with | Failure _ -> [] - | e when Logic.catchable_exception e -> anomaly "make_resolve_hyp" + | e when Logic.catchable_exception e -> anomaly (Pp.str "make_resolve_hyp") (* REM : in most cases hintname = id *) let make_unfold eref = diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index 27d086095..f86c22bcf 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -563,7 +563,7 @@ let fix_r2l_forward_rew_scheme c = (Reductionops.whd_beta Evd.empty (applist (c, extended_rel_list 3 indargs @ [mkRel 1;mkRel 3;mkRel 2])))))) - | _ -> anomaly "Ill-formed non-dependent left-to-right rewriting scheme" + | _ -> anomaly (Pp.str "Ill-formed non-dependent left-to-right rewriting scheme") (**********************************************************************) (* Build the right-to-left rewriting lemma for conclusion associated *) diff --git a/tactics/equality.ml b/tactics/equality.ml index 7ca1116ba..226f0c20f 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -946,7 +946,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt = else let (a,p_i_minus_1) = match whd_beta_stack !evdref p_i with | (_sigS,[a;p]) -> (a,p) - | _ -> anomaly "sig_clausal_form: should be a sigma type" in + | _ -> anomaly ~label:"sig_clausal_form" (Pp.str "should be a sigma type") in let ev = Evarutil.e_new_evar evdref env a in let rty = beta_applist(p_i_minus_1,[ev]) in let tuple_tail = sigrec_clausal_form (siglen-1) rty in @@ -960,7 +960,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt = applist(exist_term,[w_type;p_i_minus_1;w;tuple_tail]) else error "Cannot solve a unification problem." - | None -> anomaly "Not enough components to build the dependent tuple" + | None -> anomaly (Pp.str "Not enough components to build the dependent tuple") in let scf = sigrec_clausal_form siglen ty in Evarutil.nf_evar !evdref scf diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 2cfec1e21..f802788d4 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -583,7 +583,7 @@ let subst_hole_with_term occ tc t = open Tacmach let out_arg = function - | ArgVar _ -> anomaly "Unevaluated or_var variable" + | ArgVar _ -> anomaly (Pp.str "Unevaluated or_var variable") | ArgArg x -> x let hResolve id c occ t gl = diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4 index b873c2050..9adb237a9 100644 --- a/tactics/hipattern.ml4 +++ b/tactics/hipattern.ml4 @@ -289,7 +289,7 @@ let match_arrow_pattern t = match matches coq_arrow_pattern t with | [(m1,arg);(m2,mind)] -> assert (Id.equal m1 meta1 && Id.equal m2 meta2); (arg, mind) - | _ -> anomaly "Incorrect pattern matching" + | _ -> anomaly (Pp.str "Incorrect pattern matching") let match_with_nottype t = try @@ -373,7 +373,7 @@ let match_eq eqn eq_pat = | [(m1,t);(m2,x);(m3,t');(m4,x')] -> assert (Id.equal m1 meta1 && Id.equal m2 meta2 && Id.equal m3 meta3 && Id.equal m4 meta4); HeterogenousEq (t,x,t',x') - | _ -> anomaly "match_eq: an eq pattern should match 3 or 4 terms" + | _ -> anomaly ~label:"match_eq" (Pp.str "an eq pattern should match 3 or 4 terms") let equalities = [coq_eq_pattern, build_coq_eq_data; @@ -414,7 +414,7 @@ let match_eq_nf gls eqn eq_pat = | [(m1,t);(m2,x);(m3,y)] -> assert (Id.equal m1 meta1 && Id.equal m2 meta2 && Id.equal m3 meta3); (t,pf_whd_betadeltaiota gls x,pf_whd_betadeltaiota gls y) - | _ -> anomaly "match_eq: an eq pattern should match 3 terms" + | _ -> anomaly ~label:"match_eq" (Pp.str "an eq pattern should match 3 terms") let dest_nf_eq gls eqn = try @@ -435,7 +435,7 @@ let match_sigma ex ex_pat = assert (Id.equal m1 meta1 && Id.equal m2 meta2 && Id.equal m3 meta3 && Id.equal m4 meta4); (a,p,car,cdr) | _ -> - anomaly "match_sigma: a successful sigma pattern should match 4 terms" + anomaly ~label:"match_sigma" (Pp.str "a successful sigma pattern should match 4 terms") let find_sigma_data_decompose ex = (* fails with PatternMatchingFailure *) first_match (match_sigma ex) @@ -448,7 +448,7 @@ let coq_sig_pattern = lazy PATTERN [ %coq_sig_ref ?X1 ?X2 ] let match_sigma t = match matches (Lazy.force coq_sig_pattern) t with | [(_,a); (_,p)] -> (a,p) - | _ -> anomaly "Unexpected pattern" + | _ -> anomaly (Pp.str "Unexpected pattern") let is_matching_sigma t = is_matching (Lazy.force coq_sig_pattern) t @@ -486,7 +486,7 @@ let match_eqdec t = match subst with | [(_,typ);(_,c1);(_,c2)] -> eqonleft, Globnames.constr_of_global (Lazy.force op), c1, c2, typ - | _ -> anomaly "Unexpected pattern" + | _ -> anomaly (Pp.str "Unexpected pattern") (* Patterns "~ ?" and "? -> False" *) let coq_not_pattern = lazy PATTERN [ ~ _ ] diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index 811ee03c7..cc4b9d392 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -167,7 +167,7 @@ let build_signature evars env m (cstrs : (types * types option) option list) let arg' = mkApp (Lazy.force forall_relation, [| ty ; pred ; liftarg |]) in if Option.is_empty obj then evars, mkProd(na, ty, b), arg', (ty, None) :: cstrs else error "build_signature: no constraint can apply on a dependent argument" - | _, obj :: _ -> anomaly "build_signature: not enough products" + | _, obj :: _ -> anomaly ~label:"build_signature" (Pp.str "not enough products") | _, [] -> (match finalcstr with | None | Some (_, None) -> @@ -1440,7 +1440,7 @@ let rec strategy_of_ast = function | "try" -> Strategies.try_ | "any" -> Strategies.any | "repeat" -> Strategies.repeat - | _ -> anomalylabstrm "strategy_of_ast" (str"Unkwnon strategy: " ++ str f) + | _ -> anomaly ~label:"strategy_of_ast" (str"Unkwnon strategy: " ++ str f) in f' s' | StratBinary (f, s, t) -> let s' = strategy_of_ast s in @@ -1448,7 +1448,7 @@ let rec strategy_of_ast = function let f' = match f with | "compose" -> Strategies.seq | "choice" -> Strategies.choice - | _ -> anomalylabstrm "strategy_of_ast" (str"Unkwnon strategy: " ++ str f) + | _ -> anomaly ~label:"strategy_of_ast" (str"Unkwnon strategy: " ++ str f) in f' s' t' | StratConstr (c, b) -> apply_glob_constr (fst c) b AllOccurrences | StratHints (old, id) -> if old then Strategies.old_hints id else Strategies.hints id diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index 8fbab3ca1..d3c9e6bb6 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -773,8 +773,8 @@ and intern_tacarg strict onlytac ist = function (match Dyn.tag t with | "tactic" | "value" -> x | "constr" -> if onlytac then error_tactic_expected loc else x - | s -> anomaly_loc (loc, "", - str "Unknown dynamic: <" ++ str s ++ str ">")) + | s -> anomaly ~loc + (str "Unknown dynamic: <" ++ str s ++ str ">")) (* Reads the rules of a Match Context or a Match *) and intern_match_rule onlytac ist = function diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 7a041214d..730be9303 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -234,7 +234,7 @@ let try_interp_ltac_var coerce ist env (loc,id) = let interp_ltac_var coerce ist env locid = try try_interp_ltac_var coerce ist env locid - with Not_found -> anomaly ("Detected '" ^ (Id.to_string (snd locid)) ^ "' as ltac var at interning time") + with Not_found -> anomaly (str "Detected '" ++ Id.print (snd locid) ++ str "' as ltac var at interning time") (* Interprets an identifier which must be fresh *) let coerce_to_ident fresh env = function @@ -1121,8 +1121,8 @@ and interp_tacarg ist gl arg = else if String.equal tg "constr" then VConstr ([],constr_out t) else - anomaly_loc (dloc, "Tacinterp.val_interp", - (str "Unknown dynamic: <" ++ str (Dyn.tag t) ++ str ">")) + anomaly ~loc:dloc ~label:"Tacinterp.val_interp" + (str "Unknown dynamic: <" ++ str (Dyn.tag t) ++ str ">") in !evdref , v @@ -1964,7 +1964,7 @@ let globTacticIn t = TacArg (dloc,TacDynamic (dloc,tactic_in t)) let tacticIn t = globTacticIn (fun ist -> try glob_tactic (t ist) - with e -> anomalylabstrm "tacticIn" + with e -> anomaly ~label:"tacticIn" (str "Incorrect tactic expression. Received exception is:" ++ Errors.print e)) diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml index d2d6de623..90739a4e9 100644 --- a/tactics/tacsubst.ml +++ b/tactics/tacsubst.ml @@ -284,8 +284,8 @@ and subst_tacarg subst = function | "tactic" | "value" -> x | "constr" -> TacDynamic(the_loc, constr_in (subst_mps subst (constr_out t))) - | s -> Errors.anomaly_loc (dloc, "Tacinterp.val_interp", - str "Unknown dynamic: <" ++ str s ++ str ">")) + | s -> Errors.anomaly ~loc:dloc ~label:"Tacinterp.val_interp" + (str "Unknown dynamic: <" ++ str s ++ str ">")) (* Reads the rules of a Match Context or a Match *) and subst_match_rule subst = function diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 9b32f108c..f7a8a787c 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -207,7 +207,7 @@ let compute_construtor_signatures isrec (_,k as ity) = in b :: (analrec c rest) | LetIn (_,_,_,c), rest -> false :: (analrec c rest) | _, [] -> [] - | _ -> anomaly "compute_construtor_signatures" + | _ -> anomaly (Pp.str "compute_construtor_signatures") in let (mib,mip) = Global.lookup_inductive ity in let n = mib.mind_nparams in @@ -239,7 +239,7 @@ let general_elim_then_using mk_elim let indmv = match kind_of_term (last_arg elimclause.templval.Evd.rebus) with | Meta mv -> mv - | _ -> anomaly "elimination" + | _ -> anomaly (Pp.str "elimination") in let pmv = let p, _ = decompose_app elimclause.templtyp.Evd.rebus in @@ -335,11 +335,11 @@ let make_elim_branch_assumptions ba gl = id::constargs, recargs, indargs) tl idtl - | (_, _) -> anomaly "make_elim_branch_assumptions" + | (_, _) -> anomaly (Pp.str "make_elim_branch_assumptions") in makerec ([],[],[],[],[]) ba.branchsign (try List.firstn ba.nassums (pf_hyps gl) - with Failure _ -> anomaly "make_elim_branch_assumptions") + with Failure _ -> anomaly (Pp.str "make_elim_branch_assumptions")) let elim_on_ba tac ba gl = tac (make_elim_branch_assumptions ba gl) gl @@ -359,11 +359,11 @@ let make_case_branch_assumptions ba gl = id::cargs, recargs, id::constargs) tl idtl - | (_, _) -> anomaly "make_case_branch_assumptions" + | (_, _) -> anomaly (Pp.str "make_case_branch_assumptions") in makerec ([],[],[],[]) ba.branchsign (try List.firstn ba.nassums (pf_hyps gl) - with Failure _ -> anomaly "make_case_branch_assumptions") + with Failure _ -> anomaly (Pp.str "make_case_branch_assumptions")) let case_on_ba tac ba gl = tac (make_case_branch_assumptions ba gl) gl diff --git a/tactics/tactics.ml b/tactics/tactics.ml index c769fb3ba..6ba5e0e04 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -692,7 +692,7 @@ let cut_in_parallel l = let error_uninstantiated_metas t clenv = let na = meta_name clenv.evd (List.hd (Metaset.elements (metavars_of t))) in - let id = match na with Name id -> id | _ -> anomaly "unnamed dependent meta" + let id = match na with Name id -> id | _ -> anomaly (Pp.str "unnamed dependent meta") in errorlabstrm "" (str "Cannot find an instance for " ++ pr_id id ++ str".") (* For a clenv expressing some lemma [C[?1:T1,...,?n:Tn] : P] and some @@ -724,13 +724,13 @@ let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true) id c let last_arg c = match kind_of_term c with | App (f,cl) -> Array.last cl - | _ -> anomaly "last_arg" + | _ -> anomaly (Pp.str "last_arg") let nth_arg i c = if Int.equal i (-1) then last_arg c else match kind_of_term c with | App (f,cl) -> cl.(i) - | _ -> anomaly "nth_arg" + | _ -> anomaly (Pp.str "nth_arg") let index_of_ind_arg t = let rec aux i j t = match kind_of_term t with @@ -1630,7 +1630,7 @@ let quantify lconstr = *) let out_arg = function - | ArgVar _ -> anomaly "Unevaluated or_var variable" + | ArgVar _ -> anomaly (Pp.str "Unevaluated or_var variable") | ArgArg x -> x let occurrences_of_hyp id cls = @@ -2998,7 +2998,7 @@ let induction_from_context_l with_evars elim_info lid names gl = context. *) let hyp0,indvars,lid_params = match lid with - | [] -> anomaly "induction_from_context_l" + | [] -> anomaly (Pp.str "induction_from_context_l") | e::l -> let nargs_without_first = nargs_indarg_farg - 1 in let ivs,lp = cut_list nargs_without_first l in @@ -3272,7 +3272,7 @@ let elim_scheme_type elim t gl = clenv_unify ~flags:elim_flags Reduction.CUMUL t (clenv_meta_type clause mv) clause in res_pf clause' ~flags:elim_flags gl - | _ -> anomaly "elim_scheme_type" + | _ -> anomaly (Pp.str "elim_scheme_type") let elim_type t gl = let (ind,t) = pf_reduce_to_atomic_ind gl t in diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v index 0e7d653b4..4c77e4bcf 100644 --- a/test-suite/success/evars.v +++ b/test-suite/success/evars.v @@ -62,7 +62,7 @@ Check Check (fun f:(forall (v:Type->Type), v (v nat) -> nat) => f _ (Some (Some O))). -(* This used to fail with anomaly "evar was not declared" in V8.0pl3 *) +(* This used to fail with anomaly (Pp.str "evar was not declared") in V8.0pl3 *) Theorem contradiction : forall p, ~ p -> p -> False. Proof. trivial. Qed. diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index 20c02878a..6e88628bd 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -845,7 +845,7 @@ let compute_dec_tact ind lnamesparrec nparrec gsig = let make_eq_decidability mind = let mib = Global.lookup_mind mind in if not (Int.equal (Array.length mib.mind_packets) 1) then - anomaly "Decidability lemma for mutual inductive types not supported"; + anomaly (Pp.str "Decidability lemma for mutual inductive types not supported"); let ind = (mind,0) in let nparams = mib.mind_nparams in let nparrec = mib.mind_nparams_rec in diff --git a/toplevel/command.ml b/toplevel/command.ml index 55ee2a37c..d5a1da6d0 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -343,7 +343,7 @@ let extract_coercions indl = let extract_params indl = let paramsl = List.map (fun (_,params,_,_) -> params) indl in match paramsl with - | [] -> anomaly "empty list of inductive types" + | [] -> anomaly (Pp.str "empty list of inductive types") | params::paramsl -> if not (List.for_all (eq_local_binders params) paramsl) then error "Parameters should be syntactically the same for each inductive type."; diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index dcac6eb79..b12378c56 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -21,7 +21,7 @@ open Cooking let detype_param = function | (Name id,None,p) -> id, Entries.LocalAssum p | (Name id,Some p,_) -> id, Entries.LocalDef p - | (Anonymous,_,_) -> anomaly"Unnamed inductive local variable" + | (Anonymous,_,_) -> anomaly (Pp.str "Unnamed inductive local variable") (* Replace diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml index e35b8de0e..694403c9e 100644 --- a/toplevel/lemmas.ml +++ b/toplevel/lemmas.ml @@ -154,7 +154,7 @@ let look_for_possibly_mutual_statements = function let recguard,ordered_inds = find_mutually_recursive_statements thms in let thms = List.map pi2 ordered_inds in Some recguard,thms, Some (List.map (fun (_,_,i) -> succ i) ordered_inds) - | [] -> anomaly "Empty list of theorems." + | [] -> anomaly (Pp.str "Empty list of theorems.") (* Saving a goal *) @@ -209,7 +209,7 @@ let save_remaining_recthms (local,kind) body opaq i (id,(t_i,(_,imps))) = let body_i = match kind_of_term body with | Fix ((nv,0),decls) -> mkFix ((nv,i),decls) | CoFix (0,decls) -> mkCoFix (i,decls) - | _ -> anomaly "Not a proof by induction" in + | _ -> anomaly (Pp.str "Not a proof by induction") in match local with | Local -> let c = SectionLocalDef (body_i, Some t_i, opaq) in @@ -300,7 +300,7 @@ let start_proof_with_initialization kind recguard thms snl hook = let () = match thms with [_] -> () | _ -> assert false in (if Flags.is_auto_intros () then Some (intro_tac (List.hd thms)) else None), [] in match thms with - | [] -> anomaly "No proof to start" + | [] -> anomaly (Pp.str "No proof to start") | (id,(t,(_,imps)))::other_thms -> let hook strength ref = let other_thms_data = diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 60d600ca1..a785dd31a 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -323,7 +323,7 @@ let rec find_pattern nt xl = function | _, [] -> error msg_expected_form_of_recursive_notation | ((SProdList _ | NonTerminal _) :: _), _ | _, (SProdList _ :: _) -> - anomaly "Only Terminal or Break expected on left, non-SProdList on right" + anomaly (Pp.str "Only Terminal or Break expected on left, non-SProdList on right") let rec interp_list_parser hd = function | [] -> [], List.rev hd @@ -344,7 +344,7 @@ let rec interp_list_parser hd = function | NonTerminal _ as x :: tl -> let xyl,tl' = interp_list_parser [x] tl in xyl, List.rev_append hd tl' - | SProdList _ :: _ -> anomaly "Unexpected SProdList in interp_list_parser" + | SProdList _ :: _ -> anomaly (Pp.str "Unexpected SProdList in interp_list_parser") (* Find non-terminal tokens of notation *) @@ -692,7 +692,7 @@ let make_production etyps symbols = let tkl = List.flatten (List.map (function Terminal s -> [Lexer.terminal s] | Break _ -> [] - | _ -> anomaly "Found a non terminal token in recursive notation separator") sl) in + | _ -> anomaly (Pp.str "Found a non terminal token in recursive notation separator")) sl) in match List.assoc x etyps with | ETConstr typ -> expand_list_rule typ tkl x 1 0 [] ll | ETBinder o -> diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index 03bad4c1c..68dfca9f9 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -72,7 +72,7 @@ let subst_evar_constr evs n idf t = ev_hyps = hyps ; ev_chop = chop } = try evar_info k with Not_found -> - anomaly ("eterm: existential variable " ^ string_of_int k ^ " not found") + anomaly ~label:"eterm" (Pp.str "existential variable " ++ int k ++ str " not found") in seen := Int.Set.add id !seen; (* Evar arguments are created in inverse order, @@ -976,7 +976,7 @@ let next_obligation n tac = let is_open _ x = Option.is_empty x.obl_body && List.is_empty (deps_remaining obls x.obl_deps) in let i = match Array.findi is_open obls with | Some i -> i - | None -> anomaly "Could not find a solvable obligation." + | None -> anomaly (Pp.str "Could not find a solvable obligation.") in solve_obligation prg i tac diff --git a/toplevel/record.ml b/toplevel/record.ml index 7926aecbd..93868dbe3 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -84,7 +84,7 @@ let typecheck_params_and_fields id t ps nots fs = let degenerate_decl (na,b,t) = let id = match na with | Name id -> id - | Anonymous -> anomaly "Unnamed record variable" in + | Anonymous -> anomaly (Pp.str "Unnamed record variable") in match b with | None -> (id, Entries.LocalAssum t) | Some b -> (id, Entries.LocalDef b) diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml index 0da4fc8c9..abdb3b74a 100644 --- a/toplevel/toplevel.ml +++ b/toplevel/toplevel.ml @@ -86,7 +86,7 @@ let reset_input_buffer ic ibuf = let get_bols_of_loc ibuf (bp,ep) = let add_line (b,e) lines = - if b < 0 or e < b then anomaly "Bad location"; + if b < 0 or e < b then anomaly (Pp.str "Bad location"); match lines with | ([],None) -> ([], Some (b,e)) | (fl,oe) -> ((b,e)::fl, oe) diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 5c2d8604c..7e681b1a0 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -116,7 +116,7 @@ let show_script () = msg_notice (v 0 (Pp.prlist_with_sep Pp.fnl (fun x -> x) indented_cmds)) let show_thesis () = - msg_error (anomaly "TODO" ) + msg_error (anomaly (Pp.str "TODO") ) let show_top_evars () = (* spiwack: new as of Feb. 2010: shows goal evars in addition to non-goal evars. *) diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4 index 3d8a1eb76..7e27d8693 100644 --- a/toplevel/whelp.ml4 +++ b/toplevel/whelp.ml4 @@ -165,9 +165,9 @@ let rec uri_of_constr c = | GRec _ | GIf _ | GLetTuple _ | GCases _ -> error "Whelp does not support pattern-matching and (co-)fixpoint." | GVar _ | GRef _ | GHole _ | GEvar _ | GSort _ | GCast (_,_, CastCoerce) -> - anomaly "Written w/o parenthesis" + anomaly (Pp.str "Written w/o parenthesis") | GPatVar _ -> - anomaly "Found constructors not supported in constr") () + anomaly (Pp.str "Found constructors not supported in constr")) () let make_string f x = Buffer.reset b; f x; Buffer.contents b |