diff options
30 files changed, 160 insertions, 107 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index 4789d9b6fa..6c6e4bdfcb 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -320,6 +320,8 @@ azure-pipelines.yml @coq/ci-maintainers /test-suite/unit-tests/src/ @jfehrle # Secondary maintainer @SkySkimmer +/test-suite/success/Compat*.v @JasonGross + ########## Developer tools ########## /dev/tools/backport-pr.sh @Zimmi48 diff --git a/dev/README.md b/dev/README.md index 4cda60a703..0c6b8020f1 100644 --- a/dev/README.md +++ b/dev/README.md @@ -28,7 +28,7 @@ | [`dev/doc/econstr.md`](doc/econstr.md) | Describes `Econstr`, implementation of treatment of `evar` in the engine | | [`dev/doc/primproj.md`](doc/primproj.md) | Describes primitive projections | | [`dev/doc/proof-engine.md`](doc/proof-engine.md) | Tutorial on new proof engine | -| [`dev/doc/xml-protocol.md`](doc/proof-engine.md) | XML protocol that coqtop and IDEs use to communicate | +| [`dev/doc/xml-protocol.md`](doc/xml-protocol.md) | XML protocol that coqtop and IDEs use to communicate | | [`dev/doc/MERGING.md`](doc/MERGING.md) | How pull requests should be merged into `master` | | [`dev/doc/release-process.md`](doc/release-process.md) | Process of creating a new Coq release | diff --git a/doc/changelog/10-standard-library/10895-master+weak-excluded-middle-de-morgan.rst b/doc/changelog/10-standard-library/10895-master+weak-excluded-middle-de-morgan.rst new file mode 100644 index 0000000000..6e87ff93c7 --- /dev/null +++ b/doc/changelog/10-standard-library/10895-master+weak-excluded-middle-de-morgan.rst @@ -0,0 +1 @@ +- ClassicalFacts: Adding the standard equivalence between weak excluded-middle and the classical instance of De Morgan's law (`#10895 <https://github.com/coq/coq/pull/10895>`_, by Hugo Herbelin). diff --git a/engine/uState.ml b/engine/uState.ml index af714f6282..efced52990 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -520,7 +520,7 @@ let merge ?loc ~sideff rigid uctx ctx' = let merge_subst uctx s = { uctx with uctx_univ_variables = LMap.subst_union uctx.uctx_univ_variables s } -let demote_seff_univs (univs,_) uctx = +let demote_seff_univs univs uctx = let seff = LSet.union uctx.uctx_seff_univs univs in { uctx with uctx_seff_univs = seff } @@ -541,7 +541,7 @@ let merge_seff uctx ctx' = let emit_side_effects eff u = let uctxs = Safe_typing.universes_of_private eff in List.fold_left (fun u uctx -> - let u = demote_seff_univs uctx u in + let u = demote_seff_univs (fst uctx) u in merge_seff u uctx) u uctxs diff --git a/engine/uState.mli b/engine/uState.mli index 7cb2f49780..23ef84c55d 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -112,6 +112,11 @@ val merge : ?loc:Loc.t -> sideff:bool -> rigid -> t -> Univ.ContextSet.t -> t val merge_subst : t -> UnivSubst.universe_opt_subst -> t val emit_side_effects : Safe_typing.private_constants -> t -> t +val demote_seff_univs : Univ.LSet.t -> t -> t +(** Mark the universes as not local any more, because they have been + globally declared by some side effect. You should be using + emit_side_effects instead. *) + val new_univ_variable : ?loc:Loc.t -> rigid -> Id.t option -> t -> t * Univ.Level.t val add_global_univ : t -> Univ.Level.t -> t diff --git a/kernel/environ.ml b/kernel/environ.ml index 4a2aeea22d..98d66cafa1 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -50,12 +50,19 @@ type constant_key = Opaqueproof.opaque constant_body * (link_info ref * key) type mind_key = mutual_inductive_body * link_info ref -type globals = { - env_constants : constant_key Cmap_env.t; - env_inductives : mind_key Mindmap_env.t; - env_modules : module_body MPmap.t; - env_modtypes : module_type_body MPmap.t; -} +module Globals = struct + + type view = + { constants : constant_key Cmap_env.t + ; inductives : mind_key Mindmap_env.t + ; modules : module_body MPmap.t + ; modtypes : module_type_body MPmap.t + } + + type t = view + + let view x = x +end type stratification = { env_universes : UGraph.t; @@ -88,7 +95,7 @@ type rel_context_val = { } type env = { - env_globals : globals; + env_globals : Globals.t; env_named_context : named_context_val; (* section variables *) env_rel_context : rel_context_val; env_nb_rel : int; @@ -110,11 +117,12 @@ let empty_rel_context_val = { } let empty_env = { - env_globals = { - env_constants = Cmap_env.empty; - env_inductives = Mindmap_env.empty; - env_modules = MPmap.empty; - env_modtypes = MPmap.empty}; + env_globals = + { Globals.constants = Cmap_env.empty + ; inductives = Mindmap_env.empty + ; modules = MPmap.empty + ; modtypes = MPmap.empty + }; env_named_context = empty_named_context_val; env_rel_context = empty_rel_context_val; env_nb_rel = 0; @@ -215,29 +223,29 @@ let lookup_named_ctxt id ctxt = fst (Id.Map.find id ctxt.env_named_map) let fold_constants f env acc = - Cmap_env.fold (fun c (body,_) acc -> f c body acc) env.env_globals.env_constants acc + Cmap_env.fold (fun c (body,_) acc -> f c body acc) env.env_globals.Globals.constants acc let fold_inductives f env acc = - Mindmap_env.fold (fun c (body,_) acc -> f c body acc) env.env_globals.env_inductives acc + Mindmap_env.fold (fun c (body,_) acc -> f c body acc) env.env_globals.Globals.inductives acc (* Global constants *) let lookup_constant_key kn env = - Cmap_env.find kn env.env_globals.env_constants + Cmap_env.find kn env.env_globals.Globals.constants let lookup_constant kn env = - fst (Cmap_env.find kn env.env_globals.env_constants) + fst (Cmap_env.find kn env.env_globals.Globals.constants) (* Mutual Inductives *) let lookup_mind kn env = - fst (Mindmap_env.find kn env.env_globals.env_inductives) + fst (Mindmap_env.find kn env.env_globals.Globals.inductives) let mind_context env mind = let mib = lookup_mind mind env in Declareops.inductive_polymorphic_context mib let lookup_mind_key kn env = - Mindmap_env.find kn env.env_globals.env_inductives + Mindmap_env.find kn env.env_globals.Globals.inductives let oracle env = env.env_typing_flags.conv_oracle let set_oracle env o = @@ -468,10 +476,10 @@ let no_link_info = NotLinked let add_constant_key kn cb linkinfo env = let new_constants = - Cmap_env.add kn (cb,(ref linkinfo, ref None)) env.env_globals.env_constants in + Cmap_env.add kn (cb,(ref linkinfo, ref None)) env.env_globals.Globals.constants in let new_globals = { env.env_globals with - env_constants = new_constants } in + Globals.constants = new_constants } in { env with env_globals = new_globals } let add_constant kn cb env = @@ -598,10 +606,10 @@ let template_polymorphic_pind (ind,u) env = else template_polymorphic_ind ind env let add_mind_key kn (_mind, _ as mind_key) env = - let new_inds = Mindmap_env.add kn mind_key env.env_globals.env_inductives in + let new_inds = Mindmap_env.add kn mind_key env.env_globals.Globals.inductives in let new_globals = { env.env_globals with - env_inductives = new_inds; } in + Globals.inductives = new_inds; } in { env with env_globals = new_globals } let add_mind kn mib env = @@ -688,22 +696,22 @@ let keep_hyps env needed = let add_modtype mtb env = let mp = mtb.mod_mp in - let new_modtypes = MPmap.add mp mtb env.env_globals.env_modtypes in - let new_globals = { env.env_globals with env_modtypes = new_modtypes } in + let new_modtypes = MPmap.add mp mtb env.env_globals.Globals.modtypes in + let new_globals = { env.env_globals with Globals.modtypes = new_modtypes } in { env with env_globals = new_globals } let shallow_add_module mb env = let mp = mb.mod_mp in - let new_mods = MPmap.add mp mb env.env_globals.env_modules in - let new_globals = { env.env_globals with env_modules = new_mods } in + let new_mods = MPmap.add mp mb env.env_globals.Globals.modules in + let new_globals = { env.env_globals with Globals.modules = new_mods } in { env with env_globals = new_globals } let lookup_module mp env = - MPmap.find mp env.env_globals.env_modules + MPmap.find mp env.env_globals.Globals.modules -let lookup_modtype mp env = - MPmap.find mp env.env_globals.env_modtypes +let lookup_modtype mp env = + MPmap.find mp env.env_globals.Globals.modtypes (*s Judgments. *) diff --git a/kernel/environ.mli b/kernel/environ.mli index f7de98dcfb..5af2a7288b 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -46,8 +46,18 @@ type constant_key = Opaqueproof.opaque constant_body * (link_info ref * key) type mind_key = mutual_inductive_body * link_info ref -type globals -(** globals = constants + projections + inductive types + modules + module-types *) +module Globals : sig + type t + + type view = + { constants : constant_key Cmap_env.t + ; inductives : mind_key Mindmap_env.t + ; modules : module_body MPmap.t + ; modtypes : module_type_body MPmap.t + } + + val view : t -> view +end type stratification = { env_universes : UGraph.t; @@ -67,7 +77,7 @@ type rel_context_val = private { } type env = private { - env_globals : globals; + env_globals : Globals.t; env_named_context : named_context_val; (* section variables *) env_rel_context : rel_context_val; env_nb_rel : int; diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 9b4d2e69ac..fc55720583 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -173,6 +173,8 @@ let is_initial senv = | [], NONE -> ModPath.equal senv.modpath ModPath.initial | _ -> false +let sections_are_opened senv = not (Section.is_empty senv.sections) + let delta_of_senv senv = senv.modresolver,senv.paramresolver let constant_of_delta_kn_senv senv kn = @@ -587,10 +589,10 @@ type global_declaration = type exported_private_constant = Constant.t -let add_constant_aux ~in_section senv (kn, cb) = +let add_constant_aux senv (kn, cb) = let l = Constant.label kn in (* This is the only place where we hashcons the contents of a constant body *) - let cb = if in_section then cb else Declareops.hcons_const_body cb in + let cb = if sections_are_opened senv then cb else Declareops.hcons_const_body cb in let senv' = add_field (l,SFBconst cb) (C kn) senv in let senv'' = match cb.const_body with | Undef (Some lev) -> @@ -799,7 +801,7 @@ let push_opaque_proof pf senv = let senv = { senv with env = Environ.set_opaque_tables senv.env otab } in senv, o -let export_private_constants ~in_section ce senv = +let export_private_constants ce senv = let exported, ce = export_side_effects senv.revstruct senv.env ce in let map senv (kn, c) = match c.const_body with | OpaqueDef p -> @@ -815,10 +817,10 @@ let export_private_constants ~in_section ce senv = let senv, bodies = List.fold_left_map map senv exported in let exported = List.map (fun (kn, _) -> kn) exported in (* No delayed constants to declare *) - let senv = List.fold_left (add_constant_aux ~in_section) senv bodies in + let senv = List.fold_left add_constant_aux senv bodies in (ce, exported), senv -let add_constant (type a) ~(side_effect : a effect_entry) ~in_section l decl senv : (Constant.t * a) * safe_environment = +let add_constant (type a) ~(side_effect : a effect_entry) l decl senv : (Constant.t * a) * safe_environment = let kn = Constant.make2 senv.modpath l in let cb = match decl with @@ -852,14 +854,14 @@ let add_constant (type a) ~(side_effect : a effect_entry) ~in_section l decl sen | Undef _ | Def _ | Primitive _ as body -> senv, { cb with const_body = body }, [] in - let senv = add_constant_aux ~in_section senv (kn, cb) in + let senv = add_constant_aux senv (kn, cb) in add_constraints_list delayed_cst senv in let senv = match decl with | ConstantEntry (_,(Entries.PrimitiveEntry { Entries.prim_entry_content = CPrimitives.OT_type t; _ })) -> - if in_section then CErrors.anomaly (Pp.str "Primitive type not allowed in sections"); + if sections_are_opened senv then CErrors.anomaly (Pp.str "Primitive type not allowed in sections"); add_retroknowledge (Retroknowledge.Register_type(t,kn)) senv | _ -> senv in @@ -1001,12 +1003,11 @@ let close_section senv = in let fold senv = function | `Definition (kn, cb) -> - let in_section = not (Section.is_empty senv.sections) in let info = cooking_info (Section.segment_of_constant env0 kn sections0) in let r = { Cooking.from = cb; info } in let cb = Term_typing.translate_recipe senv.env kn r in (* Delayed constants are already in the global environment *) - add_constant_aux ~in_section senv (kn, cb) + add_constant_aux senv (kn, cb) | `Inductive (ind, mib) -> let info = cooking_info (Section.segment_of_inductive env0 ind sections0) in let mie = Cooking.cook_inductive info mib in diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index d97d61a72f..1b55293f1c 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -82,13 +82,13 @@ type global_declaration = type exported_private_constant = Constant.t -val export_private_constants : in_section:bool -> +val export_private_constants : private_constants Entries.proof_output -> (Constr.constr Univ.in_universe_context_set * exported_private_constant list) safe_transformer (** returns the main constant plus a certificate of its validity *) val add_constant : - side_effect:'a effect_entry -> in_section:bool -> Label.t -> global_declaration -> + side_effect:'a effect_entry -> Label.t -> global_declaration -> (Constant.t * 'a) safe_transformer (** Adding an inductive type *) @@ -138,6 +138,8 @@ val open_section : safe_transformer0 val close_section : safe_transformer0 +val sections_are_opened : safe_environment -> bool + (** Insertion of local declarations (Local or Variables) *) val push_named_assum : (Id.t * Constr.types) -> safe_transformer0 diff --git a/kernel/section.ml b/kernel/section.ml index babd9fe7a1..a1242f0faf 100644 --- a/kernel/section.ml +++ b/kernel/section.ml @@ -43,6 +43,8 @@ let empty = [] let is_empty = List.is_empty +let depth = List.length + let has_poly_univs = function | [] -> false | sec :: _ -> sec.has_poly_univs diff --git a/kernel/section.mli b/kernel/section.mli index 56b4d9ba8f..ec863b3b90 100644 --- a/kernel/section.mli +++ b/kernel/section.mli @@ -21,6 +21,9 @@ val empty : 'a t val is_empty : 'a t -> bool (** Checks whether there is no opened section *) +val depth : 'a t -> int +(** Number of nested sections (0 if no sections are open) *) + (** {6 Manipulating sections} *) type section_entry = diff --git a/library/global.ml b/library/global.ml index c4685370d1..24cfc57f28 100644 --- a/library/global.ml +++ b/library/global.ml @@ -102,8 +102,8 @@ let typing_flags () = Environ.typing_flags (env ()) let make_sprop_cumulative () = globalize0 Safe_typing.make_sprop_cumulative let set_allow_sprop b = globalize0 (Safe_typing.set_allow_sprop b) let sprop_allowed () = Environ.sprop_allowed (env()) -let export_private_constants ~in_section cd = globalize (Safe_typing.export_private_constants ~in_section cd) -let add_constant ~side_effect ~in_section id d = globalize (Safe_typing.add_constant ~side_effect ~in_section (i2l id) d) +let export_private_constants cd = globalize (Safe_typing.export_private_constants cd) +let add_constant ~side_effect id d = globalize (Safe_typing.add_constant ~side_effect (i2l id) d) let add_mind id mie = globalize (Safe_typing.add_mind (i2l id) mie) let add_modtype id me inl = globalize (Safe_typing.add_modtype (i2l id) me inl) let add_module id me inl = globalize (Safe_typing.add_module (i2l id) me inl) @@ -111,6 +111,7 @@ let add_include me ismod inl = globalize (Safe_typing.add_include me ismod inl) let open_section () = globalize0 Safe_typing.open_section let close_section fs = globalize0_with_summary fs Safe_typing.close_section +let sections_are_opened () = Safe_typing.sections_are_opened (safe_env()) let start_module id = globalize (Safe_typing.start_module (i2l id)) let start_modtype id = globalize (Safe_typing.start_modtype (i2l id)) diff --git a/library/global.mli b/library/global.mli index c45bf65d84..d689771f0a 100644 --- a/library/global.mli +++ b/library/global.mli @@ -46,12 +46,12 @@ val push_named_assum : (Id.t * Constr.types) -> unit val push_named_def : (Id.t * Entries.section_def_entry) -> unit val push_section_context : (Name.t array * Univ.UContext.t) -> unit -val export_private_constants : in_section:bool -> +val export_private_constants : Safe_typing.private_constants Entries.proof_output -> Constr.constr Univ.in_universe_context_set * Safe_typing.exported_private_constant list val add_constant : - side_effect:'a Safe_typing.effect_entry -> in_section:bool -> Id.t -> Safe_typing.global_declaration -> Constant.t * 'a + side_effect:'a Safe_typing.effect_entry -> Id.t -> Safe_typing.global_declaration -> Constant.t * 'a val add_mind : Id.t -> Entries.mutual_inductive_entry -> MutInd.t @@ -80,6 +80,8 @@ val close_section : Summary.frozen -> unit (** Close the section and reset the global state to the one at the time when the section what opened. *) +val sections_are_opened : unit -> bool + (** Interactive modules and module types *) val start_module : Id.t -> ModPath.t diff --git a/library/lib.ml b/library/lib.ml index 0d9efe2d5d..80b50b26d0 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -107,7 +107,6 @@ let segment_of_objects prefix = let initial_prefix = Nametab.{ obj_dir = default_library; obj_mp = ModPath.initial; - obj_sec = DirPath.empty; } type lib_state = { @@ -132,10 +131,10 @@ let library_dp () = let cwd () = !lib_state.path_prefix.Nametab.obj_dir let current_mp () = !lib_state.path_prefix.Nametab.obj_mp -let current_sections () = !lib_state.path_prefix.Nametab.obj_sec +let current_sections () = Safe_typing.sections_of_safe_env (Global.safe_env()) -let sections_depth () = List.length (Names.DirPath.repr (current_sections ())) -let sections_are_opened () = not (Names.DirPath.is_empty (current_sections ())) +let sections_depth () = Section.depth (current_sections()) +let sections_are_opened = Global.sections_are_opened let cwd_except_section () = Libnames.pop_dirpath_n (sections_depth ()) (cwd ()) @@ -169,7 +168,6 @@ let pop_path_prefix () = let op = !lib_state.path_prefix in lib_state := { !lib_state with path_prefix = Nametab.{ op with obj_dir = pop_dirpath op.obj_dir; - obj_sec = pop_dirpath op.obj_sec; } } let find_entry_p p = @@ -282,7 +280,7 @@ let current_mod_id () = let start_mod is_type export id mp fs = let dir = add_dirpath_suffix (!lib_state.path_prefix.Nametab.obj_dir) id in - let prefix = Nametab.{ obj_dir = dir; obj_mp = mp; obj_sec = Names.DirPath.empty } in + let prefix = Nametab.{ obj_dir = dir; obj_mp = mp; } in let exists = if is_type then Nametab.exists_cci (make_path id) else Nametab.exists_dir dir @@ -330,9 +328,9 @@ let contents_after sp = let (after,_,_) = split_lib sp in after let start_compilation s mp = if !lib_state.comp_name != None then user_err Pp.(str "compilation unit is already started"); - if not (Names.DirPath.is_empty (!lib_state.path_prefix.Nametab.obj_sec)) then + if Global.sections_are_opened () then (* XXX not sure if we need this check *) user_err Pp.(str "some sections are already opened"); - let prefix = Nametab.{ obj_dir = s; obj_mp = mp; obj_sec = DirPath.empty } in + let prefix = Nametab.{ obj_dir = s; obj_mp = mp } in add_anonymous_entry (CompilingLibrary prefix); lib_state := { !lib_state with comp_name = Some s; path_prefix = prefix } @@ -465,7 +463,7 @@ let open_section id = let () = Global.open_section () in let opp = !lib_state.path_prefix in let obj_dir = add_dirpath_suffix opp.Nametab.obj_dir id in - let prefix = Nametab.{ obj_dir; obj_mp = opp.obj_mp; obj_sec = add_dirpath_suffix opp.obj_sec id } in + let prefix = Nametab.{ obj_dir; obj_mp = opp.obj_mp; } in if Nametab.exists_dir obj_dir then user_err ~hdr:"open_section" (Id.print id ++ str " already exists."); let fs = Summary.freeze_summaries ~marshallable:false in diff --git a/library/lib.mli b/library/lib.mli index 59d77480e9..cef50a5f3b 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -95,6 +95,7 @@ val make_kn : Id.t -> KerName.t (** Are we inside an opened section *) val sections_are_opened : unit -> bool +[@@ocaml.deprecated "Use Global.sections_are_opened"] val sections_depth : unit -> int (** Are we inside an opened module type *) diff --git a/library/nametab.ml b/library/nametab.ml index aed7d08ac1..8626ee1c59 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -18,12 +18,10 @@ open Globnames type object_prefix = { obj_dir : DirPath.t; obj_mp : ModPath.t; - obj_sec : DirPath.t; } let eq_op op1 op2 = DirPath.equal op1.obj_dir op2.obj_dir && - DirPath.equal op1.obj_sec op2.obj_sec && ModPath.equal op1.obj_mp op2.obj_mp (* to this type are mapped DirPath.t's in the nametab *) diff --git a/library/nametab.mli b/library/nametab.mli index 6ee22fc283..55458fe2c6 100644 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -74,7 +74,6 @@ open Globnames type object_prefix = { obj_dir : DirPath.t; obj_mp : ModPath.t; - obj_sec : DirPath.t; } val eq_op : object_prefix -> object_prefix -> bool diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 96a3d00dc2..be9259861a 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -380,7 +380,7 @@ let check_inside_module () = warn_extraction_inside_module () let check_inside_section () = - if Lib.sections_are_opened () then + if Global.sections_are_opened () then err (str "You can't do that within a section." ++ fnl () ++ str "Close it and try again.") diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg index 9b52b710c1..1b00a93834 100644 --- a/plugins/ltac/g_tactic.mlg +++ b/plugins/ltac/g_tactic.mlg @@ -182,10 +182,6 @@ let mkCLambdaN_simple bl c = match bl with let loc_of_ne_list l = Loc.merge_opt (List.hd l).CAst.loc (List.last l).CAst.loc -let map_int_or_var f = function - | ArgArg x -> ArgArg (f x) - | ArgVar _ as y -> y - let all_concl_occs_clause = { onhyps=Some[]; concl_occs=AllOccurrences } let merge_occurrences loc cl = function @@ -269,7 +265,7 @@ GRAMMAR EXTEND Gram [ [ nl = LIST1 nat_or_var -> { OnlyOccurrences nl } | "-"; n = nat_or_var; nl = LIST0 int_or_var -> (* have used int_or_var instead of nat_or_var for compatibility *) - { AllOccurrencesBut (List.map (map_int_or_var abs) (n::nl)) } ] ] + { AllOccurrencesBut (List.map (Locusops.or_var_map abs) (n::nl)) } ] ] ; occs: [ [ "at"; occs = occs_nums -> { occs } | -> { AllOccurrences } ] ] diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml index b6e7dd64b0..bf5d49f678 100644 --- a/plugins/ltac/tacsubst.ml +++ b/plugins/ltac/tacsubst.ml @@ -76,25 +76,21 @@ let subst_and_short_name f (c,n) = (* assert (n=None); *)(* since tacdef are strictly globalized *) (f c,None) -let subst_or_var f = let open Locus in function - | ArgVar _ as x -> x - | ArgArg x -> ArgArg (f x) - let subst_located f = Loc.map f let subst_reference subst = - subst_or_var (subst_located (subst_kn subst)) + Locusops.or_var_map (subst_located (subst_kn subst)) (*CSC: subst_global_reference is used "only" for RefArgType, that propagates to the syntactic non-terminals "global", used in commands such as Print. It is also used for non-evaluable references. *) let subst_global_reference subst = - subst_or_var (subst_located (subst_global_reference subst)) + Locusops.or_var_map (subst_located (subst_global_reference subst)) let subst_evaluable subst = let subst_eval_ref = subst_evaluable_reference subst in - subst_or_var (subst_and_short_name subst_eval_ref) + Locusops.or_var_map (subst_and_short_name subst_eval_ref) let subst_constr_with_occurrences subst (l,c) = (l,subst_glob_constr subst c) diff --git a/pretyping/locusops.ml b/pretyping/locusops.ml index 02c8f6a2a8..9c6cf090a2 100644 --- a/pretyping/locusops.ml +++ b/pretyping/locusops.ml @@ -10,6 +10,12 @@ open Locus +(** Utilities on or_var *) + +let or_var_map f = function + | ArgArg x -> ArgArg (f x) + | ArgVar _ as y -> y + (** Utilities on occurrences *) let occurrences_map f = function diff --git a/pretyping/locusops.mli b/pretyping/locusops.mli index 195dbec935..47d2ffe797 100644 --- a/pretyping/locusops.mli +++ b/pretyping/locusops.mli @@ -11,6 +11,10 @@ open Names open Locus +(** Utilities on or_var *) + +val or_var_map : ('a -> 'b) -> 'a or_var -> 'b or_var + (** Utilities on occurrences *) val occurrences_map : diff --git a/printing/printmod.ml b/printing/printmod.ml index 03921bca30..4cc6bc2052 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -213,7 +213,7 @@ let print_kn locals kn = let nametab_register_dir obj_mp = let id = mk_fake_top () in let obj_dir = DirPath.make [id] in - Nametab.(push_dir (Until 1) obj_dir (GlobDirRef.DirModule { obj_dir; obj_mp; obj_sec = DirPath.empty })) + Nametab.(push_dir (Until 1) obj_dir (GlobDirRef.DirModule { obj_dir; obj_mp; })) (** Nota: the [global_reference] we register in the nametab below might differ from internal ones, since we cannot recreate here diff --git a/tactics/declare.ml b/tactics/declare.ml index 3590146dfb..61321cd605 100644 --- a/tactics/declare.ml +++ b/tactics/declare.ml @@ -249,14 +249,13 @@ let is_unsafe_typing_flags () = let define_constant ~side_effect ~name cd = (* Logically define the constant and its subproofs, no libobject tampering *) - let in_section = Lib.sections_are_opened () in let export, decl, unsafe = match cd with | DefinitionEntry de -> (* We deal with side effects *) if not de.proof_entry_opaque then (* This globally defines the side-effects in the environment. *) let body, eff = Future.force de.proof_entry_body in - let body, export = Global.export_private_constants ~in_section (body, eff.Evd.seff_private) in + let body, export = Global.export_private_constants (body, eff.Evd.seff_private) in let export = get_roles export eff in let de = { de with proof_entry_body = Future.from_val (body, ()) } in let cd = Entries.DefinitionEntry (cast_proof_entry de) in @@ -272,7 +271,7 @@ let define_constant ~side_effect ~name cd = | PrimitiveEntry e -> [], ConstantEntry (PureEntry, Entries.PrimitiveEntry e), false in - let kn, eff = Global.add_constant ~side_effect ~in_section name decl in + let kn, eff = Global.add_constant ~side_effect name decl in if unsafe || is_unsafe_typing_flags() then feedback_axiom(); kn, eff, export @@ -319,7 +318,7 @@ let declare_variable ~name ~kind d = (* The body should already have been forced upstream because it is a section-local definition, but it's not enforced by typing *) let (body, eff) = Future.force de.proof_entry_body in - let ((body, uctx), export) = Global.export_private_constants ~in_section:true (body, eff.Evd.seff_private) in + let ((body, uctx), export) = Global.export_private_constants (body, eff.Evd.seff_private) in let eff = get_roles export eff in let () = List.iter register_side_effect eff in let poly, univs = match de.proof_entry_universes with @@ -585,7 +584,7 @@ let declare_univ_binders gr pl = Lib.add_anonymous_leaf (input_univ_names (QualifiedUniv l, univs)) let do_universe ~poly l = - let in_section = Lib.sections_are_opened () in + let in_section = Global.sections_are_opened () in let () = if poly && not in_section then CErrors.user_err ~hdr:"Constraint" diff --git a/theories/Logic/ClassicalFacts.v b/theories/Logic/ClassicalFacts.v index 2a9e15ab37..8538b54c08 100644 --- a/theories/Logic/ClassicalFacts.v +++ b/theories/Logic/ClassicalFacts.v @@ -29,7 +29,7 @@ Table of contents: 3. Weak classical axioms -3.1. Weak excluded middle +3.1. Weak excluded middle and classical de Morgan law 3.2. Gödel-Dummett axiom and right distributivity of implication over disjunction @@ -514,7 +514,7 @@ End Weak_proof_irrelevance_CCI. (** * Weak classical axioms *) (** We show the following increasing in the strength of axioms: - - weak excluded-middle + - weak excluded-middle and classical De Morgan's law - right distributivity of implication over disjunction and Gödel-Dummett axiom - independence of general premises and drinker's paradox - excluded-middle @@ -523,11 +523,15 @@ End Weak_proof_irrelevance_CCI. (** ** Weak excluded-middle *) (** The weak classical logic based on [~~A \/ ~A] is referred to with - name KC in [[ChagrovZakharyaschev97]] + name KC in [[ChagrovZakharyaschev97]]. See [[SorbiTerwijn11]] for + a short survey. [[ChagrovZakharyaschev97]] Alexander Chagrov and Michael Zakharyaschev, "Modal Logic", Clarendon Press, 1997. -*) + + [[SorbiTerwijn11]] Andrea Sorbi and Sebastiaan A. Terwijn, + "Generalizations of the weak law of the excluded-middle", Notre + Dame J. Formal Logic, vol 56(2), pp 321-331, 2015. *) Definition weak_excluded_middle := forall A:Prop, ~~A \/ ~A. @@ -539,16 +543,21 @@ Definition weak_excluded_middle := Definition weak_generalized_excluded_middle := forall A B:Prop, ((A -> B) -> B) \/ (A -> B). +(** Classical De Morgan's law *) + +Definition classical_de_morgan_law := + forall A B:Prop, ~(A /\ B) -> ~A \/ ~B. + (** ** Gödel-Dummett axiom *) (** [(A->B) \/ (B->A)] is studied in [[Dummett59]] and is based on [[Gödel33]]. [[Dummett59]] Michael A. E. Dummett. "A Propositional Calculus - with a Denumerable Matrix", In the Journal of Symbolic Logic, Vol - 24 No. 2(1959), pp 97-103. + with a Denumerable Matrix", In the Journal of Symbolic Logic, vol + 24(2), pp 97-103, 1959. [[Gödel33]] Kurt Gödel. "Zum intuitionistischen Aussagenkalkül", - Ergeb. Math. Koll. 4 (1933), pp. 34-38. + Ergeb. Math. Koll. 4, pp. 34-38, 1933. *) Definition GodelDummett := forall A B:Prop, (A -> B) \/ (B -> A). @@ -590,6 +599,16 @@ Proof. right; intro HA; apply (HAnotA HA HA). Qed. +(** The weak excluded middle is equivalent to the classical De Morgan's law *) + +Lemma weak_excluded_middle_iff_classical_de_morgan_law : + weak_excluded_middle <-> classical_de_morgan_law. +Proof. + split; [intro WEM|intro CDML]; intros A *. + - destruct (WEM A); tauto. + - destruct (CDML A (~A)); tauto. +Qed. + (** ** Independence of general premises and drinker's paradox *) (** Independence of general premises is the unconstrained, non diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index 5ba8b0ab3c..f9b73a59eb 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -287,7 +287,7 @@ let context ~poly l = name,b,t,impl) ctx in - if Lib.sections_are_opened () + if Global.sections_are_opened () then context_insection sigma ~poly ctx else context_nosection sigma ~poly ctx diff --git a/vernac/comPrimitive.ml b/vernac/comPrimitive.ml index 06fafddafb..b66ff876d3 100644 --- a/vernac/comPrimitive.ml +++ b/vernac/comPrimitive.ml @@ -9,7 +9,7 @@ (************************************************************************) let do_primitive id prim typopt = - if Lib.sections_are_opened () then + if Global.sections_are_opened () then CErrors.user_err Pp.(str "Declaring a primitive is not allowed in sections."); if Dumpglob.dump () then Dumpglob.dump_definition id false "ax"; let env = Global.env () in diff --git a/vernac/declaremods.ml b/vernac/declaremods.ml index 58a7dff5fd..c7b68d18c2 100644 --- a/vernac/declaremods.ml +++ b/vernac/declaremods.ml @@ -211,7 +211,7 @@ let compute_visibility exists i = (** Iterate some function [iter_objects] on all components of a module *) let do_module exists iter_objects i obj_dir obj_mp sobjs kobjs = - let prefix = Nametab.{ obj_dir ; obj_mp; obj_sec = DirPath.empty } in + let prefix = Nametab.{ obj_dir ; obj_mp; } in let dirinfo = Nametab.GlobDirRef.DirModule prefix in consistency_checks exists obj_dir dirinfo; Nametab.push_dir (compute_visibility exists i) obj_dir dirinfo; @@ -266,14 +266,14 @@ and load_objects i prefix objs = and load_include i ((sp,kn), aobjs) = let obj_dir = Libnames.dirpath sp in let obj_mp = KerName.modpath kn in - let prefix = Nametab.{ obj_dir; obj_mp; obj_sec = DirPath.empty } in + let prefix = Nametab.{ obj_dir; obj_mp; } in let o = expand_aobjs aobjs in load_objects i prefix o and load_keep i ((sp,kn),kobjs) = (* Invariant : seg isn't empty *) let obj_dir = dir_of_sp sp and obj_mp = mp_of_kn kn in - let prefix = Nametab.{ obj_dir ; obj_mp; obj_sec = DirPath.empty } in + let prefix = Nametab.{ obj_dir ; obj_mp; } in let modobjs = try ModObjs.get obj_mp with Not_found -> assert false (* a substobjs should already be loaded *) @@ -327,7 +327,7 @@ let rec open_object i (name, obj) = | KeepObject objs -> open_keep i (name, objs) and open_module i obj_dir obj_mp sobjs = - let prefix = Nametab.{ obj_dir ; obj_mp; obj_sec = DirPath.empty } in + let prefix = Nametab.{ obj_dir ; obj_mp; } in let dirinfo = Nametab.GlobDirRef.DirModule prefix in consistency_checks true obj_dir dirinfo; Nametab.push_dir (Nametab.Exactly i) obj_dir dirinfo; @@ -353,7 +353,7 @@ and open_modtype i ((sp,kn),_) = and open_include i ((sp,kn), aobjs) = let obj_dir = Libnames.dirpath sp in let obj_mp = KerName.modpath kn in - let prefix = Nametab.{ obj_dir; obj_mp; obj_sec = DirPath.empty } in + let prefix = Nametab.{ obj_dir; obj_mp; } in let o = expand_aobjs aobjs in open_objects i prefix o @@ -363,7 +363,7 @@ and open_export i mpl = and open_keep i ((sp,kn),kobjs) = let obj_dir = dir_of_sp sp and obj_mp = mp_of_kn kn in - let prefix = Nametab.{ obj_dir; obj_mp; obj_sec = DirPath.empty } in + let prefix = Nametab.{ obj_dir; obj_mp; } in open_objects i prefix kobjs let rec cache_object (name, obj) = @@ -380,7 +380,7 @@ let rec cache_object (name, obj) = and cache_include ((sp,kn), aobjs) = let obj_dir = Libnames.dirpath sp in let obj_mp = KerName.modpath kn in - let prefix = Nametab.{ obj_dir; obj_mp; obj_sec = DirPath.empty } in + let prefix = Nametab.{ obj_dir; obj_mp; } in let o = expand_aobjs aobjs in load_objects 1 prefix o; open_objects 1 prefix o diff --git a/vernac/locality.ml b/vernac/locality.ml index f033d32874..5862f51b43 100644 --- a/vernac/locality.ml +++ b/vernac/locality.ml @@ -39,7 +39,7 @@ let enforce_locality_exp locality_flag discharge = match locality_flag, discharge with | Some b, NoDischarge -> Global (importability_of_bool b) | None, NoDischarge -> Global Declare.ImportDefaultBehavior - | None, DoDischarge when not (Lib.sections_are_opened ()) -> + | None, DoDischarge when not (Global.sections_are_opened ()) -> (* If a Let/Variable is defined outside a section, then we consider it as a local definition *) warn_local_declaration (); Global Declare.ImportNeedQualified @@ -55,7 +55,7 @@ let enforce_locality locality_flag = Local in sections is the default, Local not in section forces non-export *) let make_section_locality = - function Some b -> b | None -> Lib.sections_are_opened () + function Some b -> b | None -> Global.sections_are_opened () let enforce_section_locality locality_flag = make_section_locality locality_flag @@ -68,7 +68,7 @@ let enforce_section_locality locality_flag = let make_module_locality = function | Some false -> - if Lib.sections_are_opened () then + if Global.sections_are_opened () then CErrors.user_err Pp.(str "This command does not support the Global option in sections."); false diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 4734ce1fb9..430cee62c2 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -810,14 +810,14 @@ let vernac_combined_scheme lid l = Indschemes.do_combined_scheme lid l let vernac_universe ~poly l = - if poly && not (Lib.sections_are_opened ()) then + if poly && not (Global.sections_are_opened ()) then user_err ~hdr:"vernac_universe" (str"Polymorphic universes can only be declared inside sections, " ++ str "use Monomorphic Universe instead"); Declare.do_universe ~poly l let vernac_constraint ~poly l = - if poly && not (Lib.sections_are_opened ()) then + if poly && not (Global.sections_are_opened ()) then user_err ~hdr:"vernac_constraint" (str"Polymorphic universe constraints can only be declared" ++ str " inside sections, use Monomorphic Constraint instead"); @@ -837,7 +837,7 @@ let vernac_import export refl = 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 + if Global.sections_are_opened () then user_err Pp.(str "Modules and Module Types are not allowed inside sections."); let binders_ast = List.map (fun (export,idl,ty) -> @@ -852,7 +852,7 @@ let vernac_declare_module export {loc;v=id} binders_ast mty_ast = 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 + if Global.sections_are_opened () then user_err Pp.(str "Modules and Module Types are not allowed inside sections."); match mexpr_ast_l with | [] -> @@ -893,7 +893,7 @@ let vernac_end_module export {loc;v=id} = Option.iter (fun export -> vernac_import export [qualid_of_ident ?loc id]) export let vernac_declare_module_type {loc;v=id} binders_ast mty_sign mty_ast_l = - if Lib.sections_are_opened () then + if Global.sections_are_opened () then user_err Pp.(str "Modules and Module Types are not allowed inside sections."); match mty_ast_l with @@ -969,7 +969,7 @@ let warn_require_in_section = (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 (); + if Global.sections_are_opened () then warn_require_in_section (); let root = match from with | None -> None | Some from -> @@ -2098,7 +2098,7 @@ let vernac_register qid r = | RegisterCoqlib n -> let ns, id = Libnames.repr_qualid n in if DirPath.equal (dirpath_of_string "kernel") ns then begin - if Lib.sections_are_opened () then + if Global.sections_are_opened () then user_err Pp.(str "Registering a kernel type is not allowed in sections"); let pind = match Id.to_string id with | "ind_bool" -> CPrimitives.PIT_bool |