Merge PR #11921: Remove some cruft from Reductionops API.

Reviewed-by: SkySkimmer
Reviewed-by: gares

5 files changed, 77 insertions, 85 deletions

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 1e4b537117..8822cc2338 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -622,9 +622,8 @@ type stack_reduction_function = contextual_stack_reduction_function
 type local_stack_reduction_function =
     evar_map -> constr -> constr * constr list
 
-type contextual_state_reduction_function =
+type state_reduction_function =
     env -> evar_map -> state -> state
-type state_reduction_function = contextual_state_reduction_function
 type local_state_reduction_function = evar_map -> state -> state
 
 let pr_state env sigma (tm,sk) =
@@ -1571,10 +1570,6 @@ let vm_infer_conv ?(pb=Reduction.CUMUL) env t1 t2 =
 (*             Special-Purpose Reduction                            *)
 (********************************************************************)
 
-let whd_meta sigma c = match EConstr.kind sigma c with
-  | Meta p -> (try meta_value sigma p with Not_found -> c)
-  | _ -> c
-
 let default_plain_instance_ident = Id.of_string "H"
 
 (* Try to replace all metas. Does not replace metas in the metas' values
@@ -1810,70 +1805,3 @@ let meta_instance sigma b =
 let nf_meta sigma c =
   let cl = mk_freelisted c in
   meta_instance sigma { cl with rebus = cl.rebus }
-
-(* Instantiate metas that create beta/iota redexes *)
-
-let meta_reducible_instance evd b =
-  let fm = b.freemetas in
-  let fold mv accu =
-    let fvalue = try meta_opt_fvalue evd mv with Not_found -> None in
-    match fvalue with
-    | None -> accu
-    | Some (g, (_, s)) -> Metamap.add mv (g.rebus, s) accu
-  in
-  let metas = Metaset.fold fold fm Metamap.empty in
-  let rec irec u =
-    let u = whd_betaiota Evd.empty u (* FIXME *) in
-    match EConstr.kind evd u with
-    | Case (ci,p,c,bl) when EConstr.isMeta evd (strip_outer_cast evd c) ->
-        let m = destMeta evd (strip_outer_cast evd c) in
-        (match
-          try
-            let g, s = Metamap.find m metas in
-            let is_coerce = match s with CoerceToType -> true | _ -> false in
-            if isConstruct evd g || not is_coerce then Some g else None
-          with Not_found -> None
-          with
-            | Some g -> irec (mkCase (ci,p,g,bl))
-            | None -> mkCase (ci,irec p,c,Array.map irec bl))
-    | App (f,l) when EConstr.isMeta evd (strip_outer_cast evd f) ->
-        let m = destMeta evd (strip_outer_cast evd f) in
-        (match
-          try
-            let g, s = Metamap.find m metas in
-            let is_coerce = match s with CoerceToType -> true | _ -> false in
-            if isLambda evd g || not is_coerce then Some g else None
-          with Not_found -> None
-         with
-           | Some g -> irec (mkApp (g,l))
-           | None -> mkApp (f,Array.map irec l))
-    | Meta m ->
-        (try let g, s = Metamap.find m metas in
-          let is_coerce = match s with CoerceToType -> true | _ -> false in
-          if not is_coerce then irec g else u
-         with Not_found -> u)
-    | Proj (p,c) when isMeta evd c || isCast evd c && isMeta evd (pi1 (destCast evd c)) (* What if two nested casts? *) ->
-      let m = try destMeta evd c with _ -> destMeta evd (pi1 (destCast evd c)) (* idem *) in
-          (match
-          try
-            let g, s = Metamap.find m metas in
-            let is_coerce = match s with CoerceToType -> true | _ -> false in
-            if isConstruct evd g || not is_coerce then Some g else None
-          with Not_found -> None
-          with
-            | Some g -> irec (mkProj (p,g))
-            | None -> mkProj (p,c))
-    | _ -> EConstr.map evd irec u
-  in
-  if Metaset.is_empty fm then (* nf_betaiota? *) b.rebus
-  else irec b.rebus
-
-let betazetaevar_applist sigma n c l =
-  let rec stacklam n env t stack =
-    if Int.equal n 0 then applist (substl env t, stack) else
-    match EConstr.kind sigma t, stack with
-    | Lambda(_,_,c), arg::stacktl -> stacklam (n-1) (arg::env) c stacktl
-    | LetIn(_,b,_,c), _ -> stacklam (n-1) (substl env b::env) c stack
-    | Evar _, _ -> applist (substl env t, stack)
-    | _ -> anomaly (Pp.str "Not enough lambda/let's.") in
-  stacklam n [] c l
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 5202380a13..243a2745f0 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -139,9 +139,8 @@ type stack_reduction_function = contextual_stack_reduction_function
 type local_stack_reduction_function =
     evar_map -> constr -> constr * constr list
 
-type contextual_state_reduction_function =
+type state_reduction_function =
     env -> evar_map -> state -> state
-type state_reduction_function = contextual_state_reduction_function
 type local_state_reduction_function = evar_map -> state -> state
 
 val pr_state : env -> evar_map -> state -> Pp.t
@@ -203,8 +202,8 @@ val whd_nored_state : local_state_reduction_function
 val whd_beta_state : local_state_reduction_function
 val whd_betaiota_state : local_state_reduction_function
 val whd_betaiotazeta_state : local_state_reduction_function
-val whd_all_state : contextual_state_reduction_function
-val whd_allnolet_state : contextual_state_reduction_function
+val whd_all_state : state_reduction_function
+val whd_allnolet_state : state_reduction_function
 val whd_betalet_state : local_state_reduction_function
 
 (** {6 Head normal forms } *)
@@ -309,13 +308,6 @@ val infer_conv_gen : (conv_pb -> l2r:bool -> evar_map -> TransparentState.t ->
   ?catch_incon:bool -> ?pb:conv_pb -> ?ts:TransparentState.t -> env ->
   evar_map -> constr -> constr -> evar_map option
 
-(** {6 Special-Purpose Reduction Functions } *)
-
-val whd_meta : local_reduction_function
-val plain_instance : evar_map -> constr Metamap.t -> constr -> constr
-val instance : evar_map -> constr Metamap.t -> constr -> constr
-val betazetaevar_applist : evar_map -> int -> constr -> constr list -> constr
-
 (** {6 Heuristic for Conversion with Evar } *)
 
 val whd_betaiota_deltazeta_for_iota_state :
@@ -324,4 +316,3 @@ val whd_betaiota_deltazeta_for_iota_state :
 (** {6 Meta-related reduction functions } *)
 val meta_instance : evar_map -> constr freelisted -> constr
 val nf_meta       : evar_map -> constr -> constr
-val meta_reducible_instance : evar_map -> constr freelisted -> constr
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 821c57d033..1f091c3df8 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -97,6 +97,16 @@ let decomp_sort env sigma t =
 
 let destSort sigma s = ESorts.kind sigma (destSort sigma s)
 
+let betazetaevar_applist sigma n c l =
+  let rec stacklam n env t stack =
+    if Int.equal n 0 then applist (substl env t, stack) else
+    match EConstr.kind sigma t, stack with
+    | Lambda(_,_,c), arg::stacktl -> stacklam (n-1) (arg::env) c stacktl
+    | LetIn(_,b,_,c), _ -> stacklam (n-1) (substl env b::env) c stack
+    | Evar _, _ -> applist (substl env t, stack)
+    | _ -> anomaly (Pp.str "Not enough lambda/let's.") in
+  stacklam n [] c l
+
 let retype ?(polyprop=true) sigma =
   let rec type_of env cstr =
     match EConstr.kind sigma cstr with
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index ec3fb0758e..90dde01915 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -87,6 +87,12 @@ let occur_meta_or_undefined_evar evd c =
     | _ -> Constr.iter occrec c
   in try occrec c; false with Occur | Not_found -> true
 
+let whd_meta sigma c = match EConstr.kind sigma c with
+  | Meta p ->
+    (try Evd.meta_value sigma p with Not_found -> c)
+    (* Not recursive, for some reason *)
+  | _ -> c
+
 let occur_meta_evd sigma mv c =
   let rec occrec c =
     (* Note: evars are not instantiated by terms with metas *)
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 83ef91bfd9..37d54a4eea 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -249,6 +249,63 @@ let clenv_dependent ce = clenv_dependent_gen false ce
 
 (******************************************************************)
 
+(* Instantiate metas that create beta/iota redexes *)
+
+let meta_reducible_instance evd b =
+  let fm = b.freemetas in
+  let fold mv accu =
+    let fvalue = try meta_opt_fvalue evd mv with Not_found -> None in
+    match fvalue with
+    | None -> accu
+    | Some (g, (_, s)) -> Metamap.add mv (g.rebus, s) accu
+  in
+  let metas = Metaset.fold fold fm Metamap.empty in
+  let rec irec u =
+    let u = whd_betaiota Evd.empty u (* FIXME *) in
+    match EConstr.kind evd u with
+    | Case (ci,p,c,bl) when EConstr.isMeta evd (strip_outer_cast evd c) ->
+        let m = destMeta evd (strip_outer_cast evd c) in
+        (match
+          try
+            let g, s = Metamap.find m metas in
+            let is_coerce = match s with CoerceToType -> true | _ -> false in
+            if isConstruct evd g || not is_coerce then Some g else None
+          with Not_found -> None
+          with
+            | Some g -> irec (mkCase (ci,p,g,bl))
+            | None -> mkCase (ci,irec p,c,Array.map irec bl))
+    | App (f,l) when EConstr.isMeta evd (strip_outer_cast evd f) ->
+        let m = destMeta evd (strip_outer_cast evd f) in
+        (match
+          try
+            let g, s = Metamap.find m metas in
+            let is_coerce = match s with CoerceToType -> true | _ -> false in
+            if isLambda evd g || not is_coerce then Some g else None
+          with Not_found -> None
+         with
+           | Some g -> irec (mkApp (g,l))
+           | None -> mkApp (f,Array.map irec l))
+    | Meta m ->
+        (try let g, s = Metamap.find m metas in
+          let is_coerce = match s with CoerceToType -> true | _ -> false in
+          if not is_coerce then irec g else u
+         with Not_found -> u)
+    | Proj (p,c) when isMeta evd c || isCast evd c && isMeta evd (pi1 (destCast evd c)) (* What if two nested casts? *) ->
+      let m = try destMeta evd c with _ -> destMeta evd (pi1 (destCast evd c)) (* idem *) in
+          (match
+          try
+            let g, s = Metamap.find m metas in
+            let is_coerce = match s with CoerceToType -> true | _ -> false in
+            if isConstruct evd g || not is_coerce then Some g else None
+          with Not_found -> None
+          with
+            | Some g -> irec (mkProj (p,g))
+            | None -> mkProj (p,c))
+    | _ -> EConstr.map evd irec u
+  in
+  if Metaset.is_empty fm then (* nf_betaiota? *) b.rebus
+  else irec b.rebus
+
 let clenv_unify ?(flags=default_unify_flags ()) cv_pb t1 t2 clenv =
   { clenv with
       evd = w_unify ~flags clenv.env clenv.evd cv_pb t1 t2 }