diff options
Diffstat (limited to 'interp')
35 files changed, 242 insertions, 1007 deletions
diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml index 3ebbbdfb88..e4af0fcee0 100644 --- a/interp/constrexpr.ml +++ b/interp/constrexpr.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index bcb2f34377..8fce24249c 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli index f1a8ed202f..3ed240d356 100644 --- a/interp/constrexpr_ops.mli +++ b/interp/constrexpr_ops.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/interp/constrextern.ml b/interp/constrextern.ml index fe50bd4b08..8573dccdf9 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -757,11 +757,10 @@ let extended_glob_local_binder_of_decl ?loc u = DAst.make ?loc (extended_glob_lo (* mapping glob_constr to constr_expr *) let extern_glob_sort = function - | GSProp -> GSProp - | GProp -> GProp - | GSet -> GSet - | GType _ as s when !print_universes -> s - | GType _ -> GType [] + (* In case we print a glob_constr w/o having passed through detyping *) + | UNamed [(GSProp,0) | (GProp,0) | (GSet,0)] as u -> u + | UNamed _ when not !print_universes -> UAnonymous {rigid=true} + | UNamed _ | UAnonymous _ as u -> u let extern_universes = function | Some _ as l when !print_universes -> l @@ -1312,10 +1311,10 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with Array.map (fun (bl,_,_) -> bl) v, Array.map (fun (_,_,ty) -> ty) v, Array.map (fun (_,bd,_) -> bd) v) - | PSort Sorts.InSProp -> GSort GSProp - | PSort Sorts.InProp -> GSort GProp - | PSort Sorts.InSet -> GSort GSet - | PSort Sorts.InType -> GSort (GType []) + | PSort Sorts.InSProp -> GSort (UNamed [GSProp,0]) + | PSort Sorts.InProp -> GSort (UNamed [GProp,0]) + | PSort Sorts.InSet -> GSort (UNamed [GSet,0]) + | PSort Sorts.InType -> GSort (UAnonymous {rigid=true}) | PInt i -> GInt i let extern_constr_pattern env sigma pat = diff --git a/interp/constrextern.mli b/interp/constrextern.mli index f09b316cd6..7b8b93377b 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 1dd68f2abf..be8f99028c 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -372,6 +372,9 @@ let check_hidden_implicit_parameters ?loc id impls = strbrk "a parameter of the inductive type; bound variables in " ++ strbrk "the type of a constructor shall use a different name.") +let pure_push_name_env (id,implargs) env = + {env with ids = Id.Set.add id env.ids; impls = Id.Map.add id implargs env.impls} + let push_name_env ?(global_level=false) ntnvars implargs env = let open CAst in function @@ -386,15 +389,23 @@ let push_name_env ?(global_level=false) ntnvars implargs env = set_var_scope ?loc id false (env.tmp_scope,env.scopes) ntnvars; if global_level then Dumpglob.dump_definition CAst.(make ?loc id) true "var" else Dumpglob.dump_binding ?loc id; - {env with ids = Id.Set.add id env.ids; impls = Id.Map.add id implargs env.impls} + pure_push_name_env (id,implargs) env + +let remember_binders_impargs env bl = + List.map_filter (fun (na,_,_,_) -> + match na with + | Anonymous -> None + | Name id -> Some (id,Id.Map.find id env.impls)) bl + +let restore_binders_impargs env l = + List.fold_right pure_push_name_env l env let intern_generalized_binder ?(global_level=false) intern_type ntnvars env {loc;v=na} b' t ty = let ids = (match na with Anonymous -> fun x -> x | Name na -> Id.Set.add na) env.ids in let ty, ids' = - if t then ty, ids else - Implicit_quantifiers.implicit_application ids - Implicit_quantifiers.combine_params_freevar ty + if t then ty, ids + else Implicit_quantifiers.implicit_application ids ty in let ty' = intern_type {env with ids = ids; unb = true} ty in let fvs = Implicit_quantifiers.generalizable_vars_of_glob_constr ~bound:ids ~allowed:ids' ty' in @@ -998,18 +1009,10 @@ let intern_reference qid = in Smartlocate.global_of_extended_global r -let sort_info_of_level_info (info: level_info) : (Libnames.qualid * int) option = - match info with - | UAnonymous -> None - | UUnknown -> None - | UNamed id -> Some (id, 0) - let glob_sort_of_level (level: glob_level) : glob_sort = match level with - | GSProp -> GSProp - | GProp -> GProp - | GSet -> GSet - | GType info -> GType [sort_info_of_level_info info] + | UAnonymous {rigid} -> UAnonymous {rigid} + | UNamed id -> UNamed [id,0] (* Is it a global reference or a syntactic definition? *) let intern_qualid ?(no_secvar=false) qid intern env ntnvars us args = @@ -1045,7 +1048,7 @@ let intern_qualid ?(no_secvar=false) qid intern env ntnvars us args = DAst.make ?loc @@ GApp (DAst.make ?loc:loc' @@ GRef (ref, us), arg) | _ -> err () end - | Some [s], GSort (GType []) -> DAst.make ?loc @@ GSort (glob_sort_of_level s) + | Some [s], GSort (UAnonymous {rigid=true}) -> DAst.make ?loc @@ GSort (glob_sort_of_level s) | Some [_old_level], GSort _new_sort -> (* TODO: add old_level and new_sort to the error message *) user_err ?loc (str "Cannot change universe level of notation " ++ pr_qualid qid) @@ -1308,7 +1311,7 @@ let find_pattern_variable qid = if qualid_is_ident qid then qualid_basename qid else raise (InternalizationError(qid.CAst.loc,NotAConstructor qid)) -let check_duplicate loc fields = +let check_duplicate ?loc fields = let eq (ref1, _) (ref2, _) = qualid_eq ref1 ref2 in let dups = List.duplicates eq fields in match dups with @@ -1353,7 +1356,7 @@ let sort_fields ~complete loc fields completer = try Nametab.shortest_qualid_of_global ?loc Id.Set.empty global_record_id with Not_found -> anomaly (str "Environment corruption for records.") in - let () = check_duplicate loc fields in + let () = check_duplicate ?loc fields in let (end_index, (* one past the last field index *) first_field_index, (* index of the first field of the record *) proj_list) (* list of projections *) @@ -1843,7 +1846,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = in apply_impargs c env imp subscopes l loc - | CFix ({ CAst.loc = locid; v = iddef}, dl) -> + | CFix ({ CAst.loc = locid; v = iddef}, dl) -> let lf = List.map (fun ({CAst.v = id},_,_,_,_) -> id) dl in let dl = Array.of_list dl in let n = @@ -1865,14 +1868,18 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = rbefore) recarg in let (env',rbl) = List.fold_left intern_local_binder (env',rbefore) after in let bl = List.rev (List.map glob_local_binder_of_extended rbl) in - (n, bl, intern_type env' ty, env')) dl in - let idl = Array.map2 (fun (_,_,_,_,bd) (a,b,c,env') -> - let env'' = List.fold_left_i (fun i en name -> - let (_,bli,tyi,_) = idl_temp.(i) in - let fix_args = (List.map (fun (na, bk, _, _) -> (build_impls bk na)) bli) in - push_name_env ntnvars (impls_type_list ~args:fix_args tyi) - en (CAst.make @@ Name name)) 0 env' lf in - (a,b,c,intern {env'' with tmp_scope = None} bd)) dl idl_temp in + let bl_impls = remember_binders_impargs env' bl in + (n, bl, intern_type env' ty, bl_impls)) dl in + (* We add the recursive functions to the environment *) + let env_rec = List.fold_left_i (fun i en name -> + let (_,bli,tyi,_) = idl_temp.(i) in + let fix_args = (List.map (fun (na, bk, _, _) -> build_impls bk na) bli) in + push_name_env ntnvars (impls_type_list ~args:fix_args tyi) + en (CAst.make @@ Name name)) 0 env lf in + let idl = Array.map2 (fun (_,_,_,_,bd) (n,bl,ty,before_impls) -> + (* We add the binders common to body and type to the environment *) + let env_body = restore_binders_impargs env_rec before_impls in + (n,bl,ty,intern {env_body with tmp_scope = None} bd)) dl idl_temp in DAst.make ?loc @@ GRec (GFix (Array.map (fun (ro,_,_,_) -> ro) idl,n), @@ -1892,15 +1899,18 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = let idl_tmp = Array.map (fun ({ CAst.loc; v = id },bl,ty,_) -> let (env',rbl) = List.fold_left intern_local_binder (env,[]) bl in - (List.rev (List.map glob_local_binder_of_extended rbl), - intern_type env' ty,env')) dl in - let idl = Array.map2 (fun (_,_,_,bd) (b,c,env') -> - let env'' = List.fold_left_i (fun i en name -> - let (bli,tyi,_) = idl_tmp.(i) in - let cofix_args = List.map (fun (na, bk, _, _) -> (build_impls bk na)) bli in - push_name_env ntnvars (impls_type_list ~args:cofix_args tyi) - en (CAst.make @@ Name name)) 0 env' lf in - (b,c,intern {env'' with tmp_scope = None} bd)) dl idl_tmp in + let bl = List.rev (List.map glob_local_binder_of_extended rbl) in + let bl_impls = remember_binders_impargs env' bl in + (bl,intern_type env' ty,bl_impls)) dl in + let env_rec = List.fold_left_i (fun i en name -> + let (bli,tyi,_) = idl_tmp.(i) in + let cofix_args = List.map (fun (na, bk, _, _) -> build_impls bk na) bli in + push_name_env ntnvars (impls_type_list ~args:cofix_args tyi) + en (CAst.make @@ Name name)) 0 env lf in + let idl = Array.map2 (fun (_,_,_,bd) (b,c,bl_impls) -> + (* We add the binders common to body and type to the environment *) + let env_body = restore_binders_impargs env_rec bl_impls in + (b,c,intern {env_body with tmp_scope = None} bd)) dl idl_tmp in DAst.make ?loc @@ GRec (GCoFix n, Array.of_list lf, @@ -2443,10 +2453,8 @@ let interp_glob_context_evars ?(program_mode=false) env sigma k bl = let r = Retyping.relevance_of_type env sigma t in let d = LocalAssum (make_annot na r,t) in let impls = - if k == Implicit then - let na = match na with Name n -> Some n | Anonymous -> None in - (ExplByPos (n, na), (true, true, true)) :: impls - else impls + if k == Implicit then CAst.make (Some (na,true)) :: impls + else CAst.make None :: impls in (push_rel d env, sigma, d::params, succ n, impls) | Some b -> @@ -2455,7 +2463,7 @@ let interp_glob_context_evars ?(program_mode=false) env sigma k bl = let d = LocalDef (make_annot na r, c, t) in (push_rel d env, sigma, d::params, n, impls)) (env,sigma,[],k+1,[]) (List.rev bl) - in sigma, ((env, par), impls) + in sigma, ((env, par), List.rev impls) let interp_context_evars ?program_mode ?(global_level=false) ?(impl_env=empty_internalization_env) ?(shift=0) env sigma params = let int_env,bl = intern_context global_level env impl_env params in diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 0d4bc91f57..6c1f4898d9 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -61,10 +61,10 @@ type internalization_env = var_internalization_data Id.Map.t val empty_internalization_env : internalization_env val compute_internalization_data : env -> evar_map -> var_internalization_type -> - types -> Impargs.manual_explicitation list -> var_internalization_data + types -> Impargs.manual_implicits -> var_internalization_data val compute_internalization_env : env -> evar_map -> ?impls:internalization_env -> var_internalization_type -> - Id.t list -> types list -> Impargs.manual_explicitation list list -> + Id.t list -> types list -> Impargs.manual_implicits list -> internalization_env type ltac_sign = { @@ -189,3 +189,7 @@ val for_grammar : ('a -> 'b) -> 'a -> 'b (** Placeholder for global option, should be moved to a parameter *) val get_asymmetric_patterns : unit -> bool + +val check_duplicate : ?loc:Loc.t -> (qualid * constr_expr) list -> unit +(** Check that a list of record field definitions doesn't contain + duplicates. *) diff --git a/interp/declare.ml b/interp/declare.ml deleted file mode 100644 index cc6f29f756..0000000000 --- a/interp/declare.ml +++ /dev/null @@ -1,586 +0,0 @@ -(************************************************************************) -(* * 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 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -(** This module is about the low-level declaration of logical objects *) - -open Pp -open CErrors -open Util -open Names -open Libnames -open Globnames -open Constr -open Declarations -open Entries -open Libobject -open Lib -open Impargs -open Safe_typing -open Cooking -open Decls -open Decl_kinds - -(** flag for internal message display *) -type internal_flag = - | UserAutomaticRequest (* kernel action, a message is displayed *) - | InternalTacticRequest (* kernel action, no message is displayed *) - | UserIndividualRequest (* user action, a message is displayed *) - -(** Declaration of constants and parameters *) - -type constant_obj = { - cst_decl : Cooking.recipe option; - (** Non-empty only when rebuilding a constant after a section *) - cst_kind : logical_kind; - cst_locl : bool; -} - -type constant_declaration = Safe_typing.private_constants constant_entry * logical_kind - -(* At load-time, the segment starting from the module name to the discharge *) -(* section (if Remark or Fact) is needed to access a construction *) -let load_constant i ((sp,kn), obj) = - if Nametab.exists_cci sp then - alreadydeclared (Id.print (basename sp) ++ str " already exists"); - let con = Global.constant_of_delta_kn kn in - Nametab.push (Nametab.Until i) sp (ConstRef con); - add_constant_kind con obj.cst_kind - -let cooking_info segment = - let modlist = replacement_context () in - let { abstr_ctx = hyps; abstr_subst = subst; abstr_uctx = uctx } = segment in - let named_ctx = List.map fst hyps in - let abstract = (named_ctx, subst, uctx) in - { Opaqueproof.modlist; abstract } - -(* Opening means making the name without its module qualification available *) -let open_constant i ((sp,kn), obj) = - (* Never open a local definition *) - if obj.cst_locl then () - else - let con = Global.constant_of_delta_kn kn in - Nametab.push (Nametab.Exactly i) sp (ConstRef con) - -let exists_name id = - variable_exists id || Global.exists_objlabel (Label.of_id id) - -let check_exists id = - if exists_name id then alreadydeclared (Id.print id ++ str " already exists") - -let cache_constant ((sp,kn), obj) = - (* Invariant: the constant must exist in the logical environment, except when - redefining it when exiting a section. See [discharge_constant]. *) - let id = basename sp in - let kn' = - match obj.cst_decl with - | None -> - if Global.exists_objlabel (Label.of_id (basename sp)) - then Constant.make1 kn - else CErrors.anomaly Pp.(str"Missing constant " ++ Id.print(basename sp) ++ str".") - | Some r -> - Global.add_recipe ~in_section:(Lib.sections_are_opened ()) id r - in - assert (Constant.equal kn' (Constant.make1 kn)); - Nametab.push (Nametab.Until 1) sp (ConstRef (Constant.make1 kn)); - let cst = Global.lookup_constant kn' in - add_section_constant (Declareops.constant_is_polymorphic cst) kn' cst.const_hyps; - add_constant_kind (Constant.make1 kn) obj.cst_kind - -let discharge_constant ((sp, kn), obj) = - let con = Constant.make1 kn in - let from = Global.lookup_constant con in - let info = cooking_info (section_segment_of_constant con) in - (* This is a hack: when leaving a section, we lose the constant definition, so - we have to store it in the libobject to be able to retrieve it after. *) - Some { obj with cst_decl = Some { from; info } } - -(* Hack to reduce the size of .vo: we keep only what load/open needs *) -let dummy_constant cst = { - cst_decl = None; - cst_kind = cst.cst_kind; - cst_locl = cst.cst_locl; -} - -let classify_constant cst = Substitute (dummy_constant cst) - -let (inConstant : constant_obj -> obj) = - declare_object { (default_object "CONSTANT") with - cache_function = cache_constant; - load_function = load_constant; - open_function = open_constant; - classify_function = classify_constant; - subst_function = ident_subst_function; - discharge_function = discharge_constant } - -let declare_scheme = ref (fun _ _ -> assert false) -let set_declare_scheme f = declare_scheme := f - -let update_tables c = - declare_constant_implicits c; - Notation.declare_ref_arguments_scope Evd.empty (ConstRef c) - -let register_constant kn kind local = - let o = inConstant { - cst_decl = None; - cst_kind = kind; - cst_locl = local; - } in - let id = Label.to_id (Constant.label kn) in - let _ = add_leaf id o in - update_tables kn - -let register_side_effect (c, role) = - let () = register_constant c (IsProof Theorem) false in - match role with - | Subproof -> () - | Schema (ind, kind) -> !declare_scheme kind [|ind,c|] - -let default_univ_entry = Monomorphic_entry Univ.ContextSet.empty -let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types - ?(univs=default_univ_entry) ?(eff=Safe_typing.empty_private_constants) body = - { const_entry_body = Future.from_val ?fix_exn ((body,Univ.ContextSet.empty), eff); - const_entry_secctx = None; - const_entry_type = types; - const_entry_universes = univs; - const_entry_opaque = opaque; - const_entry_feedback = None; - const_entry_inline_code = inline} - -let define_constant ?role ?(export_seff=false) id cd = - (* Logically define the constant and its subproofs, no libobject tampering *) - let is_poly de = match de.const_entry_universes with - | Monomorphic_entry _ -> false - | Polymorphic_entry _ -> true - in - let in_section = Lib.sections_are_opened () in - let export, decl = (* We deal with side effects *) - match cd with - | DefinitionEntry de when - export_seff || - not de.const_entry_opaque || - is_poly de -> - (* This globally defines the side-effects in the environment. *) - let body, export = Global.export_private_constants ~in_section (Future.force de.const_entry_body) in - let de = { de with const_entry_body = Future.from_val (body, ()) } in - export, ConstantEntry (PureEntry, DefinitionEntry de) - | _ -> [], ConstantEntry (EffectEntry, cd) - in - let kn, eff = Global.add_constant ?role ~in_section id decl in - kn, eff, export - -let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(export_seff=false) (cd, kind) = - let () = check_exists id in - let kn, _eff, export = define_constant ~export_seff id cd in - (* Register the libobjects attached to the constants and its subproofs *) - let () = List.iter register_side_effect export in - let () = register_constant kn kind local in - kn - -let declare_private_constant ~role ?(internal=UserIndividualRequest) ?(local = false) id (cd, kind) = - let kn, eff, export = define_constant ~role id cd in - let () = assert (List.is_empty export) in - let () = register_constant kn kind local in - kn, eff - -let declare_definition ?(internal=UserIndividualRequest) - ?(opaque=false) ?(kind=Decl_kinds.Definition) ?(local = false) - id ?types (body,univs) = - let cb = - definition_entry ?types ~univs ~opaque body - in - declare_constant ~internal ~local id - (Entries.DefinitionEntry cb, Decl_kinds.IsDefinition kind) - -(** Declaration of section variables and local definitions *) -type section_variable_entry = - | SectionLocalDef of Safe_typing.private_constants definition_entry - | SectionLocalAssum of types Univ.in_universe_context_set * polymorphic * bool (** Implicit status *) - -type variable_declaration = DirPath.t * section_variable_entry * logical_kind - -let cache_variable ((sp,_),o) = - match o with - | Inl ctx -> Global.push_context_set false ctx - | Inr (id,(p,d,mk)) -> - (* Constr raisonne sur les noms courts *) - if variable_exists id then - alreadydeclared (Id.print id ++ str " already exists"); - - let impl,opaq,poly,ctx = match d with (* Fails if not well-typed *) - | SectionLocalAssum ((ty,ctx),poly,impl) -> - let () = Global.push_named_assum ((id,ty,poly),ctx) in - let impl = if impl then Implicit else Explicit in - impl, true, poly, ctx - | SectionLocalDef (de) -> - (* The body should already have been forced upstream because it is a - section-local definition, but it's not enforced by typing *) - let ((body, uctx), eff) = Global.export_private_constants ~in_section:true (Future.force de.const_entry_body) in - let () = List.iter register_side_effect eff in - let poly, univs = match de.const_entry_universes with - | Monomorphic_entry uctx -> false, uctx - | Polymorphic_entry (_, uctx) -> true, Univ.ContextSet.of_context uctx - in - let univs = Univ.ContextSet.union uctx univs in - (* We must declare the universe constraints before type-checking the - term. *) - let () = Global.push_context_set (not poly) univs in - let se = { - secdef_body = body; - secdef_secctx = de.const_entry_secctx; - secdef_feedback = de.const_entry_feedback; - secdef_type = de.const_entry_type; - } in - let () = Global.push_named_def (id, se) in - Explicit, de.const_entry_opaque, - poly, univs in - Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id); - add_section_variable id impl poly ctx; - add_variable_data id (p,opaq,ctx,poly,mk) - -let discharge_variable (_,o) = match o with - | Inr (id,_) -> - if variable_polymorphic id then None - else Some (Inl (variable_context id)) - | Inl _ -> Some o - -type variable_obj = - (Univ.ContextSet.t, Id.t * variable_declaration) union - -let inVariable : variable_obj -> obj = - declare_object { (default_object "VARIABLE") with - cache_function = cache_variable; - discharge_function = discharge_variable; - classify_function = (fun _ -> Dispose) } - -(* for initial declaration *) -let declare_variable id obj = - let oname = add_leaf id (inVariable (Inr (id,obj))) in - declare_var_implicits id; - Notation.declare_ref_arguments_scope Evd.empty (VarRef id); - oname - -(** Declaration of inductive blocks *) -let declare_inductive_argument_scopes kn mie = - List.iteri (fun i {mind_entry_consnames=lc} -> - Notation.declare_ref_arguments_scope Evd.empty (IndRef (kn,i)); - for j=1 to List.length lc do - Notation.declare_ref_arguments_scope Evd.empty (ConstructRef ((kn,i),j)); - done) mie.mind_entry_inds - -let inductive_names sp kn mie = - let (dp,_) = repr_path sp in - let kn = Global.mind_of_delta_kn kn in - let names, _ = - List.fold_left - (fun (names, n) ind -> - let ind_p = (kn,n) in - let names, _ = - List.fold_left - (fun (names, p) l -> - let sp = - Libnames.make_path dp l - in - ((sp, ConstructRef (ind_p,p)) :: names, p+1)) - (names, 1) ind.mind_entry_consnames in - let sp = Libnames.make_path dp ind.mind_entry_typename - in - ((sp, IndRef ind_p) :: names, n+1)) - ([], 0) mie.mind_entry_inds - in names - -let load_inductive i ((sp,kn),mie) = - let names = inductive_names sp kn mie in - List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until i) sp ref ) names - -let open_inductive i ((sp,kn),mie) = - let names = inductive_names sp kn mie in - List.iter (fun (sp, ref) -> Nametab.push (Nametab.Exactly i) sp ref) names - -let cache_inductive ((sp,kn),mie) = - let names = inductive_names sp kn mie in - List.iter check_exists (List.map (fun p -> basename (fst p)) names); - let id = basename sp in - let kn' = Global.add_mind id mie in - assert (MutInd.equal kn' (MutInd.make1 kn)); - let mind = Global.lookup_mind kn' in - add_section_kn (Declareops.inductive_is_polymorphic mind) kn' mind.mind_hyps; - List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until 1) sp ref) names - -let discharge_inductive ((sp,kn),mie) = - let mind = Global.mind_of_delta_kn kn in - let mie = Global.lookup_mind mind in - let info = cooking_info (section_segment_of_mutual_inductive mind) in - Some (Cooking.cook_inductive info mie) - -let dummy_one_inductive_entry mie = { - mind_entry_typename = mie.mind_entry_typename; - mind_entry_arity = mkProp; - mind_entry_template = false; - mind_entry_consnames = mie.mind_entry_consnames; - mind_entry_lc = [] -} - -(* Hack to reduce the size of .vo: we keep only what load/open needs *) -let dummy_inductive_entry m = { - mind_entry_params = []; - mind_entry_record = None; - mind_entry_finite = Declarations.BiFinite; - mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds; - mind_entry_universes = default_univ_entry; - mind_entry_variance = None; - mind_entry_private = None; -} - -(* reinfer subtyping constraints for inductive after section is dischared. *) -let rebuild_inductive mind_ent = - let env = Global.env () in - InferCumulativity.infer_inductive env mind_ent - -let inInductive : mutual_inductive_entry -> obj = - declare_object {(default_object "INDUCTIVE") with - cache_function = cache_inductive; - load_function = load_inductive; - open_function = open_inductive; - classify_function = (fun a -> Substitute (dummy_inductive_entry a)); - subst_function = ident_subst_function; - discharge_function = discharge_inductive; - rebuild_function = rebuild_inductive } - -let cache_prim (_,(p,c)) = Recordops.register_primitive_projection p c - -let load_prim _ p = cache_prim p - -let subst_prim (subst,(p,c)) = Mod_subst.subst_proj_repr subst p, Mod_subst.subst_constant subst c - -let discharge_prim (_,(p,c)) = Some (Lib.discharge_proj_repr p, c) - -let inPrim : (Projection.Repr.t * Constant.t) -> obj = - declare_object { - (default_object "PRIMPROJS") with - cache_function = cache_prim ; - load_function = load_prim; - subst_function = subst_prim; - classify_function = (fun x -> Substitute x); - discharge_function = discharge_prim } - -let declare_primitive_projection p c = Lib.add_anonymous_leaf (inPrim (p,c)) - -let declare_one_projection univs (mind,_ as ind) ~proj_npars proj_arg label (term,types) = - let id = Label.to_id label in - let univs, u = match univs with - | Monomorphic_entry _ -> - (* Global constraints already defined through the inductive *) - default_univ_entry, Univ.Instance.empty - | Polymorphic_entry (nas, ctx) -> - Polymorphic_entry (nas, ctx), Univ.UContext.instance ctx - in - let term = Vars.subst_instance_constr u term in - let types = Vars.subst_instance_constr u types in - let entry = definition_entry ~types ~univs term in - let cst = declare_constant id (DefinitionEntry entry, IsDefinition StructureComponent) in - let p = Projection.Repr.make ind ~proj_npars ~proj_arg label in - declare_primitive_projection p cst - - -let declare_projections univs mind = - let env = Global.env () in - let mib = Environ.lookup_mind mind env in - match mib.mind_record with - | PrimRecord info -> - let iter_ind i (_, labs, _, _) = - let ind = (mind, i) in - let projs = Inductiveops.compute_projections env ind in - Array.iter2_i (declare_one_projection univs ind ~proj_npars:mib.mind_nparams) labs projs - in - let () = Array.iteri iter_ind info in - true - | FakeRecord -> false - | NotRecord -> false - -(* for initial declaration *) -let declare_mind mie = - let id = match mie.mind_entry_inds with - | ind::_ -> ind.mind_entry_typename - | [] -> anomaly (Pp.str "cannot declare an empty list of inductives.") in - let (sp,kn as oname) = add_leaf id (inInductive mie) in - let mind = Global.mind_of_delta_kn kn in - let isprim = declare_projections mie.mind_entry_universes mind in - declare_mib_implicits mind; - declare_inductive_argument_scopes mind mie; - oname, isprim - -(* Declaration messages *) - -let pr_rank i = pr_nth (i+1) - -let fixpoint_message indexes l = - Flags.if_verbose Feedback.msg_info (match l with - | [] -> anomaly (Pp.str "no recursive definition.") - | [id] -> Id.print id ++ str " is recursively defined" ++ - (match indexes with - | Some [|i|] -> str " (decreasing on "++pr_rank i++str " argument)" - | _ -> mt ()) - | l -> hov 0 (prlist_with_sep pr_comma Id.print l ++ - spc () ++ str "are recursively defined" ++ - match indexes with - | Some a -> spc () ++ str "(decreasing respectively on " ++ - prvect_with_sep pr_comma pr_rank a ++ - str " arguments)" - | None -> mt ())) - -let cofixpoint_message l = - Flags.if_verbose Feedback.msg_info (match l with - | [] -> anomaly (Pp.str "No corecursive definition.") - | [id] -> Id.print id ++ str " is corecursively defined" - | l -> hov 0 (prlist_with_sep pr_comma Id.print l ++ - spc () ++ str "are corecursively defined")) - -let recursive_message isfix i l = - (if isfix then fixpoint_message i else cofixpoint_message) l - -let definition_message id = - Flags.if_verbose Feedback.msg_info (Id.print id ++ str " is defined") - -let assumption_message id = - (* Changing "assumed" to "declared", "assuming" referring more to - the type of the object than to the name of the object (see - discussion on coqdev: "Chapter 4 of the Reference Manual", 8/10/2015) *) - Flags.if_verbose Feedback.msg_info (Id.print id ++ str " is declared") - -(** Monomorphic universes need to survive sections. *) - -let input_universe_context : Univ.ContextSet.t -> Libobject.obj = - declare_object @@ local_object "Monomorphic section universes" - ~cache:(fun (na, uctx) -> Global.push_context_set false uctx) - ~discharge:(fun (_, x) -> Some x) - -let declare_universe_context poly ctx = - if poly then - (Global.push_context_set true ctx; Lib.add_section_context ctx) - else - Lib.add_anonymous_leaf (input_universe_context ctx) - -(** Global universes are not substitutive objects but global objects - bound at the *library* or *module* level. The polymorphic flag is - used to distinguish universes declared in polymorphic sections, which - are discharged and do not remain in scope. *) - -type universe_source = - | BoundUniv (* polymorphic universe, bound in a function (this will go away someday) *) - | QualifiedUniv of Id.t (* global universe introduced by some global value *) - | UnqualifiedUniv (* other global universe *) - -type universe_name_decl = universe_source * (Id.t * Univ.Level.UGlobal.t) list - -let check_exists sp = - if Nametab.exists_universe sp then - alreadydeclared (str "Universe " ++ Id.print (basename sp) ++ str " already exists") - else () - -let qualify_univ i dp src id = - match src with - | BoundUniv | UnqualifiedUniv -> - i, Libnames.make_path dp id - | QualifiedUniv l -> - let dp = DirPath.repr dp in - Nametab.map_visibility succ i, Libnames.make_path (DirPath.make (l::dp)) id - -let do_univ_name ~check i dp src (id,univ) = - let i, sp = qualify_univ i dp src id in - if check then check_exists sp; - Nametab.push_universe i sp univ - -let cache_univ_names ((sp, _), (src, univs)) = - let depth = sections_depth () in - let dp = pop_dirpath_n depth (dirpath sp) in - List.iter (do_univ_name ~check:true (Nametab.Until 1) dp src) univs - -let load_univ_names i ((sp, _), (src, univs)) = - List.iter (do_univ_name ~check:false (Nametab.Until i) (dirpath sp) src) univs - -let open_univ_names i ((sp, _), (src, univs)) = - List.iter (do_univ_name ~check:false (Nametab.Exactly i) (dirpath sp) src) univs - -let discharge_univ_names = function - | _, (BoundUniv, _) -> None - | _, ((QualifiedUniv _ | UnqualifiedUniv), _ as x) -> Some x - -let input_univ_names : universe_name_decl -> Libobject.obj = - declare_object - { (default_object "Global universe name state") with - cache_function = cache_univ_names; - load_function = load_univ_names; - open_function = open_univ_names; - discharge_function = discharge_univ_names; - subst_function = (fun (subst, a) -> (* Actually the name is generated once and for all. *) a); - classify_function = (fun a -> Substitute a) } - -let declare_univ_binders gr pl = - if Global.is_polymorphic gr then - () - else - let l = match gr with - | ConstRef c -> Label.to_id @@ Constant.label c - | IndRef (c, _) -> Label.to_id @@ MutInd.label c - | VarRef id -> anomaly ~label:"declare_univ_binders" Pp.(str "declare_univ_binders on variable " ++ Id.print id ++ str".") - | ConstructRef _ -> - anomaly ~label:"declare_univ_binders" - Pp.(str "declare_univ_binders on an constructor reference") - in - let univs = Id.Map.fold (fun id univ univs -> - match Univ.Level.name univ with - | None -> assert false (* having Prop/Set/Var as binders is nonsense *) - | Some univ -> (id,univ)::univs) pl [] - in - Lib.add_anonymous_leaf (input_univ_names (QualifiedUniv l, univs)) - -let do_universe poly l = - let in_section = Lib.sections_are_opened () in - let () = - if poly && not in_section then - user_err ~hdr:"Constraint" - (str"Cannot declare polymorphic universes outside sections") - in - let l = List.map (fun {CAst.v=id} -> (id, UnivGen.new_univ_global ())) l in - let ctx = List.fold_left (fun ctx (_,qid) -> Univ.LSet.add (Univ.Level.make qid) ctx) - Univ.LSet.empty l, Univ.Constraint.empty - in - let () = declare_universe_context poly ctx in - let src = if poly then BoundUniv else UnqualifiedUniv in - Lib.add_anonymous_leaf (input_univ_names (src, l)) - -let do_constraint poly l = - let open Univ in - let u_of_id x = - let level = Pretyping.interp_known_glob_level (Evd.from_env (Global.env ())) x in - Lib.is_polymorphic_univ level, level - in - let in_section = Lib.sections_are_opened () in - let () = - if poly && not in_section then - user_err ~hdr:"Constraint" - (str"Cannot declare polymorphic constraints outside sections") - in - let check_poly p p' = - if poly then () - else if p || p' then - user_err ~hdr:"Constraint" - (str "Cannot declare a global constraint on " ++ - str "a polymorphic universe, use " - ++ str "Polymorphic Constraint instead") - in - let constraints = List.fold_left (fun acc (l, d, r) -> - let p, lu = u_of_id l and p', ru = u_of_id r in - check_poly p p'; - Constraint.add (lu, d, ru) acc) - Constraint.empty l - in - let uctx = ContextSet.add_constraints constraints ContextSet.empty in - declare_universe_context poly uctx diff --git a/interp/declare.mli b/interp/declare.mli deleted file mode 100644 index 795d9a767d..0000000000 --- a/interp/declare.mli +++ /dev/null @@ -1,94 +0,0 @@ -(************************************************************************) -(* * 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 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -open Names -open Constr -open Entries -open Decl_kinds - -(** This module provides the official functions to declare new variables, - parameters, constants and inductive types. Using the following functions - will add the entries in the global environment (module [Global]), will - register the declarations in the library (module [Lib]) --- so that the - reset works properly --- and will fill some global tables such as - [Nametab] and [Impargs]. *) - -(** Declaration of local constructions (Variable/Hypothesis/Local) *) - -type section_variable_entry = - | SectionLocalDef of Safe_typing.private_constants definition_entry - | SectionLocalAssum of types Univ.in_universe_context_set * polymorphic * bool (** Implicit status *) - -type variable_declaration = DirPath.t * section_variable_entry * logical_kind - -val declare_variable : variable -> variable_declaration -> Libobject.object_name - -(** Declaration of global constructions - i.e. Definition/Theorem/Axiom/Parameter/... *) - -type constant_declaration = Safe_typing.private_constants constant_entry * logical_kind - -type internal_flag = - | UserAutomaticRequest - | InternalTacticRequest - | UserIndividualRequest - -(* Default definition entries, transparent with no secctx or proj information *) -val definition_entry : ?fix_exn:Future.fix_exn -> - ?opaque:bool -> ?inline:bool -> ?types:types -> - ?univs:Entries.universes_entry -> - ?eff:Safe_typing.private_constants -> constr -> Safe_typing.private_constants definition_entry - -(** [declare_constant id cd] declares a global declaration - (constant/parameter) with name [id] in the current section; it returns - the full path of the declaration - - internal specify if the constant has been created by the kernel or by the - user, and in the former case, if its errors should be silent *) -val declare_constant : - ?internal:internal_flag -> ?local:bool -> Id.t -> ?export_seff:bool -> constant_declaration -> Constant.t - -val declare_private_constant : - role:side_effect_role -> ?internal:internal_flag -> ?local:bool -> Id.t -> constant_declaration -> Constant.t * Safe_typing.private_constants - -val declare_definition : - ?internal:internal_flag -> ?opaque:bool -> ?kind:definition_object_kind -> - ?local:bool -> Id.t -> ?types:constr -> - constr Entries.in_universes_entry -> Constant.t - -(** Since transparent constants' side effects are globally declared, we - * need that *) -val set_declare_scheme : - (string -> (inductive * Constant.t) array -> unit) -> unit - -(** [declare_mind me] declares a block of inductive types with - their constructors in the current section; it returns the path of - the whole block and a boolean indicating if it is a primitive record. *) -val declare_mind : mutual_inductive_entry -> Libobject.object_name * bool - -(** Declaration messages *) - -val definition_message : Id.t -> unit -val assumption_message : Id.t -> unit -val fixpoint_message : int array option -> Id.t list -> unit -val cofixpoint_message : Id.t list -> unit -val recursive_message : bool (** true = fixpoint *) -> - int array option -> Id.t list -> unit - -val exists_name : Id.t -> bool - -(** Global universe contexts, names and constraints *) -val declare_univ_binders : GlobRef.t -> UnivNames.universe_binders -> unit - -val declare_universe_context : polymorphic -> Univ.ContextSet.t -> unit - -val do_universe : polymorphic -> lident list -> unit -val do_constraint : polymorphic -> (Glob_term.glob_level * Univ.constraint_type * Glob_term.glob_level) list -> - unit diff --git a/interp/deprecation.ml b/interp/deprecation.ml new file mode 100644 index 0000000000..3b02ba4664 --- /dev/null +++ b/interp/deprecation.ml @@ -0,0 +1,21 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <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 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +type t = { since : string option ; note : string option } + +let make ?since ?note () = { since ; note } + +let create_warning ~object_name ~warning_name name_printer = + let open Pp in + CWarnings.create ~name:warning_name ~category:"deprecated" + (fun (qid,depr) -> str object_name ++ spc () ++ name_printer qid ++ + strbrk " is deprecated" ++ + pr_opt (fun since -> str "since " ++ str since) depr.since ++ + str "." ++ pr_opt (fun note -> str note) depr.note) diff --git a/interp/deprecation.mli b/interp/deprecation.mli new file mode 100644 index 0000000000..f8083c2a5b --- /dev/null +++ b/interp/deprecation.mli @@ -0,0 +1,16 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <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 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +type t = { since : string option ; note : string option } + +val make : ?since:string -> ?note:string -> unit -> t + +val create_warning : object_name:string -> warning_name:string -> + ('b -> Pp.t) -> ?loc:Loc.t -> 'b * t -> unit diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml index a537b4848c..e1269025a4 100644 --- a/interp/dumpglob.ml +++ b/interp/dumpglob.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -91,7 +91,8 @@ let type_of_logical_kind = function (match a with | Definitional -> "defax" | Logical -> "prfax" - | Conjectural -> "prfax") + | Conjectural -> "prfax" + | Context -> "prfax") | IsProof th -> (match th with | Theorem diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli index 554da7603f..18955985a0 100644 --- a/interp/dumpglob.mli +++ b/interp/dumpglob.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/interp/genintern.ml b/interp/genintern.ml index 1b736b7977..e74f8d5f10 100644 --- a/interp/genintern.ml +++ b/interp/genintern.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/interp/genintern.mli b/interp/genintern.mli index 4100f39029..5619a7b648 100644 --- a/interp/genintern.mli +++ b/interp/genintern.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/interp/impargs.ml b/interp/impargs.ml index f3cdd64633..9977b29310 100644 --- a/interp/impargs.ml +++ b/interp/impargs.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -20,7 +20,6 @@ open Lib open Libobject open EConstr open Reductionops -open Constrexpr open Namegen module NamedDecl = Context.Named.Declaration @@ -341,77 +340,30 @@ let rec prepare_implicits f = function Some (id,imp,(set_maximality imps' f.maximal,true)) :: imps' | _::imps -> None :: prepare_implicits f imps -(* -If found, returns Some (x,(b,fi,fo)) and l with the entry removed, -otherwise returns None and l unchanged. - *) -let assoc_by_pos k l = - let rec aux = function - (ExplByPos (k', x), b) :: tl when Int.equal k k' -> Some (x,b), tl - | hd :: tl -> let (x, tl) = aux tl in x, hd :: tl - | [] -> raise Not_found - in try aux l with Not_found -> None, l - -let check_correct_manual_implicits autoimps l = - List.iter (function - | ExplByName id,(b,fi,forced) -> - if not forced then - user_err - (str "Wrong or non-dependent implicit argument name: " ++ Id.print id ++ str ".") - | ExplByPos (i,_id),_t -> - if i<1 || i>List.length autoimps then - user_err - (str "Bad implicit argument number: " ++ int i ++ str ".") - else - user_err - (str "Cannot set implicit argument number " ++ int i ++ - str ": it has no name.")) l - -(* Take a list l of explicitations, and map them to positions. *) -let flatten_explicitations l autoimps = - let rec aux k l = function - | (Name id,_)::imps -> - let value, l' = - try - let eq = Constrexpr_ops.explicitation_eq in - let flags = List.assoc_f eq (ExplByName id) l in - Some (Some id, flags), List.remove_assoc_f eq (ExplByName id) l - with Not_found -> assoc_by_pos k l - in value :: aux (k+1) l' imps - | (Anonymous,_)::imps -> - let value, l' = assoc_by_pos k l - in value :: aux (k+1) l' imps - | [] when List.is_empty l -> [] - | [] -> - check_correct_manual_implicits autoimps l; - [] - in aux 1 l autoimps - let set_manual_implicits flags enriching autoimps l = - if not (List.distinct l) then - user_err Pp.(str "Some parameters are referred more than once."); (* Compare with automatic implicits to recover printing data and names *) let rec merge k autoimps explimps = match autoimps, explimps with | autoimp::autoimps, explimp::explimps -> let imps' = merge (k+1) autoimps explimps in - begin match autoimp, explimp with - | (Name id,_), Some (_, (b, fi, _)) -> - Some (id, Manual, (set_maximality imps' b, fi)) + begin match autoimp, explimp.CAst.v with + | (Name id,_), Some (_,max) -> + Some (id, Manual, (set_maximality imps' max, true)) | (Name id,Some exp), None when enriching -> Some (id, exp, (set_maximality imps' flags.maximal, true)) | (Name _,_), None -> None - | (Anonymous,_), Some (Some id, (b, fi, true)) -> - Some (id,Manual,(b,fi)) - | (Anonymous,_), Some (None, (b, fi, true)) -> + | (Anonymous,_), Some (Name id,max) -> + Some (id,Manual,(max,true)) + | (Anonymous,_), Some (Anonymous,max) -> let id = Id.of_string ("arg_" ^ string_of_int k) in - Some (id,Manual,(b,fi)) - | (Anonymous,_), Some (_, (_, _, false)) -> None + Some (id,Manual,(max,true)) | (Anonymous,_), None -> None end :: imps' | [], [] -> [] - (* flatten_explicitations returns a list of the same length as autoimps *) - | _ -> assert false - in merge 1 autoimps (flatten_explicitations l autoimps) + | [], _ -> assert false + (* possibly more automatic than manual implicit arguments n + when the conclusion is an unfoldable constant *) + | autoimps, [] -> merge k autoimps [CAst.make None] + in merge 1 autoimps l let compute_semi_auto_implicits env sigma f t = if not f.auto then [DefaultImpArgs, []] @@ -642,9 +594,7 @@ let declare_mib_implicits kn = (inImplicits (ImplMutualInductive (kn,flags),List.flatten imps)) (* Declare manual implicits *) -type manual_explicitation = Constrexpr.explicitation * (bool * bool * bool) - -type manual_implicits = manual_explicitation list +type manual_implicits = (Name.t * bool) option CAst.t list let compute_implicits_with_manual env sigma typ enriching l = let autoimpls = compute_auto_implicits env sigma !implicit_args enriching typ in @@ -669,8 +619,6 @@ let projection_implicits env p impls = CList.skipn_at_least npars impls let declare_manual_implicits local ref ?enriching l = - assert (List.for_all (fun (_, (max, fi, fu)) -> fi && fu) l); - assert (List.for_all (fun (ex, _) -> match ex with ExplByPos (_,_) -> true | _ -> false) l); let flags = !implicit_args in let env = Global.env () in let sigma = Evd.from_env env in @@ -685,9 +633,8 @@ let declare_manual_implicits local ref ?enriching l = in add_anonymous_leaf (inImplicits (req,[ref,l])) let maybe_declare_manual_implicits local ref ?enriching l = - match l with - | [] -> () - | _ -> declare_manual_implicits local ref ?enriching l + if List.exists (fun x -> x.CAst.v <> None) l then + declare_manual_implicits local ref ?enriching l (* TODO: either turn these warnings on and document them, or handle these cases sensibly *) @@ -750,12 +697,6 @@ let extract_impargs_data impls = | [] -> [] in aux 0 impls -let lift_implicits n = - List.map (fun x -> - match fst x with - ExplByPos (k, id) -> ExplByPos (k + n, id), snd x - | _ -> x) - let make_implicits_list l = [DefaultImpArgs, l] let rec drop_first_implicits p l = diff --git a/interp/impargs.mli b/interp/impargs.mli index 1099074c63..90a7944642 100644 --- a/interp/impargs.mli +++ b/interp/impargs.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -84,13 +84,7 @@ val force_inference_of : implicit_status -> bool val positions_of_implicits : implicits_list -> int list -(** A [manual_explicitation] is a tuple of a positional or named explicitation with - maximal insertion, force inference and force usage flags. Forcing usage makes - the argument implicit even if the automatic inference considers it not inferable. *) -type manual_explicitation = Constrexpr.explicitation * - (maximal_insertion * force_inference * bool) - -type manual_implicits = manual_explicitation list +type manual_implicits = (Name.t * bool) option CAst.t list val compute_implicits_with_manual : env -> Evd.evar_map -> types -> bool -> manual_implicits -> implicit_status list @@ -131,8 +125,6 @@ val implicits_of_global : GlobRef.t -> implicits_list list val extract_impargs_data : implicits_list list -> ((int * int) option * implicit_status list) list -val lift_implicits : int -> manual_implicits -> manual_implicits - val make_implicits_list : implicit_status list -> implicits_list list val drop_first_implicits : int -> implicits_list -> implicits_list diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index bac46c2d2f..9f6281ae15 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -23,9 +23,6 @@ open Libobject open Nameops open Context.Rel.Declaration -exception MismatchedContextInstance of Environ.env * Typeclasses_errors.contexts * constr_expr list * Constr.rel_context (* found, expected *) -let mismatched_ctx_inst_err env c n m = raise (MismatchedContextInstance (env, c, n, m)) - module RelDecl = Context.Rel.Declaration (*i*) @@ -66,9 +63,6 @@ let declare_generalizable ~local gen = let find_generalizable_ident id = Id.Pred.mem (root_of_id id) !generalizable_table -let ids_of_list l = - List.fold_right Id.Set.add l Id.Set.empty - let is_global id = try ignore (Nametab.locate_extended (qualid_of_ident id)); true with Not_found -> false @@ -105,26 +99,6 @@ let free_vars_of_constr_expr c ?(bound=Id.Set.empty) l = | _ -> Constrexpr_ops.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux bdvars l c in aux bound l c -let ids_of_names l = - List.fold_left (fun acc x -> match x.CAst.v with Name na -> na :: acc | Anonymous -> acc) [] l - -let free_vars_of_binders ?(bound=Id.Set.empty) l (binders : local_binder_expr list) = - let rec aux bdvars l c = match c with - ((CLocalAssum (n, _, c)) :: tl) -> - let bound = ids_of_names n in - let l' = free_vars_of_constr_expr c ~bound:bdvars l in - aux (Id.Set.union (ids_of_list bound) bdvars) l' tl - - | ((CLocalDef (n, c, t)) :: tl) -> - let bound = match n.CAst.v with Anonymous -> [] | Name n -> [n] in - let l' = free_vars_of_constr_expr c ~bound:bdvars l in - let l'' = Option.fold_left (fun l t -> free_vars_of_constr_expr t ~bound:bdvars l) l' t in - aux (Id.Set.union (ids_of_list bound) bdvars) l'' tl - - | CLocalPattern _ :: tl -> assert false - | [] -> bdvars, l - in aux bound l binders - let generalizable_vars_of_glob_constr ?(bound=Id.Set.empty) ?(allowed=Id.Set.empty) = let rec vars bound vs c = match DAst.get c with | GVar id -> @@ -149,7 +123,7 @@ let next_name_away_from na avoid = | Anonymous -> make_fresh avoid (Global.env ()) (Id.of_string "anon") | Name id -> make_fresh avoid (Global.env ()) id -let combine_params avoid fn applied needed = +let combine_params avoid applied needed = let named, applied = List.partition (function @@ -167,47 +141,30 @@ let combine_params avoid fn applied needed = (fun x -> match x with (t, Some {CAst.loc;v=ExplByName id}) -> id, t | _ -> assert false) named in - let is_unset (_, decl) = match decl with - | LocalAssum _ -> true - | LocalDef _ -> false - in - let needed = List.filter is_unset needed in let rec aux ids avoid app need = match app, need with - [], [] -> List.rev ids, avoid - | app, (_, (LocalAssum ({binder_name=Name id}, _) | LocalDef ({binder_name=Name id}, _, _))) :: need when Id.List.mem_assoc id named -> + | _, (_, LocalDef _) :: need -> aux ids avoid app need + + | [], [] -> List.rev ids, avoid + + | app, (_, (LocalAssum ({binder_name=Name id}, _))) :: need when Id.List.mem_assoc id named -> aux (Id.List.assoc id named :: ids) avoid app need - | (x, None) :: app, (None, (LocalAssum ({binder_name=Name id}, _) | LocalDef ({binder_name=Name id}, _, _))) :: need -> + | (x, None) :: app, (None, (LocalAssum ({binder_name=Name id}, _))) :: need -> aux (x :: ids) avoid app need - | _, (Some cl, _ as d) :: need -> - let t', avoid' = fn avoid d in - aux (t' :: ids) avoid' app need - | x :: app, (None, _) :: need -> aux (fst x :: ids) avoid app need - | [], (None, _ as decl) :: need -> - let t', avoid' = fn avoid decl in - aux (t' :: ids) avoid' app need + | _, (Some _, decl) :: need | [], (None, decl) :: need -> + let id' = next_name_away_from (RelDecl.get_name decl) avoid in + let t' = CAst.make @@ CRef (qualid_of_ident id',None) in + aux (t' :: ids) (Id.Set.add id' avoid) app need | (x,_) :: _, [] -> user_err ?loc:(Constrexpr_ops.constr_loc x) (str "Typeclass does not expect more arguments") - in aux [] avoid applied needed - -let combine_params_freevar avoid (_, decl) = - let id' = next_name_away_from (RelDecl.get_name decl) avoid in - (CAst.make @@ CRef (qualid_of_ident id',None), Id.Set.add id' avoid) - -let destClassApp cl = - let open CAst in - let loc = cl.loc in - match cl.v with - | CApp ((None, { v = CRef (ref, inst) }), l) -> CAst.make ?loc (ref, List.map fst l, inst) - | CAppExpl ((None, ref, inst), l) -> CAst.make ?loc (ref, l, inst) - | CRef (ref, inst) -> CAst.make ?loc:cl.loc (ref, [], inst) - | _ -> raise Not_found + in + aux [] avoid applied needed let destClassAppExpl cl = let open CAst in @@ -217,7 +174,7 @@ let destClassAppExpl cl = | CRef (ref, inst) -> CAst.make ?loc:cl.loc (ref, [], inst) | _ -> raise Not_found -let implicit_application env ?(allow_partial=true) f ty = +let implicit_application env ty = let is_class = try let ({CAst.v=(qid, _, _)} as clapp) = destClassAppExpl ty in @@ -230,24 +187,13 @@ let implicit_application env ?(allow_partial=true) f ty = match is_class with | None -> ty, env | Some ({CAst.loc;v=(id, par, inst)}, gr) -> - let avoid = Id.Set.union env (ids_of_list (free_vars_of_constr_expr ty ~bound:env [])) in + let avoid = Id.Set.union env (Id.Set.of_list (free_vars_of_constr_expr ty ~bound:env [])) in let env = Global.env () in let sigma = Evd.from_env env in let c = class_info env sigma gr in let (ci, rd) = c.cl_context in - if not allow_partial then - begin - let opt_succ x n = match x with - | None -> succ n - | Some _ -> n - in - let applen = List.fold_left (fun acc (x, y) -> opt_succ y acc) 0 par in - let needlen = List.fold_left (fun acc x -> opt_succ x acc) 0 ci in - if not (Int.equal needlen applen) then - mismatched_ctx_inst_err (Global.env ()) Typeclasses_errors.Parameters (List.map fst par) rd - end; let pars = List.rev (List.combine ci rd) in - let args, avoid = combine_params avoid f par pars in + let args, avoid = combine_params avoid par pars in CAst.make ?loc @@ CAppExpl ((None, id, inst), args), avoid let warn_ignoring_implicit_status = @@ -257,32 +203,23 @@ let warn_ignoring_implicit_status = Name.print na ++ strbrk " and following binders") let implicits_of_glob_constr ?(with_products=true) l = - let add_impl i na bk l = match bk with - | Implicit -> - let name = - match na with - | Name id -> Some id - | Anonymous -> None - in - (ExplByPos (i, name), (true, true, true)) :: l - | _ -> l + let add_impl ?loc na bk l = match bk with + | Implicit -> CAst.make ?loc (Some (na,true)) :: l + | _ -> CAst.make ?loc None :: l in - let rec aux i c = - let abs na bk b = - add_impl i na bk (aux (succ i) b) - in + let rec aux c = match DAst.get c with | GProd (na, bk, t, b) -> - if with_products then abs na bk b + if with_products then add_impl na bk (aux b) else let () = match bk with | Implicit -> warn_ignoring_implicit_status na ?loc:c.CAst.loc | _ -> () in [] - | GLambda (na, bk, t, b) -> abs na bk b - | GLetIn (na, b, t, c) -> aux i c + | GLambda (na, bk, t, b) -> add_impl ?loc:t.CAst.loc na bk (aux b) + | GLetIn (na, b, t, c) -> aux c | GRec (fix_kind, nas, args, tys, bds) -> let nb = match fix_kind with |GFix (_, n) -> n | GCoFix n -> n in - List.fold_left_i (fun i l (na,bk,_,_) -> add_impl i na bk l) i (aux (List.length args.(nb) + i) bds.(nb)) args.(nb) + List.fold_right (fun (na,bk,t,_) l -> add_impl ?loc:c.CAst.loc na bk l) args.(nb) (aux bds.(nb)) | _ -> [] - in aux 1 l + in aux l diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli index 437fef1753..4f9c47ec36 100644 --- a/interp/implicit_quantifiers.mli +++ b/interp/implicit_quantifiers.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -11,22 +11,14 @@ open Names open Glob_term open Constrexpr -open Libnames val declare_generalizable : local:bool -> lident list option -> unit -val ids_of_list : Id.t list -> Id.Set.t -val destClassApp : constr_expr -> (qualid * constr_expr list * instance_expr option) CAst.t -val destClassAppExpl : constr_expr -> (qualid * (constr_expr * explicitation CAst.t option) list * instance_expr option) CAst.t - (** Fragile, should be used only for construction a set of identifiers to avoid *) val free_vars_of_constr_expr : constr_expr -> ?bound:Id.Set.t -> Id.t list -> Id.t list -val free_vars_of_binders : - ?bound:Id.Set.t -> Id.t list -> local_binder_expr list -> Id.Set.t * Id.t list - (** Returns the generalizable free ids in left-to-right order with the location of their first occurrence *) @@ -37,15 +29,4 @@ val make_fresh : Id.Set.t -> Environ.env -> Id.t -> Id.t val implicits_of_glob_constr : ?with_products:bool -> Glob_term.glob_constr -> Impargs.manual_implicits -val combine_params_freevar : - Id.Set.t -> GlobRef.t option * Constr.rel_declaration -> - Constrexpr.constr_expr * Id.Set.t - -val implicit_application : Id.Set.t -> ?allow_partial:bool -> - (Id.Set.t -> GlobRef.t option * Constr.rel_declaration -> - Constrexpr.constr_expr * Id.Set.t) -> - constr_expr -> constr_expr * Id.Set.t - -(* Should be likely located elsewhere *) -exception MismatchedContextInstance of Environ.env * Typeclasses_errors.contexts * constr_expr list * Constr.rel_context (* found, expected *) -val mismatched_ctx_inst_err : Environ.env -> Typeclasses_errors.contexts -> constr_expr list -> Constr.rel_context -> 'a +val implicit_application : Id.Set.t -> constr_expr -> constr_expr * Id.Set.t diff --git a/interp/interp.mllib b/interp/interp.mllib index b65a171ef9..33573edcce 100644 --- a/interp/interp.mllib +++ b/interp/interp.mllib @@ -1,3 +1,4 @@ +Deprecation NumTok Constrexpr Tactypes @@ -16,4 +17,3 @@ Implicit_quantifiers Constrintern Modintern Constrextern -Declare diff --git a/interp/modintern.ml b/interp/modintern.ml index 2f516f4f3c..955288244e 100644 --- a/interp/modintern.ml +++ b/interp/modintern.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/interp/modintern.mli b/interp/modintern.mli index 529c438c1a..75ab38c64a 100644 --- a/interp/modintern.mli +++ b/interp/modintern.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/interp/notation.ml b/interp/notation.ml index a7bac96d31..d58125e29b 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -72,6 +72,7 @@ type notation_location = (DirPath.t * DirPath.t) * string type notation_data = { not_interp : interpretation; not_location : notation_location; + not_deprecation : Deprecation.t option; } type scope = { @@ -1095,7 +1096,7 @@ let warn_notation_overridden = str "Notation" ++ spc () ++ pr_notation ntn ++ spc () ++ strbrk "was already used" ++ which_scope ++ str ".") -let declare_notation_interpretation ntn scopt pat df ~onlyprint = +let declare_notation_interpretation ntn scopt pat df ~onlyprint deprecation = let scope = match scopt with Some s -> s | None -> default_scope in let sc = find_scope scope in if not onlyprint then begin @@ -1109,6 +1110,7 @@ let declare_notation_interpretation ntn scopt pat df ~onlyprint = let notdata = { not_interp = pat; not_location = df; + not_deprecation = deprecation; } in let sc = { sc with notations = NotationMap.add ntn notdata sc.notations } in scope_map := String.Map.add scope sc !scope_map @@ -1125,10 +1127,10 @@ let declare_uninterpretation rule (metas,c as pat) = let rec find_interpretation ntn find = function | [] -> raise Not_found | Scope scope :: scopes -> - (try let (pat,df) = find scope in pat,(df,Some scope) + (try let n = find scope in (n,Some scope) with Not_found -> find_interpretation ntn find scopes) | SingleNotation ntn'::scopes when notation_eq ntn' ntn -> - (try let (pat,df) = find default_scope in pat,(df,None) + (try let n = find default_scope in (n,None) with Not_found -> (* e.g. because single notation only for constr, not cases_pattern *) find_interpretation ntn find scopes) @@ -1136,8 +1138,7 @@ let rec find_interpretation ntn find = function find_interpretation ntn find scopes let find_notation ntn sc = - let n = NotationMap.find ntn (find_scope sc).notations in - (n.not_interp, n.not_location) + NotationMap.find ntn (find_scope sc).notations let notation_of_prim_token = function | Numeral (SPlus,n) -> InConstrEntrySomeLevel, NumTok.to_string n @@ -1147,7 +1148,9 @@ let notation_of_prim_token = function let find_prim_token check_allowed ?loc p sc = (* Try for a user-defined numerical notation *) try - let (_,c),df = find_notation (notation_of_prim_token p) sc in + let n = find_notation (notation_of_prim_token p) sc in + let (_,c) = n.not_interp in + let df = n.not_location in let pat = Notation_ops.glob_constr_of_notation_constr ?loc c in check_allowed pat; pat, df @@ -1167,7 +1170,9 @@ let find_prim_token check_allowed ?loc p sc = let interp_prim_token_gen ?loc g p local_scopes = let scopes = make_current_scopes local_scopes in let p_as_ntn = try notation_of_prim_token p with Not_found -> InConstrEntrySomeLevel,"" in - try find_interpretation p_as_ntn (find_prim_token ?loc g p) scopes + try + let (pat,loc), sc = find_interpretation p_as_ntn (find_prim_token ?loc g p) scopes in + pat, (loc,sc) with Not_found -> user_err ?loc ~hdr:"interp_prim_token" ((match p with @@ -1192,11 +1197,18 @@ let rec check_allowed_ref_in_pat looked_for = DAst.(with_val (function let interp_prim_token_cases_pattern_expr ?loc looked_for p = interp_prim_token_gen ?loc (check_allowed_ref_in_pat looked_for) p +let warn_deprecated_notation = + Deprecation.create_warning ~object_name:"Notation" ~warning_name:"deprecated-notation" + pr_notation + let interp_notation ?loc ntn local_scopes = let scopes = make_current_scopes local_scopes in - try find_interpretation ntn (find_notation ntn) scopes + try + let (n,sc) = find_interpretation ntn (find_notation ntn) scopes in + Option.iter (fun d -> warn_deprecated_notation (ntn,d)) n.not_deprecation; + n.not_interp, (n.not_location, sc) with Not_found -> - user_err ?loc + user_err ?loc (str "Unknown interpretation for notation " ++ pr_notation ntn ++ str ".") let uninterp_notations c = diff --git a/interp/notation.mli b/interp/notation.mli index a67948a778..bd9b50977b 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -217,7 +217,8 @@ type interp_rule = | SynDefRule of KerName.t val declare_notation_interpretation : notation -> scope_name option -> - interpretation -> notation_location -> onlyprint:bool -> unit + interpretation -> notation_location -> onlyprint:bool -> + Deprecation.t option -> unit val declare_uninterpretation : interp_rule -> interpretation -> unit diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 7f084fffdd..fdf12faa04 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -1190,7 +1190,11 @@ let rec match_ inner u alp metas sigma a1 a2 = Array.fold_left2 (match_in u alp metas) sigma bl1 bl2 | GCast(t1, c1), NCast(t2, c2) -> match_cast (match_in u alp metas) (match_in u alp metas sigma t1 t2) c1 c2 - | GSort (GType _), NSort (GType _) when not u -> sigma + + (* Next pair of lines useful only if not coming from detyping *) + | GSort (UNamed [(GProp|GSet),0]), NSort (UAnonymous _) -> raise No_match + | GSort _, NSort (UAnonymous _) when not u -> sigma + | GSort s1, NSort s2 when glob_sort_eq s1 s2 -> sigma | GInt i1, NInt i2 when Uint63.equal i1 i2 -> sigma | GPatVar _, NHole _ -> (*Don't hide Metas, they bind in ltac*) raise No_match diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli index 58fa221b16..7919d0061f 100644 --- a/interp/notation_ops.mli +++ b/interp/notation_ops.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/interp/notation_term.ml b/interp/notation_term.ml index 5024f5c26f..908455bd05 100644 --- a/interp/notation_term.ml +++ b/interp/notation_term.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/interp/reserve.ml b/interp/reserve.ml index edbdf1dbba..e81439c3d5 100644 --- a/interp/reserve.ml +++ b/interp/reserve.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/interp/reserve.mli b/interp/reserve.mli index a10858e71f..e180fc8071 100644 --- a/interp/reserve.mli +++ b/interp/reserve.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml index 91491bdf8d..74fe5d1c80 100644 --- a/interp/smartlocate.ml +++ b/interp/smartlocate.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/interp/smartlocate.mli b/interp/smartlocate.mli index e41ef78913..d2770a2e73 100644 --- a/interp/smartlocate.mli +++ b/interp/smartlocate.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/interp/stdarg.ml b/interp/stdarg.ml index bf3a8fe215..555eb34aed 100644 --- a/interp/stdarg.ml +++ b/interp/stdarg.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/interp/stdarg.mli b/interp/stdarg.mli index c974a4403c..dffbca0054 100644 --- a/interp/stdarg.mli +++ b/interp/stdarg.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index a7e1de736c..302bb6ece2 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -19,20 +19,24 @@ open Notation_term (* Syntactic definitions. *) -type version = Flags.compat_version option +type syndef = + { syndef_pattern : interpretation; + syndef_onlyparsing : bool; + syndef_deprecation : Deprecation.t option; + } let syntax_table = - Summary.ref (KNmap.empty : (interpretation*version) KNmap.t) - ~name:"SYNTAXCONSTANT" + Summary.ref (KNmap.empty : syndef KNmap.t) + ~name:"SYNDEFS" -let add_syntax_constant kn c onlyparse = - syntax_table := KNmap.add kn (c,onlyparse) !syntax_table +let add_syntax_constant kn syndef = + syntax_table := KNmap.add kn syndef !syntax_table -let load_syntax_constant i ((sp,kn),(_,pat,onlyparse)) = +let load_syntax_constant i ((sp,kn),(_local,syndef)) = if Nametab.exists_cci sp then user_err ~hdr:"cache_syntax_constant" (Id.print (basename sp) ++ str " already exists"); - add_syntax_constant kn pat onlyparse; + add_syntax_constant kn syndef; Nametab.push_syndef (Nametab.Until i) sp kn let is_alias_of_already_visible_name sp = function @@ -42,30 +46,29 @@ let is_alias_of_already_visible_name sp = function | _ -> false -let open_syntax_constant i ((sp,kn),(_,pat,onlyparse)) = +let open_syntax_constant i ((sp,kn),(_local,syndef)) = + let pat = syndef.syndef_pattern in if not (Int.equal i 1 && is_alias_of_already_visible_name sp pat) then begin Nametab.push_syndef (Nametab.Exactly i) sp kn; - match onlyparse with - | None -> + if not syndef.syndef_onlyparsing then (* Redeclare it to be used as (short) name in case an other (distfix) notation was declared in between *) Notation.declare_uninterpretation (Notation.SynDefRule kn) pat - | _ -> () end let cache_syntax_constant d = load_syntax_constant 1 d; open_syntax_constant 1 d -let subst_syntax_constant (subst,(local,pat,onlyparse)) = - (local,Notation_ops.subst_interpretation subst pat,onlyparse) +let subst_syntax_constant (subst,(local,syndef)) = + let syndef_pattern = Notation_ops.subst_interpretation subst syndef.syndef_pattern in + (local, { syndef with syndef_pattern }) -let classify_syntax_constant (local,_,_ as o) = +let classify_syntax_constant (local,_ as o) = if local then Dispose else Substitute o -let in_syntax_constant - : bool * interpretation * Flags.compat_version option -> obj = - declare_object {(default_object "SYNTAXCONSTANT") with +let in_syntax_constant : (bool * syndef) -> obj = + declare_object {(default_object "SYNDEF") with cache_function = cache_syntax_constant; load_function = load_syntax_constant; open_function = open_syntax_constant; @@ -79,36 +82,31 @@ type syndef_interpretation = (Id.t * subscopes) list * notation_constr let in_pat (ids,ac) = (List.map (fun (id,sc) -> (id,((Constrexpr.InConstrEntrySomeLevel,sc),NtnTypeConstr))) ids,ac) let out_pat (ids,ac) = (List.map (fun (id,((_,sc),typ)) -> (id,sc)) ids,ac) -let declare_syntactic_definition local id onlyparse pat = - let _ = add_leaf id (in_syntax_constant (local,in_pat pat,onlyparse)) in () - -let pr_syndef kn = pr_qualid (Nametab.shortest_qualid_of_syndef Id.Set.empty kn) - -let pr_compat_warning (kn, def, v) = - let pp_def = match def with - | [], NRef r -> spc () ++ str "is" ++ spc () ++ Nametab.pr_global_env Id.Set.empty r - | _ -> strbrk " is a compatibility notation" +let declare_syntactic_definition ~local deprecation id ~onlyparsing pat = + let syndef = + { syndef_pattern = in_pat pat; + syndef_onlyparsing = onlyparsing; + syndef_deprecation = deprecation; + } in - pr_syndef kn ++ pp_def + let _ = add_leaf id (in_syntax_constant (local,syndef)) in () -let warn_compatibility_notation = - CWarnings.(create ~name:"compatibility-notation" - ~category:"deprecated" ~default:Enabled pr_compat_warning) +let pr_syndef kn = pr_qualid (Nametab.shortest_qualid_of_syndef Id.Set.empty kn) -let verbose_compat ?loc kn def = function - | Some v when Flags.version_strictly_greater v -> - warn_compatibility_notation ?loc (kn, def, v) - | _ -> () +let warn_deprecated_syntactic_definition = + Deprecation.create_warning ~object_name:"Notation" ~warning_name:"deprecated-syntactic-definition" + pr_syndef let search_syntactic_definition ?loc kn = - let pat,v = KNmap.find kn !syntax_table in - let def = out_pat pat in - verbose_compat ?loc kn def v; + let syndef = KNmap.find kn !syntax_table in + let def = out_pat syndef.syndef_pattern in + Option.iter (fun d -> warn_deprecated_syntactic_definition (kn,d)) syndef.syndef_deprecation; def let search_filtered_syntactic_definition ?loc filter kn = - let pat,v = KNmap.find kn !syntax_table in - let def = out_pat pat in + let syndef = KNmap.find kn !syntax_table in + let def = out_pat syndef.syndef_pattern in let res = filter def in - (match res with Some _ -> verbose_compat ?loc kn def v | None -> ()); + if Option.has_some res then + Option.iter (fun d -> warn_deprecated_syntactic_definition (kn,d)) syndef.syndef_deprecation; res diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli index 77873f8f67..0065b45b14 100644 --- a/interp/syntax_def.mli +++ b/interp/syntax_def.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -15,8 +15,8 @@ open Notation_term type syndef_interpretation = (Id.t * subscopes) list * notation_constr -val declare_syntactic_definition : bool -> Id.t -> - Flags.compat_version option -> syndef_interpretation -> unit +val declare_syntactic_definition : local:bool -> Deprecation.t option -> Id.t -> + onlyparsing:bool -> syndef_interpretation -> unit val search_syntactic_definition : ?loc:Loc.t -> KerName.t -> syndef_interpretation |