diff options
Diffstat (limited to 'pretyping/pretype_errors.ml')
| -rw-r--r-- | pretyping/pretype_errors.ml | 59 |
1 files changed, 32 insertions, 27 deletions
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index 2d52ad5fd..fd42ca0ba 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -12,10 +12,11 @@ open Util open Names open Sign open Term +open Termops open Environ open Type_errors open Rawterm -open Inductive +open Inductiveops type ml_case_error = | MlCaseAbsurd @@ -35,14 +36,7 @@ type pretype_error = exception PretypeError of env * pretype_error -(* 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 nf_evar sigma = Reduction.local_strong (whd_evar sigma) +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 } @@ -52,13 +46,22 @@ let tj_nf_evar sigma {utj_val=v;utj_type=t} = {utj_val=type_app (nf_evar sigma) v;utj_type=t} let env_ise sigma env = - map_context (nf_evar sigma) env + let sign = named_context 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_app (nf_evar sigma) b, nf_evar sigma ty) + e) + ctxt + env0 (* This simplify 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 env (na,c,t) = + let contract_context (na,c,t) env = match c with | Some c' when isRel c' -> l := (substl !l c') :: !l; @@ -81,50 +84,52 @@ let contract3 env a b c = match contract env [a;b;c] with 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 raise_located_type_error (loc,ctx,sigma,te) = + Stdpp.raise_with_loc loc (TypeError(env_ise sigma ctx,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, CCI, env, sigma, - ActualType (c,nf_evar sigma actty, nf_evar sigma expty)) + (loc, env, sigma, ActualType (j, nf_evar sigma 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, CCI, env, sigma, - CantApplyNonFunctional (j_nf_evar sigma rator, jl_nf_evar sigma randl)) + (loc, env, sigma, + CantApplyNonFunctional (j_nf_evar sigma rator, ja)) let error_cant_apply_bad_type_loc loc env sigma (n,c,t) rator randl = + let ja = Array.of_list (jl_nf_evar sigma randl) in raise_located_type_error - (loc, CCI, env, sigma, + (loc, env, sigma, CantApplyBadType ((n,nf_evar sigma c, nf_evar sigma t), - j_nf_evar sigma rator, jl_nf_evar sigma randl)) + j_nf_evar sigma rator, ja)) 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_loc loc k env sigma c i actty expty = +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, k, env, sigma, + (loc, env, sigma, IllFormedBranch (nf_evar sigma c,i,simp actty, simp expty)) -let error_number_branches_loc loc k env sigma cj expn = +let error_number_branches_loc loc env sigma cj expn = raise_located_type_error - (loc, k, env, sigma, + (loc, env, sigma, NumberBranches (j_nf_evar sigma cj, expn)) -let error_case_not_inductive_loc loc k env sigma cj = +let error_case_not_inductive_loc loc env sigma cj = raise_located_type_error - (loc, k, env, sigma, CaseNotInductive (j_nf_evar sigma cj)) + (loc, env, sigma, CaseNotInductive (j_nf_evar sigma cj)) -let error_ill_typed_rec_body_loc loc k env sigma i na jl tys = +let error_ill_typed_rec_body_loc loc env sigma i na jl tys = raise_located_type_error - (loc, k, env, sigma, + (loc, env, sigma, IllTypedRecBody (i,na,jv_nf_evar sigma jl, Array.map (nf_evar sigma) tys)) |