diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-11 00:29:02 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:27:27 +0100 |
| commit | ca993b9e7765ac58f70740818758457c9367b0da (patch) | |
| tree | a813ef9a194638afbb09cefe1d1e2bce113a9d84 /pretyping/pretype_errors.ml | |
| parent | c2855a3387be134d1220f301574b743572a94239 (diff) | |
Making judgment type generic over the type of inner constrs.
This allows to factorize code and prevents the unnecessary use of back and
forth conversions between the various types of terms.
Note that functions from typing may now raise errors as PretypeError rather
than TypeError, because they call the proper wrapper. I think that they were
wrongly calling the kernel because of an overlook of open modules.
Diffstat (limited to 'pretyping/pretype_errors.ml')
| -rw-r--r-- | pretyping/pretype_errors.ml | 24 |
1 files changed, 19 insertions, 5 deletions
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index 14b25ab36..673554005 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -31,11 +31,13 @@ type position_reporting = (position * int) * EConstr.t type subterm_unification_error = bool * position_reporting * position_reporting * (EConstr.constr * EConstr.constr * unification_error) option +type type_error = (EConstr.constr, EConstr.types) ptype_error + type pretype_error = (* Old Case *) - | CantFindCaseType of constr + | CantFindCaseType of EConstr.constr (* Type inference unification *) - | ActualTypeNotCoercible of unsafe_judgment * types * unification_error + | ActualTypeNotCoercible of EConstr.unsafe_judgment * EConstr.types * unification_error (* Tactic unification *) | UnifOccurCheck of existential_key * EConstr.constr | UnsolvableImplicit of existential_key * Evd.unsolvability_explanation option @@ -50,7 +52,7 @@ type pretype_error = | NonLinearUnification of Name.t * EConstr.constr (* Pretyping *) | VarNotFound of Id.t - | UnexpectedType of constr * constr + | UnexpectedType of EConstr.constr * EConstr.constr | NotProduct of EConstr.constr | TypingError of type_error | CannotUnifyOccurrences of subterm_unification_error @@ -75,14 +77,19 @@ let error_actual_type ?loc env sigma {uj_val=c;uj_type=actty} expty reason = raise_pretype_error ?loc (env, sigma, ActualTypeNotCoercible (j, expty, reason)) +let error_actual_type_core ?loc env sigma {uj_val=c;uj_type=actty} expty = + let j = {uj_val=c;uj_type=actty} in + raise_type_error ?loc + (env, sigma, ActualType (j, expty)) + let error_cant_apply_not_functional ?loc env sigma rator randl = raise_type_error ?loc - (env, sigma, CantApplyNonFunctional (rator, Array.of_list randl)) + (env, sigma, CantApplyNonFunctional (rator, randl)) 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)) + CantApplyBadType ((n,c,t), rator, randl)) let error_ill_formed_branch ?loc env sigma c i actty expty = raise_type_error @@ -98,9 +105,16 @@ 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_elim_arity ?loc env sigma pi s c j a = + raise_type_error ?loc + (env, sigma, ElimArity (pi, s, c, j, a)) + let error_not_a_type ?loc env sigma j = raise_type_error ?loc (env, sigma, NotAType j) +let error_assumption ?loc env sigma j = + raise_type_error ?loc (env, sigma, BadAssumption j) + (*s Implicit arguments synthesis errors. It is hard to find a precise location. *) |