diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-02-27 20:16:40 +0100 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-04-12 16:49:45 +0200 |
commit | ce2b2058587224ade9261cd4127ef4f6e94d356b (patch) | |
tree | 28e9cc9f14c0bb3a8107e67faa85ccda6c6d4dc9 /toplevel | |
parent | 4ed9c7ad75a7f09d723bdfce6f7dd086c60e0601 (diff) |
[stm] Port the toplevel to the STM.
- We clean-up `Vernac` and make it use the STM API.
- Now functions in `Vernac` for use in the toplevel and compiler take
an starting `Stateid.t`.
- Duplicated `Stm.interp` entry point is removed.
- The XML protocol call `interp` is disabled.
Diffstat (limited to 'toplevel')
-rw-r--r-- | toplevel/coqinit.ml | 11 | ||||
-rw-r--r-- | toplevel/coqinit.mli | 2 | ||||
-rw-r--r-- | toplevel/coqloop.ml | 31 | ||||
-rw-r--r-- | toplevel/coqloop.mli | 2 | ||||
-rw-r--r-- | toplevel/coqtop.ml | 17 | ||||
-rw-r--r-- | toplevel/vernac.ml | 179 | ||||
-rw-r--r-- | toplevel/vernac.mli | 26 |
7 files changed, 108 insertions, 160 deletions
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index ffd0d7805..2b9a04dad 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -27,12 +27,12 @@ let set_rcfile s = rcfile := s; rcfile_specified := true let load_rc = ref true let no_load_rc () = load_rc := false -let load_rcfile() = +let load_rcfile sid = if !load_rc then try if !rcfile_specified then if CUnix.file_readable_p !rcfile then - Vernac.load_vernac false !rcfile + Vernac.load_vernac false sid !rcfile else raise (Sys_error ("Cannot read rcfile: "^ !rcfile)) else try @@ -43,8 +43,8 @@ let load_rcfile() = Envars.home ~warn / "."^rcdefaultname^"."^Coq_config.version; Envars.home ~warn / "."^rcdefaultname ] in - Vernac.load_vernac false inferedrc - with Not_found -> () + Vernac.load_vernac false sid inferedrc + with Not_found -> sid (* Flags.if_verbose mSGNL (str ("No coqrc or coqrc."^Coq_config.version^ @@ -55,7 +55,8 @@ let load_rcfile() = let () = Feedback.msg_info (str"Load of rcfile failed.") in iraise reraise else - Flags.if_verbose Feedback.msg_info (str"Skipping rcfile loading.") + (Flags.if_verbose Feedback.msg_info (str"Skipping rcfile loading."); + sid) (* Recursively puts dir in the LoadPath if -nois was not passed *) let add_stdlib_path ~unix_path ~coq_root ~with_ml = diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli index 4ff87628c..3b42289ee 100644 --- a/toplevel/coqinit.mli +++ b/toplevel/coqinit.mli @@ -13,7 +13,7 @@ val set_debug : unit -> unit val set_rcfile : string -> unit val no_load_rc : unit -> unit -val load_rcfile : unit -> unit +val load_rcfile : Stateid.t -> Stateid.t val push_include : string -> Names.DirPath.t -> bool -> unit (** [push_include phys_path log_path implicit] *) diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index 2282932d4..17d8f5f49 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -257,7 +257,7 @@ let set_prompt prompt = let parse_to_dot = let rec dot st = match Stream.next st with | Tok.KEYWORD ("."|"...") -> () - | Tok.EOI -> raise End_of_input + | Tok.EOI -> raise Stm.End_of_input | _ -> dot st in Gram.Entry.of_parser "Coqtoplevel.dot" dot @@ -271,13 +271,11 @@ let rec discard_to_dot () = Gram.entry_parse parse_to_dot top_buffer.tokens with | Token.Error _ | CLexer.Error.E _ -> discard_to_dot () - | End_of_input -> raise End_of_input + | Stm.End_of_input -> raise Stm.End_of_input | e when CErrors.noncritical e -> () -let read_sentence input = - try - let (loc, _ as r) = Vernac.parse_sentence input in - CWarnings.set_current_loc loc; r +let read_sentence sid input = + try Stm.parse_sentence sid input with reraise -> let reraise = CErrors.push reraise in discard_to_dot (); @@ -312,25 +310,24 @@ let coqloop_feed (fb : Feedback.feedback) = let open Feedback in is caught and handled (i.e. not re-raised). *) -let do_vernac () = +let do_vernac sid = top_stderr (fnl()); if !print_emacs then top_stderr (str (top_buffer.prompt())); resynch_buffer top_buffer; try let input = (top_buffer.tokens, None) in - Vernac.process_expr top_buffer.tokens (read_sentence input) + Vernac.process_expr sid top_buffer.tokens (read_sentence sid (fst input)) with - | End_of_input | CErrors.Quit -> + | 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_error (str "There is no ML toplevel.") + else (Feedback.msg_error (str "There is no ML toplevel."); sid) (* Exception printing is done now by the feedback listener. *) (* XXX: We need this hack due to the side effects of the exception printer and the reliance of Stm.define on attaching crutial state to exceptions *) - | any -> ignore (CErrors.(iprint (push any))) - + | any -> ignore (CErrors.(iprint (push any))); sid (** Main coq loop : read vernacular expressions until Drop is entered. Ctrl-C is handled internally as Sys.Break instead of aborting Coq. @@ -349,10 +346,16 @@ let loop_flush_all () = let rec loop () = Sys.catch_break true; if !Flags.print_emacs then Vernacentries.qed_display_script := false; - Flags.coqtop_ui := true; try reset_input_buffer stdin top_buffer; - while true do do_vernac(); loop_flush_all () done + (* Be careful to keep this loop tail-recursive *) + let rec vernac_loop sid = + let nsid = do_vernac sid in + loop_flush_all (); + vernac_loop nsid + (* We recover the current stateid, threading from the caller is + not possible due exceptions. *) + in vernac_loop (Stm.get_current_state ()) with | CErrors.Drop -> () | CErrors.Quit -> exit 0 diff --git a/toplevel/coqloop.mli b/toplevel/coqloop.mli index 8a34ded6d..66bbf43f6 100644 --- a/toplevel/coqloop.mli +++ b/toplevel/coqloop.mli @@ -31,7 +31,7 @@ val coqloop_feed : Feedback.feedback -> unit (** Parse and execute one vernac command. *) -val do_vernac : unit -> unit +val do_vernac : Stateid.t -> Stateid.t (** Main entry point of Coq: read and execute vernac commands. *) diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 4968804fd..c8f3ca1ab 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -175,15 +175,15 @@ let set_include d p implicit = let load_vernacular_list = ref ([] : (string * bool) list) let add_load_vernacular verb s = load_vernacular_list := ((CUnix.make_suffix s ".v"),verb) :: !load_vernacular_list -let load_vernacular () = - List.iter - (fun (s,b) -> +let load_vernacular sid = + List.fold_left + (fun sid (s,v) -> let s = Loadpath.locate_file s in if !Flags.beautify then - with_option beautify_file (Vernac.load_vernac b) s + with_option beautify_file (Vernac.load_vernac v sid) s else - Vernac.load_vernac b s) - (List.rev !load_vernacular_list) + Vernac.load_vernac v sid s) + sid (List.rev !load_vernacular_list) let load_vernacular_obj = ref ([] : string list) let add_vernac_obj s = load_vernacular_obj := s :: !load_vernacular_obj @@ -641,8 +641,9 @@ let init_toplevel arglist = load_vernac_obj (); require (); Stm.init (); - load_rcfile(); - load_vernacular (); + let sid = load_rcfile (Stm.get_current_state ()) in + (* XXX: We ignore this for now, but should be threaded to the toplevels *) + let _sid = load_vernacular sid in compile_files (); schedule_vio_checking (); schedule_vio_compilation (); diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index d5ceeaccd..98458a57a 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -13,111 +13,30 @@ open CErrors open Util open Flags open Vernacexpr +open Vernacprop (* The functions in this module may raise (unexplainable!) exceptions. Use the module Coqtoplevel, which catches these exceptions (the exceptions are explained only at the toplevel). *) -let user_error loc s = CErrors.user_err ~loc (str s) - -(* Navigation commands are allowed in a coqtop session but not in a .v file *) - -let rec is_navigation_vernac = function - | VernacResetInitial - | VernacResetName _ - | VernacBacktrack _ - | VernacBackTo _ - | VernacBack _ - | VernacStm _ -> true - | VernacRedirect (_, (_,c)) - | VernacTime (_,c) -> - is_navigation_vernac c (* Time Back* is harmless *) - | c -> is_deep_navigation_vernac c - -and is_deep_navigation_vernac = function - | VernacTimeout (_,c) | VernacFail c -> is_navigation_vernac c - | _ -> false - -(* NB: Reset is now allowed again as asked by A. Chlipala *) - -let is_reset = function - | VernacResetInitial | VernacResetName _ -> true - | _ -> false - -let checknav_simple loc cmd = +let checknav_simple (loc, cmd) = if is_navigation_vernac cmd && not (is_reset cmd) then - user_error loc "Navigation commands forbidden in files." + CErrors.user_err ~loc (str "Navigation commands forbidden in files.") -let checknav_deep loc ast = +let checknav_deep (loc, ast) = if is_deep_navigation_vernac ast then - user_error loc "Navigation commands forbidden in nested commands." - -(* When doing Load on a file, two behaviors are possible: - - - either the history stack is grown by only one command, - the "Load" itself. This is mandatory for command-counting - interfaces (CoqIDE). - - - either each individual sub-commands in the file is added - to the history stack. This allows commands like Show Script - to work across the loaded file boundary (cf. bug #2820). - - The best of the two could probably be combined someday, - in the meanwhile we use a flag. *) - -let atomic_load = ref true - -let _ = - Goptions.declare_bool_option - { Goptions.optsync = true; - Goptions.optdepr = false; - Goptions.optname = "atomic registration of commands in a Load"; - Goptions.optkey = ["Atomic";"Load"]; - Goptions.optread = (fun () -> !atomic_load); - Goptions.optwrite = ((:=) atomic_load) } + CErrors.user_err ~loc (str "Navigation commands forbidden in nested commands.") let disable_drop = function | Drop -> CErrors.error "Drop is forbidden." | e -> e -(* Opening and closing a channel. Open it twice when verbose: the first - channel is used to read the commands, and the second one to print them. - Note: we could use only one thanks to seek_in, but seeking on and on in - the file we parse seems a bit risky to me. B.B. *) - -let open_file_twice_if verbosely longfname = - let in_chan = open_utf8_file_in longfname in - let verb_ch = - if verbosely then Some (open_utf8_file_in longfname) else None in - let po = Pcoq.Gram.parsable ~file:longfname (Stream.of_channel in_chan) in - (in_chan, longfname, (po, verb_ch)) - -let close_input in_chan (_,verb) = - try - close_in in_chan; - match verb with - | Some verb_ch -> close_in verb_ch - | _ -> () - with e when CErrors.noncritical e -> () - -let verbose_phrase verbch loc = - let loc = Loc.unloc loc in - match verbch with - | Some ch -> - let len = snd loc - fst loc in - let s = Bytes.create len in - seek_in ch (fst loc); - really_input ch s 0 len; - Feedback.msg_notice (str (Bytes.to_string s)) - | None -> () - -exception End_of_input - -let parse_sentence = Flags.with_option Flags.we_are_parsing - (fun (po, verbch) -> - match Pcoq.Gram.entry_parse Pcoq.main_entry po with - | Some (loc,_ as com) -> verbose_phrase verbch loc; com - | None -> raise End_of_input) +(* Echo from a buffer based on position. + XXX: Should move to utility file. *) +let vernac_echo loc in_chan = let open Loc in + let len = loc.ep - loc.bp in + seek_in in_chan loc.bp; + Feedback.msg_notice @@ str @@ really_input_string in_chan len (* vernac parses the given stream, executes interpfun on the syntax tree it * parses, and is verbose on "primitives" commands if verbosely is true *) @@ -184,20 +103,43 @@ let print_cmd_header loc com = Pp.pp_with !Topfmt.std_ft (pp_cmd_header loc com); Format.pp_print_flush !Topfmt.std_ft () -let rec interp_vernac po chan_beautify checknav (loc,com) = +let pr_open_cur_subgoals () = + try Printer.pr_open_subgoals () + with Proof_global.NoCurrentProof -> Pp.str "" + +let rec interp_vernac sid po (loc,com) = let interp = function | 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 verbosely f - - | v -> Stm.interp (Flags.is_verbose()) (loc,v) + load_vernac verbosely sid f + | v -> + try + let nsid, ntip = Stm.add sid (Flags.is_verbose()) (loc,v) in + + (* Main STM interaction *) + 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; *) + Stm.finish (); + + (* We could use a more refined criteria depending on the + vernac. For now we imitate the old approach. *) + let print_goals = not (!Flags.batch_mode || is_query v) in + + if print_goals then Feedback.msg_notice (pr_open_cur_subgoals ()); + nsid + + with exn when CErrors.noncritical exn -> + ignore(Stm.edit_at sid); + raise exn in try - checknav loc com; - if !beautify then pr_new_syntax po chan_beautify loc (Some com); - (* XXX: This is not 100% correct if called from an IDE context *) + (* The -time option is only supported from console-based + clients due to the way it prints. *) if !Flags.time then print_cmd_header loc com; let com = if !Flags.time then VernacTime (loc,com) else com in interp com @@ -208,26 +150,39 @@ let rec interp_vernac po chan_beautify checknav (loc,com) = else iraise (reraise, info) (* Load a vernac file. CErrors are annotated with file and location *) -and load_vernac verbosely file = +and load_vernac verbosely sid file = let chan_beautify = if !Flags.beautify_file then open_out (file^beautify_suffix) else stdout in - let (in_chan, fname, input) = open_file_twice_if verbosely file in + 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 (Stream.of_channel in_chan) in + let rsid = ref sid 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 = Flags.silently parse_sentence input in - CWarnings.set_current_loc (fst loc_ast); - Flags.silently (interp_vernac (fst input) chan_beautify checknav_simple) loc_ast; - done + let loc, ast = Stm.parse_sentence !rsid in_pa in + + (* Printing of vernacs *) + if !beautify then pr_new_syntax in_pa chan_beautify loc (Some ast); + Option.iter (vernac_echo loc) in_echo; + + checknav_simple (loc, ast); + let nsid = Flags.silently (interp_vernac !rsid in_pa) (loc, ast) in + rsid := nsid + done; + !rsid with any -> (* whatever the exception *) let (e, info) = CErrors.push any in - close_input in_chan input; (* we must close the file first *) + close_in in_chan; + Option.iter close_in in_echo; match e with - | End_of_input -> + | Stm.End_of_input -> + (* Is this called so comments at EOF are printed? *) if !beautify then - pr_new_syntax (fst input) chan_beautify (Loc.make_loc (max_int,max_int)) None; + pr_new_syntax in_pa chan_beautify (Loc.make_loc (max_int,max_int)) None; if !Flags.beautify_file then close_out chan_beautify; + !rsid | reraise -> if !Flags.beautify_file then close_out chan_beautify; iraise (disable_drop e, info) @@ -239,7 +194,9 @@ and load_vernac verbosely file = of a new state label). An example of state-preserving command is one coming from the query panel of Coqide. *) -let process_expr po loc_ast = interp_vernac po stdout checknav_deep loc_ast +let process_expr sid po loc_ast = + checknav_deep loc_ast; + interp_vernac sid po loc_ast (* XML output hooks *) let (f_xml_start_library, xml_start_library) = Hook.make ~default:ignore () @@ -308,7 +265,7 @@ let compile verbosely f = Dumpglob.dump_string ("F" ^ Names.DirPath.to_string ldir ^ "\n"); if !Flags.xml_export then Hook.get f_xml_start_library (); let wall_clock1 = Unix.gettimeofday () in - let _ = load_vernac verbosely long_f_dot_v in + let _ = load_vernac verbosely (Stm.get_current_state ()) long_f_dot_v in Stm.join (); let wall_clock2 = Unix.gettimeofday () in check_pending_proofs (); @@ -328,7 +285,7 @@ let compile verbosely f = let ldir = Flags.verbosely Library.start_library long_f_dot_vio in Dumpglob.noglob (); Stm.set_compilation_hints long_f_dot_vio; - let _ = load_vernac verbosely long_f_dot_v in + let _ = load_vernac verbosely (Stm.get_current_state ()) long_f_dot_v in Stm.finish (); check_pending_proofs (); Stm.snapshot_vio ldir long_f_dot_vio; diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli index 0d9f5871a..e75f8f9e8 100644 --- a/toplevel/vernac.mli +++ b/toplevel/vernac.mli @@ -8,30 +8,16 @@ (** Parsing of vernacular. *) -(** Read a vernac command on the specified input (parse only). - Raises [End_of_file] if EOF (or Ctrl-D) is reached. *) - -val parse_sentence : Pcoq.Gram.coq_parsable * in_channel option -> - Loc.t * Vernacexpr.vernac_expr - (** Reads and executes vernac commands from a stream. *) +val process_expr : Stateid.t -> Pcoq.Gram.coq_parsable -> Vernacexpr.vernac_expr Loc.located -> Stateid.t -exception End_of_input +(** [load_vernac echo sid file] Loads [file] on top of [sid], will + echo the commands if [echo] is set. *) +val load_vernac : bool -> Stateid.t -> string -> Stateid.t -val process_expr : Pcoq.Gram.coq_parsable -> Loc.t * Vernacexpr.vernac_expr -> unit +(** Compile a vernac file, (f is assumed without .v suffix) *) +val compile : bool -> string -> unit (** Set XML hooks *) val xml_start_library : (unit -> unit) Hook.t val xml_end_library : (unit -> unit) Hook.t - -(** Load a vernac file, verbosely or not. Errors are annotated with file - and location *) - -val load_vernac : bool -> string -> unit - - -(** Compile a vernac file, verbosely or not (f is assumed without .v suffix) *) - -val compile : bool -> string -> unit - -val is_navigation_vernac : Vernacexpr.vernac_expr -> bool |