diff options
Diffstat (limited to 'stm/vernac_classifier.ml')
| -rw-r--r-- | stm/vernac_classifier.ml | 41 |
1 files changed, 18 insertions, 23 deletions
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index f68c8b32..21704779 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -16,8 +16,6 @@ open Vernacexpr let default_proof_mode () = Proof_global.get_default_proof_mode_name () [@ocaml.warning "-3"] -let string_of_in_script b = if b then " (inside script)" else "" - let string_of_parallel = function | `Yes (solve,abs) -> "par" ^ if solve then "solve" else "" ^ if abs then "abs" else "" @@ -34,7 +32,7 @@ let string_of_vernac_type = function "ProofStep " ^ string_of_parallel parallel ^ Option.default "" proof_block_detection | VtProofMode s -> "ProofMode " ^ s - | VtQuery (b, route) -> "Query " ^ string_of_in_script b ^ " route " ^ string_of_int route + | VtQuery -> "Query" | VtMeta -> "Meta " let string_of_vernac_when = function @@ -44,25 +42,25 @@ let string_of_vernac_when = function let string_of_vernac_classification (t,w) = string_of_vernac_type t ^ " " ^ string_of_vernac_when w -let classifiers = ref [] -let declare_vernac_classifier - (s : Vernacexpr.extend_name) - (f : Genarg.raw_generic_argument list -> unit -> vernac_classification) -= - classifiers := !classifiers @ [s,f] - 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 = + [ Vernacentries.universe_polymorphism_option_name; + stm_allow_nested_proofs_option_name ] + let classify_vernac e = let 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 (_, l,_) | VernacUnsetOption (_, l)) - when CList.equal String.equal l Vernacentries.universe_polymorphism_option_name -> + when CList.exists (CList.equal String.equal l) + options_affecting_stm_scheduling -> VtSideff [], VtNow (* Qed *) | VernacAbort _ -> VtQed VtDrop, VtLater @@ -70,7 +68,7 @@ let classify_vernac e = | VernacEndProof _ | VernacExactProof _ -> VtQed VtKeep, VtLater (* Query *) | VernacShow _ | VernacPrint _ | VernacSearch _ | VernacLocate _ - | VernacCheckMayEval _ -> VtQuery (true,Feedback.default_route), VtLater + | VernacCheckMayEval _ -> VtQuery, VtLater (* ProofStep *) | VernacProof _ | VernacFocus _ | VernacUnfocus @@ -145,7 +143,7 @@ let classify_vernac e = | VernacAddLoadPath _ | VernacRemoveLoadPath _ | VernacAddMLPath _ | VernacChdir _ | VernacCreateHintDb _ | VernacRemoveHints _ | VernacHints _ - | VernacDeclareImplicits _ | VernacArguments _ | VernacArgumentsScope _ + | VernacArguments _ | VernacReserve _ | VernacGeneralizable _ | VernacSetOpacity _ | VernacSetStrategy _ @@ -157,6 +155,7 @@ let classify_vernac e = | VernacDeclareClass _ | VernacDeclareInstances _ | VernacRegister _ | VernacNameSectionHypSet _ + | VernacDeclareCustomEntry _ | VernacComments _ -> VtSideff [], VtLater (* Who knows *) | VernacLoad _ -> VtSideff [], VtNow @@ -183,30 +182,26 @@ let classify_vernac e = | VernacBack _ | VernacAbortAll | VernacUndoTo _ | VernacUndo _ | VernacResetName _ | VernacResetInitial - | VernacBacktrack _ | VernacBackTo _ | VernacRestart -> VtMeta, VtNow + | VernacBackTo _ | VernacRestart -> VtMeta, VtNow (* What are these? *) - | VernacToplevelControl _ | VernacRestoreState _ | VernacWriteState _ -> VtSideff [], VtNow (* Plugins should classify their commands *) | VernacExtend (s,l) -> - try List.assoc s !classifiers l () + try Vernacentries.get_vernac_classifier s l with Not_found -> anomaly(str"No classifier for"++spc()++str (fst s)++str".") in let rec static_control_classifier ~poly = function | VernacExpr (f, e) -> - let poly = List.fold_left (fun poly f -> - match f with - | VernacPolymorphic b -> b - | (VernacProgram | VernacLocal _) -> poly - ) poly f in + let _, atts = Vernacentries.attributes_of_flags f Vernacinterp.(mk_atts ~polymorphic:poly ()) in + let poly = atts.Vernacinterp.polymorphic in static_classifier ~poly e | VernacTimeout (_,e) -> static_control_classifier ~poly e | VernacTime (_,{v=e}) | VernacRedirect (_, {v=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 _ + | ( VtQuery | VtProofStep _ | VtSideff _ | VtProofMode _ | VtMeta), _ as x -> x | VtQed _, _ -> VtProofStep { parallel = `No; proof_block_detection = None }, @@ -215,6 +210,6 @@ let classify_vernac e = in static_control_classifier ~poly:(Flags.is_universe_polymorphism ()) e -let classify_as_query = VtQuery (true,Feedback.default_route), VtLater +let classify_as_query = VtQuery, VtLater let classify_as_sideeff = VtSideff [], VtLater let classify_as_proofstep = VtProofStep { parallel = `No; proof_block_detection = None}, VtLater |