aboutsummaryrefslogtreecommitdiff
path: root/stm
diff options
context:
space:
mode:
Diffstat (limited to 'stm')
-rw-r--r--stm/stm.mllib1
-rw-r--r--stm/vernac_classifier.ml215
-rw-r--r--stm/vernac_classifier.mli19
3 files changed, 0 insertions, 235 deletions
diff --git a/stm/stm.mllib b/stm/stm.mllib
index 831369625f..49e7195e27 100644
--- a/stm/stm.mllib
+++ b/stm/stm.mllib
@@ -3,7 +3,6 @@ Dag
Vcs
TQueue
WorkerPool
-Vernac_classifier
CoqworkmgrApi
AsyncTaskQueue
Partac
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
deleted file mode 100644
index ffae2866c0..0000000000
--- a/stm/vernac_classifier.ml
+++ /dev/null
@@ -1,215 +0,0 @@
-(************************************************************************)
-(* * 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/stm/vernac_classifier.mli b/stm/vernac_classifier.mli
deleted file mode 100644
index 61bf3a503a..0000000000
--- a/stm/vernac_classifier.mli
+++ /dev/null
@@ -1,19 +0,0 @@
-(************************************************************************)
-(* * 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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 10:30:25 +0000