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

Ack-by: SkySkimmer
Reviewed-by: ppedrot

10 files changed, 71 insertions, 5 deletions

diff --git a/doc/changelog/04-tactics/13699-fix13579.rst b/doc/changelog/04-tactics/13699-fix13579.rst
new file mode 100644
index 0000000000..9cf62fb595
--- /dev/null
+++ b/doc/changelog/04-tactics/13699-fix13579.rst
@@ -0,0 +1,6 @@
+- **Fixed:**
+  :tacn:`simpl` and :tacn:`hnf` now reduce primitive functions
+  on primitive integers, floats and arrays
+  (`#13699 <https://github.com/coq/coq/pull/13699>`_,
+  fixes `#13579 <https://github.com/coq/coq/issues/13579>`_,
+  by Pierre Roux).
diff --git a/interp/notation.ml b/interp/notation.ml
index 33d96f0439..d6002d71b5 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -1357,6 +1357,7 @@ let find_with_delimiters = function
       match (String.Map.find scope !scope_map).delimiters with
         | Some key -> Some (Some scope, Some key)
         | None -> None
+        | exception Not_found -> None
 
 let rec find_without_delimiters find (ntn_scope,ntn) = function
   | OpenScopeItem scope :: scopes ->
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 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
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.