diff options
| author | Guillaume Melquiond | 2016-05-02 15:42:10 +0200 |
|---|---|---|
| committer | Guillaume Melquiond | 2016-05-02 15:42:10 +0200 |
| commit | d7a9fea94772971a52d04f9f266fe6d5e25cd40e (patch) | |
| tree | 381752564133f3b612b2c1f0b914a02360b3c5e3 | |
| parent | bd5da52c6c625cb4559dd92051384383473ecb1b (diff) | |
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.
| -rw-r--r-- | pretyping/reductionops.ml | 6 | ||||
| -rw-r--r-- | test-suite/bugs/closed/4576.v | 3 |
2 files changed, 7 insertions, 2 deletions
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. |