summaryrefslogtreecommitdiff
path: root/stm/vernac_classifier.ml
diff options
context:
space:
mode:
Diffstat (limited to 'stm/vernac_classifier.ml')
-rw-r--r--stm/vernac_classifier.ml227
1 files changed, 227 insertions, 0 deletions
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
new file mode 100644
index 00000000..e9302bb7
--- /dev/null
+++ b/stm/vernac_classifier.ml
@@ -0,0 +1,227 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+open Vernacexpr
+open Errors
+open Pp
+
+let string_of_in_script b = if b then " (inside script)" else ""
+
+let string_of_vernac_type = function
+ | VtUnknown -> "Unknown"
+ | VtStartProof _ -> "StartProof"
+ | VtSideff _ -> "Sideff"
+ | VtQed VtKeep -> "Qed(keep)"
+ | VtQed VtKeepAsAxiom -> "Qed(admitted)"
+ | VtQed VtDrop -> "Qed(drop)"
+ | VtProofStep false -> "ProofStep"
+ | VtProofStep true -> "ProofStep (parallel)"
+ | VtProofMode s -> "ProofMode " ^ s
+ | VtQuery (b,(id,route)) ->
+ "Query " ^ string_of_in_script b ^ " report " ^ Stateid.to_string id ^
+ " route " ^ string_of_int route
+ | VtStm ((VtFinish|VtJoinDocument|VtObserve _|VtPrintDag|VtWait), b) ->
+ "Stm " ^ string_of_in_script b
+ | VtStm (VtPG, b) -> "Stm PG " ^ string_of_in_script b
+ | VtStm (VtBack _, b) -> "Stm Back " ^ string_of_in_script b
+
+let string_of_vernac_when = function
+ | VtLater -> "Later"
+ | VtNow -> "Now"
+
+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 elide_part_of_script_and_now (a, _) =
+ match a with
+ | VtQuery (_,id) -> VtQuery (false,id), VtNow
+ | VtStm (x, _) -> VtStm (x, false), VtNow
+ | x -> x, VtNow
+
+let make_polymorphic (a, b as x) =
+ match a with
+ | VtStartProof (x, _, ids) ->
+ VtStartProof (x, Doesn'tGuaranteeOpacity, ids), b
+ | _ -> x
+
+let undo_classifier = ref (fun _ -> assert false)
+let set_undo_classifier f = undo_classifier := f
+
+let rec classify_vernac e =
+ let rec static_classifier e = match e with
+ (* PG compatibility *)
+ | VernacUnsetOption (["Silent"]|["Undo"]|["Printing";"Depth"])
+ | VernacSetOption ((["Silent"]|["Undo"]|["Printing";"Depth"]),_)
+ when !Flags.print_emacs -> VtStm(VtPG,false), VtNow
+ (* Stm *)
+ | VernacStm Finish -> VtStm (VtFinish, true), VtNow
+ | VernacStm Wait -> VtStm (VtWait, true), VtNow
+ | VernacStm JoinDocument -> VtStm (VtJoinDocument, true), VtNow
+ | VernacStm PrintDag -> VtStm (VtPrintDag, true), VtNow
+ | VernacStm (Observe id) -> VtStm (VtObserve id, true), VtNow
+ | VernacStm (Command x) -> elide_part_of_script_and_now (classify_vernac x)
+ | VernacStm (PGLast x) -> fst (classify_vernac x), VtNow
+ (* Nested vernac exprs *)
+ | VernacProgram e -> classify_vernac e
+ | VernacLocal (_,e) -> classify_vernac e
+ | VernacPolymorphic (b, e) ->
+ if b || Flags.is_universe_polymorphism () (* Ok or not? *) then
+ make_polymorphic (classify_vernac e)
+ else classify_vernac e
+ | VernacTimeout (_,e) -> classify_vernac e
+ | VernacTime e -> classify_vernac_list e
+ | VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *)
+ (match classify_vernac e with
+ | ( VtQuery _ | VtProofStep _ | VtSideff _
+ | VtStm _ | VtProofMode _ ), _ as x -> x
+ | VtQed _, _ -> VtProofStep false, VtNow
+ | (VtStartProof _ | VtUnknown), _ -> VtUnknown, VtNow)
+ (* Qed *)
+ | VernacAbort _ -> VtQed VtDrop, VtLater
+ | VernacEndProof Admitted -> VtQed VtKeepAsAxiom, VtLater
+ | VernacEndProof _ | VernacExactProof _ -> VtQed VtKeep, VtLater
+ (* Query *)
+ | VernacShow _ | VernacPrint _ | VernacSearch _ | VernacLocate _
+ | VernacCheckMayEval _ ->
+ VtQuery (true,(Stateid.dummy,Feedback.default_route)), VtLater
+ (* ProofStep *)
+ | VernacSolve (SelectAllParallel,_,_,_) -> VtProofStep true, VtLater
+ | VernacProof _
+ | VernacBullet _
+ | VernacFocus _ | VernacUnfocus
+ | VernacSubproof _ | VernacEndSubproof
+ | VernacSolve _
+ | VernacCheckGuard
+ | VernacUnfocused
+ | VernacSolveExistential _ -> VtProofStep false, VtLater
+ (* Options changing parser *)
+ | VernacUnsetOption (["Default";"Proof";"Using"])
+ | VernacSetOption (["Default";"Proof";"Using"],_) -> VtSideff [], VtNow
+ (* StartProof *)
+ | VernacDefinition (
+ (Some Decl_kinds.Discharge,Decl_kinds.Definition),(_,i),ProveBody _) ->
+ VtStartProof("Classic",Doesn'tGuaranteeOpacity,[i]), VtLater
+ | VernacDefinition (_,(_,i),ProveBody _) ->
+ VtStartProof("Classic",GuaranteesOpacity,[i]), VtLater
+ | VernacStartTheoremProof (_,l,_) ->
+ let ids =
+ CList.map_filter (function (Some(_,i), _) -> Some i | _ -> None) l in
+ VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater
+ | VernacGoal _ -> VtStartProof ("Classic",GuaranteesOpacity,[]), VtLater
+ | VernacFixpoint (_,l) ->
+ let ids, open_proof =
+ List.fold_left (fun (l,b) (((_,id),_,_,_,p),_) ->
+ id::l, b || p = None) ([],false) l in
+ if open_proof
+ then VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater
+ else VtSideff ids, VtLater
+ | VernacCoFixpoint (_,l) ->
+ let ids, open_proof =
+ List.fold_left (fun (l,b) (((_,id),_,_,p),_) ->
+ id::l, b || p = None) ([],false) l in
+ if open_proof
+ then VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater
+ 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 snd l) l) in
+ VtSideff ids, VtLater
+ | VernacDefinition (_,(_,id),DefineBody _) -> VtSideff [id], VtLater
+ | VernacInductive (_,_,l) ->
+ let ids = List.map (fun (((_,(_,id)),_,_,_,cl),_) -> id :: match cl with
+ | Constructors l -> List.map (fun (_,((_,id),_)) -> id) l
+ | RecordDecl (oid,l) -> (match oid with Some (_,x) -> [x] | _ -> []) @
+ CList.map_filter (function
+ | ((_,AssumExpr((_,Names.Name n),_)),_),_ -> Some n
+ | _ -> None) l) l in
+ VtSideff (List.flatten ids), VtLater
+ | VernacScheme l ->
+ let ids = List.map snd (CList.map_filter (fun (x,_) -> x) l) in
+ VtSideff ids, VtLater
+ | VernacCombinedScheme ((_,id),_) -> VtSideff [id], VtLater
+ | VernacUniverse _ | VernacConstraint _
+ | VernacBeginSection _
+ | VernacCanonical _ | VernacCoercion _ | VernacIdentityCoercion _
+ | VernacAddLoadPath _ | VernacRemoveLoadPath _ | VernacAddMLPath _
+ | VernacChdir _
+ | VernacCreateHintDb _ | VernacRemoveHints _ | VernacHints _
+ | VernacDeclareImplicits _ | VernacArguments _ | VernacArgumentsScope _
+ | VernacReserve _
+ | VernacGeneralizable _
+ | VernacSetOpacity _ | VernacSetStrategy _
+ | VernacUnsetOption _ | VernacSetOption _
+ | VernacAddOption _ | VernacRemoveOption _
+ | VernacMemOption _ | VernacPrintOption _
+ | VernacGlobalCheck _
+ | VernacDeclareReduction _
+ | VernacDeclareClass _ | VernacDeclareInstances _
+ | VernacRegister _
+ | VernacDeclareTacticDefinition _
+ | VernacNameSectionHypSet _
+ | VernacComments _ -> 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,(_,id),bl,_)
+ | VernacDefineModule (exp,(_,id),bl,_,_) ->
+ VtSideff [id], if bl = [] && exp = None then VtLater else VtNow
+ | VernacDeclareModuleType ((_,id),bl,_,_) ->
+ VtSideff [id], if bl = [] then VtLater else VtNow
+ (* These commands alter the parser *)
+ | VernacOpenCloseScope _ | VernacDelimiters _ | VernacBindScope _
+ | VernacInfix _ | VernacNotation _ | VernacNotationAddFormat _
+ | VernacSyntaxExtension _
+ | VernacSyntacticDefinition _
+ | VernacTacticNotation _
+ | VernacRequire _ | VernacImport _ | VernacInclude _
+ | VernacDeclareMLModule _
+ | VernacContext _ (* TASSI: unsure *)
+ | VernacProofMode _
+ (* These are ambiguous *)
+ | VernacInstance _ -> VtUnknown, VtNow
+ (* Stm will install a new classifier to handle these *)
+ | VernacBack _ | VernacAbortAll
+ | VernacUndoTo _ | VernacUndo _
+ | VernacResetName _ | VernacResetInitial
+ | VernacBacktrack _ | VernacBackTo _ | VernacRestart -> !undo_classifier e
+ (* What are these? *)
+ | VernacNop
+ | VernacToplevelControl _
+ | VernacRestoreState _
+ | VernacWriteState _ -> VtUnknown, VtNow
+ | VernacError _ -> assert false
+ (* Plugins should classify their commands *)
+ | VernacExtend (s,l) ->
+ try List.assoc s !classifiers l ()
+ with Not_found -> anomaly(str"No classifier for"++spc()++str (fst s))
+ and classify_vernac_list = function
+ (* spiwack: It would be better to define a monoid on classifiers.
+ So that the classifier of the list would be the composition of
+ the classifier of the individual commands. Currently: special
+ case for singleton lists.*)
+ | [_,c] -> static_classifier c
+ | l -> VtUnknown,VtNow
+ in
+ let res = static_classifier e in
+ if Flags.is_universe_polymorphism () then
+ make_polymorphic res
+ else res
+
+let classify_as_query =
+ VtQuery (true,(Stateid.dummy,Feedback.default_route)), VtLater
+let classify_as_sideeff = VtSideff [], VtLater
+let classify_as_proofstep = VtProofStep false, VtLater
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-15 23:45:13 +0000