From ed18f926e4695acc730218925ca156abe56ba5fc Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 13 Feb 2018 18:26:00 +0100 Subject: [toplevel] Make toplevel state into a record. We organize the toplevel execution as a record and pass it around. This will be used by future PRs as to for example decouple goal printing from the classifier. --- toplevel/coqinit.ml | 8 +++--- toplevel/coqinit.mli | 2 +- toplevel/coqloop.ml | 33 +++++++++++++----------- toplevel/coqloop.mli | 6 ++--- toplevel/coqtop.ml | 73 ++++++++++++++++++++++++++++------------------------ toplevel/coqtop.mli | 7 +++-- toplevel/vernac.ml | 43 +++++++++++++++++++------------ toplevel/vernac.mli | 14 ++++++++-- 8 files changed, 107 insertions(+), 79 deletions(-) (limited to 'toplevel') diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 8574092b8..d8aaf3db8 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -21,12 +21,12 @@ let set_debug () = let rcdefaultname = "coqrc" -let load_rcfile ~rcfile ~time doc sid = +let load_rcfile ~rcfile ~time ~state = try match rcfile with | Some rcfile -> if CUnix.file_readable_p rcfile then - Vernac.load_vernac ~time ~verbosely:false ~interactive:false ~check:true doc sid rcfile + Vernac.load_vernac ~time ~verbosely:false ~interactive:false ~check:true ~state rcfile else raise (Sys_error ("Cannot read rcfile: "^ rcfile)) | None -> try @@ -37,8 +37,8 @@ let load_rcfile ~rcfile ~time doc sid = Envars.home ~warn / "."^rcdefaultname^"."^Coq_config.version; Envars.home ~warn / "."^rcdefaultname ] in - Vernac.load_vernac ~time ~verbosely:false ~interactive:false ~check:true doc sid inferedrc - with Not_found -> doc, sid + Vernac.load_vernac ~time ~verbosely:false ~interactive:false ~check:true ~state inferedrc + with Not_found -> state (* Flags.if_verbose mSGNL (str ("No coqrc or coqrc."^Coq_config.version^ diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli index 0ceba5b38..14f39170c 100644 --- a/toplevel/coqinit.mli +++ b/toplevel/coqinit.mli @@ -10,7 +10,7 @@ val set_debug : unit -> unit -val load_rcfile : rcfile:(string option) -> time:bool -> Stm.doc -> Stateid.t -> Stm.doc * Stateid.t +val load_rcfile : rcfile:(string option) -> time:bool -> state:Vernac.State.t -> Vernac.State.t val init_ocaml_path : unit -> unit diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index aade101a4..ae0b94476 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -258,8 +258,9 @@ let rec discard_to_dot () = | Stm.End_of_input -> raise Stm.End_of_input | e when CErrors.noncritical e -> () -let read_sentence ~doc sid input = - try Stm.parse_sentence ~doc sid input +let read_sentence ~state input = + let open Vernac.State in + try Stm.parse_sentence ~doc:state.doc state.sid input with reraise -> let reraise = CErrors.push reraise in discard_to_dot (); @@ -300,19 +301,20 @@ let coqloop_feed (fb : Feedback.feedback) = let open Feedback in is caught and handled (i.e. not re-raised). *) -let do_vernac ~time doc sid = +let do_vernac ~time ~state = + let open Vernac.State in top_stderr (fnl()); - if !print_emacs then top_stderr (str (top_buffer.prompt doc)); + 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 doc sid (read_sentence ~doc sid (fst input)) + 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."); doc, sid) + 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. *) @@ -321,7 +323,7 @@ let do_vernac ~time doc sid = 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; - doc, sid + state (** Main coq loop : read vernacular expressions until Drop is entered. Ctrl-C is handled internally as Sys.Break instead of aborting Coq. @@ -337,20 +339,21 @@ let loop_flush_all () = Format.pp_print_flush !Topfmt.std_ft (); Format.pp_print_flush !Topfmt.err_ft () -let rec loop ~time doc = +let rec loop ~time ~state = + let open Vernac.State in Sys.catch_break true; try - reset_input_buffer doc stdin top_buffer; + reset_input_buffer state.doc stdin top_buffer; (* Be careful to keep this loop tail-recursive *) - let rec vernac_loop doc sid = - let ndoc, nsid = do_vernac ~time doc sid in + let rec vernac_loop ~state = + let nstate = do_vernac ~time ~state in loop_flush_all (); - vernac_loop ndoc nsid + vernac_loop ~state:nstate (* We recover the current stateid, threading from the caller is not possible due exceptions. *) - in vernac_loop doc (Stm.get_current_state ~doc) + in vernac_loop ~state with - | CErrors.Drop -> doc + | CErrors.Drop -> state | CErrors.Quit -> exit 0 | any -> top_stderr (str "Anomaly: main loop exited with exception: " ++ @@ -358,4 +361,4 @@ let rec loop ~time doc = fnl() ++ str"Please report" ++ strbrk" at " ++ str Coq_config.wwwbugtracker ++ str "."); - loop ~time doc + loop ~time ~state diff --git a/toplevel/coqloop.mli b/toplevel/coqloop.mli index 09240ec82..1c1309051 100644 --- a/toplevel/coqloop.mli +++ b/toplevel/coqloop.mli @@ -31,9 +31,7 @@ val set_prompt : (unit -> string) -> unit val coqloop_feed : Feedback.feedback -> unit (** Parse and execute one vernac command. *) - -val do_vernac : time:bool -> Stm.doc -> Stateid.t -> Stm.doc * Stateid.t +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 -> Stm.doc -> Stm.doc +val loop : time:bool -> state:Vernac.State.t -> Vernac.State.t diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 9058f0846..26ede1834 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -37,16 +37,16 @@ let coqtop_init_feed = Coqloop.coqloop_feed let drop_last_doc = ref None (* Default toplevel loop *) -let console_toploop_run opts doc = +let console_toploop_run opts ~state = (* We initialize the console only if we run the toploop_run *) let tl_feed = Feedback.add_feeder Coqloop.coqloop_feed in if Dumpglob.dump () then begin Flags.if_verbose warning "Dumpglob cannot be used in interactive mode."; Dumpglob.noglob () end; - let doc = Coqloop.loop ~time:opts.time doc in + let state = Coqloop.loop ~time:opts.time ~state in (* Initialise and launch the Ocaml toplevel *) - drop_last_doc := Some doc; + drop_last_doc := Some state; Coqinit.init_ocaml_path(); Mltop.ocaml_toploop(); (* We let the feeder in place for users of Drop *) @@ -90,24 +90,26 @@ let outputstate opts = (******************************************************************************) (* Interactive Load File Simulation *) (******************************************************************************) -let load_vernacular opts doc sid = +let load_vernacular opts ~state = List.fold_left - (fun (doc,sid) (f_in, verbosely) -> + (fun state (f_in, verbosely) -> let s = Loadpath.locate_file f_in in - if !Flags.beautify then - Flags.with_option Flags.beautify_file (Vernac.load_vernac ~time:opts.time ~verbosely ~interactive:false ~check:true doc sid) f_in - else - Vernac.load_vernac ~time:opts.time ~verbosely ~interactive:false ~check:true doc sid s) - (doc, sid) (List.rev opts.load_vernacular_list) - -let load_init_vernaculars opts doc sid = - let doc, sid = if opts.load_rcfile then - Coqinit.load_rcfile ~rcfile:opts.rcfile ~time:opts.time doc sid + (* Should make the beautify logic clearer *) + let load_vernac f = Vernac.load_vernac ~time:opts.time ~verbosely ~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 + ) state (List.rev opts.load_vernacular_list) + +let load_init_vernaculars opts ~state = + let state = if opts.load_rcfile then + Coqinit.load_rcfile ~rcfile:opts.rcfile ~time:opts.time ~state else begin Flags.if_verbose Feedback.msg_info (str"Skipping rcfile loading."); - doc,sid + state end in - load_vernacular opts doc sid + + load_vernacular opts ~state (******************************************************************************) (* Startup LoadPath and Modules *) @@ -193,6 +195,7 @@ let ensure_exists f = (* Compile a vernac file *) let compile opts ~verbosely ~f_in ~f_out = + let open Vernac.State in let check_pending_proofs () = let pfs = Proof_global.get_all_proof_names () in if not (CList.is_empty pfs) then @@ -220,16 +223,17 @@ let compile opts ~verbosely ~f_in ~f_out = iload_path; require_libs; stm_options; }) in - let doc, sid = load_init_vernaculars opts doc sid in - let ldir = Stm.get_ldir ~doc in + let state = { doc; sid; proof = None } in + let state = load_init_vernaculars opts ~state in + let ldir = Stm.get_ldir ~doc:state.doc in Aux_file.(start_aux_file ~aux_file:(aux_file_name_for long_f_dot_vo) ~v_file:long_f_dot_v); 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 doc, _ = Vernac.load_vernac ~time:opts.time ~verbosely ~check:true ~interactive:false doc (Stm.get_current_state ~doc) long_f_dot_v in - let _doc = Stm.join ~doc in + let state = Vernac.load_vernac ~time:opts.time ~verbosely ~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 (); Library.save_library_to ldir long_f_dot_vo (Global.opaque_tables ()); @@ -266,11 +270,11 @@ let compile opts ~verbosely ~f_in ~f_out = iload_path; require_libs; stm_options; }) in - let doc, sid = load_init_vernaculars opts doc sid in - - let ldir = Stm.get_ldir ~doc in - let doc, _ = Vernac.load_vernac ~time:opts.time ~verbosely ~check:false ~interactive:false doc (Stm.get_current_state ~doc) long_f_dot_v in - let doc = Stm.finish ~doc in + let state = { doc; sid; proof = None } 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 ~verbosely ~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 Stm.reset_task_queue () @@ -465,12 +469,15 @@ let init_toplevel arglist = let iload_path = build_load_path opts in let require_libs = require_libs opts in let stm_options = opts.stm_flags in - try let doc, sid = - Stm.(new_doc - { doc_type = Interactive opts.toplevel_name; - iload_path; require_libs; stm_options; - }) in - Some (load_init_vernaculars opts doc sid), opts + try + let open Vernac.State in + let doc, sid = + Stm.(new_doc + { doc_type = Interactive opts.toplevel_name; + iload_path; require_libs; stm_options; + }) in + let state = { doc; sid; proof = None } 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 *) end else begin @@ -496,8 +503,8 @@ let init_toplevel arglist = let start () = match init_toplevel (List.tl (Array.to_list Sys.argv)) with (* Batch mode *) - | Some (doc, sid), opts when not opts.batch_mode -> - !toploop_run opts doc; + | Some state, opts when not opts.batch_mode -> + !toploop_run opts ~state; exit 1 | _ , opts -> flush_all(); diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli index 4d625a03d..dedb298e2 100644 --- a/toplevel/coqtop.mli +++ b/toplevel/coqtop.mli @@ -11,14 +11,13 @@ state, load the files given on the command line, load the resource file, produce the output state if any, and finally will launch [Coqloop.loop]. *) -val init_toplevel : string list -> (Stm.doc * Stateid.t) option * Coqargs.coq_cmdopts +val init_toplevel : string list -> Vernac.State.t option * Coqargs.coq_cmdopts val start : unit -> unit (* Last document seen after `Drop` *) -val drop_last_doc : Stm.doc option ref +val drop_last_doc : Vernac.State.t option ref (* For other toploops *) val toploop_init : (Coqargs.coq_cmdopts -> string list -> string list) ref -val toploop_run : (Coqargs.coq_cmdopts -> Stm.doc -> unit) ref - +val toploop_run : (Coqargs.coq_cmdopts -> state:Vernac.State.t -> unit) ref diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 6b45a94bc..1f681d9cf 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -110,14 +110,25 @@ let pr_open_cur_subgoals () = (* Stm.End_of_input -> true *) (* | _ -> false *) -let rec interp_vernac ~time ~check ~interactive doc sid (loc,com) = +module State = struct + + type t = { + doc : Stm.doc; + sid : Stateid.t; + proof : Proof.t option; + } + +end + +let rec interp_vernac ~time ~check ~interactive ~state (loc,com) = + let open State in let interp v = match under_control v with | VernacLoad (verbosely, fname) -> let fname = Envars.expand_path_macros ~warn:(fun x -> Feedback.msg_warning (str x)) fname in let fname = CUnix.make_suffix fname ".v" in let f = Loadpath.locate_file fname in - load_vernac ~time ~verbosely ~check ~interactive doc sid f + load_vernac ~time ~verbosely ~check ~interactive ~state f | _ -> (* XXX: We need to run this before add as the classification is highly dynamic and depends on the structure of the @@ -134,7 +145,7 @@ let rec interp_vernac ~time ~check ~interactive doc sid (loc,com) = in CWarnings.set_flags wflags; - let doc, nsid, ntip = Stm.add ~doc ~ontop:sid (not !Flags.quiet) (loc,v) in + let doc, nsid, ntip = Stm.add ~doc:state.doc ~ontop:state.sid (not !Flags.quiet) (loc,v) in (* Main STM interaction *) if ntip <> `NewTip then @@ -152,7 +163,8 @@ let rec interp_vernac ~time ~check ~interactive doc sid (loc,com) = is_proof_step && Proof_global.there_are_pending_proofs () in if print_goals then Feedback.msg_notice (pr_open_cur_subgoals ()); - ndoc, nsid + let new_proof = Proof_global.give_me_the_proof_opt () in + { doc = ndoc; sid = nsid; proof = new_proof } in try (* The -time option is only supported from console-based @@ -163,7 +175,7 @@ let rec interp_vernac ~time ~check ~interactive doc sid (loc,com) = with reraise -> (* XXX: In non-interactive mode edit_at seems to do very weird things, so we better avoid it while we investigate *) - if interactive then ignore(Stm.edit_at ~doc sid); + if interactive then ignore(Stm.edit_at ~doc:state.doc state.sid); let (reraise, info) = CErrors.push reraise in let info = begin match Loc.get_loc info with @@ -172,7 +184,7 @@ let rec interp_vernac ~time ~check ~interactive doc sid (loc,com) = end in iraise (reraise, info) (* Load a vernac file. CErrors are annotated with file and location *) -and load_vernac ~time ~verbosely ~check ~interactive doc sid file = +and load_vernac ~time ~verbosely ~check ~interactive ~state file = let ft_beautify, close_beautify = if !Flags.beautify_file then let chan_beautify = open_out (file^beautify_suffix) in @@ -183,14 +195,14 @@ and load_vernac ~time ~verbosely ~check ~interactive doc sid file = let in_chan = open_utf8_file_in file in let in_echo = if verbosely then Some (open_utf8_file_in file) else None in let in_pa = Pcoq.Gram.parsable ~file:(Loc.InFile file) (Stream.of_channel in_chan) in - let rsid = ref sid in - let rdoc = ref doc in + let rstate = ref state 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 loc, ast = - Stm.parse_sentence ~doc:!rdoc !rsid in_pa + 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 @@ -214,11 +226,10 @@ and load_vernac ~time ~verbosely ~check ~interactive doc sid file = Option.iter (vernac_echo ?loc) in_echo; checknav_simple (loc, ast); - let ndoc, nsid = Flags.silently (interp_vernac ~time ~check ~interactive !rdoc !rsid) (loc, ast) in - rsid := nsid; - rdoc := ndoc + let state = Flags.silently (interp_vernac ~time ~check ~interactive ~state:!rstate) (loc, ast) in + rstate := state; done; - !rdoc, !rsid + !rstate with any -> (* whatever the exception *) let (e, info) = CErrors.push any in close_in in_chan; @@ -229,7 +240,7 @@ and load_vernac ~time ~verbosely ~check ~interactive doc sid file = if !Flags.beautify then pr_new_syntax ~loc:(Loc.make_loc (max_int,max_int)) in_pa ft_beautify None; if !Flags.beautify_file then close_beautify (); - !rdoc, !rsid + !rstate | reraise -> if !Flags.beautify_file then close_beautify (); iraise (disable_drop e, info) @@ -241,6 +252,6 @@ and load_vernac ~time ~verbosely ~check ~interactive doc sid file = of a new state label). An example of state-preserving command is one coming from the query panel of Coqide. *) -let process_expr ~time doc sid loc_ast = +let process_expr ~time ~state loc_ast = checknav_deep loc_ast; - interp_vernac ~time ~interactive:true ~check:true doc sid loc_ast + interp_vernac ~time ~interactive:true ~check:true ~state loc_ast diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli index b77b024fa..e909ada1e 100644 --- a/toplevel/vernac.mli +++ b/toplevel/vernac.mli @@ -7,14 +7,24 @@ (************************************************************************) (** Parsing of vernacular. *) +module State : sig + + type t = { + doc : Stm.doc; + sid : Stateid.t; + proof : Proof.t option; + } + +end (** [process_expr sid cmd] Executes vernac command [cmd]. Callers are 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 -> Stm.doc -> Stateid.t -> Vernacexpr.vernac_control Loc.located -> Stm.doc * Stateid.t +val process_expr : time:bool -> state:State.t -> Vernacexpr.vernac_control Loc.located -> 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 -> verbosely:bool -> check:bool -> interactive:bool -> Stm.doc -> Stateid.t -> string -> Stm.doc * Stateid.t +val load_vernac : time:bool -> verbosely:bool -> check:bool -> interactive:bool -> + state:State.t -> string -> State.t -- cgit v1.2.3