diff options
| -rw-r--r-- | pretyping/evarutil.ml | 27 | ||||
| -rw-r--r-- | pretyping/evarutil.mli | 8 | ||||
| -rw-r--r-- | pretyping/pretype_errors.ml | 23 | ||||
| -rw-r--r-- | pretyping/pretype_errors.mli | 14 | ||||
| -rw-r--r-- | pretyping/typing.ml | 4 | ||||
| -rw-r--r-- | toplevel/himsg.ml | 44 |
6 files changed, 54 insertions, 66 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index fcc284832..0c339df4e 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -36,11 +36,28 @@ let rec flush_and_check_evars sigma c = | Some c -> flush_and_check_evars sigma c) | _ -> map_constr (flush_and_check_evars sigma) c -let nf_evar = Pretype_errors.nf_evar -let j_nf_evar = Pretype_errors.j_nf_evar -let jl_nf_evar = Pretype_errors.jl_nf_evar -let jv_nf_evar = Pretype_errors.jv_nf_evar -let tj_nf_evar = Pretype_errors.tj_nf_evar +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 } +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 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_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 let nf_named_context_evar sigma ctx = Sign.map_named_context (Reductionops.nf_evar sigma) ctx diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index 9c6f1ad47..5c32a9a5c 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -184,6 +184,14 @@ val nf_evar_info : evar_map -> evar_info -> evar_info val nf_evar_map : evar_map -> evar_map val nf_evar_map_undefined : evar_map -> evar_map +val env_nf_evar : evar_map -> env -> env +val env_nf_betaiotaevar : evar_map -> env -> env + +val j_nf_betaiotaevar : evar_map -> unsafe_judgment -> unsafe_judgment +val jv_nf_betaiotaevar : + evar_map -> unsafe_judgment array -> unsafe_judgment array +(** Presenting terms without solved evars *) + (** Replacing all evars, possibly raising [Uninstantiated_evar] *) exception Uninstantiated_evar of existential_key val flush_and_check_evars : evar_map -> constr -> constr diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index ad6922dbe..19ccb2375 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -45,29 +45,6 @@ let precatchable_exception = function Nametab.GlobalizationError _ | PretypeError _)) -> true | _ -> false -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 } -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 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_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 = diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli index 558f3d5bb..3a4c6aad5 100644 --- a/pretyping/pretype_errors.mli +++ b/pretyping/pretype_errors.mli @@ -43,20 +43,6 @@ 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 env_nf_evar : Evd.evar_map -> env -> env -val env_nf_betaiotaevar : Evd.evar_map -> env -> env - -val j_nf_betaiotaevar : Evd.evar_map -> unsafe_judgment -> unsafe_judgment -val jv_nf_betaiotaevar : - Evd.evar_map -> unsafe_judgment array -> unsafe_judgment array - (** Raising errors *) val error_actual_type_loc : Loc.t -> env -> Evd.evar_map -> unsafe_judgment -> constr -> 'b diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 0f9100e79..5ae04488f 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -205,12 +205,12 @@ let rec execute env evdref cstr = (* Sort-polymorphism of inductive types *) make_judge f (inductive_type_knowing_parameters env ind - (jv_nf_evar !evdref jl)) + (Evarutil.jv_nf_evar !evdref jl)) | Const cst -> (* Sort-polymorphism of inductive types *) make_judge f (constant_type_knowing_parameters env cst - (jv_nf_evar !evdref jl)) + (Evarutil.jv_nf_evar !evdref jl)) | _ -> execute env evdref f in diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index cfaea3d74..8e6ff1eb7 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -46,7 +46,7 @@ let explain_unbound_var env v = str "No such section variable or assumption: " ++ var ++ str "." let explain_not_type env sigma j = - let j = j_nf_evar sigma j in + let j = Evarutil.j_nf_evar sigma j in let pe = pr_ne_context_of (str "In environment") env in let pc,pt = pr_ljudge_env env j in pe ++ str "The term" ++ brk(1,1) ++ pc ++ spc () ++ @@ -106,7 +106,7 @@ let explain_elim_arity env ind sorts c pj okinds = fnl () ++ msg let explain_case_not_inductive env sigma cj = - let cj = j_nf_evar sigma cj in + let cj = Evarutil.j_nf_evar sigma cj in let env = make_all_name_different env in let pc = pr_lconstr_env env cj.uj_val in let pct = pr_lconstr_env env cj.uj_type in @@ -119,7 +119,7 @@ let explain_case_not_inductive env sigma cj = str "which is not a (co-)inductive type." let explain_number_branches env sigma cj expn = - let cj = j_nf_evar sigma cj in + let cj = Evarutil.j_nf_evar sigma cj in let env = make_all_name_different env in let pc = pr_lconstr_env env cj.uj_val in let pct = pr_lconstr_env env cj.uj_type in @@ -128,8 +128,8 @@ let explain_number_branches env sigma cj expn = str "expects " ++ int expn ++ str " branches." let explain_ill_formed_branch env sigma c ci actty expty = - let simp t = Reduction.nf_betaiota (nf_evar sigma t) in - let c = nf_evar sigma c in + let simp t = Reduction.nf_betaiota (Evarutil.nf_evar sigma t) in + let c = Evarutil.nf_evar sigma c in let env = make_all_name_different env in let pc = pr_lconstr_env env c in let pa = pr_lconstr_env env (simp actty) in @@ -150,7 +150,7 @@ let explain_generalization env (name,var) j = spc () ++ str "which should be Set, Prop or Type." let explain_actual_type env sigma j pt = - let j = j_nf_betaiotaevar sigma j in + let j = Evarutil.j_nf_betaiotaevar sigma j in let pt = Reductionops.nf_betaiota sigma pt in let pe = pr_ne_context_of (str "In environment") env in let (pc,pct) = pr_ljudge_env env j in @@ -161,10 +161,10 @@ let explain_actual_type env sigma j pt = str "while it is expected to have type" ++ brk(1,1) ++ pt ++ str "." let explain_cant_apply_bad_type env sigma (n,exptyp,actualtyp) rator randl = - let randl = jv_nf_betaiotaevar sigma randl in - let exptyp = nf_evar sigma exptyp in + let randl = Evarutil.jv_nf_betaiotaevar sigma randl in + let exptyp = Evarutil.nf_evar sigma exptyp in let actualtyp = Reductionops.nf_betaiota sigma actualtyp in - let rator = j_nf_evar sigma rator in + let rator = Evarutil.j_nf_evar sigma rator in let env = make_all_name_different env in let nargs = Array.length randl in (* let pe = pr_ne_context_of (str "in environment") env in*) @@ -187,8 +187,8 @@ let explain_cant_apply_bad_type env sigma (n,exptyp,actualtyp) rator randl = pr_lconstr_env env exptyp ++ str "." let explain_cant_apply_not_functional env sigma rator randl = - let randl = jv_nf_evar sigma randl in - let rator = j_nf_evar sigma rator in + let randl = Evarutil.jv_nf_evar sigma randl in + let rator = Evarutil.j_nf_evar sigma rator in let env = make_all_name_different env in let nargs = Array.length randl in (* let pe = pr_ne_context_of (str "in environment") env in*) @@ -208,15 +208,15 @@ let explain_cant_apply_not_functional env sigma rator randl = str " " ++ v 0 appl let explain_unexpected_type env sigma actual_type expected_type = - let actual_type = nf_evar sigma actual_type in - let expected_type = nf_evar sigma expected_type in + let actual_type = Evarutil.nf_evar sigma actual_type in + let expected_type = Evarutil.nf_evar sigma expected_type in let pract = pr_lconstr_env env actual_type in let prexp = pr_lconstr_env env expected_type in str "Found type" ++ spc () ++ pract ++ spc () ++ str "where" ++ spc () ++ prexp ++ str " was expected." let explain_not_product env sigma c = - let c = nf_evar sigma c in + let c = Evarutil.nf_evar sigma c in let pr = pr_lconstr_env env c in str "The type of this term is a product" ++ spc () ++ str "while it is expected to be" ++ @@ -306,8 +306,8 @@ let explain_ill_formed_rec_body env err names i fixenv vdefj = with _ -> mt ()) let explain_ill_typed_rec_body env sigma i names vdefj vargs = - let vdefj = jv_nf_evar sigma vdefj in - let vargs = Array.map (nf_evar sigma) vargs in + let vdefj = Evarutil.jv_nf_evar sigma vdefj in + let vargs = Array.map (Evarutil.nf_evar sigma) vargs in let env = make_all_name_different env in let pvd,pvdt = pr_ljudge_env env (vdefj.(i)) in let pv = pr_lconstr_env env vargs.(i) in @@ -318,13 +318,13 @@ let explain_ill_typed_rec_body env sigma i names vdefj vargs = str "while it should be" ++ spc () ++ pv ++ str "." let explain_cant_find_case_type env sigma c = - let c = nf_evar sigma c in + let c = Evarutil.nf_evar sigma c in let env = make_all_name_different env in let pe = pr_lconstr_env env c in str "Cannot infer type of pattern-matching on" ++ ws 1 ++ pe ++ str "." let explain_occur_check env sigma ev rhs = - let rhs = nf_evar sigma rhs in + let rhs = Evarutil.nf_evar sigma rhs in let env = make_all_name_different env in let id = Evd.string_of_existential ev in let pt = pr_lconstr_env env rhs in @@ -369,7 +369,7 @@ let explain_evar_kind env evi = function assert false let explain_not_clean env sigma ev t k = - let t = nf_evar sigma t in + let t = Evarutil.nf_evar sigma t in let env = make_all_name_different env in let id = Evd.string_of_existential ev in let var = pr_lconstr_env env t in @@ -414,8 +414,8 @@ let explain_wrong_case_info env ind ci = spc () ++ pc ++ str "." let explain_cannot_unify env sigma m n = - let m = nf_evar sigma m in - let n = nf_evar sigma n in + let m = Evarutil.nf_evar sigma m in + let n = Evarutil.nf_evar sigma n in let pm = pr_lconstr_env env m in let pn = pr_lconstr_env env n in str "Impossible to unify" ++ brk(1,1) ++ pm ++ spc () ++ @@ -507,7 +507,7 @@ let explain_type_error env sigma err = explain_wrong_case_info env ind ci let explain_pretype_error env sigma err = - let env = env_nf_betaiotaevar sigma env in + let env = Evarutil.env_nf_betaiotaevar sigma env in let env = make_all_name_different env in match err with | CantFindCaseType c -> explain_cant_find_case_type env sigma c |