STM: encode in static types that vernac_when is only used when VtSideff

The stm.ml changes show that for the other classifications either the
vernac_when was ignored, or there was an assert on it forcing it to be
Now or Later depending on the vernac_type.

One may also note that the classification used in top_printers
`VtQuery,VtNow` would have failed those asserts...

2 files changed, 63 insertions, 71 deletions

diff --git a/stm/stm.ml b/stm/stm.ml
index 1e89d6937c..d77e37c910 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1563,7 +1563,7 @@ end = struct (* {{{ *)
   let perform_states query =
     if query = [] then [] else
     let is_tac e = match Vernac_classifier.classify_vernac e with
-    | VtProofStep _, _ -> true
+    | VtProofStep _ -> true
     | _ -> false
     in
     let initial =
@@ -2860,12 +2860,12 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ())
         "  classified as: " ^ Vernac_classifier.string_of_vernac_classification c);
       match c with
       (* Meta *)
-      | VtMeta, _ ->
+      | VtMeta ->
         let id = Backtrack.undo_vernac_classifier expr ~doc in
         process_back_meta_command ~newtip ~head id x
 
       (* Query *)
-      | VtQuery, w ->
+      | VtQuery ->
           let id = VCS.new_node ~id:newtip proof_mode () in
           let queue =
             if VCS.is_vio_doc () &&
@@ -2875,10 +2875,10 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ())
             else `MainQueue in
           VCS.commit id (mkTransCmd x [] false queue);
           VCS.set_parsing_state id head_parsing;
-          Backtrack.record (); assert (w == VtLater); `Ok
+          Backtrack.record (); `Ok
 
       (* Proof *)
-      | VtStartProof (guarantee, names), w ->
+      | VtStartProof (guarantee, names) ->
 
          if not (get_allow_nested_proofs ()) && VCS.proof_nesting () > 0 then
            "Nested proofs are not allowed unless you turn option Nested Proofs Allowed on."
@@ -2900,9 +2900,9 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ())
             VCS.merge id ~ours:(Fork (x, bname, guarantee, names)) head
           end;
           VCS.set_parsing_state id head_parsing;
-          Backtrack.record (); assert (w == VtLater); `Ok
+          Backtrack.record (); `Ok
 
-      | VtProofStep { parallel; proof_block_detection = cblock }, w ->
+      | VtProofStep { parallel; proof_block_detection = cblock } ->
           let id = VCS.new_node ~id:newtip proof_mode () in
           let queue =
             match parallel with
@@ -2914,18 +2914,18 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ())
              detection should occur here.
           detect_proof_block id cblock; *)
           VCS.set_parsing_state id head_parsing;
-          Backtrack.record (); assert (w == VtLater); `Ok
+          Backtrack.record (); `Ok
 
-      | VtQed keep, w ->
+      | VtQed keep ->
           let valid = VCS.get_branch_pos head in
           let rc =
             merge_proof_branch ~valid ~id:newtip x keep head in
           VCS.checkout_shallowest_proof_branch ();
-          Backtrack.record (); assert (w == VtLater);
+          Backtrack.record ();
           rc
 
       (* Side effect in a (still open) proof is replayed on all branches*)
-      | VtSideff l, w ->
+      | VtSideff (l, w) ->
           let id = VCS.new_node ~id:newtip proof_mode () in
           let new_ids =
             match (VCS.get_branch head).VCS.kind with
@@ -2961,15 +2961,13 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ())
               VCS.set_parsing_state id parsing_state) new_ids;
           `Ok
 
-      | VtProofMode pm, VtNow ->
+      | VtProofMode pm ->
         let proof_mode = Pvernac.lookup_proof_mode pm in
         let id = VCS.new_node ~id:newtip proof_mode () in
         VCS.commit id (mkTransCmd x [] false `MainQueue);
         VCS.set_parsing_state id head_parsing;
         Backtrack.record (); `Ok
 
-      | VtProofMode _, VtLater ->
-          anomaly(str"classifier: VtProofMode must imply VtNow.")
     end in
     let pr_rc rc = match rc with
       | `Ok -> Pp.(seq [str "newtip ("; str (Stateid.to_string (VCS.cur_tip ())); str ")"])
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index aa16f9535d..cfeca1fa62 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -20,9 +20,13 @@ let string_of_parallel = function
        "par" ^ if solve then "solve" else "" ^ if abs then "abs" else ""
   | `No -> ""
 
-let string_of_vernac_type = function
+let string_of_vernac_when = function
+  | VtLater -> "Later"
+  | VtNow -> "Now"
+
+let string_of_vernac_classification = function
   | VtStartProof _ -> "StartProof"
-  | VtSideff _ -> "Sideff"
+  | VtSideff (_,w) -> "Sideff"^" "^(string_of_vernac_when w)
   | VtQed (VtKeep VtKeepAxiom) -> "Qed(admitted)"
   | VtQed (VtKeep (VtKeepOpaque | VtKeepDefined)) -> "Qed(keep)"
   | VtQed VtDrop -> "Qed(drop)"
@@ -33,13 +37,6 @@ let string_of_vernac_type = function
   | VtMeta -> "Meta "
   | VtProofMode _ -> "Proof Mode"
 
-let string_of_vernac_when = function
-  | VtLater -> "Later"
-  | VtNow -> "Now"
-
-let string_of_vernac_classification (t,w) =
-  string_of_vernac_type t ^ " " ^ string_of_vernac_when w
-
 let vtkeep_of_opaque = let open Proof_global in function
   | Opaque -> VtKeepOpaque
   | Transparent -> VtKeepDefined
@@ -67,15 +64,15 @@ let classify_vernac e =
     | VernacSetOption (_, l,_)
       when CList.exists (CList.equal String.equal l)
         options_affecting_stm_scheduling ->
-       VtSideff [], VtNow
+       VtSideff ([], VtNow)
     (* Qed *)
-    | VernacAbort _ -> VtQed VtDrop, VtLater
-    | VernacEndProof Admitted -> VtQed (VtKeep VtKeepAxiom), VtLater
-    | VernacEndProof (Proved (opaque,_)) -> VtQed (VtKeep (vtkeep_of_opaque opaque)), VtLater
-    | VernacExactProof _ -> VtQed (VtKeep VtKeepOpaque), VtLater
+    | VernacAbort _ -> VtQed VtDrop
+    | VernacEndProof Admitted -> VtQed (VtKeep VtKeepAxiom)
+    | VernacEndProof (Proved (opaque,_)) -> VtQed (VtKeep (vtkeep_of_opaque opaque))
+    | VernacExactProof _ -> VtQed (VtKeep VtKeepOpaque)
     (* Query *)
     | VernacShow _ | VernacPrint _ | VernacSearch _ | VernacLocate _
-    | VernacCheckMayEval _ -> VtQuery, VtLater
+    | VernacCheckMayEval _ -> VtQuery
     (* ProofStep *)
     | VernacProof _ 
     | VernacFocus _ | VernacUnfocus
@@ -83,27 +80,25 @@ let classify_vernac e =
     | VernacCheckGuard
     | VernacUnfocused
     | VernacSolveExistential _ ->
-        VtProofStep { parallel = `No; proof_block_detection = None }, VtLater
+        VtProofStep { parallel = `No; proof_block_detection = None }
     | VernacBullet _ ->
-        VtProofStep { parallel = `No; proof_block_detection = Some "bullet" },
-        VtLater
+        VtProofStep { parallel = `No; proof_block_detection = Some "bullet" }
     | VernacEndSubproof -> 
         VtProofStep { parallel = `No;
-                      proof_block_detection = Some "curly" },
-        VtLater
+                      proof_block_detection = Some "curly" }
     (* StartProof *)
     | VernacDefinition ((Decl_kinds.DoDischarge,_),({v=i},_),ProveBody _) ->
-      VtStartProof(Doesn'tGuaranteeOpacity, idents_of_name i), VtLater
+      VtStartProof(Doesn'tGuaranteeOpacity, idents_of_name i)
 
     | VernacDefinition (_,({v=i},_),ProveBody _) ->
       let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in
       let guarantee = if polymorphic then Doesn'tGuaranteeOpacity else GuaranteesOpacity in
-      VtStartProof(guarantee, idents_of_name i), VtLater
+      VtStartProof(guarantee, idents_of_name i)
     | VernacStartTheoremProof (_,l) ->
       let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in
       let ids = List.map (fun (({v=i}, _), _) -> i) l in
       let guarantee = if polymorphic then Doesn'tGuaranteeOpacity else GuaranteesOpacity in
-      VtStartProof (guarantee,ids), VtLater
+      VtStartProof (guarantee,ids)
     | VernacFixpoint (discharge,l) ->
       let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in
        let guarantee =
@@ -114,8 +109,8 @@ let classify_vernac e =
           List.fold_left (fun (l,b) ((({v=id},_),_,_,_,p),_) ->
             id::l, b || p = None) ([],false) l in
         if open_proof
-        then VtStartProof (guarantee,ids), VtLater
-        else VtSideff ids, VtLater
+        then VtStartProof (guarantee,ids)
+        else VtSideff (ids, VtLater)
     | VernacCoFixpoint (discharge,l) ->
       let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in
        let guarantee =
@@ -126,15 +121,15 @@ let classify_vernac e =
           List.fold_left (fun (l,b) ((({v=id},_),_,_,p),_) ->
             id::l, b || p = None) ([],false) l in
         if open_proof
-        then VtStartProof (guarantee,ids), VtLater
-        else VtSideff ids, VtLater
+        then VtStartProof (guarantee,ids)
+        else VtSideff (ids, VtLater)
     (* Sideff: apply to all open branches. usually run on master only *)
     | VernacAssumption (_,_,l) ->
         let ids = List.flatten (List.map (fun (_,(l,_)) -> List.map (fun (id, _) -> id.v) l) l) in
-        VtSideff ids, VtLater
+        VtSideff (ids, VtLater)
     | VernacPrimitive (id,_,_) ->
-        VtSideff [id.CAst.v], VtLater
-    | VernacDefinition (_,({v=id},_),DefineBody _) -> VtSideff (idents_of_name id), VtLater
+        VtSideff ([id.CAst.v], VtLater)
+    | VernacDefinition (_,({v=id},_),DefineBody _) -> VtSideff (idents_of_name id, VtLater)
     | VernacInductive (_, _,_,l) ->
         let ids = List.map (fun (((_,({v=id},_)),_,_,_,cl),_) -> id :: match cl with
         | Constructors l -> List.map (fun (_,({v=id},_)) -> id) l
@@ -142,12 +137,12 @@ let classify_vernac e =
            CList.map_filter (function
             | AssumExpr({v=Names.Name n},_), _ -> Some n
             | _ -> None) l) l in
-        VtSideff (List.flatten ids), VtLater
+        VtSideff (List.flatten ids, VtLater)
     | VernacScheme l ->
         let ids = List.map (fun {v}->v) (CList.map_filter (fun (x,_) -> x) l) in
-        VtSideff ids, VtLater
-    | VernacCombinedScheme ({v=id},_) -> VtSideff [id], VtLater
-    | VernacBeginSection {v=id} -> VtSideff [id], VtLater
+        VtSideff (ids, VtLater)
+    | VernacCombinedScheme ({v=id},_) -> VtSideff ([id], VtLater)
+    | VernacBeginSection {v=id} -> VtSideff ([id], VtLater)
     | VernacUniverse _ | VernacConstraint _
     | VernacCanonical _ | VernacCoercion _ | VernacIdentityCoercion _
     | VernacAddLoadPath _ | VernacRemoveLoadPath _ | VernacAddMLPath _
@@ -166,17 +161,17 @@ let classify_vernac e =
     | VernacRegister _
     | VernacNameSectionHypSet _
     | VernacComments _
-    | VernacDeclareInstance _ -> VtSideff [], VtLater
+    | VernacDeclareInstance _ -> VtSideff ([], VtLater)
     (* Who knows *)
-    | VernacLoad _ -> VtSideff [], VtNow
+    | VernacLoad _ -> VtSideff ([], VtNow)
     (* (Local) Notations have to disappear *)
-    | VernacEndSegment _ -> VtSideff [], VtNow
+    | VernacEndSegment _ -> VtSideff ([], VtNow)
     (* Modules with parameters have to be executed: can import notations *)
     | VernacDeclareModule (exp,{v=id},bl,_)
     | VernacDefineModule (exp,{v=id},bl,_,_) ->
-        VtSideff [id], if bl = [] && exp = None then VtLater else VtNow
+        VtSideff ([id], if bl = [] && exp = None then VtLater else VtNow)
     | VernacDeclareModuleType ({v=id},bl,_,_) ->
-        VtSideff [id], if bl = [] then VtLater else VtNow
+        VtSideff ([id], if bl = [] then VtLater else VtNow)
     (* These commands alter the parser *)
     | VernacDeclareCustomEntry _
     | VernacOpenCloseScope _ | VernacDeclareScope _
@@ -186,40 +181,39 @@ let classify_vernac e =
     | VernacSyntacticDefinition _
     | VernacRequire _ | VernacImport _ | VernacInclude _
     | VernacDeclareMLModule _
-    | VernacContext _ (* TASSI: unsure *) -> VtSideff [], VtNow
-    | VernacProofMode pm -> VtProofMode pm, VtNow
+    | VernacContext _ (* TASSI: unsure *) -> VtSideff ([], VtNow)
+    | VernacProofMode pm -> VtProofMode pm
     | VernacInstance ((name,_),_,_,None,_) when not (Attributes.parse_drop_extra Attributes.program atts) ->
       let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in
       let guarantee = if polymorphic then Doesn'tGuaranteeOpacity else GuaranteesOpacity in
-      VtStartProof (guarantee, idents_of_name name.CAst.v), VtLater
+      VtStartProof (guarantee, idents_of_name name.CAst.v)
     | VernacInstance ((name,_),_,_,_,_) ->
-      VtSideff (idents_of_name name.CAst.v), VtLater
+      VtSideff (idents_of_name name.CAst.v, VtLater)
     (* Stm will install a new classifier to handle these *)
     | VernacBack _ | VernacAbortAll
     | VernacUndoTo _ | VernacUndo _
     | VernacResetName _ | VernacResetInitial
-    | VernacBackTo _ | VernacRestart -> VtMeta, VtNow
+    | VernacBackTo _ | VernacRestart -> VtMeta
     (* What are these? *)
     | VernacRestoreState _
-    | VernacWriteState _ -> VtSideff [], VtNow
+    | VernacWriteState _ -> VtSideff ([], VtNow)
     (* Plugins should classify their commands *)
     | VernacExtend (s,l) ->
         try Vernacextend.get_vernac_classifier s l
         with Not_found -> anomaly(str"No classifier for"++spc()++str (fst s)++str".")
   in
   let rec static_control_classifier v = v |> CAst.with_val (function
-    | VernacExpr (atts, e) ->
-      static_classifier ~atts e
-    | VernacTimeout (_,e) -> static_control_classifier e
-    | VernacTime (_,e) | VernacRedirect (_, e) ->
-       static_control_classifier e
-    | VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *)
+      | VernacExpr (atts, e) ->
+        static_classifier ~atts e
+      | VernacTimeout (_,e) -> static_control_classifier e
+      | VernacTime (_,e) | VernacRedirect (_, e) ->
+        static_control_classifier e
+      | VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *)
+        (* XXX why is Fail not always Query? *)
         (match static_control_classifier e with
-        | ( VtQuery | VtProofStep _ | VtSideff _
-          | VtMeta), _ as x -> x
-        | VtQed _, _ ->
-            VtProofStep { parallel = `No; proof_block_detection = None },
-            VtLater
-        | (VtStartProof _ | VtProofMode _), _ -> VtQuery, VtLater))
+         | VtQuery | VtProofStep _ | VtSideff _
+         | VtMeta as x -> x
+         | VtQed _ -> VtProofStep { parallel = `No; proof_block_detection = None }
+         | VtStartProof _ | VtProofMode _ -> VtQuery))
   in
   static_control_classifier e