diff options
Diffstat (limited to 'pretyping/pretype_errors.ml')
| -rw-r--r-- | pretyping/pretype_errors.ml | 153 |
1 files changed, 70 insertions, 83 deletions
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index 52122974..030b4a11 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -1,100 +1,68 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Compat open Util open Names -open Sign open Term -open Termops -open Namegen open Environ open Type_errors -open Glob_term -open Inductiveops + +type unification_error = + | OccurCheck of existential_key * 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 + | UnifUnivInconsistency of Univ.univ_inconsistency + | CannotSolveConstraint of Evd.evar_constraint * unification_error + +type position = (Id.t * Locus.hyp_location_flag) option + +type position_reporting = (position * int) * constr + +type subterm_unification_error = bool * position_reporting * position_reporting * (constr * constr * unification_error) option type pretype_error = (* Old Case *) | CantFindCaseType of constr - (* Unification *) - | OccurCheck of existential_key * constr - | NotClean of existential_key * constr * Evd.hole_kind - | UnsolvableImplicit of Evd.evar_info * Evd.hole_kind * - Evd.unsolvability_explanation option - | CannotUnify of constr * 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 + | CannotUnify of constr * constr * unification_error option | CannotUnifyLocal of constr * constr * constr | CannotUnifyBindingType of constr * constr | CannotGeneralize of constr - | NoOccurrenceFound of constr * identifier option - | CannotFindWellTypedAbstraction of constr * constr list - | AbstractionOverMeta of name * name - | NonLinearUnification of name * constr + | NoOccurrenceFound of constr * Id.t option + | CannotFindWellTypedAbstraction of constr * constr list * (env * type_error) option + | WrongAbstractionType of Name.t * constr * types * types + | AbstractionOverMeta of Name.t * Name.t + | NonLinearUnification of Name.t * constr (* Pretyping *) - | VarNotFound of identifier + | VarNotFound of Id.t | UnexpectedType of constr * constr | NotProduct of constr | TypingError of type_error + | CannotUnifyOccurrences of subterm_unification_error + | UnsatisfiableConstraints of + (existential_key * Evar_kinds.t) option * Evar.Set.t option exception PretypeError of env * Evd.evar_map * pretype_error let precatchable_exception = function - | Util.UserError _ | TypeError _ | PretypeError _ - | Loc.Exc_located(_,(Util.UserError _ | TypeError _ | - Nametab.GlobalizationError _ | PretypeError _)) -> true + | Errors.UserError _ | TypeError _ | PretypeError _ + | Nametab.GlobalizationError _ -> true | _ -> false -let nf_evar = Reductionops.nf_evar -let j_nf_evar sigma j = - { uj_val = nf_evar sigma j.uj_val; - uj_type = nf_evar sigma j.uj_type } -let j_nf_betaiotaevar sigma j = - { uj_val = nf_evar sigma j.uj_val; - uj_type = Reductionops.nf_betaiota sigma j.uj_type } -let jl_nf_evar sigma jl = List.map (j_nf_evar sigma) jl -let jv_nf_betaiotaevar sigma jl = - Array.map (j_nf_betaiotaevar sigma) jl -let jv_nf_evar sigma = Array.map (j_nf_evar sigma) -let tj_nf_evar sigma {utj_val=v;utj_type=t} = - {utj_val=nf_evar sigma v;utj_type=t} - -let env_nf_evar sigma env = - process_rel_context - (fun d e -> push_rel (map_rel_declaration (nf_evar sigma) d) e) env - -let env_nf_betaiotaevar sigma env = - process_rel_context - (fun d e -> - push_rel (map_rel_declaration (Reductionops.nf_betaiota sigma) d) e) env - -(* This simplifies the typing context of Cases clauses *) -(* hope it does not disturb other typing contexts *) -let contract env lc = - let l = ref [] in - let contract_context (na,c,t) env = - match c with - | Some c' when isRel c' -> - l := (substl !l c') :: !l; - env - | _ -> - let t' = substl !l t in - let c' = Option.map (substl !l) c in - let na' = named_hd env t' na in - l := (mkRel 1) :: List.map (lift 1) !l; - push_rel (na',c',t') env in - let env = process_rel_context contract_context env in - (env, List.map (substl !l) lc) - -let contract2 env a b = match contract env [a;b] with - | env, [a;b] -> env,a,b | _ -> assert false - -let contract3 env a b c = match contract env [a;b;c] with - | env, [a;b;c] -> env,a,b,c | _ -> assert false - let raise_pretype_error (loc,env,sigma,te) = Loc.raise loc (PretypeError(env,sigma,te)) @@ -102,10 +70,10 @@ let raise_located_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 = - let env, c, actty, expty = contract3 env c actty expty in +let error_actual_type_loc loc env sigma {uj_val=c;uj_type=actty} expty reason = let j = {uj_val=c;uj_type=actty} in - raise_located_type_error (loc, env, sigma, ActualType (j, expty)) + 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 @@ -137,26 +105,29 @@ let error_not_a_type_loc loc env sigma j = a precise location. *) let error_occur_check env sigma ev c = - raise (PretypeError (env, sigma, OccurCheck (ev,c))) - -let error_not_clean env sigma ev c (loc,k) = - Loc.raise loc (PretypeError (env, sigma, NotClean (ev,c,k))) + raise (PretypeError (env, sigma, UnifOccurCheck (ev,c))) -let error_unsolvable_implicit loc env sigma evi e explain = +let error_unsolvable_implicit loc env sigma evk explain = Loc.raise loc - (PretypeError (env, sigma, UnsolvableImplicit (evi, e, explain))) + (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 (m,n) = - raise (PretypeError (env, sigma,CannotUnify (m,n))) +let error_cannot_unify env sigma ?reason (m,n) = + raise (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))) let error_cannot_coerce env sigma (m,n) = - raise (PretypeError (env, sigma,CannotUnify (m,n))) + raise (PretypeError (env, sigma,CannotUnify (m,n,None))) -let error_cannot_find_well_typed_abstraction env sigma p l = - raise (PretypeError (env, sigma,CannotFindWellTypedAbstraction (p,l))) +let error_cannot_find_well_typed_abstraction env sigma p l e = + raise (PretypeError (env, sigma,CannotFindWellTypedAbstraction (p,l,e))) + +let error_wrong_abstraction_type env sigma na a p l = + raise (PretypeError (env, sigma,WrongAbstractionType (na,a,p,l))) let error_abstraction_over_meta env sigma hdmeta metaarg = let m = Evd.meta_name sigma hdmeta and n = Evd.meta_name sigma metaarg in @@ -174,7 +145,6 @@ let error_cant_find_case_type_loc loc env sigma expr = (*s Pretyping errors *) let error_unexpected_type_loc loc env sigma actty expty = - let env, actty, expty = contract2 env actty expty in raise_pretype_error (loc, env, sigma, UnexpectedType (actty, expty)) let error_not_product_loc loc env sigma c = @@ -184,3 +154,20 @@ let error_not_product_loc loc env sigma c = let error_var_not_found_loc loc s = raise_pretype_error (loc, empty_env, Evd.empty, VarNotFound s) + +(*s Typeclass errors *) + +let unsatisfiable_constraints env evd ev comp = + match ev with + | None -> + let err = UnsatisfiableConstraints (None, comp) in + raise (PretypeError (env,evd,err)) + | 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)) + +let unsatisfiable_exception exn = + match exn with + | PretypeError (_, _, UnsatisfiableConstraints _) -> true + | _ -> false |