aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-09-18 13:27:20 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-09-19 11:43:42 +0200
commit84accdaea3ce094cc5d0232107d3e2ea654a76c2 (patch)
treeeab140c332984b597536d1cabdf9b2ecd474b929 /stm
parentd87bc5b9fb353655f8b905d73293abe96b0ad063 (diff)
Remove STM vernaculars.
Diffstat (limited to 'stm')
-rw-r--r--stm/stm.ml32
-rw-r--r--stm/vernac_classifier.ml8
2 files changed, 15 insertions, 25 deletions
diff --git a/stm/stm.ml b/stm/stm.ml
index 7e17fa2f5..e0064df9b 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1049,7 +1049,7 @@ end = struct (* {{{ *)
try
match v with
| VernacResetInitial ->
- VtStm (VtBack Stateid.initial, true), VtNow
+ VtBack (true, Stateid.initial), VtNow
| VernacResetName (_,name) ->
let id = VCS.get_branch_pos (VCS.current_branch ()) in
(try
@@ -1057,20 +1057,20 @@ end = struct (* {{{ *)
fold_until (fun b (id,_,label,_,_) ->
if b then `Stop id else `Cont (List.mem name label))
false id in
- VtStm (VtBack oid, true), VtNow
+ VtBack (true, oid), VtNow
with Not_found ->
- VtStm (VtBack id, true), VtNow)
+ VtBack (true, id), 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
- VtStm (VtBack oid, true), VtNow
+ VtBack (true, oid), 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
- VtStm (VtBack oid, true), VtLater
+ VtBack (true, oid), VtLater
| VernacUndoTo _
| VernacRestart as e ->
let m = match e with VernacUndoTo m -> m | _ -> 0 in
@@ -1087,16 +1087,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
- VtStm (VtBack oid, true), VtLater
+ VtBack (true, oid), 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
- VtStm (VtBack oid, true), VtLater
+ VtBack (true, oid), VtLater
| VernacBacktrack (id,_,_)
| VernacBackTo id ->
- VtStm (VtBack (Stateid.of_int id), not !Flags.batch_mode), VtNow
+ VtBack (not !Flags.batch_mode, Stateid.of_int id), VtNow
| _ -> VtUnknown, VtNow
with
| Not_found ->
@@ -2484,14 +2484,8 @@ let process_transaction ?(newtip=Stateid.fresh ())
stm_prerr_endline (fun () ->
" classified as: " ^ string_of_vernac_classification c);
match c with
- (* Joining various parts of the document *)
- | VtStm (VtJoinDocument, b), VtNow -> join (); `Ok
- | VtStm (VtWait, b), VtNow -> wait (); `Ok
- | VtStm ((VtJoinDocument|VtWait),_), VtLater ->
- anomaly(str"classifier: join actions cannot be classified as VtLater.")
-
(* Back *)
- | VtStm (VtBack oid, true), w ->
+ | VtBack (true, oid), 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
@@ -2510,12 +2504,12 @@ let process_transaction ?(newtip=Stateid.fresh ())
VCS.checkout_shallowest_proof_branch ();
VCS.commit id (Alias (oid,x));
Backtrack.record (); if w == VtNow then finish (); `Ok
- | VtStm (VtBack id, false), VtNow ->
+ | VtBack (false, id), VtNow ->
stm_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
- | VtStm (VtBack id, false), VtLater ->
+ | VtBack (false, id), VtLater ->
anomaly(str"classifier: VtBack + VtLater must imply part_of_script.")
(* Query *)
@@ -2779,8 +2773,8 @@ let query ~at ~route s =
let clas = classify_vernac ast in
let aast = { verbose = true; indentation; strlen; loc; expr = ast } in
match clas with
- | VtStm (w,_), _ ->
- ignore(process_transaction aast (VtStm (w,false), VtNow))
+ | VtBack (_,id), _ -> (* TODO: can this still happen ? *)
+ ignore(process_transaction aast (VtBack (false,id), VtNow))
| _ ->
ignore(process_transaction aast (VtQuery (false, route), VtNow)))
s
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index c2ebea961..158ad9084 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -31,8 +31,7 @@ let string_of_vernac_type = function
Option.default "" proof_block_detection
| VtProofMode s -> "ProofMode " ^ s
| VtQuery (b, route) -> "Query " ^ string_of_in_script b ^ " route " ^ string_of_int route
- | VtStm ((VtJoinDocument|VtWait), b) -> "Stm " ^ string_of_in_script b
- | VtStm (VtBack _, b) -> "Stm Back " ^ string_of_in_script b
+ | VtBack (b, _) -> "Stm Back " ^ string_of_in_script b
let string_of_vernac_when = function
| VtLater -> "Later"
@@ -64,9 +63,6 @@ let rec classify_vernac e =
* look at the entire dag to detect this option. *)
| VernacSetOption (["Universe"; "Polymorphism"],_)
| VernacUnsetOption (["Universe"; "Polymorphism"]) -> VtSideff [], VtNow
- (* Stm *)
- | VernacStm Wait -> VtStm (VtWait, true), VtNow
- | VernacStm JoinDocument -> VtStm (VtJoinDocument, true), VtNow
(* Nested vernac exprs *)
| VernacProgram e -> classify_vernac e
| VernacLocal (_,e) -> classify_vernac e
@@ -79,7 +75,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 _
- | VtStm _ | VtProofMode _ ), _ as x -> x
+ | VtBack _ | VtProofMode _ ), _ as x -> x
| VtQed _, _ ->
VtProofStep { parallel = `No; proof_block_detection = None },
VtNow