diff options
Diffstat (limited to 'pretyping/pretype_errors.ml')
| -rw-r--r-- | pretyping/pretype_errors.ml | 115 |
1 files changed, 81 insertions, 34 deletions
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index f35b1b10b6..4d6af242be 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -14,6 +14,7 @@ open Term open Environ open Type_errors open Rawterm +open Inductive type ml_case_error = | MlCaseAbsurd @@ -21,7 +22,7 @@ type ml_case_error = type pretype_error = (* Old Case *) - | MlCase of ml_case_error + | MlCase of ml_case_error * inductive_type * unsafe_judgment | CantFindCaseType of constr (* Unification *) | OccurCheck of int * constr @@ -33,58 +34,104 @@ type pretype_error = exception PretypeError of env * pretype_error -let raise_pretype_error (loc,ctx,te) = - Stdpp.raise_with_loc loc (PretypeError(ctx,te)) +(* Replacing defined evars for error messages *) +let rec whd_evar sigma c = + match kind_of_term c with + | IsEvar (ev,args) when Evd.in_dom sigma ev & Evd.is_defined sigma ev -> + whd_evar sigma (Instantiate.existential_value sigma (ev,args)) + | _ -> collapse_appl c -let raise_located_type_error (loc,k,ctx,te) = - Stdpp.raise_with_loc loc (TypeError(k,ctx,te)) +let nf_evar sigma = Reduction.local_strong (whd_evar sigma) +let j_nf_evar sigma j = + { uj_val = nf_evar sigma j.uj_val; + uj_type = nf_evar sigma j.uj_type } +let jl_nf_evar sigma jl = List.map (j_nf_evar 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=type_app (nf_evar sigma) v;utj_type=t} -let error_cant_find_case_type_loc loc env expr = - raise_pretype_error (loc, env, CantFindCaseType expr) -let error_ill_formed_branch_loc loc k env c i actty expty = - raise_located_type_error (loc, k, env, IllFormedBranch (c,i,actty,expty)) +let env_ise sigma env = + map_context (nf_evar sigma) env -let error_actual_type_loc loc env c actty expty = - raise_located_type_error (loc, CCI, env, ActualType (c,actty,expty)) -let error_cant_apply_not_functional_loc loc env rator randl = +let raise_pretype_error (loc,ctx,sigma,te) = + Stdpp.raise_with_loc loc (PretypeError(env_ise sigma ctx,te)) + +let raise_located_type_error (loc,k,ctx,sigma,te) = + Stdpp.raise_with_loc loc (TypeError(k,env_ise sigma ctx,te)) + + +let error_actual_type_loc loc env sigma {uj_val=c;uj_type=actty} expty = + raise_located_type_error + (loc, CCI, env, sigma, + ActualType (c,nf_evar sigma actty, nf_evar sigma expty)) + +let error_cant_apply_not_functional_loc loc env sigma rator randl = + raise_located_type_error + (loc, CCI, env, sigma, + CantApplyNonFunctional (j_nf_evar sigma rator, jl_nf_evar sigma randl)) + +let error_cant_apply_bad_type_loc loc env sigma (n,c,t) rator randl = raise_located_type_error - (loc,CCI,env, CantApplyNonFunctional (rator,randl)) + (loc, CCI, env, sigma, + CantApplyBadType + ((n,nf_evar sigma c, nf_evar sigma t), + j_nf_evar sigma rator, jl_nf_evar sigma randl)) -let error_cant_apply_bad_type_loc loc env t rator randl = - raise_located_type_error (loc, CCI, env, CantApplyBadType (t,rator,randl)) +let error_cant_find_case_type_loc loc env sigma expr = + raise_pretype_error + (loc, env, sigma, CantFindCaseType (nf_evar sigma expr)) -let error_ill_formed_branch k env c i actty expty = - raise (TypeError (k, env, IllFormedBranch (c,i,actty,expty))) +let error_ill_formed_branch_loc loc k env sigma c i actty expty = + let simp t = Reduction.nf_betaiota (nf_evar sigma t) in + raise_located_type_error + (loc, k, env, sigma, + IllFormedBranch (nf_evar sigma c,i,simp actty, simp expty)) -let error_number_branches_loc loc k env c ct expn = - raise_located_type_error (loc, k, env, NumberBranches (c,ct,expn)) +let error_number_branches_loc loc k env sigma cj expn = + raise_located_type_error + (loc, k, env, sigma, + NumberBranches (j_nf_evar sigma cj, expn)) -let error_case_not_inductive_loc loc k env c ct = - raise_located_type_error (loc, k, env, CaseNotInductive (c,ct)) +let error_case_not_inductive_loc loc k env sigma cj = + raise_located_type_error + (loc, k, env, sigma, CaseNotInductive (j_nf_evar sigma cj)) +let error_ill_typed_rec_body_loc loc k env sigma i na jl tys = + raise_located_type_error + (loc, k, env, sigma, + IllTypedRecBody (i,na,jv_nf_evar sigma jl, + Array.map (nf_evar sigma) tys)) -(*s Implicit arguments synthesis errors *) +(*s Implicit arguments synthesis errors. It is hard to find + a precise location. *) -let error_occur_check env ev c = - raise (PretypeError (env, OccurCheck (ev,c))) +let error_occur_check env sigma ev c = + let c = nf_evar sigma c in + raise (PretypeError (env_ise sigma env, OccurCheck (ev,c))) -let error_not_clean env ev c = - raise (PretypeError (env, NotClean (ev,c))) +let error_not_clean env sigma ev c = + let c = nf_evar sigma c in + raise (PretypeError (env_ise sigma env, NotClean (ev,c))) (*s Ml Case errors *) -let error_ml_case_loc loc env mes = - raise_pretype_error (loc, env, MlCase mes) +let error_ml_case_loc loc env sigma mes indt j = + raise_pretype_error + (loc, env, sigma, MlCase (mes, indt, j_nf_evar sigma j)) (*s Pretyping errors *) -let error_var_not_found_loc loc s = - raise_pretype_error (loc, Global.env() (*bidon*), VarNotFound s) +let error_unexpected_type_loc loc env sigma actty expty = + raise_pretype_error + (loc, env, sigma, + UnexpectedType (nf_evar sigma actty, nf_evar sigma expty)) + +let error_not_product_loc loc env sigma c = + raise_pretype_error (loc, env, sigma, NotProduct (nf_evar sigma c)) -let error_unexpected_type_loc loc env actty expty = - raise_pretype_error (loc, env, UnexpectedType (actty, expty)) +(*s Error in conversion from AST to rawterms *) -let error_not_product_loc loc env c = - raise_pretype_error (loc, env, NotProduct c) +let error_var_not_found_loc loc s = + raise_pretype_error (loc, empty_env, Evd.empty, VarNotFound s) |