Merge PR #13699: Fix #13579 (hnf on primitives raises an anomaly)

Ack-by: SkySkimmer
Reviewed-by: ppedrot

3 files changed, 23 insertions, 5 deletions

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 3da75f67b9..10caf855ba 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -978,6 +978,9 @@ let whd_betalet = red_of_state_red whd_betalet_state
 
 (* 2. Delta Reduction Functions *)
 
+let whd_const_state c e = raw_whd_state_gen CClosure.RedFlags.(mkflags [fCONST c]) e
+let whd_const c = red_of_state_red (whd_const_state c)
+
 let whd_delta_state e = raw_whd_state_gen CClosure.delta e
 let whd_delta_stack = stack_red_of_state_red whd_delta_state
 let whd_delta = red_of_state_red whd_delta_state
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 59bc4a8b72..9d41e7ab58 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -185,6 +185,7 @@ val whd_betalet_stack : stack_reduction_function
 
 (** {6 Head normal forms } *)
 
+val whd_const : Constant.t -> reduction_function
 val whd_delta_stack :  stack_reduction_function
 val whd_delta :  reduction_function
 val whd_betadeltazeta_stack :  stack_reduction_function
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 01819a650b..1523ec502d 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -68,8 +68,7 @@ let error_not_evaluable r =
      spc () ++ str "to an evaluable reference.")
 
 let is_evaluable_const env cst =
-  is_transparent env (ConstKey cst) &&
-    (evaluable_constant cst env || is_primitive env cst)
+  is_transparent env (ConstKey cst) && evaluable_constant cst env
 
 let is_evaluable_var env id =
   is_transparent env (VarKey id) && evaluable_named id env
@@ -163,6 +162,10 @@ let reference_value env sigma c u =
     | None -> raise NotEvaluable
     | Some d -> d
 
+let is_primitive_val sigma c = match EConstr.kind sigma c with
+  | Int _ | Float _ | Array _ -> true
+  | _ -> false
+
 (************************************************************************)
 (* Reduction of constants hiding a fixpoint (e.g. for "simpl" tactic).  *)
 (* One reuses the name of the function after reduction of the fixpoint  *)
@@ -714,7 +717,8 @@ and reduce_params env sigma stack l =
         let arg = List.nth stack i in
         let rarg = whd_construct_stack env sigma arg in
           match EConstr.kind sigma (fst rarg) with
-          | Construct _ -> List.assign stack i (applist rarg)
+          | Construct _ | Int _ | Float _ | Array _ ->
+             List.assign stack i (applist rarg)
           | _ -> raise Redelimination)
       stack l
 
@@ -770,6 +774,16 @@ and whd_simpl_stack env sigma =
                  else s'
                with Redelimination -> s')
 
+      | Const (cst, _) when is_primitive env cst ->
+         (try
+            let args =
+              List.map_filter_i (fun i a ->
+                  match a with CPrimitives.Kwhnf -> Some i | _ -> None)
+                (CPrimitives.kind (Option.get (get_primitive env cst))) in
+            let stack = reduce_params env sigma stack args in
+            whd_const cst env sigma (applist (x, stack)), []
+          with Redelimination -> s')
+
       | _ ->
         match match_eval_ref env sigma x stack with
         | Some (ref, u) ->
@@ -880,11 +894,11 @@ and special_red_case env sigma (ci, u, pms, p, iv, c, lf) =
   in
   redrec (push_app sigma (c, []))
 
-(* reduce until finding an applied constructor or fail *)
+(* reduce until finding an applied constructor (or primitive value) or fail *)
 
 and whd_construct_stack env sigma s =
   let (constr, cargs as s') = whd_simpl_stack env sigma (s, []) in
-  if reducible_mind_case sigma constr then s'
+  if reducible_mind_case sigma constr || is_primitive_val sigma constr then s'
   else match match_eval_ref env sigma constr cargs with
   | Some (ref, u) ->
     (match reference_opt_value env sigma ref u with