Merge PR #13418: [sysinit] new component

Reviewed-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: JasonGross

3 files changed, 235 insertions, 0 deletions

diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib
index cd0dd5e9a6..007a3b05fc 100644
--- a/vernac/vernac.mllib
+++ b/vernac/vernac.mllib
@@ -45,3 +45,4 @@ ComArguments
 Vernacentries
 ComTactic
 Vernacinterp
+Vernac_classifier
diff --git a/vernac/vernac_classifier.ml b/vernac/vernac_classifier.ml
new file mode 100644
index 0000000000..ffae2866c0
--- /dev/null
+++ b/vernac/vernac_classifier.ml
@@ -0,0 +1,215 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open CErrors
+open Util
+open Pp
+open CAst
+open Vernacextend
+open Vernacexpr
+
+let string_of_vernac_when = function
+  | VtLater -> "Later"
+  | VtNow -> "Now"
+
+let string_of_vernac_classification = function
+  | VtStartProof _ -> "StartProof"
+  | VtSideff (_,w) -> "Sideff"^" "^(string_of_vernac_when w)
+  | VtQed (VtKeep VtKeepAxiom) -> "Qed(admitted)"
+  | VtQed (VtKeep (VtKeepOpaque | VtKeepDefined)) -> "Qed(keep)"
+  | VtQed VtDrop -> "Qed(drop)"
+  | VtProofStep {  proof_block_detection } ->
+      "ProofStep " ^ Option.default "" proof_block_detection
+  | VtQuery -> "Query"
+  | VtMeta -> "Meta "
+  | VtProofMode _ -> "Proof Mode"
+
+let vtkeep_of_opaque = function
+  | Opaque -> VtKeepOpaque
+  | Transparent -> VtKeepDefined
+
+let idents_of_name : Names.Name.t -> Names.Id.t list =
+  function
+  | Names.Anonymous -> []
+  | Names.Name n -> [n]
+
+let stm_allow_nested_proofs_option_name = ["Nested";"Proofs";"Allowed"]
+
+let options_affecting_stm_scheduling =
+  [ Attributes.universe_polymorphism_option_name;
+    stm_allow_nested_proofs_option_name;
+    Vernacinterp.proof_mode_opt_name;
+    Attributes.program_mode_option_name;
+    Proof_using.proof_using_opt_name;
+  ]
+
+let classify_vernac e =
+  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. *)
+    | VernacSetOption (_, l,_)
+      when CList.exists (CList.equal String.equal l)
+        options_affecting_stm_scheduling ->
+       VtSideff ([], VtNow)
+    (* Qed *)
+    | 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
+    (* ProofStep *)
+    | VernacProof _
+    | VernacFocus _ | VernacUnfocus
+    | VernacSubproof _
+    | VernacCheckGuard
+    | VernacUnfocused
+    | VernacSolveExistential _ ->
+        VtProofStep { proof_block_detection = None }
+    | VernacBullet _ ->
+        VtProofStep { proof_block_detection = Some "bullet" }
+    | VernacEndSubproof ->
+        VtProofStep { proof_block_detection = Some "curly" }
+    (* StartProof *)
+    | VernacDefinition ((DoDischarge,_),({v=i},_),ProveBody _) ->
+      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)
+    | 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)
+    | VernacFixpoint (discharge,l) ->
+      let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in
+       let guarantee =
+         if discharge = DoDischarge || polymorphic then Doesn'tGuaranteeOpacity
+         else GuaranteesOpacity
+       in
+        let ids, open_proof =
+          List.fold_left (fun (l,b) {Vernacexpr.fname={CAst.v=id}; body_def} ->
+            id::l, b || body_def = None) ([],false) l in
+        if open_proof
+        then VtStartProof (guarantee,ids)
+        else VtSideff (ids, VtLater)
+    | VernacCoFixpoint (discharge,l) ->
+      let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in
+       let guarantee =
+         if discharge = DoDischarge || polymorphic then Doesn'tGuaranteeOpacity
+         else GuaranteesOpacity
+       in
+        let ids, open_proof =
+          List.fold_left (fun (l,b) { Vernacexpr.fname={CAst.v=id}; body_def } ->
+            id::l, b || body_def = None) ([],false) l in
+        if open_proof
+        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)
+    | VernacPrimitive ((id,_),_,_) ->
+        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
+        | RecordDecl (oid,l) -> (match oid with Some {v=x} -> [x] | _ -> []) @
+           CList.map_filter (function
+            | AssumExpr({v=Names.Name n},_,_), _ -> Some n
+            | _ -> None) l) l in
+        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)
+    | VernacUniverse _ | VernacConstraint _
+    | VernacCanonical _ | VernacCoercion _ | VernacIdentityCoercion _
+    | VernacAddLoadPath _ | VernacRemoveLoadPath _ | VernacAddMLPath _
+    | VernacChdir _
+    | VernacCreateHintDb _ | VernacRemoveHints _ | VernacHints _
+    | VernacArguments _
+    | VernacReserve _
+    | VernacGeneralizable _
+    | VernacSetOpacity _ | VernacSetStrategy _
+    | VernacSetOption _
+    | VernacAddOption _ | VernacRemoveOption _
+    | VernacMemOption _ | VernacPrintOption _
+    | VernacGlobalCheck _
+    | VernacDeclareReduction _
+    | VernacExistingClass _ | VernacExistingInstance _
+    | VernacRegister _
+    | VernacNameSectionHypSet _
+    | VernacComments _
+    | VernacDeclareInstance _ -> VtSideff ([], VtLater)
+    (* Who knows *)
+    | VernacLoad _ -> VtSideff ([], VtNow)
+    (* (Local) Notations have to disappear *)
+    | 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)
+    | VernacDeclareModuleType ({v=id},bl,_,_) ->
+        VtSideff ([id], if bl = [] then VtLater else VtNow)
+    (* These commands alter the parser *)
+    | VernacDeclareCustomEntry _
+    | VernacOpenCloseScope _ | VernacDeclareScope _
+    | VernacDelimiters _ | VernacBindScope _
+    | VernacInfix _ | VernacNotation _ | VernacNotationAddFormat _
+    | VernacSyntaxExtension _
+    | VernacSyntacticDefinition _
+    | VernacRequire _ | VernacImport _ | VernacInclude _
+    | VernacDeclareMLModule _
+    | VernacContext _ (* TASSI: unsure *) -> VtSideff ([], VtNow)
+    | VernacProofMode pm -> VtProofMode pm
+    | VernacInstance ((name,_),_,_,props,_) ->
+      let program, refine =
+        Attributes.(parse_drop_extra Notations.(program ++ Classes.refine_att) atts)
+      in
+      if program || (props <> None && not refine) then
+        VtSideff (idents_of_name name.CAst.v, VtLater)
+      else
+        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)
+    (* Stm will install a new classifier to handle these *)
+    | VernacBack _ | VernacAbortAll
+    | VernacUndoTo _ | VernacUndo _
+    | VernacResetName _ | VernacResetInitial
+    | VernacRestart -> VtMeta
+    (* What are these? *)
+    | VernacRestoreState _
+    | 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 static_control_classifier ({ CAst.v ; _ } as cmd) =
+    (* Fail Qed or Fail Lemma must not join/fork the DAG *)
+    (* XXX why is Fail not always Query? *)
+    if Vernacprop.has_Fail cmd then
+      (match static_classifier ~atts:v.attrs v.expr with
+         | VtQuery | VtProofStep _ | VtSideff _
+         | VtMeta as x -> x
+         | VtQed _ -> VtProofStep { proof_block_detection = None }
+         | VtStartProof _ | VtProofMode _ -> VtQuery)
+    else
+      static_classifier ~atts:v.attrs v.expr
+
+  in
+  static_control_classifier e
diff --git a/vernac/vernac_classifier.mli b/vernac/vernac_classifier.mli
new file mode 100644
index 0000000000..61bf3a503a
--- /dev/null
+++ b/vernac/vernac_classifier.mli
@@ -0,0 +1,19 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Vernacextend
+
+val string_of_vernac_classification : vernac_classification -> string
+
+(** What does a vernacular do *)
+val classify_vernac : Vernacexpr.vernac_control -> vernac_classification
+
+(**  *)
+val stm_allow_nested_proofs_option_name : string list