aboutsummaryrefslogtreecommitdiff
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/assumptions.ml6
-rw-r--r--vernac/auto_ind_decl.ml8
-rw-r--r--vernac/comInductive.ml124
-rw-r--r--vernac/comInductive.mli14
-rw-r--r--vernac/declareObl.ml2
-rw-r--r--vernac/library.ml651
-rw-r--r--vernac/library.mli81
-rw-r--r--vernac/obligations.ml2
-rw-r--r--vernac/record.ml85
-rw-r--r--vernac/vernac.mllib1
-rw-r--r--vernac/vernacentries.ml34
11 files changed, 917 insertions, 91 deletions
diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml
index a72e43de01..cb034bdff6 100644
--- a/vernac/assumptions.ml
+++ b/vernac/assumptions.ml
@@ -353,6 +353,8 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t =
let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in
ContextObjectMap.add (Axiom (TypeInType obj, l)) Constr.mkProp accu
in
- accu
-
+ if not mind.mind_typing_flags.check_template then
+ let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in
+ ContextObjectMap.add (Axiom (TemplatePolymorphic m, l)) Constr.mkProp accu
+ else accu
in GlobRef.Map_env.fold fold graph ContextObjectMap.empty
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index d414d57c0d..98fe436a22 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -345,7 +345,7 @@ let build_beq_scheme mode kn =
Vars.substl subst cores.(i)
in
create_input fix),
- UState.make (Global.universes ())),
+ UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ())),
!eff
let beq_scheme_kind = declare_mutual_scheme_object "_beq" build_beq_scheme
@@ -690,7 +690,7 @@ let make_bl_scheme mode mind =
let lnonparrec,lnamesparrec = (* TODO subst *)
context_chop (nparams-nparrec) mib.mind_params_ctxt in
let bl_goal, eff = compute_bl_goal ind lnamesparrec nparrec in
- let ctx = UState.make (Global.universes ()) in
+ let ctx = UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()) in
let side_eff = side_effect_of_mode mode in
let bl_goal = EConstr.of_constr bl_goal in
let (ans, _, ctx) = Pfedit.build_by_tactic ~poly:false ~side_eff (Global.env()) ctx bl_goal
@@ -820,7 +820,7 @@ let make_lb_scheme mode mind =
let lnonparrec,lnamesparrec =
context_chop (nparams-nparrec) mib.mind_params_ctxt in
let lb_goal, eff = compute_lb_goal ind lnamesparrec nparrec in
- let ctx = UState.make (Global.universes ()) in
+ let ctx = UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()) in
let side_eff = side_effect_of_mode mode in
let lb_goal = EConstr.of_constr lb_goal in
let (ans, _, ctx) = Pfedit.build_by_tactic ~poly:false ~side_eff (Global.env()) ctx lb_goal
@@ -996,7 +996,7 @@ let make_eq_decidability mode mind =
let nparams = mib.mind_nparams in
let nparrec = mib.mind_nparams_rec in
let u = Univ.Instance.empty in
- let ctx = UState.make (Global.universes ()) in
+ let ctx = UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()) in
let lnonparrec,lnamesparrec =
context_chop (nparams-nparrec) mib.mind_params_ctxt in
let side_eff = side_effect_of_mode mode in
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index adbe196699..98b869d72e 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -114,20 +114,22 @@ let mk_mltype_data sigma env assums arity indname =
inductives which are recognized when a "Type" appears at the end of the conlusion in
the source syntax. *)
-let rec check_anonymous_type ind =
+let rec check_type_conclusion ind =
let open Glob_term in
match DAst.get ind with
- | GSort (UAnonymous {rigid=true}) -> true
+ | GSort (UAnonymous {rigid=true}) -> (Some true)
+ | GSort (UNamed _) -> (Some false)
| GProd ( _, _, _, e)
| GLetIn (_, _, _, e)
| GLambda (_, _, _, e)
| GApp (e, _)
- | GCast (e, _) -> check_anonymous_type e
- | _ -> false
+ | GCast (e, _) -> check_type_conclusion e
+ | _ -> None
-let make_conclusion_flexible sigma = function
+let make_anonymous_conclusion_flexible sigma = function
| None -> sigma
- | Some s ->
+ | Some (false, _) -> sigma
+ | Some (true, s) ->
(match EConstr.ESorts.kind sigma s with
| Type u ->
(match Univ.universe_level u with
@@ -136,17 +138,23 @@ let make_conclusion_flexible sigma = function
| None -> sigma)
| _ -> sigma)
-let interp_ind_arity env sigma ind =
+let intern_ind_arity env sigma ind =
let c = intern_gen IsType env sigma ind.ind_arity in
let impls = Implicit_quantifiers.implicits_of_glob_constr ~with_products:true c in
+ let pseudo_poly = check_type_conclusion c in
+ (constr_loc ind.ind_arity, c, impls, pseudo_poly)
+
+let pretype_ind_arity env sigma (loc, c, impls, pseudo_poly) =
let sigma,t = understand_tcc env sigma ~expected_type:IsType c in
- let pseudo_poly = check_anonymous_type c in
match Reductionops.sort_of_arity env sigma t with
| exception Invalid_argument _ ->
- user_err ?loc:(constr_loc ind.ind_arity) (str "Not an arity")
+ user_err ?loc (str "Not an arity")
| s ->
- let concl = if pseudo_poly then Some s else None in
- sigma, (t, Retyping.relevance_of_sort s, concl, impls)
+ let concl = match pseudo_poly with
+ | Some b -> Some (b, s)
+ | None -> None
+ in
+ sigma, (t, Retyping.relevance_of_sort s, concl, impls)
let interp_cstrs env sigma impls mldata arity ind =
let cnames,ctyps = List.split ind.ind_lc in
@@ -251,7 +259,7 @@ let solve_constraints_system levels level_bounds =
done;
v
-let inductive_levels env evd poly arities inds =
+let inductive_levels env evd arities inds =
let destarities = List.map (fun x -> x, Reduction.dest_arity env x) arities in
let levels = List.map (fun (x,(ctx,a)) ->
if Sorts.is_prop a || Sorts.is_sprop a then None
@@ -286,7 +294,7 @@ let inductive_levels env evd poly arities inds =
CList.fold_left3 (fun (evd, arities) cu (arity,(ctx,du)) len ->
if is_impredicative_sort env du then
(* Any product is allowed here. *)
- evd, arity :: arities
+ evd, (false, arity) :: arities
else (* If in a predicative sort, or asked to infer the type,
we take the max of:
- indices (if in indices-matter mode)
@@ -300,7 +308,6 @@ let inductive_levels env evd poly arities inds =
raise (InductiveError LargeNonPropInductiveNotInType)
else evd
else evd
- (* Evd.set_leq_sort env evd (Type cu) du *)
in
let evd =
if len >= 2 && Univ.is_type0m_univ cu then
@@ -311,14 +318,14 @@ let inductive_levels env evd poly arities inds =
else evd
in
let duu = Sorts.univ_of_sort du in
- let evd =
+ let template_prop, evd =
if not (Univ.is_small_univ duu) && Univ.Universe.equal cu duu then
if is_flexible_sort evd duu && not (Evd.check_leq evd Univ.type0_univ duu) then
- Evd.set_eq_sort env evd Sorts.prop du
- else evd
- else Evd.set_eq_sort env evd (sort_of_univ cu) du
+ true, Evd.set_eq_sort env evd Sorts.prop du
+ else false, evd
+ else false, Evd.set_eq_sort env evd (sort_of_univ cu) du
in
- (evd, arity :: arities))
+ (evd, (template_prop, arity) :: arities))
(evd,[]) (Array.to_list levels') destarities sizes
in evd, List.rev arities
@@ -328,6 +335,17 @@ let check_named {CAst.loc;v=na} = match na with
let msg = str "Parameters must be named." in
user_err ?loc msg
+let template_polymorphism_candidate env uctx params concl =
+ match uctx with
+ | Entries.Monomorphic_entry uctx ->
+ let concltemplate = Option.cata (fun s -> not (Sorts.is_small s)) false concl in
+ if not concltemplate then false
+ else
+ let template_check = Environ.check_template env in
+ let conclu = Option.cata Sorts.univ_of_sort Univ.type0m_univ concl in
+ let params, conclunivs = IndTyping.template_polymorphic_univs ~template_check uctx params conclu in
+ not (template_check && Univ.LSet.is_empty conclunivs)
+ | Entries.Polymorphic_entry _ -> false
let check_param = function
| CLocalDef (na, _, _) -> check_named na
@@ -345,25 +363,46 @@ let restrict_inductive_universes sigma ctx_params arities constructors =
let uvars = List.fold_right (fun (_,ctypes,_) -> List.fold_right merge_universes_of_constr ctypes) constructors uvars in
Evd.restrict_universe_context sigma uvars
-let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) notations ~cumulative ~poly ~private_ind finite =
- check_all_names_different indl;
- List.iter check_param paramsl;
- if not (List.is_empty uparamsl) && not (List.is_empty notations)
- then user_err (str "Inductives with uniform parameters may not have attached notations.");
- let sigma, udecl = interp_univ_decl_opt env0 udecl in
+let interp_params env udecl uparamsl paramsl =
+ let sigma, udecl = interp_univ_decl_opt env udecl in
let sigma, (uimpls, ((env_uparams, ctx_uparams), useruimpls)) =
- interp_context_evars ~program_mode:false env0 sigma uparamsl in
+ interp_context_evars ~program_mode:false env sigma uparamsl in
let sigma, (impls, ((env_params, ctx_params), userimpls)) =
interp_context_evars ~program_mode:false ~impl_env:uimpls env_uparams sigma paramsl
in
- let indnames = List.map (fun ind -> ind.ind_name) indl in
-
(* Names of parameters as arguments of the inductive type (defs removed) *)
let assums = List.filter is_local_assum ctx_params in
- let params = List.map (RelDecl.get_name %> Name.get_id) assums in
+ sigma, env_params, (ctx_params, env_uparams, ctx_uparams,
+ List.map (RelDecl.get_name %> Name.get_id) assums, userimpls, useruimpls, impls, udecl)
+
+let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) notations ~cumulative ~poly ~private_ind finite =
+ check_all_names_different indl;
+ List.iter check_param paramsl;
+ if not (List.is_empty uparamsl) && not (List.is_empty notations)
+ then user_err (str "Inductives with uniform parameters may not have attached notations.");
+
+ let indnames = List.map (fun ind -> ind.ind_name) indl in
+ let sigma, env_params, infos =
+ interp_params env0 udecl uparamsl paramsl
+ in
(* Interpret the arities *)
- let sigma, arities = List.fold_left_map (fun sigma -> interp_ind_arity env_params sigma) sigma indl in
+ let arities = List.map (intern_ind_arity env_params sigma) indl in
+
+ let sigma, env_params, (ctx_params, env_uparams, ctx_uparams, params, userimpls, useruimpls, impls, udecl), arities, is_template =
+ let is_template = List.exists (fun (_,_,_,pseudo_poly) -> not (Option.is_empty pseudo_poly)) arities in
+ if not poly && is_template then
+ (* In case of template polymorphism, we need to compute more constraints *)
+ let env0 = Environ.set_universes_lbound env0 Univ.Level.prop in
+ let sigma, env_params, infos =
+ interp_params env0 udecl uparamsl paramsl
+ in
+ let arities = List.map (intern_ind_arity env_params sigma) indl in
+ sigma, env_params, infos, arities, is_template
+ else sigma, env_params, infos, arities, is_template
+ in
+
+ let sigma, arities = List.fold_left_map (pretype_ind_arity env_params) sigma arities in
let arities, relevances, arityconcl, indimpls = List.split4 arities in
let fullarities = List.map (fun c -> EConstr.it_mkProd_or_LetIn c ctx_params) arities in
@@ -410,31 +449,36 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not
let nf = Evarutil.nf_evars_universes sigma in
let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf cl,impsl)) constructors in
let arities = List.map EConstr.(to_constr sigma) arities in
- let sigma = List.fold_left make_conclusion_flexible sigma arityconcl in
- let sigma, arities = inductive_levels env_ar_params sigma poly arities constructors in
+ let sigma = List.fold_left make_anonymous_conclusion_flexible sigma arityconcl in
+ let sigma, arities = inductive_levels env_ar_params sigma arities constructors in
let sigma = Evd.minimize_universes sigma in
let nf = Evarutil.nf_evars_universes sigma in
- let arities = List.map nf arities in
+ let arities = List.map (fun (template, arity) -> template, nf arity) arities in
let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf cl,impsl)) constructors in
let ctx_params = List.map Termops.(map_rel_decl (EConstr.to_constr sigma)) ctx_params in
- let arityconcl = List.map (Option.map (EConstr.ESorts.kind sigma)) arityconcl in
- let sigma = restrict_inductive_universes sigma ctx_params arities constructors in
+ let arityconcl = List.map (Option.map (fun (anon, s) -> EConstr.ESorts.kind sigma s)) arityconcl in
+ let sigma = restrict_inductive_universes sigma ctx_params (List.map snd arities) constructors in
let uctx = Evd.check_univ_decl ~poly sigma udecl in
- List.iter (fun c -> check_evars env_params (Evd.from_env env_params) sigma (EConstr.of_constr c)) arities;
+ List.iter (fun c -> check_evars env_params (Evd.from_env env_params) sigma (EConstr.of_constr (snd c))) arities;
Context.Rel.iter (fun c -> check_evars env0 (Evd.from_env env0) sigma (EConstr.of_constr c)) ctx_params;
List.iter (fun (_,ctyps,_) ->
List.iter (fun c -> check_evars env_ar_params (Evd.from_env env_ar_params) sigma (EConstr.of_constr c)) ctyps)
constructors;
(* Build the inductive entries *)
- let entries = List.map4 (fun ind arity concl (cnames,ctypes,cimpls) ->
+ let entries = List.map4 (fun ind (templatearity, arity) concl (cnames,ctypes,cimpls) ->
+ let template_candidate () =
+ templatearity || template_polymorphism_candidate env0 uctx ctx_params concl in
let template = match template with
| Some template ->
- if poly && template then user_err Pp.(strbrk "template and polymorphism not compatible");
+ if poly && template then user_err
+ Pp.(strbrk "Template-polymorphism and universe polymorphism are not compatible.");
+ if template && not (template_candidate ()) then
+ user_err Pp.(strbrk "Inductive " ++ Id.print ind.ind_name ++
+ str" cannot be made template polymorphic.");
template
| None ->
- should_auto_template ind.ind_name (not poly &&
- Option.cata (fun s -> not (Sorts.is_small s)) false concl)
+ should_auto_template ind.ind_name (template_candidate ())
in
{ mind_entry_typename = ind.ind_name;
mind_entry_arity = arity;
diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli
index 285be8cd51..7587bd165f 100644
--- a/vernac/comInductive.mli
+++ b/vernac/comInductive.mli
@@ -62,3 +62,17 @@ val should_auto_template : Id.t -> bool -> bool
(** [should_auto_template x b] is [true] when [b] is [true] and we
automatically use template polymorphism. [x] is the name of the
inductive under consideration. *)
+
+val template_polymorphism_candidate :
+ Environ.env -> Entries.universes_entry -> Constr.rel_context -> Sorts.t option -> bool
+(** [template_polymorphism_candidate env uctx params conclsort] is
+ [true] iff an inductive with params [params] and conclusion
+ [conclsort] would be definable as template polymorphic. It should
+ have at least one universe in its monomorphic universe context that
+ can be made parametric in its conclusion sort, if one is given.
+ If the [Template Check] flag is false we just check that the conclusion sort
+ is not small. *)
+
+val sign_level : Environ.env -> Evd.evar_map -> Constr.rel_declaration list -> Univ.Universe.t
+(** [sign_level env sigma ctx] computes the universe level of the context [ctx]
+ as the [sup] of its individual assumptions, which should be well-typed in [env] and [sigma] *)
diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml
index e3cffa8523..8fd6bc7eab 100644
--- a/vernac/declareObl.ml
+++ b/vernac/declareObl.ml
@@ -530,7 +530,7 @@ let obligation_terminator entries uctx { name; num; auto } =
declares the univs of the constant,
each subsequent obligation declares its own additional
universes and constraints if any *)
- if defined then UState.make (Global.universes ())
+ if defined then UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ())
else ctx
in
let prg = {prg with prg_ctx} in
diff --git a/vernac/library.ml b/vernac/library.ml
new file mode 100644
index 0000000000..e91cb965f5
--- /dev/null
+++ b/vernac/library.ml
@@ -0,0 +1,651 @@
+(************************************************************************)
+(* * 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) *)
+(************************************************************************)
+
+open Pp
+open CErrors
+open Util
+
+open Names
+open Libnames
+open Lib
+open Libobject
+
+(************************************************************************)
+(*s Low-level interning/externing of libraries to files *)
+
+let raw_extern_library f =
+ System.raw_extern_state Coq_config.vo_magic_number f
+
+let raw_intern_library f =
+ System.with_magic_number_check
+ (System.raw_intern_state Coq_config.vo_magic_number) f
+
+(************************************************************************)
+(** Serialized objects loaded on-the-fly *)
+
+exception Faulty of string
+
+module Delayed :
+sig
+
+type 'a delayed
+val in_delayed : string -> in_channel -> 'a delayed * Digest.t
+val fetch_delayed : 'a delayed -> 'a
+
+end =
+struct
+
+type 'a delayed = {
+ del_file : string;
+ del_off : int;
+ del_digest : Digest.t;
+}
+
+let in_delayed f ch =
+ let pos = pos_in ch in
+ let _, digest = System.skip_in_segment f ch in
+ ({ del_file = f; del_digest = digest; del_off = pos; }, digest)
+
+(** Fetching a table of opaque terms at position [pos] in file [f],
+ expecting to find first a copy of [digest]. *)
+
+let fetch_delayed del =
+ let { del_digest = digest; del_file = f; del_off = pos; } = del in
+ try
+ let ch = raw_intern_library f in
+ let () = seek_in ch pos in
+ let obj, _, digest' = System.marshal_in_segment f ch in
+ let () = close_in ch in
+ if not (String.equal digest digest') then raise (Faulty f);
+ obj
+ with e when CErrors.noncritical e -> raise (Faulty f)
+
+end
+
+open Delayed
+
+
+(************************************************************************)
+(*s Modules on disk contain the following informations (after the magic
+ number, and before the digest). *)
+
+type compilation_unit_name = DirPath.t
+
+type library_disk = {
+ md_compiled : Safe_typing.compiled_library;
+ md_objects : Declaremods.library_objects;
+}
+
+type summary_disk = {
+ md_name : compilation_unit_name;
+ md_imports : compilation_unit_name array;
+ md_deps : (compilation_unit_name * Safe_typing.vodigest) array;
+}
+
+(*s Modules loaded in memory contain the following informations. They are
+ kept in the global table [libraries_table]. *)
+
+type library_t = {
+ library_name : compilation_unit_name;
+ library_data : library_disk delayed;
+ library_deps : (compilation_unit_name * Safe_typing.vodigest) array;
+ library_imports : compilation_unit_name array;
+ library_digests : Safe_typing.vodigest;
+ library_extra_univs : Univ.ContextSet.t;
+}
+
+type library_summary = {
+ libsum_name : compilation_unit_name;
+ libsum_digests : Safe_typing.vodigest;
+ libsum_imports : compilation_unit_name array;
+}
+
+module LibraryOrdered = DirPath
+module LibraryMap = Map.Make(LibraryOrdered)
+module LibraryFilenameMap = Map.Make(LibraryOrdered)
+
+(* This is a map from names to loaded libraries *)
+let libraries_table : library_summary LibraryMap.t ref =
+ Summary.ref LibraryMap.empty ~name:"LIBRARY"
+
+(* This is the map of loaded libraries filename *)
+(* (not synchronized so as not to be caught in the states on disk) *)
+let libraries_filename_table = ref LibraryFilenameMap.empty
+
+(* These are the _ordered_ sets of loaded, imported and exported libraries *)
+let libraries_loaded_list = Summary.ref [] ~name:"LIBRARY-LOAD"
+let libraries_imports_list = Summary.ref [] ~name:"LIBRARY-IMPORT"
+let libraries_exports_list = Summary.ref [] ~name:"LIBRARY-EXPORT"
+
+(* various requests to the tables *)
+
+let find_library dir =
+ LibraryMap.find dir !libraries_table
+
+let try_find_library dir =
+ try find_library dir
+ with Not_found ->
+ user_err ~hdr:"Library.find_library"
+ (str "Unknown library " ++ DirPath.print dir)
+
+let register_library_filename dir f =
+ (* Not synchronized: overwrite the previous binding if one existed *)
+ (* from a previous play of the session *)
+ libraries_filename_table :=
+ LibraryFilenameMap.add dir f !libraries_filename_table
+
+let library_full_filename dir =
+ try LibraryFilenameMap.find dir !libraries_filename_table
+ with Not_found -> "<unavailable filename>"
+
+let overwrite_library_filenames f =
+ let f =
+ if Filename.is_relative f then Filename.concat (Sys.getcwd ()) f else f in
+ LibraryMap.iter (fun dir _ -> register_library_filename dir f)
+ !libraries_table
+
+let library_is_loaded dir =
+ try let _ = find_library dir in true
+ with Not_found -> false
+
+let library_is_opened dir =
+ List.exists (fun name -> DirPath.equal name dir) !libraries_imports_list
+
+let loaded_libraries () = !libraries_loaded_list
+
+let opened_libraries () = !libraries_imports_list
+
+ (* If a library is loaded several time, then the first occurrence must
+ be performed first, thus the libraries_loaded_list ... *)
+
+let register_loaded_library m =
+ let libname = m.libsum_name in
+ let link () =
+ let dirname = Filename.dirname (library_full_filename libname) in
+ let prefix = Nativecode.mod_uid_of_dirpath libname ^ "." in
+ let f = prefix ^ "cmo" in
+ let f = Dynlink.adapt_filename f in
+ if Coq_config.native_compiler then
+ Nativelib.link_library (Global.env()) ~prefix ~dirname ~basename:f
+ in
+ let rec aux = function
+ | [] -> link (); [libname]
+ | m'::_ as l when DirPath.equal m' libname -> l
+ | m'::l' -> m' :: aux l' in
+ libraries_loaded_list := aux !libraries_loaded_list;
+ libraries_table := LibraryMap.add libname m !libraries_table
+
+ (* ... while if a library is imported/exported several time, then
+ only the last occurrence is really needed - though the imported
+ list may differ from the exported list (consider the sequence
+ Export A; Export B; Import A which results in A;B for exports but
+ in B;A for imports) *)
+
+let rec remember_last_of_each l m =
+ match l with
+ | [] -> [m]
+ | m'::l' when DirPath.equal m' m -> remember_last_of_each l' m
+ | m'::l' -> m' :: remember_last_of_each l' m
+
+let register_open_library export m =
+ libraries_imports_list := remember_last_of_each !libraries_imports_list m;
+ if export then
+ libraries_exports_list := remember_last_of_each !libraries_exports_list m
+
+(************************************************************************)
+(*s Opening libraries *)
+
+(* [open_library export explicit m] opens library [m] if not already
+ opened _or_ if explicitly asked to be (re)opened *)
+
+let open_library export explicit_libs m =
+ if
+ (* Only libraries indirectly to open are not reopen *)
+ (* Libraries explicitly mentioned by the user are always reopen *)
+ List.exists (fun m' -> DirPath.equal m m') explicit_libs
+ || not (library_is_opened m)
+ then begin
+ register_open_library export m;
+ Declaremods.really_import_module (MPfile m)
+ end
+ else
+ if export then
+ libraries_exports_list := remember_last_of_each !libraries_exports_list m
+
+(* open_libraries recursively open a list of libraries but opens only once
+ a library that is re-exported many times *)
+
+let open_libraries export modl =
+ let to_open_list =
+ List.fold_left
+ (fun l m ->
+ let subimport =
+ Array.fold_left
+ (fun l m -> remember_last_of_each l m)
+ l m.libsum_imports
+ in remember_last_of_each subimport m.libsum_name)
+ [] modl in
+ let explicit = List.map (fun m -> m.libsum_name) modl in
+ List.iter (open_library export explicit) to_open_list
+
+
+(**********************************************************************)
+(* import and export of libraries - synchronous operations *)
+(* at the end similar to import and export of modules except that it *)
+(* is optimized: when importing several libraries at the same time *)
+(* which themselves indirectly imports the very same modules, these *)
+(* ones are imported only ones *)
+
+let open_import_library i (_,(modl,export)) =
+ if Int.equal i 1 then
+ (* even if the library is already imported, we re-import it *)
+ (* if not (library_is_opened dir) then *)
+ open_libraries export (List.map try_find_library modl)
+
+let cache_import_library obj =
+ open_import_library 1 obj
+
+let subst_import_library (_,o) = o
+
+let classify_import_library (_,export as obj) =
+ if export then Substitute obj else Dispose
+
+let in_import_library : DirPath.t list * bool -> obj =
+ declare_object {(default_object "IMPORT LIBRARY") with
+ cache_function = cache_import_library;
+ open_function = open_import_library;
+ subst_function = subst_import_library;
+ classify_function = classify_import_library }
+
+(************************************************************************)
+(** {6 Tables of opaque proof terms} *)
+
+(** We now store opaque proof terms apart from the rest of the environment.
+ See the [Indirect] constructor in [Lazyconstr.lazy_constr]. This way,
+ we can quickly load a first half of a .vo file without these opaque
+ terms, and access them only when a specific command (e.g. Print or
+ Print Assumptions) needs it. *)
+
+(** Delayed / available tables of opaque terms *)
+
+type 'a table_status =
+ | ToFetch of 'a array delayed
+ | Fetched of 'a array
+
+let opaque_tables =
+ ref (LibraryMap.empty : (Opaqueproof.opaque_proofterm table_status) LibraryMap.t)
+
+let add_opaque_table dp st =
+ opaque_tables := LibraryMap.add dp st !opaque_tables
+
+let access_table what tables dp i =
+ let t = match LibraryMap.find dp !tables with
+ | Fetched t -> t
+ | ToFetch f ->
+ let dir_path = Names.DirPath.to_string dp in
+ Flags.if_verbose Feedback.msg_info (str"Fetching " ++ str what++str" from disk for " ++ str dir_path);
+ let t =
+ try fetch_delayed f
+ with Faulty f ->
+ user_err ~hdr:"Library.access_table"
+ (str "The file " ++ str f ++ str " (bound to " ++ str dir_path ++
+ str ") is inaccessible or corrupted,\ncannot load some " ++
+ str what ++ str " in it.\n")
+ in
+ tables := LibraryMap.add dp (Fetched t) !tables;
+ t
+ in
+ assert (i < Array.length t); t.(i)
+
+let access_opaque_table dp i =
+ let what = "opaque proofs" in
+ access_table what opaque_tables dp i
+
+let indirect_accessor = {
+ Opaqueproof.access_proof = access_opaque_table;
+ Opaqueproof.access_discharge = Cooking.cook_constr;
+}
+
+(************************************************************************)
+(* Internalise libraries *)
+
+type seg_sum = summary_disk
+type seg_lib = library_disk
+type seg_univ = (* true = vivo, false = vi *)
+ Univ.ContextSet.t * bool
+type seg_proofs = Opaqueproof.opaque_proofterm array
+
+let mk_library sd md digests univs =
+ {
+ library_name = sd.md_name;
+ library_data = md;
+ library_deps = sd.md_deps;
+ library_imports = sd.md_imports;
+ library_digests = digests;
+ library_extra_univs = univs;
+ }
+
+let mk_summary m = {
+ libsum_name = m.library_name;
+ libsum_imports = m.library_imports;
+ libsum_digests = m.library_digests;
+}
+
+let intern_from_file f =
+ let ch = raw_intern_library f in
+ let (lsd : seg_sum), _, digest_lsd = System.marshal_in_segment f ch in
+ let ((lmd : seg_lib delayed), digest_lmd) = in_delayed f ch in
+ let (univs : seg_univ option), _, digest_u = System.marshal_in_segment f ch in
+ let _ = System.skip_in_segment f ch in
+ let ((del_opaque : seg_proofs delayed),_) = in_delayed f ch in
+ close_in ch;
+ register_library_filename lsd.md_name f;
+ add_opaque_table lsd.md_name (ToFetch del_opaque);
+ let open Safe_typing in
+ match univs with
+ | None -> mk_library lsd lmd (Dvo_or_vi digest_lmd) Univ.ContextSet.empty
+ | Some (uall,true) ->
+ mk_library lsd lmd (Dvivo (digest_lmd,digest_u)) uall
+ | Some (_,false) ->
+ mk_library lsd lmd (Dvo_or_vi digest_lmd) Univ.ContextSet.empty
+
+module DPMap = Map.Make(DirPath)
+
+let rec intern_library ~lib_resolver (needed, contents) (dir, f) from =
+ (* Look if in the current logical environment *)
+ try (find_library dir).libsum_digests, (needed, contents)
+ with Not_found ->
+ (* Look if already listed and consequently its dependencies too *)
+ try (DPMap.find dir contents).library_digests, (needed, contents)
+ with Not_found ->
+ Feedback.feedback(Feedback.FileDependency (from, DirPath.to_string dir));
+ (* [dir] is an absolute name which matches [f] which must be in loadpath *)
+ let f = match f with Some f -> f | None -> lib_resolver dir in
+ let m = intern_from_file f in
+ if not (DirPath.equal dir m.library_name) then
+ user_err ~hdr:"load_physical_library"
+ (str "The file " ++ str f ++ str " contains library" ++ spc () ++
+ DirPath.print m.library_name ++ spc () ++ str "and not library" ++
+ spc() ++ DirPath.print dir);
+ Feedback.feedback (Feedback.FileLoaded(DirPath.to_string dir, f));
+ m.library_digests, intern_library_deps ~lib_resolver (needed, contents) dir m f
+
+and intern_library_deps ~lib_resolver libs dir m from =
+ let needed, contents =
+ Array.fold_left (intern_mandatory_library ~lib_resolver dir from)
+ libs m.library_deps in
+ (dir :: needed, DPMap.add dir m contents )
+
+and intern_mandatory_library ~lib_resolver caller from libs (dir,d) =
+ let digest, libs = intern_library ~lib_resolver libs (dir, None) (Some from) in
+ if not (Safe_typing.digest_match ~actual:digest ~required:d) then
+ user_err (str "Compiled library " ++ DirPath.print caller ++
+ str " (in file " ++ str from ++ str ") makes inconsistent assumptions \
+ over library " ++ DirPath.print dir);
+ libs
+
+let rec_intern_library ~lib_resolver libs (dir, f) =
+ let _, libs = intern_library ~lib_resolver libs (dir, Some f) None in
+ libs
+
+let native_name_from_filename f =
+ let ch = raw_intern_library f in
+ let (lmd : seg_sum), pos, digest_lmd = System.marshal_in_segment f ch in
+ Nativecode.mod_uid_of_dirpath lmd.md_name
+
+(**********************************************************************)
+(*s [require_library] loads and possibly opens a library. This is a
+ synchronized operation. It is performed as follows:
+
+ preparation phase: (functions require_library* ) the library and its
+ dependencies are read from to disk (using intern_* )
+ [they are read from disk to ensure that at section/module
+ discharging time, the physical library referred to outside the
+ section/module is the one that was used at type-checking time in
+ the section/module]
+
+ execution phase: (through add_leaf and cache_require)
+ the library is loaded in the environment and Nametab, the objects are
+ registered etc, using functions from Declaremods (via load_library,
+ which recursively loads its dependencies)
+*)
+
+let register_library m =
+ let l = fetch_delayed m.library_data in
+ Declaremods.register_library
+ m.library_name
+ l.md_compiled
+ l.md_objects
+ m.library_digests
+ m.library_extra_univs;
+ register_loaded_library (mk_summary m)
+
+(* Follow the semantics of Anticipate object:
+ - called at module or module type closing when a Require occurs in
+ the module or module type
+ - not called from a library (i.e. a module identified with a file) *)
+let load_require _ (_,(needed,modl,_)) =
+ List.iter register_library needed
+
+let open_require i (_,(_,modl,export)) =
+ Option.iter (fun exp -> open_libraries exp (List.map find_library modl))
+ export
+
+ (* [needed] is the ordered list of libraries not already loaded *)
+let cache_require o =
+ load_require 1 o;
+ open_require 1 o
+
+let discharge_require (_,o) = Some o
+
+(* open_function is never called from here because an Anticipate object *)
+
+type require_obj = library_t list * DirPath.t list * bool option
+
+let in_require : require_obj -> obj =
+ declare_object {(default_object "REQUIRE") with
+ cache_function = cache_require;
+ load_function = load_require;
+ open_function = (fun _ _ -> assert false);
+ discharge_function = discharge_require;
+ classify_function = (fun o -> Anticipate o) }
+
+(* Require libraries, import them if [export <> None], mark them for export
+ if [export = Some true] *)
+
+let warn_require_in_module =
+ CWarnings.create ~name:"require-in-module" ~category:"deprecated"
+ (fun () -> strbrk "Require inside a module is" ++
+ strbrk " deprecated and strongly discouraged. " ++
+ strbrk "You can Require a module at toplevel " ++
+ strbrk "and optionally Import it inside another one.")
+
+let require_library_from_dirpath ~lib_resolver modrefl export =
+ let needed, contents = List.fold_left (rec_intern_library ~lib_resolver) ([], DPMap.empty) modrefl in
+ let needed = List.rev_map (fun dir -> DPMap.find dir contents) needed in
+ let modrefl = List.map fst modrefl in
+ if Lib.is_module_or_modtype () then
+ begin
+ warn_require_in_module ();
+ add_anonymous_leaf (in_require (needed,modrefl,None));
+ Option.iter (fun exp ->
+ add_anonymous_leaf (in_import_library (modrefl,exp)))
+ export
+ end
+ else
+ add_anonymous_leaf (in_require (needed,modrefl,export));
+ ()
+
+(* the function called by Vernacentries.vernac_import *)
+
+let safe_locate_module qid =
+ try Nametab.locate_module qid
+ with Not_found ->
+ user_err ?loc:qid.CAst.loc ~hdr:"safe_locate_module"
+ (pr_qualid qid ++ str " is not a module")
+
+let import_module export modl =
+ (* Optimization: libraries in a raw in the list are imported
+ "globally". If there is non-library in the list; it breaks the
+ optimization For instance: "Import Arith MyModule Zarith" will
+ not be optimized (possibly resulting in redefinitions, but
+ "Import MyModule Arith Zarith" and "Import Arith Zarith MyModule"
+ will have the submodules imported by both Arith and ZArith
+ imported only once *)
+ let flush = function
+ | [] -> ()
+ | modl -> add_anonymous_leaf (in_import_library (List.rev modl, export)) in
+ let rec aux acc = function
+ | qid :: l ->
+ let m,acc =
+ try Nametab.locate_module qid, acc
+ with Not_found-> flush acc; safe_locate_module qid, [] in
+ (match m with
+ | MPfile dir -> aux (dir::acc) l
+ | mp ->
+ flush acc;
+ try Declaremods.import_module export mp; aux [] l
+ with Not_found ->
+ user_err ?loc:qid.CAst.loc ~hdr:"import_module"
+ (pr_qualid qid ++ str " is not a module"))
+ | [] -> flush acc
+ in aux [] modl
+
+(************************************************************************)
+(*s Initializing the compilation of a library. *)
+
+let load_library_todo f =
+ let ch = raw_intern_library f in
+ let (s0 : seg_sum), _, _ = System.marshal_in_segment f ch in
+ let (s1 : seg_lib), _, _ = System.marshal_in_segment f ch in
+ let (s2 : seg_univ option), _, _ = System.marshal_in_segment f ch in
+ let tasks, _, _ = System.marshal_in_segment f ch in
+ let (s4 : seg_proofs), _, _ = System.marshal_in_segment f ch in
+ close_in ch;
+ if tasks = None then user_err ~hdr:"restart" (str"not a .vio file");
+ if s2 = None then user_err ~hdr:"restart" (str"not a .vio file");
+ if snd (Option.get s2) then user_err ~hdr:"restart" (str"not a .vio file");
+ s0, s1, Option.get s2, Option.get tasks, s4
+
+(************************************************************************)
+(*s [save_library dir] ends library [dir] and save it to the disk. *)
+
+let current_deps () =
+ let map name =
+ let m = try_find_library name in
+ (name, m.libsum_digests)
+ in
+ List.map map !libraries_loaded_list
+
+let current_reexports () = !libraries_exports_list
+
+let error_recursively_dependent_library dir =
+ user_err
+ (strbrk "Unable to use logical name " ++ DirPath.print dir ++
+ strbrk " to save current library because" ++
+ strbrk " it already depends on a library of this name.")
+
+(* We now use two different digests in a .vo file. The first one
+ only covers half of the file, without the opaque table. It is
+ used for identifying this version of this library : this digest
+ is the one leading to "inconsistent assumptions" messages.
+ The other digest comes at the very end, and covers everything
+ before it. This one is used for integrity check of the whole
+ file when loading the opaque table. *)
+
+(* Security weakness: file might have been changed on disk between
+ writing the content and computing the checksum... *)
+
+let save_library_to ?todo ~output_native_objects dir f otab =
+ let except = match todo with
+ | None ->
+ (* XXX *)
+ (* assert(!Flags.compilation_mode = Flags.BuildVo); *)
+ assert(Filename.check_suffix f ".vo");
+ Future.UUIDSet.empty
+ | Some (l,_) ->
+ assert(Filename.check_suffix f ".vio");
+ List.fold_left (fun e (r,_) -> Future.UUIDSet.add r.Stateid.uuid e)
+ Future.UUIDSet.empty l in
+ let cenv, seg, ast = Declaremods.end_library ~output_native_objects ~except dir in
+ let opaque_table, f2t_map = Opaqueproof.dump ~except otab in
+ let tasks, utab =
+ match todo with
+ | None -> None, None
+ | Some (tasks, rcbackup) ->
+ let tasks =
+ List.map Stateid.(fun (r,b) ->
+ try { r with uuid = Future.UUIDMap.find r.uuid f2t_map }, b
+ with Not_found -> assert b; { r with uuid = -1 }, b)
+ tasks in
+ Some (tasks,rcbackup),
+ Some (Univ.ContextSet.empty,false)
+ in
+ let sd = {
+ md_name = dir;
+ md_deps = Array.of_list (current_deps ());
+ md_imports = Array.of_list (current_reexports ());
+ } in
+ let md = {
+ md_compiled = cenv;
+ md_objects = seg;
+ } in
+ if Array.exists (fun (d,_) -> DirPath.equal d dir) sd.md_deps then
+ error_recursively_dependent_library dir;
+ (* Open the vo file and write the magic number *)
+ let f' = f in
+ let ch = raw_extern_library f' in
+ try
+ (* Writing vo payload *)
+ System.marshal_out_segment f' ch (sd : seg_sum);
+ System.marshal_out_segment f' ch (md : seg_lib);
+ System.marshal_out_segment f' ch (utab : seg_univ option);
+ System.marshal_out_segment f' ch (tasks : 'tasks option);
+ System.marshal_out_segment f' ch (opaque_table : seg_proofs);
+ close_out ch;
+ (* Writing native code files *)
+ if output_native_objects then
+ let fn = Filename.dirname f'^"/"^Nativecode.mod_uid_of_dirpath dir in
+ Nativelib.compile_library dir ast fn
+ with reraise ->
+ let reraise = CErrors.push reraise in
+ let () = Feedback.msg_warning (str "Removed file " ++ str f') in
+ let () = close_out ch in
+ let () = Sys.remove f' in
+ iraise reraise
+
+let save_library_raw f sum lib univs proofs =
+ let ch = raw_extern_library f in
+ System.marshal_out_segment f ch (sum : seg_sum);
+ System.marshal_out_segment f ch (lib : seg_lib);
+ System.marshal_out_segment f ch (Some univs : seg_univ option);
+ System.marshal_out_segment f ch (None : 'tasks option);
+ System.marshal_out_segment f ch (proofs : seg_proofs);
+ close_out ch
+
+module StringOrd = struct type t = string let compare = String.compare end
+module StringSet = Set.Make(StringOrd)
+
+let get_used_load_paths () =
+ StringSet.elements
+ (List.fold_left (fun acc m -> StringSet.add
+ (Filename.dirname (library_full_filename m)) acc)
+ StringSet.empty !libraries_loaded_list)
+
+let _ = Nativelib.get_load_paths := get_used_load_paths
+
+(* These commands may not be very safe due to ML-side plugin loading
+ etc... use at your own risk *)
+let extern_state s =
+ System.extern_state Coq_config.state_magic_number s (States.freeze ~marshallable:true)
+
+let intern_state s =
+ States.unfreeze (System.with_magic_number_check (System.intern_state Coq_config.state_magic_number) s);
+ overwrite_library_filenames s
diff --git a/vernac/library.mli b/vernac/library.mli
new file mode 100644
index 0000000000..973b369226
--- /dev/null
+++ b/vernac/library.mli
@@ -0,0 +1,81 @@
+(************************************************************************)
+(* * 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) *)
+(************************************************************************)
+
+open Names
+open Libnames
+
+(** This module provides functions to load, open and save
+ libraries. Libraries correspond to the subclass of modules that
+ coincide with a file on disk (the ".vo" files). Libraries on the
+ disk comes with checksums (obtained with the [Digest] module), which
+ are checked at loading time to prevent inconsistencies between files
+ written at various dates.
+*)
+
+(** {6 ... }
+ Require = load in the environment + open (if the optional boolean
+ is not [None]); mark also for export if the boolean is [Some true] *)
+val require_library_from_dirpath
+ : lib_resolver:(DirPath.t -> CUnix.physical_path)
+ -> (DirPath.t * string) list
+ -> bool option
+ -> unit
+
+(** {6 Start the compilation of a library } *)
+
+(** Segments of a library *)
+type seg_sum
+type seg_lib
+type seg_univ = (* all_cst, finished? *)
+ Univ.ContextSet.t * bool
+type seg_proofs = Opaqueproof.opaque_proofterm array
+
+(** Open a module (or a library); if the boolean is true then it's also
+ an export otherwise just a simple import *)
+val import_module : bool -> qualid list -> unit
+
+(** End the compilation of a library and save it to a ".vo" file.
+ [output_native_objects]: when producing vo objects, also compile the native-code version. *)
+val save_library_to :
+ ?todo:(((Future.UUID.t,'document) Stateid.request * bool) list * 'counters) ->
+ output_native_objects:bool ->
+ DirPath.t -> string -> Opaqueproof.opaquetab -> unit
+
+val load_library_todo
+ : CUnix.physical_path
+ -> seg_sum * seg_lib * seg_univ * 'tasks * seg_proofs
+
+val save_library_raw : string -> seg_sum -> seg_lib -> seg_univ -> seg_proofs -> unit
+
+(** {6 Interrogate the status of libraries } *)
+
+ (** - Tell if a library is loaded or opened *)
+val library_is_loaded : DirPath.t -> bool
+val library_is_opened : DirPath.t -> bool
+
+ (** - Tell which libraries are loaded or imported *)
+val loaded_libraries : unit -> DirPath.t list
+val opened_libraries : unit -> DirPath.t list
+
+ (** - Return the full filename of a loaded library. *)
+val library_full_filename : DirPath.t -> string
+
+ (** - Overwrite the filename of all libraries (used when restoring a state) *)
+val overwrite_library_filenames : string -> unit
+
+(** {6 Native compiler. } *)
+val native_name_from_filename : string -> string
+
+(** {6 Opaque accessors} *)
+val indirect_accessor : Opaqueproof.indirect_accessor
+
+(** Low-level state overwriting, not very safe *)
+val intern_state : string -> unit
+val extern_state : string -> unit
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 5d153fa8be..da14b6e979 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -454,7 +454,7 @@ let obligation_hook prg obl num auto { DeclareDef.Hook.S.uctx = ctx'; dref; _ }
if not prg.prg_poly (* Not polymorphic *) then
(* The universe context was declared globally, we continue
from the new global environment. *)
- let ctx = UState.make (Global.universes ()) in
+ let ctx = UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()) in
let ctx' = UState.merge_subst ctx (UState.subst ctx') in
Univ.Instance.empty, ctx'
else
diff --git a/vernac/record.ml b/vernac/record.ml
index 11237f3873..831fb53549 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -85,10 +85,10 @@ let interp_fields_evars env sigma impls_env nots l =
let compute_constructor_level evars env l =
List.fold_right (fun d (env, univ) ->
- let univ =
+ let univ =
if is_local_assum d then
let s = Retyping.get_sort_of env evars (RelDecl.get_type d) in
- Univ.sup (univ_of_sort s) univ
+ Univ.sup (univ_of_sort s) univ
else univ
in (EConstr.push_rel d env, univ))
l (env, Univ.Universe.sprop)
@@ -101,8 +101,19 @@ let binder_of_decl = function
let binders_of_decls = List.map binder_of_decl
+let check_anonymous_type ind =
+ match ind with
+ | { CAst.v = CSort (Glob_term.UAnonymous {rigid=true}) } -> true
+ | _ -> false
+
let typecheck_params_and_fields finite def poly pl ps records =
let env0 = Global.env () in
+ (* Special case elaboration for template-polymorphic inductives,
+ lower bound on introduced universes is Prop so that we do not miss
+ any Set <= i constraint for universes that might actually be instantiated with Prop. *)
+ let is_template =
+ List.exists (fun (_, arity, _, _) -> Option.cata check_anonymous_type true arity) records in
+ let env0 = if not poly && is_template then Environ.set_universes_lbound env0 Univ.Level.prop else env0 in
let sigma, decl = Constrexpr_ops.interp_univ_decl_opt env0 pl in
let () =
let error bk {CAst.loc; v=name} =
@@ -111,15 +122,15 @@ let typecheck_params_and_fields finite def poly pl ps records =
user_err ?loc ~hdr:"record" (str "Record parameters must be named")
| _ -> ()
in
- List.iter
+ List.iter
(function CLocalDef (b, _, _) -> error default_binder_kind b
| CLocalAssum (ls, bk, ce) -> List.iter (error bk) ls
| CLocalPattern {CAst.loc} ->
Loc.raise ?loc (Stream.Error "pattern with quote not allowed in record parameters")) ps
- in
+ in
let sigma, (impls_env, ((env1,newps), imps)) = interp_context_evars ~program_mode:false env0 sigma ps in
let fold (sigma, template) (_, t, _, _) = match t with
- | Some t ->
+ | Some t ->
let env = EConstr.push_rel_context newps env0 in
let poly =
match t with
@@ -138,7 +149,7 @@ let typecheck_params_and_fields finite def poly pl ps records =
(sigma, false), (s, s')
else (sigma, false), (s, s'))
| _ -> user_err ?loc:(constr_loc t) (str"Sort expected."))
- | None ->
+ | None ->
let uvarkind = Evd.univ_flexible_alg in
let sigma, s = Evd.new_sort_variable uvarkind sigma in
(sigma, template), (EConstr.mkSort s, s)
@@ -168,23 +179,23 @@ let typecheck_params_and_fields finite def poly pl ps records =
let _, univ = compute_constructor_level sigma env_ar newfs in
let univ = if Sorts.is_sprop sort then univ else Univ.Universe.sup univ Univ.type0m_univ in
if not def && is_impredicative_sort env0 sort then
- sigma, typ
+ sigma, (univ, typ)
else
let sigma = Evd.set_leq_sort env_ar sigma (Sorts.sort_of_univ univ) sort in
if Univ.is_small_univ univ &&
Option.cata (Evd.is_flexible_level sigma) false (Evd.is_sort_variable sigma sort) then
(* We can assume that the level in aritysort is not constrained
and clear it, if it is flexible *)
- Evd.set_eq_sort env_ar sigma Sorts.set sort, EConstr.mkSort (Sorts.sort_of_univ univ)
- else sigma, typ
+ Evd.set_eq_sort env_ar sigma Sorts.set sort, (univ, EConstr.mkSort (Sorts.sort_of_univ univ))
+ else sigma, (univ, typ)
in
let (sigma, typs) = List.fold_left2_map fold sigma typs data in
let sigma, (newps, ans) = Evarutil.finalize sigma (fun nf ->
let newps = List.map (RelDecl.map_constr_het nf) newps in
- let map (impls, newfs) typ =
+ let map (impls, newfs) (univ, typ) =
let newfs = List.map (RelDecl.map_constr_het nf) newfs in
let typ = nf typ in
- (typ, impls, newfs)
+ (univ, typ, impls, newfs)
in
let ans = List.map2 map data typs in
newps, ans)
@@ -295,7 +306,7 @@ let declare_projections indsp ctx ?(kind=Decls.StructureComponent) binder_name f
let x = make_annot (Name binder_name) mip.mind_relevance in
let fields = instantiate_possibly_recursive_type (fst indsp) u mib.mind_ntypes paramdecls fields in
let lifted_fields = Termops.lift_rel_context 1 fields in
- let primitive =
+ let primitive =
match mib.mind_record with
| PrimRecord _ -> true
| FakeRecord | NotRecord -> false
@@ -310,7 +321,7 @@ let declare_projections indsp ctx ?(kind=Decls.StructureComponent) binder_name f
| Anonymous ->
(None::sp_projs,i,NoProjection fi::subst)
| Name fid -> try
- let kn, term =
+ let kn, term =
if is_local_assum decl && primitive then
let p = Projection.Repr.make indsp
~proj_npars:mib.mind_nparams
@@ -345,12 +356,12 @@ let declare_projections indsp ctx ?(kind=Decls.StructureComponent) binder_name f
let kn = declare_constant ~name:fid ~kind (Declare.DefinitionEntry entry) in
let constr_fip =
let proj_args = (*Rel 1 refers to "x"*) paramargs@[mkRel 1] in
- applist (mkConstU (kn,u),proj_args)
+ applist (mkConstU (kn,u),proj_args)
in
Declare.definition_message fid;
kn, constr_fip
with Type_errors.TypeError (ctx,te) ->
- raise (NotDefinable (BadTypedProj (fid,ctx,te)))
+ raise (NotDefinable (BadTypedProj (fid,ctx,te)))
in
let refi = GlobRef.ConstRef kn in
Impargs.maybe_declare_manual_implicits false refi impls;
@@ -404,29 +415,33 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa
let binder_name =
match name with
| None ->
- let map (id, _, _, _, _, _, _) =
+ let map (id, _, _, _, _, _, _, _) =
Id.of_string (Unicode.lowercase_first_char (Id.to_string id))
in
Array.map_of_list map record_data
| Some n -> n
in
let ntypes = List.length record_data in
- let mk_block i (id, idbuild, arity, _, fields, _, _) =
+ let mk_block i (id, idbuild, min_univ, arity, _, fields, _, _) =
let nfields = List.length fields in
let args = Context.Rel.to_extended_list mkRel nfields params in
let ind = applist (mkRel (ntypes - i + nparams + nfields), args) in
let type_constructor = it_mkProd_or_LetIn ind fields in
let template =
+ let template_candidate () =
+ ComInductive.template_polymorphism_candidate (Global.env ()) univs params
+ (Some (Sorts.sort_of_univ min_univ))
+ in
match template with
| Some template, _ ->
(* templateness explicitly requested *)
if poly && template then user_err Pp.(strbrk "template and polymorphism not compatible");
+ if template && not (template_candidate ()) then
+ user_err Pp.(strbrk "record cannot be made template polymorphic on any universe");
template
| None, template ->
(* auto detect template *)
- ComInductive.should_auto_template id (template && not poly &&
- let _, s = Reduction.dest_arity (Global.env()) arity in
- not (Sorts.is_small s))
+ ComInductive.should_auto_template id (template && template_candidate ())
in
{ mind_entry_typename = id;
mind_entry_arity = arity;
@@ -437,7 +452,7 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa
let blocks = List.mapi mk_block record_data in
let primitive =
!primitive_flag &&
- List.for_all (fun (_,_,_,_,fields,_,_) -> List.exists is_local_assum fields) record_data
+ List.for_all (fun (_,_,_,_,_,fields,_,_) -> List.exists is_local_assum fields) record_data
in
let mie =
{ mind_entry_params = params;
@@ -454,7 +469,7 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa
let kn = ComInductive.declare_mutual_inductive_with_eliminations mie ubinders impls
~primitive_expected:!primitive_flag
in
- let map i (_, _, _, fieldimpls, fields, is_coe, coers) =
+ let map i (_, _, _, _, fieldimpls, fields, is_coe, coers) =
let rsp = (kn, i) in (* This is ind path of idstruc *)
let cstr = (rsp, 1) in
let kinds,sp_projs = declare_projections rsp ctx ~kind binder_name.(i) coers fieldimpls fields in
@@ -469,7 +484,7 @@ let implicits_of_context ctx =
List.map (fun name -> CAst.make (Some (name,true)))
(List.rev (Anonymous :: (List.map RelDecl.get_name ctx)))
-let declare_class def cumulative ubinders univs id idbuild paramimpls params arity
+let declare_class def cumulative ubinders univs id idbuild paramimpls params univ arity
template fieldimpls fields ?(kind=Decls.StructureComponent) coers priorities =
let fieldimpls =
(* Make the class implicit in the projections, and the params if applicable. *)
@@ -484,7 +499,7 @@ let declare_class def cumulative ubinders univs id idbuild paramimpls params ari
let binder = {binder with binder_name=Name binder_name} in
let class_body = it_mkLambda_or_LetIn field params in
let class_type = it_mkProd_or_LetIn arity params in
- let class_entry =
+ let class_entry =
Declare.definition_entry ~types:class_type ~univs class_body in
let cst = Declare.declare_constant ~name:id
(DefinitionEntry class_entry) ~kind:Decls.(IsDefinition Definition)
@@ -509,18 +524,18 @@ let declare_class def cumulative ubinders univs id idbuild paramimpls params ari
Impargs.declare_manual_implicits false (GlobRef.ConstRef proj_cst) (List.hd fieldimpls);
Classes.set_typeclass_transparency (EvalConstRef cst) false false;
let sub = match List.hd coers with
- | Some b -> Some ((if b then Backward else Forward), List.hd priorities)
- | None -> None
+ | Some b -> Some ((if b then Backward else Forward), List.hd priorities)
+ | None -> None
in
[cref, [Name proj_name, sub, Some proj_cst]]
| _ ->
- let record_data = [id, idbuild, arity, fieldimpls, fields, false,
+ let record_data = [id, idbuild, univ, arity, fieldimpls, fields, false,
List.map (fun _ -> { pf_subclass = false ; pf_canonical = true }) fields] in
let inds = declare_structure ~cumulative Declarations.BiFinite ubinders univs paramimpls
params template ~kind:Decls.Method ~name:[|binder_name|] record_data
in
- let coers = List.map2 (fun coe pri ->
- Option.map (fun b ->
+ let coers = List.map2 (fun coe pri ->
+ Option.map (fun b ->
if b then Backward, pri else Forward, pri) coe)
coers priorities
in
@@ -575,7 +590,7 @@ let add_constant_class env sigma cst =
let ctx, _ = decompose_prod_assum ty in
let args = Context.Rel.to_extended_vect Constr.mkRel 0 ctx in
let t = mkApp (mkConstU (cst, Univ.make_abstract_instance univs), args) in
- let tc =
+ let tc =
{ cl_univs = univs;
cl_impl = GlobRef.ConstRef cst;
cl_context = (List.map (const None) ctx, ctx);
@@ -679,24 +694,24 @@ let definition_structure udecl kind ~template ~cumulative ~poly finite records =
let template = template, auto_template in
match kind with
| Class def ->
- let (_, id, _, cfs, idbuild, _), (arity, implfs, fields) = match records, data with
+ let (_, id, _, cfs, idbuild, _), (univ, arity, implfs, fields) = match records, data with
| [r], [d] -> r, d
| _, _ -> CErrors.user_err (str "Mutual definitional classes are not handled")
in
let priorities = List.map (fun (_, { rf_priority }) -> {hint_priority = rf_priority ; hint_pattern = None}) cfs in
let coers = List.map (fun (_, { rf_subclass }) -> rf_subclass) cfs in
declare_class def cumulative ubinders univs id.CAst.v idbuild
- implpars params arity template implfs fields coers priorities
+ implpars params univ arity template implfs fields coers priorities
| _ ->
let map impls = implpars @ [CAst.make None] @ impls in
- let data = List.map (fun (arity, implfs, fields) -> (arity, List.map map implfs, fields)) data in
- let map (arity, implfs, fields) (is_coe, id, _, cfs, idbuild, _) =
+ let data = List.map (fun (univ, arity, implfs, fields) -> (univ, arity, List.map map implfs, fields)) data in
+ let map (univ, arity, implfs, fields) (is_coe, id, _, cfs, idbuild, _) =
let coe = List.map (fun (_, { rf_subclass ; rf_canonical }) ->
{ pf_subclass = not (Option.is_empty rf_subclass);
pf_canonical = rf_canonical })
cfs
in
- id.CAst.v, idbuild, arity, implfs, fields, is_coe, coe
+ id.CAst.v, idbuild, univ, arity, implfs, fields, is_coe, coe
in
let data = List.map2 map data records in
let inds = declare_structure ~cumulative finite ubinders univs implpars params template data in
diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib
index 20de6b4ff2..cd13f83e96 100644
--- a/vernac/vernac.mllib
+++ b/vernac/vernac.mllib
@@ -16,6 +16,7 @@ DeclareDef
DeclareObl
Canonical
RecLemmas
+Library
Lemmas
Class
Auto_ind_decl
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 4ae9d6d54f..3d14e8d510 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -606,6 +606,24 @@ let vernac_assumption ~atts discharge kind l nl =
| DeclareDef.Discharge -> Dumpglob.dump_definition lid true "var") idl) l;
ComAssumption.do_assumptions ~poly:atts.polymorphic ~program_mode:atts.program ~scope ~kind nl l
+let set_template_check b =
+ let typing_flags = Environ.typing_flags (Global.env ()) in
+ Global.set_typing_flags { typing_flags with Declarations.check_template = b }
+
+let is_template_check () =
+ let typing_flags = Environ.typing_flags (Global.env ()) in
+ typing_flags.Declarations.check_template
+
+let () =
+ let tccheck =
+ { optdepr = true;
+ optname = "Template universe check";
+ optkey = ["Template"; "Check"];
+ optread = (fun () -> is_template_check ());
+ optwrite = (fun b -> set_template_check b)}
+ in
+ declare_bool_option tccheck
+
let is_polymorphic_inductive_cumulativity =
declare_bool_option_and_ref ~depr:false ~value:false
~name:"Polymorphic inductive cumulativity"
@@ -1161,11 +1179,11 @@ let vernac_chdir = function
let vernac_write_state file =
let file = CUnix.make_suffix file ".coq" in
- States.extern_state file
+ Library.extern_state file
let vernac_restore_state file =
let file = Loadpath.locate_file (CUnix.make_suffix file ".coq") in
- States.intern_state file
+ Library.intern_state file
(************)
(* Commands *)
@@ -1954,9 +1972,9 @@ let vernac_print ~pstate ~atts =
function
| PrintTypingFlags -> pr_typing_flags (Environ.typing_flags (Global.env ()))
| PrintTables -> print_tables ()
- | PrintFullContext-> print_full_context_typ env sigma
- | PrintSectionContext qid -> print_sec_context_typ env sigma qid
- | PrintInspect n -> inspect env sigma n
+ | PrintFullContext-> print_full_context_typ Library.indirect_accessor env sigma
+ | PrintSectionContext qid -> print_sec_context_typ Library.indirect_accessor env sigma qid
+ | PrintInspect n -> inspect Library.indirect_accessor env sigma n
| PrintGrammar ent -> Metasyntax.pr_grammar ent
| PrintCustomGrammar ent -> Metasyntax.pr_custom_grammar ent
| PrintLoadPath dir -> (* For compatibility ? *) print_loadpath dir
@@ -1969,7 +1987,7 @@ let vernac_print ~pstate ~atts =
| PrintDebugGC -> Mltop.print_gc ()
| PrintName (qid,udecl) ->
dump_global qid;
- print_name env sigma qid udecl
+ print_name Library.indirect_accessor env sigma qid udecl
| PrintGraph -> Prettyp.print_graph ()
| PrintClasses -> Prettyp.print_classes()
| PrintTypeClasses -> Prettyp.print_typeclasses()
@@ -2267,7 +2285,7 @@ let with_fail ~st f =
user_err ~hdr:"Fail" (str "The command has not failed!")
| Ok msg ->
if not !Flags.quiet || !test_mode
- then Feedback.msg_info (str "The command has indeed failed with message:" ++ fnl () ++ msg)
+ then Feedback.msg_notice (str "The command has indeed failed with message:" ++ fnl () ++ msg)
let locate_if_not_already ?loc (e, info) =
match Loc.get_loc info with
@@ -2538,7 +2556,7 @@ let rec translate_vernac ~atts v = let open Vernacextend in match v with
VtDefault(fun () ->
vernac_hints ~atts dbnames hints)
| VernacSyntacticDefinition (id,c,b) ->
- VtDefault(fun () -> vernac_syntactic_definition ~atts id c b)
+ VtDefault(fun () -> vernac_syntactic_definition ~atts id c b)
| VernacArguments (qid, args, more_implicits, nargs, bidi, flags) ->
VtDefault(fun () ->
with_section_locality ~atts (vernac_arguments qid args more_implicits nargs bidi flags))
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-07 02:33:11 +0000