diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/pretype_errors.ml | 79 | ||||
| -rw-r--r-- | pretyping/pretype_errors.mli | 41 | ||||
| -rw-r--r-- | pretyping/unification.ml | 12 |
3 files changed, 57 insertions, 75 deletions
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index eb07addb07..cd2ed76c1f 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -38,8 +38,9 @@ type pretype_error = | VarNotFound of identifier | UnexpectedType of constr * constr | NotProduct of constr + | TypingError of type_error -exception PretypeError of env * pretype_error +exception PretypeError of env * Evd.evar_map * pretype_error let precatchable_exception = function | Util.UserError _ | TypeError _ | PretypeError _ @@ -55,13 +56,13 @@ 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 jl_nf_betaiotaevar sigma jl = - List.map (j_nf_betaiotaevar 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_ise sigma env = +let env_nf_evar sigma env = let sign = named_context_val env in let ctxt = rel_context env in let env0 = reset_with_named_context sign env in @@ -97,110 +98,90 @@ let contract2 env a b = match contract env [a;b] with 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,ctx,sigma,te) = - Loc.raise loc (PretypeError(env_ise sigma ctx,te)) +let raise_pretype_error (loc,env,sigma,te) = + Loc.raise loc (PretypeError(env,sigma,te)) -let raise_located_type_error (loc,ctx,sigma,te) = - Loc.raise loc (TypeError(env_ise sigma ctx,te)) +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 j = j_nf_evar sigma {uj_val=c;uj_type=actty} in - raise_located_type_error - (loc, env, sigma, ActualType (j, nf_evar sigma expty)) + let j = {uj_val=c;uj_type=actty} in + raise_located_type_error (loc, env, sigma, ActualType (j, expty)) let error_cant_apply_not_functional_loc loc env sigma rator randl = - let ja = Array.of_list (jl_nf_evar sigma randl) in raise_located_type_error - (loc, env, sigma, - CantApplyNonFunctional (j_nf_evar sigma rator, ja)) + (loc, env, sigma, CantApplyNonFunctional (rator, Array.of_list randl)) let error_cant_apply_bad_type_loc loc env sigma (n,c,t) rator randl = - let ja = Array.of_list (jl_nf_betaiotaevar sigma randl) in raise_located_type_error (loc, env, sigma, - CantApplyBadType - ((n,nf_evar sigma c, Reductionops.nf_betaiota sigma t), - j_nf_evar sigma rator, ja)) + CantApplyBadType ((n,c,t), rator, Array.of_list randl)) let error_ill_formed_branch_loc loc env sigma c i actty expty = - let simp t = Reduction.nf_betaiota (nf_evar sigma t) in raise_located_type_error - (loc, env, sigma, - IllFormedBranch (nf_evar sigma c,i,simp actty, simp expty)) + (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 (j_nf_evar sigma cj, expn)) + raise_located_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 (j_nf_evar sigma cj)) + raise_located_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,jv_nf_evar sigma jl, - Array.map (nf_evar sigma) tys)) + (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_nf_evar sigma j)) + raise_located_type_error (loc, env, sigma, NotAType j) (*s Implicit arguments synthesis errors. It is hard to find a precise location. *) let error_occur_check env sigma ev c = - let c = nf_evar sigma c in - raise (PretypeError (env_ise sigma env, OccurCheck (ev,c))) + raise (PretypeError (env, sigma, OccurCheck (ev,c))) let error_not_clean env sigma ev c (loc,k) = - let c = nf_evar sigma c in - Loc.raise loc - (PretypeError (env_ise sigma env, NotClean (ev,c,k))) + Loc.raise loc (PretypeError (env, sigma, NotClean (ev,c,k))) let error_unsolvable_implicit loc env sigma evi e explain = Loc.raise loc - (PretypeError (env_ise sigma env, UnsolvableImplicit (evi, e, explain))) + (PretypeError (env, sigma, UnsolvableImplicit (evi, e, explain))) let error_cannot_unify env sigma (m,n) = - let m = nf_evar sigma m and n = nf_evar sigma n in - raise (PretypeError (env_ise sigma env,CannotUnify (m,n))) + raise (PretypeError (env, sigma,CannotUnify (m,n))) let error_cannot_unify_local env sigma (m,n,sn) = - raise (PretypeError (env_ise sigma env,CannotUnifyLocal (m,n,sn))) + raise (PretypeError (env, sigma,CannotUnifyLocal (m,n,sn))) let error_cannot_coerce env sigma (m,n) = - raise (PretypeError (env_ise sigma env,CannotUnify (m,n))) + raise (PretypeError (env, sigma,CannotUnify (m,n))) let error_cannot_find_well_typed_abstraction env sigma p l = - raise (PretypeError (env_ise sigma env,CannotFindWellTypedAbstraction (p,l))) + raise (PretypeError (env, sigma,CannotFindWellTypedAbstraction (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 - raise (PretypeError (env_ise sigma env,AbstractionOverMeta (m,n))) + raise (PretypeError (env, sigma,AbstractionOverMeta (m,n))) let error_non_linear_unification env sigma hdmeta t = let m = Evd.meta_name sigma hdmeta in - raise (PretypeError (env_ise sigma env,NonLinearUnification (m,t))) + raise (PretypeError (env, sigma,NonLinearUnification (m,t))) (*s Ml Case errors *) let error_cant_find_case_type_loc loc env sigma expr = - raise_pretype_error - (loc, env, sigma, CantFindCaseType (nf_evar sigma expr)) + raise_pretype_error (loc, env, sigma, CantFindCaseType 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 (nf_evar sigma actty, nf_evar sigma 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 (nf_evar sigma c)) + raise_pretype_error (loc, env, sigma, NotProduct c) (*s Error in conversion from AST to rawterms *) diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli index d81adb6b01..cdf6b523c9 100644 --- a/pretyping/pretype_errors.mli +++ b/pretyping/pretype_errors.mli @@ -37,47 +37,48 @@ type pretype_error = | VarNotFound of identifier | UnexpectedType of constr * constr | NotProduct of constr + | TypingError of Type_errors.type_error -exception PretypeError of env * pretype_error +exception PretypeError of env * Evd.evar_map * pretype_error val precatchable_exception : exn -> bool (** Presenting terms without solved evars *) -val nf_evar : Evd.evar_map -> constr -> constr -val j_nf_evar : Evd.evar_map -> unsafe_judgment -> unsafe_judgment -val jl_nf_evar : - Evd.evar_map -> unsafe_judgment list -> unsafe_judgment list -val jv_nf_evar : - Evd.evar_map -> unsafe_judgment array -> unsafe_judgment array -val tj_nf_evar : - Evd.evar_map -> unsafe_type_judgment -> unsafe_type_judgment +val nf_evar : Evd.evar_map -> constr -> constr +val j_nf_evar : Evd.evar_map -> unsafe_judgment -> unsafe_judgment +val jl_nf_evar : Evd.evar_map -> unsafe_judgment list -> unsafe_judgment list +val jv_nf_evar : Evd.evar_map -> unsafe_judgment array -> unsafe_judgment array +val tj_nf_evar : Evd.evar_map -> unsafe_type_judgment -> unsafe_type_judgment +val env_nf_evar : Evd.evar_map -> env -> env +val jv_nf_betaiotaevar : + Evd.evar_map -> unsafe_judgment array -> unsafe_judgment array (** Raising errors *) val error_actual_type_loc : - loc -> env -> Evd.evar_map -> unsafe_judgment -> constr -> 'b + loc -> env -> Evd.evar_map -> unsafe_judgment -> constr -> 'b val error_cant_apply_not_functional_loc : - loc -> env -> Evd.evar_map -> + loc -> env -> Evd.evar_map -> unsafe_judgment -> unsafe_judgment list -> 'b val error_cant_apply_bad_type_loc : - loc -> env -> Evd.evar_map -> int * constr * constr -> + loc -> env -> Evd.evar_map -> int * constr * constr -> unsafe_judgment -> unsafe_judgment list -> 'b val error_case_not_inductive_loc : - loc -> env -> Evd.evar_map -> unsafe_judgment -> 'b + loc -> env -> Evd.evar_map -> unsafe_judgment -> 'b val error_ill_formed_branch_loc : - loc -> env -> Evd.evar_map -> + loc -> env -> Evd.evar_map -> constr -> int -> constr -> constr -> 'b val error_number_branches_loc : - loc -> env -> Evd.evar_map -> + loc -> env -> Evd.evar_map -> unsafe_judgment -> int -> 'b val error_ill_typed_rec_body_loc : - loc -> env -> Evd.evar_map -> + loc -> env -> Evd.evar_map -> int -> name array -> unsafe_judgment array -> types array -> 'b val error_not_a_type_loc : @@ -87,7 +88,7 @@ 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 -> existential_key -> constr -> 'b val error_not_clean : env -> Evd.evar_map -> existential_key -> constr -> loc * Evd.hole_kind -> 'b @@ -112,15 +113,15 @@ val error_non_linear_unification : env -> Evd.evar_map -> (** {6 Ml Case errors } *) val error_cant_find_case_type_loc : - loc -> env -> Evd.evar_map -> constr -> 'b + loc -> env -> Evd.evar_map -> constr -> 'b (** {6 Pretyping errors } *) val error_unexpected_type_loc : - loc -> env -> Evd.evar_map -> constr -> constr -> 'b + loc -> env -> Evd.evar_map -> constr -> constr -> 'b val error_not_product_loc : - loc -> env -> Evd.evar_map -> constr -> 'b + loc -> env -> Evd.evar_map -> constr -> 'b (** {6 Error in conversion from AST to rawterms } *) diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 38cf59bc0d..6c17567c31 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -844,7 +844,7 @@ let w_unify_to_subterm env ?(flags=default_unify_flags) (op,cl) evd = in try matchrec cl with ex when precatchable_exception ex -> - raise (PretypeError (env,NoOccurrenceFound (op, None))) + raise (PretypeError (env,evd,NoOccurrenceFound (op, None))) (* Tries to find all instances of term [cl] in term [op]. Unifies [cl] to every subterm of [op] and return all the matches. @@ -906,7 +906,7 @@ let w_unify_to_subterm_all env ?(flags=default_unify_flags) (op,cl) evd = in let res = matchrec cl [] in if res = [] then - raise (PretypeError (env,NoOccurrenceFound (op, None))) + raise (PretypeError (env,evd,NoOccurrenceFound (op, None))) else res @@ -922,7 +922,7 @@ let w_unify_to_subterm_list env flags allow_K hdmeta oplist t evd = try (* This is up to delta for subterms w/o metas ... *) w_unify_to_subterm env ~flags (strip_outer_cast op,t) evd - with PretypeError (env,NoOccurrenceFound _) when allow_K -> (evd,op) + with PretypeError (env,_,NoOccurrenceFound _) when allow_K -> (evd,op) in if not allow_K && (* ensure we found a different instance *) List.exists (fun op -> eq_constr op cl) l @@ -932,7 +932,7 @@ let w_unify_to_subterm_list env flags allow_K hdmeta oplist t evd = (evd,op::l) else (* This is not up to delta ... *) - raise (PretypeError (env,NoOccurrenceFound (op, None)))) + raise (PretypeError (env,evd,NoOccurrenceFound (op, None)))) oplist (evd,[]) @@ -996,13 +996,13 @@ let w_unify allow_K env cv_pb ?(flags=default_unify_flags) ty1 ty2 evd = with ex when precatchable_exception ex -> try w_unify2 env flags allow_K cv_pb ty1 ty2 evd - with PretypeError (env,NoOccurrenceFound _) as e -> raise e) + with PretypeError (env,_,NoOccurrenceFound _) as e -> raise e) (* Second order case *) | (Meta _, true, _, _ | _, _, Meta _, true) -> (try w_unify2 env flags allow_K cv_pb ty1 ty2 evd - with PretypeError (env,NoOccurrenceFound _) as e -> raise e + with PretypeError (env,_,NoOccurrenceFound _) as e -> raise e | ex when precatchable_exception ex -> try w_typed_unify env cv_pb flags ty1 ty2 evd |