diff options
Diffstat (limited to 'vernac/vernacentries.ml')
| -rw-r--r-- | vernac/vernacentries.ml | 123 |
1 files changed, 76 insertions, 47 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index bab5c5ae9..4c9b41b21 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1,15 +1,18 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * 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) *) (************************************************************************) (* Concrete syntax of the mathematical vernacular MV V2.6 *) open Pp open CErrors +open CAst open Util open Names open Nameops @@ -69,7 +72,7 @@ let show_top_evars () = let show_universes () = let pfts = Proof_global.give_me_the_proof () in let gls,_,_,_,sigma = Proof.proof pfts in - let ctx = Evd.universe_context_set (Evd.nf_constraints sigma) in + let ctx = Evd.universe_context_set (Evd.minimize_universes sigma) in Termops.pr_evar_universe_context (Evd.evar_universe_context sigma) ++ fnl () ++ str "Normalized constraints: " ++ Univ.pr_universe_context_set (Termops.pr_evd_level sigma) ctx @@ -471,13 +474,13 @@ let vernac_definition_hook p = function | SubClass -> Class.add_subclass_hook p | _ -> no_hook -let vernac_definition ~atts discharge kind ((loc, id), pl) def = +let vernac_definition ~atts discharge kind ({loc;v=id}, pl) def = let local = enforce_locality_exp atts.locality discharge in let hook = vernac_definition_hook atts.polymorphic kind in let () = match id with | Anonymous -> () - | Name n -> let lid = (loc, n) in + | Name n -> let lid = CAst.make ?loc n in match local with | Discharge -> Dumpglob.dump_definition lid true "var" | Local | Global -> Dumpglob.dump_definition lid false "def" @@ -491,7 +494,7 @@ let vernac_definition ~atts discharge kind ((loc, id), pl) def = (match def with | ProveBody (bl,t) -> (* local binders, typ *) start_proof_and_print (local, atts.polymorphic, DefinitionBody kind) - [((loc, name), pl), (bl, t)] hook + [(CAst.make ?loc name, pl), (bl, t)] hook | DefineBody (bl,red_option,c,typ_opt) -> let red_option = match red_option with | None -> None @@ -546,14 +549,14 @@ let should_treat_as_cumulative cum poly = let vernac_record cum k poly finite struc binders sort nameopt cfs = let is_cumulative = should_treat_as_cumulative cum poly in let const = match nameopt with - | None -> add_prefix "Build_" (snd (fst (snd struc))) - | Some (_,id as lid) -> + | None -> add_prefix "Build_" (fst (snd struc)).v + | Some ({v=id} as lid) -> Dumpglob.dump_definition lid false "constr"; id in if Dumpglob.dump () then ( Dumpglob.dump_definition (fst (snd struc)) false "rec"; List.iter (fun (((_, x), _), _) -> match x with - | Vernacexpr.AssumExpr ((loc, Name id), _) -> Dumpglob.dump_definition (loc,id) false "proj" + | Vernacexpr.AssumExpr ({loc;v=Name id}, _) -> Dumpglob.dump_definition (make ?loc id) false "proj" | _ -> ()) cfs); ignore(Record.definition_structure (k,is_cumulative,poly,finite,struc,binders,cfs,const,sort)) @@ -582,9 +585,9 @@ let vernac_inductive ~atts cum lo finite indl = atts.polymorphic finite id bl c oc fs | [ ( id , bl , c , Class _, Constructors [l]), [] ] -> let f = - let (coe, ((loc, id), ce)) = l in + let (coe, ({loc;v=id}, ce)) = l in let coe' = if coe then Some true else None in - (((coe', AssumExpr ((loc, Name id), ce)), None), []) + (((coe', AssumExpr ((make ?loc @@ Name id), ce)), None), []) in vernac_record cum (Class true) atts.polymorphic finite id bl c None [f] | [ ( _ , _, _, Class _, Constructors _), [] ] -> user_err Pp.(str "Inductive classes not supported") @@ -637,7 +640,7 @@ let vernac_scheme l = let vernac_combined_scheme lid l = if Dumpglob.dump () then (Dumpglob.dump_definition lid false "def"; - List.iter (fun lid -> dump_global (Misctypes.AN (Ident lid))) l); + List.iter (fun {loc;v=id} -> dump_global (Misctypes.AN (Ident (Loc.tag ?loc id)))) l); Indschemes.do_combined_scheme lid l let vernac_universe ~atts l = @@ -660,7 +663,7 @@ let vernac_constraint ~atts l = let vernac_import export refl = Library.import_module export (List.map qualid_of_reference refl) -let vernac_declare_module export (loc, id) binders_ast mty_ast = +let vernac_declare_module export {loc;v=id} binders_ast mty_ast = (* We check the state of the system (in section, in module type) and what module information is supplied *) if Lib.sections_are_opened () then @@ -678,7 +681,7 @@ let vernac_declare_module export (loc, id) binders_ast mty_ast = Flags.if_verbose Feedback.msg_info (str "Module " ++ Id.print 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 = +let vernac_define_module export {loc;v=id} (binders_ast : module_binder list) mty_ast_o mexpr_ast_l = (* We check the state of the system (in section, in module type) and what module information is supplied *) if Lib.sections_are_opened () then @@ -689,7 +692,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l = let binders_ast,argsexport = List.fold_right (fun (export,idl,ty) (args,argsexport) -> - (idl,ty)::args, (List.map (fun (_,i) -> export,i)idl)@argsexport) binders_ast + (idl,ty)::args, (List.map (fun {v=i} -> export,i)idl)@argsexport) binders_ast ([],[]) in let mp = Declaremods.start_module Modintern.interp_module_ast @@ -719,13 +722,13 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l = Option.iter (fun export -> vernac_import export [Ident (Loc.tag id)]) export -let vernac_end_module export (loc,id as lid) = +let vernac_end_module export {loc;v=id} = let mp = Declaremods.end_module () in Dumpglob.dump_modref ?loc mp "mod"; Flags.if_verbose Feedback.msg_info (str "Module " ++ Id.print id ++ str " is defined"); - Option.iter (fun export -> vernac_import export [Ident lid]) export + Option.iter (fun export -> vernac_import export [Ident (Loc.tag ?loc id)]) export -let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l = +let vernac_declare_module_type {loc;v=id} binders_ast mty_sign mty_ast_l = if Lib.sections_are_opened () then user_err Pp.(str "Modules and Module Types are not allowed inside sections."); @@ -735,7 +738,7 @@ let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l = let binders_ast,argsexport = List.fold_right (fun (export,idl,ty) (args,argsexport) -> - (idl,ty)::args, (List.map (fun (_,i) -> export,i)idl)@argsexport) binders_ast + (idl,ty)::args, (List.map (fun {v=i} -> export,i)idl)@argsexport) binders_ast ([],[]) in let mp = @@ -765,7 +768,7 @@ let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l = Flags.if_verbose Feedback.msg_info (str "Module Type " ++ Id.print id ++ str " is defined") -let vernac_end_modtype (loc,id) = +let vernac_end_modtype {loc;v=id} = let mp = Declaremods.end_modtype () in Dumpglob.dump_modref ?loc mp "modtype"; Flags.if_verbose Feedback.msg_info (str "Module Type " ++ Id.print id ++ str " is defined") @@ -778,21 +781,21 @@ let vernac_include l = (* Sections *) -let vernac_begin_section (_, id as lid) = +let vernac_begin_section ({v=id} as lid) = Proof_global.check_no_pending_proof (); Dumpglob.dump_definition lid true "sec"; Lib.open_section id -let vernac_end_section (loc,_) = +let vernac_end_section {CAst.loc} = Dumpglob.dump_reference ?loc (DirPath.to_string (Lib.current_dirpath true)) "<>" "sec"; Lib.close_section () -let vernac_name_sec_hyp (_,id) set = Proof_using.name_set id set +let vernac_name_sec_hyp {v=id} set = Proof_using.name_set id set (* Dispatcher of the "End" command *) -let vernac_end_segment (_,id as lid) = +let vernac_end_segment ({v=id} as lid) = Proof_global.check_no_pending_proof (); match Lib.find_opening_node id with | Lib.OpenedModule (false,export,_,_) -> vernac_end_module export lid @@ -802,7 +805,14 @@ let vernac_end_segment (_,id as lid) = (* Libraries *) +let warn_require_in_section = + let name = "require-in-section" in + let category = "deprecated" in + CWarnings.create ~name ~category + (fun () -> strbrk "Use of “Require” inside a section is deprecated.") + let vernac_require from import qidl = + if Lib.sections_are_opened () then warn_require_in_section (); let qidl = List.map qualid_of_reference qidl in let root = match from with | None -> None @@ -975,7 +985,7 @@ let vernac_hints ~atts lb h = let vernac_syntactic_definition ~atts lid x y = Dumpglob.dump_definition lid false "syndef"; let local = enforce_module_locality atts.locality in - Metasyntax.add_syntactic_definition (Global.env()) (snd lid) x local y + Metasyntax.add_syntactic_definition (Global.env()) lid.v x local y let vernac_declare_implicits ~atts r l = let local = make_section_locality atts.locality in @@ -1024,7 +1034,9 @@ let vernac_arguments ~atts reference args more_implicits nargs_for_red flags = let sr = smart_global reference in let inf_names = let ty, _ = Global.type_of_global_in_context (Global.env ()) sr in - Impargs.compute_implicits_names (Global.env ()) ty + let env = Global.env () in + let sigma = Evd.from_env env in + Impargs.compute_implicits_names env sigma (EConstr.of_constr ty) in let prev_names = try Arguments_renaming.arguments_names sr with Not_found -> inf_names @@ -1211,7 +1223,7 @@ let vernac_arguments ~atts reference args more_implicits nargs_for_red flags = end; if scopes_specified || clear_scopes_flag then begin - let scopes = List.map (Option.map (fun (loc,k) -> + let scopes = List.map (Option.map (fun {loc;v=k} -> try ignore (Notation.find_scope k); k with UserError _ -> Notation.find_delimiters_scope ?loc k)) scopes @@ -1252,7 +1264,7 @@ let vernac_reserve bl = let env = Global.env() in let sigma = Evd.from_env env in let t,ctx = Constrintern.interp_type env sigma c in - let t = Detyping.detype Detyping.Now false Id.Set.empty env (Evd.from_ctx ctx) (EConstr.of_constr t) in + let t = Detyping.detype Detyping.Now false Id.Set.empty env (Evd.from_ctx ctx) t in let t,_ = Notation_ops.notation_constr_of_glob_constr (default_env ()) t in Reserve.declare_reserved_type idl t) in List.iter sb_decl bl @@ -1468,6 +1480,14 @@ let _ = let _ = declare_bool_option { optdepr = false; + optname = "dumping VM lambda code after compilation"; + optkey = ["Dump";"Lambda"]; + optread = Flags.get_dump_lambda; + optwrite = Flags.set_dump_lambda } + +let _ = + declare_bool_option + { optdepr = false; optname = "explicitly parsing implicit arguments"; optkey = ["Parsing";"Explicit"]; optread = (fun () -> !Constrintern.parsing_explicit); @@ -1618,6 +1638,7 @@ let vernac_global_check c = let senv = Global.safe_env() in let uctx = UState.context_set uctx in let senv = Safe_typing.push_context_set false uctx senv in + let c = EConstr.to_constr sigma c in let j = Safe_typing.typing senv c in let env = Safe_typing.env_of_safe_env senv in print_safe_judgment env sigma j ++ @@ -1738,10 +1759,10 @@ let interp_search_restriction = function open Search -let interp_search_about_item env = +let interp_search_about_item env sigma = function | SearchSubPattern pat -> - let _,pat = intern_constr_pattern env pat in + let _,pat = intern_constr_pattern env sigma pat in GlobSearchSubPattern pat | SearchString (s,None) when Id.is_valid s -> GlobSearchString s @@ -1787,13 +1808,13 @@ let vernac_search ~atts s gopt r = (* if goal selector is given and wrong, then let exceptions be raised. *) | Some g -> snd (Pfedit.get_goal_context g) , Some g in - let get_pattern c = snd (intern_constr_pattern env c) in + let get_pattern c = snd (intern_constr_pattern env Evd.(from_env env) c) in let pr_search ref env c = let pr = pr_global ref in let pp = if !search_output_name_only then pr else begin - let pc = pr_lconstr_env env Evd.empty c in + let pc = pr_lconstr_env env Evd.(from_env env) c in hov 2 (pr ++ str":" ++ spc () ++ pc) end in Feedback.msg_notice pp @@ -1806,7 +1827,8 @@ let vernac_search ~atts s gopt r = | SearchHead c -> (Search.search_by_head gopt (get_pattern c) r |> Search.prioritize_search) pr_search | SearchAbout sl -> - (Search.search_about gopt (List.map (on_snd (interp_search_about_item env)) sl) r |> Search.prioritize_search) pr_search + (Search.search_about gopt (List.map (on_snd (interp_search_about_item env Evd.(from_env env))) sl) r |> + Search.prioritize_search) pr_search let vernac_locate = function | LocateAny (AN qid) -> print_located_qualid qid @@ -1824,7 +1846,7 @@ let vernac_locate = function let vernac_register id r = if Proof_global.there_are_pending_proofs () then user_err Pp.(str "Cannot register a primitive while in proof editing mode."); - let kn = Constrintern.global_reference (snd id) in + let kn = Constrintern.global_reference id.v in if not (isConstRef kn) then user_err Pp.(str "Register inline: a constant is expected"); match r with @@ -1901,8 +1923,7 @@ let vernac_check_guard () = let message = try let { Evd.it=gl ; sigma=sigma } = Proof.V82.top_goal pts in - Inductiveops.control_only_guard (Goal.V82.env sigma gl) - (EConstr.Unsafe.to_constr pfterm); + Inductiveops.control_only_guard (Goal.V82.env sigma gl) sigma pfterm; (str "The condition holds up to here") with UserError(_,s) -> (str ("Condition violated: ") ++s) @@ -1917,6 +1938,8 @@ exception End_of_input without a considerable amount of refactoring. *) let vernac_load interp fname = + if Proof_global.there_are_pending_proofs () then + CErrors.user_err Pp.(str "Load is not supported inside proofs."); let interp x = let proof_mode = Proof_global.get_default_proof_mode_name () [@ocaml.warning "-3"] in Proof_global.activate_proof_mode proof_mode [@ocaml.warning "-3"]; @@ -1933,8 +1956,13 @@ let vernac_load interp fname = let longfname = Loadpath.locate_file fname in let in_chan = open_utf8_file_in longfname in Pcoq.Gram.parsable ~file:(Loc.InFile longfname) (Stream.of_channel in_chan) in - try while true do interp (snd (parse_sentence input)) done - with End_of_input -> () + begin + try while true do interp (snd (parse_sentence input)) done + with End_of_input -> () + end; + (* If Load left a proof open, we fail too. *) + if Proof_global.there_are_pending_proofs () then + CErrors.user_err Pp.(str "Files processed by Load cannot leave open proofs.") (* "locality" is the prefix "Local" attribute, while the "local" component * is the outdated/deprecated "Local" attribute of some vernacular commands @@ -1945,6 +1973,7 @@ let interp ?proof ~atts ~st c = vernac_pperr_endline (fun () -> str "interpreting: " ++ Ppvernac.pr_vernac_expr c); match c with + (* Loading a file requires access to the control interpreter *) | VernacLoad _ -> assert false (* The STM should handle that, but LOAD bypasses the STM... *) @@ -2015,7 +2044,7 @@ let interp ?proof ~atts ~st c = | VernacImport (export,qidl) -> vernac_import export qidl | VernacCanonical qid -> vernac_canonical qid | VernacCoercion (r,s,t) -> vernac_coercion ~atts r s t - | VernacIdentityCoercion ((_,id),s,t) -> + | VernacIdentityCoercion ({v=id},s,t) -> vernac_identity_coercion ~atts id s t (* Type classes *) @@ -2233,12 +2262,12 @@ let interp ?(verbosely=true) ?proof ~st (loc,c) = aux ~polymorphism ~atts v | VernacFail v -> with_fail st true (fun () -> control v) | VernacTimeout (n,v) -> - current_timeout := Some n; - control v - | VernacRedirect (s, (_,v)) -> - Topfmt.with_output_to_file s control v - | VernacTime (batch, (_loc,v)) -> - System.with_time ~batch control v; + current_timeout := Some n; + control v + | VernacRedirect (s, {v}) -> + Topfmt.with_output_to_file s control v + | VernacTime (batch, {v}) -> + System.with_time ~batch control v; and aux ~polymorphism ~atts : _ -> unit = function |