diff options
Diffstat (limited to 'pretyping/pretype_errors.mli')
-rw-r--r-- | pretyping/pretype_errors.mli | 99 |
1 files changed, 56 insertions, 43 deletions
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli index 880f48e5..6f14d025 100644 --- a/pretyping/pretype_errors.mli +++ b/pretyping/pretype_errors.mli @@ -1,27 +1,30 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names -open Term +open Constr open Environ +open EConstr open Type_errors (** {6 The type of errors raised by the pretyper } *) type unification_error = - | OccurCheck of existential_key * constr + | OccurCheck of Evar.t * constr | NotClean of existential * env * constr | NotSameArgSize | NotSameHead | NoCanonicalStructure | ConversionFailed of env * constr * constr - | MetaOccurInBody of existential_key - | InstanceNotSameType of existential_key * env * types * types + | MetaOccurInBody of Evar.t + | InstanceNotSameType of Evar.t * env * types * types | UnifUnivInconsistency of Univ.univ_inconsistency | CannotSolveConstraint of Evd.evar_constraint * unification_error | ProblemBeyondCapabilities @@ -32,14 +35,16 @@ type position_reporting = (position * int) * constr type subterm_unification_error = bool * position_reporting * position_reporting * (constr * constr * unification_error) option +type type_error = (constr, types) ptype_error + type pretype_error = (** Old Case *) | CantFindCaseType of constr (** Type inference unification *) | ActualTypeNotCoercible of unsafe_judgment * types * unification_error (** Tactic Unification *) - | UnifOccurCheck of existential_key * constr - | UnsolvableImplicit of existential_key * Evd.unsolvability_explanation option + | UnifOccurCheck of Evar.t * constr + | UnsolvableImplicit of Evar.t * Evd.unsolvability_explanation option | CannotUnify of constr * constr * unification_error option | CannotUnifyLocal of constr * constr * constr | CannotUnifyBindingType of constr * constr @@ -56,7 +61,7 @@ type pretype_error = | TypingError of type_error | CannotUnifyOccurrences of subterm_unification_error | UnsatisfiableConstraints of - (existential_key * Evar_kinds.t) option * Evar.Set.t option + (Evar.t * Evar_kinds.t) option * Evar.Set.t option (** unresolvable evar, connex component *) exception PretypeError of env * Evd.evar_map * pretype_error @@ -64,52 +69,60 @@ 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 -> - unsafe_judgment -> unsafe_judgment list -> 'b +val error_actual_type_core : + ?loc:Loc.t -> env -> Evd.evar_map -> unsafe_judgment -> constr -> 'b + +val error_cant_apply_not_functional : + ?loc:Loc.t -> env -> Evd.evar_map -> + unsafe_judgment -> unsafe_judgment array -> 'b -val error_cant_apply_bad_type_loc : - Loc.t -> env -> Evd.evar_map -> int * constr * constr -> - unsafe_judgment -> unsafe_judgment list -> 'b +val error_cant_apply_bad_type : + ?loc:Loc.t -> env -> Evd.evar_map -> int * constr * constr -> + unsafe_judgment -> unsafe_judgment array -> '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_elim_arity : + ?loc:Loc.t -> env -> Evd.evar_map -> + pinductive -> Sorts.family list -> constr -> + unsafe_judgment -> (Sorts.family * Sorts.family * arity_error) option -> 'b + +val error_not_a_type : + ?loc:Loc.t -> env -> Evd.evar_map -> unsafe_judgment -> 'b + +val error_assumption : + ?loc:Loc.t -> env -> Evd.evar_map -> unsafe_judgment -> 'b val error_cannot_coerce : env -> Evd.evar_map -> constr * constr -> 'b (** {6 Implicit arguments synthesis errors } *) -val error_occur_check : env -> Evd.evar_map -> existential_key -> constr -> 'b +val error_occur_check : env -> Evd.evar_map -> Evar.t -> constr -> 'b val error_unsolvable_implicit : - Loc.t -> env -> Evd.evar_map -> existential_key -> + ?loc:Loc.t -> env -> Evd.evar_map -> Evar.t -> 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,24 +139,24 @@ 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 } *) -val unsatisfiable_constraints : env -> Evd.evar_map -> Evd.evar option -> +val unsatisfiable_constraints : env -> Evd.evar_map -> Evar.t option -> Evar.Set.t option -> 'a val unsatisfiable_exception : exn -> bool |