Making Evarutil independent from Reductionops.

Author: ppedrot

dev/printers.mllib

@@ -123,14 +123,15 @@ Evd
 Sigma
 Glob_ops
 Redops
+Pretype_errors
+Evarutil
 Reductionops
 Inductiveops
 Arguments_renaming
 Nativenorm
 Retyping
 Cbv
-Pretype_errors
-Evarutil
+
 Evardefine
 Evarsolve
 Recordops

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

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

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;

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 :

pretyping/pretyping.mllib

@@ -1,14 +1,14 @@
 Locusops
+Pretype_errors
+Evarutil
 Reductionops
 Inductiveops
 Vnorm
 Arguments_renaming
 Nativenorm
 Retyping
 Cbv
-Pretype_errors
 Find_subterm
-Evarutil
 Evardefine
 Evarsolve
 Recordops

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

tactics/hints.ml

@@ -1072,7 +1072,7 @@ let prepare_hint check (poly,local) env init (sigma,c) =
       subst := (evar,mkVar id)::!subst;
       mkNamedLambda id t (iter (replace_term evar (mkVar id) c)) in
   let c' = iter c in
-    if check then Evarutil.check_evars (Global.env()) Evd.empty sigma c';
+    if check then Pretyping.check_evars (Global.env()) Evd.empty sigma c';
     let diff = Univ.ContextSet.diff (Evd.universe_context_set sigma) (Evd.universe_context_set init) in
     if poly then IsConstr (c', diff)
     else if local then IsConstr (c', diff)

tactics/rewrite.ml

@@ -1880,7 +1880,7 @@ let build_morphism_signature m =
   let morph = e_app_poly env evd PropGlobal.proper_type [| t; sig_; m |] in
   let evd = solve_constraints env !evd in
   let m = Evarutil.nf_evar evd morph in
-    Evarutil.check_evars env Evd.empty evd m; m
+    Pretyping.check_evars env Evd.empty evd m; m
 
 let default_morphism sign m =
   let env = Global.env () in

toplevel/classes.ml

@@ -191,7 +191,7 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro
 	  let t = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in
 	    nf t
 	in
-	Evarutil.check_evars env Evd.empty !evars termtype;
+	Pretyping.check_evars env Evd.empty !evars termtype;
 	let pl, ctx = Evd.universe_context ?names:pl !evars in
 	let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id
 	  (ParameterEntry 
@@ -287,7 +287,7 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro
       let evm, nf = Evarutil.nf_evar_map_universes !evars in
       let termtype = nf termtype in
       let _ = (* Check that the type is free of evars now. *)
-	Evarutil.check_evars env Evd.empty evm termtype
+	Pretyping.check_evars env Evd.empty evm termtype
       in
       let term = Option.map nf term in
 	if not (Evd.has_undefined evm) && not (Option.is_empty term) then
@@ -361,7 +361,7 @@ let context poly l =
   let _, ((env', fullctx), impls) = interp_context_evars env evars l in
   let subst = Evarutil.evd_comb0 Evarutil.nf_evars_and_universes evars in
   let fullctx = Context.Rel.map subst fullctx in
-  let ce t = Evarutil.check_evars env Evd.empty !evars t in
+  let ce t = Pretyping.check_evars env Evd.empty !evars t in
   let () = List.iter (fun decl -> Context.Rel.Declaration.iter_constr ce decl) fullctx in
   let ctx =
     try named_of_rel_context fullctx

toplevel/himsg.ml

@@ -76,6 +76,15 @@ let rec contract3' env a b c = function
       let y,x = contract3' env a b c x in
       y,CannotSolveConstraint ((pb,env,t,u),x)
 
+(** Ad-hoc reductions *)
+
+let j_nf_betaiotaevar sigma j =
+  { uj_val = Evarutil.nf_evar sigma j.uj_val;
+    uj_type = Reductionops.nf_betaiota sigma j.uj_type }
+
+let jv_nf_betaiotaevar sigma jl =
+  Array.map (j_nf_betaiotaevar sigma) jl
+
 (** Printers *)
 
 let pr_lconstr c = quote (pr_lconstr c)
@@ -322,7 +331,7 @@ let explain_unification_error env sigma p1 p2 = function
 
 let explain_actual_type env sigma j t reason =
   let env = make_all_name_different env in
-  let j = Evarutil.j_nf_betaiotaevar sigma j in
+  let j = j_nf_betaiotaevar sigma j in
   let t = Reductionops.nf_betaiota sigma t in
   (** Actually print *)
   let pe = pr_ne_context_of (str "In environment") env sigma in
@@ -337,7 +346,7 @@ let explain_actual_type env sigma j t reason =
   ppreason ++ str ".")
 
 let explain_cant_apply_bad_type env sigma (n,exptyp,actualtyp) rator randl =
-  let randl = Evarutil.jv_nf_betaiotaevar sigma randl in
+  let randl = jv_nf_betaiotaevar sigma randl in
   let exptyp = Evarutil.nf_evar sigma exptyp in
   let actualtyp = Reductionops.nf_betaiota sigma actualtyp in
   let rator = Evarutil.j_nf_evar sigma rator in

toplevel/record.ml

@@ -156,7 +156,7 @@ let typecheck_params_and_fields def id pl t ps nots fs =
   let evars, nf = Evarutil.nf_evars_and_universes evars in
   let newps = Context.Rel.map nf newps in
   let newfs = Context.Rel.map nf newfs in
-  let ce t = Evarutil.check_evars env0 Evd.empty evars t in
+  let ce t = Pretyping.check_evars env0 Evd.empty evars t in
     List.iter (iter_constr ce) (List.rev newps);
     List.iter (iter_constr ce) (List.rev newfs);
     Evd.universe_context ?names:pl evars, nf arity, template, imps, newps, impls, newfs