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/comDefinition.ml4
-rw-r--r--vernac/comDefinition.mli2
-rw-r--r--vernac/comInductive.ml124
-rw-r--r--vernac/comInductive.mli14
-rw-r--r--vernac/comProgramFixpoint.ml53
-rw-r--r--vernac/declareDef.ml2
-rw-r--r--vernac/declareDef.mli4
-rw-r--r--vernac/declareObl.ml23
-rw-r--r--vernac/declareObl.mli2
-rw-r--r--vernac/indschemes.ml21
-rw-r--r--vernac/lemmas.ml22
-rw-r--r--vernac/library.ml517
-rw-r--r--vernac/library.mli74
-rw-r--r--vernac/obligations.ml6
-rw-r--r--vernac/proof_using.ml2
-rw-r--r--vernac/record.ml96
-rw-r--r--vernac/vernac.mllib1
-rw-r--r--vernac/vernacentries.ml54
20 files changed, 857 insertions, 178 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/comDefinition.ml b/vernac/comDefinition.ml
index 57de719cb4..9745358ba2 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -85,12 +85,12 @@ let do_definition ~program_mode ?hook ~name ~scope ~poly ~kind univdecl bl red_o
in
if program_mode then
let env = Global.env () in
- let (c,ctx), sideff = Future.force ce.Proof_global.proof_entry_body in
+ let (c,ctx), sideff = Future.force ce.Declare.proof_entry_body in
assert(Safe_typing.empty_private_constants = sideff.Evd.seff_private);
assert(Univ.ContextSet.is_empty ctx);
Obligations.check_evars env evd;
let c = EConstr.of_constr c in
- let typ = match ce.Proof_global.proof_entry_type with
+ let typ = match ce.Declare.proof_entry_type with
| Some t -> EConstr.of_constr t
| None -> Retyping.get_type_of env evd c
in
diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli
index db0c102e14..01505d0733 100644
--- a/vernac/comDefinition.mli
+++ b/vernac/comDefinition.mli
@@ -41,5 +41,5 @@ val interp_definition
-> red_expr option
-> constr_expr
-> constr_expr option
- -> Evd.side_effects Proof_global.proof_entry *
+ -> Evd.side_effects Declare.proof_entry *
Evd.evar_map * UState.universe_decl * Impargs.manual_implicits
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/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index 3497e6369f..0e17f2b274 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -44,41 +44,68 @@ let mkSubset sigma name typ prop =
let make_qref s = qualid_of_string s
let lt_ref = make_qref "Init.Peano.lt"
+type family = SPropF | PropF | TypeF
+let family_of_sort_family = let open Sorts in function
+ | InSProp -> SPropF
+ | InProp -> PropF
+ | InSet | InType -> TypeF
+
+let get_sigmatypes sigma ~sort ~predsort =
+ let open EConstr in
+ let which, sigsort = match predsort, sort with
+ | SPropF, _ | _, SPropF ->
+ user_err Pp.(str "SProp arguments not supported by Program Fixpoint yet.")
+ | PropF, PropF -> "ex", PropF
+ | PropF, TypeF -> "sig", TypeF
+ | TypeF, (PropF|TypeF) -> "sigT", TypeF
+ in
+ let sigma, ty = Evarutil.new_global sigma (lib_ref ("core."^which^".type")) in
+ let uinstance = snd (destRef sigma ty) in
+ let intro = mkRef (lib_ref ("core."^which^".intro"), uinstance) in
+ let p1 = mkRef (lib_ref ("core."^which^".proj1"), uinstance) in
+ let p2 = mkRef (lib_ref ("core."^which^".proj2"), uinstance) in
+ sigma, ty, intro, p1, p2, sigsort
+
let rec telescope sigma l =
let open EConstr in
let open Vars in
match l with
| [] -> assert false
- | [LocalAssum (n, t)] ->
+ | [LocalAssum (n, t), _] ->
sigma, t, [LocalDef (n, mkRel 1, t)], mkRel 1
- | LocalAssum (n, t) :: tl ->
- let sigma, ty, tys, (k, constr) =
+ | (LocalAssum (n, t), tsort) :: tl ->
+ let sigma, ty, _tysort, tys, (k, constr) =
List.fold_left
- (fun (sigma, ty, tys, (k, constr)) decl ->
+ (fun (sigma, ty, tysort, tys, (k, constr)) (decl,sort) ->
let t = RelDecl.get_type decl in
let pred = mkLambda (RelDecl.get_annot decl, t, ty) in
- let sigma, ty = Evarutil.new_global sigma (lib_ref "core.sigT.type") in
- let sigma, intro = Evarutil.new_global sigma (lib_ref "core.sigT.intro") in
+ let sigma, ty, intro, p1, p2, sigsort = get_sigmatypes sigma ~predsort:tysort ~sort in
let sigty = mkApp (ty, [|t; pred|]) in
let intro = mkApp (intro, [|lift k t; lift k pred; mkRel k; constr|]) in
- (sigma, sigty, pred :: tys, (succ k, intro)))
- (sigma, t, [], (2, mkRel 1)) tl
+ (sigma, sigty, sigsort, (pred, p1, p2) :: tys, (succ k, intro)))
+ (sigma, t, tsort, [], (2, mkRel 1)) tl
in
let sigma, last, subst = List.fold_right2
- (fun pred decl (sigma, prev, subst) ->
+ (fun (pred,p1,p2) (decl,_) (sigma, prev, subst) ->
let t = RelDecl.get_type decl in
- let sigma, p1 = Evarutil.new_global sigma (lib_ref "core.sigT.proj1") in
- let sigma, p2 = Evarutil.new_global sigma (lib_ref "core.sigT.proj2") in
let proj1 = applist (p1, [t; pred; prev]) in
let proj2 = applist (p2, [t; pred; prev]) in
(sigma, lift 1 proj2, LocalDef (get_annot decl, proj1, t) :: subst))
(List.rev tys) tl (sigma, mkRel 1, [])
in sigma, ty, (LocalDef (n, last, t) :: subst), constr
- | LocalDef (n, b, t) :: tl ->
+ | (LocalDef (n, b, t), _) :: tl ->
let sigma, ty, subst, term = telescope sigma tl in
sigma, ty, (LocalDef (n, b, t) :: subst), lift 1 term
+let telescope env sigma l =
+ let l, _ = List.fold_right_map (fun d env ->
+ let s = Retyping.get_sort_family_of env sigma (RelDecl.get_type d) in
+ let env = EConstr.push_rel d env in
+ (d, family_of_sort_family s), env) l env
+ in
+ telescope sigma l
+
let nf_evar_context sigma ctx =
List.map (map_constr (fun c -> Evarutil.nf_evar sigma c)) ctx
@@ -94,7 +121,7 @@ let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation =
let top_env = push_rel_context binders_rel env in
let sigma, top_arity = interp_type_evars ~program_mode:true top_env sigma arityc in
let full_arity = it_mkProd_or_LetIn top_arity binders_rel in
- let sigma, argtyp, letbinders, make = telescope sigma binders_rel in
+ let sigma, argtyp, letbinders, make = telescope env sigma binders_rel in
let argname = Id.of_string "recarg" in
let arg = LocalAssum (make_annot (Name argname) Sorts.Relevant, argtyp) in
let binders = letbinders @ [arg] in
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index 5e4f2dcd34..1926faaf0e 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -44,7 +44,7 @@ end
(* Locality stuff *)
let declare_definition ~name ~scope ~kind ?hook_data udecl ce imps =
- let fix_exn = Future.fix_exn_of ce.Proof_global.proof_entry_body in
+ let fix_exn = Future.fix_exn_of ce.proof_entry_body in
let gr = match scope with
| Discharge ->
let () =
diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli
index 606cfade46..54a0c9a7e8 100644
--- a/vernac/declareDef.mli
+++ b/vernac/declareDef.mli
@@ -45,7 +45,7 @@ val declare_definition
-> kind:Decls.definition_object_kind
-> ?hook_data:(Hook.t * UState.t * (Id.t * Constr.t) list)
-> UnivNames.universe_binders
- -> Evd.side_effects Proof_global.proof_entry
+ -> Evd.side_effects Declare.proof_entry
-> Impargs.manual_implicits
-> GlobRef.t
@@ -66,7 +66,7 @@ val prepare_definition : allow_evars:bool ->
?opaque:bool -> ?inline:bool -> poly:bool ->
Evd.evar_map -> UState.universe_decl ->
types:EConstr.t option -> body:EConstr.t ->
- Evd.evar_map * Evd.side_effects Proof_global.proof_entry
+ Evd.evar_map * Evd.side_effects Declare.proof_entry
val prepare_parameter : allow_evars:bool ->
poly:bool -> Evd.evar_map -> UState.universe_decl -> EConstr.types ->
diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml
index c5cbb095ca..8fd6bc7eab 100644
--- a/vernac/declareObl.ml
+++ b/vernac/declareObl.ml
@@ -149,18 +149,8 @@ let declare_obligation prg obl body ty uctx =
if get_shrink_obligations () && not poly then shrink_body body ty
else ([], body, ty, [||])
in
- let body =
- ((body, Univ.ContextSet.empty), Evd.empty_side_effects)
- in
- let ce =
- Proof_global.{ proof_entry_body = Future.from_val ~fix_exn:(fun x -> x) body
- ; proof_entry_secctx = None
- ; proof_entry_type = ty
- ; proof_entry_universes = uctx
- ; proof_entry_opaque = opaque
- ; proof_entry_inline_code = false
- ; proof_entry_feedback = None }
- in
+ let ce = Declare.definition_entry ?types:ty ~opaque ~univs:uctx body in
+
(* ppedrot: seems legit to have obligations as local *)
let constant =
Declare.declare_constant ~name:obl.obl_name
@@ -495,12 +485,11 @@ type obligation_qed_info =
}
let obligation_terminator entries uctx { name; num; auto } =
- let open Proof_global in
match entries with
| [entry] ->
let env = Global.env () in
- let ty = entry.proof_entry_type in
- let body, eff = Future.force entry.proof_entry_body in
+ let ty = entry.Declare.proof_entry_type in
+ let body, eff = Future.force entry.Declare.proof_entry_body in
let (body, cstr) = Safe_typing.inline_private_constants env (body, eff.Evd.seff_private) in
let sigma = Evd.from_ctx uctx in
let sigma = Evd.merge_context_set ~sideff:true Evd.univ_rigid sigma cstr in
@@ -514,7 +503,7 @@ let obligation_terminator entries uctx { name; num; auto } =
let obls, rem = prg.prg_obligations in
let obl = obls.(num) in
let status =
- match obl.obl_status, entry.proof_entry_opaque with
+ match obl.obl_status, entry.Declare.proof_entry_opaque with
| (_, Evar_kinds.Expand), true -> err_not_transp ()
| (true, _), true -> err_not_transp ()
| (false, _), true -> Evar_kinds.Define true
@@ -541,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/declareObl.mli b/vernac/declareObl.mli
index 2a8fa734b3..7d8a112cc6 100644
--- a/vernac/declareObl.mli
+++ b/vernac/declareObl.mli
@@ -76,7 +76,7 @@ type obligation_qed_info =
}
val obligation_terminator
- : Evd.side_effects Proof_global.proof_entry list
+ : Evd.side_effects Declare.proof_entry list
-> UState.t
-> obligation_qed_info -> unit
(** [obligation_terminator] part 2 of saving an obligation *)
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index cf87646905..a6c577a878 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -98,20 +98,11 @@ let () =
(* Util *)
-let define ~poly name sigma c t =
+let define ~poly name sigma c types =
let f = declare_constant ~kind:Decls.(IsDefinition Scheme) in
let univs = Evd.univ_entry ~poly sigma in
- let open Proof_global in
- let kn = f ~name
- (DefinitionEntry
- { proof_entry_body = c;
- proof_entry_secctx = None;
- proof_entry_type = t;
- proof_entry_universes = univs;
- proof_entry_opaque = false;
- proof_entry_inline_code = false;
- proof_entry_feedback = None;
- }) in
+ let entry = Declare.definition_entry ~univs ?types c in
+ let kn = f ~name (DefinitionEntry entry) in
definition_message name;
kn
@@ -412,8 +403,7 @@ let do_mutual_induction_scheme ?(force_mutual=false) lnamedepindsort =
let declare decl fi lrecref =
let decltype = Retyping.get_type_of env0 sigma (EConstr.of_constr decl) in
let decltype = EConstr.to_constr sigma decltype in
- let proof_output = Future.from_val ((decl,Univ.ContextSet.empty),Evd.empty_side_effects) in
- let cst = define ~poly fi sigma proof_output (Some decltype) in
+ let cst = define ~poly fi sigma decl (Some decltype) in
GlobRef.ConstRef cst :: lrecref
in
let _ = List.fold_right2 declare listdecl lrecnames [] in
@@ -534,7 +524,6 @@ let do_combined_scheme name schemes =
schemes
in
let sigma,body,typ = build_combined_scheme (Global.env ()) csts in
- let proof_output = Future.from_val ((body,Univ.ContextSet.empty),Evd.empty_side_effects) in
(* It is possible for the constants to have different universe
polymorphism from each other, however that is only when the user
manually defined at least one of them (as Scheme would pick the
@@ -542,7 +531,7 @@ let do_combined_scheme name schemes =
some other polymorphism they can also manually define the
combined scheme. *)
let poly = Global.is_polymorphic (GlobRef.ConstRef (List.hd csts)) in
- ignore (define ~poly name.v sigma proof_output (Some typ));
+ ignore (define ~poly name.v sigma body (Some typ));
fixpoint_message None [name.v]
(**********************************************************************)
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 7809425a10..42d1a1f3fc 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -383,10 +383,9 @@ let adjust_guardness_conditions const = function
| possible_indexes ->
(* Try all combinations... not optimal *)
let env = Global.env() in
- let open Proof_global in
{ const with
- proof_entry_body =
- Future.chain const.proof_entry_body
+ Declare.proof_entry_body =
+ Future.chain const.Declare.proof_entry_body
(fun ((body, ctx), eff) ->
match Constr.kind body with
| Fix ((nv,0),(_,_,fixdefs as fixdecls)) ->
@@ -404,10 +403,11 @@ let finish_proved env sigma idopt po info =
let name = match idopt with
| None -> name
| Some { CAst.v = save_id } -> check_anonymity name save_id; save_id in
- let fix_exn = Future.fix_exn_of const.proof_entry_body in
+ let fix_exn = Future.fix_exn_of const.Declare.proof_entry_body in
let () = try
let const = adjust_guardness_conditions const compute_guard in
- let should_suggest = const.proof_entry_opaque && Option.is_empty const.proof_entry_secctx in
+ let should_suggest = const.Declare.proof_entry_opaque &&
+ Option.is_empty const.Declare.proof_entry_secctx in
let open DeclareDef in
let r = match scope with
| Discharge ->
@@ -451,7 +451,7 @@ let finish_derived ~f ~name ~idopt ~entries =
in
(* The opacity of [f_def] is adjusted to be [false], as it
must. Then [f] is declared in the global environment. *)
- let f_def = { f_def with Proof_global.proof_entry_opaque = false } in
+ let f_def = { f_def with Declare.proof_entry_opaque = false } in
let f_kind = Decls.(IsDefinition Definition) in
let f_def = Declare.DefinitionEntry f_def in
let f_kn = Declare.declare_constant ~name:f ~kind:f_kind f_def in
@@ -463,17 +463,17 @@ let finish_derived ~f ~name ~idopt ~entries =
let substf c = Vars.replace_vars [f,f_kn_term] c in
(* Extracts the type of the proof of [suchthat]. *)
let lemma_pretype =
- match Proof_global.(lemma_def.proof_entry_type) with
+ match lemma_def.Declare.proof_entry_type with
| Some t -> t
| None -> assert false (* Proof_global always sets type here. *)
in
(* The references of [f] are subsituted appropriately. *)
let lemma_type = substf lemma_pretype in
(* The same is done in the body of the proof. *)
- let lemma_body = Future.chain Proof_global.(lemma_def.proof_entry_body) (fun ((b,ctx),fx) -> (substf b, ctx), fx) in
- let lemma_def = let open Proof_global in
+ let lemma_body = Future.chain lemma_def.Declare.proof_entry_body (fun ((b,ctx),fx) -> (substf b, ctx), fx) in
+ let lemma_def =
{ lemma_def with
- proof_entry_body = lemma_body;
+ Declare.proof_entry_body = lemma_body;
proof_entry_type = Some lemma_type }
in
let lemma_def = Declare.DefinitionEntry lemma_def in
@@ -530,7 +530,7 @@ let save_lemma_admitted_delayed ~proof ~info =
let { Info.hook; scope; impargs; other_thms } = info in
if List.length entries <> 1 then
user_err Pp.(str "Admitted does not support multiple statements");
- let { proof_entry_secctx; proof_entry_type; proof_entry_universes } = List.hd entries in
+ let { Declare.proof_entry_secctx; proof_entry_type; proof_entry_universes } = List.hd entries in
let poly = match proof_entry_universes with
| Entries.Monomorphic_entry _ -> false
| Entries.Polymorphic_entry (_, _) -> true in
diff --git a/vernac/library.ml b/vernac/library.ml
new file mode 100644
index 0000000000..8125c3de35
--- /dev/null
+++ b/vernac/library.ml
@@ -0,0 +1,517 @@
+(************************************************************************)
+(* * 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 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_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_digests : Safe_typing.vodigest;
+ library_extra_univs : Univ.ContextSet.t;
+}
+
+type library_summary = {
+ libsum_name : compilation_unit_name;
+ libsum_digests : Safe_typing.vodigest;
+}
+
+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"
+
+(* 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
+
+ (* 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
+
+ let loaded_libraries () = !libraries_loaded_list
+
+(************************************************************************)
+(** {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_digests = digests;
+ library_extra_univs = univs;
+ }
+
+let mk_summary m = {
+ libsum_name = m.library_name;
+ 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 export -> Declaremods.import_modules ~export @@ List.map (fun m -> MPfile m) 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 export ->
+ List.iter (fun m -> Declaremods.import_module ~export (MPfile m)) modrefl)
+ export
+ end
+ else
+ add_anonymous_leaf (in_require (needed,modrefl,export));
+ ()
+
+(************************************************************************)
+(*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 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 ());
+ } 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..6a32413248
--- /dev/null
+++ b/vernac/library.mli
@@ -0,0 +1,74 @@
+(************************************************************************)
+(* * 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
+
+(** 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
+
+(** 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 *)
+val library_is_loaded : DirPath.t -> bool
+
+ (** - Tell which libraries are loaded *)
+val loaded_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 37fe0df0ee..da14b6e979 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -423,11 +423,11 @@ let solve_by_tac ?loc name evi t poly ctx =
Pfedit.build_constant_by_tactic
~name ~poly ctx evi.evar_hyps evi.evar_concl t in
let env = Global.env () in
- let (body, eff) = Future.force entry.Proof_global.proof_entry_body in
+ let (body, eff) = Future.force entry.Declare.proof_entry_body in
let body = Safe_typing.inline_private_constants env (body, eff.Evd.seff_private) in
let ctx' = Evd.merge_context_set ~sideff:true Evd.univ_rigid (Evd.from_ctx ctx') (snd body) in
Inductiveops.control_only_guard env ctx' (EConstr.of_constr (fst body));
- Some (fst body, entry.Proof_global.proof_entry_type, Evd.evar_universe_context ctx')
+ Some (fst body, entry.Declare.proof_entry_type, Evd.evar_universe_context ctx')
with
| Refiner.FailError (_, s) as exn ->
let _ = CErrors.push exn in
@@ -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/proof_using.ml b/vernac/proof_using.ml
index 094e2c1184..cfb3248c7b 100644
--- a/vernac/proof_using.ml
+++ b/vernac/proof_using.ml
@@ -130,7 +130,7 @@ let suggest_common env ppid used ids_typ skip =
str "should start with one of the following commands:"++spc()++
v 0 (
prlist_with_sep cut (fun x->str"Proof using " ++x++ str". ") !valid_exprs));
- if !Flags.record_aux_file
+ if Aux_file.recording ()
then
let s = string_of_ppcmds (prlist_with_sep (fun _ -> str";") (fun x->x) !valid_exprs) in
record_proof_using s
diff --git a/vernac/record.ml b/vernac/record.ml
index 86745212e7..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
@@ -340,26 +351,17 @@ let declare_projections indsp ctx ?(kind=Decls.StructureComponent) binder_name f
let projtyp =
it_mkProd_or_LetIn (mkProd (x,rp,ccl)) paramdecls in
try
- let open Proof_global in
- let entry = {
- proof_entry_body =
- Future.from_val ((proj, Univ.ContextSet.empty), Evd.empty_side_effects);
- proof_entry_secctx = None;
- proof_entry_type = Some projtyp;
- proof_entry_universes = ctx;
- proof_entry_opaque = false;
- proof_entry_inline_code = false;
- proof_entry_feedback = None } in
+ let entry = Declare.definition_entry ~univs:ctx ~types:projtyp proj in
let kind = Decls.IsDefinition kind in
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;
@@ -413,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;
@@ -446,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;
@@ -463,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
@@ -478,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. *)
@@ -493,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)
@@ -518,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
@@ -584,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);
@@ -688,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..43b58d6d4b 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -171,16 +171,9 @@ let print_loadpath dir =
prlist_with_sep fnl Loadpath.pp l
let print_modules () =
- let opened = Library.opened_libraries ()
- and loaded = Library.loaded_libraries () in
- (* we intersect over opened to preserve the order of opened since *)
- (* non-commutative operations (e.g. visibility) are done at import time *)
- let loaded_opened = List.intersect DirPath.equal opened loaded
- and only_loaded = List.subtract DirPath.equal loaded opened in
- str"Loaded and imported library files: " ++
- pr_vertical_list DirPath.print loaded_opened ++ fnl () ++
- str"Loaded and not imported library files: " ++
- pr_vertical_list DirPath.print only_loaded
+ let loaded = Library.loaded_libraries () in
+ str"Loaded library files: " ++
+ pr_vertical_list DirPath.print loaded
let print_module qid =
@@ -606,6 +599,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"
@@ -844,7 +855,12 @@ let vernac_constraint ~poly l =
(* Modules *)
let vernac_import export refl =
- Library.import_module export refl
+ let import_mod qid =
+ try Declaremods.import_module ~export @@ Nametab.locate_module qid
+ with Not_found ->
+ CErrors.user_err Pp.(str "Cannot find module " ++ pr_qualid qid)
+ in
+ List.iter import_mod refl
let vernac_declare_module export {loc;v=id} binders_ast mty_ast =
(* We check the state of the system (in section, in module type)
@@ -1161,11 +1177,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 +1970,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 +1985,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 +2283,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 +2554,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-05-05 04:37:20 +0000