From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 27 Dec 2016 16:53:30 +0100 Subject: Imported Upstream version 8.6 --- toplevel/vernac.ml | 287 ++++++++++++++++++++++++++--------------------------- 1 file changed, 140 insertions(+), 147 deletions(-) (limited to 'toplevel/vernac.ml') diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 7c4920df..bfdae85d 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -9,27 +9,29 @@ (* Parsing of vernacular. *) open Pp -open Errors +open CErrors open Util open Flags -open System open Vernacexpr (* 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). *) -(* The navigation vernac commands will be handled separately *) +let user_error loc s = CErrors.user_err_loc (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 _ -> true - | VernacRedirect (_, l) | VernacTime l -> - List.exists - (fun (_,c) -> is_navigation_vernac c) l (* Time Back* is harmless *) + | 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 @@ -42,6 +44,14 @@ let is_reset = function | VernacResetInitial | VernacResetName _ -> true | _ -> false +let checknav_simple loc cmd = + if is_navigation_vernac cmd && not (is_reset cmd) then + user_error loc "Navigation commands forbidden in files." + +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, @@ -66,32 +76,10 @@ let _ = Goptions.optread = (fun () -> !atomic_load); Goptions.optwrite = ((:=) atomic_load) } -(* In case of error, register the file being currently Load'ed and the - inner file in which the error has been encountered. Any intermediate files - between the two are discarded. *) - -type location_files = { outer : string; inner : string } - -let files_of_exn : location_files Exninfo.t = Exninfo.make () - -let get_exn_files e = Exninfo.get e files_of_exn - -let add_exn_files e f = Exninfo.add e files_of_exn f - -let enrich_with_file f (e, info) = - let inner = match get_exn_files info with None -> f | Some x -> x.inner in - (e, add_exn_files info { outer = f; inner }) - -let raise_with_file f e = iraise (enrich_with_file f e) - -let cur_file = ref None - let disable_drop = function - | Drop -> Errors.error "Drop is forbidden." + | Drop -> CErrors.error "Drop is forbidden." | e -> e -let user_error loc s = Errors.user_err_loc (loc,"_",str s) - (* 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 @@ -101,7 +89,7 @@ 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 (Stream.of_channel in_chan) 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) = @@ -110,7 +98,7 @@ let close_input in_chan (_,verb) = match verb with | Some verb_ch -> close_in verb_ch | _ -> () - with e when Errors.noncritical e -> () + with e when CErrors.noncritical e -> () let verbose_phrase verbch loc = let loc = Loc.unloc loc in @@ -120,8 +108,7 @@ let verbose_phrase verbch loc = let s = String.create len in seek_in ch (fst loc); really_input ch s 0 len; - ppnl (str s); - pp_flush() + Feedback.msg_notice (str s) | None -> () exception End_of_input @@ -135,51 +122,44 @@ let parse_sentence = Flags.with_option Flags.we_are_parsing (* vernac parses the given stream, executes interpfun on the syntax tree it * parses, and is verbose on "primitives" commands if verbosely is true *) -let just_parsing = ref false let chan_beautify = ref stdout let beautify_suffix = ".beautified" -let set_formatter_translator() = - let ch = !chan_beautify in +let set_formatter_translator ch = let out s b e = output ch s b e in Format.set_formatter_output_functions out (fun () -> flush ch); Format.set_max_boxes max_int -let pr_new_syntax loc ocom = +let pr_new_syntax_in_context loc chan_beautify ocom = let loc = Loc.unloc loc in - if !beautify_file then set_formatter_translator(); + if !beautify_file then set_formatter_translator chan_beautify; let fs = States.freeze ~marshallable:`No in - let com = match ocom with - | Some VernacNop -> mt() - | Some com -> Ppvernac.pr_vernac com - | None -> mt() in - if !beautify_file then - msg (hov 0 (comment (fst loc) ++ com ++ comment (snd loc))) - else - msg_info (hov 4 (str"New Syntax:" ++ fnl() ++ (hov 0 com))); - States.unfreeze fs; - Format.set_formatter_out_channel stdout - -let save_translator_coqdoc () = - (* translator state *) - let ch = !chan_beautify in - let cl = !Pp.comments in - let cs = Lexer.com_state() in - (* end translator state *) - let coqdocstate = Lexer.location_table () in - ch,cl,cs,coqdocstate - -let restore_translator_coqdoc (ch,cl,cs,coqdocstate) = - if !Flags.beautify_file then close_out !chan_beautify; - chan_beautify := ch; - Pp.comments := cl; - Lexer.restore_com_state cs; - Lexer.restore_location_table coqdocstate + (* The content of this is not supposed to fail, but if ever *) + try + (* Side-effect: order matters *) + let before = comment (CLexer.extract_comments (fst loc)) in + let com = match ocom with + | Some com -> Ppvernac.pr_vernac com + | None -> mt() in + let after = comment (CLexer.extract_comments (snd loc)) in + if !beautify_file then + Pp.msg_with !Pp_control.std_ft (hov 0 (before ++ com ++ after)) + else + Feedback.msg_info (hov 4 (str"New Syntax:" ++ fnl() ++ (hov 0 com))); + States.unfreeze fs; + Format.set_formatter_out_channel stdout + with any -> + States.unfreeze fs; + Format.set_formatter_out_channel stdout + +let pr_new_syntax po loc chan_beautify ocom = + (* Reinstall the context of parsing which includes the bindings of comments to locations *) + Pcoq.Gram.with_parsable po (pr_new_syntax_in_context chan_beautify loc) ocom (* For coqtop -time, we display the position in the file, and a glimpse of the executed command *) -let display_cmd_header loc com = +let pp_cmd_header loc com = let shorten s = try (String.sub s 0 30)^"..." with _ -> s in let noblank s = for i = 0 to String.length s - 1 do @@ -194,75 +174,63 @@ let display_cmd_header loc com = try Ppvernac.pr_vernac x with e -> str (Printexc.to_string e) in let cmd = noblank (shorten (string_of_ppcmds (safe_pr_vernac com))) - in - Pp.pp (str "Chars " ++ int start ++ str " - " ++ int stop ++ - str " [" ++ str cmd ++ str "] "); - Pp.flush_all () + in str "Chars " ++ int start ++ str " - " ++ int stop ++ + str " [" ++ str cmd ++ str "] " -let rec vernac_com verbose checknav (loc,com) = +(* This is a special case where we assume we are in console batch mode + and take control of the console. + *) +let print_cmd_header loc com = + Pp.pp_with ~pp_tag:Ppstyle.pp_tag !Pp_control.std_ft (pp_cmd_header loc com); + Format.pp_print_flush !Pp_control.std_ft () + +let rec interp_vernac po chan_beautify checknav (loc,com) = let interp = function | VernacLoad (verbosely, fname) -> - let fname = Envars.expand_path_macros ~warn:(fun x -> msg_warning (str x)) fname in + 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 - let st = save_translator_coqdoc () in - if !Flags.beautify_file then - begin - chan_beautify := open_out (f^beautify_suffix); - Pp.comments := [] - end; - begin - try - read_vernac_file verbosely f; - restore_translator_coqdoc st; - with reraise -> - let reraise = Errors.push reraise in - restore_translator_coqdoc st; - iraise reraise - end - - | v when !just_parsing -> () - - | v -> Stm.interp verbose (loc,v) + load_vernac verbosely f + + | v -> Stm.interp (Flags.is_verbose()) (loc,v) in try checknav loc com; - if do_beautify () then pr_new_syntax loc (Some com); - if !Flags.time then display_cmd_header loc com; - let com = if !Flags.time then VernacTime [loc,com] else com in + if !beautify then pr_new_syntax po chan_beautify loc (Some com); + (* XXX: This is not 100% correct if called from an IDE context *) + if !Flags.time then print_cmd_header loc com; + let com = if !Flags.time then VernacTime (loc,com) else com in interp com with reraise -> - let (reraise, info) = Errors.push reraise in - Format.set_formatter_out_channel stdout; + let (reraise, info) = CErrors.push reraise in let loc' = Option.default Loc.ghost (Loc.get_loc info) in if Loc.is_ghost loc' then iraise (reraise, Loc.add_loc info loc) else iraise (reraise, info) -and read_vernac_file verbosely s = - let checknav loc cmd = - if is_navigation_vernac cmd && not (is_reset cmd) then - user_error loc "Navigation commands forbidden in files" - in - let (in_chan, fname, input) = open_file_twice_if verbosely s in - cur_file := Some fname; +(* Load a vernac file. CErrors are annotated with file and location *) +and load_vernac verbosely 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 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 = parse_sentence input in - vernac_com verbosely checknav loc_ast; - pp_flush () + 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 with any -> (* whatever the exception *) - let (e, info) = Errors.push any in - Format.set_formatter_out_channel stdout; + let (e, info) = CErrors.push any in close_input in_chan input; (* we must close the file first *) match e with | End_of_input -> - cur_file := None; - if do_beautify () then - pr_new_syntax (Loc.make_loc (max_int,max_int)) None - | _ -> raise_with_file fname (disable_drop e, info) + if !beautify then + pr_new_syntax (fst input) chan_beautify (Loc.make_loc (max_int,max_int)) None; + if !Flags.beautify_file then close_out chan_beautify; + | reraise -> + if !Flags.beautify_file then close_out chan_beautify; + iraise (disable_drop e, info) (** [eval_expr : ?preserving:bool -> Loc.t * Vernacexpr.vernac_expr -> unit] It executes one vernacular command. By default the command is @@ -271,34 +239,50 @@ and read_vernac_file verbosely s = of a new state label). An example of state-preserving command is one coming from the query panel of Coqide. *) -let checknav loc ast = - if is_deep_navigation_vernac ast then - user_error loc "Navigation commands forbidden in nested commands" - -let eval_expr loc_ast = vernac_com (Flags.is_verbose()) checknav loc_ast +let process_expr po loc_ast = interp_vernac po stdout checknav_deep loc_ast (* XML output hooks *) let (f_xml_start_library, xml_start_library) = Hook.make ~default:ignore () let (f_xml_end_library, xml_end_library) = Hook.make ~default:ignore () -(* Load a vernac file. Errors are annotated with file and location *) -let load_vernac verb file = - chan_beautify := - if !Flags.beautify_file then open_out (file^beautify_suffix) else stdout; - try - Flags.silently (read_vernac_file verb) file; - if !Flags.beautify_file then close_out !chan_beautify; - with any -> - let (e, info) = Errors.push any in - if !Flags.beautify_file then close_out !chan_beautify; - raise_with_file file (disable_drop e, info) +let warn_file_no_extension = + CWarnings.create ~name:"file-no-extension" ~category:"filesystem" + (fun (f,ext) -> + str "File \"" ++ str f ++ + strbrk "\" has been implicitly expanded to \"" ++ + str f ++ str ext ++ str "\"") -let ensure_v f = - if Filename.check_suffix f ".v" then f +let ensure_ext ext f = + if Filename.check_suffix f ext then f else begin - msg_warning (str "File \"" ++ str f ++ strbrk "\" has been implicitly \ - expanded to \"" ++ str f ++ str ".v\""); - f ^ ".v" + warn_file_no_extension (f,ext); + f ^ ext + end + +let chop_extension f = + try Filename.chop_extension f with _ -> f + +let ensure_bname src tgt = + let src, tgt = Filename.basename src, Filename.basename tgt in + let src, tgt = chop_extension src, chop_extension tgt in + if src <> tgt then begin + Feedback.msg_error (str "Source and target file names must coincide, directories can differ"); + Feedback.msg_error (str "Source: " ++ str src); + Feedback.msg_error (str "Target: " ++ str tgt); + flush_all (); + exit 1 + end + +let ensure ext src tgt = ensure_bname src tgt; ensure_ext ext tgt + +let ensure_v v = ensure ".v" v v +let ensure_vo v vo = ensure ".vo" v vo +let ensure_vio v vio = ensure ".vio" v vio + +let ensure_exists f = + if not (Sys.file_exists f) then begin + Feedback.msg_error (hov 0 (str "Can't find file" ++ spc () ++ str f)); + exit 1 end (* Compile a vernac file *) @@ -306,14 +290,21 @@ let compile verbosely f = let check_pending_proofs () = let pfs = Pfedit.get_all_proof_names () in if not (List.is_empty pfs) then - (msg_error (str "There are pending proofs"); flush_all (); exit 1) in + (Feedback.msg_error (str "There are pending proofs"); flush_all (); exit 1) in match !Flags.compilation_mode with | BuildVo -> let long_f_dot_v = ensure_v f in - let ldir = Flags.verbosely Library.start_library long_f_dot_v in - Stm.set_compilation_hints long_f_dot_v; - Aux_file.start_aux_file_for long_f_dot_v; - Dumpglob.start_dump_glob long_f_dot_v; + ensure_exists long_f_dot_v; + let long_f_dot_vo = + match !Flags.compilation_output_name with + | None -> long_f_dot_v ^ "o" + | Some f -> ensure_vo long_f_dot_v f in + let ldir = Flags.verbosely Library.start_library long_f_dot_vo in + Stm.set_compilation_hints long_f_dot_vo; + 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"); if !Flags.xml_export then Hook.get f_xml_start_library (); let wall_clock1 = Unix.gettimeofday () in @@ -321,7 +312,7 @@ let compile verbosely f = Stm.join (); let wall_clock2 = Unix.gettimeofday () in check_pending_proofs (); - Library.save_library_to ldir long_f_dot_v (Global.opaque_tables ()); + Library.save_library_to ldir long_f_dot_vo (Global.opaque_tables ()); Aux_file.record_in_aux_at Loc.ghost "vo_compile_time" (Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1)); Aux_file.stop_aux_file (); @@ -329,13 +320,18 @@ let compile verbosely f = Dumpglob.end_dump_glob () | BuildVio -> let long_f_dot_v = ensure_v f in - let ldir = Flags.verbosely Library.start_library long_f_dot_v in + ensure_exists long_f_dot_v; + let long_f_dot_vio = + match !Flags.compilation_output_name with + | None -> long_f_dot_v ^ "io" + | Some f -> ensure_vio long_f_dot_v f in + let ldir = Flags.verbosely Library.start_library long_f_dot_vio in Dumpglob.noglob (); - Stm.set_compilation_hints long_f_dot_v; + Stm.set_compilation_hints long_f_dot_vio; let _ = load_vernac verbosely long_f_dot_v in Stm.finish (); check_pending_proofs (); - Stm.snapshot_vio ldir long_f_dot_v; + Stm.snapshot_vio ldir long_f_dot_vio; Stm.reset_task_queue () | Vio2Vo -> let open Filename in @@ -352,8 +348,5 @@ let compile v f = compile v f; CoqworkmgrApi.giveback 1 -let () = Hook.set Stm.process_error_hook (fun e -> - match !cur_file with - | None -> Cerrors.process_vernac_interp_error e - | Some f -> enrich_with_file f (Cerrors.process_vernac_interp_error e) -) +let () = Hook.set Stm.process_error_hook + ExplainErr.process_vernac_interp_error -- cgit v1.2.3