diff options
Diffstat (limited to 'toplevel/coqloop.ml')
-rw-r--r-- | toplevel/coqloop.ml | 357 |
1 files changed, 212 insertions, 145 deletions
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index e9771cfa..3239d360 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -1,36 +1,36 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Pp -open CErrors -open Util -open Flags -open Vernac -open Pcoq -let top_stderr x = msg_with ~pp_tag:Ppstyle.pp_tag !Pp_control.err_ft x +let print_emacs = ref false + +let top_stderr x = + Format.fprintf !Topfmt.err_ft "@[%a@]%!" pp_with x (* A buffer for the character read from a channel. We store the command * entered to be able to report errors without pretty-printing. *) type input_buffer = { - mutable prompt : unit -> string; - mutable str : string; (* buffer of already read characters *) + mutable prompt : Stm.doc -> string; + mutable str : Bytes.t; (* buffer of already read characters *) mutable len : int; (* number of chars in the buffer *) mutable bols : int list; (* offsets in str of beginning of lines *) - mutable tokens : Gram.coq_parsable; (* stream of tokens *) + mutable tokens : Pcoq.Gram.coq_parsable; (* stream of tokens *) mutable start : int } (* stream count of the first char of the buffer *) (* Double the size of the buffer. *) -let resize_buffer ibuf = - let nstr = String.create (2 * String.length ibuf.str + 1) in - String.blit ibuf.str 0 nstr 0 (String.length ibuf.str); +let resize_buffer ibuf = let open Bytes in + let nstr = create (2 * length ibuf.str + 1) in + blit ibuf.str 0 nstr 0 (length ibuf.str); ibuf.str <- nstr (* Delete all irrelevant lines of the input buffer. Keep the last line @@ -40,7 +40,7 @@ let resynch_buffer ibuf = match ibuf.bols with | ll::_ -> let new_len = ibuf.len - ll in - String.blit ibuf.str ll ibuf.str 0 new_len; + Bytes.blit ibuf.str ll ibuf.str 0 new_len; ibuf.len <- new_len; ibuf.bols <- []; ibuf.start <- ibuf.start + ll @@ -49,24 +49,22 @@ let resynch_buffer ibuf = (* emacs special prompt tag for easy detection. No special character, to avoid interfering with utf8. Compatibility code removed. *) - -let emacs_prompt_startstring() = Printer.emacs_str "<prompt>" - -let emacs_prompt_endstring() = Printer.emacs_str "</prompt>" +let emacs_prompt_startstring () = if !print_emacs then "<prompt>" else "" +let emacs_prompt_endstring () = if !print_emacs then "</prompt>" else "" (* Read a char in an input channel, displaying a prompt at every beginning of line. *) -let prompt_char ic ibuf count = +let prompt_char doc ic ibuf count = let bol = match ibuf.bols with | ll::_ -> Int.equal ibuf.len ll | [] -> Int.equal ibuf.len 0 in - if bol && not !print_emacs then top_stderr (str (ibuf.prompt())); + if bol && not !print_emacs then top_stderr (str (ibuf.prompt doc)); try let c = input_char ic in if c == '\n' then ibuf.bols <- (ibuf.len+1) :: ibuf.bols; - if ibuf.len == String.length ibuf.str then resize_buffer ibuf; - ibuf.str.[ibuf.len] <- c; + if ibuf.len == Bytes.length ibuf.str then resize_buffer ibuf; + Bytes.set ibuf.str ibuf.len c; ibuf.len <- ibuf.len + 1; Some c with End_of_file -> @@ -74,21 +72,22 @@ let prompt_char ic ibuf count = (* Reinitialize the char stream (after a Drop) *) -let reset_input_buffer ic ibuf = - ibuf.str <- ""; +let reset_input_buffer doc ic ibuf = + ibuf.str <- Bytes.empty; ibuf.len <- 0; ibuf.bols <- []; - ibuf.tokens <- Gram.parsable (Stream.from (prompt_char ic ibuf)); + ibuf.tokens <- Pcoq.Gram.parsable (Stream.from (prompt_char doc ic ibuf)); ibuf.start <- 0 (* Functions to print underlined locations from an input buffer. *) +module TopErr = struct (* Given a location, returns the list of locations of each line. The last line is returned separately. It also checks the location bounds. *) let get_bols_of_loc ibuf (bp,ep) = let add_line (b,e) lines = - if b < 0 || e < b then anomaly (Pp.str "Bad location"); + if b < 0 || e < b then CErrors.anomaly (Pp.str "Bad location."); match lines with | ([],None) -> ([], Some (b,e)) | (fl,oe) -> ((b,e)::fl, oe) @@ -109,86 +108,93 @@ let dotted_location (b,e) = else (String.make (e-b-1) '.', " ") -let blanch_utf8_string s bp ep = - let s' = String.make (ep-bp) ' ' in +let blanch_utf8_string s bp ep = let open Bytes in + let s' = make (ep-bp) ' ' in let j = ref 0 in for i = bp to ep - 1 do - let n = Char.code s.[i] in + let n = Char.code (get s i) in (* Heuristic: assume utf-8 chars are printed using a single fixed-size char and therefore contract all utf-8 code into one space; in any case, preserve tabulation so that its effective interpretation in terms of spacing is preserved *) - if s.[i] == '\t' then s'.[!j] <- '\t'; + if get s i == '\t' then set s' !j '\t'; if n < 0x80 || 0xC0 <= n then incr j done; - String.sub s' 0 !j + Bytes.sub_string s' 0 !j + +let adjust_loc_buf ib loc = let open Loc in + { loc with ep = loc.ep - ib.start; bp = loc.bp - ib.start } let print_highlight_location ib loc = let (bp,ep) = Loc.unloc loc in - let bp = bp - ib.start - and ep = ep - ib.start in let highlight_lines = match get_bols_of_loc ib (bp,ep) with | ([],(bl,el)) -> let shift = blanch_utf8_string ib.str bl bp in let span = String.length (blanch_utf8_string ib.str bp ep) in - (str"> " ++ str(String.sub ib.str bl (el-bl-1)) ++ fnl () ++ + (str"> " ++ str(Bytes.sub_string ib.str bl (el-bl-1)) ++ fnl () ++ str"> " ++ str(shift) ++ str(String.make span '^')) | ((b1,e1)::ml,(bn,en)) -> let (d1,s1) = dotted_location (b1,bp) in let (dn,sn) = dotted_location (ep,en) in let l1 = (str"> " ++ str d1 ++ str s1 ++ - str(String.sub ib.str bp (e1-bp))) in + str(Bytes.sub_string ib.str bp (e1-bp))) in let li = prlist (fun (bi,ei) -> - (str"> " ++ str(String.sub ib.str bi (ei-bi)))) ml in - let ln = (str"> " ++ str(String.sub ib.str bn (ep-bn)) ++ + (str"> " ++ str(Bytes.sub_string ib.str bi (ei-bi)))) ml in + let ln = (str"> " ++ str(Bytes.sub_string ib.str bn (ep-bn)) ++ str sn ++ str dn) in (l1 ++ li ++ ln) in - let loc = Loc.make_loc (bp,ep) in - (Pp.pr_loc loc ++ highlight_lines ++ fnl ()) - -(* Functions to report located errors in a file. *) - -let print_location_in_file loc = - let fname = loc.Loc.fname in - let errstrm = str"Error while reading " ++ str fname in - if Loc.is_ghost loc then - hov 1 (errstrm ++ spc() ++ str" (unknown location):") ++ fnl () - else - let errstrm = mt () - (* if String.equal outer_fname fname then mt() else errstrm ++ str":" ++ fnl() *) - in - let open Loc in - hov 0 (* No line break so as to follow emacs error message format *) - (errstrm ++ Pp.pr_loc loc) + highlight_lines let valid_buffer_loc ib loc = - not (Loc.is_ghost loc) && let (b,e) = Loc.unloc loc in b-ib.start >= 0 && e-ib.start < ib.len && b<=e +(* Toplevel error explanation. *) +let error_info_for_buffer ?loc buf = + Option.map (fun loc -> + let fname = loc.Loc.fname in + let hl, loc = + (* We are in the toplevel *) + match fname with + | Loc.ToplevelInput -> + let nloc = adjust_loc_buf buf loc in + if valid_buffer_loc buf loc then + (fnl () ++ print_highlight_location buf nloc, nloc) + (* in the toplevel, but not a valid buffer *) + else (mt (), nloc) + (* we are in batch mode, don't adjust location *) + | Loc.InFile _ -> + (mt (), loc) + in Topfmt.pr_loc loc ++ hl + ) loc + +(* Actual printing routine *) +let print_error_for_buffer ?loc lvl msg buf = + let pre_hdr = error_info_for_buffer ?loc buf in + if !print_emacs + then Topfmt.emacs_logger ?pre_hdr lvl msg + else Topfmt.std_logger ?pre_hdr lvl msg + +(* +let print_toplevel_parse_error (e, info) buf = + let loc = Loc.get_loc info in + let lvl = Feedback.Error in + let msg = CErrors.iprint (e, info) in + print_error_for_buffer ?loc lvl msg buf +*) +end + (*s The Coq prompt is the name of the focused proof, if any, and "Coq" otherwise. We trap all exceptions to prevent the error message printing from cycling. *) let make_prompt () = try - (Names.Id.to_string (Pfedit.get_current_proof_name ())) ^ " < " + (Names.Id.to_string (Proof_global.get_current_proof_name ())) ^ " < " with Proof_global.NoCurrentProof -> "Coq < " -(*let build_pending_list l = - let pl = ref ">" in - let l' = ref l in - let res = - while List.length !l' > 1 do - pl := !pl ^ "|" Names.Id.to_string x; - l':=List.tl !l' - done in - let last = try List.hd !l' with _ -> in - "<"^l' -*) - (* the coq prompt added to the default one when in emacs mode The prompt contains the current state label [n] (for global backtracking) and the current proof state [p] (for proof @@ -197,70 +203,50 @@ let make_prompt () = "n |lem1|lem2|lem3| p < " *) -let make_emacs_prompt() = - let statnum = Stateid.to_string (Stm.get_current_state ()) in - let dpth = Stm.current_proof_depth() in - let pending = Stm.get_all_proof_names() in +let make_emacs_prompt doc = + let statnum = Stateid.to_string (Stm.get_current_state ~doc) in + let dpth = Stm.current_proof_depth ~doc in + let pending = Stm.get_all_proof_names ~doc in let pendingprompt = List.fold_left - (fun acc x -> acc ^ (if String.is_empty acc then "" else "|") ^ Names.Id.to_string x) + (fun acc x -> acc ^ (if CString.is_empty acc then "" else "|") ^ Names.Id.to_string x) "" pending in let proof_info = if dpth >= 0 then string_of_int dpth else "0" in - if !Flags.print_emacs then statnum ^ " |" ^ pendingprompt ^ "| " ^ proof_info ^ " < " + if !print_emacs then statnum ^ " |" ^ pendingprompt ^ "| " ^ proof_info ^ " < " else "" (* A buffer to store the current command read on stdin. It is * initialized when a vernac command is immediately followed by "\n", * or after a Drop. *) let top_buffer = - let pr() = + let pr doc = emacs_prompt_startstring() ^ make_prompt() - ^ make_emacs_prompt() + ^ make_emacs_prompt doc ^ emacs_prompt_endstring() in { prompt = pr; - str = ""; + str = Bytes.empty; len = 0; bols = []; - tokens = Gram.parsable (Stream.of_list []); + tokens = Pcoq.Gram.parsable (Stream.of_list []); start = 0 } let set_prompt prompt = top_buffer.prompt - <- (fun () -> + <- (fun doc -> emacs_prompt_startstring() ^ prompt () ^ emacs_prompt_endstring()) -(* The following exceptions need not be located. *) - -let locate_exn = function - | Out_of_memory | Stack_overflow | Sys.Break -> false - | _ -> true - -(* Toplevel error explanation. *) - -let print_toplevel_error (e, info) = - let loc = Option.default Loc.ghost (Loc.get_loc info) in - let fname = loc.Loc.fname in - let locmsg = - if Loc.is_ghost loc || String.equal fname "" then - if locate_exn e && valid_buffer_loc top_buffer loc then - print_highlight_location top_buffer loc - else mt () - else print_location_in_file loc - in - locmsg ++ CErrors.iprint (e, info) - (* Read the input stream until a dot is encountered *) let parse_to_dot = - let rec dot st = match Compat.get_tok (Stream.next st) with + 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 + Pcoq.Gram.Entry.of_parser "Coqtoplevel.dot" dot (* If an error occurred while parsing, we try to read the input until a dot token is encountered. @@ -268,20 +254,56 @@ let parse_to_dot = let rec discard_to_dot () = try - Gram.entry_parse parse_to_dot top_buffer.tokens + Pcoq.Gram.entry_parse parse_to_dot top_buffer.tokens with - | Compat.Token.Error _ | CLexer.Error.E _ -> discard_to_dot () - | End_of_input -> raise End_of_input + | Token.Error _ | CLexer.Error.E _ -> discard_to_dot () + | 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 ~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 (); - iraise reraise + (* The caller of read_sentence does the error printing now, this + should be re-enabled once we rely on the feedback error + printer again *) + (* TopErr.print_toplevel_parse_error reraise top_buffer; *) + Exninfo.iraise reraise + +let extract_default_loc loc doc_id sid : Loc.t option = + match loc with + | Some _ -> loc + | None -> + try + let doc = Stm.get_doc doc_id in + Option.cata fst None Stm.(get_ast ~doc sid) + with _ -> loc + +(** Coqloop Console feedback handler *) +let coqloop_feed (fb : Feedback.feedback) = let open Feedback in + match fb.contents with + | Processed -> () + | Incomplete -> () + | Complete -> () + | ProcessingIn _ -> () + | InProgress _ -> () + | WorkerStatus (_,_) -> () + | AddedAxiom -> () + | GlobRef (_,_,_,_,_) -> () + | GlobDef (_,_,_,_) -> () + | FileDependency (_,_) -> () + | FileLoaded (_,_) -> () + | Custom (_,_,_) -> () + (* Re-enable when we switch back to feedback-based error printing *) + | Message (Error,loc,msg) -> () + (* TopErr.print_error_for_buffer ?loc lvl msg top_buffer *) + | Message (Warning,loc,msg) -> + let loc = extract_default_loc loc fb.doc_id fb.span_id in + TopErr.print_error_for_buffer ?loc Warning msg top_buffer + | 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: @@ -293,24 +315,29 @@ let read_sentence input = is caught and handled (i.e. not re-raised). *) -let do_vernac () = +let do_vernac ~time ~state = + let open Vernac.State in top_stderr (fnl()); - if !print_emacs then top_stderr (str (top_buffer.prompt())); + 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 top_buffer.tokens (read_sentence input) + Vernac.process_expr ~time ~state (read_sentence ~state (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_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 any = CErrors.push any in - let msg = print_toplevel_error any ++ fnl () in - pp_with ~pp_tag:Ppstyle.pp_tag !Pp_control.std_ft msg; - Format.pp_print_flush !Pp_control.std_ft () + 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. @@ -318,37 +345,77 @@ let do_vernac () = exit the loop are Drop and Quit. Any other exception there indicates an issue with [print_toplevel_error] above. *) -(* -let feed_emacs = function - | { Interface.id = Interface.State id; - Interface.content = Interface.GlobRef (_,a,_,c,_) } -> - prerr_endline ("<info>" ^"<id>"^Stateid.to_string id ^"</id>" - ^a^" "^c^ "</info>") - | _ -> () -*) - (* Flush in a compatible order with 8.5 *) (* This mimics the semantics of the old Pp.flush_all *) let loop_flush_all () = Pervasives.flush stderr; Pervasives.flush stdout; - Format.pp_print_flush !Pp_control.std_ft (); - Format.pp_print_flush !Pp_control.err_ft () + Format.pp_print_flush !Topfmt.std_ft (); + Format.pp_print_flush !Topfmt.err_ft () + +let pr_open_cur_subgoals () = + try + let proof = Proof_global.give_me_the_proof () in + Printer.pr_open_subgoals ~proof + with Proof_global.NoCurrentProof -> Pp.str "" + +(* Goal equality heuristic. *) +let pequal cmp1 cmp2 (a1,a2) (b1,b2) = cmp1 a1 b1 && cmp2 a2 b2 +let evleq e1 e2 = CList.equal Evar.equal e1 e2 +let cproof p1 p2 = + let (a1,a2,a3,a4,_),(b1,b2,b3,b4,_) = Proof.proof p1, Proof.proof p2 in + evleq a1 b1 && + CList.equal (pequal evleq evleq) a2 b2 && + CList.equal Evar.equal a3 b3 && + CList.equal Evar.equal a4 b4 + +(* We try to behave better when goal printing raises an exception + [usually Ctrl-C] + + This is mostly a hack as we should protect printing in a more + generic way, but that'll do for now *) +let top_goal_print oldp newp = + try + let proof_changed = not (Option.equal cproof oldp newp) 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 ()) + with + | CErrors.Drop | CErrors.Quit as exn -> raise exn + | exn -> + let (e, info) = CErrors.push exn 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 + +let drop_last_doc = ref None -let rec loop () = +let rec loop ~time ~state = + let open Vernac.State in 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 + 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 + top_goal_print state.proof nstate.proof; + loop_flush_all (); + vernac_loop ~state:nstate + in vernac_loop ~state with - | CErrors.Drop -> () + | 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 | any -> - Feedback.msg_error (str"Anomaly: main loop exited with exception: " ++ - str (Printexc.to_string any) ++ - fnl() ++ - str"Please report" ++ - strbrk" at " ++ str Coq_config.wwwbugtracker ++ str "."); - loop () + 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 |