diff options
| -rw-r--r-- | pretyping/coercion.ml | 17 | ||||
| -rw-r--r-- | pretyping/coercion.mli | 7 | ||||
| -rw-r--r-- | pretyping/pretype_errors.ml | 12 | ||||
| -rw-r--r-- | pretyping/pretype_errors.mli | 10 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 4 |
5 files changed, 37 insertions, 13 deletions
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index c98eeab16..6141d3025 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -8,7 +8,7 @@ open Term open Reduction open Environ open Typeops -open Type_errors +open Pretype_errors open Classops open Recordops open Evarconv @@ -136,7 +136,10 @@ let rec inh_conv_coerce_to env isevars c1 hj = else (* let ju1 = exemeta_rec def_vty_con env isevars u1 in let assu1 = assumption_of_judgement env !isevars ju1 in *) - let assu1 = outcast_type u1 in + let assu1 = + if not (isCast u1) then + make_typed u1 (get_sort_of env !isevars u1) + else outcast_type u1 in let name = (match name with | Anonymous -> Name (id_of_string "x") | _ -> name) in @@ -153,20 +156,20 @@ let rec inh_conv_coerce_to env isevars c1 hj = fst (abs_rel env !isevars name assu1 h2) | _ -> failwith "inh_coerce_to") -let inh_cast_rel env isevars cj tj = +let inh_cast_rel loc env isevars cj tj = let cj' = try inh_conv_coerce_to env isevars tj.uj_val cj with Not_found | Failure _ -> let rcj = j_nf_ise env !isevars cj in let atj = j_nf_ise env !isevars tj in - error_actual_type CCI env rcj.uj_val rcj.uj_type atj.uj_type + error_actual_type_loc loc env rcj.uj_val rcj.uj_type atj.uj_type in { uj_val = mkCast cj'.uj_val tj.uj_val; uj_type = tj.uj_val; uj_kind = whd_betadeltaiota env !isevars tj.uj_type } -let inh_apply_rel_list nocheck env isevars argjl funj vtcon = +let inh_apply_rel_list nocheck apploc env isevars argjl funj vtcon = let rec apply_rec n acc typ = function | [] -> let resj = @@ -190,13 +193,13 @@ let inh_apply_rel_list nocheck env isevars argjl funj vtcon = (try inh_conv_coerce_to env isevars c1 hj with Failure _ | Not_found -> - error_cant_apply_bad_type CCI env (n,c1,hj.uj_type) + error_cant_apply_bad_type_loc apploc env (n,c1,hj.uj_type) (j_nf_ise env !isevars funj) (jl_nf_ise env !isevars argjl)) in apply_rec (n+1) (hj'::acc) (subst1 hj'.uj_val c2) restjl | _ -> - error_cant_apply_not_functional CCI env + error_cant_apply_not_functional_loc apploc env (j_nf_ise env !isevars funj) (jl_nf_ise env !isevars argjl) in apply_rec 1 [] funj.uj_type argjl diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli index 060ac6ce2..cb892ed7c 100644 --- a/pretyping/coercion.mli +++ b/pretyping/coercion.mli @@ -23,9 +23,10 @@ val inh_coerce_to : env -> 'a evar_defs -> constr -> unsafe_judgment -> unsafe_judgment val inh_conv_coerce_to : env -> 'a evar_defs -> constr -> unsafe_judgment -> unsafe_judgment -val inh_cast_rel : + +val inh_cast_rel : Rawterm.loc -> env -> 'a evar_defs -> unsafe_judgment -> unsafe_judgment -> unsafe_judgment -val inh_apply_rel_list : bool -> env -> 'a evar_defs -> - unsafe_judgment list -> unsafe_judgment -> 'b * ('c * constr option) +val inh_apply_rel_list : bool -> Rawterm.loc -> env -> 'a evar_defs -> + unsafe_judgment list -> unsafe_judgment -> trad_constraint -> unsafe_judgment diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index 4067d0064..74f4c5748 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -14,7 +14,17 @@ let error_var_not_found_loc loc k s = raise_pretype_error (loc,k, Global.context() (*bidon*), VarNotFound s) let error_cant_find_case_type_loc loc env expr = - raise_pretype_error (loc,CCI,context env,CantFindCaseType expr) + raise_pretype_error (loc, CCI, context env, CantFindCaseType expr) + +let error_actual_type_loc loc env c actty expty = + raise_pretype_error (loc, CCI, context env, ActualType (c,actty,expty)) + +let error_cant_apply_not_functional_loc loc env rator randl = + raise_pretype_error + (loc,CCI,context env, CantApplyNonFunctional (rator,randl)) + +let error_cant_apply_bad_type_loc loc env t rator randl = + raise_pretype_error (loc, CCI, context env, CantApplyBadType (t,rator,randl)) let error_ill_formed_branch k env c i actty expty = raise (TypeError (k, context env, IllFormedBranch (c,i,actty,expty))) diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli index 9944f55a8..852232897 100644 --- a/pretyping/pretype_errors.mli +++ b/pretyping/pretype_errors.mli @@ -22,6 +22,16 @@ val error_cant_find_case_type_loc : val error_ill_formed_branch_loc : loc -> path_kind -> env -> constr -> int -> constr -> constr -> 'b +val error_actual_type_loc : + loc -> env -> constr -> constr -> constr -> 'b + +val error_cant_apply_not_functional_loc : + loc -> env -> unsafe_judgment -> unsafe_judgment list -> 'b + +val error_cant_apply_bad_type_loc : + loc -> env -> int * constr * constr -> + unsafe_judgment -> unsafe_judgment list -> 'b + val error_number_branches_loc : loc -> path_kind -> env -> constr -> constr -> int -> 'b diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 2493ae7a0..72eed91c5 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -352,7 +352,7 @@ match cstr with (* Où teste-t-on que le résultat doit satisfaire tycon ? *) (rtc,cj::jl) in let jl = List.rev (snd (List.fold_left apply_one_arg (mk_tycon j.uj_type,[]) args)) in - inh_apply_rel_list !trad_nocheck env isevars jl j vtcon + inh_apply_rel_list !trad_nocheck loc env isevars jl j vtcon | RBinder(loc,BLambda,name,c1,c2) -> let j = @@ -450,7 +450,7 @@ match cstr with (* Où teste-t-on que le résultat doit satisfaire tycon ? *) let cj = pretype (mk_tycon2 vtcon (body_of_type (assumption_of_judgment env !isevars tj))) env isevars lvar lmeta c in - inh_cast_rel env isevars cj tj + inh_cast_rel loc env isevars cj tj (* Maintenant, tout s'exécute... | _ -> error_cant_execute CCI env (nf_ise1 env !isevars cstr) |