Merge PR #9530: Remove `VtUnkown` classification

Reviewed-by: JasonGross
Reviewed-by: SkySkimmer

2 files changed, 22 insertions, 65 deletions

diff --git a/stm/stm.ml b/stm/stm.ml
index 21618bc044..6f7cefb582 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -364,7 +364,6 @@ module VCS : sig
   val set_parsing_state : id -> Vernacstate.Parser.state -> unit
   val get_parsing_state : id -> Vernacstate.Parser.state option
   val get_proof_mode : id -> Pvernac.proof_mode option
-  val set_proof_mode : id -> Pvernac.proof_mode option -> unit
 
   (* cuts from start -> stop, raising Expired if some nodes are not there *)
   val slice : block_start:id -> block_stop:id -> vcs
@@ -572,6 +571,7 @@ end = struct (* {{{ *)
     (match Vernacprop.under_control x with
     | VernacDefinition (_,({CAst.v=Name i},_),_) -> Id.to_string i
     | VernacStartTheoremProof (_,[({CAst.v=i},_),_]) -> Id.to_string i
+    | VernacInstance (_,(({CAst.v=Name i},_),_,_),_,_) -> Id.to_string i
     | _ -> "branch")
   let edit_branch = Branch.make "edit"
   let branch ?root ?pos name kind = vcs := branch !vcs ?root ?pos name kind
@@ -611,7 +611,6 @@ end = struct (* {{{ *)
     info.state <- new_state
 
   let get_proof_mode id = (get_info id).proof_mode
-  let set_proof_mode id pm = (get_info id).proof_mode <- pm
 
   let reached id =
     let info = get_info id in
@@ -3050,53 +3049,6 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ())
               VCS.set_parsing_state id parsing_state) new_ids;
           `Ok
 
-      (* Unknown: we execute it, check for open goals and propagate sideeff *)
-      | VtUnknown, VtNow ->
-          let in_proof = not (VCS.Branch.equal head VCS.Branch.master) in
-          if not (get_allow_nested_proofs ()) && in_proof then
-            "Commands which may open proofs are not allowed in a proof unless you turn option Nested Proofs Allowed on."
-            |> Pp.str
-            |> (fun s -> (UserError (None, s), Exninfo.null))
-            |> State.exn_on ~valid:Stateid.dummy newtip
-            |> Exninfo.iraise
-          else
-            let id = VCS.new_node ~id:newtip proof_mode () in
-          let head_id = VCS.get_branch_pos head in
-          let _st : unit = Reach.known_state ~doc ~cache:true head_id in (* ensure it is ok *)
-          let step () =
-            VCS.checkout VCS.Branch.master;
-            let mid = VCS.get_branch_pos VCS.Branch.master in
-            let _st' : unit = Reach.known_state ~doc ~cache:(VCS.is_interactive ()) mid in
-            let st = Vernacstate.freeze_interp_state ~marshallable:false in
-            ignore(stm_vernac_interp id st x);
-            (* Vernac x may or may not start a proof *)
-            if not in_proof && PG_compat.there_are_pending_proofs () then
-            begin
-              let bname = VCS.mk_branch_name x in
-              let opacity_of_produced_term = function
-                (* This AST is ambiguous, hence we check it dynamically *)
-                | VernacInstance (_,_ , None, _) -> GuaranteesOpacity
-                | _ -> Doesn'tGuaranteeOpacity in
-              VCS.commit id (Fork (x,bname,opacity_of_produced_term (Vernacprop.under_control x.expr),[]));
-              VCS.set_proof_mode id (Some (Vernacentries.get_default_proof_mode ()));
-              VCS.branch bname (`Proof (VCS.proof_nesting () + 1));
-            end else begin
-              begin match (VCS.get_branch head).VCS.kind with
-              | `Edit _ -> VCS.commit id (mkTransCmd x [] in_proof `MainQueue);
-              | `Master -> VCS.commit id (mkTransCmd x [] in_proof `MainQueue);
-              | `Proof _ ->
-                  VCS.commit id (mkTransCmd x [] in_proof `MainQueue);
-                  (* We hope it can be replayed, but we can't really know *)
-                  ignore(VCS.propagate_sideff ~action:(ReplayCommand x));
-              end;
-              VCS.checkout_shallowest_proof_branch ();
-            end in
-          State.define ~doc ~safe_id:head_id ~cache:true step id;
-          Backtrack.record (); `Ok
-
-      | VtUnknown, VtLater ->
-          anomaly(str"classifier: VtUnknown must imply VtNow.")
-
       | VtProofMode pm, VtNow ->
         let proof_mode = Pvernac.lookup_proof_mode pm in
         let id = VCS.new_node ~id:newtip proof_mode () in
@@ -3106,7 +3058,6 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ())
 
       | 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 4a4c5c94e9..7cecd801e4 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -21,7 +21,6 @@ let string_of_parallel = function
   | `No -> ""
 
 let string_of_vernac_type = function
-  | VtUnknown -> "Unknown"
   | VtStartProof _ -> "StartProof"
   | VtSideff _ -> "Sideff"
   | VtQed (VtKeep VtKeepAxiom) -> "Qed(admitted)"
@@ -61,7 +60,7 @@ let options_affecting_stm_scheduling =
   ]
 
 let classify_vernac e =
-  let static_classifier ~poly e = match e with
+  let static_classifier ~atts 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. *)
@@ -97,15 +96,18 @@ let classify_vernac e =
       VtStartProof(Doesn'tGuaranteeOpacity, idents_of_name i), VtLater
 
     | VernacDefinition (_,({v=i},_),ProveBody _) ->
-       let guarantee = if poly then Doesn'tGuaranteeOpacity else GuaranteesOpacity in
-        VtStartProof(guarantee, idents_of_name i), VtLater
+      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
     | VernacStartTheoremProof (_,l) ->
-        let ids = List.map (fun (({v=i}, _), _) -> i) l in
-       let guarantee = if poly then Doesn'tGuaranteeOpacity else GuaranteesOpacity in
-        VtStartProof (guarantee,ids), VtLater
+      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
     | VernacFixpoint (discharge,l) ->
+      let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in
        let guarantee =
-         if discharge = Decl_kinds.DoDischarge || poly then Doesn'tGuaranteeOpacity
+         if discharge = Decl_kinds.DoDischarge || polymorphic then Doesn'tGuaranteeOpacity
          else GuaranteesOpacity
        in
         let ids, open_proof =
@@ -115,8 +117,9 @@ let classify_vernac e =
         then VtStartProof (guarantee,ids), VtLater
         else VtSideff ids, VtLater
     | VernacCoFixpoint (discharge,l) ->
+      let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in
        let guarantee =
-         if discharge = Decl_kinds.DoDischarge || poly then Doesn'tGuaranteeOpacity
+         if discharge = Decl_kinds.DoDischarge || polymorphic then Doesn'tGuaranteeOpacity
          else GuaranteesOpacity
        in
         let ids, open_proof =
@@ -185,8 +188,12 @@ let classify_vernac e =
     | VernacDeclareMLModule _
     | VernacContext _ (* TASSI: unsure *) -> VtSideff [], VtNow
     | VernacProofMode pm -> VtProofMode pm, VtNow
-    (* These are ambiguous *)
-    | VernacInstance _ -> VtUnknown, VtNow
+    | 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
+    | VernacInstance (_,((name,_),_,_),_,_) ->
+      VtSideff (idents_of_name name.CAst.v), VtLater
     (* Stm will install a new classifier to handle these *)
     | VernacBack _ | VernacAbortAll
     | VernacUndoTo _ | VernacUndo _
@@ -201,9 +208,8 @@ let classify_vernac e =
         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 (f, e) ->
-      let poly = Attributes.(parse_drop_extra polymorphic_nowarn f) in
-      static_classifier ~poly e
+    | VernacExpr (atts, e) ->
+      static_classifier ~atts e
     | VernacTimeout (_,e) -> static_control_classifier e
     | VernacTime (_,e) | VernacRedirect (_, e) ->
        static_control_classifier e
@@ -214,6 +220,6 @@ let classify_vernac e =
         | VtQed _, _ ->
             VtProofStep { parallel = `No; proof_block_detection = None },
             VtLater
-        | (VtStartProof _ | VtUnknown | VtProofMode _), _ -> VtQuery, VtLater))
+        | (VtStartProof _ | VtProofMode _), _ -> VtQuery, VtLater))
   in
   static_control_classifier e