From d7a9fea94772971a52d04f9f266fe6d5e25cd40e Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Mon, 2 May 2016 15:42:10 +0200
Subject: Avoid infinite loop/stack overflow when using "simpl nomatch" (bug
 #4576).

When encountering a "simpl nomatch" constant, the reduction machinery tries
to unfold it. If the subsequent partial reduction does not produce any
match construct, it keeps going from the reduced term. Unfortunately, the
reduced term has been refolded in the meantime, which means that some of
the previous reduction steps have been canceled, thus causing an infinite
loop. This patch delays the refolding till the very end, so that reduction
always progresses.

Disclaimer: I have no idea what I am doing here. The patch compiles the
standard library and the test suite properly, so hopefully they contain
enough tests to exercise the reduction machinery.
---
 pretyping/reductionops.ml     | 6 ++++--
 test-suite/bugs/closed/4576.v | 3 +++
 2 files changed, 7 insertions(+), 2 deletions(-)
 create mode 100644 test-suite/bugs/closed/4576.v

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 13b7fb4079..7c7b31395e 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -811,7 +811,7 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma =
     let fold () =
       let () = if !debug_RAKAM then
 	  let open Pp in pp (str "<><><><><>" ++ fnl ()) in
-      if tactic_mode then (Stack.best_state s cst_l,Cst_stack.empty) else (s,cst_l)
+      (s,cst_l)
     in
     match kind_of_term x with
     | Rel n when Closure.RedFlags.red_set flags Closure.RedFlags.fDELTA ->
@@ -1002,7 +1002,9 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma =
     | Rel _ | Var _ | Const _ | LetIn _ | Proj _ -> fold ()
     | Sort _ | Ind _ | Prod _ -> fold ()
   in
-  whrec (Option.default Cst_stack.empty csts)
+  fun xs ->
+  let (s,cst_l as res) = whrec (Option.default Cst_stack.empty csts) xs in
+  if tactic_mode then (Stack.best_state s cst_l,Cst_stack.empty) else res
 
 (** reduction machine without global env and refold machinery *)
 let local_whd_state_gen flags sigma =
diff --git a/test-suite/bugs/closed/4576.v b/test-suite/bugs/closed/4576.v
new file mode 100644
index 0000000000..2c643ea779
--- /dev/null
+++ b/test-suite/bugs/closed/4576.v
@@ -0,0 +1,3 @@
+Definition foo := O.
+Arguments foo : simpl nomatch.
+Timeout 1 Eval cbn in id foo.
-- 
cgit v1.2.3