An optimization of tactic constructor.

As was questioned on Stack Overflow and discussed on Gitter, reduction
of the conclusion of the goal was done up to n+1 times for a failing
call to "constructor" on an inductive type of n constructors. We do it
at most once.

Reworking the layout of the code at the same time.

2 files changed, 246 insertions, 29 deletions

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 5698312ae..2b06e1133 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2219,27 +2219,27 @@ let check_number_of_constructors expctdnumopt i nconstr =
   end;
   if i > nconstr then error "Not enough constructors."
 
-let constructor_tac with_evars expctdnumopt i lbind =
+let constructor_core with_evars cstr lbind =
   Proofview.Goal.enter begin fun gl ->
     let sigma = Proofview.Goal.sigma gl in
+    let env = Proofview.Goal.env gl in
+    let (sigma, (cons, u)) = Evd.fresh_constructor_instance env sigma cstr in
+    let cons = mkConstructU (cons, EInstance.make u) in
+    let apply_tac = general_apply true false with_evars None (Loc.tag (cons,lbind)) in
+    Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma) apply_tac
+  end
+
+let constructor_tac with_evars expctdnumopt i lbind =
+  Proofview.Goal.enter begin fun gl ->
     let cl = Tacmach.New.pf_concl gl in
-    let reduce_to_quantified_ind =
-      Tacmach.New.pf_apply Tacred.reduce_to_quantified_ind gl
-    in
-    let (mind,redcl) = reduce_to_quantified_ind cl in
-    let nconstr =
-      Array.length (snd (Global.lookup_inductive (fst mind))).mind_consnames in
-      check_number_of_constructors expctdnumopt i nconstr;
-
-      let (sigma, (cons, u)) = Evd.fresh_constructor_instance
-	(Proofview.Goal.env gl) sigma (fst mind, i) in
-      let cons = mkConstructU (cons, EInstance.make u) in
-	
-      let apply_tac = general_apply true false with_evars None (Loc.tag (cons,lbind)) in
-      Tacticals.New.tclTHENLIST
-         [ Proofview.Unsafe.tclEVARS sigma;
-           convert_concl_no_check redcl DEFAULTcast;
-           intros; apply_tac]
+    let ((ind,_),redcl) = Tacmach.New.pf_apply Tacred.reduce_to_quantified_ind gl cl in
+    let nconstr = Array.length (snd (Global.lookup_inductive ind)).mind_consnames in
+    check_number_of_constructors expctdnumopt i nconstr;
+    Tacticals.New.tclTHENLIST [
+      convert_concl_no_check redcl DEFAULTcast;
+      intros;
+      constructor_core with_evars (ind, i) lbind
+    ]
   end
 
 let one_constructor i lbind = constructor_tac false None i lbind
@@ -2251,23 +2251,24 @@ let one_constructor i lbind = constructor_tac false None i lbind
 
 let any_constructor with_evars tacopt =
   let one_constr =
-    let tac i = constructor_tac with_evars None i NoBindings in
+    let tac cstr = constructor_core with_evars cstr NoBindings in
     match tacopt with
     | None -> tac
-    | Some t -> fun i -> Tacticals.New.tclTHEN (tac i) t in
-  let rec any_constr n i () =
-    if Int.equal i n then one_constr i
-    else Tacticals.New.tclORD (one_constr i) (any_constr n (i + 1)) in
+    | Some t -> fun cstr -> Tacticals.New.tclTHEN (tac cstr) t in
+  let rec any_constr ind n i () =
+    if Int.equal i n then one_constr (ind,i)
+    else Tacticals.New.tclORD (one_constr (ind,i)) (any_constr ind n (i + 1)) in
   Proofview.Goal.enter begin fun gl ->
     let cl = Tacmach.New.pf_concl gl in
-    let reduce_to_quantified_ind =
-      Tacmach.New.pf_apply Tacred.reduce_to_quantified_ind gl
-    in
-    let mind = fst (reduce_to_quantified_ind cl) in
+    let (ind,_),redcl = Tacmach.New.pf_apply Tacred.reduce_to_quantified_ind gl cl in
     let nconstr =
-      Array.length (snd (Global.lookup_inductive (fst mind))).mind_consnames in
+      Array.length (snd (Global.lookup_inductive ind)).mind_consnames in
     if Int.equal nconstr 0 then error "The type has no constructors.";
-    any_constr nconstr 1 ()
+    Tacticals.New.tclTHENLIST [
+      convert_concl_no_check redcl DEFAULTcast;
+      intros;
+      any_constr ind nconstr 1 ()
+    ]
  end
 
 let left_with_bindings  with_evars = constructor_tac with_evars (Some 2) 1
diff --git a/test-suite/complexity/constructor.v b/test-suite/complexity/constructor.v
new file mode 100644
index 000000000..c5e195382
--- /dev/null
+++ b/test-suite/complexity/constructor.v
@@ -0,0 +1,216 @@
+(* Checks that constructor does not repeat the reduction of the conclusion *)
+(* Expected time < 3.00s *)
+
+(* Note: on i7 2.2GZ, time decreases from 85s to 0.1s *)
+
+Inductive T : bool -> Prop :=
+| C000 : T true | C001 : T true | C002 : T true | C003 : T true | C004 : T true
+| C005 : T true | C006 : T true | C007 : T true | C008 : T true | C009 : T true
+| C010 : T true | C011 : T true | C012 : T true | C013 : T true | C014 : T true
+| C015 : T true | C016 : T true | C017 : T true | C018 : T true | C019 : T true
+| C020 : T true | C021 : T true | C022 : T true | C023 : T true | C024 : T true
+| C025 : T true | C026 : T true | C027 : T true | C028 : T true | C029 : T true
+| C030 : T true | C031 : T true | C032 : T true | C033 : T true | C034 : T true
+| C035 : T true | C036 : T true | C037 : T true | C038 : T true | C039 : T true
+| C040 : T true | C041 : T true | C042 : T true | C043 : T true | C044 : T true
+| C045 : T true | C046 : T true | C047 : T true | C048 : T true | C049 : T true
+| C050 : T true | C051 : T true | C052 : T true | C053 : T true | C054 : T true
+| C055 : T true | C056 : T true | C057 : T true | C058 : T true | C059 : T true
+| C060 : T true | C061 : T true | C062 : T true | C063 : T true | C064 : T true
+| C065 : T true | C066 : T true | C067 : T true | C068 : T true | C069 : T true
+| C070 : T true | C071 : T true | C072 : T true | C073 : T true | C074 : T true
+| C075 : T true | C076 : T true | C077 : T true | C078 : T true | C079 : T true
+| C080 : T true | C081 : T true | C082 : T true | C083 : T true | C084 : T true
+| C085 : T true | C086 : T true | C087 : T true | C088 : T true | C089 : T true
+| C090 : T true | C091 : T true | C092 : T true | C093 : T true | C094 : T true
+| C095 : T true | C096 : T true | C097 : T true | C098 : T true | C099 : T true
+| C100 : T true | C101 : T true | C102 : T true | C103 : T true | C104 : T true
+| C105 : T true | C106 : T true | C107 : T true | C108 : T true | C109 : T true
+| C110 : T true | C111 : T true | C112 : T true | C113 : T true | C114 : T true
+| C115 : T true | C116 : T true | C117 : T true | C118 : T true | C119 : T true
+| C120 : T true | C121 : T true | C122 : T true | C123 : T true | C124 : T true
+| C125 : T true | C126 : T true | C127 : T true | C128 : T true | C129 : T true
+| C130 : T true | C131 : T true | C132 : T true | C133 : T true | C134 : T true
+| C135 : T true | C136 : T true | C137 : T true | C138 : T true | C139 : T true
+| C140 : T true | C141 : T true | C142 : T true | C143 : T true | C144 : T true
+| C145 : T true | C146 : T true | C147 : T true | C148 : T true | C149 : T true
+| C150 : T true | C151 : T true | C152 : T true | C153 : T true | C154 : T true
+| C155 : T true | C156 : T true | C157 : T true | C158 : T true | C159 : T true
+| C160 : T true | C161 : T true | C162 : T true | C163 : T true | C164 : T true
+| C165 : T true | C166 : T true | C167 : T true | C168 : T true | C169 : T true
+| C170 : T true | C171 : T true | C172 : T true | C173 : T true | C174 : T true
+| C175 : T true | C176 : T true | C177 : T true | C178 : T true | C179 : T true
+| C180 : T true | C181 : T true | C182 : T true | C183 : T true | C184 : T true
+| C185 : T true | C186 : T true | C187 : T true | C188 : T true | C189 : T true
+| C190 : T true | C191 : T true | C192 : T true | C193 : T true | C194 : T true
+| C195 : T true | C196 : T true | C197 : T true | C198 : T true | C199 : T true
+| C200 : T true | C201 : T true | C202 : T true | C203 : T true | C204 : T true
+| C205 : T true | C206 : T true | C207 : T true | C208 : T true | C209 : T true
+| C210 : T true | C211 : T true | C212 : T true | C213 : T true | C214 : T true
+| C215 : T true | C216 : T true | C217 : T true | C218 : T true | C219 : T true
+| C220 : T true | C221 : T true | C222 : T true | C223 : T true | C224 : T true
+| C225 : T true | C226 : T true | C227 : T true | C228 : T true | C229 : T true
+| C230 : T true | C231 : T true | C232 : T true | C233 : T true | C234 : T true
+| C235 : T true | C236 : T true | C237 : T true | C238 : T true | C239 : T true
+| C240 : T true | C241 : T true | C242 : T true | C243 : T true | C244 : T true
+| C245 : T true | C246 : T true | C247 : T true | C248 : T true | C249 : T true
+| C250 : T true | C251 : T true | C252 : T true | C253 : T true | C254 : T true
+| C255 : T true | C256 : T true | C257 : T true | C258 : T true | C259 : T true
+| C260 : T true | C261 : T true | C262 : T true | C263 : T true | C264 : T true
+| C265 : T true | C266 : T true | C267 : T true | C268 : T true | C269 : T true
+| C270 : T true | C271 : T true | C272 : T true | C273 : T true | C274 : T true
+| C275 : T true | C276 : T true | C277 : T true | C278 : T true | C279 : T true
+| C280 : T true | C281 : T true | C282 : T true | C283 : T true | C284 : T true
+| C285 : T true | C286 : T true | C287 : T true | C288 : T true | C289 : T true
+| C290 : T true | C291 : T true | C292 : T true | C293 : T true | C294 : T true
+| C295 : T true | C296 : T true | C297 : T true | C298 : T true | C299 : T true
+| C300 : T true | C301 : T true | C302 : T true | C303 : T true | C304 : T true
+| C305 : T true | C306 : T true | C307 : T true | C308 : T true | C309 : T true
+| C310 : T true | C311 : T true | C312 : T true | C313 : T true | C314 : T true
+| C315 : T true | C316 : T true | C317 : T true | C318 : T true | C319 : T true
+| C320 : T true | C321 : T true | C322 : T true | C323 : T true | C324 : T true
+| C325 : T true | C326 : T true | C327 : T true | C328 : T true | C329 : T true
+| C330 : T true | C331 : T true | C332 : T true | C333 : T true | C334 : T true
+| C335 : T true | C336 : T true | C337 : T true | C338 : T true | C339 : T true
+| C340 : T true | C341 : T true | C342 : T true | C343 : T true | C344 : T true
+| C345 : T true | C346 : T true | C347 : T true | C348 : T true | C349 : T true
+| C350 : T true | C351 : T true | C352 : T true | C353 : T true | C354 : T true
+| C355 : T true | C356 : T true | C357 : T true | C358 : T true | C359 : T true
+| C360 : T true | C361 : T true | C362 : T true | C363 : T true | C364 : T true
+| C365 : T true | C366 : T true | C367 : T true | C368 : T true | C369 : T true
+| C370 : T true | C371 : T true | C372 : T true | C373 : T true | C374 : T true
+| C375 : T true | C376 : T true | C377 : T true | C378 : T true | C379 : T true
+| C380 : T true | C381 : T true | C382 : T true | C383 : T true | C384 : T true
+| C385 : T true | C386 : T true | C387 : T true | C388 : T true | C389 : T true
+| C390 : T true | C391 : T true | C392 : T true | C393 : T true | C394 : T true
+| C395 : T true | C396 : T true | C397 : T true | C398 : T true | C399 : T true
+| C400 : T true | C401 : T true | C402 : T true | C403 : T true | C404 : T true
+| C405 : T true | C406 : T true | C407 : T true | C408 : T true | C409 : T true
+| C410 : T true | C411 : T true | C412 : T true | C413 : T true | C414 : T true
+| C415 : T true | C416 : T true | C417 : T true | C418 : T true | C419 : T true
+| C420 : T true | C421 : T true | C422 : T true | C423 : T true | C424 : T true
+| C425 : T true | C426 : T true | C427 : T true | C428 : T true | C429 : T true
+| C430 : T true | C431 : T true | C432 : T true | C433 : T true | C434 : T true
+| C435 : T true | C436 : T true | C437 : T true | C438 : T true | C439 : T true
+| C440 : T true | C441 : T true | C442 : T true | C443 : T true | C444 : T true
+| C445 : T true | C446 : T true | C447 : T true | C448 : T true | C449 : T true
+| C450 : T true | C451 : T true | C452 : T true | C453 : T true | C454 : T true
+| C455 : T true | C456 : T true | C457 : T true | C458 : T true | C459 : T true
+| C460 : T true | C461 : T true | C462 : T true | C463 : T true | C464 : T true
+| C465 : T true | C466 : T true | C467 : T true | C468 : T true | C469 : T true
+| C470 : T true | C471 : T true | C472 : T true | C473 : T true | C474 : T true
+| C475 : T true | C476 : T true | C477 : T true | C478 : T true | C479 : T true
+| C480 : T true | C481 : T true | C482 : T true | C483 : T true | C484 : T true
+| C485 : T true | C486 : T true | C487 : T true | C488 : T true | C489 : T true
+| C490 : T true | C491 : T true | C492 : T true | C493 : T true | C494 : T true
+| C495 : T true | C496 : T true | C497 : T true | C498 : T true | C499 : T true
+| C500 : T true | C501 : T true | C502 : T true | C503 : T true | C504 : T true
+| C505 : T true | C506 : T true | C507 : T true | C508 : T true | C509 : T true
+| C510 : T true | C511 : T true | C512 : T true | C513 : T true | C514 : T true
+| C515 : T true | C516 : T true | C517 : T true | C518 : T true | C519 : T true
+| C520 : T true | C521 : T true | C522 : T true | C523 : T true | C524 : T true
+| C525 : T true | C526 : T true | C527 : T true | C528 : T true | C529 : T true
+| C530 : T true | C531 : T true | C532 : T true | C533 : T true | C534 : T true
+| C535 : T true | C536 : T true | C537 : T true | C538 : T true | C539 : T true
+| C540 : T true | C541 : T true | C542 : T true | C543 : T true | C544 : T true
+| C545 : T true | C546 : T true | C547 : T true | C548 : T true | C549 : T true
+| C550 : T true | C551 : T true | C552 : T true | C553 : T true | C554 : T true
+| C555 : T true | C556 : T true | C557 : T true | C558 : T true | C559 : T true
+| C560 : T true | C561 : T true | C562 : T true | C563 : T true | C564 : T true
+| C565 : T true | C566 : T true | C567 : T true | C568 : T true | C569 : T true
+| C570 : T true | C571 : T true | C572 : T true | C573 : T true | C574 : T true
+| C575 : T true | C576 : T true | C577 : T true | C578 : T true | C579 : T true
+| C580 : T true | C581 : T true | C582 : T true | C583 : T true | C584 : T true
+| C585 : T true | C586 : T true | C587 : T true | C588 : T true | C589 : T true
+| C590 : T true | C591 : T true | C592 : T true | C593 : T true | C594 : T true
+| C595 : T true | C596 : T true | C597 : T true | C598 : T true | C599 : T true
+| C600 : T true | C601 : T true | C602 : T true | C603 : T true | C604 : T true
+| C605 : T true | C606 : T true | C607 : T true | C608 : T true | C609 : T true
+| C610 : T true | C611 : T true | C612 : T true | C613 : T true | C614 : T true
+| C615 : T true | C616 : T true | C617 : T true | C618 : T true | C619 : T true
+| C620 : T true | C621 : T true | C622 : T true | C623 : T true | C624 : T true
+| C625 : T true | C626 : T true | C627 : T true | C628 : T true | C629 : T true
+| C630 : T true | C631 : T true | C632 : T true | C633 : T true | C634 : T true
+| C635 : T true | C636 : T true | C637 : T true | C638 : T true | C639 : T true
+| C640 : T true | C641 : T true | C642 : T true | C643 : T true | C644 : T true
+| C645 : T true | C646 : T true | C647 : T true | C648 : T true | C649 : T true
+| C650 : T true | C651 : T true | C652 : T true | C653 : T true | C654 : T true
+| C655 : T true | C656 : T true | C657 : T true | C658 : T true | C659 : T true
+| C660 : T true | C661 : T true | C662 : T true | C663 : T true | C664 : T true
+| C665 : T true | C666 : T true | C667 : T true | C668 : T true | C669 : T true
+| C670 : T true | C671 : T true | C672 : T true | C673 : T true | C674 : T true
+| C675 : T true | C676 : T true | C677 : T true | C678 : T true | C679 : T true
+| C680 : T true | C681 : T true | C682 : T true | C683 : T true | C684 : T true
+| C685 : T true | C686 : T true | C687 : T true | C688 : T true | C689 : T true
+| C690 : T true | C691 : T true | C692 : T true | C693 : T true | C694 : T true
+| C695 : T true | C696 : T true | C697 : T true | C698 : T true | C699 : T true
+| C700 : T true | C701 : T true | C702 : T true | C703 : T true | C704 : T true
+| C705 : T true | C706 : T true | C707 : T true | C708 : T true | C709 : T true
+| C710 : T true | C711 : T true | C712 : T true | C713 : T true | C714 : T true
+| C715 : T true | C716 : T true | C717 : T true | C718 : T true | C719 : T true
+| C720 : T true | C721 : T true | C722 : T true | C723 : T true | C724 : T true
+| C725 : T true | C726 : T true | C727 : T true | C728 : T true | C729 : T true
+| C730 : T true | C731 : T true | C732 : T true | C733 : T true | C734 : T true
+| C735 : T true | C736 : T true | C737 : T true | C738 : T true | C739 : T true
+| C740 : T true | C741 : T true | C742 : T true | C743 : T true | C744 : T true
+| C745 : T true | C746 : T true | C747 : T true | C748 : T true | C749 : T true
+| C750 : T true | C751 : T true | C752 : T true | C753 : T true | C754 : T true
+| C755 : T true | C756 : T true | C757 : T true | C758 : T true | C759 : T true
+| C760 : T true | C761 : T true | C762 : T true | C763 : T true | C764 : T true
+| C765 : T true | C766 : T true | C767 : T true | C768 : T true | C769 : T true
+| C770 : T true | C771 : T true | C772 : T true | C773 : T true | C774 : T true
+| C775 : T true | C776 : T true | C777 : T true | C778 : T true | C779 : T true
+| C780 : T true | C781 : T true | C782 : T true | C783 : T true | C784 : T true
+| C785 : T true | C786 : T true | C787 : T true | C788 : T true | C789 : T true
+| C790 : T true | C791 : T true | C792 : T true | C793 : T true | C794 : T true
+| C795 : T true | C796 : T true | C797 : T true | C798 : T true | C799 : T true
+| C800 : T true | C801 : T true | C802 : T true | C803 : T true | C804 : T true
+| C805 : T true | C806 : T true | C807 : T true | C808 : T true | C809 : T true
+| C810 : T true | C811 : T true | C812 : T true | C813 : T true | C814 : T true
+| C815 : T true | C816 : T true | C817 : T true | C818 : T true | C819 : T true
+| C820 : T true | C821 : T true | C822 : T true | C823 : T true | C824 : T true
+| C825 : T true | C826 : T true | C827 : T true | C828 : T true | C829 : T true
+| C830 : T true | C831 : T true | C832 : T true | C833 : T true | C834 : T true
+| C835 : T true | C836 : T true | C837 : T true | C838 : T true | C839 : T true
+| C840 : T true | C841 : T true | C842 : T true | C843 : T true | C844 : T true
+| C845 : T true | C846 : T true | C847 : T true | C848 : T true | C849 : T true
+| C850 : T true | C851 : T true | C852 : T true | C853 : T true | C854 : T true
+| C855 : T true | C856 : T true | C857 : T true | C858 : T true | C859 : T true
+| C860 : T true | C861 : T true | C862 : T true | C863 : T true | C864 : T true
+| C865 : T true | C866 : T true | C867 : T true | C868 : T true | C869 : T true
+| C870 : T true | C871 : T true | C872 : T true | C873 : T true | C874 : T true
+| C875 : T true | C876 : T true | C877 : T true | C878 : T true | C879 : T true
+| C880 : T true | C881 : T true | C882 : T true | C883 : T true | C884 : T true
+| C885 : T true | C886 : T true | C887 : T true | C888 : T true | C889 : T true
+| C890 : T true | C891 : T true | C892 : T true | C893 : T true | C894 : T true
+| C895 : T true | C896 : T true | C897 : T true | C898 : T true | C899 : T true
+| C900 : T true | C901 : T true | C902 : T true | C903 : T true | C904 : T true
+| C905 : T true | C906 : T true | C907 : T true | C908 : T true | C909 : T true
+| C910 : T true | C911 : T true | C912 : T true | C913 : T true | C914 : T true
+| C915 : T true | C916 : T true | C917 : T true | C918 : T true | C919 : T true
+| C920 : T true | C921 : T true | C922 : T true | C923 : T true | C924 : T true
+| C925 : T true | C926 : T true | C927 : T true | C928 : T true | C929 : T true
+| C930 : T true | C931 : T true | C932 : T true | C933 : T true | C934 : T true
+| C935 : T true | C936 : T true | C937 : T true | C938 : T true | C939 : T true
+| C940 : T true | C941 : T true | C942 : T true | C943 : T true | C944 : T true
+| C945 : T true | C946 : T true | C947 : T true | C948 : T true | C949 : T true
+| C950 : T true | C951 : T true | C952 : T true | C953 : T true | C954 : T true
+| C955 : T true | C956 : T true | C957 : T true | C958 : T true | C959 : T true
+| C960 : T true | C961 : T true | C962 : T true | C963 : T true | C964 : T true
+| C965 : T true | C966 : T true | C967 : T true | C968 : T true | C969 : T true
+| C970 : T true | C971 : T true | C972 : T true | C973 : T true | C974 : T true
+| C975 : T true | C976 : T true | C977 : T true | C978 : T true | C979 : T true
+| C980 : T true | C981 : T true | C982 : T true | C983 : T true | C984 : T true
+| C985 : T true | C986 : T true | C987 : T true | C988 : T true | C989 : T true
+| C990 : T true | C991 : T true | C992 : T true | C993 : T true | C994 : T true
+| C995 : T true | C996 : T true | C997 : T true | C998 : T true | C999 : T true
+| C1000 : T false.
+
+Fixpoint expand (n : nat) : Prop :=
+  match n with
+  | O => T false
+  | S n => expand n
+  end.
+
+Example Expand : expand 2500.
+Time constructor. (* ~0.45 secs *)