Making Evarutil independent from Reductionops.

6 files changed, 62 insertions, 63 deletions

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 35b66918c..2bd67dcdc 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -17,9 +17,12 @@ open Namegen
 open Pre_env
 open Environ
 open Evd
-open Pretype_errors
 open Sigma.Notations
 
+let safe_evar_value sigma ev =
+  try Some (Evd.existential_value sigma ev)
+  with NotInstantiatedEvar | Not_found -> None
+
 (** Combinators *)
 
 let evd_comb0 f evdref =
@@ -61,22 +64,41 @@ let rec flush_and_check_evars sigma c =
 
 (* let nf_evar_key = Profile.declare_profile "nf_evar"  *)
 (* let nf_evar = Profile.profile2 nf_evar_key Reductionops.nf_evar *)
-let nf_evar = Reductionops.nf_evar
+
+let rec whd_evar sigma c =
+  match kind_of_term c with
+    | Evar ev ->
+        let (evk, args) = ev in
+        let args = Array.map (fun c -> whd_evar sigma c) args in
+        (match safe_evar_value sigma (evk, args) with
+            Some c -> whd_evar sigma c
+          | None -> c)
+    | Sort (Type u) -> 
+      let u' = Evd.normalize_universe sigma u in
+	if u' == u then c else mkSort (Sorts.sort_of_univ u')
+    | Const (c', u) when not (Univ.Instance.is_empty u) -> 
+      let u' = Evd.normalize_universe_instance sigma u in
+	if u' == u then c else mkConstU (c', u')
+    | Ind (i, u) when not (Univ.Instance.is_empty u) -> 
+      let u' = Evd.normalize_universe_instance sigma u in
+	if u' == u then c else mkIndU (i, u')
+    | Construct (co, u) when not (Univ.Instance.is_empty u) ->
+      let u' = Evd.normalize_universe_instance sigma u in
+	if u' == u then c else mkConstructU (co, u')
+    | _ -> c
+
+let rec nf_evar sigma t = Constr.map (fun t -> nf_evar sigma t) (whd_evar sigma t)
+
 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 nf_evars_universes evm =
-  Universes.nf_evars_and_universes_opt_subst (Reductionops.safe_evar_value evm) 
+  Universes.nf_evars_and_universes_opt_subst (safe_evar_value evm) 
     (Evd.universe_subst evm)
     
 let nf_evars_and_universes evm =
@@ -469,7 +491,7 @@ let rec check_and_clear_in_constr env evdref err ids c =
       | Evar (evk,l as ev) ->
 	  if Evd.is_defined !evdref evk then
 	    (* If evk is already defined we replace it by its definition *)
-	    let nc = Reductionops.whd_evar !evdref c in
+	    let nc = whd_evar !evdref c in
 	      (check_and_clear_in_constr env evdref err ids nc)
 	  else
 	    (* We check for dependencies to elements of ids in the
@@ -524,7 +546,7 @@ let rec check_and_clear_in_constr env evdref err ids c =
 	      let evi' = { evi with evar_extra = extra' } in
 	      evdref := Evd.add !evdref evk evi' ;
 	    (* spiwack: /hacking session *)
-              Reductionops.whd_evar !evdref c
+              whd_evar !evdref c
 
       | _ -> map_constr (check_and_clear_in_constr env evdref err ids) c
 
@@ -647,23 +669,6 @@ let undefined_evars_of_evar_info evd evi =
        (undefined_evars_of_named_context evd
 	  (named_context_of_val evi.evar_hyps)))
 
-(* [check_evars] fails if some unresolved evar remains *)
-
-let check_evars env initial_sigma sigma c =
-  let rec proc_rec c =
-    match kind_of_term c with
-    | Evar (evk,_ as ev) ->
-        (match existential_opt_value sigma ev with
-        | Some c -> proc_rec c
-        | None ->
-	  if not (Evd.mem initial_sigma evk) then
-            let (loc,k) = evar_source evk sigma in
-	      match k with
-	      | Evar_kinds.ImplicitArg (gr, (i, id), false) -> ()
-	      | _ -> error_unsolvable_implicit loc env sigma evk None)
-      | _ -> iter_constr proc_rec c
-  in proc_rec c
-
 (* spiwack: this is a more complete version of
    {!Termops.occur_evar}. The latter does not look recursively into an
    [evar_map]. If unification only need to check superficially, tactics
@@ -692,7 +697,7 @@ let subterm_source evk (loc,k) =
 
 (** Term exploration up to instantiation. *)
 let kind_of_term_upto sigma t =
-  Constr.kind (Reductionops.whd_evar sigma t)
+  Constr.kind (whd_evar sigma t)
 
 (** [eq_constr_univs_test sigma1 sigma2 t u] tests equality of [t] and
     [u] up to existential variable instantiation and equalisable
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index a4f852765..ffff2c5dd 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -78,6 +78,8 @@ val new_evar_instance :
 
 val make_pure_subst : evar_info -> constr array -> (Id.t * constr) list
 
+val safe_evar_value : evar_map -> existential -> constr option
+
 (** {6 Evars/Metas switching...} *)
 
 val non_instantiated : evar_map -> evar_info Evar.Map.t
@@ -96,9 +98,6 @@ val has_undefined_evars : evar_map -> constr -> bool
 
 val is_ground_term :  evar_map -> constr -> bool
 val is_ground_env  :  evar_map -> env -> bool
-(** [check_evars env initial_sigma extended_sigma c] fails if some
-   new unresolved evar remains in [c] *)
-val check_evars : env -> evar_map -> evar_map -> constr -> unit
 
 (** [gather_dependent_evars evm seeds] classifies the evars in [evm]
     as dependent_evars and goals (these may overlap). A goal is an
@@ -134,6 +133,7 @@ val judge_of_new_Type : 'r Sigma.t -> (unsafe_judgment, 'r) Sigma.sigma
 (** [flush_and_check_evars] raise [Uninstantiated_evar] if an evar remains
     uninstantiated; [nf_evar] leaves uninstantiated evars as is *)
 
+val whd_evar :  evar_map -> constr -> constr
 val nf_evar :  evar_map -> constr -> constr
 val j_nf_evar :  evar_map -> unsafe_judgment -> unsafe_judgment
 val jl_nf_evar :
@@ -151,9 +151,6 @@ 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 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 *)
 
 val nf_evars_universes : evar_map -> constr -> constr
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 30e26c6f8..a765d3091 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -235,6 +235,23 @@ let check_extra_evars_are_solved env current_sigma pending =
 	| _ ->
 	    error_unsolvable_implicit loc env current_sigma evk None) pending
 
+(* [check_evars] fails if some unresolved evar remains *)
+
+let check_evars env initial_sigma sigma c =
+  let rec proc_rec c =
+    match kind_of_term c with
+    | Evar (evk,_ as ev) ->
+        (match existential_opt_value sigma ev with
+        | Some c -> proc_rec c
+        | None ->
+	  if not (Evd.mem initial_sigma evk) then
+            let (loc,k) = evar_source evk sigma in
+	      match k with
+	      | Evar_kinds.ImplicitArg (gr, (i, id), false) -> ()
+	      | _ -> Pretype_errors.error_unsolvable_implicit loc env sigma evk None)
+      | _ -> Constr.iter proc_rec c
+  in proc_rec c
+
 let check_evars_are_solved env current_sigma frozen pending =
   check_typeclasses_instances_are_solved env current_sigma frozen;
   check_problems_are_solved env current_sigma;
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 40745ed09..4c4c535d8 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -130,6 +130,10 @@ val solve_remaining_evars : inference_flags ->
 val check_evars_are_solved :
   env -> (* current map: *) evar_map -> (* map to check: *) pending -> unit
 
+(** [check_evars env initial_sigma extended_sigma c] fails if some
+   new unresolved evar remains in [c] *)
+val check_evars : env -> evar_map -> evar_map -> constr -> unit
+
 (**/**)
 (** Internal of Pretyping... *)
 val pretype :
diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib
index e8c0bbbf9..be517d1aa 100644
--- a/pretyping/pretyping.mllib
+++ b/pretyping/pretyping.mllib
@@ -1,4 +1,6 @@
 Locusops
+Pretype_errors
+Evarutil
 Reductionops
 Inductiveops
 Vnorm
@@ -6,9 +8,7 @@ Arguments_renaming
 Nativenorm
 Retyping
 Cbv
-Pretype_errors
 Find_subterm
-Evarutil
 Evardefine
 Evarsolve
 Recordops
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 935e18d8d..7f4249c5b 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -594,9 +594,7 @@ let pr_state (tm,sk) =
 (*** Reduction Functions Operators ***)
 (*************************************)
 
-let safe_evar_value sigma ev =
-  try Some (Evd.existential_value sigma ev)
-  with NotInstantiatedEvar | Not_found -> None
+let safe_evar_value = Evarutil.safe_evar_value
 
 let safe_meta_value sigma ev =
   try Some (Evd.meta_value sigma ev)
@@ -1183,30 +1181,8 @@ let whd_zeta c = Stack.zip (local_whd_state_gen zeta Evd.empty (c,Stack.empty))
 (****************************************************************************)
 
 (* Replacing defined evars for error messages *)
-let rec whd_evar sigma c =
-  match kind_of_term c with
-    | Evar ev ->
-        let (evk, args) = ev in
-        let args = Array.map (fun c -> whd_evar sigma c) args in
-        (match safe_evar_value sigma (evk, args) with
-            Some c -> whd_evar sigma c
-          | None -> c)
-    | Sort (Type u) -> 
-      let u' = Evd.normalize_universe sigma u in
-	if u' == u then c else mkSort (Sorts.sort_of_univ u')
-    | Const (c', u) when not (Univ.Instance.is_empty u) -> 
-      let u' = Evd.normalize_universe_instance sigma u in
-	if u' == u then c else mkConstU (c', u')
-    | Ind (i, u) when not (Univ.Instance.is_empty u) -> 
-      let u' = Evd.normalize_universe_instance sigma u in
-	if u' == u then c else mkIndU (i, u')
-    | Construct (co, u) when not (Univ.Instance.is_empty u) ->
-      let u' = Evd.normalize_universe_instance sigma u in
-	if u' == u then c else mkConstructU (co, u')
-    | _ -> c
-
-let nf_evar =
-  local_strong whd_evar
+let whd_evar = Evarutil.whd_evar
+let nf_evar = Evarutil.nf_evar
 
 (* lazy reduction functions. The infos must be created for each term *)
 (* Note by HH [oct 08] : why would it be the job of clos_norm_flags to add