From c78de8b5456fdaf2067b6b2d5c128923b4cda7fc Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Thu, 12 Oct 2017 12:21:36 +0200
Subject: [stm] Remove all but one use of VtUnknown.

Together with #1122, this makes `VernacInstance` the only command in
the Coq codebase that cannot be statically determined to open a proof.

The reasoning for the commands moved to `VtSideff` is that
parser-altering commands should be always marked `VtNow`; the rest can
be usually marked as `VtLater`.
---
 grammar/vernacextend.mlp |  2 +-
 intf/vernacexpr.ml       | 29 +++++++++++++++++++++++++----
 plugins/ltac/g_ltac.ml4  |  2 +-
 stm/vernac_classifier.ml |  6 +++---
 4 files changed, 30 insertions(+), 9 deletions(-)

diff --git a/grammar/vernacextend.mlp b/grammar/vernacextend.mlp
index f6f46710c..a561ea370 100644
--- a/grammar/vernacextend.mlp
+++ b/grammar/vernacextend.mlp
@@ -82,7 +82,7 @@ let make_clause_classifier cg s { r_patt = pt; r_class = c; } =
          "classifiers. Only one classifier is called.") ^ "\n");
     (make_patt pt,
       ploc_vala None,
-      <:expr< fun loc -> (Vernacexpr.VtUnknown, Vernacexpr.VtNow) >>)
+      <:expr< fun () -> ( CErrors.anomaly (Pp.str "No classification given for command " ^ s ) ) >>)
 
 let make_fun_clauses loc s l =
   let map c =
diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml
index 5c9141fd6..3f3ade724 100644
--- a/intf/vernacexpr.ml
+++ b/intf/vernacexpr.ml
@@ -482,18 +482,39 @@ and vernac_argument_status = {
   implicit_status : vernac_implicit_status;
 }
 
-(* A vernac classifier has to tell if a command:
-   vernac_when: has to be executed now (alters the parser) or later
-   vernac_type: if it is starts, ends, continues a proof or
+(* A vernac classifier provides information about the exectuion of a
+   command:
+
+   - vernac_when: encodes if the vernac may alter the parser [thus
+     forcing immediate execution], or if indeed it is pure and parsing
+     can continue without its execution.
+
+   - vernac_type: if it is starts, ends, continues a proof or
      alters the global state or is a control command like BackTo or is
-     a query like Check *)
+     a query like Check.
+
+   The classification works on the assumption that we have 3 states:
+   parsing, execution (global enviroment, etc...), and proof
+   state. For example, commands that only alter the proof state are
+   considered safe to delegate to a worker.
+
+*)
 type vernac_type =
+  (* Start of a proof *)
   | VtStartProof of vernac_start
+  (* Command altering the global state, bad for parallel
+     processing. *)
   | VtSideff of vernac_sideff_type
+  (* End of a proof *)
   | VtQed of vernac_qed_type
+  (* A proof step *)
   | VtProofStep of proof_step
+  (* To be removed *)
   | VtProofMode of string
+  (* Queries are commands assumed to be "pure", that is to say, they
+     don't modify the interpretation state. *)
   | VtQuery of vernac_part_of_script * Feedback.route_id
+  (* To be removed *)
   | VtMeta
   | VtUnknown
 and vernac_qed_type = VtKeep | VtKeepAsAxiom | VtDrop (* Qed/Admitted, Abort *)
diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index 34fea6175..8b9eb3983 100644
--- a/plugins/ltac/g_ltac.ml4
+++ b/plugins/ltac/g_ltac.ml4
@@ -471,7 +471,7 @@ END
 
 VERNAC COMMAND FUNCTIONAL EXTEND VernacTacticNotation
 | [ "Tactic" "Notation" ltac_tactic_level_opt(n) ne_ltac_production_item_list(r) ":=" tactic(e) ] =>
-  [ VtUnknown, VtNow ] ->
+  [ VtSideff [], VtNow ] ->
   [ fun ~atts ~st -> let open Vernacinterp in
       let n = Option.default 0 n in
       Tacentries.add_tactic_notation (Locality.make_module_locality atts.locality) n r e;
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 1ca572a36..c5ae27a11 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -185,12 +185,12 @@ let rec classify_vernac e =
     (* These commands alter the parser *)
     | VernacOpenCloseScope _ | VernacDelimiters _ | VernacBindScope _
     | VernacInfix _ | VernacNotation _ | VernacNotationAddFormat _
-    | VernacSyntaxExtension _ 
+    | VernacSyntaxExtension _
     | VernacSyntacticDefinition _
     | VernacRequire _ | VernacImport _ | VernacInclude _
     | VernacDeclareMLModule _
     | VernacContext _ (* TASSI: unsure *)
-    | VernacProofMode _ 
+    | VernacProofMode _ -> VtSideff [], VtNow
     (* These are ambiguous *)
     | VernacInstance _ -> VtUnknown, VtNow
     (* Stm will install a new classifier to handle these *)
@@ -201,7 +201,7 @@ let rec classify_vernac e =
     (* What are these? *)
     | VernacToplevelControl _
     | VernacRestoreState _
-    | VernacWriteState _ -> VtUnknown, VtNow
+    | VernacWriteState _ -> VtSideff [], VtNow
     (* Plugins should classify their commands *)
     | VernacExtend (s,l) ->
         try List.assoc s !classifiers l ()
-- 
cgit v1.2.3