diff options
Diffstat (limited to 'pretyping/pretype_errors.ml')
-rw-r--r-- | pretyping/pretype_errors.ml | 113 |
1 files changed, 45 insertions, 68 deletions
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index 688a25b9..2cf16791 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -1,15 +1,13 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: pretype_errors.ml 14641 2011-11-06 11:59:10Z herbelin $ *) - +open Compat open Util -open Stdpp open Names open Sign open Term @@ -17,7 +15,7 @@ open Termops open Namegen open Environ open Type_errors -open Rawterm +open Glob_term open Inductiveops type pretype_error = @@ -40,12 +38,13 @@ 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 _ - | Stdpp.Exc_located(_,(Util.UserError _ | TypeError _ | + | Loc.Exc_located(_,(Util.UserError _ | TypeError _ | Nametab.GlobalizationError _ | PretypeError _)) -> true | _ -> false @@ -57,25 +56,22 @@ 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 sign = named_context_val env in - let ctxt = rel_context env in - let env0 = reset_with_named_context sign env in - Sign.fold_rel_context - (fun (na,b,ty) e -> - push_rel - (na, Option.map (nf_evar sigma) b, nf_evar sigma ty) - e) - ctxt - ~init:env0 - -(* This simplify the typing context of Cases clauses *) +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 @@ -99,111 +95,92 @@ 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) = - Stdpp.raise_with_loc 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) = - Stdpp.raise_with_loc 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 - raise_with_loc 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 = - raise_with_loc loc - (PretypeError (env_ise sigma env, UnsolvableImplicit (evi, e, explain))) + Loc.raise loc + (PretypeError (env, sigma, UnsolvableImplicit (evi, e, explain))) let error_cannot_unify env sigma (m,n) = - 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 *) +(*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) |