From 910612984259c0c032f1292ce4d7ac6f290b8e20 Mon Sep 17 00:00:00 2001 From: ppedrot Date: Sun, 10 Feb 2013 00:37:49 +0000 Subject: Moved code from Pretype_error to Evarutil git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16194 85f007b7-540e-0410-9357-904b9bb8a0f7 --- pretyping/evarutil.ml | 27 ++++++++++++++++++++++----- pretyping/evarutil.mli | 8 ++++++++ pretyping/pretype_errors.ml | 23 ----------------------- pretyping/pretype_errors.mli | 14 -------------- pretyping/typing.ml | 4 ++-- 5 files changed, 32 insertions(+), 44 deletions(-) (limited to 'pretyping') 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 -- cgit v1.2.3