diff options
Diffstat (limited to 'vernac')
32 files changed, 1191 insertions, 355 deletions
diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml index ab341e4ab8..cb034bdff6 100644 --- a/vernac/assumptions.ml +++ b/vernac/assumptions.ml @@ -313,9 +313,15 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t = if cb.const_typing_flags.check_guarded then accu else let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in - ContextObjectMap.add (Axiom (Guarded kn, l)) Constr.mkProp accu + ContextObjectMap.add (Axiom (Guarded obj, l)) Constr.mkProp accu in - if not (Declareops.constant_has_body cb) || not cb.const_typing_flags.check_universes then + let accu = + if cb.const_typing_flags.check_universes then accu + else + let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in + ContextObjectMap.add (Axiom (TypeInType obj, l)) Constr.mkProp accu + in + if not (Declareops.constant_has_body cb) then let t = type_of_constant cb in let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in ContextObjectMap.add (Axiom (Constant kn,l)) t accu @@ -329,10 +335,26 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t = accu | IndRef (m,_) | ConstructRef ((m,_),_) -> let mind = lookup_mind m in - if mind.mind_typing_flags.check_guarded then - accu - else + let accu = + if mind.mind_typing_flags.check_positive then accu + else + let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in + ContextObjectMap.add (Axiom (Positive m, l)) Constr.mkProp accu + in + let accu = + if mind.mind_typing_flags.check_guarded then accu + else + let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in + ContextObjectMap.add (Axiom (Guarded obj, l)) Constr.mkProp accu + in + let accu = + if mind.mind_typing_flags.check_universes then accu + else + let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in + ContextObjectMap.add (Axiom (TypeInType obj, l)) Constr.mkProp accu + in + 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 (Positive m, l)) Constr.mkProp accu - in - GlobRef.Map_env.fold fold graph ContextObjectMap.empty + 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/classes.ml b/vernac/classes.ml index efe452d5f1..d5f5656e1d 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -28,9 +28,7 @@ module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration (*i*) -open Decl_kinds - -let set_typeclass_transparency c local b = +let set_typeclass_transparency c local b = Hints.add_hints ~local [typeclasses_db] (Hints.HintsTransparencyEntry (Hints.HintsReferences [c], b)) @@ -179,7 +177,7 @@ let discharge_class (_,cl) = let open CVars in let repl = Lib.replacement_context () in let rel_of_variable_context ctx = List.fold_right - ( fun (decl,_) (ctx', subst) -> + ( fun decl (ctx', subst) -> let decl' = decl |> NamedDecl.map_constr (substn_vars 1 subst) |> NamedDecl.to_rel_decl in (decl' :: ctx', NamedDecl.get_id decl :: subst) ) ctx ([], []) in @@ -527,7 +525,7 @@ let do_instance_program env env' sigma ?hook ~global ~poly cty k u ctx ctx' pri let interp_instance_context ~program_mode env ctx ~generalize pl tclass = let sigma, decl = Constrexpr_ops.interp_univ_decl_opt env pl in let tclass = - if generalize then CAst.make @@ CGeneralization (Implicit, Some AbsPi, tclass) + if generalize then CAst.make @@ CGeneralization (Glob_term.Implicit, Some AbsPi, tclass) else tclass in let sigma, (impls, ((env', ctx), imps)) = interp_context_evars ~program_mode env sigma ctx in diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index d59d471d5f..e3f90ab98c 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -59,7 +59,7 @@ match scope with let sigma = Evd.from_env env in let () = Classes.declare_instance env sigma None true r in let () = if is_coe then Class.try_add_new_coercion r ~local:true ~poly:false in - (r,Univ.Instance.empty,true) + (r,Univ.Instance.empty) | Global local -> let do_instance = should_axiom_into_instance kind in @@ -84,7 +84,7 @@ match scope with | Polymorphic_entry (_, univs) -> Univ.UContext.instance univs | Monomorphic_entry _ -> Univ.Instance.empty in - (gr,inst,Lib.is_modtype_strict ()) + (gr,inst) let interp_assumption ~program_mode sigma env impls c = let sigma, (ty, impls) = interp_type_evars_impls ~program_mode env sigma ~impls c in @@ -98,14 +98,13 @@ let next_uctx = | Monomorphic_entry _ -> empty_uctx let declare_assumptions idl is_coe ~scope ~poly ~kind typ uctx pl imps nl = - let refs, status, _ = - List.fold_left (fun (refs,status,uctx) id -> - let ref',u',status' = - declare_assumption is_coe ~scope ~poly ~kind typ uctx pl imps false nl id in - (ref',u')::refs, status' && status, next_uctx uctx) - ([],true,uctx) idl + let refs, _ = + List.fold_left (fun (refs,uctx) id -> + let ref = declare_assumption is_coe ~scope ~poly ~kind typ uctx pl imps Glob_term.Explicit nl id in + ref::refs, next_uctx uctx) + ([],uctx) idl in - List.rev refs, status + List.rev refs let maybe_error_many_udecls = function @@ -178,15 +177,17 @@ let do_assumptions ~program_mode ~poly ~scope ~kind nl l = let sigma = Evd.restrict_universe_context sigma uvars in let uctx = Evd.check_univ_decl ~poly sigma udecl in let ubinders = Evd.universe_binders sigma in - pi2 (List.fold_left (fun (subst,status,uctx) ((is_coe,idl),typ,imps) -> + let _, _ = List.fold_left (fun (subst,uctx) ((is_coe,idl),typ,imps) -> let typ = replace_vars subst typ in - let refs, status' = declare_assumptions idl is_coe ~poly ~scope ~kind typ uctx ubinders imps nl in + let refs = declare_assumptions idl is_coe ~poly ~scope ~kind typ uctx ubinders imps nl in let subst' = List.map2 (fun {CAst.v=id} (c,u) -> (id, Constr.mkRef (c,u))) idl refs in - subst'@subst, status' && status, next_uctx uctx) - ([], true, uctx) l) + subst'@subst, next_uctx uctx) + ([], uctx) l + in + () let do_primitive id prim typopt = if Lib.sections_are_opened () then @@ -270,41 +271,43 @@ let context ~poly l = Monomorphic_entry Univ.ContextSet.empty end in - let fn status (name, b, t) = + let fn (name, b, t) = let b, t = Option.map (EConstr.to_constr sigma) b, EConstr.to_constr sigma t in if Lib.is_modtype () && not (Lib.sections_are_opened ()) then (* Declare the universe context once *) let kind = Decls.(IsAssumption Logical) in let decl = match b with - | None -> - Declare.ParameterEntry (None,(t,univs),None) - | Some b -> - let entry = Declare.definition_entry ~univs ~types:t b in - Declare.DefinitionEntry entry + | None -> + Declare.ParameterEntry (None,(t,univs),None) + | Some b -> + let entry = Declare.definition_entry ~univs ~types:t b in + Declare.DefinitionEntry entry in let cst = Declare.declare_constant ~name ~kind decl in let env = Global.env () in Classes.declare_instance env sigma (Some Hints.empty_hint_info) true (GlobRef.ConstRef cst); - status + () else let test x = match x.CAst.v with - | Some (Name id',_) -> Id.equal name id' - | _ -> false + | Some (Name id',_) -> Id.equal name id' + | _ -> false in - let impl = List.exists test impls in + let impl = if List.exists test impls then Glob_term.Implicit else Glob_term.Explicit in let scope = if Lib.sections_are_opened () then DeclareDef.Discharge else DeclareDef.Global ImportDefaultBehavior in - let nstatus = match b with + match b with | None -> - pi3 (declare_assumption false ~scope ~poly ~kind:Decls.Context t univs UnivNames.empty_binders [] impl - Declaremods.NoInline (CAst.make name)) + let _, _ = + declare_assumption false ~scope ~poly ~kind:Decls.Context t + univs UnivNames.empty_binders [] impl + Declaremods.NoInline (CAst.make name) + in + () | Some b -> let entry = Declare.definition_entry ~univs ~types:t b in let _gr = DeclareDef.declare_definition ~name ~scope:DeclareDef.Discharge ~kind:Decls.Definition UnivNames.empty_binders entry [] in - Lib.sections_are_opened () || Lib.is_modtype_strict () - in - status && nstatus + () in - List.fold_left fn true (List.rev ctx) + List.iter fn (List.rev ctx) diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli index 028ed39656..2715bd8305 100644 --- a/vernac/comAssumption.mli +++ b/vernac/comAssumption.mli @@ -21,7 +21,7 @@ val do_assumptions -> kind:Decls.assumption_object_kind -> Declaremods.inline -> (ident_decl list * constr_expr) with_coercion list - -> bool + -> unit (** returns [false] if the assumption is neither local to a section, nor in a module type and meant to be instantiated. *) @@ -34,10 +34,10 @@ val declare_assumption -> Entries.universes_entry -> UnivNames.universe_binders -> Impargs.manual_implicits - -> bool (** implicit *) + -> Glob_term.binding_kind -> Declaremods.inline -> variable CAst.t - -> GlobRef.t * Univ.Instance.t * bool + -> GlobRef.t * Univ.Instance.t (** Context command *) @@ -46,6 +46,6 @@ val declare_assumption val context : poly:bool -> local_binder_expr list - -> bool + -> unit val do_primitive : lident -> CPrimitives.op_or_type -> constr_expr option -> unit 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/comFixpoint.ml b/vernac/comFixpoint.ml index 74c9bc2886..b6843eab33 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -323,11 +323,6 @@ let adjust_rec_order ~structonly binders rec_order = in Option.map (extract_decreasing_argument ~structonly) rec_order -let check_safe () = - let open Declarations in - let flags = Environ.typing_flags (Global.env ()) in - flags.check_universes && flags.check_guarded - let do_fixpoint_common (fixl : Vernacexpr.fixpoint_expr list) = let fixl = List.map (fun fix -> Vernacexpr.{ fix @@ -339,13 +334,11 @@ let do_fixpoint_common (fixl : Vernacexpr.fixpoint_expr list) = let do_fixpoint_interactive ~scope ~poly l : Lemmas.t = let fixl, ntns, fix, possible_indexes = do_fixpoint_common l in let lemma = declare_fixpoint_interactive_generic ~indexes:possible_indexes ~scope ~poly fix ntns in - if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else (); lemma let do_fixpoint ~scope ~poly l = let fixl, ntns, fix, possible_indexes = do_fixpoint_common l in - declare_fixpoint_generic ~indexes:possible_indexes ~scope ~poly fix ntns; - if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else () + declare_fixpoint_generic ~indexes:possible_indexes ~scope ~poly fix ntns let do_cofixpoint_common (fixl : Vernacexpr.cofixpoint_expr list) = let fixl = List.map (fun fix -> {fix with Vernacexpr.rec_order = None}) fixl in @@ -355,10 +348,8 @@ let do_cofixpoint_common (fixl : Vernacexpr.cofixpoint_expr list) = let do_cofixpoint_interactive ~scope ~poly l = let cofix, ntns = do_cofixpoint_common l in let lemma = declare_fixpoint_interactive_generic ~scope ~poly cofix ntns in - if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else (); lemma let do_cofixpoint ~scope ~poly l = let cofix, ntns = do_cofixpoint_common l in - declare_fixpoint_generic ~scope ~poly cofix ntns; - if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else () + declare_fixpoint_generic ~scope ~poly cofix ntns diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 664010c917..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; @@ -567,9 +611,7 @@ let do_mutual_inductive ~template udecl indl ~cumulative ~poly ~private_ind ~uni (* Declare the possible notations of inductive types *) List.iter (Metasyntax.add_notation_interpretation (Global.env ())) ntns; (* Declare the coercions *) - List.iter (fun qid -> Class.try_add_new_coercion (Nametab.locate qid) ~local:false ~poly) coes; - (* If positivity is assumed declares itself as unsafe. *) - if Environ.deactivated_guard (Global.env ()) then Feedback.feedback Feedback.AddedAxiom else () + List.iter (fun qid -> Class.try_add_new_coercion (Nametab.locate qid) ~local:false ~poly) coes (** Prepare a "match" template for a given inductive type. For each branch of the match, we list the constructor name 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 c6e68effd7..3497e6369f 100644 --- a/vernac/comProgramFixpoint.ml +++ b/vernac/comProgramFixpoint.ml @@ -292,7 +292,7 @@ let do_program_recursive ~scope ~poly fixkind fixl = let ntns = List.map_append (fun { Vernacexpr.notations } -> notations ) fixl in Obligations.add_mutual_definitions defs ~poly ~scope ~kind ~univdecl:pl ctx ntns fixkind -let do_program_fixpoint ~scope ~poly l = +let do_fixpoint ~scope ~poly l = let g = List.map (fun { Vernacexpr.rec_order } -> rec_order) l in match g, l with | [Some { CAst.v = CWfRec (n,r) }], @@ -322,19 +322,9 @@ let do_program_fixpoint ~scope ~poly l = do_program_recursive ~scope ~poly fixkind l | _, _ -> - user_err ~hdr:"do_program_fixpoint" + user_err ~hdr:"do_fixpoint" (str "Well-founded fixpoints not allowed in mutually recursive blocks") -let check_safe () = - let open Declarations in - let flags = Environ.typing_flags (Global.env ()) in - flags.check_universes && flags.check_guarded - -let do_fixpoint ~scope ~poly l = - do_program_fixpoint ~scope ~poly l; - if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else () - let do_cofixpoint ~scope ~poly fixl = let fixl = List.map (fun fix -> { fix with Vernacexpr.rec_order = None }) fixl in - do_program_recursive ~scope ~poly DeclareObl.IsCoFixpoint fixl; - if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else () + do_program_recursive ~scope ~poly DeclareObl.IsCoFixpoint fixl 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/dune b/vernac/dune index 45b567d631..ba361b1377 100644 --- a/vernac/dune +++ b/vernac/dune @@ -5,12 +5,4 @@ (wrapped false) (libraries tactics parsing)) -(rule - (targets g_proofs.ml) - (deps (:mlg-file g_proofs.mlg)) - (action (run coqpp %{mlg-file}))) - -(rule - (targets g_vernac.ml) - (deps (:mlg-file g_vernac.mlg)) - (action (run coqpp %{mlg-file}))) +(coq.pp (modules g_proofs g_vernac)) diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index ad5d98669d..8a94a010a0 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -72,16 +72,29 @@ let parse_compat_version = let open Flags in function CErrors.user_err ~hdr:"get_compat_version" Pp.(str "Unknown compatibility version \"" ++ str s ++ str "\".") +(* For now we just keep the top-level location of the whole + vernacular, that is to say, including attributes and control flags; + this is not very convenient for advanced clients tho, so in the + future it'd be cool to actually locate the attributes and control + flags individually too. *) +let add_control_flag ~loc ~flag { CAst.v = cmd } = + CAst.make ~loc { cmd with control = flag :: cmd.control } + } GRAMMAR EXTEND Gram GLOBAL: vernac_control quoted_attributes gallina_ext noedit_mode subprf; vernac_control: FIRST - [ [ IDENT "Time"; c = vernac_control -> { CAst.make ~loc @@ VernacTime (false,c) } - | IDENT "Redirect"; s = ne_string; c = vernac_control -> { CAst.make ~loc @@ VernacRedirect (s, c) } - | IDENT "Timeout"; n = natural; v = vernac_control -> { CAst.make ~loc @@ VernacTimeout(n,v) } - | IDENT "Fail"; v = vernac_control -> { CAst.make ~loc @@ VernacFail v } - | v = decorated_vernac -> { let (f, v) = v in CAst.make ~loc @@ VernacExpr(f, v) } ] + [ [ IDENT "Time"; c = vernac_control -> + { add_control_flag ~loc ~flag:(ControlTime false) c } + | IDENT "Redirect"; s = ne_string; c = vernac_control -> + { add_control_flag ~loc ~flag:(ControlRedirect s) c } + | IDENT "Timeout"; n = natural; c = vernac_control -> + { add_control_flag ~loc ~flag:(ControlTimeout n) c } + | IDENT "Fail"; c = vernac_control -> + { add_control_flag ~loc ~flag:ControlFail c } + | v = decorated_vernac -> + { let (attrs, expr) = v in CAst.make ~loc { control = []; attrs; expr = expr } } ] ] ; decorated_vernac: @@ -519,7 +532,7 @@ END let only_starredidentrefs = Pcoq.Entry.of_parser "test_only_starredidentrefs" - (fun strm -> + (fun _ strm -> let rec aux n = match Util.stream_nth n strm with | KEYWORD "." -> () @@ -1035,6 +1048,7 @@ GRAMMAR EXTEND Gram | IDENT "Coercion"; IDENT "Paths"; s = class_rawexpr; t = class_rawexpr -> { PrintCoercionPaths (s,t) } | IDENT "Canonical"; IDENT "Projections" -> { PrintCanonicalConversions } + | IDENT "Typing"; IDENT "Flags" -> { PrintTypingFlags } | IDENT "Tables" -> { PrintTables } | IDENT "Options" -> { PrintTables (* A Synonymous to Tables *) } | IDENT "Hint" -> { PrintHintGoal } diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index 23a8bf20a3..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] (**********************************************************************) @@ -553,7 +542,7 @@ let declare_default_schemes kn = let mib = Global.lookup_mind kn in let n = Array.length mib.mind_packets in if !elim_flag && (mib.mind_finite <> Declarations.BiFinite || !bifinite_elim_flag) - && mib.mind_typing_flags.check_guarded then + && mib.mind_typing_flags.check_positive then declare_induction_schemes kn; if !case_flag then map_inductive_block declare_one_case_analysis_scheme kn n; if is_eq_flag() then try_declare_beq_scheme kn; diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 6a754a0cde..42d1a1f3fc 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -258,7 +258,7 @@ let save_remaining_recthms env sigma ~poly ~scope ~udecl uctx body opaq i { Rect let open DeclareDef in (match scope with | Discharge -> - let impl = false in (* copy values from Vernacentries *) + let impl = Glob_term.Explicit in let univs = match univs with | Polymorphic_entry (_, univs) -> (* What is going on here? *) @@ -336,8 +336,7 @@ let finish_admitted env sigma ~name ~poly ~scope pe ctx hook ~udecl impargs othe let () = Declare.assumption_message name in Declare.declare_univ_binders (GlobRef.ConstRef kn) (UState.universe_binders ctx); (* This takes care of the implicits and hook for the current constant*) - process_recthms ?fix_exn:None ?hook env sigma ctx ~udecl ~poly ~scope:(Global local) (GlobRef.ConstRef kn) impargs other_thms; - Feedback.feedback Feedback.AddedAxiom + process_recthms ?fix_exn:None ?hook env sigma ctx ~udecl ~poly ~scope:(Global local) (GlobRef.ConstRef kn) impargs other_thms let save_lemma_admitted ~(lemma : t) : unit = (* Used for printing in recthms *) @@ -384,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)) -> @@ -405,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 -> @@ -452,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 @@ -464,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 @@ -531,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..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 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/ppvernac.ml b/vernac/ppvernac.ml index 0eb0b1b6f6..f91983d31c 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -514,6 +514,8 @@ let string_of_theorem_kind = let open Decls in function ++ pr_class_rawexpr t | PrintCanonicalConversions -> keyword "Print Canonical Structures" + | PrintTypingFlags -> + keyword "Print Typing Flags" | PrintTables -> keyword "Print Tables" | PrintHintGoal -> @@ -1266,6 +1268,16 @@ let string_of_definition_object_kind = let open Decls in function | VernacEndSubproof -> return (str "}") +let pr_control_flag (p : control_flag) = + let w = match p with + | ControlTime _ -> keyword "Time" + | ControlRedirect s -> keyword "Redirect" ++ spc() ++ qs s + | ControlTimeout n -> keyword "Timeout " ++ int n + | ControlFail -> keyword "Fail" in + w ++ spc () + +let pr_vernac_control flags = Pp.prlist pr_control_flag flags + let rec pr_vernac_flag (k, v) = let k = keyword k in let open Attributes in @@ -1281,19 +1293,11 @@ let pr_vernac_attributes = | [] -> mt () | flags -> str "#[" ++ pr_vernac_flags flags ++ str "]" ++ cut () - let rec pr_vernac_control v = - let return = tag_vernac v in - match v.v with - | VernacExpr (f, v') -> pr_vernac_attributes f ++ pr_vernac_expr v' ++ sep_end v' - | VernacTime (_,v) -> - return (keyword "Time" ++ spc() ++ pr_vernac_control v) - | VernacRedirect (s, v) -> - return (keyword "Redirect" ++ spc() ++ qs s ++ spc() ++ pr_vernac_control v) - | VernacTimeout(n,v) -> - return (keyword "Timeout " ++ int n ++ spc() ++ pr_vernac_control v) - | VernacFail v-> - return (keyword "Fail" ++ spc() ++ pr_vernac_control v) - - let pr_vernac v = - try pr_vernac_control v - with e -> CErrors.print e +let pr_vernac ({v = {control; attrs; expr}} as v) = + try + tag_vernac v + (pr_vernac_control control ++ + pr_vernac_attributes attrs ++ + pr_vernac_expr expr ++ + sep_end expr) + with e -> CErrors.print e 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/pvernac.ml b/vernac/pvernac.ml index da28e260b3..826e88cabf 100644 --- a/vernac/pvernac.ml +++ b/vernac/pvernac.ml @@ -67,7 +67,7 @@ module Vernac_ = let command_entry = Pcoq.Entry.of_parser "command_entry" - (fun strm -> Pcoq.Entry.parse_token_stream (select_tactic_entry !command_entry_ref) strm) + (fun _ strm -> Pcoq.Entry.parse_token_stream (select_tactic_entry !command_entry_ref) strm) end 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 9af8d8b67c..3d14e8d510 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -604,8 +604,25 @@ let vernac_assumption ~atts discharge kind l nl = match scope with | DeclareDef.Global _ -> Dumpglob.dump_definition lid false "ax" | DeclareDef.Discharge -> Dumpglob.dump_definition lid true "var") idl) l; - let status = ComAssumption.do_assumptions ~poly:atts.polymorphic ~program_mode:atts.program ~scope ~kind nl l in - if not status then Feedback.feedback Feedback.AddedAxiom + 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 @@ -1074,9 +1091,6 @@ let vernac_declare_instance ~atts id bl inst pri = let global = not (make_section_locality locality) in Classes.declare_new_instance ~program_mode:program ~global ~poly id bl inst pri -let vernac_context ~poly l = - if not (ComAssumption.context ~poly l) then Feedback.feedback Feedback.AddedAxiom - let vernac_existing_instance ~section_local insts = let glob = not section_local in List.iter (fun (id, info) -> Classes.existing_instance glob id (Some info)) insts @@ -1165,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 *) @@ -1728,6 +1742,30 @@ let () = optread = Nativenorm.get_profiling_enabled; optwrite = Nativenorm.set_profiling_enabled } +let _ = + declare_bool_option + { optdepr = false; + optname = "guard checking"; + optkey = ["Guard"; "Checking"]; + optread = (fun () -> (Global.typing_flags ()).Declarations.check_guarded); + optwrite = (fun b -> Global.set_check_guarded b) } + +let _ = + declare_bool_option + { optdepr = false; + optname = "positivity/productivity checking"; + optkey = ["Positivity"; "Checking"]; + optread = (fun () -> (Global.typing_flags ()).Declarations.check_positive); + optwrite = (fun b -> Global.set_check_positive b) } + +let _ = + declare_bool_option + { optdepr = false; + optname = "universes checking"; + optkey = ["Universe"; "Checking"]; + optread = (fun () -> (Global.typing_flags ()).Declarations.check_universes); + optwrite = (fun b -> Global.set_check_universes b) } + let vernac_set_strategy ~local l = let local = Option.default false local in let glob_ref r = @@ -1932,10 +1970,11 @@ let print_about_hyp_globs ~pstate ?loc ref_or_by_not udecl glopt = let vernac_print ~pstate ~atts = let sigma, env = get_current_or_global_context ~pstate in 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 @@ -1948,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() @@ -2246,14 +2285,40 @@ 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 | None -> (e, Option.cata (Loc.add_loc info) info loc) | Some l -> (e, info) -exception End_of_input +let mk_time_header = + (* Drop the time header to print the command, we should indeed use a + different mechanism to `-time` commands than the current hack of + adding a time control to the AST. *) + let pr_time_header vernac = + let vernac = match vernac with + | { v = { control = ControlTime _ :: control; attrs; expr }; loc } -> + CAst.make ?loc { control; attrs; expr } + | _ -> vernac + in + Topfmt.pr_cmd_header vernac + in + fun vernac -> Lazy.from_fun (fun () -> pr_time_header vernac) + +let interp_control_flag ~time_header (f : control_flag) ~st + (fn : st:Vernacstate.t -> Vernacstate.LemmaStack.t option) = + match f with + | ControlFail -> + with_fail ~st (fun () -> fn ~st); + st.Vernacstate.lemmas + | ControlTimeout timeout -> + vernac_timeout ~timeout (fun () -> fn ~st) () + | ControlTime batch -> + let header = if batch then Lazy.force time_header else Pp.mt () in + System.with_time ~batch ~header (fun () -> fn ~st) () + | ControlRedirect s -> + Topfmt.with_output_to_file s (fun () -> fn ~st) () (* EJGA: We may remove this, only used twice below *) let vernac_require_open_lemma ~stack f = @@ -2439,7 +2504,7 @@ let rec translate_vernac ~atts v = let open Vernacextend in match v with | VernacDeclareInstance (id, bl, inst, info) -> VtDefault(fun () -> vernac_declare_instance ~atts id bl inst info) | VernacContext sup -> - VtDefault(fun () -> vernac_context ~poly:(only_polymorphism atts) sup) + VtDefault(fun () -> ComAssumption.context ~poly:(only_polymorphism atts) sup) | VernacExistingInstance insts -> VtDefault(fun () -> with_section_locality ~atts vernac_existing_instance insts) | VernacExistingClass id -> @@ -2491,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)) @@ -2614,7 +2679,7 @@ let rec translate_vernac ~atts v = let open Vernacextend in match v with * is the outdated/deprecated "Local" attribute of some vernacular commands * still parsed as the obsolete_locality grammar entry for retrocompatibility. * loc is the Loc.t of the vernacular command being interpreted. *) -and interp_expr ?proof ~atts ~st c = +and interp_expr ~atts ~st c = let stack = st.Vernacstate.lemmas in vernac_pperr_endline (fun () -> str "interpreting: " ++ Ppvernac.pr_vernac_expr c); match c with @@ -2644,6 +2709,8 @@ and interp_expr ?proof ~atts ~st c = without a considerable amount of refactoring. *) and vernac_load ~verbosely fname = + let exception End_of_input in + (* Note that no proof should be open here, so the state here is just token for now *) let st = Vernacstate.freeze_interp_state ~marshallable:false in let fname = @@ -2664,7 +2731,7 @@ and vernac_load ~verbosely fname = try let proof_mode = Option.map (fun _ -> get_default_proof_mode ()) stack in let stack = - v_mod (interp_control ?proof:None ~st:{ st with Vernacstate.lemmas = stack }) + v_mod (interp_control ~st:{ st with Vernacstate.lemmas = stack }) (parse_sentence proof_mode input) in load_loop ~stack with @@ -2677,23 +2744,36 @@ and vernac_load ~verbosely fname = CErrors.user_err Pp.(str "Files processed by Load cannot leave open proofs."); () -and interp_control ?proof ~st v = match v with - | { v=VernacExpr (atts, cmd) } -> - let before_univs = Global.universes () in - let pstack = interp_expr ?proof ~atts ~st cmd in - if before_univs == Global.universes () then pstack - else Option.map (Vernacstate.LemmaStack.map_top_pstate ~f:Proof_global.update_global_env) pstack - | { v=VernacFail v } -> - with_fail ~st (fun () -> interp_control ?proof ~st v); - st.Vernacstate.lemmas - | { v=VernacTimeout (timeout,v) } -> - vernac_timeout ~timeout (interp_control ?proof ~st) v - | { v=VernacRedirect (s, v) } -> - Topfmt.with_output_to_file s (interp_control ?proof ~st) v - | { v=VernacTime (batch, cmd) }-> - let header = if batch then Topfmt.pr_cmd_header cmd else Pp.mt () in - System.with_time ~batch ~header (interp_control ?proof ~st) cmd - +and interp_control ~st ({ v = cmd } as vernac) = + let time_header = mk_time_header vernac in + List.fold_right (fun flag fn -> interp_control_flag ~time_header flag fn) + cmd.control + (fun ~st -> + let before_univs = Global.universes () in + let pstack = interp_expr ~atts:cmd.attrs ~st cmd.expr in + if before_univs == Global.universes () then pstack + else Option.map (Vernacstate.LemmaStack.map_top_pstate ~f:Proof_global.update_global_env) pstack) + ~st + +(* Interpreting a possibly delayed proof *) +let interp_qed_delayed ~proof ~info ~st pe : Vernacstate.LemmaStack.t option = + let stack = st.Vernacstate.lemmas in + let stack = Option.cata (fun stack -> snd @@ Vernacstate.LemmaStack.pop stack) None stack in + let () = match pe with + | Admitted -> + save_lemma_admitted_delayed ~proof ~info + | Proved (_,idopt) -> + save_lemma_proved_delayed ~proof ~info ~idopt in + stack + +let interp_qed_delayed_control ~proof ~info ~st ~control { loc; v=pe } = + let time_header = mk_time_header (CAst.make ?loc { control; attrs = []; expr = VernacEndProof pe }) in + List.fold_right (fun flag fn -> interp_control_flag ~time_header flag fn) + control + (fun ~st -> interp_qed_delayed ~proof ~info ~st pe) + ~st + +(* General interp with management of state *) let () = declare_int_option { optdepr = false; @@ -2703,11 +2783,11 @@ let () = optwrite = ((:=) default_timeout) } (* Be careful with the cache here in case of an exception. *) -let interp ?(verbosely=true) ~st cmd = +let interp_gen ~verbosely ~st ~interp_fn cmd = Vernacstate.unfreeze_interp_state st; try vernac_timeout (fun st -> let v_mod = if verbosely then Flags.verbosely else Flags.silently in - let ontop = v_mod (interp_control ~st) cmd in + let ontop = v_mod (interp_fn ~st) cmd in Vernacstate.Proof_global.set ontop [@ocaml.warning "-3"]; Vernacstate.freeze_interp_state ~marshallable:false ) st @@ -2717,18 +2797,10 @@ let interp ?(verbosely=true) ~st cmd = Vernacstate.invalidate_cache (); iraise exn -let interp_qed_delayed_proof ~proof ~info ~st ?loc pe : Vernacstate.t = - let stack = st.Vernacstate.lemmas in - let stack = Option.cata (fun stack -> snd @@ Vernacstate.LemmaStack.pop stack) None stack in - try - let () = match pe with - | Admitted -> - save_lemma_admitted_delayed ~proof ~info - | Proved (_,idopt) -> - save_lemma_proved_delayed ~proof ~info ~idopt in - { st with Vernacstate.lemmas = stack } - with exn -> - let exn = CErrors.push exn in - let exn = locate_if_not_already ?loc exn in - Vernacstate.invalidate_cache (); - iraise exn +(* Regular interp *) +let interp ?(verbosely=true) ~st cmd = + interp_gen ~verbosely ~st ~interp_fn:interp_control cmd + +let interp_qed_delayed_proof ~proof ~info ~st ~control pe : Vernacstate.t = + interp_gen ~verbosely:false ~st + ~interp_fn:(interp_qed_delayed_control ~proof ~info ~control) pe diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli index e618cdcefe..e65f9d3cfe 100644 --- a/vernac/vernacentries.mli +++ b/vernac/vernacentries.mli @@ -17,8 +17,8 @@ val interp_qed_delayed_proof : proof:Proof_global.proof_object -> info:Lemmas.Info.t -> st:Vernacstate.t - -> ?loc:Loc.t - -> Vernacexpr.proof_end + -> control:Vernacexpr.control_flag list + -> Vernacexpr.proof_end CAst.t -> Vernacstate.t (** [with_fail ~st f] runs [f ()] and expects it to fail, otherwise it fails. *) diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index 0968632c2d..b712d7e264 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -24,6 +24,7 @@ type goal_reference = | GoalId of Id.t type printable = + | PrintTypingFlags | PrintTables | PrintFullContext | PrintSectionContext of qualid @@ -169,7 +170,7 @@ type inductive_expr = type one_inductive_expr = lident * local_binder_expr list * constr_expr option * constructor_expr list -type typeclass_constraint = name_decl * Decl_kinds.binding_kind * constr_expr +type typeclass_constraint = name_decl * Glob_term.binding_kind * constr_expr and typeclass_context = typeclass_constraint list type proof_expr = @@ -414,12 +415,17 @@ type nonrec vernac_expr = (* For extension *) | VernacExtend of extend_name * Genarg.raw_generic_argument list -type vernac_control_r = - | VernacExpr of Attributes.vernac_flags * vernac_expr +type control_flag = + | ControlTime of bool (* boolean is true when the `-time` batch-mode command line flag was set. the flag is used to print differently in `-time` vs `Time foo` *) - | VernacTime of bool * vernac_control - | VernacRedirect of string * vernac_control - | VernacTimeout of int * vernac_control - | VernacFail of vernac_control + | ControlRedirect of string + | ControlTimeout of int + | ControlFail + +type vernac_control_r = + { control : control_flag list + ; attrs : Attributes.vernac_flags + ; expr : vernac_expr + } and vernac_control = vernac_control_r CAst.t diff --git a/vernac/vernacprop.ml b/vernac/vernacprop.ml index 747998c6cc..903a28e953 100644 --- a/vernac/vernacprop.ml +++ b/vernac/vernacprop.ml @@ -13,47 +13,26 @@ open Vernacexpr -let rec under_control v = v |> CAst.with_val (function - | VernacExpr (_, c) -> c - | VernacRedirect (_,c) - | VernacTime (_,c) - | VernacFail c - | VernacTimeout (_,c) -> under_control c - ) - -let rec has_Fail v = v |> CAst.with_val (function - | VernacExpr _ -> false - | VernacRedirect (_,c) - | VernacTime (_,c) - | VernacTimeout (_,c) -> has_Fail c - | VernacFail _ -> true) +(* Does this vernacular involve Fail? *) +let has_Fail { CAst.v } = List.mem ControlFail v.control (* Navigation commands are allowed in a coqtop session but not in a .v file *) -let is_navigation_vernac_expr = function +let is_navigation_vernac = function | VernacResetInitial | VernacResetName _ | VernacBack _ -> true | _ -> false -let is_navigation_vernac c = - is_navigation_vernac_expr (under_control c) - -let rec is_deep_navigation_vernac v = v |> CAst.with_val (function - | VernacTime (_,c) -> is_deep_navigation_vernac c - | VernacRedirect (_, c) - | VernacTimeout (_, c) | VernacFail c -> is_navigation_vernac c - | VernacExpr _ -> false) - (* NB: Reset is now allowed again as asked by A. Chlipala *) -let is_reset = CAst.with_val (function - | VernacExpr ( _, VernacResetInitial) - | VernacExpr (_, VernacResetName _) -> true - | _ -> false) +let is_reset = function + | VernacResetInitial + | VernacResetName _ -> true + | _ -> false -let is_debug cmd = match under_control cmd with +let is_debug = function | VernacSetOption (_, ["Ltac";"Debug"], _) -> true | _ -> false -let is_undo cmd = match under_control cmd with +let is_undo = function | VernacUndo _ | VernacUndoTo _ -> true | _ -> false diff --git a/vernac/vernacprop.mli b/vernac/vernacprop.mli index 8875b86d94..320878e401 100644 --- a/vernac/vernacprop.mli +++ b/vernac/vernacprop.mli @@ -13,16 +13,9 @@ open Vernacexpr -(* Return the vernacular command below control (Time, Timeout, Redirect, Fail). - Beware that Fail can change many properties of the underlying command, since - a success of Fail means the command was backtracked over. *) -val under_control : vernac_control -> vernac_expr - val has_Fail : vernac_control -> bool - -val is_navigation_vernac : vernac_control -> bool -val is_deep_navigation_vernac : vernac_control -> bool -val is_reset : vernac_control -> bool -val is_debug : vernac_control -> bool -val is_undo : vernac_control -> bool +val is_navigation_vernac : vernac_expr -> bool +val is_reset : vernac_expr -> bool +val is_debug : vernac_expr -> bool +val is_undo : vernac_expr -> bool |