aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--ide/texmacspp.ml3
-rw-r--r--intf/vernacexpr.mli23
-rw-r--r--parsing/g_vernac.ml410
-rw-r--r--printing/ppvernac.ml16
-rw-r--r--stm/stm.ml51
-rw-r--r--stm/vernac_classifier.ml22
-rw-r--r--toplevel/vernac.ml3
-rw-r--r--toplevel/vernacentries.ml4
8 files changed, 112 insertions, 20 deletions
diff --git a/ide/texmacspp.ml b/ide/texmacspp.ml
index dbcd8630b..680da7f54 100644
--- a/ide/texmacspp.ml
+++ b/ide/texmacspp.ml
@@ -724,6 +724,9 @@ let rec tmpp v loc =
| VernacComments (cl) ->
xmlComment loc (List.flatten (List.map pp_comment cl))
+ (* Stm backdoor *)
+ | VernacStm _ as x -> xmlTODO loc x
+
(* Proof management *)
| VernacGoal _ as x -> xmlTODO loc x
| VernacAbort _ as x -> xmlTODO loc x
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index f77a940a7..92e4dd618 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -283,6 +283,16 @@ type bullet =
| Star of int
| Plus of int
+(** {6 Types concerning Stm} *)
+type 'a stm_vernac =
+ | JoinDocument
+ | Finish
+ | Wait
+ | PrintDag
+ | Observe of Stateid.t
+ | Command of 'a (* An out of flow command not to be recorded by Stm *)
+ | PGLast of 'a (* To ease the life of PG *)
+
(** {6 Types concerning the module layer} *)
(** Rigid / flexible module signature *)
@@ -441,6 +451,9 @@ type vernac_expr =
| VernacRegister of lident * register_kind
| VernacComments of comment list
+ (* Stm backdoor *)
+ | VernacStm of vernac_expr stm_vernac
+
(* Proof management *)
| VernacGoal of constr_expr
| VernacAbort of lident option
@@ -495,7 +508,7 @@ type vernac_type =
| VtProofStep of proof_step
| VtProofMode of string
| VtQuery of vernac_part_of_script * report_with
- | VtBack of Stateid.t * vernac_part_of_script
+ | VtStm of vernac_control * vernac_part_of_script
| VtUnknown
and report_with = Stateid.t * Feedback.route_id (* feedback on id/route *)
and vernac_qed_type = VtKeep | VtKeepAsAxiom | VtDrop (* Qed/Admitted, Abort *)
@@ -503,6 +516,14 @@ and vernac_start = string * opacity_guarantee * Id.t list
and vernac_sideff_type = Id.t list
and vernac_is_alias = bool
and vernac_part_of_script = bool
+and vernac_control =
+ | VtFinish
+ | VtWait
+ | VtJoinDocument
+ | VtPrintDag
+ | VtObserve of Stateid.t
+ | VtBack of Stateid.t
+ | VtPG
and opacity_guarantee =
| GuaranteesOpacity (** Only generates opaque terms at [Qed] *)
| Doesn'tGuaranteeOpacity (** May generate transparent terms even with [Qed].*)
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 4ba9eeefa..9b52d1bf3 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -64,6 +64,16 @@ GEXTEND Gram
| IDENT "Local"; v = vernac_poly -> VernacLocal (true, v)
| IDENT "Global"; v = vernac_poly -> VernacLocal (false, v)
+ (* Stm backdoor *)
+ | IDENT "Stm"; IDENT "JoinDocument"; "." -> VernacStm JoinDocument
+ | IDENT "Stm"; IDENT "Finish"; "." -> VernacStm Finish
+ | IDENT "Stm"; IDENT "Wait"; "." -> VernacStm Wait
+ | IDENT "Stm"; IDENT "PrintDag"; "." -> VernacStm PrintDag
+ | IDENT "Stm"; IDENT "Observe"; id = INT; "." ->
+ VernacStm (Observe (Stateid.of_int (int_of_string id)))
+ | IDENT "Stm"; IDENT "Command"; v = vernac_aux -> VernacStm (Command v)
+ | IDENT "Stm"; IDENT "PGLast"; v = vernac_aux -> VernacStm (PGLast v)
+
| v = vernac_poly -> v ]
]
;
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index a6b1c97f5..3494ad006 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -538,6 +538,22 @@ module Make
| VernacLocal (local, v) ->
return (pr_locality local ++ spc() ++ pr_vernac_body v)
+ (* Stm *)
+ | VernacStm JoinDocument ->
+ return (keyword "Stm JoinDocument")
+ | VernacStm PrintDag ->
+ return (keyword "Stm PrintDag")
+ | VernacStm Finish ->
+ return (keyword "Stm Finish")
+ | VernacStm Wait ->
+ return (keyword "Stm Wait")
+ | VernacStm (Observe id) ->
+ return (keyword "Stm Observe " ++ str(Stateid.to_string id))
+ | VernacStm (Command v) ->
+ return (keyword "Stm Command " ++ pr_vernac_body v)
+ | VernacStm (PGLast v) ->
+ return (keyword "Stm PGLast " ++ pr_vernac_body v)
+
(* Proof management *)
| VernacAbortAll ->
return (keyword "Abort All")
diff --git a/stm/stm.ml b/stm/stm.ml
index 0ddaf604a..e387e6322 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -989,7 +989,7 @@ end = struct (* {{{ *)
try
match v with
| VernacResetInitial ->
- VtBack (Stateid.initial, true), VtNow
+ VtStm (VtBack Stateid.initial, true), VtNow
| VernacResetName (_,name) ->
let id = VCS.get_branch_pos (VCS.current_branch ()) in
(try
@@ -997,20 +997,20 @@ end = struct (* {{{ *)
fold_until (fun b (id,_,label,_,_) ->
if b then `Stop id else `Cont (List.mem name label))
false id in
- VtBack (oid, true), VtNow
+ VtStm (VtBack oid, true), VtNow
with Not_found ->
- VtBack (id, true), VtNow)
+ VtStm (VtBack id, true), VtNow)
| VernacBack n ->
let id = VCS.get_branch_pos (VCS.current_branch ()) in
let oid = fold_until (fun n (id,_,_,_,_) ->
if Int.equal n 0 then `Stop id else `Cont (n-1)) n id in
- VtBack (oid, true), VtNow
+ VtStm (VtBack oid, true), VtNow
| VernacUndo n ->
let id = VCS.get_branch_pos (VCS.current_branch ()) in
let oid = fold_until (fun n (id,_,_,tactic,undo) ->
let value = (if tactic then 1 else 0) - undo in
if Int.equal n 0 then `Stop id else `Cont (n-value)) n id in
- VtBack (oid, true), VtLater
+ VtStm (VtBack oid, true), VtLater
| VernacUndoTo _
| VernacRestart as e ->
let m = match e with VernacUndoTo m -> m | _ -> 0 in
@@ -1027,16 +1027,16 @@ end = struct (* {{{ *)
0 id in
let oid = fold_until (fun n (id,_,_,_,_) ->
if Int.equal n 0 then `Stop id else `Cont (n-1)) (n-m-1) id in
- VtBack (oid, true), VtLater
+ VtStm (VtBack oid, true), VtLater
| VernacAbortAll ->
let id = VCS.get_branch_pos (VCS.current_branch ()) in
let oid = fold_until (fun () (id,vcs,_,_,_) ->
match Vcs_.branches vcs with [_] -> `Stop id | _ -> `Cont ())
() id in
- VtBack (oid, true), VtLater
+ VtStm (VtBack oid, true), VtLater
| VernacBacktrack (id,_,_)
| VernacBackTo id ->
- VtBack (Stateid.of_int id, not !Flags.print_emacs), VtNow
+ VtStm (VtBack (Stateid.of_int id), not !Flags.print_emacs), VtNow
| _ -> VtUnknown, VtNow
with
| Not_found ->
@@ -2428,8 +2428,22 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty
prerr_endline (fun () ->
" classified as: " ^ string_of_vernac_classification c);
match c with
+ (* PG stuff *)
+ | VtStm(VtPG,false), VtNow -> vernac_interp Stateid.dummy x; `Ok
+ | VtStm(VtPG,_), _ -> anomaly(str "PG command in script or VtLater")
+ (* Joining various parts of the document *)
+ | VtStm (VtJoinDocument, b), VtNow -> join (); `Ok
+ | VtStm (VtFinish, b), VtNow -> finish (); `Ok
+ | VtStm (VtWait, b), VtNow -> finish (); wait (); `Ok
+ | VtStm (VtPrintDag, b), VtNow ->
+ VCS.print ~now:true (); `Ok
+ | VtStm (VtObserve id, b), VtNow -> observe id; `Ok
+ | VtStm ((VtObserve _ | VtFinish | VtJoinDocument
+ |VtPrintDag |VtWait),_), VtLater ->
+ anomaly(str"classifier: join actions cannot be classified as VtLater")
+
(* Back *)
- | VtBack(oid, true), w ->
+ | VtStm (VtBack oid, true), w ->
let id = VCS.new_node ~id:newtip () in
let { mine; others } = Backtrack.branches_of oid in
let valid = VCS.get_branch_pos head in
@@ -2448,12 +2462,12 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty
VCS.checkout_shallowest_proof_branch ();
VCS.commit id (Alias (oid,x));
Backtrack.record (); if w == VtNow then finish (); `Ok
- | VtBack (id, false), VtNow ->
+ | VtStm (VtBack id, false), VtNow ->
prerr_endline (fun () -> "undo to state " ^ Stateid.to_string id);
Backtrack.backto id;
VCS.checkout_shallowest_proof_branch ();
Reach.known_state ~cache:(interactive ()) id; `Ok
- | VtBack (id, false), VtLater ->
+ | VtStm (VtBack id, false), VtLater ->
anomaly(str"classifier: VtBack + VtLater must imply part_of_script")
(* Query *)
@@ -2590,6 +2604,15 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty
| VtUnknown, VtLater ->
anomaly(str"classifier: VtUnknown must imply VtNow")
end in
+ (* Proof General *)
+ begin match expr with
+ | VernacStm (PGLast _) ->
+ if not (VCS.Branch.equal head VCS.Branch.master) then
+ vernac_interp Stateid.dummy
+ { verbose = true; loc = Loc.ghost; indentation = 0; strlen = 0;
+ expr = VernacShow (ShowGoal OpenSubgoals) }
+ | _ -> ()
+ end;
prerr_endline (fun () -> "processed }}}");
VCS.print ();
rc
@@ -2651,8 +2674,8 @@ let query ~at ?(report_with=(Stateid.dummy,default_route)) s =
let clas = classify_vernac ast in
let aast = { verbose = true; indentation; strlen; loc; expr = ast } in
match clas with
- | VtBack (w,_), _ ->
- ignore(process_transaction ~tty:false aast (VtBack (w,false), VtNow))
+ | VtStm (w,_), _ ->
+ ignore(process_transaction ~tty:false aast (VtStm (w,false), VtNow))
| _ ->
ignore(process_transaction
~tty:false aast (VtQuery (false,report_with), VtNow)))
@@ -2799,7 +2822,7 @@ let interp verb (loc,e) =
let print_goals =
verb && match clas with
| VtQuery _, _ -> false
- | (VtProofStep _ | VtBack (_, _) | VtStartProof _), _ -> true
+ | (VtProofStep _ | VtStm (VtBack _, _) | VtStartProof _), _ -> true
| _ -> not !Flags.coqtop_ui in
try finish ~print_goals ()
with e ->
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index f9bf9653f..dc5be08a3 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -33,7 +33,10 @@ let string_of_vernac_type = function
| VtQuery (b,(id,route)) ->
"Query " ^ string_of_in_script b ^ " report " ^ Stateid.to_string id ^
" route " ^ string_of_int route
- | VtBack(_, b) -> "Stm Back " ^ string_of_in_script b
+ | 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"
@@ -52,7 +55,7 @@ let declare_vernac_classifier
let elide_part_of_script_and_now (a, _) =
match a with
| VtQuery (_,id) -> VtQuery (false,id), VtNow
- | VtBack (x, _) -> VtBack (x, false), VtNow
+ | VtStm (x, _) -> VtStm (x, false), VtNow
| x -> x, VtNow
let make_polymorphic (a, b as x) =
@@ -66,12 +69,23 @@ let set_undo_classifier f = undo_classifier := f
let rec classify_vernac e =
let 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
(* 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 (["Universe"; "Polymorphism"],_)
| VernacUnsetOption (["Universe"; "Polymorphism"]) -> VtSideff [], 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
@@ -84,7 +98,7 @@ let rec classify_vernac e =
| VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *)
(match classify_vernac e with
| ( VtQuery _ | VtProofStep _ | VtSideff _
- | VtBack _ | VtProofMode _ ), _ as x -> x
+ | VtStm _ | VtProofMode _ ), _ as x -> x
| VtQed _, _ ->
VtProofStep { parallel = `No; proof_block_detection = None },
VtNow
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index ba5bc5506..bfdae85d5 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -27,7 +27,8 @@ let rec is_navigation_vernac = function
| VernacResetName _
| VernacBacktrack _
| VernacBackTo _
- | VernacBack _ -> true
+ | VernacBack _
+ | VernacStm _ -> true
| VernacRedirect (_, (_,c))
| VernacTime (_,c) ->
is_navigation_vernac c (* Time Back* is harmless *)
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index f0e63aa7c..230e62607 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1941,6 +1941,7 @@ let interp ?proof ~loc locality poly c =
| VernacTime _ -> assert false
| VernacRedirect _ -> assert false
| VernacTimeout _ -> assert false
+ | VernacStm _ -> assert false
| VernacError e -> raise e
@@ -2208,6 +2209,9 @@ let interp ?(verbosely=true) ?proof (loc,c) =
aux ?locality ~polymorphism:b isprogcmd c
| VernacPolymorphic (b, c) -> CErrors.error "Polymorphism specified twice"
| VernacLocal _ -> CErrors.error "Locality specified twice"
+ | VernacStm (Command c) -> aux ?locality ?polymorphism isprogcmd c
+ | VernacStm (PGLast c) -> aux ?locality ?polymorphism isprogcmd c
+ | VernacStm _ -> assert false (* Done by Stm *)
| VernacFail v ->
with_fail true (fun () -> aux ?locality ?polymorphism isprogcmd v)
| VernacTimeout (n,v) ->
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-12 03:25:27 +0000