Merge PR #7375: Implement to_constr with nf_evars_and_universes_opt_subst

2 files changed, 37 insertions, 53 deletions

diff --git a/engine/evd.ml b/engine/evd.ml
index 6dcec2760..af22de5cd 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -1290,30 +1290,14 @@ module MiniEConstr = struct
   let unsafe_eq = Refl
 
   let to_constr ?(abort_on_undefined_evars=true) sigma c =
-    let rec to_constr c = match Constr.kind c with
-      | Evar ev ->
-        begin match safe_evar_value sigma ev with
-          | Some c -> to_constr c
-          | None ->
-            if abort_on_undefined_evars then
-              anomaly ~label:"econstr" Pp.(str "grounding a non evar-free term")
-            else
-              Constr.map (fun c -> to_constr c) c
-        end
-      | Sort (Sorts.Type u) ->
-        let u' = 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' = 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' = 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' = normalize_universe_instance sigma u in
-        if u' == u then c else mkConstructU (co, u')
-      | _ -> Constr.map (fun c -> to_constr c) c
-    in to_constr c
+    let evar_value =
+      if not abort_on_undefined_evars then fun ev -> safe_evar_value sigma ev
+      else fun ev ->
+        match safe_evar_value sigma ev with
+        | Some _ as v -> v
+        | None -> anomaly ~label:"econstr" Pp.(str "grounding a non evar-free term")
+    in
+    Universes.nf_evars_and_universes_opt_subst evar_value (universe_subst sigma) c
 
   let of_named_decl d = d
   let unsafe_to_named_decl d = d
diff --git a/engine/universes.ml b/engine/universes.ml
index e98708724..0410d1aea 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -592,35 +592,6 @@ let subst_univs_constr =
       CProfile.profile2 subst_univs_constr_key subst_univs_constr
   else subst_univs_constr
 
-let subst_univs_fn_puniverses lsubst (c, u as cu) =
-  let u' = Instance.subst_fn lsubst u in
-    if u' == u then cu else (c, u')
-
-let nf_evars_and_universes_opt_subst f subst =
-  let subst = fun l -> match LMap.find l subst with None -> raise Not_found | Some l' -> l' in
-  let lsubst = level_subst_of subst in
-  let rec aux c =
-    match kind c with
-    | Evar (evk, args) ->
-      let args = Array.map aux args in
-      (match try f (evk, args) with Not_found -> None with
-      | None -> c
-      | Some c -> aux c)
-    | Const pu -> 
-      let pu' = subst_univs_fn_puniverses lsubst pu in
-	if pu' == pu then c else mkConstU pu'
-    | Ind pu ->
-      let pu' = subst_univs_fn_puniverses lsubst pu in
-	if pu' == pu then c else mkIndU pu'
-    | Construct pu ->
-      let pu' = subst_univs_fn_puniverses lsubst pu in
-	if pu' == pu then c else mkConstructU pu'
-    | Sort (Type u) ->
-      let u' = Univ.subst_univs_universe subst u in
-	if u' == u then c else mkSort (sort_of_univ u')
-    | _ -> Constr.map aux c
-  in aux
-
 let fresh_universe_context_set_instance ctx =
   if ContextSet.is_empty ctx then LMap.empty, ctx
   else
@@ -679,6 +650,35 @@ let normalize_opt_subst ctx =
 
 type universe_opt_subst = Universe.t option universe_map
 
+let subst_univs_fn_puniverses f (c, u as cu) =
+  let u' = Instance.subst_fn f u in
+    if u' == u then cu else (c, u')
+
+let nf_evars_and_universes_opt_subst f subst =
+  let subst = normalize_univ_variable_opt_subst (ref subst) in
+  let lsubst = level_subst_of subst in
+  let rec aux c =
+    match kind c with
+    | Evar (evk, args) ->
+      let args = Array.map aux args in
+      (match try f (evk, args) with Not_found -> None with
+      | None -> mkEvar (evk, args)
+      | Some c -> aux c)
+    | Const pu ->
+      let pu' = subst_univs_fn_puniverses lsubst pu in
+        if pu' == pu then c else mkConstU pu'
+    | Ind pu ->
+      let pu' = subst_univs_fn_puniverses lsubst pu in
+        if pu' == pu then c else mkIndU pu'
+    | Construct pu ->
+      let pu' = subst_univs_fn_puniverses lsubst pu in
+        if pu' == pu then c else mkConstructU pu'
+    | Sort (Type u) ->
+      let u' = Univ.subst_univs_universe subst u in
+        if u' == u then c else mkSort (sort_of_univ u')
+    | _ -> Constr.map aux c
+  in aux
+
 let make_opt_subst s = 
   fun x -> 
     (match Univ.LMap.find x s with