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 --- toplevel/coqloop.ml | 23 ++++++++------- toplevel/g_toplevel.mlg | 18 ++++++------ toplevel/vernac.ml | 74 +++++++++++++++++++------------------------------ 3 files changed, 52 insertions(+), 63 deletions(-) (limited to 'toplevel') diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index e58b9ccac7..cdbe444e5b 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -243,7 +243,7 @@ let set_prompt prompt = let parse_to_dot = let rec dot st = match Stream.next st with | Tok.KEYWORD ("."|"...") -> () - | Tok.EOI -> raise Stm.End_of_input + | Tok.EOI -> () | _ -> dot st in Pcoq.Entry.of_parser "Coqtoplevel.dot" dot @@ -257,12 +257,12 @@ let rec discard_to_dot () = Pcoq.Entry.parse parse_to_dot top_buffer.tokens with | Gramlib.Plexing.Error _ | CLexer.Error.E _ -> discard_to_dot () - | Stm.End_of_input -> raise Stm.End_of_input | e when CErrors.noncritical e -> () let read_sentence ~state input = (* XXX: careful with ignoring the state Eugene!*) - try G_toplevel.parse_toplevel input + let open Vernac.State in + try Stm.parse_sentence ~doc:state.doc state.sid ~entry:G_toplevel.vernac_toplevel input with reraise -> let reraise = CErrors.push reraise in discard_to_dot (); @@ -366,7 +366,6 @@ let top_goal_print ~doc c oldp newp = let msg = CErrors.iprint (e, info) in TopErr.print_error_for_buffer ?loc Feedback.Error msg top_buffer -(* Careful to keep this loop tail-rec *) let rec vernac_loop ~state = let open CAst in let open Vernac.State in @@ -379,26 +378,30 @@ let rec vernac_loop ~state = try let input = top_buffer.tokens in match read_sentence ~state input with - | {v=VernacBacktrack(bid,_,_)} -> + | Some { v = VernacBacktrack(bid,_,_) } -> let bid = Stateid.of_int bid in let doc, res = Stm.edit_at ~doc:state.doc bid in assert (res = `NewTip); let state = { state with doc; sid = bid } in vernac_loop ~state - | {v=VernacQuit} -> + | Some { v = VernacQuit } -> exit 0 - | {v=VernacDrop} -> + + | Some { v = VernacDrop } -> if Mltop.is_ocaml_top() then (drop_last_doc := Some state; state) else (Feedback.msg_warning (str "There is no ML toplevel."); vernac_loop ~state) - | {v=VernacControl c; loc} -> + + | Some { v = VernacControl c; loc } -> let nstate = Vernac.process_expr ~state (make ?loc c) in top_goal_print ~doc:state.doc c state.proof nstate.proof; vernac_loop ~state:nstate + + | None -> + top_stderr (fnl ()); exit 0 + with - | Stm.End_of_input -> - top_stderr (fnl ()); exit 0 (* Exception printing should be done by the feedback listener, however this is not yet ready so we rely on the exception for now. *) diff --git a/toplevel/g_toplevel.mlg b/toplevel/g_toplevel.mlg index 5aba3d6b0b..7f1cca277e 100644 --- a/toplevel/g_toplevel.mlg +++ b/toplevel/g_toplevel.mlg @@ -21,7 +21,7 @@ type vernac_toplevel = | VernacControl of vernac_control module Toplevel_ : sig - val vernac_toplevel : vernac_toplevel CAst.t Entry.t + val vernac_toplevel : vernac_toplevel CAst.t option Entry.t end = struct let gec_vernac s = Entry.create ("toplevel:" ^ s) let vernac_toplevel = gec_vernac "vernac_toplevel" @@ -34,14 +34,14 @@ open Toplevel_ GRAMMAR EXTEND Gram GLOBAL: vernac_toplevel; vernac_toplevel: FIRST - [ [ IDENT "Drop"; "." -> { CAst.make VernacDrop } - | IDENT "Quit"; "." -> { CAst.make VernacQuit } + [ [ IDENT "Drop"; "." -> { Some (CAst.make VernacDrop) } + | IDENT "Quit"; "." -> { Some (CAst.make VernacQuit) } | IDENT "Backtrack"; n = natural ; m = natural ; p = natural; "." -> - { CAst.make (VernacBacktrack (n,m,p)) } - | cmd = Pvernac.main_entry -> + { Some (CAst.make (VernacBacktrack (n,m,p))) } + | cmd = Pvernac.Vernac_.main_entry -> { match cmd with - | None -> raise Stm.End_of_input - | Some (loc,c) -> CAst.make ~loc (VernacControl c) } + | None -> None + | Some (loc,c) -> Some (CAst.make ~loc (VernacControl c)) } ] ] ; @@ -49,6 +49,8 @@ END { -let parse_toplevel pa = Pcoq.Entry.parse vernac_toplevel pa +let vernac_toplevel pm = + Pvernac.Unsafe.set_tactic_entry pm; + vernac_toplevel } diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index d8465aac27..45ca658857 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -68,10 +68,8 @@ let interp_vernac ~check ~interactive ~state ({CAst.loc;_} as com) = if ntip <> `NewTip then anomaly (str "vernac.ml: We got an unfocus operation on the toplevel!"); - (* Due to bug #5363 we cannot use observe here as we should, - it otherwise reveals bugs *) - (* Stm.observe nsid; *) - let ndoc = if check then Stm.finish ~doc else doc in + (* Force the command *) + let ndoc = if check then Stm.observe ~doc nsid else doc in let new_proof = Proof_global.give_me_the_proof_opt () in { state with doc = ndoc; sid = nsid; proof = new_proof; } with reraise -> @@ -92,51 +90,37 @@ let load_vernac_core ~echo ~check ~interactive ~state file = let in_echo = if echo then Some (open_utf8_file_in file) else None in let input_cleanup () = close_in in_chan; Option.iter close_in in_echo in - let in_pa = Pcoq.Parsable.make ~file:(Loc.InFile file) (Stream.of_channel in_chan) in - let rstate = ref state in - (* For beautify, list of parsed sids *) - let rids = ref [] in + let in_pa = + Pcoq.Parsable.make ~file:(Loc.InFile file) (Stream.of_channel in_chan) in let open State in - try - (* we go out of the following infinite loop when a End_of_input is - * raised, which means that we raised the end of the file being loaded *) - while true do - let { CAst.loc; _ } as ast = - Stm.parse_sentence ~doc:!rstate.doc !rstate.sid in_pa - (* If an error in parsing occurs, we propagate the exception - so the caller of load_vernac will take care of it. However, - in the future it could be possible that we want to handle - all the errors as feedback events, thus in this case we - should relay the exception here for convenience. A - possibility is shown below, however we may want to refactor - this code: - - try Stm.parse_sentence !rsid in_pa - with - | any when not is_end_of_input any -> - let (e, info) = CErrors.push any in - let loc = Loc.get_loc info in - let msg = CErrors.iprint (e, info) in - Feedback.msg_error ?loc msg; - iraise (e, info) - *) - in - (* Printing of vernacs *) - Option.iter (vernac_echo ?loc) in_echo; - - checknav_simple ast; - let state = Flags.silently (interp_vernac ~check ~interactive ~state:!rstate) ast in - rids := state.sid :: !rids; - rstate := state; - done; - input_cleanup (); - !rstate, !rids, Pcoq.Parsable.comment_state in_pa + + (* ids = For beautify, list of parsed sids *) + let rec loop state ids = + match + Stm.parse_sentence + ~doc:state.doc ~entry:Pvernac.main_entry state.sid in_pa + with + | None -> + input_cleanup (); + state, ids, Pcoq.Parsable.comment_state in_pa + | Some (loc, ast) -> + let ast = CAst.make ~loc ast in + + (* Printing of AST for -compile-verbose *) + Option.iter (vernac_echo ~loc) in_echo; + + checknav_simple ast; + + let state = + Flags.silently (interp_vernac ~check ~interactive ~state) ast in + + loop state (state.sid :: ids) + in + try loop state [] with any -> (* whatever the exception *) let (e, info) = CErrors.push any in input_cleanup (); - match e with - | Stm.End_of_input -> !rstate, !rids, Pcoq.Parsable.comment_state in_pa - | reraise -> iraise (e, info) + iraise (e, info) let process_expr ~state loc_ast = checknav_deep loc_ast; -- cgit v1.2.3