diff options
Diffstat (limited to 'toplevel/toplevel.ml')
-rw-r--r-- | toplevel/toplevel.ml | 298 |
1 files changed, 298 insertions, 0 deletions
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml new file mode 100644 index 000000000..dcad19bed --- /dev/null +++ b/toplevel/toplevel.ml @@ -0,0 +1,298 @@ + +(* $Id$ *) + +open Pp +open Util +open Options +open Errors +open Vernac +open Pcoq +open Protectedtoplevel + +(* 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 len : int; (* number of chars in the buffer *) + mutable bols : int list; (* offsets in str of begining of lines *) + mutable tokens : Gram.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); + ibuf.str <- nstr + +(* Delete all irrelevent lines of the input buffer. Keep the last line + in the buffer (useful when there are several commands on the same line. *) + +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; + ibuf.len <- new_len; + ibuf.bols <- []; + ibuf.start <- ibuf.start + ll + | _ -> () + +(* Read a char in an input channel, displaying a prompt af every + begining of line. *) + +let prompt_char ic ibuf count = + let bol = match ibuf.bols with + | ll::_ -> ibuf.len == ll + | [] -> ibuf.len == 0 + in + if bol then mSGERR [< 'sTR (ibuf.prompt()) >]; + 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; + ibuf.len <- ibuf.len + 1; + Some c + with End_of_file -> + None + +(* Reinitialize the char stream (after a Drop) *) + +let reset_input_buffer ic ibuf = + ibuf.str <- ""; + ibuf.len <- 0; + ibuf.bols <- []; + ibuf.tokens <- Gram.parsable (Stream.from (prompt_char ic ibuf)); + ibuf.start <- 0 + +(* Functions to print underlined locations from an input buffer. *) + +(* 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 or e < b then anomaly "Bad location"; + match lines with + | ([],None) -> ([], Some (b,e)) + | (fl,oe) -> ((b,e)::fl, oe) + in + let rec lines_rec ba after = function + | [] -> add_line (0,ba) after + | ll::_ when ll <= bp -> add_line (ll,ba) after + | ll::fl -> + let nafter = if ll < ep then add_line (ll,ba) after else after in + lines_rec ll nafter fl + in + let (fl,ll) = lines_rec ibuf.len ([],None) ibuf.bols in + (fl,out_some ll) + +let dotted_location (b,e) = + if e-b < 3 then + ("", String.make (e-b) ' ') + else + (String.make (e-b-1) '.', " ") + +let print_highlight_location ib (bp,ep) = + 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)) -> + [< 'sTR"> "; 'sTR(String.sub ib.str bl (el-bl)); + 'sTR"> "; 'sTR(String.make (bp-bl) ' '); + 'sTR(String.make (ep-bp) '^') >] + | ((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 + 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 sn; 'sTR dn >] in + [< l1; li; ln >] + in + [< 'sTR"Toplevel input, characters "; Errors.print_loc (bp,ep); 'fNL; + highlight_lines; 'fNL >] + +(* Functions to report located errors in a file. *) + +let print_location_in_file s fname (bp,ep) = + let errstrm = [< 'sTR"Error while reading "; 'sTR s; 'sTR" :"; 'fNL; + 'sTR"File "; 'sTR ("\""^fname^"\"") >] in + if (bp,ep) = Ast.dummy_loc + then + [< errstrm; 'sTR", unknown location."; 'fNL >] + else + let ic = open_in fname in + let rec line_of_pos lin bol cnt = + if cnt < bp then + if input_char ic == '\n' + then line_of_pos (lin + 1) (cnt +1) (cnt+1) + else line_of_pos lin bol (cnt+1) + else (lin, bol) + in + try + let (line, bol) = line_of_pos 1 0 0 in + close_in ic; + [< errstrm; 'sTR", line "; 'iNT line; + 'sTR", characters "; Errors.print_loc (bp-bol,ep-bol); 'fNL >] + with e -> (close_in ic; [< errstrm; 'sTR", invalid location."; 'fNL >]) + +let print_command_location ib dloc = + match dloc with + | Some (bp,ep) -> + [< 'sTR"Error during interpretation of command:"; 'fNL; + 'sTR(String.sub ib.str (bp-ib.start) (ep-bp)); 'fNL >] + | None -> [<>] + +let valid_loc dloc (b,e) = + (b,e) <> Ast.dummy_loc + & match dloc with + | Some (bd,ed) -> bd<=b & e<=ed + | _ -> true + +let valid_buffer_loc ib dloc (b,e) = + valid_loc dloc (b,e) & b-ib.start >= 0 & e-ib.start < ib.len & b<=e + +(* 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() = + (Pfedit.proof_prompt())^(emacs_str (String.make 1 (Char.chr 249))) + in + { prompt = pr; + str = ""; + len = 0; + bols = []; + tokens = Gram.parsable [<>]; + start = 0 } + +let set_prompt prompt = + top_buffer.prompt + <- (fun () -> (prompt ()) ^ (emacs_str (String.make 1 (Char.chr 249)))) + +(* Removes and prints the location of the error. The following exceptions + need not be located. *) +let rec is_pervasive_exn = function + | Out_of_memory | Stack_overflow | Sys.Break -> true + | Error_in_file (_,_,e) -> is_pervasive_exn e + | Stdpp.Exc_located (_,e) -> is_pervasive_exn e + | DuringCommandInterp (_,e) -> is_pervasive_exn e + | _ -> false + +(* Toplevel error explanation, dealing with locations, Drop, Ctrl-D + May raise only the following exceptions: Drop and End_of_input, + meaning we get out of the Coq loop *) +let print_toplevel_error exc = + let (dloc,exc) = + match exc with + | DuringCommandInterp (loc,ie) -> + if loc = Ast.dummy_loc then (None,ie) else (Some loc, ie) + | _ -> (None, exc) + in + let (locstrm,exc) = + match exc with + | Stdpp.Exc_located (loc, ie) -> + if valid_buffer_loc top_buffer dloc loc then + (print_highlight_location top_buffer loc, ie) + else + (print_command_location top_buffer dloc, ie) + | Error_in_file (s, (fname, loc), ie) -> + (print_location_in_file s fname loc, ie) + | _ -> (print_command_location top_buffer dloc, exc) + in + match exc with + | End_of_input -> + mSGERRNL [<>]; pp_flush(); exit 0 + | Vernacinterp.Drop -> (* Last chance *) + if Mltop.is_ocaml_top() then raise Vernacinterp.Drop; + [< 'sTR"There is no ML toplevel."; 'fNL >] + | Vernacinterp.ProtectedLoop -> + raise Vernacinterp.ProtectedLoop + | Vernacinterp.Quit -> + raise Vernacinterp.Quit + | _ -> + [< if is_pervasive_exn exc then [<>] else locstrm; + Errors.explain_exn exc >] + +(* Read the input stream until a dot is encountered *) +let parse_to_dot = + let rec dot = parser + | [< '("", ".") >] -> () + | [< '("EOI", "") >] -> raise End_of_input + | [< '_; s >] -> dot s + in + Gram.Entry.of_parser "Coqtoplevel.dot" dot + +(* We assume that when a lexer error occurs, at least one char was eaten *) +let rec discard_to_dot () = + try + Gram.Entry.parse parse_to_dot top_buffer.tokens + with Stdpp.Exc_located(_,Token.Error _) -> + discard_to_dot() + + +(* If the error occured while parsing, we read the input until a dot token + * in encountered. + *) +let process_error = function + | DuringCommandInterp _ as e -> e + | e -> + if is_pervasive_exn e then + e + else + try + discard_to_dot (); e + with + | End_of_input -> End_of_input + | de -> if is_pervasive_exn de then de else e + +(* 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 *) +let do_vernac () = + mSGERRNL [<>]; + resynch_buffer top_buffer; + begin + try + raw_do_vernac top_buffer.tokens + with e -> mSGNL (print_toplevel_error (process_error e)) + end; + flush_all() + +(* coq and go read vernacular expressions until Drop is entered. + * Ctrl-C will raise the exception Break instead of aborting Coq. + * Here we catch the exceptions terminating the Coq loop, and decide + * if we really must quit. + * The boolean value is used to choose between a protected loop, which + * we think is more suited for communication with other programs, or + * plain communication. *) + +let rec coq_switch b = + Sys.catch_break true; + try + if b then begin + reset_input_buffer stdin top_buffer; + while true do do_vernac() done + end else + protected_loop stdin + with + | Vernacinterp.Drop -> () + | Vernacinterp.ProtectedLoop -> coq_switch false + | End_of_input -> mSGERRNL [<>]; pp_flush(); exit 0 + | Vernacinterp.Quit -> exit 0 + | e -> + mSGERRNL [< 'sTR"Anomaly in the toplevel loop. Please report." >]; + coq_switch b + +let loop () = coq_switch true |