Separate vernac controls and regular commands.

Virtually all classifications of vernacular commands (the STM
classifier, "filtered commands", "navigation commands", etc.) were
broken in presence of control vernaculars like Time, Timeout, Fail.

Funny examples of bugs include Time Abort All in coqtop or Time Set Ltac
Debug in CoqIDE.

This change introduces a type separation between vernacular controls and
vernacular commands, together with an "under_control" combinator.

1 files changed, 35 insertions, 39 deletions

diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index c5ae27a11..1291b7642 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -8,6 +8,7 @@
 
 open Vernacexpr
 open CErrors
+open Util
 open Pp
 
 let default_proof_mode () = Proof_global.get_default_proof_mode_name () [@ocaml.warning "-3"]
@@ -47,36 +48,18 @@ let declare_vernac_classifier
 =
   classifiers := !classifiers @ [s,f]
 
-let make_polymorphic (a, b as x) =
-  match a with
-  | VtStartProof (x, _, ids) ->
-      VtStartProof (x, Doesn'tGuaranteeOpacity, ids), b
-  | _ -> x
-
-let rec classify_vernac e =
-  let static_classifier e = match e with
+let classify_vernac e =
+  let rec static_classifier ~poly e = match e with
     (* Univ poly compatibility: we run it now, so that we can just
      * look at Flags in stm.ml.  Would be nicer to have the stm
      * look at the entire dag to detect this option. *)
-    | VernacSetOption (["Universe"; "Polymorphism"],_)
-    | VernacUnsetOption (["Universe"; "Polymorphism"]) -> VtSideff [], VtNow
+    | ( VernacSetOption (l,_) | VernacUnsetOption l)
+      when CList.equal String.equal l Vernacentries.universe_polymorphism_option_name ->
+       VtSideff [], VtNow
     (* Nested vernac exprs *)
-    | VernacProgram e -> classify_vernac e
-    | VernacLocal (_,e) -> classify_vernac e
-    | VernacPolymorphic (b, e) -> 
-      if b || Flags.is_universe_polymorphism () (* Ok or not? *) then
-	make_polymorphic (classify_vernac e)
-      else classify_vernac e
-    | VernacTimeout (_,e) -> classify_vernac e
-    | VernacTime (_,e) | VernacRedirect (_, (_,e)) -> classify_vernac e
-    | VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *)
-        (match classify_vernac e with
-        | ( VtQuery _ | VtProofStep _ | VtSideff _
-          | VtProofMode _ | VtMeta), _ as x -> x
-        | VtQed _, _ ->
-            VtProofStep { parallel = `No; proof_block_detection = None },
-            VtNow
-        | (VtStartProof _ | VtUnknown), _ -> VtUnknown, VtNow)
+    | VernacProgram e -> static_classifier ~poly e
+    | VernacLocal (_,e) -> static_classifier ~poly e
+    | VernacPolymorphic (b, e) -> static_classifier ~poly:b e
     (* Qed *)
     | VernacAbort _ -> VtQed VtDrop, VtLater
     | VernacEndProof Admitted -> VtQed VtKeepAsAxiom, VtLater
@@ -106,17 +89,20 @@ let rec classify_vernac e =
     | VernacDefinition ((Decl_kinds.DoDischarge,_),((_,i),_),ProveBody _) ->
         VtStartProof(default_proof_mode (),Doesn'tGuaranteeOpacity,[i]), VtLater
     | VernacDefinition (_,((_,i),_),ProveBody _) ->
-        VtStartProof(default_proof_mode (),GuaranteesOpacity,[i]), VtLater
+       let guarantee = if poly then Doesn'tGuaranteeOpacity else GuaranteesOpacity in
+        VtStartProof(default_proof_mode (),guarantee,[i]), VtLater
     | VernacStartTheoremProof (_,l) ->
         let ids = 
           CList.map_filter (function (Some ((_,i),pl), _) -> Some i | _ -> None) l in
-        VtStartProof (default_proof_mode (),GuaranteesOpacity,ids), VtLater
-    | VernacGoal _ -> VtStartProof (default_proof_mode (),GuaranteesOpacity,[]), VtLater
+       let guarantee = if poly then Doesn'tGuaranteeOpacity else GuaranteesOpacity in
+        VtStartProof (default_proof_mode (),guarantee,ids), VtLater
+    | VernacGoal _ ->
+       let guarantee = if poly then Doesn'tGuaranteeOpacity else GuaranteesOpacity in
+       VtStartProof (default_proof_mode (),guarantee,[]), VtLater
     | VernacFixpoint (discharge,l) ->
        let guarantee =
-         match discharge with
-         | Decl_kinds.NoDischarge -> GuaranteesOpacity
-         | Decl_kinds.DoDischarge -> Doesn'tGuaranteeOpacity
+         if discharge = Decl_kinds.DoDischarge || poly then Doesn'tGuaranteeOpacity
+         else GuaranteesOpacity
        in
         let ids, open_proof =
           List.fold_left (fun (l,b) ((((_,id),_),_,_,_,p),_) ->
@@ -126,9 +112,8 @@ let rec classify_vernac e =
         else VtSideff ids, VtLater
     | VernacCoFixpoint (discharge,l) ->
        let guarantee =
-         match discharge with
-         | Decl_kinds.NoDischarge -> GuaranteesOpacity
-         | Decl_kinds.DoDischarge -> Doesn'tGuaranteeOpacity
+         if discharge = Decl_kinds.DoDischarge || poly then Doesn'tGuaranteeOpacity
+         else GuaranteesOpacity
        in
         let ids, open_proof =
           List.fold_left (fun (l,b) ((((_,id),_),_,_,p),_) ->
@@ -207,10 +192,21 @@ let rec classify_vernac e =
         try List.assoc s !classifiers l ()
         with Not_found -> anomaly(str"No classifier for"++spc()++str (fst s)++str".")
   in
-  let res = static_classifier e in
-    if Flags.is_universe_polymorphism () then
-      make_polymorphic res
-    else res
+  let rec static_control_classifier ~poly = function
+    | VernacExpr e -> static_classifier ~poly e
+    | VernacTimeout (_,e) -> static_control_classifier ~poly e
+    | VernacTime (_,e) | VernacRedirect (_, (_,e)) ->
+       static_control_classifier ~poly e
+    | VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *)
+        (match static_control_classifier ~poly e with
+        | ( VtQuery _ | VtProofStep _ | VtSideff _
+          | VtProofMode _ | VtMeta), _ as x -> x
+        | VtQed _, _ ->
+            VtProofStep { parallel = `No; proof_block_detection = None },
+            VtNow
+        | (VtStartProof _ | VtUnknown), _ -> VtUnknown, VtNow)
+  in
+  static_control_classifier ~poly:(Flags.is_universe_polymorphism ()) e
 
 let classify_as_query = VtQuery (true,Feedback.default_route), VtLater
 let classify_as_sideeff = VtSideff [], VtLater