From e43c35ba795520fe111ac39a834f334753491b28 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 17 Apr 2017 10:31:29 +0200 Subject: [STM] explicit handling of parsing states DAG nodes hold now a system state and a parsing state. The latter is always passed to the parser. This paves the way to decoupling the effect of commands on the parsing state and the system state, and hence never force to interpret, say, Notation. Handling proof modes is now done explicitly in the STM, not by interpreting VernacStartLemma. Similarly Notation execution could be split in two phases in order to obtain a parsing state without fully executing it (that requires executing all commands before it). Co-authored-by: Maxime Dénès Co-authored-by: Emilio Jesus Gallego Arias --- stm/stm.ml | 483 +++++++++++++++++++++++++---------------------- stm/stm.mli | 13 +- stm/vernac_classifier.ml | 26 ++- 3 files changed, 281 insertions(+), 241 deletions(-) (limited to 'stm') diff --git a/stm/stm.ml b/stm/stm.ml index 8ed7f2c866..dfe5581ed5 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -126,8 +126,6 @@ type aast = { } let pr_ast { expr; indentation } = Pp.(int indentation ++ str " " ++ Ppvernac.pr_vernac expr) -let default_proof_mode () = Proof_global.get_default_proof_mode_name () [@ocaml.warning "-3"] - (* Commands piercing opaque *) let may_pierce_opaque = function | VernacPrint _ @@ -146,13 +144,13 @@ let update_global_env () = module Vcs_ = Vcs.Make(Stateid.Self) type future_proof = Proof_global.closed_proof_output Future.computation -type proof_mode = string + type depth = int type branch_type = [ `Master - | `Proof of proof_mode * depth + | `Proof of depth | `Edit of - proof_mode * Stateid.t * Stateid.t * Vernacextend.vernac_qed_type * Vcs_.Branch.t ] + Stateid.t * Stateid.t * Vernacextend.vernac_qed_type * Vcs_.Branch.t ] (* TODO 8.7 : split commands and tactics, since this type is too messy now *) type cmd_t = { ctac : bool; (* is a tactic *) @@ -203,10 +201,10 @@ let summary_pstate = Evarutil.meta_counter_summary_tag, Obligations.program_tcc_summary_tag type cached_state = - | Empty - | Error of Exninfo.iexn - | Valid of Vernacstate.t - + | EmptyState + | ParsingState of Vernacstate.Parser.state + | FullState of Vernacstate.t + | ErrorState of Vernacstate.Parser.state option * Exninfo.iexn type branch = Vcs_.Branch.t * branch_type Vcs_.branch_info type backup = { mine : branch; others : branch list } @@ -214,10 +212,16 @@ type 'vcs state_info = { (* TODO: Make this record private to VCS *) mutable n_reached : int; (* debug cache: how many times was computed *) mutable n_goals : int; (* open goals: indentation *) mutable state : cached_state; (* state value *) + mutable proof_mode : Pvernac.proof_mode option; mutable vcs_backup : 'vcs option * backup option; } -let default_info () = - { n_reached = 0; n_goals = 0; state = Empty; vcs_backup = None,None } +let default_info proof_mode = + { + n_reached = 0; n_goals = 0; + state = EmptyState; + proof_mode; + vcs_backup = (None,None); + } module DynBlockData : Dyn.S = Dyn.Make () @@ -256,15 +260,15 @@ end = struct (* {{{ *) List.fold_left max 0 (CList.map_filter (function - | { Vcs_.kind = `Proof (_,n) } -> Some n + | { Vcs_.kind = `Proof n } -> Some n | { Vcs_.kind = `Edit _ } -> Some 1 | _ -> None) (List.map (Vcs_.get_branch vcs) (Vcs_.branches vcs))) let find_proof_at_depth vcs pl = try List.find (function - | _, { Vcs_.kind = `Proof(m, n) } -> Int.equal n pl - | _, { Vcs_.kind = `Edit _ } -> anomaly(Pp.str "find_proof_at_depth.") + | _, { Vcs_.kind = `Proof n } -> Int.equal n pl + | _, { Vcs_.kind = `Edit _ } -> anomaly(Pp.str "find_proof_at_depth") | _ -> false) (List.map (fun h -> h, Vcs_.get_branch vcs h) (Vcs_.branches vcs)) with Not_found -> failwith "find_proof_at_depth" @@ -326,7 +330,7 @@ module VCS : sig type vcs = (branch_type, transaction, vcs state_info, box) Vcs_.t - val init : stm_doc_type -> id -> doc + val init : stm_doc_type -> id -> Vernacstate.Parser.state -> doc (* val get_type : unit -> stm_doc_type *) val set_ldir : Names.DirPath.t -> unit val get_ldir : unit -> Names.DirPath.t @@ -339,7 +343,7 @@ module VCS : sig val branches : unit -> Branch.t list val get_branch : Branch.t -> branch_type branch_info val get_branch_pos : Branch.t -> id - val new_node : ?id:Stateid.t -> unit -> id + val new_node : ?id:Stateid.t -> Pvernac.proof_mode option -> unit -> id val merge : id -> ours:transaction -> ?into:Branch.t -> Branch.t -> unit val rewrite_merge : id -> ours:transaction -> at:id -> Branch.t -> unit val delete_branch : Branch.t -> unit @@ -356,6 +360,10 @@ module VCS : sig val goals : id -> int -> unit val set_state : id -> cached_state -> unit val get_state : id -> cached_state + val set_parsing_state : id -> Vernacstate.Parser.state -> unit + val get_parsing_state : id -> Vernacstate.Parser.state option + val get_proof_mode : id -> Pvernac.proof_mode option + val set_proof_mode : id -> Pvernac.proof_mode option -> unit (* cuts from start -> stop, raising Expired if some nodes are not there *) val slice : block_start:id -> block_stop:id -> vcs @@ -369,7 +377,8 @@ module VCS : sig val proof_nesting : unit -> int val checkout_shallowest_proof_branch : unit -> unit - val propagate_sideff : action:seff_t -> unit + val propagate_sideff : action:seff_t -> Stateid.t list + val propagate_qed : unit -> unit val gc : unit -> unit @@ -411,11 +420,11 @@ end = struct (* {{{ *) | Qed { qast } -> Pp.string_of_ppcmds (pr_ast qast) in let is_green id = match get_info vcs id with - | Some { state = Valid _ } -> true + | Some { state = FullState _ } -> true | _ -> false in let is_red id = match get_info vcs id with - | Some { state = Error _ } -> true + | Some { state = ErrorState _ } -> true | _ -> false in let head = current_branch vcs in let heads = @@ -517,10 +526,11 @@ end = struct (* {{{ *) let doc_type = ref (Interactive (TopLogical (Names.DirPath.make []))) let ldir = ref Names.DirPath.empty - let init dt id = + let init dt id ps = doc_type := dt; vcs := empty id; - vcs := set_info !vcs id (default_info ()); + let info = { (default_info None) with state = ParsingState ps } in + vcs := set_info !vcs id info; dummy_doc let set_ldir ld = @@ -545,9 +555,9 @@ end = struct (* {{{ *) let branches () = branches !vcs let get_branch head = get_branch !vcs head let get_branch_pos head = (get_branch head).pos - let new_node ?(id=Stateid.fresh ()) () = + let new_node ?(id=Stateid.fresh ()) proof_mode () = assert(Vcs_.get_info !vcs id = None); - vcs := set_info !vcs id (default_info ()); + vcs := set_info !vcs id (default_info proof_mode); id let merge id ~ours ?into branch = vcs := merge !vcs id ~ours ~theirs:Noop ?into branch @@ -569,9 +579,39 @@ end = struct (* {{{ *) | Some x -> x | None -> raise Vcs_aux.Expired let set_state id s = - (get_info id).state <- s; - if async_proofs_is_master !cur_opt then Hooks.(call state_ready ~doc:dummy_doc (* XXX should be taken in input *) id) + let info = get_info id in + info.state <- s; + let is_full_state_valid = match s with + | FullState _ -> true + | EmptyState | ErrorState _ | ParsingState _ -> false + in + if async_proofs_is_master !cur_opt && is_full_state_valid then + Hooks.(call state_ready ~doc:dummy_doc (* XXX should be taken in input *) id) + let get_state id = (get_info id).state + + let get_parsing_state id = + stm_pperr_endline (fun () -> str "retrieve parsing state state " ++ str (Stateid.to_string id) ++ str " }}}"); + match (get_info id).state with + | FullState s -> Some s.Vernacstate.parsing + | ParsingState s -> Some s + | ErrorState (s,_) -> s + | EmptyState -> None + + let set_parsing_state id ps = + let info = get_info id in + let new_state = + match info.state with + | FullState s -> assert false + | ParsingState s -> assert false + | ErrorState _ -> assert false + | EmptyState -> ParsingState ps + in + info.state <- new_state + + let get_proof_mode id = (get_info id).proof_mode + let set_proof_mode id pm = (get_info id).proof_mode <- pm + let reached id = let info = get_info id in info.n_reached <- info.n_reached + 1 @@ -582,28 +622,33 @@ end = struct (* {{{ *) let checkout_shallowest_proof_branch () = if List.mem edit_branch (Vcs_.branches !vcs) then begin - checkout edit_branch; - match get_branch edit_branch with - | { kind = `Edit (mode, _,_,_,_) } -> Proof_global.activate_proof_mode mode [@ocaml.warning "-3"] - | _ -> assert false + checkout edit_branch end else let pl = proof_nesting () in try - let branch, mode = match Vcs_aux.find_proof_at_depth !vcs pl with - | h, { Vcs_.kind = `Proof (m, _) } -> h, m | _ -> assert false in - checkout branch; - stm_prerr_endline (fun () -> "mode:" ^ mode); - Proof_global.activate_proof_mode mode [@ocaml.warning "-3"] + let branch = fst @@ Vcs_aux.find_proof_at_depth !vcs pl in + checkout branch with Failure _ -> - checkout Branch.master; - Proof_global.disactivate_current_proof_mode () [@ocaml.warning "-3"] + checkout Branch.master (* copies the transaction on every open branch *) let propagate_sideff ~action = + List.map (fun b -> + checkout b; + let proof_mode = get_proof_mode @@ get_branch_pos b in + let id = new_node proof_mode () in + merge id ~ours:(Sideff action) ~into:b Branch.master; + id) + (List.filter (fun b -> not (Branch.equal b Branch.master)) (branches ())) + + let propagate_qed () = List.iter (fun b -> checkout b; - let id = new_node () in - merge id ~ours:(Sideff action) ~into:b Branch.master) + let proof_mode = get_proof_mode @@ get_branch_pos b in + let id = new_node proof_mode () in + let parsing = Option.get @@ get_parsing_state (get_branch_pos b) in + merge id ~ours:(Sideff CherryPickEnv) ~into:b Branch.master; + set_parsing_state id parsing) (List.filter (fun b -> not (Branch.equal b Branch.master)) (branches ())) let visit id = Vcs_aux.visit !vcs id @@ -625,10 +670,12 @@ end = struct (* {{{ *) let slice ~block_start ~block_stop = let l = nodes_in_slice ~block_start ~block_stop in let copy_info v id = + let info = get_info id in Vcs_.set_info v id - { (get_info id) with state = Empty; vcs_backup = None,None } in + { info with state = EmptyState; + vcs_backup = None,None } in let make_shallow = function - | Valid st -> Valid (Vernacstate.make_shallow st) + | FullState st -> FullState (Vernacstate.make_shallow st) | x -> x in let copy_info_w_state v id = @@ -651,12 +698,14 @@ end = struct (* {{{ *) let v = copy_info v id in v) l v in (* Stm should have reached the beginning of proof *) - assert (match (get_info block_start).state with Valid _ -> true | _ -> false); + assert (match get_state block_start + with FullState _ -> true | _ -> false); (* We put in the new dag the most recent state known to master *) let rec fill id = - match (get_info id).state with - | Empty | Error _ -> fill (Vcs_aux.visit v id).next - | Valid _ -> copy_info_w_state v id in + match get_state id with + | EmptyState | ErrorState _ | ParsingState _ -> fill (Vcs_aux.visit v id).next + | FullState _ -> copy_info_w_state v id + in let v = fill block_stop in (* We put in the new dag the first state (since Qed shall run on it, * see check_task_aux) *) @@ -753,13 +802,12 @@ end = struct (* {{{ *) end (* }}} *) let state_of_id ~doc id = - try match (VCS.get_info id).state with - | Valid s -> `Valid (Some s) - | Error (e,_) -> `Error e - | Empty -> `Valid None + try match VCS.get_state id with + | FullState s -> `Valid (Some s) + | ErrorState (_,(e,_)) -> `Error e + | EmptyState | ParsingState _ -> `Valid None with VCS.Expired -> `Expired - (****** A cache: fills in the nodes of the VCS document with their value ******) module State : sig @@ -782,6 +830,7 @@ module State : sig val fix_exn_ref : (Exninfo.iexn -> Exninfo.iexn) ref val install_cached : Stateid.t -> unit + (* val install_parsing_state : Stateid.t -> unit *) val is_cached : ?cache:bool -> Stateid.t -> bool val is_cached_and_valid : ?cache:bool -> Stateid.t -> bool @@ -804,10 +853,6 @@ module State : sig val register_root_state : unit -> unit val restore_root_state : unit -> unit - (* Only for internal use to catch problems in parse_sentence, should - be removed in the state handling refactoring. *) - val cur_id : Stateid.t ref - val purify : ('a -> 'b) -> 'a -> 'b end = struct (* {{{ *) @@ -824,6 +869,8 @@ end = struct (* {{{ *) Vernacstate.unfreeze_interp_state st.vernac_state; cur_id := st.id + let invalidate_cur_state () = cur_id := Stateid.dummy + type proof_part = Proof_global.t * int * (* Evarutil.meta_counter_summary_tag *) @@ -842,49 +889,58 @@ end = struct (* {{{ *) Summary.project_from_summary st Util.(pi3 summary_pstate) let cache_state ~marshallable id = - VCS.set_state id (Valid (Vernacstate.freeze_interp_state ~marshallable)) + VCS.set_state id (FullState (Vernacstate.freeze_interp_state ~marshallable)) - let freeze_invalid id iexn = VCS.set_state id (Error iexn) + let freeze_invalid id iexn = + let ps = VCS.get_parsing_state id in + VCS.set_state id (ErrorState (ps,iexn)) let is_cached ?(cache=false) id only_valid = if Stateid.equal id !cur_id then try match VCS.get_info id with - | { state = Empty } when cache -> cache_state ~marshallable:false id; true + | ({ state = EmptyState } | { state = ParsingState _ }) when cache -> cache_state ~marshallable:false id; true | _ -> true with VCS.Expired -> false else - try match VCS.get_info id with - | { state = Empty } -> false - | { state = Valid _ } -> true - | { state = Error _ } -> not only_valid + try match VCS.get_state id with + | EmptyState | ParsingState _ -> false + | FullState _ -> true + | ErrorState _ -> not only_valid with VCS.Expired -> false let is_cached_and_valid ?cache id = is_cached ?cache id true let is_cached ?cache id = is_cached ?cache id false let install_cached id = - match VCS.get_info id with - | { state = Valid s } -> + match VCS.get_state id with + | FullState s -> Vernacstate.unfreeze_interp_state s; cur_id := id - | { state = Error ie } -> + | ErrorState (_,ie) -> Exninfo.iraise ie - | _ -> - (* coqc has a 1 slot cache and only for valid states *) - if not (VCS.is_interactive ()) && Stateid.equal id !cur_id then () - else anomaly Pp.(str "installing a non cached state.") + | EmptyState | ParsingState _ -> + (* coqc has a 1 slot cache and only for valid states *) + if (VCS.is_interactive ()) || not (Stateid.equal id !cur_id) then + anomaly Pp.(str "installing a non cached state.") + + (* + let install_parsing_state id = + if not (Stateid.equal id !cur_id) then begin + Vernacstate.Parser.install @@ VCS.get_parsing_state id + end + *) let get_cached id = - try match VCS.get_info id with - | { state = Valid s } -> s + try match VCS.get_state id with + | FullState s -> s | _ -> anomaly Pp.(str "not a cached state.") with VCS.Expired -> anomaly Pp.(str "not a cached state (expired).") let assign id what = let open Vernacstate in - if VCS.get_state id <> Empty then () else + if VCS.get_state id <> EmptyState then () else try match what with | `Full s -> let s = @@ -896,7 +952,7 @@ end = struct (* {{{ *) ~src:(get_cached prev).proof ~tgt:s.proof } else s with VCS.Expired -> s in - VCS.set_state id (Valid s) + VCS.set_state id (FullState s) | `ProofOnly(ontop,(pstate,c1,c2,c3)) -> if is_cached_and_valid ontop then let s = get_cached ontop in @@ -912,7 +968,7 @@ end = struct (* {{{ *) st end } in - VCS.set_state id (Valid s) + VCS.set_state id (FullState s) with VCS.Expired -> () let exn_on id ~valid (e, info) = @@ -958,7 +1014,7 @@ end = struct (* {{{ *) with e -> let (e, info) = CErrors.push e in let good_id = !cur_id in - cur_id := Stateid.dummy; + invalidate_cur_state (); VCS.reached id; let ie = match Stateid.get info, safe_id with @@ -1130,7 +1186,7 @@ module Backtrack : sig val branches_of : Stateid.t -> backup (* Returns the state that the command should backtract to *) - val undo_vernac_classifier : vernac_control -> doc:doc -> Stateid.t * vernac_when + val undo_vernac_classifier : vernac_control -> doc:doc -> Stateid.t val get_prev_proof : doc:doc -> Stateid.t -> Proof.t option end = struct (* {{{ *) @@ -1205,30 +1261,30 @@ end = struct (* {{{ *) try match Vernacprop.under_control v with | VernacResetInitial -> - Stateid.initial, VtNow + Stateid.initial | VernacResetName {CAst.v=name} -> - let id = VCS.get_branch_pos (VCS.current_branch ()) in + let id = VCS.cur_tip () in (try let oid = fold_until (fun b (id,_,label,_,_) -> if b then `Stop id else `Cont (List.mem name label)) false id in - oid, VtNow + oid with Not_found -> - id, VtNow) + id) | VernacBack n -> - let id = VCS.get_branch_pos (VCS.current_branch ()) in + let id = VCS.cur_tip () in let oid = fold_until (fun n (id,_,_,_,_) -> if Int.equal n 0 then `Stop id else `Cont (n-1)) n id in - oid, VtNow + oid | VernacUndo n -> - let id = VCS.get_branch_pos (VCS.current_branch ()) in + let id = VCS.cur_tip () in let oid = fold_until back_tactic n id in - oid, VtLater + oid | VernacUndoTo _ | VernacRestart as e -> let m = match e with VernacUndoTo m -> m | _ -> 0 in - let id = VCS.get_branch_pos (VCS.current_branch ()) in + let id = VCS.cur_tip () in let vcs = match (VCS.get_info id).vcs_backup with | None, _ -> anomaly Pp.(str"Backtrack: tip with no vcs_backup.") @@ -1241,15 +1297,15 @@ 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 - oid, VtLater + oid | VernacAbortAll -> - let id = VCS.get_branch_pos (VCS.current_branch ()) in + let id = VCS.cur_tip () in let oid = fold_until (fun () (id,vcs,_,_,_) -> match Vcs_.branches vcs with [_] -> `Stop id | _ -> `Cont ()) () id in - oid, VtLater + oid | VernacBackTo id -> - Stateid.of_int id, VtNow + Stateid.of_int id | _ -> anomaly Pp.(str "incorrect VtMeta classification") with | Not_found -> @@ -2331,8 +2387,8 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = (Proofview.Goal.goal gl) goals_to_admit then Proofview.give_up else Proofview.tclUNIT () end in - match (VCS.get_info base_state).state with - | Valid { Vernacstate.proof } -> + match VCS.get_state base_state with + | FullState { Vernacstate.proof } -> Proof_global.unfreeze proof; Proof_global.with_current_proof (fun _ p -> feedback ~id:id Feedback.AddedAxiom; @@ -2469,7 +2525,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = VCS.create_proof_task_box nodes ~qed:id ~block_start; begin match brinfo, qed.fproof with | { VCS.kind = `Edit _ }, None -> assert false - | { VCS.kind = `Edit (_,_,_, okeep, _) }, Some (ofp, cancel) -> + | { VCS.kind = `Edit (_,_, okeep, _) }, Some (ofp, cancel) -> assert(redefine_qed = true); if okeep <> keep then msg_warning(strbrk("The command closing the proof changed. " @@ -2655,7 +2711,7 @@ let new_doc { doc_type ; iload_path; require_libs; stm_options } = (* We must reset the whole state before creating a document! *) State.restore_root_state (); - let doc = VCS.init doc_type Stateid.initial in + let doc = VCS.init doc_type Stateid.initial (Vernacstate.Parser.init ()) in (* Set load path; important, this has to happen before we declare the library below as [Declaremods/Library] will infer the module @@ -2723,16 +2779,8 @@ let observe ~doc id = let finish ~doc = let head = VCS.current_branch () in - let doc =observe ~doc (VCS.get_branch_pos head) in - VCS.print (); - (* EJGA: Setting here the proof state looks really wrong, and it - hides true bugs cf bug #5363. Also, what happens with observe? *) - (* Some commands may by side effect change the proof mode *) - (match VCS.get_branch head with - | { VCS.kind = `Edit (mode,_,_,_,_) } -> Proof_global.activate_proof_mode mode [@ocaml.warning "-3"] - | { VCS.kind = `Proof (mode, _) } -> Proof_global.activate_proof_mode mode [@ocaml.warning "-3"] - | _ -> () - ); doc + let doc = observe ~doc (VCS.get_branch_pos head) in + VCS.print (); doc let wait ~doc = let doc = observe ~doc (VCS.get_branch_pos VCS.Branch.master) in @@ -2809,12 +2857,14 @@ let merge_proof_branch ~valid ?id qast keep brname = match brinfo with | { VCS.kind = `Proof _ } -> VCS.checkout VCS.Branch.master; - let id = VCS.new_node ?id () in + let id = VCS.new_node ?id None () in + let parsing = Option.get @@ VCS.get_parsing_state (VCS.cur_tip ()) in VCS.merge id ~ours:(Qed (qed None)) brname; + VCS.set_parsing_state id parsing; VCS.delete_branch brname; - VCS.propagate_sideff ~action:CherryPickEnv; + VCS.propagate_qed (); `Ok - | { VCS.kind = `Edit (mode, qed_id, master_id, _,_) } -> + | { VCS.kind = `Edit (qed_id, master_id, _,_) } -> let ofp = match VCS.visit qed_id with | { step = `Qed ({ fproof }, _) } -> fproof @@ -2846,25 +2896,32 @@ let snapshot_vio ~doc ldir long_f_dot_vo = let reset_task_queue = Slaves.reset_task_queue (* Document building *) -let process_back_meta_command ~newtip ~head oid aast w = - let id = VCS.new_node ~id:newtip () in - let { mine; others } = Backtrack.branches_of oid in + +(* We process a meta command found in the document *) +let process_back_meta_command ~newtip ~head oid aast = let valid = VCS.get_branch_pos head in + let old_parsing = Option.get @@ VCS.get_parsing_state oid in + + (* Merge in and discard all the branches currently open that were not open in `oid` *) + let { mine; others } = Backtrack.branches_of oid in List.iter (fun branch -> if not (List.mem_assoc branch (mine::others)) then ignore(merge_proof_branch ~valid aast VtDrop branch)) (VCS.branches ()); + + (* We add a node on top of every branch, to represent state aliasing *) VCS.checkout_shallowest_proof_branch (); let head = VCS.current_branch () in List.iter (fun b -> - if not(VCS.Branch.equal b head) then begin - VCS.checkout b; - VCS.commit (VCS.new_node ()) (Alias (oid,aast)); - end) + VCS.checkout b; + let id = if (VCS.Branch.equal b head) then Some newtip else None in + let proof_mode = VCS.get_proof_mode @@ VCS.cur_tip () in + let id = VCS.new_node ?id proof_mode () in + VCS.commit id (Alias (oid,aast)); + VCS.set_parsing_state id old_parsing) (VCS.branches ()); VCS.checkout_shallowest_proof_branch (); - VCS.commit id (Alias (oid,aast)); - Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc); `Ok + Backtrack.record (); `Ok let get_allow_nested_proofs = Goptions.declare_bool_option_and_ref @@ -2873,6 +2930,7 @@ let get_allow_nested_proofs = ~key:Vernac_classifier.stm_allow_nested_proofs_option_name ~value:false +(** [process_transaction] adds a node in the document *) let process_transaction ~doc ?(newtip=Stateid.fresh ()) ({ verbose; loc; expr } as x) c = stm_pperr_endline (fun () -> str "{{{ processing: " ++ pr_ast x); @@ -2880,18 +2938,21 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ()) try let head = VCS.current_branch () in VCS.checkout head; + let head_parsing = + Option.get @@ VCS.(get_parsing_state (get_branch_pos head)) in + let proof_mode = VCS.(get_proof_mode (get_branch_pos head)) in let rc = begin stm_prerr_endline (fun () -> " classified as: " ^ Vernac_classifier.string_of_vernac_classification c); match c with (* Meta *) | VtMeta, _ -> - let id, w = Backtrack.undo_vernac_classifier expr ~doc in - process_back_meta_command ~newtip ~head id x w + let id = Backtrack.undo_vernac_classifier expr ~doc in + process_back_meta_command ~newtip ~head id x (* Query *) | VtQuery, w -> - let id = VCS.new_node ~id:newtip () in + let id = VCS.new_node ~id:newtip proof_mode () in let queue = if VCS.is_vio_doc () && VCS.((get_branch head).kind = `Master) && @@ -2899,10 +2960,11 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ()) then `SkipQueue else `MainQueue in VCS.commit id (mkTransCmd x [] false queue); - Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc); `Ok + VCS.set_parsing_state id head_parsing; + Backtrack.record (); assert (w == VtLater); `Ok (* Proof *) - | VtStartProof (mode, guarantee, names), w -> + | VtStartProof (guarantee, names), w -> if not (get_allow_nested_proofs ()) && VCS.proof_nesting () > 0 then "Nested proofs are not allowed unless you turn option Nested Proofs Allowed on." @@ -2912,39 +2974,22 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ()) |> Exninfo.iraise else - let id = VCS.new_node ~id:newtip () in + let proof_mode = Some (Vernacentries.get_default_proof_mode ()) in + let id = VCS.new_node ~id:newtip proof_mode () in let bname = VCS.mk_branch_name x in VCS.checkout VCS.Branch.master; if VCS.Branch.equal head VCS.Branch.master then begin VCS.commit id (Fork (x, bname, guarantee, names)); - VCS.branch bname (`Proof (mode, VCS.proof_nesting () + 1)) + VCS.branch bname (`Proof (VCS.proof_nesting () + 1)) end else begin - VCS.branch bname (`Proof (mode, VCS.proof_nesting () + 1)); + VCS.branch bname (`Proof (VCS.proof_nesting () + 1)); VCS.merge id ~ours:(Fork (x, bname, guarantee, names)) head end; - Proof_global.activate_proof_mode mode [@ocaml.warning "-3"]; - Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc); `Ok - | VtProofMode _, VtLater -> - anomaly(str"VtProofMode must be executed VtNow.") - | VtProofMode mode, VtNow -> - let id = VCS.new_node ~id:newtip () in - VCS.commit id (mkTransCmd x [] false `MainQueue); - List.iter - (fun bn -> match VCS.get_branch bn with - | { VCS.root; kind = `Master; pos } -> () - | { VCS.root; kind = `Proof(_,d); pos } -> - VCS.delete_branch bn; - VCS.branch ~root ~pos bn (`Proof(mode,d)) - | { VCS.root; kind = `Edit(_,f,q,k,ob); pos } -> - VCS.delete_branch bn; - VCS.branch ~root ~pos bn (`Edit(mode,f,q,k,ob))) - (VCS.branches ()); - VCS.checkout_shallowest_proof_branch (); - Backtrack.record (); - ignore(finish ~doc:dummy_doc); - `Ok + VCS.set_parsing_state id head_parsing; + Backtrack.record (); assert (w == VtLater); `Ok + | VtProofStep { parallel; proof_block_detection = cblock }, w -> - let id = VCS.new_node ~id:newtip () in + let id = VCS.new_node ~id:newtip proof_mode () in let queue = match parallel with | `Yes(solve,abstract) -> `TacQueue (solve, abstract, ref false) @@ -2954,21 +2999,25 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ()) If/when and UI will make something useful with this piece of info, detection should occur here. detect_proof_block id cblock; *) - Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc); `Ok + VCS.set_parsing_state id head_parsing; + Backtrack.record (); assert (w == VtLater); `Ok + | VtQed keep, w -> let valid = VCS.get_branch_pos head in - let rc = merge_proof_branch ~valid ~id:newtip x keep head in + let rc = + merge_proof_branch ~valid ~id:newtip x keep head in VCS.checkout_shallowest_proof_branch (); - Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc); + Backtrack.record (); assert (w == VtLater); rc (* Side effect in a (still open) proof is replayed on all branches*) | VtSideff l, w -> - let id = VCS.new_node ~id:newtip () in - begin match (VCS.get_branch head).VCS.kind with - | `Edit _ -> VCS.commit id (mkTransCmd x l true `MainQueue); - | `Master -> VCS.commit id (mkTransCmd x l false `MainQueue); - | `Proof _ -> + let id = VCS.new_node ~id:newtip proof_mode () in + let new_ids = + match (VCS.get_branch head).VCS.kind with + | `Edit _ -> VCS.commit id (mkTransCmd x l true `MainQueue); [] + | `Master -> VCS.commit id (mkTransCmd x l false `MainQueue); [] + | `Proof _ -> VCS.checkout VCS.Branch.master; VCS.commit id (mkTransCmd x l true `MainQueue); (* We can't replay a Definition since universes may be differently @@ -2976,10 +3025,27 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ()) let action = match Vernacprop.under_control x.expr with | VernacDefinition(_, _, DefineBody _) -> CherryPickEnv | _ -> ReplayCommand x in - VCS.propagate_sideff ~action; - end; + VCS.propagate_sideff ~action + in VCS.checkout_shallowest_proof_branch (); - Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc); `Ok + Backtrack.record (); + let parsing_state = + begin match w with + | VtNow -> + (* We need to execute to get the new parsing state *) + ignore(finish ~doc:dummy_doc); + let parsing = Vernacstate.Parser.cur_state () in + (* If execution has not been put in cache, we need to save the parsing state *) + if (VCS.get_info id).state == EmptyState then VCS.set_parsing_state id parsing; + parsing + | VtLater -> VCS.set_parsing_state id head_parsing; head_parsing + end + in + (* We save the parsing state on non-master branches *) + List.iter (fun id -> + if (VCS.get_info id).state == EmptyState then + VCS.set_parsing_state id parsing_state) new_ids; + `Ok (* Unknown: we execute it, check for open goals and propagate sideeff *) | VtUnknown, VtNow -> @@ -2991,7 +3057,7 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ()) |> State.exn_on ~valid:Stateid.dummy Stateid.dummy |> Exninfo.iraise else - let id = VCS.new_node ~id:newtip () in + let id = VCS.new_node ~id:newtip proof_mode () in let head_id = VCS.get_branch_pos head in let _st : unit = Reach.known_state ~doc ~cache:true head_id in (* ensure it is ok *) let step () = @@ -3009,9 +3075,8 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ()) | VernacInstance (_,_ , None, _) -> GuaranteesOpacity | _ -> Doesn'tGuaranteeOpacity in VCS.commit id (Fork (x,bname,opacity_of_produced_term (Vernacprop.under_control x.expr),[])); - let proof_mode = default_proof_mode () in - VCS.branch bname (`Proof (proof_mode, VCS.proof_nesting () + 1)); - Proof_global.activate_proof_mode proof_mode [@ocaml.warning "-3"]; + VCS.set_proof_mode id (Some (Vernacentries.get_default_proof_mode ())); + VCS.branch bname (`Proof (VCS.proof_nesting () + 1)); end else begin begin match (VCS.get_branch head).VCS.kind with | `Edit _ -> VCS.commit id (mkTransCmd x [] in_proof `MainQueue); @@ -3019,7 +3084,7 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ()) | `Proof _ -> VCS.commit id (mkTransCmd x [] in_proof `MainQueue); (* We hope it can be replayed, but we can't really know *) - VCS.propagate_sideff ~action:(ReplayCommand x); + ignore(VCS.propagate_sideff ~action:(ReplayCommand x)); end; VCS.checkout_shallowest_proof_branch (); end in @@ -3028,6 +3093,17 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ()) | VtUnknown, VtLater -> anomaly(str"classifier: VtUnknown must imply VtNow.") + + | VtProofMode pm, VtNow -> + let proof_mode = Pvernac.lookup_proof_mode pm in + let id = VCS.new_node ~id:newtip proof_mode () in + VCS.commit id (mkTransCmd x [] false `MainQueue); + VCS.set_parsing_state id head_parsing; + Backtrack.record (); `Ok + + | VtProofMode _, VtLater -> + anomaly(str"classifier: VtProofMode must imply VtNow.") + end in let pr_rc rc = match rc with | `Ok -> Pp.(seq [str "newtip ("; str (Stateid.to_string (VCS.cur_tip ())); str ")"]) @@ -3051,45 +3127,10 @@ let get_ast ~doc id = let stop_worker n = Slaves.cancel_worker n -(* We must parse on top of a state id, it should be something like: - - - get parsing information for that state. - - feed the parsable / parser with the right parsing information. - - call the parser - - Now, the invariant in ensured by the callers, but this is a bit - problematic. -*) -exception End_of_input - -let parse_sentence ~doc sid pa = - (* XXX: Should this restore the previous state? - Using reach here to try to really get to the - proper state makes the error resilience code fail *) - (* Reach.known_state ~cache:`Yes sid; *) - let cur_tip = VCS.cur_tip () in - let real_tip = !State.cur_id in - if not (Stateid.equal sid cur_tip) then - user_err ~hdr:"Stm.parse_sentence" - (str "Currently, the parsing api only supports parsing at the tip of the document." ++ fnl () ++ - str "You wanted to parse at: " ++ str (Stateid.to_string sid) ++ - str " but the current tip is: " ++ str (Stateid.to_string cur_tip)) ; - if not (Stateid.equal sid real_tip) && !Flags.debug && !stm_debug then - Feedback.msg_debug - (str "Warning, the real tip doesn't match the current tip." ++ - str "You wanted to parse at: " ++ str (Stateid.to_string sid) ++ - str " but the real tip is: " ++ str (Stateid.to_string real_tip) ++ fnl () ++ - str "This is usually due to use of Stm.observe to evaluate a state different than the tip. " ++ - str "All is good if not parsing changes occur between the two states, however if they do, a problem might occur."); - Flags.with_option Flags.we_are_parsing (fun () -> - try - match Pcoq.Entry.parse Pvernac.main_entry pa with - | None -> raise End_of_input - | Some (loc, cmd) -> CAst.make ~loc cmd - with e when CErrors.noncritical e -> - let (e, info) = CErrors.push e in - Exninfo.iraise (e, info)) - () +let parse_sentence ~doc sid ~entry pa = + let ps = Option.get @@ VCS.get_parsing_state sid in + let proof_mode = VCS.get_proof_mode sid in + Vernacstate.Parser.parse ps (entry proof_mode) pa (* You may need to know the len + indentation of previous command to compute * the indentation of the current one. @@ -3153,20 +3194,20 @@ let query ~doc ~at ~route s = State.purify (fun s -> if Stateid.equal at Stateid.dummy then ignore(finish ~doc:dummy_doc) else Reach.known_state ~doc ~cache:true at; - try - while true do - let { CAst.loc; v=ast } = parse_sentence ~doc at s in - let indentation, strlen = compute_indentation ?loc at in - let st = State.get_cached at in - let aast = { verbose = true; indentation; strlen; loc; expr = ast } in - ignore(stm_vernac_interp ~route at st aast) - done; - with - | End_of_input -> () - | exn -> - let iexn = CErrors.push exn in - Exninfo.iraise iexn - ) + let rec loop () = + match parse_sentence ~doc at ~entry:Pvernac.main_entry s with + | None -> () + | Some (loc, ast) -> + let indentation, strlen = compute_indentation ~loc at in + let st = State.get_cached at in + let aast = { + verbose = true; indentation; strlen; + loc = Some loc; expr = ast } in + ignore(stm_vernac_interp ~route at st aast); + loop () + in + loop () + ) s let edit_at ~doc id = @@ -3204,21 +3245,21 @@ let edit_at ~doc id = | { step = `Sideff (ReplayCommand _,id) } -> id | { step = `Sideff _ } -> tip | { next } -> master_for_br root next in - let reopen_branch start at_id mode qed_id tip old_branch = + let reopen_branch start at_id qed_id tip old_branch = let master_id, cancel_switch, keep = (* Hum, this should be the real start_id in the cluster and not next *) match VCS.visit qed_id with | { step = `Qed ({ fproof = Some (_,cs); keep },_) } -> start, cs, keep | _ -> anomaly (str "ProofTask not ending with Qed.") in VCS.branch ~root:master_id ~pos:id - VCS.edit_branch (`Edit (mode, qed_id, master_id, keep, old_branch)); + VCS.edit_branch (`Edit (qed_id, master_id, keep, old_branch)); VCS.delete_boxes_of id; cancel_switch := true; Reach.known_state ~doc ~cache:(VCS.is_interactive ()) id; VCS.checkout_shallowest_proof_branch (); `Focus { stop = qed_id; start = master_id; tip } in let no_edit = function - | `Edit (pm, _,_,_,_) -> `Proof(pm,1) + | `Edit (_,_,_,_) -> `Proof 1 | x -> x in let backto id bn = List.iter VCS.delete_branch (VCS.branches ()); @@ -3244,17 +3285,17 @@ let edit_at ~doc id = let focused = List.exists ((=) VCS.edit_branch) (VCS.branches ()) in let branch_info = match snd (VCS.get_info id).vcs_backup with - | Some{ mine = bn, { VCS.kind = `Proof(m,_) }} -> Some(m,bn) - | Some{ mine = _, { VCS.kind = `Edit(m,_,_,_,bn) }} -> Some (m,bn) + | Some{ mine = bn, { VCS.kind = `Proof _ }} -> Some bn + | Some{ mine = _, { VCS.kind = `Edit(_,_,_,bn) }} -> Some bn | _ -> None in match focused, VCS.proof_task_box_of id, branch_info with | _, Some _, None -> assert false - | false, Some { qed = qed_id ; lemma = start }, Some(mode,bn) -> + | false, Some { qed = qed_id ; lemma = start }, Some bn -> let tip = VCS.cur_tip () in if has_failed qed_id && is_pure qed_id && not !cur_opt.async_proofs_never_reopen_branch - then reopen_branch start id mode qed_id tip bn + then reopen_branch start id qed_id tip bn else backto id (Some bn) - | true, Some { qed = qed_id }, Some(mode,bn) -> + | true, Some { qed = qed_id }, Some bn -> if on_cur_branch id then begin assert false end else if is_ancestor_of_cur_branch id then begin @@ -3273,7 +3314,7 @@ let edit_at ~doc id = end else begin anomaly(str"Cannot leave an `Edit branch open.") end - | false, None, Some(_,bn) -> backto id (Some bn) + | false, None, Some bn -> backto id (Some bn) | false, None, None -> backto id None in VCS.print (); diff --git a/stm/stm.mli b/stm/stm.mli index b6071fa56b..821ab59a43 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -93,16 +93,17 @@ val init_core : unit -> unit (** [new_doc opt] Creates a new document with options [opt] *) val new_doc : stm_init_options -> doc * Stateid.t -(** [parse_sentence sid pa] Reads a sentence from [pa] with parsing - state [sid] Returns [End_of_input] if the stream ends *) -val parse_sentence : doc:doc -> Stateid.t -> Pcoq.Parsable.t -> - Vernacexpr.vernac_control CAst.t +(** [parse_sentence sid entry pa] Reads a sentence from [pa] with parsing state + [sid] and non terminal [entry]. [entry] receives in input the current proof + mode. [sid] should be associated with a valid parsing state (which may not + be the case if an error was raised at parsing time). *) +val parse_sentence : + doc:doc -> Stateid.t -> + entry:(Pvernac.proof_mode option -> 'a Pcoq.Entry.t) -> Pcoq.Parsable.t -> 'a (* Reminder: A parsable [pa] is constructed using [Pcoq.Parsable.t stream], where [stream : char Stream.t]. *) -exception End_of_input - (* [add ~ontop ?newtip verbose cmd] adds a new command [cmd] ontop of the state [ontop]. The [ontop] parameter just asserts that the GUI is on diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 09f531ce13..710ddb5571 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -15,8 +15,6 @@ open CAst open Vernacextend open Vernacexpr -let default_proof_mode () = Proof_global.get_default_proof_mode_name () [@ocaml.warning "-3"] - let string_of_parallel = function | `Yes (solve,abs) -> "par" ^ if solve then "solve" else "" ^ if abs then "abs" else "" @@ -32,9 +30,9 @@ let string_of_vernac_type = function | VtProofStep { parallel; proof_block_detection } -> "ProofStep " ^ string_of_parallel parallel ^ Option.default "" proof_block_detection - | VtProofMode s -> "ProofMode " ^ s | VtQuery -> "Query" | VtMeta -> "Meta " + | VtProofMode _ -> "Proof Mode" let string_of_vernac_when = function | VtLater -> "Later" @@ -57,7 +55,7 @@ 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; - Proof_global.proof_mode_opt_name; + Vernacentries.proof_mode_opt_name; ] let classify_vernac e = @@ -97,15 +95,15 @@ let classify_vernac e = | VernacSetOption (_, ["Default";"Proof";"Using"],_) -> VtSideff [], VtNow (* StartProof *) | VernacDefinition ((Decl_kinds.DoDischarge,_),({v=i},_),ProveBody _) -> - VtStartProof(default_proof_mode (),Doesn'tGuaranteeOpacity, idents_of_name i), VtLater + VtStartProof(Doesn'tGuaranteeOpacity, idents_of_name i), VtLater | VernacDefinition (_,({v=i},_),ProveBody _) -> let guarantee = if poly then Doesn'tGuaranteeOpacity else GuaranteesOpacity in - VtStartProof(default_proof_mode (),guarantee, idents_of_name i), VtLater + VtStartProof(guarantee, idents_of_name i), VtLater | VernacStartTheoremProof (_,l) -> let ids = List.map (fun (({v=i}, _), _) -> i) l in let guarantee = if poly then Doesn'tGuaranteeOpacity else GuaranteesOpacity in - VtStartProof (default_proof_mode (),guarantee,ids), VtLater + VtStartProof (guarantee,ids), VtLater | VernacFixpoint (discharge,l) -> let guarantee = if discharge = Decl_kinds.DoDischarge || poly then Doesn'tGuaranteeOpacity @@ -115,7 +113,7 @@ let classify_vernac e = List.fold_left (fun (l,b) ((({v=id},_),_,_,_,p),_) -> id::l, b || p = None) ([],false) l in if open_proof - then VtStartProof (default_proof_mode (),guarantee,ids), VtLater + then VtStartProof (guarantee,ids), VtLater else VtSideff ids, VtLater | VernacCoFixpoint (discharge,l) -> let guarantee = @@ -126,7 +124,7 @@ let classify_vernac e = List.fold_left (fun (l,b) ((({v=id},_),_,_,p),_) -> id::l, b || p = None) ([],false) l in if open_proof - then VtStartProof (default_proof_mode (),guarantee,ids), VtLater + then VtStartProof (guarantee,ids), VtLater else VtSideff ids, VtLater (* Sideff: apply to all open branches. usually run on master only *) | VernacAssumption (_,_,l) -> @@ -184,8 +182,8 @@ let classify_vernac e = | VernacSyntacticDefinition _ | VernacRequire _ | VernacImport _ | VernacInclude _ | VernacDeclareMLModule _ - | VernacContext _ (* TASSI: unsure *) - | VernacProofMode _ -> VtSideff [], VtNow + | VernacContext _ (* TASSI: unsure *) -> VtSideff [], VtNow + | VernacProofMode pm -> VtProofMode pm, VtNow (* These are ambiguous *) | VernacInstance _ -> VtUnknown, VtNow (* Stm will install a new classifier to handle these *) @@ -211,10 +209,10 @@ let classify_vernac e = | VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *) (match static_control_classifier e with | ( VtQuery | VtProofStep _ | VtSideff _ - | VtProofMode _ | VtMeta), _ as x -> x + | VtMeta), _ as x -> x | VtQed _, _ -> VtProofStep { parallel = `No; proof_block_detection = None }, - VtNow - | (VtStartProof _ | VtUnknown), _ -> VtQuery, VtLater) + VtLater + | (VtStartProof _ | VtUnknown | VtProofMode _), _ -> VtQuery, VtLater) in static_control_classifier e -- cgit v1.2.3