diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2016-07-07 04:56:24 +0200 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2016-08-19 01:48:30 +0200 |
commit | de038270f72214b169d056642eb7144a79e6f126 (patch) | |
tree | c1a5dc835f5042c79418fdbadc7b266a473b8c82 /pretyping | |
parent | 13fb26d615cdb03a4c4841c20b108deab2de60b3 (diff) |
Unify location handling of error functions.
In some cases prior to this patch, there were two cases for the same
error function, one taking a location, the other not.
We unify them by using an option parameter, in the line with recent
changes in warnings and feedback.
This implies a bit of clean up in some places, but more importantly, is
the preparation for subsequent patches making `Loc.location` opaque,
change that could be use to improve modularity and allow a more
functional implementation strategy --- for example --- of the
beautifier.
Diffstat (limited to 'pretyping')
-rw-r--r-- | pretyping/cases.ml | 44 | ||||
-rw-r--r-- | pretyping/cases.mli | 4 | ||||
-rw-r--r-- | pretyping/coercion.ml | 8 | ||||
-rw-r--r-- | pretyping/detyping.ml | 8 | ||||
-rw-r--r-- | pretyping/evarconv.ml | 4 | ||||
-rw-r--r-- | pretyping/evardefine.ml | 4 | ||||
-rw-r--r-- | pretyping/patternops.ml | 14 | ||||
-rw-r--r-- | pretyping/pretype_errors.ml | 80 | ||||
-rw-r--r-- | pretyping/pretype_errors.mli | 53 | ||||
-rw-r--r-- | pretyping/pretyping.ml | 66 |
10 files changed, 138 insertions, 147 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 447a4c487..85c518019 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -45,22 +45,22 @@ type pattern_matching_error = exception PatternMatchingError of env * evar_map * pattern_matching_error -let raise_pattern_matching_error (loc,env,sigma,te) = - Loc.raise loc (PatternMatchingError(env,sigma,te)) +let raise_pattern_matching_error ?loc (env,sigma,te) = + Loc.raise ?loc (PatternMatchingError(env,sigma,te)) -let error_bad_pattern_loc loc env sigma cstr ind = - raise_pattern_matching_error - (loc, env, sigma, BadPattern (cstr,ind)) +let error_bad_pattern ?loc env sigma cstr ind = + raise_pattern_matching_error ?loc + (env, sigma, BadPattern (cstr,ind)) -let error_bad_constructor_loc loc env cstr ind = +let error_bad_constructor ?loc env cstr ind = raise_pattern_matching_error - (loc, env, Evd.empty, BadConstructor (cstr,ind)) + (env, Evd.empty, BadConstructor (cstr,ind)) -let error_wrong_numarg_constructor_loc loc env c n = - raise_pattern_matching_error (loc, env, Evd.empty, WrongNumargConstructor(c,n)) +let error_wrong_numarg_constructor ?loc env c n = + raise_pattern_matching_error (env, Evd.empty, WrongNumargConstructor(c,n)) -let error_wrong_numarg_inductive_loc loc env c n = - raise_pattern_matching_error (loc, env, Evd.empty, WrongNumargInductive(c,n)) +let error_wrong_numarg_inductive ?loc env c n = + raise_pattern_matching_error (env, Evd.empty, WrongNumargInductive(c,n)) let rec list_try_compile f = function | [a] -> f a @@ -479,26 +479,25 @@ let check_and_adjust_constructor env ind cstrs = function let args' = adjust_local_defs loc (args, List.rev ci.cs_args) in PatCstr (loc, cstr, args', alias) with NotAdjustable -> - error_wrong_numarg_constructor_loc loc env cstr nb_args_constr + error_wrong_numarg_constructor ~loc env cstr nb_args_constr else (* Try to insert a coercion *) try Coercion.inh_pattern_coerce_to loc env pat ind' ind with Not_found -> - error_bad_constructor_loc loc env cstr ind + error_bad_constructor ~loc env cstr ind let check_all_variables env sigma typ mat = List.iter (fun eqn -> match current_pattern eqn with | PatVar (_,id) -> () | PatCstr (loc,cstr_sp,_,_) -> - error_bad_pattern_loc loc env sigma cstr_sp typ) + error_bad_pattern ~loc env sigma cstr_sp typ) mat let check_unused_pattern env eqn = if not !(eqn.used) then - raise_pattern_matching_error - (eqn.eqn_loc, env, Evd.empty, UnusedClause eqn.patterns) + raise_pattern_matching_error ~loc:eqn.eqn_loc (env, Evd.empty, UnusedClause eqn.patterns) let set_used_pattern eqn = eqn.used := true @@ -1305,8 +1304,7 @@ let build_branch initial current realargs deps (realnames,curname) pb arsign eqn let submat = adjust_impossible_cases pb pred tomatch submat in let () = match submat with | [] -> - raise_pattern_matching_error - (Loc.ghost, pb.env, Evd.empty, NonExhaustive (complete_history history)) + raise_pattern_matching_error (pb.env, Evd.empty, NonExhaustive (complete_history history)) | _ -> () in @@ -1834,8 +1832,8 @@ let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign = | None -> [LocalAssum (na, lift n typ)] | Some b -> [LocalDef (na, lift n b, lift n typ)]) | Some (loc,_,_) -> - user_err_loc (loc,"", - str"Unexpected type annotation for a term of non inductive type.")) + user_err ~loc "" + (str"Unexpected type annotation for a term of non inductive type.")) | IsInd (term,IndType(indf,realargs),_) -> let indf' = if dolift then lift_inductive_family n indf else indf in let ((ind,u),_) = dest_ind_family indf' in @@ -1845,7 +1843,7 @@ let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign = match t with | Some (loc,ind',realnal) -> if not (eq_ind ind ind') then - user_err_loc (loc,"",str "Wrong inductive type."); + user_err ~loc "" (str "Wrong inductive type."); if not (Int.equal nrealargs_ctxt (List.length realnal)) then anomaly (Pp.str "Ill-formed 'in' clause in cases"); List.rev realnal @@ -2036,11 +2034,11 @@ let constr_of_pat env evdref arsign pat avoid = let cind = inductive_of_constructor cstr in let IndType (indf, _) = try find_rectype env ( !evdref) (lift (-(List.length realargs)) ty) - with Not_found -> error_case_not_inductive env + with Not_found -> error_case_not_inductive env !evdref {uj_val = ty; uj_type = Typing.unsafe_type_of env !evdref ty} in let (ind,u), params = dest_ind_family indf in - if not (eq_ind ind cind) then error_bad_constructor_loc l env cstr ind; + if not (eq_ind ind cind) then error_bad_constructor ~loc:l env cstr ind; let cstrs = get_constructors env indf in let ci = cstrs.(i-1) in let nb_args_constr = ci.cs_nargs in diff --git a/pretyping/cases.mli b/pretyping/cases.mli index ba566f374..6bc61f6dd 100644 --- a/pretyping/cases.mli +++ b/pretyping/cases.mli @@ -28,9 +28,9 @@ type pattern_matching_error = exception PatternMatchingError of env * evar_map * pattern_matching_error -val error_wrong_numarg_constructor_loc : Loc.t -> env -> constructor -> int -> 'a +val error_wrong_numarg_constructor : ?loc:Loc.t -> env -> constructor -> int -> 'a -val error_wrong_numarg_inductive_loc : Loc.t -> env -> inductive -> int -> 'a +val error_wrong_numarg_inductive : ?loc:Loc.t -> env -> inductive -> int -> 'a val irrefutable : env -> cases_pattern -> bool diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 913e80f39..98dea9fc9 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -412,7 +412,7 @@ let inh_tosort_force loc env evd j = let j2 = on_judgment_type (whd_evar evd) j1 in (evd,type_judgment env j2) with Not_found | NoCoercion -> - error_not_a_type_loc loc env evd j + error_not_a_type ~loc env evd j let inh_coerce_to_sort loc env evd j = let typ = whd_all env evd j.uj_type in @@ -506,16 +506,16 @@ let inh_conv_coerce_to_gen resolve_tc rigidonly loc env evd cj t = else raise NoSubtacCoercion with | NoSubtacCoercion when not resolve_tc || not !use_typeclasses_for_conversion -> - error_actual_type_loc loc env best_failed_evd cj t e + error_actual_type ~loc env best_failed_evd cj t e | NoSubtacCoercion -> let evd' = saturate_evd env evd in try if evd' == evd then - error_actual_type_loc loc env best_failed_evd cj t e + error_actual_type ~loc env best_failed_evd cj t e else inh_conv_coerce_to_fail loc env evd' rigidonly (Some cj.uj_val) cj.uj_type t with NoCoercionNoUnifier (_evd,_error) -> - error_actual_type_loc loc env best_failed_evd cj t e + error_actual_type ~loc env best_failed_evd cj t e in let val' = match val' with Some v -> v | None -> assert(false) in (evd',{ uj_val = val'; uj_type = t }) diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 85125a502..ab9393915 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -67,15 +67,15 @@ let isomorphic_to_tuple lc = Int.equal (Array.length lc) 1 let encode_bool r = let (x,lc) = encode_inductive r in if not (has_two_constructors lc) then - user_err_loc (loc_of_reference r,"encode_if", - str "This type has not exactly two constructors."); + user_err ~loc:(loc_of_reference r) "encode_if" + (str "This type has not exactly two constructors."); x let encode_tuple r = let (x,lc) = encode_inductive r in if not (isomorphic_to_tuple lc) then - user_err_loc (loc_of_reference r,"encode_tuple", - str "This type cannot be seen as a tuple type."); + user_err ~loc:(loc_of_reference r) "encode_tuple" + (str "This type cannot be seen as a tuple type."); x module PrintingInductiveMake = diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 0fea2ba22..26af90958 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -1249,7 +1249,7 @@ let consider_remaining_unif_problems env aux evd pbs progress (pb :: stuck) end | UnifFailure (evd,reason) -> - Pretype_errors.error_cannot_unify_loc (loc_of_conv_pb evd pb) + Pretype_errors.error_cannot_unify ~loc:(loc_of_conv_pb evd pb) env evd ~reason (t1, t2)) | _ -> if progress then aux evd stuck false [] @@ -1258,7 +1258,7 @@ let consider_remaining_unif_problems env | [] -> (* We're finished *) evd | (pbty,env,t1,t2 as pb) :: _ -> (* There remains stuck problems *) - Pretype_errors.error_cannot_unify_loc (loc_of_conv_pb evd pb) + Pretype_errors.error_cannot_unify ~loc:(loc_of_conv_pb evd pb) env evd (t1, t2) in let (evd,pbs) = extract_all_conv_pbs evd in diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml index f9ab75cea..b91ae6c72 100644 --- a/pretyping/evardefine.ml +++ b/pretyping/evardefine.ml @@ -135,7 +135,7 @@ let define_pure_evar_as_lambda env evd evk = let evd1,(na,dom,rng) = match kind_of_term typ with | Prod (na,dom,rng) -> (evd,(na,dom,rng)) | Evar ev' -> let evd,typ = define_evar_as_product evd ev' in evd,destProd typ - | _ -> error_not_product_loc Loc.ghost env evd typ in + | _ -> error_not_product env evd typ in let avoid = ids_of_named_context (evar_context evi) in let id = next_name_away_with_default_using_types "x" na avoid (Reductionops.whd_evar evd dom) in @@ -191,7 +191,7 @@ let split_tycon loc env evd tycon = | App (c,args) when isEvar c -> let (evd',lam) = define_evar_as_lambda env evd (destEvar c) in real_split evd' (mkApp (lam,args)) - | _ -> error_not_product_loc loc env evd c + | _ -> error_not_product ~loc env evd c in match tycon with | None -> evd,(Anonymous,None,None) diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index fe73b6105..99c3772db 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -315,7 +315,7 @@ let rec subst_pattern subst pat = let mkPLambda na b = PLambda(na,PMeta None,b) let rev_it_mkPLambda = List.fold_right mkPLambda -let err loc pp = user_err_loc (loc,"pattern_of_glob_constr", pp) +let err ?loc pp = user_err ?loc "pattern_of_glob_constr" pp let warn_cast_in_pattern = CWarnings.create ~name:"cast-in-pattern" ~category:"automation" @@ -387,7 +387,7 @@ let rec pat_of_raw metas vars = function rev_it_mkPLambda nal (mkPLambda na (pat_of_raw metas nvars p)) | (None | Some (GHole _)), _ -> PMeta None | Some p, None -> - user_err_loc (loc,"",strbrk "Clause \"in\" expected in patterns over \"match\" expressions with an explicit \"return\" clause.") + user_err ~loc "" (strbrk "Clause \"in\" expected in patterns over \"match\" expressions with an explicit \"return\" clause.") in let info = { cip_style = sty; @@ -400,12 +400,12 @@ let rec pat_of_raw metas vars = function one non-trivial branch. These facts are used in [Constrextern]. *) PCase (info, pred, pat_of_raw metas vars c, brs) - | r -> err (loc_of_glob_constr r) (Pp.str "Non supported pattern.") + | r -> err ~loc:(loc_of_glob_constr r) (Pp.str "Non supported pattern.") and pats_of_glob_branches loc metas vars ind brs = let get_arg = function | PatVar(_,na) -> na - | PatCstr(loc,_,_,_) -> err loc (Pp.str "Non supported pattern.") + | PatCstr(loc,_,_,_) -> err ~loc (Pp.str "Non supported pattern.") in let rec get_pat indexes = function | [] -> false, [] @@ -414,10 +414,10 @@ and pats_of_glob_branches loc metas vars ind brs = let () = match ind with | Some sp when eq_ind sp indsp -> () | _ -> - err loc (Pp.str "All constructors must be in the same inductive type.") + err ~loc (Pp.str "All constructors must be in the same inductive type.") in if Int.Set.mem (j-1) indexes then - err loc + err ~loc (str "No unique branch for " ++ int j ++ str"-th constructor."); let lna = List.map get_arg lv in let vars' = List.rev lna @ vars in @@ -425,7 +425,7 @@ and pats_of_glob_branches loc metas vars ind brs = let ext,pats = get_pat (Int.Set.add (j-1) indexes) brs in let tags = List.map (fun _ -> false) lv (* approximation, w/o let-in *) in ext, ((j-1, tags, pat) :: pats) - | (loc,_,_,_) :: _ -> err loc (Pp.str "Non supported pattern.") + | (loc,_,_,_) :: _ -> err ~loc (Pp.str "Non supported pattern.") in get_pat Int.Set.empty brs diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index 00b6100c0..5b0958695 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -64,43 +64,42 @@ let precatchable_exception = function | Nametab.GlobalizationError _ -> true | _ -> false -let raise_pretype_error (loc,env,sigma,te) = - Loc.raise loc (PretypeError(env,sigma,te)) +let raise_pretype_error ?loc (env,sigma,te) = + Loc.raise ?loc (PretypeError(env,sigma,te)) -let raise_located_type_error (loc,env,sigma,te) = - Loc.raise loc (PretypeError(env,sigma,TypingError te)) +let raise_type_error ?loc (env,sigma,te) = + Loc.raise ?loc (PretypeError(env,sigma,TypingError te)) - -let error_actual_type_loc loc env sigma {uj_val=c;uj_type=actty} expty reason = +let error_actual_type ?loc env sigma {uj_val=c;uj_type=actty} expty reason = let j = {uj_val=c;uj_type=actty} in - raise_pretype_error - (loc, env, sigma, ActualTypeNotCoercible (j, expty, reason)) + raise_pretype_error ?loc + (env, sigma, ActualTypeNotCoercible (j, expty, reason)) -let error_cant_apply_not_functional_loc loc env sigma rator randl = - raise_located_type_error - (loc, env, sigma, CantApplyNonFunctional (rator, Array.of_list randl)) +let error_cant_apply_not_functional ?loc env sigma rator randl = + raise_type_error ?loc + (env, sigma, CantApplyNonFunctional (rator, Array.of_list randl)) -let error_cant_apply_bad_type_loc loc env sigma (n,c,t) rator randl = - raise_located_type_error - (loc, env, sigma, +let error_cant_apply_bad_type ?loc env sigma (n,c,t) rator randl = + raise_type_error ?loc + (env, sigma, CantApplyBadType ((n,c,t), rator, Array.of_list randl)) -let error_ill_formed_branch_loc loc env sigma c i actty expty = - raise_located_type_error - (loc, env, sigma, IllFormedBranch (c, i, actty, expty)) +let error_ill_formed_branch ?loc env sigma c i actty expty = + raise_type_error + ?loc (env, sigma, IllFormedBranch (c, i, actty, expty)) -let error_number_branches_loc loc env sigma cj expn = - raise_located_type_error (loc, env, sigma, NumberBranches (cj, expn)) +let error_number_branches ?loc env sigma cj expn = + raise_type_error ?loc (env, sigma, NumberBranches (cj, expn)) -let error_case_not_inductive_loc loc env sigma cj = - raise_located_type_error (loc, env, sigma, CaseNotInductive cj) +let error_case_not_inductive ?loc env sigma cj = + raise_type_error ?loc (env, sigma, CaseNotInductive cj) -let error_ill_typed_rec_body_loc loc env sigma i na jl tys = - raise_located_type_error - (loc, env, sigma, IllTypedRecBody (i, na, jl, tys)) +let error_ill_typed_rec_body ?loc env sigma i na jl tys = + raise_type_error ?loc + (env, sigma, IllTypedRecBody (i, na, jl, tys)) -let error_not_a_type_loc loc env sigma j = - raise_located_type_error (loc, env, sigma, NotAType j) +let error_not_a_type ?loc env sigma j = + raise_type_error ?loc (env, sigma, NotAType j) (*s Implicit arguments synthesis errors. It is hard to find a precise location. *) @@ -108,15 +107,12 @@ let error_not_a_type_loc loc env sigma j = let error_occur_check env sigma ev c = raise (PretypeError (env, sigma, UnifOccurCheck (ev,c))) -let error_unsolvable_implicit loc env sigma evk explain = - Loc.raise loc +let error_unsolvable_implicit ?loc env sigma evk explain = + Loc.raise ?loc (PretypeError (env, sigma, UnsolvableImplicit (evk, explain))) -let error_cannot_unify_loc loc env sigma ?reason (m,n) = - Loc.raise loc (PretypeError (env, sigma,CannotUnify (m,n,reason))) - -let error_cannot_unify env sigma ?reason (m,n) = - raise (PretypeError (env, sigma,CannotUnify (m,n,reason))) +let error_cannot_unify ?loc env sigma ?reason (m,n) = + Loc.raise ?loc (PretypeError (env, sigma,CannotUnify (m,n,reason))) let error_cannot_unify_local env sigma (m,n,sn) = raise (PretypeError (env, sigma,CannotUnifyLocal (m,n,sn))) @@ -140,21 +136,21 @@ let error_non_linear_unification env sigma hdmeta t = (*s Ml Case errors *) -let error_cant_find_case_type_loc loc env sigma expr = - raise_pretype_error (loc, env, sigma, CantFindCaseType expr) +let error_cant_find_case_type ?loc env sigma expr = + raise_pretype_error ?loc (env, sigma, CantFindCaseType expr) (*s Pretyping errors *) -let error_unexpected_type_loc loc env sigma actty expty = - raise_pretype_error (loc, env, sigma, UnexpectedType (actty, expty)) +let error_unexpected_type ?loc env sigma actty expty = + raise_pretype_error ?loc (env, sigma, UnexpectedType (actty, expty)) -let error_not_product_loc loc env sigma c = - raise_pretype_error (loc, env, sigma, NotProduct c) +let error_not_product ?loc env sigma c = + raise_pretype_error ?loc (env, sigma, NotProduct c) (*s Error in conversion from AST to glob_constr *) -let error_var_not_found_loc loc s = - raise_pretype_error (loc, empty_env, Evd.empty, VarNotFound s) +let error_var_not_found ?loc s = + raise_pretype_error ?loc (empty_env, Evd.empty, VarNotFound s) (*s Typeclass errors *) @@ -166,7 +162,7 @@ let unsatisfiable_constraints env evd ev comp = | Some ev -> let loc, kind = Evd.evar_source ev evd in let err = UnsatisfiableConstraints (Some (ev, kind), comp) in - Loc.raise loc (PretypeError (env,evd,err)) + Loc.raise ~loc (PretypeError (env,evd,err)) let unsatisfiable_exception exn = match exn with diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli index 880f48e5f..73f81923f 100644 --- a/pretyping/pretype_errors.mli +++ b/pretyping/pretype_errors.mli @@ -64,35 +64,35 @@ exception PretypeError of env * Evd.evar_map * pretype_error val precatchable_exception : exn -> bool (** Raising errors *) -val error_actual_type_loc : - Loc.t -> env -> Evd.evar_map -> unsafe_judgment -> constr -> +val error_actual_type : + ?loc:Loc.t -> env -> Evd.evar_map -> unsafe_judgment -> constr -> unification_error -> 'b -val error_cant_apply_not_functional_loc : - Loc.t -> env -> Evd.evar_map -> +val error_cant_apply_not_functional : + ?loc:Loc.t -> env -> Evd.evar_map -> unsafe_judgment -> unsafe_judgment list -> 'b -val error_cant_apply_bad_type_loc : - Loc.t -> env -> Evd.evar_map -> int * constr * constr -> +val error_cant_apply_bad_type : + ?loc:Loc.t -> env -> Evd.evar_map -> int * constr * constr -> unsafe_judgment -> unsafe_judgment list -> 'b -val error_case_not_inductive_loc : - Loc.t -> env -> Evd.evar_map -> unsafe_judgment -> 'b +val error_case_not_inductive : + ?loc:Loc.t -> env -> Evd.evar_map -> unsafe_judgment -> 'b -val error_ill_formed_branch_loc : - Loc.t -> env -> Evd.evar_map -> +val error_ill_formed_branch : + ?loc:Loc.t -> env -> Evd.evar_map -> constr -> pconstructor -> constr -> constr -> 'b -val error_number_branches_loc : - Loc.t -> env -> Evd.evar_map -> +val error_number_branches : + ?loc:Loc.t -> env -> Evd.evar_map -> unsafe_judgment -> int -> 'b -val error_ill_typed_rec_body_loc : - Loc.t -> env -> Evd.evar_map -> +val error_ill_typed_rec_body : + ?loc:Loc.t -> env -> Evd.evar_map -> int -> Name.t array -> unsafe_judgment array -> types array -> 'b -val error_not_a_type_loc : - Loc.t -> env -> Evd.evar_map -> unsafe_judgment -> 'b +val error_not_a_type : + ?loc:Loc.t -> env -> Evd.evar_map -> unsafe_judgment -> 'b val error_cannot_coerce : env -> Evd.evar_map -> constr * constr -> 'b @@ -101,15 +101,12 @@ val error_cannot_coerce : env -> Evd.evar_map -> constr * constr -> 'b val error_occur_check : env -> Evd.evar_map -> existential_key -> constr -> 'b val error_unsolvable_implicit : - Loc.t -> env -> Evd.evar_map -> existential_key -> + ?loc:Loc.t -> env -> Evd.evar_map -> existential_key -> Evd.unsolvability_explanation option -> 'b -val error_cannot_unify_loc : Loc.t -> env -> Evd.evar_map -> +val error_cannot_unify : ?loc:Loc.t -> env -> Evd.evar_map -> ?reason:unification_error -> constr * constr -> 'b -val error_cannot_unify : env -> Evd.evar_map -> ?reason:unification_error -> - constr * constr -> 'b - val error_cannot_unify_local : env -> Evd.evar_map -> constr * constr * constr -> 'b val error_cannot_find_well_typed_abstraction : env -> Evd.evar_map -> @@ -126,20 +123,20 @@ val error_non_linear_unification : env -> Evd.evar_map -> (** {6 Ml Case errors } *) -val error_cant_find_case_type_loc : - Loc.t -> env -> Evd.evar_map -> constr -> 'b +val error_cant_find_case_type : + ?loc:Loc.t -> env -> Evd.evar_map -> constr -> 'b (** {6 Pretyping errors } *) -val error_unexpected_type_loc : - Loc.t -> env -> Evd.evar_map -> constr -> constr -> 'b +val error_unexpected_type : + ?loc:Loc.t -> env -> Evd.evar_map -> constr -> constr -> 'b -val error_not_product_loc : - Loc.t -> env -> Evd.evar_map -> constr -> 'b +val error_not_product : + ?loc:Loc.t -> env -> Evd.evar_map -> constr -> 'b (** {6 Error in conversion from AST to glob_constr } *) -val error_var_not_found_loc : Loc.t -> Id.t -> 'b +val error_var_not_found : ?loc:Loc.t -> Id.t -> 'b (** {6 Typeclass errors } *) diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 1ef96e034..8b0bdb009 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -160,7 +160,7 @@ let search_guard loc env possible_indexes fixdefs = with TypeError _ -> ()) (List.combinations possible_indexes); let errmsg = "Cannot guess decreasing argument of fix." in - user_err_loc (loc,"search_guard", Pp.str errmsg) + user_err ~loc "search_guard" (Pp.str errmsg) with Found indexes -> indexes) (* To force universe name declaration before use *) @@ -211,8 +211,8 @@ let interp_universe_level_name evd (loc,s) = with Not_found -> if not (is_strict_universe_declarations ()) then new_univ_level_variable ~loc ~name:s univ_rigid evd - else user_err_loc (loc, "interp_universe_level_name", - Pp.(str "Undeclared universe: " ++ str s)) + else user_err ~loc "interp_universe_level_name" + (Pp.(str "Undeclared universe: " ++ str s)) let interp_universe ?loc evd = function | [] -> let evd, l = new_univ_level_variable ?loc univ_rigid evd in @@ -298,7 +298,7 @@ let check_extra_evars_are_solved env current_sigma pending = match k with | Evar_kinds.ImplicitArg (gr, (i, id), false) -> () | _ -> - error_unsolvable_implicit loc env current_sigma evk None) pending + error_unsolvable_implicit ~loc env current_sigma evk None) pending (* [check_evars] fails if some unresolved evar remains *) @@ -313,7 +313,7 @@ let check_evars env initial_sigma sigma c = let (loc,k) = evar_source evk sigma in match k with | Evar_kinds.ImplicitArg (gr, (i, id), false) -> () - | _ -> Pretype_errors.error_unsolvable_implicit loc env sigma evk None) + | _ -> Pretype_errors.error_unsolvable_implicit ~loc env sigma evk None) | _ -> Constr.iter proc_rec c in proc_rec c @@ -359,7 +359,7 @@ let evar_type_fixpoint loc env evdref lna lar vdefj = for i = 0 to lt-1 do if not (e_cumul env.ExtraEnv.env evdref (vdefj.(i)).uj_type (lift lt lar.(i))) then - error_ill_typed_rec_body_loc loc env.ExtraEnv.env !evdref + error_ill_typed_rec_body ~loc env.ExtraEnv.env !evdref i lna vdefj lar done @@ -373,9 +373,9 @@ let check_instance loc subst = function | [] -> () | (id,_) :: _ -> if List.mem_assoc id subst then - user_err_loc (loc,"",pr_id id ++ str "appears more than once.") + user_err ~loc "" (pr_id id ++ str "appears more than once.") else - user_err_loc (loc,"",str "No such variable in the signature of the existential variable: " ++ pr_id id ++ str ".") + user_err ~loc "" (str "No such variable in the signature of the existential variable: " ++ pr_id id ++ str ".") (* used to enforce a name in Lambda when the type constraints itself is named, hence possibly dependent *) @@ -454,8 +454,8 @@ let pretype_id pretype k0 loc env evdref lvar id = (* and build a nice error message *) if Id.Map.mem id lvar.ltac_genargs then begin let Geninterp.Val.Dyn (typ, _) = Id.Map.find id lvar.ltac_genargs in - user_err_loc (loc,"", - str "Variable " ++ pr_id id ++ str " should be bound to a term but is \ + user_err ~loc "" + (str "Variable " ++ pr_id id ++ str " should be bound to a term but is \ bound to a " ++ Geninterp.Val.pr typ ++ str ".") end; (* Check if [id] is a section or goal variable *) @@ -463,7 +463,7 @@ let pretype_id pretype k0 loc env evdref lvar id = { uj_val = mkVar id; uj_type = (get_type (lookup_named id env)) } with Not_found -> (* [id] not found, standard error message *) - error_var_not_found_loc loc id + error_var_not_found ~loc id let evar_kind_of_term sigma c = kind_of_term (whd_evar sigma c) @@ -486,16 +486,16 @@ let pretype_global loc rigid env evd gr us = let arr = Univ.Instance.to_array (Univ.UContext.instance ctx) in let len = Array.length arr in if len != List.length l then - user_err_loc (loc, "pretype", - str "Universe instance should have length " ++ int len) + user_err ~loc "pretype" + (str "Universe instance should have length " ++ int len) else let evd, l' = List.fold_left (fun (evd, univs) l -> let evd, l = interp_universe_level_name loc evd l in (evd, l :: univs)) (evd, []) l in if List.exists (fun l -> Univ.Level.is_prop l) l' then - user_err_loc (loc, "pretype", - str "Universe instances cannot contain Prop, polymorphic" ++ + user_err ~loc "pretype" + (str "Universe instances cannot contain Prop, polymorphic" ++ str " universe instances must be greater or equal to Set."); evd, Some (Univ.Instance.of_array (Array.of_list (List.rev l'))) in @@ -510,7 +510,7 @@ let pretype_ref loc evdref env ref us = (* This may happen if env is a goal env and section variables have been cleared - section variables should be different from goal variables *) - Pretype_errors.error_var_not_found_loc loc id) + Pretype_errors.error_var_not_found ~loc id) | ref -> let evd, c = pretype_global loc univ_flexible env !evdref ref us in let () = evdref := evd in @@ -566,7 +566,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let evk = try Evd.evar_key id !evdref with Not_found -> - user_err_loc (loc,"",str "Unknown existential variable.") in + user_err ~loc "" (str "Unknown existential variable.") in let hyps = evar_filtered_context (Evd.find !evdref evk) in let args = pretype_instance k0 resolve_tc env evdref lvar loc hyps evk inst in let c = mkEvar (evk, args) in @@ -749,9 +749,9 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre | _ -> let hj = pretype empty_tycon env evdref lvar c in - error_cant_apply_not_functional_loc - (Loc.merge floc argloc) env.ExtraEnv.env !evdref - resj [hj] + error_cant_apply_not_functional + ~loc:(Loc.merge floc argloc) env.ExtraEnv.env !evdref + resj [hj] in let resj = apply_rec env 1 fj candargs args in let resj = @@ -844,15 +844,15 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre try find_rectype env.ExtraEnv.env !evdref cj.uj_type with Not_found -> let cloc = loc_of_glob_constr c in - error_case_not_inductive_loc cloc env.ExtraEnv.env !evdref cj + error_case_not_inductive ~loc:cloc env.ExtraEnv.env !evdref cj in let cstrs = get_constructors env.ExtraEnv.env indf in if not (Int.equal (Array.length cstrs) 1) then - user_err_loc (loc,"",str "Destructing let is only for inductive types" ++ + user_err ~loc "" (str "Destructing let is only for inductive types" ++ str " with one constructor."); let cs = cstrs.(0) in if not (Int.equal (List.length nal) cs.cs_nargs) then - user_err_loc (loc,"", str "Destructing let on this type expects " ++ + user_err ~loc:loc "" (str "Destructing let on this type expects " ++ int cs.cs_nargs ++ str " variables."); let fsign, record = match get_projections env.ExtraEnv.env indf with @@ -918,7 +918,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre if noccur_between 1 cs.cs_nargs ccl then lift (- cs.cs_nargs) ccl else - error_cant_find_case_type_loc loc env.ExtraEnv.env !evdref + error_cant_find_case_type ~loc env.ExtraEnv.env !evdref cj.uj_val in (* let ccl = refresh_universes ccl in *) let p = it_mkLambda_or_LetIn (lift (nar+1) ccl) psign in @@ -934,11 +934,11 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre try find_rectype env.ExtraEnv.env !evdref cj.uj_type with Not_found -> let cloc = loc_of_glob_constr c in - error_case_not_inductive_loc cloc env.ExtraEnv.env !evdref cj in + error_case_not_inductive ~loc:cloc env.ExtraEnv.env !evdref cj in let cstrs = get_constructors env.ExtraEnv.env indf in if not (Int.equal (Array.length cstrs) 2) then - user_err_loc (loc,"", - str "If is only for inductive types with two constructors."); + user_err ~loc "" + (str "If is only for inductive types with two constructors."); let arsgn = let arsgn,_ = get_arity env.ExtraEnv.env indf in @@ -1020,9 +1020,9 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let (evd,b) = Reductionops.vm_infer_conv env.ExtraEnv.env !evdref cty tval in if b then (evdref := evd; cj, tval) else - error_actual_type_loc loc env.ExtraEnv.env !evdref cj tval + error_actual_type ~loc env.ExtraEnv.env !evdref cj tval (ConversionFailed (env.ExtraEnv.env,cty,tval)) - else user_err_loc (loc,"",str "Cannot check cast with vm: " ++ + else user_err ~loc "" (str "Cannot check cast with vm: " ++ str "unresolved arguments remain.") | NATIVEcast -> let cj = pretype empty_tycon env evdref lvar c in @@ -1031,7 +1031,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let (evd,b) = Nativenorm.native_infer_conv env.ExtraEnv.env !evdref cty tval in if b then (evdref := evd; cj, tval) else - error_actual_type_loc loc env.ExtraEnv.env !evdref cj tval + error_actual_type ~loc env.ExtraEnv.env !evdref cj tval (ConversionFailed (env.ExtraEnv.env,cty,tval)) end | _ -> @@ -1059,7 +1059,7 @@ and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update = let t' = lookup_named id env |> get_type in if is_conv env.ExtraEnv.env !evdref t t' then mkVar id, update else raise Not_found with Not_found -> - user_err_loc (loc,"",str "Cannot interpret " ++ + user_err ~loc "" (str "Cannot interpret " ++ pr_existential_key !evdref evk ++ str " in current context: no binding for " ++ pr_id id ++ str ".") in ((id,c)::subst, update) in @@ -1097,8 +1097,8 @@ and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar = function | Some v -> if e_cumul env.ExtraEnv.env evdref v tj.utj_val then tj else - error_unexpected_type_loc - (loc_of_glob_constr c) env.ExtraEnv.env !evdref tj.utj_val v + error_unexpected_type + ~loc:(loc_of_glob_constr c) env.ExtraEnv.env !evdref tj.utj_val v let ise_pretype_gen flags env sigma lvar kind c = let env = make_env env in |