Fix #13579 (hnf on primitives raises an anomaly)

Also works for simpl.

8 files changed, 64 insertions, 5 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index 6f2aeab203..63fbaa6a3b 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -571,6 +571,12 @@ let is_primitive env c =
   | Declarations.Primitive _ -> true
   | _ -> false
 
+let get_primitive env c =
+  let cb = lookup_constant c env in
+  match cb.Declarations.const_body with
+  | Declarations.Primitive p -> Some p
+  | _ -> None
+
 let is_int63_type env c =
   match env.retroknowledge.Retroknowledge.retro_int63 with
   | None -> false
diff --git a/kernel/environ.mli b/kernel/environ.mli
index dfd9173d10..414ef2b4d7 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -248,6 +248,7 @@ val constant_type_in : env -> Constant.t puniverses -> types
 val constant_opt_value_in : env -> Constant.t puniverses -> constr option
 
 val is_primitive : env -> Constant.t -> bool
+val get_primitive : env -> Constant.t -> CPrimitives.t option
 
 val is_array_type : env -> Constant.t -> bool
 val is_int63_type : env -> Constant.t -> bool
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 52f60fbc5e..ec7f0ef377 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -955,6 +955,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 ae93eb48b4..8250a1122b 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -182,6 +182,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 411fb0cd89..b4ff6ce923 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  *)
@@ -708,7 +711,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
 
@@ -764,6 +768,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) ->
@@ -874,11 +888,11 @@ and special_red_case env sigma (ci, 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
diff --git a/test-suite/output/Int63Syntax.out b/test-suite/output/Int63Syntax.out
index ca8e1b58a8..7ca4de1e46 100644
--- a/test-suite/output/Int63Syntax.out
+++ b/test-suite/output/Int63Syntax.out
@@ -56,3 +56,21 @@ t = 2%i63
      : int
      = 37151199385380486
      : int
+     = 4
+     : int
+     = 4
+     : int
+     = 4
+     : int
+     = add
+     : int -> int -> int
+     = 12
+     : int
+     = 12
+     : int
+     = 12
+     : int
+     = 3 + x
+     : int
+     = 1 + 2 + x
+     : int
diff --git a/test-suite/output/Int63Syntax.v b/test-suite/output/Int63Syntax.v
index 6f1046f7a5..50910264f2 100644
--- a/test-suite/output/Int63Syntax.v
+++ b/test-suite/output/Int63Syntax.v
@@ -40,3 +40,18 @@ Open Scope int63_scope.
 Check (2+2).
 Eval vm_compute in 2+2.
 Eval vm_compute in 65675757 * 565675998.
+
+Eval simpl in 2+2.
+Eval hnf in 2+2.
+Eval cbn in 2+2.
+Eval hnf in PrimInt63.add.
+
+Eval simpl in (2 * 3) + (2 * 3).
+Eval hnf in (2 * 3) + (2 * 3).
+Eval cbn in (2 * 3) + (2 * 3).
+
+Section TestNoSimpl.
+Variable x : int.
+Eval simpl in 1 + 2 + x.
+Eval hnf in 1 + 2 + x.
+End TestNoSimpl.
diff --git a/theories/Numbers/Cyclic/Int63/Int63.v b/theories/Numbers/Cyclic/Int63/Int63.v
index f324bbf52b..7bb725538b 100644
--- a/theories/Numbers/Cyclic/Int63/Int63.v
+++ b/theories/Numbers/Cyclic/Int63/Int63.v
@@ -954,6 +954,7 @@ Proof.
    intros _ HH; generalize (HH H1); discriminate.
  clear H.
  generalize (ltb_spec j i); case Int63.ltb; intros H2; unfold bit; simpl.
+   change 62%int63 with (digits - 1)%int63.
    assert (F2: (φ j < φ i)%Z) by (case H2; auto); clear H2.
    replace (is_zero (((x << i) >> j) << (digits - 1))) with true; auto.
    case (to_Z_bounded j); intros  H1j H2j.