From 75f569f35fbbbbab5a4629eaf3385335a3024e0b Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 11 Mar 2018 03:16:09 +0100 Subject: [vernac] Move `Quit` and `Drop` to the toplevel layer. This is a first step towards moving REPL-specific commands out of the core layers. In particular, we remove `Quit` and `Drop` from the core vernacular to specific toplevel-level parsing rules. --- toplevel/coqinit.ml | 6 +-- toplevel/coqinit.mli | 4 +- toplevel/coqloop.ml | 106 ++++++++++++++++++++---------------------------- toplevel/coqloop.mli | 5 +-- toplevel/coqtop.ml | 16 ++++---- toplevel/g_toplevel.ml4 | 43 ++++++++++++++++++++ toplevel/toplevel.mllib | 1 + toplevel/vernac.ml | 30 +++++++------- toplevel/vernac.mli | 5 ++- 9 files changed, 121 insertions(+), 95 deletions(-) create mode 100644 toplevel/g_toplevel.ml4 (limited to 'toplevel') diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 96a0bd5ec..3e7a83085 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -23,12 +23,12 @@ let set_debug () = let rcdefaultname = "coqrc" -let load_rcfile ~rcfile ~time ~state = +let load_rcfile ~rcfile ~state = try match rcfile with | Some rcfile -> if CUnix.file_readable_p rcfile then - Vernac.load_vernac ~time ~echo:false ~interactive:false ~check:true ~state rcfile + Vernac.load_vernac ~echo:false ~interactive:false ~check:true ~state rcfile else raise (Sys_error ("Cannot read rcfile: "^ rcfile)) | None -> try @@ -39,7 +39,7 @@ let load_rcfile ~rcfile ~time ~state = Envars.home ~warn / "."^rcdefaultname^"."^Coq_config.version; Envars.home ~warn / "."^rcdefaultname ] in - Vernac.load_vernac ~time ~echo:false ~interactive:false ~check:true ~state inferedrc + Vernac.load_vernac ~echo:false ~interactive:false ~check:true ~state inferedrc with Not_found -> state (* Flags.if_verbose diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli index 71b5523cd..c891e736b 100644 --- a/toplevel/coqinit.mli +++ b/toplevel/coqinit.mli @@ -12,12 +12,12 @@ val set_debug : unit -> unit -val load_rcfile : rcfile:(string option) -> time:bool -> state:Vernac.State.t -> Vernac.State.t +val load_rcfile : rcfile:(string option) -> state:Vernac.State.t -> Vernac.State.t val init_ocaml_path : unit -> unit (* LoadPath for toploop toplevels *) -val toplevel_init_load_path : unit -> Mltop.coq_path list +val toplevel_init_load_path : unit -> Mltop.coq_path list (* LoadPath for Coq user libraries *) val libs_init_load_path : load_init:bool -> Mltop.coq_path list diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index a103cfe7f..64d839f18 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -261,8 +261,8 @@ let rec discard_to_dot () = | e when CErrors.noncritical e -> () let read_sentence ~state input = - let open Vernac.State in - try Stm.parse_sentence ~doc:state.doc state.sid input + (* XXX: careful with ignoring the state Eugene!*) + try G_toplevel.parse_toplevel input with reraise -> let reraise = CErrors.push reraise in discard_to_dot (); @@ -293,40 +293,6 @@ let coqloop_feed (fb : Feedback.feedback) = let open Feedback in | Message (lvl,loc,msg) -> TopErr.print_error_for_buffer ?loc lvl msg top_buffer -(** [do_vernac] reads and executes a toplevel phrase, and print error - messages when an exception is raised, except for the following: - - Drop: kill the Coq toplevel, going down to the Caml toplevel if it exists. - Otherwise, exit. - - End_of_input: Ctrl-D was typed in, we will quit. - - In particular, this is normally the only place where a Sys.Break - is caught and handled (i.e. not re-raised). -*) - -let do_vernac ~time ~state = - let open Vernac.State in - top_stderr (fnl()); - if !print_emacs then top_stderr (str (top_buffer.prompt state.doc)); - resynch_buffer top_buffer; - try - let input = (top_buffer.tokens, None) in - Vernac.process_expr ~time ~state (read_sentence ~state (fst input)) - with - | Stm.End_of_input | CErrors.Quit -> - top_stderr (fnl ()); raise CErrors.Quit - | CErrors.Drop -> (* Last chance *) - if Mltop.is_ocaml_top() then raise CErrors.Drop - else (Feedback.msg_warning (str "There is no ML toplevel."); state) - (* Exception printing should be done by the feedback listener, - however this is not yet ready so we rely on the exception for - now. *) - | any -> - let (e, info) = CErrors.push any in - let loc = Loc.get_loc info in - let msg = CErrors.iprint (e, info) in - TopErr.print_error_for_buffer ?loc Feedback.Error msg top_buffer; - state - (** Main coq loop : read vernacular expressions until Drop is entered. Ctrl-C is handled internally as Sys.Break instead of aborting Coq. Normally, the only exceptions that can come out of [do_vernac] and @@ -359,37 +325,55 @@ let cproof p1 p2 = let drop_last_doc = ref None -let rec loop ~time ~state = +(* Careful to keep this loop tail-rec *) +let rec vernac_loop ~state = + let open CAst in let open Vernac.State in - Sys.catch_break true; + let open G_toplevel in + loop_flush_all (); + top_stderr (fnl()); + if !print_emacs then top_stderr (str (top_buffer.prompt state.doc)); + resynch_buffer top_buffer; + (* execute one command *) try - reset_input_buffer state.doc stdin top_buffer; - (* Be careful to keep this loop tail-recursive *) - let rec vernac_loop ~state = - let nstate = do_vernac ~time ~state in + let input = top_buffer.tokens in + match read_sentence ~state input with + | {v=VernacQuit} -> + exit 0 + | {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} -> + let nstate = Vernac.process_expr ~state (make ?loc c) in let proof_changed = not (Option.equal cproof nstate.proof state.proof) in let print_goals = not !Flags.quiet && proof_changed && Proof_global.there_are_pending_proofs () in if print_goals then Feedback.msg_notice (pr_open_cur_subgoals ()); - loop_flush_all (); vernac_loop ~state:nstate - (* We recover the current stateid, threading from the caller is - not possible due exceptions. *) - in vernac_loop ~state with - | CErrors.Drop -> - (* Due to using exceptions as a form of control, state here goes - out of sync as [do_vernac] will never return. We must thus do - this hack until we make `Drop` a toplevel-only command. See - bug #6872. *) - let state = { state with sid = Stm.get_current_state ~doc:state.doc } in - drop_last_doc := Some state; - state - | CErrors.Quit -> exit 0 + | 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. *) + | any -> + let (e, info) = CErrors.push any in + let loc = Loc.get_loc info in + let msg = CErrors.iprint (e, info) in + TopErr.print_error_for_buffer ?loc Feedback.Error msg top_buffer; + vernac_loop ~state + +let rec loop ~state = + let open Vernac.State in + Sys.catch_break true; + try + reset_input_buffer state.doc stdin top_buffer; + vernac_loop ~state + with | any -> - top_stderr (str "Anomaly: main loop exited with exception: " ++ - str (Printexc.to_string any) ++ - fnl() ++ - str"Please report" ++ - strbrk" at " ++ str Coq_config.wwwbugtracker ++ str "."); - loop ~time ~state + top_stderr + (hov 0 (str "Anomaly: main loop exited with exception:" ++ spc () ++ + str (Printexc.to_string any)) ++ spc () ++ + hov 0 (str "Please report at " ++ str Coq_config.wwwbugtracker ++ str ".")); + loop ~state diff --git a/toplevel/coqloop.mli b/toplevel/coqloop.mli index bbb9b1383..39a9de4f8 100644 --- a/toplevel/coqloop.mli +++ b/toplevel/coqloop.mli @@ -32,11 +32,8 @@ val set_prompt : (unit -> string) -> unit (** Toplevel feedback printer. *) val coqloop_feed : Feedback.feedback -> unit -(** Parse and execute one vernac command. *) -val do_vernac : time:bool -> state:Vernac.State.t -> Vernac.State.t - (** Main entry point of Coq: read and execute vernac commands. *) -val loop : time:bool -> state:Vernac.State.t -> Vernac.State.t +val loop : state:Vernac.State.t -> Vernac.State.t (** Last document seen after `Drop` *) val drop_last_doc : Vernac.State.t option ref diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index cd831c05c..a08cfa9f4 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -45,7 +45,7 @@ let console_toploop_run opts ~state = Flags.if_verbose warning "Dumpglob cannot be used in interactive mode."; Dumpglob.noglob () end; - let _ = Coqloop.loop ~time:opts.time ~state in + let _ = Coqloop.loop ~state in (* Initialise and launch the Ocaml toplevel *) Coqinit.init_ocaml_path(); Mltop.ocaml_toploop(); @@ -95,7 +95,7 @@ let load_vernacular opts ~state = (fun state (f_in, echo) -> let s = Loadpath.locate_file f_in in (* Should make the beautify logic clearer *) - let load_vernac f = Vernac.load_vernac ~time:opts.time ~echo ~interactive:false ~check:true ~state f in + let load_vernac f = Vernac.load_vernac ~echo ~interactive:false ~check:true ~state f in if !Flags.beautify then Flags.with_option Flags.beautify_file load_vernac f_in else load_vernac s @@ -103,7 +103,7 @@ let load_vernacular opts ~state = let load_init_vernaculars opts ~state = let state = if opts.load_rcfile then - Coqinit.load_rcfile ~rcfile:opts.rcfile ~time:opts.time ~state + Coqinit.load_rcfile ~rcfile:opts.rcfile ~state else begin Flags.if_verbose Feedback.msg_info (str"Skipping rcfile loading."); state @@ -223,7 +223,7 @@ let compile opts ~echo ~f_in ~f_out = iload_path; require_libs; stm_options; }) in - let state = { doc; sid; proof = None } in + let state = { doc; sid; proof = None; time = opts.time } in let state = load_init_vernaculars opts ~state in let ldir = Stm.get_ldir ~doc:state.doc in Aux_file.(start_aux_file @@ -232,7 +232,7 @@ let compile opts ~echo ~f_in ~f_out = Dumpglob.start_dump_glob ~vfile:long_f_dot_v ~vofile:long_f_dot_vo; Dumpglob.dump_string ("F" ^ Names.DirPath.to_string ldir ^ "\n"); let wall_clock1 = Unix.gettimeofday () in - let state = Vernac.load_vernac ~time:opts.time ~echo ~check:true ~interactive:false ~state long_f_dot_v in + let state = Vernac.load_vernac ~echo ~check:true ~interactive:false ~state long_f_dot_v in let _doc = Stm.join ~doc:state.doc in let wall_clock2 = Unix.gettimeofday () in check_pending_proofs (); @@ -270,10 +270,10 @@ let compile opts ~echo ~f_in ~f_out = iload_path; require_libs; stm_options; }) in - let state = { doc; sid; proof = None } in + let state = { doc; sid; proof = None; time = opts.time } in let state = load_init_vernaculars opts ~state in let ldir = Stm.get_ldir ~doc:state.doc in - let state = Vernac.load_vernac ~time:opts.time ~echo ~check:false ~interactive:false ~state long_f_dot_v in + let state = Vernac.load_vernac ~echo ~check:false ~interactive:false ~state long_f_dot_v in let doc = Stm.finish ~doc:state.doc in check_pending_proofs (); let _doc = Stm.snapshot_vio ~doc ldir long_f_dot_vio in @@ -476,7 +476,7 @@ let init_toplevel arglist = { doc_type = Interactive opts.toplevel_name; iload_path; require_libs; stm_options; }) in - let state = { doc; sid; proof = None } in + let state = { doc; sid; proof = None; time = opts.time } in Some (load_init_vernaculars opts ~state), opts with any -> flush_all(); fatal_error_exn any (* Non interactive: we perform a sequence of compilation steps *) diff --git a/toplevel/g_toplevel.ml4 b/toplevel/g_toplevel.ml4 new file mode 100644 index 000000000..7526f3071 --- /dev/null +++ b/toplevel/g_toplevel.ml4 @@ -0,0 +1,43 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* CAst.make VernacDrop + | IDENT "Quit"; "." -> CAst.make VernacQuit + | cmd = main_entry -> + match cmd with + | None -> raise Stm.End_of_input + | Some (loc,c) -> CAst.make ~loc (VernacControl c) + ] + ] + ; +END + +let parse_toplevel pa = Pcoq.Gram.entry_parse vernac_toplevel pa diff --git a/toplevel/toplevel.mllib b/toplevel/toplevel.mllib index 9fb2e33d7..78b96e5e2 100644 --- a/toplevel/toplevel.mllib +++ b/toplevel/toplevel.mllib @@ -1,5 +1,6 @@ Vernac Usage +G_toplevel Coqloop Coqinit Coqargs diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index fdd0d4ed3..c1bbb20d5 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -28,10 +28,6 @@ let checknav_deep {CAst.loc;v=ast} = if is_deep_navigation_vernac ast then CErrors.user_err ?loc (str "Navigation commands forbidden in nested commands.") -let disable_drop = function - | Drop -> CErrors.user_err Pp.(str "Drop is forbidden.") - | e -> e - (* Echo from a buffer based on position. XXX: Should move to utility file. *) let vernac_echo ?loc in_chan = let open Loc in @@ -80,17 +76,21 @@ module State = struct doc : Stm.doc; sid : Stateid.t; proof : Proof.t option; + time : bool; } end -let interp_vernac ~time ~check ~interactive ~state ({CAst.loc;_} as com) = +let interp_vernac ~check ~interactive ~state ({CAst.loc;_} as com) = let open State in try (* The -time option is only supported from console-based clients due to the way it prints. *) - if time then print_cmd_header com; - let com = if time then CAst.make ?loc @@ VernacTime(time,com) else com in + let com = if state.time + then begin + print_cmd_header com; + CAst.make ?loc @@ VernacTime(state.time,com) + end else com in let doc, nsid, ntip = Stm.add ~doc:state.doc ~ontop:state.sid (not !Flags.quiet) com in (* Main STM interaction *) @@ -102,7 +102,7 @@ let interp_vernac ~time ~check ~interactive ~state ({CAst.loc;_} as com) = (* Stm.observe nsid; *) let ndoc = if check then Stm.finish ~doc else doc in let new_proof = Proof_global.give_me_the_proof_opt () in - { doc = ndoc; sid = nsid; proof = new_proof } + { state with doc = ndoc; sid = nsid; proof = new_proof; } with reraise -> (* XXX: In non-interactive mode edit_at seems to do very weird things, so we better avoid it while we investigate *) @@ -115,7 +115,7 @@ let interp_vernac ~time ~check ~interactive ~state ({CAst.loc;_} as com) = end in iraise (reraise, info) (* Load a vernac file. CErrors are annotated with file and location *) -let load_vernac_core ~time ~echo ~check ~interactive ~state file = +let load_vernac_core ~echo ~check ~interactive ~state file = (* Keep in sync *) let in_chan = open_utf8_file_in file in let in_echo = if echo then Some (open_utf8_file_in file) else None in @@ -154,7 +154,7 @@ let load_vernac_core ~time ~echo ~check ~interactive ~state file = Option.iter (vernac_echo ?loc) in_echo; checknav_simple ast; - let state = Flags.silently (interp_vernac ~time ~check ~interactive ~state:!rstate) ast in + let state = Flags.silently (interp_vernac ~check ~interactive ~state:!rstate) ast in rids := state.sid :: !rids; rstate := state; done; @@ -165,11 +165,11 @@ let load_vernac_core ~time ~echo ~check ~interactive ~state file = input_cleanup (); match e with | Stm.End_of_input -> !rstate, !rids, Pcoq.Gram.comment_state in_pa - | reraise -> iraise (disable_drop e, info) + | reraise -> iraise (e, info) -let process_expr ~time ~state loc_ast = +let process_expr ~state loc_ast = checknav_deep loc_ast; - interp_vernac ~time ~interactive:true ~check:true ~state loc_ast + interp_vernac ~interactive:true ~check:true ~state loc_ast (******************************************************************************) (* Beautify-specific code *) @@ -220,8 +220,8 @@ let beautify_pass ~doc ~comments ~ids ~filename = (* Main driver for file loading. For now, we only do one beautify pass. *) -let load_vernac ~time ~echo ~check ~interactive ~state filename = - let ostate, ids, comments = load_vernac_core ~time ~echo ~check ~interactive ~state filename in +let load_vernac ~echo ~check ~interactive ~state filename = + let ostate, ids, comments = load_vernac_core ~echo ~check ~interactive ~state filename in (* Pass for beautify *) if !Flags.beautify then beautify_pass ~doc:ostate.State.doc ~comments ~ids:List.(rev ids) ~filename; (* End pass *) diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli index 51758642e..126954023 100644 --- a/toplevel/vernac.mli +++ b/toplevel/vernac.mli @@ -15,6 +15,7 @@ module State : sig doc : Stm.doc; sid : Stateid.t; proof : Proof.t option; + time : bool; } end @@ -23,10 +24,10 @@ end expected to handle and print errors in form of exceptions, however care is taken so the state machine is left in a consistent state. *) -val process_expr : time:bool -> state:State.t -> Vernacexpr.vernac_control CAst.t -> State.t +val process_expr : state:State.t -> Vernacexpr.vernac_control CAst.t -> State.t (** [load_vernac echo sid file] Loads [file] on top of [sid], will echo the commands if [echo] is set. Callers are expected to handle and print errors in form of exceptions. *) -val load_vernac : time:bool -> echo:bool -> check:bool -> interactive:bool -> +val load_vernac : echo:bool -> check:bool -> interactive:bool -> state:State.t -> string -> State.t -- cgit v1.2.3