Merge PR coq#20004: Make cbn consider primitive values "constructors"

Reviewed-by: ppedrot Ack-by: SkySkimmer Co-authored-by: ppedrot <[email protected]>
proux01 · Jan 11, 2025 · 7431b4e · 7431b4e
2 parents 1af9c55 + f0cacc7
commit 7431b4e
Show file tree

Hide file tree

Showing 4 changed files with 144 additions and 18 deletions.
diff --git a/doc/changelog/04-tactics/20004-janno-cbn-prim-constructor.rst b/doc/changelog/04-tactics/20004-janno-cbn-prim-constructor.rst
@@ -0,0 +1,6 @@
+- **Fixed:**
+  `cbn` now considers primitive literals (integers, floats, arrays, strings)
+  "constructors", i.e. they now satisfy the `!` modifier in `Arguments`
+  (`#20004 <https://github.com/coq/coq/pull/20004>`_,
+  fixes `#20003 <https://github.com/coq/coq/issues/20003>`_,
+  by Jan-Oliver Kaiser).
diff --git a/tactics/cbn.ml b/tactics/cbn.ml
@@ -823,29 +823,19 @@ let whd_state_gen ?csts flags env sigma =
                  let stack' = (c, Stack.Proj (p, r, cst_l) :: stack) in
                  whrec Cst_stack.empty(* cst_l *) stack'
                | curr :: remains ->
-                 if curr == 0 then (* Try to reduce the record argument *)
+                 match Stack.strip_n_app curr (Stack.append_app [|c|] stack) with
+                 | None -> fold ()
+                 | Some (bef,arg,s') ->
                    let cst_l = Stack.Cst
                        { const=Stack.Cst_proj (p,r);
-                         volatile; curr; remains;
-                         params=Stack.empty;
+                         curr;
+                         remains;
+                         volatile;
+                         params=bef;
                          cst_l;
                        }
                    in
-                   whrec Cst_stack.empty (c, cst_l::stack)
-                 else
-                   match Stack.strip_n_app curr stack with
-                   | None -> fold ()
-                   | Some (bef,arg,s') ->
-                     let cst_l = Stack.Cst
-                         { const=Stack.Cst_proj (p,r);
-                           curr;
-                           remains;
-                           volatile;
-                           params=Stack.append_app [|c|] bef;
-                           cst_l;
-                         }
-                     in
-                     whrec Cst_stack.empty (arg,cst_l::s')
+                   whrec Cst_stack.empty (arg,cst_l::s')
            end)
 
     | LetIn (_,b,_,c) when RedFlags.red_set flags RedFlags.fZETA ->
@@ -953,6 +943,39 @@ let whd_state_gen ?csts flags env sigma =
                | Some t -> whrec cst_l' (t,s)
                | None -> ((mkApp (mkConstU kn, args), s), cst_l)
              end
+        |args, (Stack.Cst {const;curr;remains;volatile;params=s';cst_l} :: s'') ->
+          let x' = Stack.zip sigma (x, args) in
+          begin match remains with
+          | [] ->
+            (match const with
+            | Stack.Cst_const const ->
+              (match constant_opt_value_in env const with
+              | None -> fold ()
+              | Some body ->
+                let const = (fst const, EInstance.make (snd const)) in
+                let body = EConstr.of_constr body in
+                let cst_l = Cst_stack.add_cst ~volatile (mkConstU const) cst_l in
+                whrec cst_l (body, s' @ (Stack.append_app [|x'|] s'')))
+            | Stack.Cst_proj (p,r) ->
+              let stack = s' @ (Stack.append_app [|x'|] s'') in
+              match Stack.strip_n_app 0 stack with
+              | None -> assert false
+              | Some (_,arg,s'') ->
+                whrec Cst_stack.empty (arg, Stack.Proj (p,r,cst_l) :: s''))
+          | next :: remains' -> match Stack.strip_n_app (next-curr-1) s'' with
+            | None -> fold ()
+            | Some (bef,arg,s''') ->
+              let cst_l = Stack.Cst
+                  { const;
+                    curr=next;
+                    volatile;
+                    remains=remains';
+                    params=s' @ (Stack.append_app [|x'|] bef);
+                    cst_l;
+                  }
+              in
+              whrec Cst_stack.empty (arg, cst_l :: s''')
+          end
        | _ -> fold ()
       end
 

diff --git a/test-suite/bugs/bug_20003.v b/test-suite/bugs/bug_20003.v
@@ -0,0 +1,7 @@
+Require Import Corelib.Strings.PrimString.
+Definition t (s : string) := True.
+Arguments t !_ /.
+Goal t "test".
+Proof.
+  progress cbn.
+Abort.
diff --git a/test-suite/bugs/bug_20008.v b/test-suite/bugs/bug_20008.v
@@ -0,0 +1,90 @@
+Set Primitive Projections.
+
+Record R A := mk { p : A -> A -> A }.
+
+Arguments mk {_} _.
+Arguments p {_} _ !_ !_.
+
+(* using nat *)
+
+Goal forall x, p (mk (fun _ _ => 2)) x x = 0.
+Proof.
+  Fail progress cbn.
+Abort.
+
+Goal forall x, p (mk (fun _ _ => 2)) 3 x = 0.
+Proof.
+  Fail progress cbn.
+Abort.
+
+Goal p (mk (fun _ _ => 2)) 3 4 = 0.
+Proof.
+  progress cbn.
+Abort.
+
+Arguments p {_} _ !_ _.
+
+Goal forall x, p (mk (fun _ _ => 2)) x x = 0.
+Proof.
+  Fail progress cbn.
+Abort.
+
+Goal forall x, p (mk (fun _ _ => 2)) 3 x = 0.
+Proof.
+  progress cbn.
+Abort.
+
+Goal forall x, p (mk (fun _ _ => 2)) x 4 = 0.
+Proof.
+  Fail progress cbn.
+Abort.
+
+Goal p (mk (fun _ _ => 2)) 3 4 = 0.
+Proof.
+  progress cbn.
+Abort.
+
+(* using prim int *)
+Require Import PrimInt63.
+
+Open Scope int63_scope.
+
+Arguments p {_} _ !_ !_.
+
+Goal forall x, p (mk (fun _ _ => 2)) x x = 0.
+Proof.
+  intros x. Check x : int. (* sanity check that the scope is correct *)
+  Fail progress cbn.
+Abort.
+
+Goal forall x, p (mk (fun _ _ => 2)) 3 x = 0.
+Proof.
+  Fail progress cbn.
+Abort.
+
+Goal p (mk (fun _ _ => 2)) 3 4 = 0.
+Proof.
+  progress cbn.
+Abort.
+
+Arguments p {_} _ !_ _.
+
+Goal forall x, p (mk (fun _ _ => 2)) x x = 0.
+Proof.
+  Fail progress cbn.
+Abort.
+
+Goal forall x, p (mk (fun _ _ => 2)) 3 x = 0.
+Proof.
+  progress cbn.
+Abort.
+
+Goal forall x, p (mk (fun _ _ => 2)) x 4 = 0.
+Proof.
+  Fail progress cbn.
+Abort.
+
+Goal p (mk (fun _ _ => 2)) 3 4 = 0.
+Proof.
+  progress cbn.
+Abort.