summaryrefslogtreecommitdiff
path: root/toplevel/coqloop.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/coqloop.ml')
-rw-r--r--toplevel/coqloop.ml357
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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-07 23:01:30 +0000