From fb482f6b02156c1fcf029263083b0371e030a2cd Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 20 Sep 2017 08:30:24 +0200 Subject: [flags] Flag `open Flags` An incoming commit is removing some toplevel-specific global flags in favor of local toplevel state; this commit flags `Flags` use so it becomes clearer in the code whether we are relying on some "global" settable status in code. A good candidate for further cleanup is the pattern: `Flags.if_verbose Feedback.msg_info` --- checker/checker.ml | 7 +++---- pretyping/classops.ml | 3 +-- toplevel/coqtop.ml | 39 +++++++++++++++++++-------------------- toplevel/vernac.ml | 15 +++++++-------- vernac/command.ml | 3 +-- vernac/lemmas.ml | 5 ++--- vernac/metasyntax.ml | 7 +++---- vernac/mltop.ml | 3 +-- vernac/vernacentries.ml | 25 ++++++++++++------------- 9 files changed, 49 insertions(+), 58 deletions(-) diff --git a/checker/checker.ml b/checker/checker.ml index 7a69700d2..67b812133 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -10,7 +10,6 @@ open Pp open CErrors open Util open System -open Flags open Names open Check @@ -74,7 +73,7 @@ let add_path ~unix_path:dir ~coq_root:coq_dirpath = let convert_string d = try Id.of_string d with CErrors.UserError _ -> - if_verbose Feedback.msg_warning + Flags.if_verbose Feedback.msg_warning (str "Directory " ++ str d ++ str " cannot be used as a Coq identifier (skipped)"); raise Exit @@ -342,7 +341,7 @@ let parse_args argv = | ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage () | ("-v"|"--version") :: _ -> version () - | "-boot" :: rem -> boot := true; parse rem + | "-boot" :: rem -> Flags.boot := true; parse rem | ("-m" | "--memory") :: rem -> Check_stat.memory_stat := true; parse rem | ("-o" | "--output-context") :: rem -> Check_stat.output_context := true; parse rem @@ -374,7 +373,7 @@ let init_with_argv argv = parse_args argv; if !Flags.debug then Printexc.record_backtrace true; Envars.set_coqlib ~fail:(fun x -> CErrors.user_err Pp.(str x)); - if_verbose print_header (); + Flags.if_verbose print_header (); init_load_path (); engage (); with e -> diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 1cc072a2a..260cd0444 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -9,7 +9,6 @@ open CErrors open Util open Pp -open Flags open Names open Libnames open Globnames @@ -387,7 +386,7 @@ let add_coercion_in_graph (ic,source,target) = old_inheritance_graph end; let is_ambig = match !ambig_paths with [] -> false | _ -> true in - if is_ambig && not !quiet then + if is_ambig && not !Flags.quiet then Feedback.msg_info (message_ambig !ambig_paths) type coercion = { diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 0f8524e92..57902cb27 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -8,7 +8,6 @@ open Pp open CErrors -open Flags open Libnames open Coqinit @@ -31,7 +30,7 @@ let print_header () = Feedback.msg_notice (str "Welcome to Coq " ++ str ver ++ str " (" ++ str rev ++ str ")"); flush_all () -let warning s = with_option Flags.warn Feedback.msg_warning (strbrk s) +let warning s = Flags.(with_option warn Feedback.msg_warning (strbrk s)) let toploop = ref None @@ -87,7 +86,7 @@ let console_toploop_run () = (* We initialize the console only if we run the toploop_run *) let tl_feed = Feedback.add_feeder Coqloop.coqloop_feed in if Dumpglob.dump () then begin - if_verbose warning "Dumpglob cannot be used in interactive mode."; + Flags.if_verbose warning "Dumpglob cannot be used in interactive mode."; Dumpglob.noglob () end; Coqloop.loop(); @@ -130,7 +129,7 @@ let set_type_in_type () = let engage () = Global.set_engagement !impredicative_set -let set_batch_mode () = batch_mode := true +let set_batch_mode () = Flags.batch_mode := true let toplevel_default_name = Names.(DirPath.make [Id.of_string "Top"]) let toplevel_name = ref toplevel_default_name @@ -177,7 +176,7 @@ let load_vernacular sid = (fun sid (s,v) -> let s = Loadpath.locate_file s in if !Flags.beautify then - with_option beautify_file (Vernac.load_vernac v sid) s + Flags.(with_option beautify_file (Vernac.load_vernac v sid) s) else Vernac.load_vernac v sid s) sid (List.rev !load_vernacular_list) @@ -199,7 +198,7 @@ let require_prelude () = let require_list = ref ([] : string list) let add_require s = require_list := s :: !require_list let require () = - let () = if !load_init then silently require_prelude () in + let () = if !Flags.load_init then Flags.silently require_prelude () in let map dir = Qualid (Loc.tag @@ qualid_of_string dir) in Vernacentries.vernac_require None (Some false) (List.rev_map map !require_list) @@ -229,7 +228,7 @@ let add_compile verbose s = let compile_file (v,f) = if !Flags.beautify then - with_option beautify_file (Vernac.compile v) f + Flags.(with_option beautify_file (Vernac.compile v) f) else Vernac.compile v f @@ -304,7 +303,7 @@ let usage () = init_load_path (); with NoCoqLib -> usage_no_coqlib () end; - if !batch_mode then Usage.print_usage_coqc () + if !Flags.batch_mode then Usage.print_usage_coqc () else begin Mltop.load_ml_objects_raw_rex (Str.regexp (if Mltop.is_native then "^.*top.cmxs$" else "^.*top.cma$")); @@ -538,7 +537,7 @@ let parse_args arglist = |"-with-geoproof" -> Coq_config.with_geoproof := get_bool opt (next ()) |"-main-channel" -> Spawned.main_channel := get_host_port opt (next()) |"-control-channel" -> Spawned.control_channel := get_host_port opt (next()) - |"-vio2vo" -> add_compile false (next ()); Flags.compilation_mode := Vio2Vo + |"-vio2vo" -> add_compile false (next ()); Flags.compilation_mode := Flags.Vio2Vo |"-toploop" -> set_toploop (next ()) |"-w" | "-W" -> CWarnings.set_flags (CWarnings.normalize_flags_string (next ())) |"-o" -> Flags.compilation_output_name := Some (next()) @@ -551,9 +550,9 @@ let parse_args arglist = |"-async-proofs-never-reopen-branch" -> Flags.async_proofs_never_reopen_branch := true; |"-batch" -> set_batch_mode () - |"-test-mode" -> test_mode := true - |"-beautify" -> beautify := true - |"-boot" -> boot := true; no_load_rc () + |"-test-mode" -> Flags.test_mode := true + |"-beautify" -> Flags.beautify := true + |"-boot" -> Flags.boot := true; no_load_rc () |"-bt" -> Backtrace.record_backtrace true |"-color" -> set_color (next ()) |"-config"|"--config" -> print_config := true @@ -567,17 +566,17 @@ let parse_args arglist = |"-indices-matter" -> Indtypes.enforce_indices_matter () |"-just-parsing" -> warning "-just-parsing option has been removed in 8.6" |"-m"|"--memory" -> memory_stat := true - |"-noinit"|"-nois" -> load_init := false + |"-noinit"|"-nois" -> Flags.load_init := false |"-no-glob"|"-noglob" -> Dumpglob.noglob (); glob_opt := true |"-native-compiler" -> if Coq_config.no_native_compiler then warning "Native compilation was disabled at configure time." - else native_compiler := true + else Flags.native_compiler := true |"-output-context" -> output_context := true |"-profile-ltac" -> Flags.profile_ltac := true |"-q" -> no_load_rc () |"-quiet"|"-silent" -> Flags.quiet := true; Flags.make_warn false - |"-quick" -> Flags.compilation_mode := BuildVio + |"-quick" -> Flags.compilation_mode := Flags.BuildVio |"-list-tags" -> print_tags := true |"-time" -> Flags.time := true |"-type-in-type" -> set_type_in_type () @@ -620,11 +619,11 @@ let init_toplevel arglist = prerr_endline "See -help for the list of supported options"; exit 1 end; - if_verbose print_header (); + Flags.if_verbose print_header (); inputstate (); Mltop.init_known_plugins (); engage (); - if (not !batch_mode || CList.is_empty !compile_list) + if (not !Flags.batch_mode || CList.is_empty !compile_list) && Global.env_is_initial () then Declaremods.start_library !toplevel_name; init_library_roots (); @@ -645,16 +644,16 @@ let init_toplevel arglist = with any -> flush_all(); let extra = - if !batch_mode && not Stateid.(equal (Stm.get_current_state ()) dummy) + if !Flags.batch_mode && not Stateid.(equal (Stm.get_current_state ()) dummy) then None else Some (str "Error during initialization: ") in fatal_error ?extra any end; - if !batch_mode then begin + if !Flags.batch_mode then begin flush_all(); if !output_context then - Feedback.msg_notice (with_option raw_print Prettyp.print_full_pure_context () ++ fnl ()); + Feedback.msg_notice Flags.(with_option raw_print Prettyp.print_full_pure_context () ++ fnl ()); Profile.print_profile (); exit 0 end; diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 1602f9c68..c33f6b9b8 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -11,7 +11,6 @@ open Pp open CErrors open Util -open Flags open Vernacexpr open Vernacprop @@ -53,7 +52,7 @@ let set_formatter_translator ch = let pr_new_syntax_in_context ?loc chan_beautify ocom = let loc = Option.cata Loc.unloc (0,0) loc in - if !beautify_file then set_formatter_translator chan_beautify; + if !Flags.beautify_file then set_formatter_translator chan_beautify; let fs = States.freeze ~marshallable:`No in (* The content of this is not supposed to fail, but if ever *) try @@ -63,7 +62,7 @@ let pr_new_syntax_in_context ?loc chan_beautify ocom = | Some com -> Ppvernac.pr_vernac com | None -> mt() in let after = comment (CLexer.extract_comments (snd loc)) in - if !beautify_file then + if !Flags.beautify_file then (Pp.pp_with !Topfmt.std_ft (hov 0 (before ++ com ++ after)); Format.pp_print_flush !Topfmt.std_ft ()) else @@ -209,7 +208,7 @@ and load_vernac verbosely sid file = *) in (* Printing of vernacs *) - if !beautify then pr_new_syntax ?loc in_pa chan_beautify (Some ast); + if !Flags.beautify then pr_new_syntax ?loc in_pa chan_beautify (Some ast); Option.iter (vernac_echo ?loc) in_echo; checknav_simple (loc, ast); @@ -224,7 +223,7 @@ and load_vernac verbosely sid file = match e with | Stm.End_of_input -> (* Is this called so comments at EOF are printed? *) - if !beautify then + if !Flags.beautify then pr_new_syntax ~loc:(Loc.make_loc (max_int,max_int)) in_pa chan_beautify None; if !Flags.beautify_file then close_out chan_beautify; !rsid @@ -290,7 +289,7 @@ let compile verbosely f = ++ str ".") in match !Flags.compilation_mode with - | BuildVo -> + | Flags.BuildVo -> let long_f_dot_v = ensure_v f in ensure_exists long_f_dot_v; let long_f_dot_vo = @@ -314,7 +313,7 @@ let compile verbosely f = (Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1)); Aux_file.stop_aux_file (); Dumpglob.end_dump_glob () - | BuildVio -> + | Flags.BuildVio -> let long_f_dot_v = ensure_v f in ensure_exists long_f_dot_v; let long_f_dot_vio = @@ -329,7 +328,7 @@ let compile verbosely f = check_pending_proofs (); Stm.snapshot_vio ldir long_f_dot_vio; Stm.reset_task_queue () - | Vio2Vo -> + | Flags.Vio2Vo -> let open Filename in let open Library in Dumpglob.noglob (); diff --git a/vernac/command.ml b/vernac/command.ml index 32ab5401a..b611edc41 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -9,7 +9,6 @@ open Pp open CErrors open Util -open Flags open Term open Vars open Termops @@ -692,7 +691,7 @@ let declare_mutual_inductive_with_eliminations mie pl impls = constrimpls) impls; let warn_prim = match mie.mind_entry_record with Some (Some _) -> not prim | _ -> false in - if_verbose Feedback.msg_info (minductive_message warn_prim names); + Flags.if_verbose Feedback.msg_info (minductive_message warn_prim names); if mie.mind_entry_private == None then declare_default_schemes mind; mind diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 645320c60..590fa6213 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -11,7 +11,6 @@ open CErrors open Util -open Flags open Pp open Names open Term @@ -137,7 +136,7 @@ let find_mutually_recursive_statements thms = assert (List.is_empty rest); (* One occ. of common coind ccls and no common inductive hyps *) if not (List.is_empty common_same_indhyp) then - if_verbose Feedback.msg_info (str "Assuming mutual coinductive statements."); + Flags.if_verbose Feedback.msg_info (str "Assuming mutual coinductive statements."); flush_all (); indccl, true, [] | [], _::_ -> @@ -145,7 +144,7 @@ let find_mutually_recursive_statements thms = | ind :: _ -> if List.distinct_f ind_ord (List.map pi1 ind) then - if_verbose Feedback.msg_info + Flags.if_verbose Feedback.msg_info (strbrk ("Coinductive statements do not follow the order of "^ "definition, assuming the proof to be by induction.")); diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index c424b1d50..7b0d59812 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -7,7 +7,6 @@ (************************************************************************) open Pp -open Flags open CErrors open Util open Names @@ -794,7 +793,7 @@ type notation_modifier = { (* common to syn_data below *) only_parsing : bool; only_printing : bool; - compat : compat_version option; + compat : Flags.compat_version option; format : string Loc.located option; extra : (string * string) list; } @@ -1073,7 +1072,7 @@ module SynData = struct (* Fields coming from the vernac-level modifiers *) only_parsing : bool; only_printing : bool; - compat : compat_version option; + compat : Flags.compat_version option; format : string Loc.located option; extra : (string * string) list; @@ -1389,7 +1388,7 @@ let add_notation_interpretation ((loc,df),c,sc) = let set_notation_for_interpretation impls ((_,df),c,sc) = (try ignore - (silently (fun () -> add_notation_interpretation_core false df ~impls c sc false false None) ()); + (Flags.silently (fun () -> add_notation_interpretation_core false df ~impls c sc false false None) ()); with NoSyntaxRule -> user_err Pp.(str "Parsing rule for this notation has to be previously declared.")); Option.iter (fun sc -> Notation.open_close_scope (false,true,sc)) sc diff --git a/vernac/mltop.ml b/vernac/mltop.ml index e8a0ba3dd..1edbd1a85 100644 --- a/vernac/mltop.ml +++ b/vernac/mltop.ml @@ -9,7 +9,6 @@ open CErrors open Util open Pp -open Flags open Libobject open System @@ -365,7 +364,7 @@ let trigger_ml_object verb cache reinit ?path name = else begin let file = file_of_name (Option.default name path) in let path = - if_verbose_load (verb && not !quiet) load_ml_object name ?path file in + if_verbose_load (verb && not !Flags.quiet) load_ml_object name ?path file in add_loaded_module name (Some path); if cache then perform_cache_obj name end diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 4fd08b42d..b0e438a8e 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -11,7 +11,6 @@ open Pp open CErrors open Util -open Flags open Names open Nameops open Term @@ -657,7 +656,7 @@ let vernac_declare_module export (loc, id) binders_ast mty_ast = id binders_ast (Enforce mty_ast) [] in Dumpglob.dump_moddef ?loc mp "mod"; - if_verbose Feedback.msg_info (str "Module " ++ pr_id id ++ str " is declared"); + Flags.if_verbose Feedback.msg_info (str "Module " ++ pr_id id ++ str " is declared"); Option.iter (fun export -> vernac_import export [Ident (Loc.tag id)]) export let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l = @@ -678,7 +677,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l = export id binders_ast mty_ast_o in Dumpglob.dump_moddef ?loc mp "mod"; - if_verbose Feedback.msg_info + Flags.if_verbose Feedback.msg_info (str "Interactive Module " ++ pr_id id ++ str " started"); List.iter (fun (export,id) -> @@ -696,7 +695,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l = id binders_ast mty_ast_o mexpr_ast_l in Dumpglob.dump_moddef ?loc mp "mod"; - if_verbose Feedback.msg_info + Flags.if_verbose Feedback.msg_info (str "Module " ++ pr_id id ++ str " is defined"); Option.iter (fun export -> vernac_import export [Ident (Loc.tag id)]) export @@ -704,7 +703,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l = let vernac_end_module export (loc,id as lid) = let mp = Declaremods.end_module () in Dumpglob.dump_modref ?loc mp "mod"; - if_verbose Feedback.msg_info (str "Module " ++ pr_id id ++ str " is defined"); + Flags.if_verbose Feedback.msg_info (str "Module " ++ pr_id id ++ str " is defined"); Option.iter (fun export -> vernac_import export [Ident lid]) export let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l = @@ -725,7 +724,7 @@ let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l = id binders_ast mty_sign in Dumpglob.dump_moddef ?loc mp "modtype"; - if_verbose Feedback.msg_info + Flags.if_verbose Feedback.msg_info (str "Interactive Module Type " ++ pr_id id ++ str " started"); List.iter (fun (export,id) -> @@ -744,13 +743,13 @@ let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l = id binders_ast mty_sign mty_ast_l in Dumpglob.dump_moddef ?loc mp "modtype"; - if_verbose Feedback.msg_info + Flags.if_verbose Feedback.msg_info (str "Module Type " ++ pr_id id ++ str " is defined") let vernac_end_modtype (loc,id) = let mp = Declaremods.end_modtype () in Dumpglob.dump_modref ?loc mp "modtype"; - if_verbose Feedback.msg_info (str "Module Type " ++ pr_id id ++ str " is defined") + Flags.if_verbose Feedback.msg_info (str "Module Type " ++ pr_id id ++ str " is defined") let vernac_include l = Declaremods.declare_include Modintern.interp_module_ast l @@ -818,7 +817,7 @@ let vernac_coercion locality poly local ref qids qidt = let source = cl_of_qualid qids in let ref' = smart_global ref in Class.try_add_new_coercion_with_target ref' ~local poly ~source ~target; - if_verbose Feedback.msg_info (pr_global ref' ++ str " is now a coercion") + Flags.if_verbose Feedback.msg_info (pr_global ref' ++ str " is now a coercion") let vernac_identity_coercion locality poly local id qids qidt = let local = enforce_locality locality local in @@ -920,7 +919,7 @@ let vernac_chdir = function so we make it an error. *) user_err Pp.(str ("Cd failed: " ^ err)) end; - if_verbose Feedback.msg_info (str (Sys.getcwd())) + Flags.if_verbose Feedback.msg_info (str (Sys.getcwd())) (********************) @@ -1302,7 +1301,7 @@ let _ = optname = "automatic introduction of variables"; optkey = ["Automatic";"Introduction"]; optread = Flags.is_auto_intros; - optwrite = make_auto_intros } + optwrite = Flags.make_auto_intros } let _ = declare_bool_option @@ -2050,7 +2049,7 @@ let interp ?proof ?loc locality poly c = | VernacSearch (s,g,r) -> vernac_search ?loc s g r | VernacLocate l -> vernac_locate l | VernacRegister (id, r) -> vernac_register id r - | VernacComments l -> if_verbose Feedback.msg_info (str "Comments ok\n") + | VernacComments l -> Flags.if_verbose Feedback.msg_info (str "Comments ok\n") (* Proof management *) | VernacGoal t -> vernac_start_proof locality poly Theorem [None,([],t)] @@ -2176,7 +2175,7 @@ let with_fail b f = | HasNotFailed -> user_err ~hdr:"Fail" (str "The command has not failed!") | HasFailed msg -> - if not !Flags.quiet || !test_mode || !ide_slave then Feedback.msg_info + if not !Flags.quiet || !Flags.test_mode || !Flags.ide_slave then Feedback.msg_info (str "The command has indeed failed with message:" ++ fnl () ++ msg) | _ -> assert false end -- cgit v1.2.3