From d437078a4ca82f7ca6d19be5ee9452359724f9a0 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Fri, 15 Sep 2017 15:46:30 +0200 Subject: Use Maps and ids for universe binders Before sometimes there were lists and strings. --- vernac/classes.ml | 4 ++-- vernac/command.ml | 2 +- vernac/obligations.ml | 4 ++-- vernac/record.ml | 2 +- 4 files changed, 6 insertions(+), 6 deletions(-) (limited to 'vernac') diff --git a/vernac/classes.ml b/vernac/classes.ml index 20cb43b24e..ed37bab6db 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -411,14 +411,14 @@ let context poly l = let decl = (Discharge, poly, Definitional) in let nstatus = match b with | None -> - pi3 (Command.declare_assumption false decl (t, !uctx) [] [] impl + pi3 (Command.declare_assumption false decl (t, !uctx) Universes.empty_binders [] impl Vernacexpr.NoInline (Loc.tag id)) | Some b -> let ctx = Univ.ContextSet.to_context !uctx in let decl = (Discharge, poly, Definition) in let entry = Declare.definition_entry ~poly ~univs:ctx ~types:t b in let hook = Lemmas.mk_hook (fun _ gr -> gr) in - let _ = DeclareDef.declare_definition id decl entry [] [] hook in + let _ = DeclareDef.declare_definition id decl entry Universes.empty_binders [] hook in Lib.sections_are_opened () || Lib.is_modtype_strict () in status && nstatus diff --git a/vernac/command.ml b/vernac/command.ml index 257c003b5a..5d83de0708 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -258,7 +258,7 @@ let do_assumptions_unbound_univs (_, poly, _ as kind) nl l = let l = List.map (on_pi2 nf_evar) l in pi2 (List.fold_left (fun (subst,status,ctx) ((is_coe,idl),t,imps) -> let t = replace_vars subst t in - let (refs,status') = declare_assumptions idl is_coe kind (t,ctx) [] imps false nl in + let (refs,status') = declare_assumptions idl is_coe kind (t,ctx) Universes.empty_binders imps false nl in let subst' = List.map2 (fun (_,id) (c,u) -> (id,Universes.constr_of_global_univ (c,u))) idl refs diff --git a/vernac/obligations.ml b/vernac/obligations.ml index a44de66e96..590332d083 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -484,7 +484,7 @@ let declare_definition prg = let () = progmap_remove prg in let cst = DeclareDef.declare_definition prg.prg_name - prg.prg_kind ce [] prg.prg_implicits + prg.prg_kind ce Universes.empty_binders prg.prg_implicits (Lemmas.mk_hook (fun l r -> Lemmas.call_hook fix_exn prg.prg_hook l r prg.prg_ctx; r)) in Universes.register_universe_binders cst pl; @@ -554,7 +554,7 @@ let declare_mutual_definition l = (* Declare the recursive definitions *) let ctx = Evd.evar_context_universe_context first.prg_ctx in let fix_exn = Hook.get get_fix_exn () in - let kns = List.map4 (DeclareDef.declare_fix ~opaque (local, poly, kind) [] ctx) + let kns = List.map4 (DeclareDef.declare_fix ~opaque (local, poly, kind) Universes.empty_binders ctx) fixnames fixdecls fixtypes fiximps in (* Declare notations *) List.iter (Metasyntax.add_notation_interpretation (Global.env())) first.prg_notations; diff --git a/vernac/record.ml b/vernac/record.ml index f09b570489..6ffbd1584e 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -426,7 +426,7 @@ let declare_structure finite univs id idbuild paramimpls params arity template else mie in - let kn = Command.declare_mutual_inductive_with_eliminations mie [] [(paramimpls,[])] in + let kn = Command.declare_mutual_inductive_with_eliminations mie Universes.empty_binders [(paramimpls,[])] in let rsp = (kn,0) in (* This is ind path of idstruc *) let cstr = (rsp,1) in let fields = -- cgit v1.2.3 From a5feb9687819c5e7ef0db6e7b74d0e236a296674 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Fri, 15 Sep 2017 21:01:57 +0200 Subject: Separate checking univ_decls and obtaining universe binder names. --- vernac/class.ml | 2 +- vernac/classes.ml | 8 ++++---- vernac/command.ml | 48 +++++++++++++++++++++++++++--------------------- vernac/indschemes.ml | 2 +- vernac/lemmas.ml | 12 ++++++------ vernac/obligations.ml | 15 ++++++--------- vernac/record.ml | 5 +++-- vernac/vernacentries.ml | 6 +++--- 8 files changed, 51 insertions(+), 47 deletions(-) (limited to 'vernac') diff --git a/vernac/class.ml b/vernac/class.ml index 44f20a0887..e59482b712 100644 --- a/vernac/class.ml +++ b/vernac/class.ml @@ -212,7 +212,7 @@ let build_id_coercion idf_opt source poly = Id.of_string ("Id_"^(ident_key_of_class source)^"_"^ (ident_key_of_class cl)) in - let univs = (snd (Evd.universe_context ~names:[] ~extensible:true sigma)) in + let univs = Evd.universe_context ~names:[] ~extensible:true sigma in let constr_entry = (* Cast is necessary to express [val_f] is identity *) DefinitionEntry (definition_entry ~types:typ_f ~poly ~univs diff --git a/vernac/classes.ml b/vernac/classes.ml index ed37bab6db..6f5f96ee24 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -119,14 +119,14 @@ let declare_instance_constant k info global imps ?hook id decl poly evm term ter (Univops.universes_of_constr term) in Evd.restrict_universe_context evm levels in - let pl, uctx = Evd.check_univ_decl evm decl in + let uctx = Evd.check_univ_decl evm decl in let entry = Declare.definition_entry ~types:termtype ~poly ~univs:uctx term in let cdecl = (DefinitionEntry entry, kind) in let kn = Declare.declare_constant id cdecl in Declare.definition_message id; - Universes.register_universe_binders (ConstRef kn) pl; + Universes.register_universe_binders (ConstRef kn) (Evd.universe_binders evm); instance_hook k info global imps ?hook (ConstRef kn); id @@ -203,12 +203,12 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) nf t in Pretyping.check_evars env Evd.empty !evars (EConstr.of_constr termtype); - let pl, ctx = Evd.check_univ_decl !evars decl in + let ctx = Evd.check_univ_decl !evars decl in let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id (ParameterEntry (None,poly,(termtype,ctx),None), Decl_kinds.IsAssumption Decl_kinds.Logical) in - Universes.register_universe_binders (ConstRef cst) pl; + Universes.register_universe_binders (ConstRef cst) (Evd.universe_binders !evars); instance_hook k pri global imps ?hook (ConstRef cst); id end else ( diff --git a/vernac/command.ml b/vernac/command.ml index 5d83de0708..5a063f173c 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -107,8 +107,9 @@ let interp_definition pl bl p red_option c ctypopt = let body = nf (it_mkLambda_or_LetIn c ctx) in let vars = Univops.universes_of_constr body in let evd = Evd.restrict_universe_context !evdref vars in - let pl, uctx = Evd.check_univ_decl evd decl in - imps1@(Impargs.lift_implicits nb_args imps2), pl, + let uctx = Evd.check_univ_decl evd decl in + let binders = Evd.universe_binders evd in + imps1@(Impargs.lift_implicits nb_args imps2), binders, definition_entry ~univs:uctx ~poly:p body | Some ctyp -> let ty, impsty = interp_type_evars_impls ~impls env_bl evdref ctyp in @@ -133,8 +134,9 @@ let interp_definition pl bl p red_option c ctypopt = let vars = Univ.LSet.union (Univops.universes_of_constr body) (Univops.universes_of_constr typ) in let ctx = Evd.restrict_universe_context !evdref vars in - let pl, uctx = Evd.check_univ_decl ctx decl in - imps1@(Impargs.lift_implicits nb_args impsty), pl, + let uctx = Evd.check_univ_decl ctx decl in + let binders = Evd.universe_binders evd in + imps1@(Impargs.lift_implicits nb_args impsty), binders, definition_entry ~types:typ ~poly:p ~univs:uctx body in @@ -277,9 +279,10 @@ let do_assumptions_bound_univs coe kind nl id pl c = let ty = nf ty in let vars = Univops.universes_of_constr ty in let evd = Evd.restrict_universe_context !evdref vars in - let pl, uctx = Evd.check_univ_decl evd decl in + let uctx = Evd.check_univ_decl evd decl in + let binders = Evd.universe_binders evd in let uctx = Univ.ContextSet.of_context uctx in - let (_, _, st) = declare_assumption coe kind (ty, uctx) pl impls false nl id in + let (_, _, st) = declare_assumption coe kind (ty, uctx) binders impls false nl id in st let do_assumptions kind nl l = match l with @@ -576,7 +579,7 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite = let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf' cl,impsl)) constructors in let ctx_params = Context.Rel.map nf ctx_params in let evd = !evdref in - let pl, uctx = Evd.check_univ_decl evd decl in + let uctx = Evd.check_univ_decl evd decl in List.iter (fun c -> check_evars env_params Evd.empty evd (EConstr.of_constr c)) arities; Context.Rel.iter (fun c -> check_evars env0 Evd.empty evd (EConstr.of_constr c)) ctx_params; List.iter (fun (_,ctyps,_) -> @@ -617,7 +620,7 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite = in (if poly && cum then Inductiveops.infer_inductive_subtyping env_ar evd mind_ent - else mind_ent), pl, impls + else mind_ent), Evd.universe_binders evd, impls (* Very syntactical equality *) let eq_local_binders bl1 bl2 = @@ -1025,17 +1028,18 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = if List.length binders_rel > 1 then let name = add_suffix recname "_func" in let hook l gr _ = - let body = it_mkLambda_or_LetIn (mkApp (Evarutil.e_new_global evdref gr, [|make|])) binders_rel in - let ty = it_mkProd_or_LetIn top_arity binders_rel in - let ty = EConstr.Unsafe.to_constr ty in - let pl, univs = Evd.universe_context ~names:pl ~extensible:plext !evdref in - (*FIXME poly? *) - let ce = definition_entry ~poly ~types:ty ~univs (EConstr.to_constr !evdref body) in - (** FIXME: include locality *) - let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in - let gr = ConstRef c in - if Impargs.is_implicit_args () || not (List.is_empty impls) then - Impargs.declare_manual_implicits false gr [impls] + let body = it_mkLambda_or_LetIn (mkApp (Evarutil.e_new_global evdref gr, [|make|])) binders_rel in + let ty = it_mkProd_or_LetIn top_arity binders_rel in + let ty = EConstr.Unsafe.to_constr ty in + let univs = Evd.universe_context ~names:pl ~extensible:plext !evdref in + (*FIXME poly? *) + let ce = definition_entry ~poly ~types:ty ~univs (EConstr.to_constr !evdref body) in + (** FIXME: include locality *) + let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in + let gr = ConstRef c in + let () = Universes.register_universe_binders gr (Evd.universe_binders !evdref) in + if Impargs.is_implicit_args () || not (List.is_empty impls) then + Impargs.declare_manual_implicits false gr [impls] in let typ = it_mkProd_or_LetIn top_arity binders in hook, name, typ @@ -1168,7 +1172,8 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind List.map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in let evd = Evd.from_ctx ctx in let evd = Evd.restrict_universe_context evd vars in - let pl, ctx = Evd.check_univ_decl evd pl in + let ctx = Evd.check_univ_decl evd pl in + let pl = Evd.universe_binders evd in let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in ignore (List.map4 (DeclareDef.declare_fix (local, poly, Fixpoint) pl ctx) fixnames fixdecls fixtypes fiximps); @@ -1200,7 +1205,8 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n let fiximps = List.map (fun (len,imps,idx) -> imps) fiximps in let evd = Evd.from_ctx ctx in let evd = Evd.restrict_universe_context evd vars in - let pl, ctx = Evd.check_univ_decl evd pl in + let ctx = Evd.check_univ_decl evd pl in + let pl = Evd.universe_binders evd in ignore (List.map4 (DeclareDef.declare_fix (local, poly, CoFixpoint) pl ctx) fixnames fixdecls fixtypes fiximps); (* Declare the recursive definitions *) diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index c0ddc7e2ce..58f39e3036 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -109,7 +109,7 @@ let _ = let define id internal ctx c t = let f = declare_constant ~internal in - let _, univs = Evd.universe_context ~names:[] ~extensible:true ctx in + let univs = Evd.universe_context ~names:[] ~extensible:true ctx in let univs = if Flags.is_universe_polymorphism () then Polymorphic_const_entry univs else Monomorphic_const_entry univs diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index a025bfff83..cd30c7a68d 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -49,7 +49,7 @@ let retrieve_first_recthm uctx = function (NamedDecl.get_value (Global.lookup_named id),variable_opacity id) | ConstRef cst -> let cb = Global.lookup_constant cst in - let (_, uctx) = UState.universe_context ~names:[] ~extensible:true uctx in + let uctx = UState.universe_context ~names:[] ~extensible:true uctx in let inst = Univ.UContext.instance uctx in let map (c, ctx) = Vars.subst_instance_constr inst c in (Option.map map (Global.body_of_constant_body cb), is_opaque cb) @@ -223,7 +223,7 @@ let compute_proof_name locality = function let avoid = Id.Set.of_list (Proof_global.get_all_proof_names ()) in next_global_ident_away default_thm_id avoid -let save_remaining_recthms (locality,p,kind) norm ctx binders body opaq i (id,(t_i,(_,imps))) = +let save_remaining_recthms (locality,p,kind) norm ctx body opaq i (id,(t_i,(_,imps))) = let t_i = norm t_i in match body with | None -> @@ -420,9 +420,9 @@ let start_proof_with_initialization kind ctx decl recguard thms snl hook = let body,opaq = retrieve_first_recthm ctx ref in let subst = Evd.evar_universe_context_subst ctx in let norm c = Universes.subst_opt_univs_constr subst c in - let binders, ctx = Evd.check_univ_decl (Evd.from_ctx ctx) decl in + let ctx = Evd.check_univ_decl (Evd.from_ctx ctx) decl in let body = Option.map norm body in - List.map_i (save_remaining_recthms kind norm ctx binders body opaq) 1 other_thms in + List.map_i (save_remaining_recthms kind norm ctx body opaq) 1 other_thms in let thms_data = (strength,ref,imps)::other_thms_data in List.iter (fun (strength,ref,imps) -> maybe_declare_manual_implicits false ref imps; @@ -513,9 +513,9 @@ let save_proof ?proof = function | _ -> None in let decl = Proof_global.get_universe_decl () in let evd = Evd.from_ctx universes in - let binders, ctx = Evd.check_univ_decl evd decl in + let ctx = Evd.check_univ_decl evd decl in let poly = pi2 k in - let binders = if poly then Some binders else None in + let binders = if poly then Some (UState.universe_binders universes) else None in Admitted(id,k,(sec_vars, poly, (typ, ctx), None), (universes, binders)) in diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 590332d083..2168018112 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -475,20 +475,17 @@ let declare_definition prg = (Evd.evar_universe_context_subst prg.prg_ctx) in let opaque = prg.prg_opaque in let fix_exn = Hook.get get_fix_exn () in - let pl, ctx = Evd.check_univ_decl (Evd.from_ctx prg.prg_ctx) prg.prg_univdecl in + let () = ignore(UState.check_univ_decl prg.prg_ctx prg.prg_univdecl) in let ce = definition_entry ~fix_exn ~opaque ~types:(nf typ) ~poly:(pi2 prg.prg_kind) ~univs:(Evd.evar_context_universe_context prg.prg_ctx) (nf body) in let () = progmap_remove prg in - let cst = - DeclareDef.declare_definition prg.prg_name - prg.prg_kind ce Universes.empty_binders prg.prg_implicits - (Lemmas.mk_hook (fun l r -> Lemmas.call_hook fix_exn prg.prg_hook l r prg.prg_ctx; r)) - in - Universes.register_universe_binders cst pl; - cst + let ubinders = UState.universe_binders prg.prg_ctx in + DeclareDef.declare_definition prg.prg_name + prg.prg_kind ce ubinders prg.prg_implicits + (Lemmas.mk_hook (fun l r -> Lemmas.call_hook fix_exn prg.prg_hook l r prg.prg_ctx; r)) let rec lam_index n t acc = match Constr.kind t with @@ -893,7 +890,7 @@ in let ctx' = Evd.merge_universe_subst evd (Evd.universe_subst (Evd.from_ctx ctx')) in Univ.Instance.empty, Evd.evar_universe_context ctx' else - let (_, uctx) = UState.universe_context ~names:[] ~extensible:true ctx' in + let uctx = UState.universe_context ~names:[] ~extensible:true ctx' in Univ.UContext.instance uctx, ctx' in let obl = { obl with obl_body = Some (DefinedObl (cst, inst)) } in diff --git a/vernac/record.ml b/vernac/record.ml index 6ffbd1584e..9fef8f682a 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -168,9 +168,10 @@ let typecheck_params_and_fields finite def id pl t ps nots fs = let typ = EConstr.to_constr evars typ in let ce t = Pretyping.check_evars env0 Evd.empty evars (EConstr.of_constr t) in let univs = Evd.check_univ_decl evars decl in + let ubinders = Evd.universe_binders evars in List.iter (iter_constr ce) (List.rev newps); List.iter (iter_constr ce) (List.rev newfs); - univs, typ, template, imps, newps, impls, newfs + ubinders, univs, typ, template, imps, newps, impls, newfs let degenerate_decl decl = let id = match RelDecl.get_name decl with @@ -605,7 +606,7 @@ let definition_structure (kind,cum,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cf if isnot_class && List.exists (fun opt -> not (Option.is_empty opt)) priorities then user_err Pp.(str "Priorities only allowed for type class substructures"); (* Now, younger decl in params and fields is on top *) - let (pl, ctx), arity, template, implpars, params, implfs, fields = + let pl, ctx, arity, template, implpars, params, implfs, fields = States.with_state_protection (fun () -> typecheck_params_and_fields finite (kind = Class true) idstruc pl s ps notations fs) () in let sign = structure_signature (fields@params) in diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 62c7edb19d..e2f28a371a 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1555,8 +1555,8 @@ let vernac_check_may_eval ?loc redexp glopt rc = let sigma' = Evarconv.solve_unif_constraints_with_heuristics env sigma' in Evarconv.check_problems_are_solved env sigma'; let sigma',nf = Evarutil.nf_evars_and_universes sigma' in - let pl, uctx = Evd.universe_context ~names:[] ~extensible:true sigma' in - let env = Environ.push_context uctx (Evarutil.nf_env_evar sigma' env) in + let uctx = Evd.universe_context_set sigma' in + let env = Environ.push_context_set uctx (Evarutil.nf_env_evar sigma' env) in let c = nf c in let j = if Evarutil.has_undefined_evars sigma' (EConstr.of_constr c) then @@ -1572,7 +1572,7 @@ let vernac_check_may_eval ?loc redexp glopt rc = let j = { j with Environ.uj_type = Reductionops.nf_betaiota sigma' j.Environ.uj_type } in Feedback.msg_notice (print_judgment env sigma' j ++ pr_ne_evar_set (fnl () ++ str "where" ++ fnl ()) (mt ()) sigma' l ++ - Printer.pr_universe_ctx sigma uctx) + Printer.pr_universe_ctx_set sigma uctx) | Some r -> let (sigma',r_interp) = Hook.get f_interp_redexp env sigma' r in let redfun env evm c = -- cgit v1.2.3 From 60770e86f4ec925fce52ad3565a92beb98d253c1 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Fri, 15 Sep 2017 22:21:46 +0200 Subject: Stop exposing UState.universe_context and its Evd wrapper. We can enforce properties through check_univ_decl, or get an arbitrary ordered context with UState.context / Evd.to_universe_context (the later being a new wrapper of the former). --- vernac/class.ml | 2 +- vernac/command.ml | 4 +--- vernac/indschemes.ml | 2 +- vernac/lemmas.ml | 15 ++++++++------- vernac/obligations.ml | 13 +++++++------ 5 files changed, 18 insertions(+), 18 deletions(-) (limited to 'vernac') diff --git a/vernac/class.ml b/vernac/class.ml index e59482b712..68fd22cb62 100644 --- a/vernac/class.ml +++ b/vernac/class.ml @@ -212,7 +212,7 @@ let build_id_coercion idf_opt source poly = Id.of_string ("Id_"^(ident_key_of_class source)^"_"^ (ident_key_of_class cl)) in - let univs = Evd.universe_context ~names:[] ~extensible:true sigma in + let univs = Evd.to_universe_context sigma in let constr_entry = (* Cast is necessary to express [val_f] is identity *) DefinitionEntry (definition_entry ~types:typ_f ~poly ~univs diff --git a/vernac/command.ml b/vernac/command.ml index 5a063f173c..80599c5345 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -1022,8 +1022,6 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = let binders_rel = nf_evar_context !evdref binders_rel in let binders = nf_evar_context !evdref binders in let top_arity = Evarutil.nf_evar !evdref top_arity in - let pl, plext = Option.cata - (fun d -> d.univdecl_instance, d.univdecl_extensible_instance) ([],true) pl in let hook, recname, typ = if List.length binders_rel > 1 then let name = add_suffix recname "_func" in @@ -1031,7 +1029,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = let body = it_mkLambda_or_LetIn (mkApp (Evarutil.e_new_global evdref gr, [|make|])) binders_rel in let ty = it_mkProd_or_LetIn top_arity binders_rel in let ty = EConstr.Unsafe.to_constr ty in - let univs = Evd.universe_context ~names:pl ~extensible:plext !evdref in + let univs = Evd.check_univ_decl !evdref decl in (*FIXME poly? *) let ce = definition_entry ~poly ~types:ty ~univs (EConstr.to_constr !evdref body) in (** FIXME: include locality *) diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index 58f39e3036..c728c26712 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -109,7 +109,7 @@ let _ = let define id internal ctx c t = let f = declare_constant ~internal in - let univs = Evd.universe_context ~names:[] ~extensible:true ctx in + let univs = Evd.to_universe_context ctx in let univs = if Flags.is_universe_polymorphism () then Polymorphic_const_entry univs else Monomorphic_const_entry univs diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index cd30c7a68d..71d80c4db0 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -49,7 +49,8 @@ let retrieve_first_recthm uctx = function (NamedDecl.get_value (Global.lookup_named id),variable_opacity id) | ConstRef cst -> let cb = Global.lookup_constant cst in - let uctx = UState.universe_context ~names:[] ~extensible:true uctx in + (* we get the right order somehow but surely it could be enforced in a better way *) + let uctx = UState.context uctx in let inst = Univ.UContext.instance uctx in let map (c, ctx) = Vars.subst_instance_constr inst c in (Option.map map (Global.body_of_constant_body cb), is_opaque cb) @@ -420,8 +421,8 @@ let start_proof_with_initialization kind ctx decl recguard thms snl hook = let body,opaq = retrieve_first_recthm ctx ref in let subst = Evd.evar_universe_context_subst ctx in let norm c = Universes.subst_opt_univs_constr subst c in - let ctx = Evd.check_univ_decl (Evd.from_ctx ctx) decl in - let body = Option.map norm body in + let ctx = UState.check_univ_decl ctx decl in + let body = Option.map norm body in List.map_i (save_remaining_recthms kind norm ctx body opaq) 1 other_thms in let thms_data = (strength,ref,imps)::other_thms_data in List.iter (fun (strength,ref,imps) -> @@ -453,9 +454,9 @@ let start_proof_com ?inference_hook kind thms hook = let evd, nf = Evarutil.nf_evars_and_universes !evdref in let thms = List.map (fun (n, (t, info)) -> (n, (nf t, info))) thms in let () = - if not decl.Misctypes.univdecl_extensible_instance then - ignore (Evd.universe_context evd ~names:decl.Misctypes.univdecl_instance ~extensible:false) - else () + let open Misctypes in + if not (decl.univdecl_extensible_instance && decl.univdecl_extensible_constraints) then + ignore (Evd.check_univ_decl evd decl) in let evd = if pi2 kind then evd @@ -490,7 +491,7 @@ let save_proof ?proof = function if const_entry_type = None then user_err Pp.(str "Admitted requires an explicit statement"); let typ = Option.get const_entry_type in - let ctx = Evd.evar_context_universe_context (fst universes) in + let ctx = UState.context (fst universes) in let sec_vars = if !keep_admitted_vars then const_entry_secctx else None in Admitted(id, k, (sec_vars, pi2 k, (typ, ctx), None), universes) | None -> diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 2168018112..43af8968fe 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -479,7 +479,7 @@ let declare_definition prg = let ce = definition_entry ~fix_exn ~opaque ~types:(nf typ) ~poly:(pi2 prg.prg_kind) - ~univs:(Evd.evar_context_universe_context prg.prg_ctx) (nf body) + ~univs:(UState.context prg.prg_ctx) (nf body) in let () = progmap_remove prg in let ubinders = UState.universe_binders prg.prg_ctx in @@ -549,7 +549,7 @@ let declare_mutual_definition l = mk_proof (mkCoFix (i,fixdecls))) 0 l in (* Declare the recursive definitions *) - let ctx = Evd.evar_context_universe_context first.prg_ctx in + let ctx = UState.context first.prg_ctx in let fix_exn = Hook.get get_fix_exn () in let kns = List.map4 (DeclareDef.declare_fix ~opaque (local, poly, kind) Universes.empty_binders ctx) fixnames fixdecls fixtypes fiximps in @@ -855,7 +855,7 @@ let obligation_terminator name num guard hook auto pf = | (_, status), Vernacexpr.Transparent -> status in let obl = { obl with obl_status = false, status } in - let uctx = Evd.evar_context_universe_context ctx in + let uctx = UState.context ctx in let (_, obl) = declare_obligation prg obl body ty uctx in let obls = Array.copy obls in let _ = obls.(num) <- obl in @@ -890,7 +890,8 @@ in let ctx' = Evd.merge_universe_subst evd (Evd.universe_subst (Evd.from_ctx ctx')) in Univ.Instance.empty, Evd.evar_universe_context ctx' else - let uctx = UState.universe_context ~names:[] ~extensible:true ctx' in + (* We get the right order somehow, but surely it could be enforced in a clearer way. *) + let uctx = UState.context ctx' in Univ.UContext.instance uctx, ctx' in let obl = { obl with obl_body = Some (DefinedObl (cst, inst)) } in @@ -969,7 +970,7 @@ and solve_obligation_by_tac prg obls i tac = solve_by_tac obl.obl_name (evar_of_obligation obl) tac (pi2 prg.prg_kind) (Evd.evar_universe_context evd) in - let uctx = Evd.evar_context_universe_context ctx in + let uctx = UState.context ctx in let prg = {prg with prg_ctx = ctx} in let def, obl' = declare_obligation prg obl t ty uctx in obls.(i) <- obl'; @@ -1120,7 +1121,7 @@ let admit_prog prg = match x.obl_body with | None -> let x = subst_deps_obl obls x in - let ctx = Evd.evar_context_universe_context prg.prg_ctx in + let ctx = UState.context prg.prg_ctx in let kn = Declare.declare_constant x.obl_name ~local:true (ParameterEntry (None,false,(x.obl_type,ctx),None), IsAssumption Conjectural) in -- cgit v1.2.3 From e414c07e193db7d4256c09167f6efd545831fa2b Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Fri, 15 Sep 2017 22:33:23 +0200 Subject: Register universe binders for record projections. --- vernac/record.ml | 35 +++++++++++++++++++---------------- vernac/record.mli | 24 ------------------------ 2 files changed, 19 insertions(+), 40 deletions(-) (limited to 'vernac') diff --git a/vernac/record.ml b/vernac/record.ml index 9fef8f682a..e465e06162 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -266,7 +266,7 @@ let warn_non_primitive_record = strbrk" could not be defined as a primitive record"))) (* We build projections *) -let declare_projections indsp ?(kind=StructureComponent) binder_name coers fieldimpls fields = +let declare_projections indsp ?(kind=StructureComponent) binder_name coers ubinders fieldimpls fields = let env = Global.env() in let (mib,mip) = Global.lookup_inductive indsp in let poly = Declareops.inductive_is_polymorphic mib in @@ -305,9 +305,11 @@ let declare_projections indsp ?(kind=StructureComponent) binder_name coers field let kn, term = if is_local_assum decl && primitive then (** Already defined in the kernel silently *) - let kn = destConstRef (Nametab.locate (Libnames.qualid_of_ident fid)) in - Declare.definition_message fid; - kn, mkProj (Projection.make kn false,mkRel 1) + let gr = Nametab.locate (Libnames.qualid_of_ident fid) in + let kn = destConstRef gr in + Declare.definition_message fid; + Universes.register_universe_binders gr ubinders; + kn, mkProj (Projection.make kn false,mkRel 1) else let ccl = subst_projection fid subst ti in let body = match decl with @@ -344,8 +346,9 @@ let declare_projections indsp ?(kind=StructureComponent) binder_name coers field let constr_fip = let proj_args = (*Rel 1 refers to "x"*) paramargs@[mkRel 1] in applist (mkConstU (kn,u),proj_args) - in - Declare.definition_message fid; + in + Declare.definition_message fid; + Universes.register_universe_binders (ConstRef kn) ubinders; kn, constr_fip with Type_errors.TypeError (ctx,te) -> raise (NotDefinable (BadTypedProj (fid,ctx,te))) @@ -383,7 +386,7 @@ let structure_signature ctx = open Typeclasses -let declare_structure finite univs id idbuild paramimpls params arity template +let declare_structure finite ubinders univs id idbuild paramimpls params arity template fieldimpls fields ?(kind=StructureComponent) ?name is_coe coers sign = let nparams = List.length params and nfields = List.length fields in let args = Context.Rel.to_extended_list mkRel nfields params in @@ -436,10 +439,11 @@ let declare_structure finite univs id idbuild paramimpls params arity template Context.Rel.map (fun c -> Vars.subst_univs_level_constr subst c) fields else fields in - let kinds,sp_projs = declare_projections rsp ~kind binder_name coers fieldimpls fields in + let kinds,sp_projs = declare_projections rsp ~kind binder_name coers ubinders fieldimpls fields in let build = ConstructRef cstr in let () = if is_coe then Class.try_add_new_coercion build ~local:false poly in Recordops.declare_structure(rsp,cstr,List.rev kinds,List.rev sp_projs); + Universes.register_universe_binders (IndRef rsp) ubinders; rsp let implicits_of_context ctx = @@ -451,7 +455,7 @@ let implicits_of_context ctx = in ExplByPos (i, explname), (true, true, true)) 1 (List.rev (Anonymous :: (List.map RelDecl.get_name ctx))) -let declare_class finite def cum poly ctx id idbuild paramimpls params arity +let declare_class finite def cum poly ubinders ctx id idbuild paramimpls params arity template fieldimpls fields ?(kind=StructureComponent) is_coe coers priorities sign = let fieldimpls = (* Make the class implicit in the projections, and the params if applicable. *) @@ -486,7 +490,9 @@ let declare_class finite def cum poly ctx id idbuild paramimpls params arity in let cref = ConstRef cst in Impargs.declare_manual_implicits false cref [paramimpls]; + Universes.register_universe_binders cref ubinders; Impargs.declare_manual_implicits false (ConstRef proj_cst) [List.hd fieldimpls]; + Universes.register_universe_binders (ConstRef proj_cst) ubinders; 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) @@ -503,7 +509,7 @@ let declare_class finite def cum poly ctx id idbuild paramimpls params arity else Monomorphic_ind_entry ctx in - let ind = declare_structure BiFinite univs (snd id) idbuild paramimpls + let ind = declare_structure BiFinite ubinders univs (snd id) idbuild paramimpls params arity template fieldimpls fields ~kind:Method ~name:binder_name false (List.map (fun _ -> false) fields) sign in @@ -610,10 +616,10 @@ let definition_structure (kind,cum,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cf States.with_state_protection (fun () -> typecheck_params_and_fields finite (kind = Class true) idstruc pl s ps notations fs) () in let sign = structure_signature (fields@params) in - let gr = match kind with + match kind with | Class def -> let priorities = List.map (fun id -> {hint_priority = id; hint_pattern = None}) priorities in - let gr = declare_class finite def cum poly ctx (loc,idstruc) idbuild + let gr = declare_class finite def cum poly pl ctx (loc,idstruc) idbuild implpars params arity template implfs fields is_coe coers priorities sign in gr | _ -> @@ -630,10 +636,7 @@ let definition_structure (kind,cum,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cf else Monomorphic_ind_entry ctx in - let ind = declare_structure finite univs idstruc + let ind = declare_structure finite pl univs idstruc idbuild implpars params arity template implfs fields is_coe (List.map (fun coe -> not (Option.is_empty coe)) coers) sign in IndRef ind - in - Universes.register_universe_binders gr pl; - gr diff --git a/vernac/record.mli b/vernac/record.mli index 33c2fba89c..9fdd5e1c46 100644 --- a/vernac/record.mli +++ b/vernac/record.mli @@ -7,36 +7,12 @@ (************************************************************************) open Names -open Constr open Vernacexpr open Constrexpr -open Impargs open Globnames val primitive_flag : bool ref -(** [declare_projections ref name coers params fields] declare projections of - record [ref] (if allowed) using the given [name] as argument, and put them - as coercions accordingly to [coers]; it returns the absolute names of projections *) - -val declare_projections : - inductive -> ?kind:Decl_kinds.definition_object_kind -> Id.t -> - coercion_flag list -> manual_explicitation list list -> Context.Rel.t -> - (Name.t * bool) list * Constant.t option list - -val declare_structure : - Decl_kinds.recursivity_kind -> - Entries.inductive_universes -> - Id.t -> Id.t -> - manual_explicitation list -> Context.Rel.t -> (** params *) constr -> (** arity *) - bool (** template arity ? *) -> - Impargs.manual_explicitation list list -> Context.Rel.t -> (** fields *) - ?kind:Decl_kinds.definition_object_kind -> ?name:Id.t -> - bool -> (** coercion? *) - bool list -> (** field coercions *) - Evd.evar_map -> - inductive - val definition_structure : inductive_kind * Decl_kinds.cumulative_inductive_flag * Decl_kinds.polymorphic * Decl_kinds.recursivity_kind * ident_decl with_coercion * local_binder_expr list * -- cgit v1.2.3 From 4eb6d29d1ca7e0cc28d59d19a50adb83f7b30a2a Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Fri, 15 Sep 2017 23:39:11 +0200 Subject: Fix defining non primitive projections with abstracted universes. I think this only affects printing (in the new test you would get [Var (0)] when printing runwrap) but is still ugly. --- vernac/record.ml | 16 ++++------------ 1 file changed, 4 insertions(+), 12 deletions(-) (limited to 'vernac') diff --git a/vernac/record.ml b/vernac/record.ml index e465e06162..0819dadb4f 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -266,11 +266,10 @@ let warn_non_primitive_record = strbrk" could not be defined as a primitive record"))) (* We build projections *) -let declare_projections indsp ?(kind=StructureComponent) binder_name coers ubinders fieldimpls fields = +let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers ubinders fieldimpls fields = let env = Global.env() in let (mib,mip) = Global.lookup_inductive indsp in let poly = Declareops.inductive_is_polymorphic mib in - let ctx = Univ.AUContext.repr (Declareops.inductive_polymorphic_context mib) in let u = Univ.UContext.instance ctx in let paramdecls = Inductive.inductive_paramdecls (mib, u) in let indu = indsp, u in @@ -394,7 +393,7 @@ let declare_structure finite ubinders univs id idbuild paramimpls params arity t let type_constructor = it_mkProd_or_LetIn ind fields in let poly, ctx = match univs with - | Monomorphic_ind_entry ctx -> false, ctx + | Monomorphic_ind_entry ctx -> false, Univ.UContext.empty | Polymorphic_ind_entry ctx -> true, ctx | Cumulative_ind_entry cumi -> true, (Univ.CumulativityInfo.univ_context cumi) in @@ -430,20 +429,13 @@ let declare_structure finite ubinders univs id idbuild paramimpls params arity t else mie in - let kn = Command.declare_mutual_inductive_with_eliminations mie Universes.empty_binders [(paramimpls,[])] in + let kn = Command.declare_mutual_inductive_with_eliminations mie ubinders [(paramimpls,[])] in let rsp = (kn,0) in (* This is ind path of idstruc *) let cstr = (rsp,1) in - let fields = - if poly then - let subst, _ = Univ.abstract_universes ctx in - Context.Rel.map (fun c -> Vars.subst_univs_level_constr subst c) fields - else fields - in - let kinds,sp_projs = declare_projections rsp ~kind binder_name coers ubinders fieldimpls fields in + let kinds,sp_projs = declare_projections rsp ctx ~kind binder_name coers ubinders fieldimpls fields in let build = ConstructRef cstr in let () = if is_coe then Class.try_add_new_coercion build ~local:false poly in Recordops.declare_structure(rsp,cstr,List.rev kinds,List.rev sp_projs); - Universes.register_universe_binders (IndRef rsp) ubinders; rsp let implicits_of_context ctx = -- cgit v1.2.3 From 58c0784745f8b2ba7523f246c4611d780c9f3f70 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Mon, 18 Sep 2017 14:50:07 +0200 Subject: When declaring constants/inductives use ContextSet if monomorphic. Also use constant_universes_entry instead of a bool flag to indicate polymorphism in ParameterEntry. There are a few places where we convert back to ContextSet because check_univ_decl returns a UContext, this could be improved. --- vernac/classes.ml | 34 +++++++++++++++++++++++----------- vernac/command.ml | 15 +++++++++------ vernac/indschemes.ml | 6 +++--- vernac/lemmas.ml | 19 +++++++++++++++---- vernac/obligations.ml | 45 ++++++++++++++++++++++++++------------------- vernac/record.ml | 36 +++++++++++++++++++----------------- 6 files changed, 95 insertions(+), 60 deletions(-) (limited to 'vernac') diff --git a/vernac/classes.ml b/vernac/classes.ml index 6f5f96ee24..c99eba2cc9 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -200,16 +200,22 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) let nf, subst = Evarutil.e_nf_evars_and_universes evars in let termtype = let t = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in - nf t - in - Pretyping.check_evars env Evd.empty !evars (EConstr.of_constr termtype); + nf t + in + Pretyping.check_evars env Evd.empty !evars (EConstr.of_constr termtype); let ctx = Evd.check_univ_decl !evars decl in - let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id - (ParameterEntry - (None,poly,(termtype,ctx),None), Decl_kinds.IsAssumption Decl_kinds.Logical) - in + let ctx = if poly + then Polymorphic_const_entry ctx + else + (* FIXME be smarter about this *) + Monomorphic_const_entry (Univ.ContextSet.of_context ctx) + in + let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id + (ParameterEntry + (None,(termtype,ctx),None), Decl_kinds.IsAssumption Decl_kinds.Logical) + in Universes.register_universe_binders (ConstRef cst) (Evd.universe_binders !evars); - instance_hook k pri global imps ?hook (ConstRef cst); id + instance_hook k pri global imps ?hook (ConstRef cst); id end else ( let props = @@ -384,14 +390,20 @@ let context poly l = let uctx = ref (Evd.universe_context_set !evars) in let fn status (id, b, t) = if Lib.is_modtype () && not (Lib.sections_are_opened ()) then - let ctx = Univ.ContextSet.to_context !uctx in (* Declare the universe context once *) + let univs = !uctx in let () = uctx := Univ.ContextSet.empty in let decl = match b with | None -> - (ParameterEntry (None,poly,(t,ctx),None), IsAssumption Logical) + let univs = if poly + then Polymorphic_const_entry (Univ.ContextSet.to_context univs) + else Monomorphic_const_entry univs + in + (ParameterEntry (None,(t,univs),None), IsAssumption Logical) | Some b -> - let entry = Declare.definition_entry ~poly ~univs:ctx ~types:t b in + (* FIXME be smarter about this *) + let univs = Univ.ContextSet.to_context univs in + let entry = Declare.definition_entry ~poly ~univs ~types:t b in (DefinitionEntry entry, IsAssumption Logical) in let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id decl in diff --git a/vernac/command.ml b/vernac/command.ml index 80599c5345..06d0c8470e 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -197,8 +197,11 @@ match local with | DefaultInline -> Some (Flags.get_inline_level()) | InlineAt i -> Some i in - let ctx = Univ.ContextSet.to_context ctx in - let decl = (ParameterEntry (None,p,(c,ctx),inl), IsAssumption kind) in + let ctx = if p + then Polymorphic_const_entry (Univ.ContextSet.to_context ctx) + else Monomorphic_const_entry ctx + in + let decl = (ParameterEntry (None,(c,ctx),inl), IsAssumption kind) in let kn = declare_constant ident ~local decl in let gr = ConstRef kn in let () = maybe_declare_manual_implicits false gr imps in @@ -206,9 +209,9 @@ match local with let () = assumption_message ident in let () = Typeclasses.declare_instance None false gr in let () = if is_coe then Class.try_add_new_coercion gr ~local p in - let inst = - if p (* polymorphic *) then Univ.UContext.instance ctx - else Univ.Instance.empty + let inst = match ctx with + | Polymorphic_const_entry ctx -> Univ.UContext.instance ctx + | Monomorphic_const_entry _ -> Univ.Instance.empty in (gr,inst,Lib.is_modtype_strict ()) @@ -606,7 +609,7 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite = Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context uctx) else Polymorphic_ind_entry uctx else - Monomorphic_ind_entry uctx + Monomorphic_ind_entry (Univ.ContextSet.of_context uctx) in (* Build the mutual inductive entry *) let mind_ent = diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index c728c26712..e4ca98749c 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -109,10 +109,10 @@ let _ = let define id internal ctx c t = let f = declare_constant ~internal in - let univs = Evd.to_universe_context ctx in let univs = - if Flags.is_universe_polymorphism () then Polymorphic_const_entry univs - else Monomorphic_const_entry univs + if Flags.is_universe_polymorphism () + then Polymorphic_const_entry (Evd.to_universe_context ctx) + else Monomorphic_const_entry (Evd.universe_context_set ctx) in let kn = f id (DefinitionEntry diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 71d80c4db0..f59b5fcae9 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -242,7 +242,11 @@ let save_remaining_recthms (locality,p,kind) norm ctx body opaq i (id,(t_i,(_,im | Global -> false | Discharge -> assert false in - let decl = (ParameterEntry (None,p,(t_i,ctx),None), k) in + let ctx = if p + then Polymorphic_const_entry ctx + else Monomorphic_const_entry (Univ.ContextSet.of_context ctx) + in + let decl = (ParameterEntry (None,(t_i,ctx),None), k) in let kn = declare_constant id ~local decl in (locality,ConstRef kn,imps)) | Some body -> @@ -491,9 +495,12 @@ let save_proof ?proof = function if const_entry_type = None then user_err Pp.(str "Admitted requires an explicit statement"); let typ = Option.get const_entry_type in - let ctx = UState.context (fst universes) in + let ctx = if pi2 k (* polymorphic *) + then Polymorphic_const_entry (UState.context (fst universes)) + else Monomorphic_const_entry (UState.context_set (fst universes)) + in let sec_vars = if !keep_admitted_vars then const_entry_secctx else None in - Admitted(id, k, (sec_vars, pi2 k, (typ, ctx), None), universes) + Admitted(id, k, (sec_vars, (typ, ctx), None), universes) | None -> let pftree = Proof_global.give_me_the_proof () in let id, k, typ = Pfedit.current_proof_statement () in @@ -516,8 +523,12 @@ let save_proof ?proof = function let evd = Evd.from_ctx universes in let ctx = Evd.check_univ_decl evd decl in let poly = pi2 k in + let ctx = if poly + then Polymorphic_const_entry ctx + else Monomorphic_const_entry (Univ.ContextSet.of_context ctx) + in let binders = if poly then Some (UState.universe_binders universes) else None in - Admitted(id,k,(sec_vars, poly, (typ, ctx), None), + Admitted(id,k,(sec_vars, (typ, ctx), None), (universes, binders)) in Proof_global.apply_terminator (Proof_global.get_terminator ()) pe diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 43af8968fe..a9110c76cb 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -633,12 +633,11 @@ let declare_obligation prg obl body ty uctx = shrink_body body ty else [], body, ty, [||] in let body = ((body,Univ.ContextSet.empty),Safe_typing.empty_private_constants) in - let univs = if poly then Polymorphic_const_entry uctx else Monomorphic_const_entry uctx in let ce = { const_entry_body = Future.from_val ~fix_exn:(fun x -> x) body; const_entry_secctx = None; const_entry_type = ty; - const_entry_universes = univs; + const_entry_universes = uctx; const_entry_opaque = opaque; const_entry_inline_code = false; const_entry_feedback = None; @@ -647,13 +646,15 @@ let declare_obligation prg obl body ty uctx = let constant = Declare.declare_constant obl.obl_name ~local:true (DefinitionEntry ce,IsProof Property) in - if not opaque then add_hint (Locality.make_section_locality None) prg constant; - definition_message obl.obl_name; - true, { obl with obl_body = - if poly then - Some (DefinedObl (constant, Univ.UContext.instance uctx)) - else - Some (TermObl (it_mkLambda_or_LetIn_or_clean (mkApp (mkConst constant, args)) ctx)) } + if not opaque then add_hint (Locality.make_section_locality None) prg constant; + definition_message obl.obl_name; + let body = match uctx with + | Polymorphic_const_entry uctx -> + Some (DefinedObl (constant, Univ.UContext.instance uctx)) + | Monomorphic_const_entry _ -> + Some (TermObl (it_mkLambda_or_LetIn_or_clean (mkApp (mkConst constant, args)) ctx)) + in + true, { obl with obl_body = body } let init_prog_info ?(opaque = false) sign n udecl b t ctx deps fixkind notations obls impls kind reduce hook = @@ -855,7 +856,10 @@ let obligation_terminator name num guard hook auto pf = | (_, status), Vernacexpr.Transparent -> status in let obl = { obl with obl_status = false, status } in - let uctx = UState.context ctx in + let uctx = if pi2 prg.prg_kind + then Polymorphic_const_entry (UState.context ctx) + else Monomorphic_const_entry (UState.context_set ctx) + in let (_, obl) = declare_obligation prg obl body ty uctx in let obls = Array.copy obls in let _ = obls.(num) <- obl in @@ -967,13 +971,16 @@ and solve_obligation_by_tac prg obls i tac = let evd = Evd.from_ctx prg.prg_ctx in let evd = Evd.update_sigma_env evd (Global.env ()) in let t, ty, ctx = - solve_by_tac obl.obl_name (evar_of_obligation obl) tac - (pi2 prg.prg_kind) (Evd.evar_universe_context evd) - in - let uctx = UState.context ctx in - let prg = {prg with prg_ctx = ctx} in - let def, obl' = declare_obligation prg obl t ty uctx in - obls.(i) <- obl'; + solve_by_tac obl.obl_name (evar_of_obligation obl) tac + (pi2 prg.prg_kind) (Evd.evar_universe_context evd) + in + let uctx = if pi2 prg.prg_kind + then Polymorphic_const_entry (UState.context ctx) + else Monomorphic_const_entry (UState.context_set ctx) + in + let prg = {prg with prg_ctx = ctx} in + let def, obl' = declare_obligation prg obl t ty uctx in + obls.(i) <- obl'; if def && not (pi2 prg.prg_kind) then ( (* Declare the term constraints with the first obligation only *) let evd = Evd.from_env (Global.env ()) in @@ -1121,9 +1128,9 @@ let admit_prog prg = match x.obl_body with | None -> let x = subst_deps_obl obls x in - let ctx = UState.context prg.prg_ctx in + let ctx = Monomorphic_const_entry (UState.context_set prg.prg_ctx) in let kn = Declare.declare_constant x.obl_name ~local:true - (ParameterEntry (None,false,(x.obl_type,ctx),None), IsAssumption Conjectural) + (ParameterEntry (None,(x.obl_type,ctx),None), IsAssumption Conjectural) in assumption_message x.obl_name; obls.(i) <- { x with obl_body = Some (DefinedObl (kn, Univ.Instance.empty)) } diff --git a/vernac/record.ml b/vernac/record.ml index 0819dadb4f..faf277d86d 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -270,7 +270,10 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers u let env = Global.env() in let (mib,mip) = Global.lookup_inductive indsp in let poly = Declareops.inductive_is_polymorphic mib in - let u = Univ.UContext.instance ctx in + let u = match ctx with + | Polymorphic_const_entry ctx -> Univ.UContext.instance ctx + | Monomorphic_const_entry ctx -> Univ.Instance.empty + in let paramdecls = Inductive.inductive_paramdecls (mib, u) in let indu = indsp, u in let r = mkIndU (indsp,u) in @@ -327,16 +330,12 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers u let projtyp = it_mkProd_or_LetIn (mkProd (x,rp,ccl)) paramdecls in try - let univs = - if poly then Polymorphic_const_entry ctx - else Monomorphic_const_entry ctx - in let entry = { const_entry_body = Future.from_val (Safe_typing.mk_pure_proof proj); const_entry_secctx = None; const_entry_type = Some projtyp; - const_entry_universes = univs; + const_entry_universes = ctx; const_entry_opaque = false; const_entry_inline_code = false; const_entry_feedback = None } in @@ -391,11 +390,14 @@ let declare_structure finite ubinders univs id idbuild paramimpls params arity t let args = Context.Rel.to_extended_list mkRel nfields params in let ind = applist (mkRel (1+nparams+nfields), args) in let type_constructor = it_mkProd_or_LetIn ind fields in - let poly, ctx = + let template, ctx = match univs with - | Monomorphic_ind_entry ctx -> false, Univ.UContext.empty - | Polymorphic_ind_entry ctx -> true, ctx - | Cumulative_ind_entry cumi -> true, (Univ.CumulativityInfo.univ_context cumi) + | Monomorphic_ind_entry ctx -> + template, Monomorphic_const_entry Univ.ContextSet.empty + | Polymorphic_ind_entry ctx -> + false, Polymorphic_const_entry ctx + | Cumulative_ind_entry cumi -> + false, Polymorphic_const_entry (Univ.CumulativityInfo.univ_context cumi) in let binder_name = match name with @@ -405,7 +407,7 @@ let declare_structure finite ubinders univs id idbuild paramimpls params arity t let mie_ind = { mind_entry_typename = id; mind_entry_arity = arity; - mind_entry_template = not poly && template; + mind_entry_template = template; mind_entry_consnames = [idbuild]; mind_entry_lc = [type_constructor] } in @@ -419,14 +421,13 @@ let declare_structure finite ubinders univs id idbuild paramimpls params arity t } in let mie = - if poly then - begin + match ctx with + | Polymorphic_const_entry ctx -> let env = Global.env () in let env' = Environ.push_context ctx env in let evd = Evd.from_env env' in Inductiveops.infer_inductive_subtyping env' evd mie - end - else + | Monomorphic_const_entry _ -> mie in let kn = Command.declare_mutual_inductive_with_eliminations mie ubinders [(paramimpls,[])] in @@ -434,6 +435,7 @@ let declare_structure finite ubinders univs id idbuild paramimpls params arity t let cstr = (rsp,1) in let kinds,sp_projs = declare_projections rsp ctx ~kind binder_name coers ubinders fieldimpls fields in let build = ConstructRef cstr in + let poly = match ctx with | Polymorphic_const_entry _ -> true | Monomorphic_const_entry _ -> false in let () = if is_coe then Class.try_add_new_coercion build ~local:false poly in Recordops.declare_structure(rsp,cstr,List.rev kinds,List.rev sp_projs); rsp @@ -499,7 +501,7 @@ let declare_class finite def cum poly ubinders ctx id idbuild paramimpls params else Polymorphic_ind_entry ctx else - Monomorphic_ind_entry ctx + Monomorphic_ind_entry (Univ.ContextSet.of_context ctx) in let ind = declare_structure BiFinite ubinders univs (snd id) idbuild paramimpls params arity template fieldimpls fields @@ -626,7 +628,7 @@ let definition_structure (kind,cum,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cf else Polymorphic_ind_entry ctx else - Monomorphic_ind_entry ctx + Monomorphic_ind_entry (Univ.ContextSet.of_context ctx) in let ind = declare_structure finite pl univs idstruc idbuild implpars params arity template implfs -- cgit v1.2.3 From 34d85e1e899f8a045659ccc53bfd6a1f5104130b Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Mon, 18 Sep 2017 17:22:24 +0200 Subject: Use Entries.constant_universes_entry more. This reduces conversions between ContextSet/UContext and encodes whether we are polymorphic by which constructor we use rather than using some boolean. --- vernac/class.ml | 4 ++-- vernac/classes.ml | 34 +++++++++++++------------------- vernac/command.ml | 44 +++++++++++++++++++++++------------------ vernac/declareDef.ml | 4 ++-- vernac/declareDef.mli | 7 +++++-- vernac/lemmas.ml | 36 ++++++++++++++-------------------- vernac/obligations.ml | 17 +++++----------- vernac/record.ml | 54 +++++++++++++++++++++++++++------------------------ 8 files changed, 97 insertions(+), 103 deletions(-) (limited to 'vernac') diff --git a/vernac/class.ml b/vernac/class.ml index 68fd22cb62..943da8fa8a 100644 --- a/vernac/class.ml +++ b/vernac/class.ml @@ -212,10 +212,10 @@ let build_id_coercion idf_opt source poly = Id.of_string ("Id_"^(ident_key_of_class source)^"_"^ (ident_key_of_class cl)) in - let univs = Evd.to_universe_context sigma in + let univs = Evd.const_univ_entry ~poly sigma in let constr_entry = (* Cast is necessary to express [val_f] is identity *) DefinitionEntry - (definition_entry ~types:typ_f ~poly ~univs + (definition_entry ~types:typ_f ~univs ~inline:true (mkCast (val_f, DEFAULTcast, typ_f))) in let decl = (constr_entry, IsDefinition IdentityCoercion) in diff --git a/vernac/classes.ml b/vernac/classes.ml index c99eba2cc9..1833b7a1dd 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -119,9 +119,9 @@ let declare_instance_constant k info global imps ?hook id decl poly evm term ter (Univops.universes_of_constr term) in Evd.restrict_universe_context evm levels in - let uctx = Evd.check_univ_decl evm decl in + let uctx = Evd.check_univ_decl ~poly evm decl in let entry = - Declare.definition_entry ~types:termtype ~poly ~univs:uctx term + Declare.definition_entry ~types:termtype ~univs:uctx term in let cdecl = (DefinitionEntry entry, kind) in let kn = Declare.declare_constant id cdecl in @@ -203,16 +203,10 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) nf t in Pretyping.check_evars env Evd.empty !evars (EConstr.of_constr termtype); - let ctx = Evd.check_univ_decl !evars decl in - let ctx = if poly - then Polymorphic_const_entry ctx - else - (* FIXME be smarter about this *) - Monomorphic_const_entry (Univ.ContextSet.of_context ctx) - in + let univs = Evd.check_univ_decl ~poly !evars decl in let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id (ParameterEntry - (None,(termtype,ctx),None), Decl_kinds.IsAssumption Decl_kinds.Logical) + (None,(termtype,univs),None), Decl_kinds.IsAssumption Decl_kinds.Logical) in Universes.register_universe_binders (ConstRef cst) (Evd.universe_binders !evars); instance_hook k pri global imps ?hook (ConstRef cst); id @@ -391,19 +385,16 @@ let context poly l = let fn status (id, b, t) = if Lib.is_modtype () && not (Lib.sections_are_opened ()) then (* Declare the universe context once *) - let univs = !uctx in + let univs = if poly + then Polymorphic_const_entry (Univ.ContextSet.to_context !uctx) + else Monomorphic_const_entry !uctx + in let () = uctx := Univ.ContextSet.empty in let decl = match b with | None -> - let univs = if poly - then Polymorphic_const_entry (Univ.ContextSet.to_context univs) - else Monomorphic_const_entry univs - in (ParameterEntry (None,(t,univs),None), IsAssumption Logical) | Some b -> - (* FIXME be smarter about this *) - let univs = Univ.ContextSet.to_context univs in - let entry = Declare.definition_entry ~poly ~univs ~types:t b in + let entry = Declare.definition_entry ~univs ~types:t b in (DefinitionEntry entry, IsAssumption Logical) in let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id decl in @@ -426,9 +417,12 @@ let context poly l = pi3 (Command.declare_assumption false decl (t, !uctx) Universes.empty_binders [] impl Vernacexpr.NoInline (Loc.tag id)) | Some b -> - let ctx = Univ.ContextSet.to_context !uctx in + let univs = if poly + then Polymorphic_const_entry (Univ.ContextSet.to_context !uctx) + else Monomorphic_const_entry !uctx + in let decl = (Discharge, poly, Definition) in - let entry = Declare.definition_entry ~poly ~univs:ctx ~types:t b in + let entry = Declare.definition_entry ~univs ~types:t b in let hook = Lemmas.mk_hook (fun _ gr -> gr) in let _ = DeclareDef.declare_definition id decl entry Universes.empty_binders [] hook in Lib.sections_are_opened () || Lib.is_modtype_strict () diff --git a/vernac/command.ml b/vernac/command.ml index 06d0c8470e..1a8b16a893 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -88,7 +88,7 @@ let warn_implicits_in_term = strbrk "Implicit arguments declaration relies on type." ++ spc () ++ strbrk "The term declares more implicits than the type here.") -let interp_definition pl bl p red_option c ctypopt = +let interp_definition pl bl poly red_option c ctypopt = let env = Global.env() in let evd, decl = Univdecls.interp_univ_decl_opt env pl in let evdref = ref evd in @@ -105,15 +105,15 @@ let interp_definition pl bl p red_option c ctypopt = let c = EConstr.Unsafe.to_constr c in let nf,subst = Evarutil.e_nf_evars_and_universes evdref in let body = nf (it_mkLambda_or_LetIn c ctx) in - let vars = Univops.universes_of_constr body in - let evd = Evd.restrict_universe_context !evdref vars in - let uctx = Evd.check_univ_decl evd decl in + let vars = Univops.universes_of_constr body in + let evd = Evd.restrict_universe_context !evdref vars in + let uctx = Evd.check_univ_decl ~poly evd decl in let binders = Evd.universe_binders evd in imps1@(Impargs.lift_implicits nb_args imps2), binders, - definition_entry ~univs:uctx ~poly:p body + definition_entry ~univs:uctx body | Some ctyp -> - let ty, impsty = interp_type_evars_impls ~impls env_bl evdref ctyp in - let subst = evd_comb0 Evd.nf_univ_variables evdref in + let ty, impsty = interp_type_evars_impls ~impls env_bl evdref ctyp in + let subst = evd_comb0 Evd.nf_univ_variables evdref in let ctx = Context.Rel.map (Vars.subst_univs_constr subst) ctx in let env_bl = push_rel_context ctx env in let c, imps2 = interp_casted_constr_evars_impls ~impls env_bl evdref c ty in @@ -134,10 +134,10 @@ let interp_definition pl bl p red_option c ctypopt = let vars = Univ.LSet.union (Univops.universes_of_constr body) (Univops.universes_of_constr typ) in let ctx = Evd.restrict_universe_context !evdref vars in - let uctx = Evd.check_univ_decl ctx decl in + let uctx = Evd.check_univ_decl ~poly ctx decl in let binders = Evd.universe_binders evd in imps1@(Impargs.lift_implicits nb_args impsty), binders, - definition_entry ~types:typ ~poly:p + definition_entry ~types:typ ~univs:uctx body in red_constant_entry (Context.Rel.length ctx) ce !evdref red_option, !evdref, decl, pl, imps @@ -282,9 +282,14 @@ let do_assumptions_bound_univs coe kind nl id pl c = let ty = nf ty in let vars = Univops.universes_of_constr ty in let evd = Evd.restrict_universe_context !evdref vars in - let uctx = Evd.check_univ_decl evd decl in + let uctx = Evd.check_univ_decl ~poly:(pi2 kind) evd decl in let binders = Evd.universe_binders evd in - let uctx = Univ.ContextSet.of_context uctx in + let uctx = match uctx with + | Polymorphic_const_entry uctx -> + (* ?? *) + Univ.ContextSet.of_context uctx + | Monomorphic_const_entry uctx -> uctx + in let (_, _, st) = declare_assumption coe kind (ty, uctx) binders impls false nl id in st @@ -582,7 +587,7 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite = let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf' cl,impsl)) constructors in let ctx_params = Context.Rel.map nf ctx_params in let evd = !evdref in - let uctx = Evd.check_univ_decl evd decl in + let uctx = Evd.check_univ_decl ~poly evd decl in List.iter (fun c -> check_evars env_params Evd.empty evd (EConstr.of_constr c)) arities; Context.Rel.iter (fun c -> check_evars env0 Evd.empty evd (EConstr.of_constr c)) ctx_params; List.iter (fun (_,ctyps,_) -> @@ -604,12 +609,13 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite = userimpls @ (lift_implicits len impls)) cimpls) indimpls constructors in let univs = - if poly then + match uctx with + | Polymorphic_const_entry uctx -> if cum then Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context uctx) else Polymorphic_ind_entry uctx - else - Monomorphic_ind_entry (Univ.ContextSet.of_context uctx) + | Monomorphic_const_entry uctx -> + Monomorphic_ind_entry uctx in (* Build the mutual inductive entry *) let mind_ent = @@ -1032,9 +1038,9 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = let body = it_mkLambda_or_LetIn (mkApp (Evarutil.e_new_global evdref gr, [|make|])) binders_rel in let ty = it_mkProd_or_LetIn top_arity binders_rel in let ty = EConstr.Unsafe.to_constr ty in - let univs = Evd.check_univ_decl !evdref decl in + let univs = Evd.check_univ_decl ~poly !evdref decl in (*FIXME poly? *) - let ce = definition_entry ~poly ~types:ty ~univs (EConstr.to_constr !evdref body) in + let ce = definition_entry ~types:ty ~univs (EConstr.to_constr !evdref body) in (** FIXME: include locality *) let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in let gr = ConstRef c in @@ -1173,7 +1179,7 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind List.map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in let evd = Evd.from_ctx ctx in let evd = Evd.restrict_universe_context evd vars in - let ctx = Evd.check_univ_decl evd pl in + let ctx = Evd.check_univ_decl ~poly evd pl in let pl = Evd.universe_binders evd in let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in ignore (List.map4 (DeclareDef.declare_fix (local, poly, Fixpoint) pl ctx) @@ -1206,7 +1212,7 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n let fiximps = List.map (fun (len,imps,idx) -> imps) fiximps in let evd = Evd.from_ctx ctx in let evd = Evd.restrict_universe_context evd vars in - let ctx = Evd.check_univ_decl evd pl in + let ctx = Evd.check_univ_decl ~poly evd pl in let pl = Evd.universe_binders evd in ignore (List.map4 (DeclareDef.declare_fix (local, poly, CoFixpoint) pl ctx) fixnames fixdecls fixtypes fiximps); diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index c18744052e..980db4109a 100644 --- a/vernac/declareDef.ml +++ b/vernac/declareDef.ml @@ -57,7 +57,7 @@ let declare_definition ident (local, p, k) ce pl imps hook = declare_global_definition ident ce local k pl imps in Lemmas.call_hook fix_exn hook local r -let declare_fix ?(opaque = false) (_,poly,_ as kind) pl ctx f ((def,_),eff) t imps = - let ce = definition_entry ~opaque ~types:t ~poly ~univs:ctx ~eff def in +let declare_fix ?(opaque = false) (_,poly,_ as kind) pl univs f ((def,_),eff) t imps = + let ce = definition_entry ~opaque ~types:t ~univs ~eff def in declare_definition f kind ce pl imps (Lemmas.mk_hook (fun _ r -> r)) diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli index 01a87818a3..55f7c78616 100644 --- a/vernac/declareDef.mli +++ b/vernac/declareDef.mli @@ -15,5 +15,8 @@ val declare_definition : Id.t -> definition_kind -> Safe_typing.private_constants Entries.definition_entry -> Universes.universe_binders -> Impargs.manual_implicits -> Globnames.global_reference Lemmas.declaration_hook -> Globnames.global_reference -val declare_fix : ?opaque:bool -> definition_kind -> Universes.universe_binders -> Univ.UContext.t -> Id.t -> - Safe_typing.private_constants Entries.proof_output -> Constr.types -> Impargs.manual_implicits -> Globnames.global_reference +val declare_fix : ?opaque:bool -> definition_kind -> + Universes.universe_binders -> Entries.constant_universes_entry -> + Id.t -> Safe_typing.private_constants Entries.proof_output -> + Constr.types -> Impargs.manual_implicits -> + Globnames.global_reference diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index f59b5fcae9..a787ec6fac 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -224,7 +224,7 @@ let compute_proof_name locality = function let avoid = Id.Set.of_list (Proof_global.get_all_proof_names ()) in next_global_ident_away default_thm_id avoid -let save_remaining_recthms (locality,p,kind) norm ctx body opaq i (id,(t_i,(_,imps))) = +let save_remaining_recthms (locality,p,kind) norm univs body opaq i (id,(t_i,(_,imps))) = let t_i = norm t_i in match body with | None -> @@ -232,7 +232,13 @@ let save_remaining_recthms (locality,p,kind) norm ctx body opaq i (id,(t_i,(_,im | Discharge -> let impl = false in (* copy values from Vernacentries *) let k = IsAssumption Conjectural in - let c = SectionLocalAssum ((t_i,Univ.ContextSet.of_context ctx),p,impl) in + let univs = match univs with + | Polymorphic_const_entry univs -> + (* What is going on here? *) + Univ.ContextSet.of_context univs + | Monomorphic_const_entry univs -> univs + in + let c = SectionLocalAssum ((t_i, univs),p,impl) in let _ = declare_variable id (Lib.cwd(),c,k) in (Discharge, VarRef id,imps) | Local | Global -> @@ -242,11 +248,7 @@ let save_remaining_recthms (locality,p,kind) norm ctx body opaq i (id,(t_i,(_,im | Global -> false | Discharge -> assert false in - let ctx = if p - then Polymorphic_const_entry ctx - else Monomorphic_const_entry (Univ.ContextSet.of_context ctx) - in - let decl = (ParameterEntry (None,(t_i,ctx),None), k) in + let decl = (ParameterEntry (None,(t_i,univs),None), k) in let kn = declare_constant id ~local decl in (locality,ConstRef kn,imps)) | Some body -> @@ -264,8 +266,7 @@ let save_remaining_recthms (locality,p,kind) norm ctx body opaq i (id,(t_i,(_,im let body_i = body_i body in match locality with | Discharge -> - let const = definition_entry ~types:t_i ~opaque:opaq ~poly:p - ~univs:ctx body_i in + let const = definition_entry ~types:t_i ~opaque:opaq ~univs body_i in let c = SectionLocalDef const in let _ = declare_variable id (Lib.cwd(), c, k) in (Discharge,VarRef id,imps) @@ -276,7 +277,7 @@ let save_remaining_recthms (locality,p,kind) norm ctx body opaq i (id,(t_i,(_,im | Discharge -> assert false in let const = - Declare.definition_entry ~types:t_i ~poly:p ~univs:ctx ~opaque:opaq body_i + Declare.definition_entry ~types:t_i ~univs ~opaque:opaq body_i in let kn = declare_constant id ~local (DefinitionEntry const, k) in (locality,ConstRef kn,imps) @@ -425,7 +426,7 @@ let start_proof_with_initialization kind ctx decl recguard thms snl hook = let body,opaq = retrieve_first_recthm ctx ref in let subst = Evd.evar_universe_context_subst ctx in let norm c = Universes.subst_opt_univs_constr subst c in - let ctx = UState.check_univ_decl ctx decl in + let ctx = UState.check_univ_decl ~poly:(pi2 kind) ctx decl in let body = Option.map norm body in List.map_i (save_remaining_recthms kind norm ctx body opaq) 1 other_thms in let thms_data = (strength,ref,imps)::other_thms_data in @@ -460,7 +461,7 @@ let start_proof_com ?inference_hook kind thms hook = let () = let open Misctypes in if not (decl.univdecl_extensible_instance && decl.univdecl_extensible_constraints) then - ignore (Evd.check_univ_decl evd decl) + ignore (Evd.check_univ_decl ~poly:(pi2 kind) evd decl) in let evd = if pi2 kind then evd @@ -495,10 +496,7 @@ let save_proof ?proof = function if const_entry_type = None then user_err Pp.(str "Admitted requires an explicit statement"); let typ = Option.get const_entry_type in - let ctx = if pi2 k (* polymorphic *) - then Polymorphic_const_entry (UState.context (fst universes)) - else Monomorphic_const_entry (UState.context_set (fst universes)) - in + let ctx = UState.const_univ_entry ~poly:(pi2 k) (fst universes) in let sec_vars = if !keep_admitted_vars then const_entry_secctx else None in Admitted(id, k, (sec_vars, (typ, ctx), None), universes) | None -> @@ -521,12 +519,8 @@ let save_proof ?proof = function | _ -> None in let decl = Proof_global.get_universe_decl () in let evd = Evd.from_ctx universes in - let ctx = Evd.check_univ_decl evd decl in let poly = pi2 k in - let ctx = if poly - then Polymorphic_const_entry ctx - else Monomorphic_const_entry (Univ.ContextSet.of_context ctx) - in + let ctx = Evd.check_univ_decl ~poly evd decl in let binders = if poly then Some (UState.universe_binders universes) else None in Admitted(id,k,(sec_vars, (typ, ctx), None), (universes, binders)) diff --git a/vernac/obligations.ml b/vernac/obligations.ml index a9110c76cb..97cdd7977c 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -475,12 +475,8 @@ let declare_definition prg = (Evd.evar_universe_context_subst prg.prg_ctx) in let opaque = prg.prg_opaque in let fix_exn = Hook.get get_fix_exn () in - let () = ignore(UState.check_univ_decl prg.prg_ctx prg.prg_univdecl) in - let ce = - definition_entry ~fix_exn - ~opaque ~types:(nf typ) ~poly:(pi2 prg.prg_kind) - ~univs:(UState.context prg.prg_ctx) (nf body) - in + let univs = UState.check_univ_decl ~poly:(pi2 prg.prg_kind) prg.prg_ctx prg.prg_univdecl in + let ce = definition_entry ~fix_exn ~opaque ~types:(nf typ) ~univs (nf body) in let () = progmap_remove prg in let ubinders = UState.universe_binders prg.prg_ctx in DeclareDef.declare_definition prg.prg_name @@ -549,9 +545,9 @@ let declare_mutual_definition l = mk_proof (mkCoFix (i,fixdecls))) 0 l in (* Declare the recursive definitions *) - let ctx = UState.context first.prg_ctx in + let univs = UState.const_univ_entry ~poly first.prg_ctx in let fix_exn = Hook.get get_fix_exn () in - let kns = List.map4 (DeclareDef.declare_fix ~opaque (local, poly, kind) Universes.empty_binders ctx) + let kns = List.map4 (DeclareDef.declare_fix ~opaque (local, poly, kind) Universes.empty_binders univs) fixnames fixdecls fixtypes fiximps in (* Declare notations *) List.iter (Metasyntax.add_notation_interpretation (Global.env())) first.prg_notations; @@ -856,10 +852,7 @@ let obligation_terminator name num guard hook auto pf = | (_, status), Vernacexpr.Transparent -> status in let obl = { obl with obl_status = false, status } in - let uctx = if pi2 prg.prg_kind - then Polymorphic_const_entry (UState.context ctx) - else Monomorphic_const_entry (UState.context_set ctx) - in + let uctx = UState.const_univ_entry ~poly:(pi2 prg.prg_kind) ctx in let (_, obl) = declare_obligation prg obl body ty uctx in let obls = Array.copy obls in let _ = obls.(num) <- obl in diff --git a/vernac/record.ml b/vernac/record.ml index faf277d86d..1d255b08e0 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -95,7 +95,7 @@ let binder_of_decl = function let binders_of_decls = List.map binder_of_decl -let typecheck_params_and_fields finite def id pl t ps nots fs = +let typecheck_params_and_fields finite def id poly pl t ps nots fs = let env0 = Global.env () in let evd, decl = Univdecls.interp_univ_decl_opt env0 pl in let evars = ref evd in @@ -167,7 +167,7 @@ let typecheck_params_and_fields finite def id pl t ps nots fs = let newps = List.map (EConstr.to_rel_decl evars) newps in let typ = EConstr.to_constr evars typ in let ce t = Pretyping.check_evars env0 Evd.empty evars (EConstr.of_constr t) in - let univs = Evd.check_univ_decl evars decl in + let univs = Evd.check_univ_decl ~poly evars decl in let ubinders = Evd.universe_binders evars in List.iter (iter_constr ce) (List.rev newps); List.iter (iter_constr ce) (List.rev newfs); @@ -449,7 +449,7 @@ let implicits_of_context ctx = in ExplByPos (i, explname), (true, true, true)) 1 (List.rev (Anonymous :: (List.map RelDecl.get_name ctx))) -let declare_class finite def cum poly ubinders ctx id idbuild paramimpls params arity +let declare_class finite def cum ubinders univs id idbuild paramimpls params arity template fieldimpls fields ?(kind=StructureComponent) is_coe coers priorities sign = let fieldimpls = (* Make the class implicit in the projections, and the params if applicable. *) @@ -464,21 +464,21 @@ let declare_class finite def cum poly ubinders ctx id idbuild paramimpls params let class_body = it_mkLambda_or_LetIn field params in let class_type = it_mkProd_or_LetIn arity params in let class_entry = - Declare.definition_entry ~types:class_type ~poly ~univs:ctx class_body in + Declare.definition_entry ~types:class_type ~univs class_body in let cst = Declare.declare_constant (snd id) (DefinitionEntry class_entry, IsDefinition Definition) in - let cstu = (cst, if poly then Univ.UContext.instance ctx else Univ.Instance.empty) in + let cstu = (cst, match univs with + | Polymorphic_const_entry univs -> Univ.UContext.instance univs + | Monomorphic_const_entry _ -> Univ.Instance.empty) + in let inst_type = appvectc (mkConstU cstu) (Termops.rel_vect 0 (List.length params)) in let proj_type = it_mkProd_or_LetIn (mkProd(Name binder_name, inst_type, lift 1 field)) params in let proj_body = it_mkLambda_or_LetIn (mkLambda (Name binder_name, inst_type, mkRel 1)) params in - let proj_entry = - Declare.definition_entry ~types:proj_type ~poly - ~univs:(if poly then ctx else Univ.UContext.empty) proj_body - in + let proj_entry = Declare.definition_entry ~types:proj_type ~univs proj_body in let proj_cst = Declare.declare_constant proj_name (DefinitionEntry proj_entry, IsDefinition Definition) in @@ -495,13 +495,14 @@ let declare_class finite def cum poly ubinders ctx id idbuild paramimpls params cref, [Name proj_name, sub, Some proj_cst] | _ -> let univs = - if poly then + match univs with + | Polymorphic_const_entry univs -> if cum then - Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context ctx) + Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context univs) else - Polymorphic_ind_entry ctx - else - Monomorphic_ind_entry (Univ.ContextSet.of_context ctx) + Polymorphic_ind_entry univs + | Monomorphic_const_entry univs -> + Monomorphic_ind_entry univs in let ind = declare_structure BiFinite ubinders univs (snd id) idbuild paramimpls params arity template fieldimpls fields @@ -524,13 +525,15 @@ let declare_class finite def cum poly ubinders ctx id idbuild paramimpls params params, params in let univs, ctx_context, fields = - if poly then - let usubst, auctx = Univ.abstract_universes ctx in + match univs with + | Polymorphic_const_entry univs -> + let usubst, auctx = Univ.abstract_universes univs in let map c = Vars.subst_univs_level_constr usubst c in let fields = Context.Rel.map map fields in let ctx_context = on_snd (fun d -> Context.Rel.map map d) ctx_context in auctx, ctx_context, fields - else Univ.AUContext.empty, ctx_context, fields + | Monomorphic_const_entry _ -> + Univ.AUContext.empty, ctx_context, fields in let k = { cl_univs = univs; @@ -606,14 +609,14 @@ let definition_structure (kind,cum,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cf if isnot_class && List.exists (fun opt -> not (Option.is_empty opt)) priorities then user_err Pp.(str "Priorities only allowed for type class substructures"); (* Now, younger decl in params and fields is on top *) - let pl, ctx, arity, template, implpars, params, implfs, fields = + let pl, univs, arity, template, implpars, params, implfs, fields = States.with_state_protection (fun () -> - typecheck_params_and_fields finite (kind = Class true) idstruc pl s ps notations fs) () in + typecheck_params_and_fields finite (kind = Class true) idstruc poly pl s ps notations fs) () in let sign = structure_signature (fields@params) in match kind with | Class def -> let priorities = List.map (fun id -> {hint_priority = id; hint_pattern = None}) priorities in - let gr = declare_class finite def cum poly pl ctx (loc,idstruc) idbuild + let gr = declare_class finite def cum pl univs (loc,idstruc) idbuild implpars params arity template implfs fields is_coe coers priorities sign in gr | _ -> @@ -622,13 +625,14 @@ let definition_structure (kind,cum,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cf (succ (List.length params)) impls) implfs in let univs = - if poly then + match univs with + | Polymorphic_const_entry univs -> if cum then - Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context ctx) + Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context univs) else - Polymorphic_ind_entry ctx - else - Monomorphic_ind_entry (Univ.ContextSet.of_context ctx) + Polymorphic_ind_entry univs + | Monomorphic_const_entry univs -> + Monomorphic_ind_entry univs in let ind = declare_structure finite pl univs idstruc idbuild implpars params arity template implfs -- cgit v1.2.3 From e6c87412d70b71daaf417bd4b8e4ae6f1f28515b Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 24 Nov 2017 18:32:35 +0100 Subject: Fix obligations handling of universes anticipating stronger restrict --- vernac/obligations.ml | 94 +++++++++++++++++++++++++++++---------------------- 1 file changed, 54 insertions(+), 40 deletions(-) (limited to 'vernac') diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 97cdd7977c..17a596c42a 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -824,49 +824,63 @@ let obligation_terminator name num guard hook auto pf = match pf with | Admitted _ -> apply_terminator term pf | Proved (opq, id, proof) -> - if not !shrink_obligations then apply_terminator term pf - else - let (_, (entry, uctx, _)) = Pfedit.cook_this_proof proof in - let env = Global.env () in - let entry = Safe_typing.inline_private_constants_in_definition_entry env entry in - let ty = entry.Entries.const_entry_type in - let (body, cstr), () = Future.force entry.Entries.const_entry_body in - let sigma = Evd.from_ctx (fst uctx) in - let sigma = Evd.merge_context_set ~sideff:true Evd.univ_rigid sigma cstr in - Inductiveops.control_only_guard (Global.env ()) body; - (** Declare the obligation ourselves and drop the hook *) - let prg = get_info (ProgMap.find name !from_prg) in - (** Ensure universes are substituted properly in body and type *) - let body = EConstr.to_constr sigma (EConstr.of_constr body) in - let ty = Option.map (fun x -> EConstr.to_constr sigma (EConstr.of_constr x)) ty in - let ctx = Evd.evar_universe_context sigma in - let prg = { prg with prg_ctx = ctx } in - let obls, rem = prg.prg_obligations in - let obl = obls.(num) in - let status = - match obl.obl_status, opq with - | (_, Evar_kinds.Expand), Vernacexpr.Opaque -> err_not_transp () - | (true, _), Vernacexpr.Opaque -> err_not_transp () - | (false, _), Vernacexpr.Opaque -> Evar_kinds.Define true - | (_, Evar_kinds.Define true), Vernacexpr.Transparent -> Evar_kinds.Define false - | (_, status), Vernacexpr.Transparent -> status - in - let obl = { obl with obl_status = false, status } in - let uctx = UState.const_univ_entry ~poly:(pi2 prg.prg_kind) ctx in - let (_, obl) = declare_obligation prg obl body ty uctx in - let obls = Array.copy obls in - let _ = obls.(num) <- obl in - try + let (_, (entry, uctx, _)) = Pfedit.cook_this_proof proof in + let env = Global.env () in + let entry = Safe_typing.inline_private_constants_in_definition_entry env entry in + let ty = entry.Entries.const_entry_type in + let (body, cstr), () = Future.force entry.Entries.const_entry_body in + let sigma = Evd.from_ctx (fst uctx) in + let sigma = Evd.merge_context_set ~sideff:true Evd.univ_rigid sigma cstr in + Inductiveops.control_only_guard (Global.env ()) body; + (** Declare the obligation ourselves and drop the hook *) + let prg = get_info (ProgMap.find name !from_prg) in + (** Ensure universes are substituted properly in body and type *) + let body = EConstr.to_constr sigma (EConstr.of_constr body) in + let ty = Option.map (fun x -> EConstr.to_constr sigma (EConstr.of_constr x)) ty in + let ctx = Evd.evar_universe_context sigma in + let obls, rem = prg.prg_obligations in + let obl = obls.(num) in + let status = + match obl.obl_status, opq with + | (_, Evar_kinds.Expand), Vernacexpr.Opaque -> err_not_transp () + | (true, _), Vernacexpr.Opaque -> err_not_transp () + | (false, _), Vernacexpr.Opaque -> Evar_kinds.Define true + | (_, Evar_kinds.Define true), Vernacexpr.Transparent -> + Evar_kinds.Define false + | (_, status), Vernacexpr.Transparent -> status + in + let obl = { obl with obl_status = false, status } in + let ctx = + if pi2 prg.prg_kind then ctx + else UState.union prg.prg_ctx ctx + in + let uctx = UState.const_univ_entry ~poly:(pi2 prg.prg_kind) ctx in + let (_, obl) = declare_obligation prg obl body ty uctx in + let obls = Array.copy obls in + let _ = obls.(num) <- obl in + let prg_ctx = + if pi2 (prg.prg_kind) then (* Polymorphic *) + (** We merge the new universes and constraints of the + polymorphic obligation with the existing ones *) + UState.union prg.prg_ctx ctx + else + (** The first obligation declares the univs of the constant, + each subsequent obligation declares its own additional + universes and constraints if any *) + UState.make (Global.universes ()) + in + let prg = { prg with prg_ctx } in + try ignore (update_obls prg obls (pred rem)); if pred rem > 0 then begin - let deps = dependencies obls num in - if not (Int.Set.is_empty deps) then - ignore (auto (Some name) None deps) - end - with e when CErrors.noncritical e -> - let e = CErrors.push e in - pperror (CErrors.iprint (ExplainErr.process_vernac_interp_error e)) + let deps = dependencies obls num in + if not (Int.Set.is_empty deps) then + ignore (auto (Some name) None deps) + end + with e when CErrors.noncritical e -> + let e = CErrors.push e in + pperror (CErrors.iprint (ExplainErr.process_vernac_interp_error e)) let obligation_hook prg obl num auto ctx' _ gr = let obls, rem = prg.prg_obligations in -- cgit v1.2.3 From 280c922fc55b57c430cad721c83650a796a375fd Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Wed, 20 Sep 2017 19:45:43 +0200 Subject: Allow local universe renaming in Print. --- vernac/vernacentries.ml | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) (limited to 'vernac') diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index e2f28a371a..22e3e9c99c 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1609,9 +1609,10 @@ exception NoHyp (* Printing "About" information of a hypothesis of the current goal. We only print the type and a small statement to this comes from the goal. Precondition: there must be at least one current goal. *) -let print_about_hyp_globs ?loc ref_or_by_not glopt = +let print_about_hyp_globs ?loc ref_or_by_not udecl glopt = let open Context.Named.Declaration in try + (* FIXME error on non None udecl if we find the hyp. *) let glnumopt = query_command_selector ?loc glopt in let gl,id = match glnumopt,ref_or_by_not with @@ -1634,7 +1635,7 @@ let print_about_hyp_globs ?loc ref_or_by_not glopt = with (* fallback to globals *) | NoHyp | Not_found -> let sigma, env = Pfedit.get_current_context () in - print_about env sigma ref_or_by_not + print_about env sigma ref_or_by_not udecl let vernac_print ?loc env sigma = let open Feedback in function @@ -1651,7 +1652,7 @@ let vernac_print ?loc env sigma = let open Feedback in function | PrintMLLoadPath -> msg_notice (Mltop.print_ml_path ()) | PrintMLModules -> msg_notice (Mltop.print_ml_modules ()) | PrintDebugGC -> msg_notice (Mltop.print_gc ()) - | PrintName qid -> dump_global qid; msg_notice (print_name env sigma qid) + | PrintName (qid,udecl) -> dump_global qid; msg_notice (print_name env sigma qid udecl) | PrintGraph -> msg_notice (Prettyp.print_graph()) | PrintClasses -> msg_notice (Prettyp.print_classes()) | PrintTypeClasses -> msg_notice (Prettyp.print_typeclasses()) @@ -1681,8 +1682,8 @@ let vernac_print ?loc env sigma = let open Feedback in function msg_notice (Notation.pr_scope (Constrextern.without_symbols (pr_lglob_constr_env env)) s) | PrintVisibility s -> msg_notice (Notation.pr_visibility (Constrextern.without_symbols (pr_lglob_constr_env env)) s) - | PrintAbout (ref_or_by_not,glnumopt) -> - msg_notice (print_about_hyp_globs ?loc ref_or_by_not glnumopt) + | PrintAbout (ref_or_by_not,udecl,glnumopt) -> + msg_notice (print_about_hyp_globs ?loc ref_or_by_not udecl glnumopt) | PrintImplicit qid -> dump_global qid; msg_notice (print_impargs qid) | PrintAssumptions (o,t,r) -> -- cgit v1.2.3 From 765392492df2f5e065b2b5e706b6620846337cc0 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 21 Sep 2017 00:53:10 +0200 Subject: Universe binders survive sections, modules and compilation. --- vernac/lemmas.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'vernac') diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index a787ec6fac..42631a15be 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -204,7 +204,7 @@ let save ?export_seff id const cstrs pl do_guard (locality,poly,kind) hook = (locality, ConstRef kn) in definition_message id; - Option.iter (Universes.register_universe_binders r) pl; + Universes.register_universe_binders r (Option.default Universes.empty_binders pl); call_hook (fun exn -> exn) hook l r with e when CErrors.noncritical e -> let e = CErrors.push e in @@ -312,7 +312,7 @@ let admit (id,k,e) pl hook () = | Local, _, _ | Discharge, _, _ -> warn_let_as_axiom id in let () = assumption_message id in - Option.iter (Universes.register_universe_binders (ConstRef kn)) pl; + Universes.register_universe_binders (ConstRef kn) (Option.default Universes.empty_binders pl); call_hook (fun exn -> exn) hook Global (ConstRef kn) (* Starting a goal *) -- cgit v1.2.3 From 4940f99922b0784d726b7c50abe63395713f012f Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Fri, 17 Nov 2017 23:48:21 +0100 Subject: Fix #5347: unify declaration of axioms with and without bound univs. Note that this makes the following syntax valid: Axiom foo@{i} bar : Type@{i}. (ie putting a universe declaration on the first axiom in the list, the declaration then holds for the whole list). --- vernac/classes.ml | 10 ++-- vernac/command.ml | 145 ++++++++++++++++++++++++++--------------------------- vernac/command.mli | 2 +- 3 files changed, 77 insertions(+), 80 deletions(-) (limited to 'vernac') diff --git a/vernac/classes.ml b/vernac/classes.ml index 1833b7a1dd..b80741269f 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -412,15 +412,15 @@ let context poly l = in let impl = List.exists test impls in let decl = (Discharge, poly, Definitional) in + let univs = if poly + then Polymorphic_const_entry (Univ.ContextSet.to_context !uctx) + else Monomorphic_const_entry !uctx + in let nstatus = match b with | None -> - pi3 (Command.declare_assumption false decl (t, !uctx) Universes.empty_binders [] impl + pi3 (Command.declare_assumption false decl (t, univs) Universes.empty_binders [] impl Vernacexpr.NoInline (Loc.tag id)) | Some b -> - let univs = if poly - then Polymorphic_const_entry (Univ.ContextSet.to_context !uctx) - else Monomorphic_const_entry !uctx - in let decl = (Discharge, poly, Definition) in let entry = Declare.definition_entry ~univs ~types:t b in let hook = Lemmas.mk_hook (fun _ gr -> gr) in diff --git a/vernac/command.ml b/vernac/command.ml index 1a8b16a893..373e5a1be2 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -177,6 +177,10 @@ let do_definition ident k univdecl bl red_option c ctypopt hook = let declare_assumption is_coe (local,p,kind) (c,ctx) pl imps impl nl (_,ident) = match local with | Discharge when Lib.sections_are_opened () -> + let ctx = match ctx with + | Monomorphic_const_entry ctx -> ctx + | Polymorphic_const_entry ctx -> Univ.ContextSet.of_context ctx + in let decl = (Lib.cwd(), SectionLocalAssum ((c,ctx),p,impl), IsAssumption kind) in let _ = declare_variable ident decl in let () = assumption_message ident in @@ -197,10 +201,6 @@ match local with | DefaultInline -> Some (Flags.get_inline_level()) | InlineAt i -> Some i in - let ctx = if p - then Polymorphic_const_entry (Univ.ContextSet.to_context ctx) - else Monomorphic_const_entry ctx - in let decl = (ParameterEntry (None,(c,ctx),inl), IsAssumption kind) in let kn = declare_constant ident ~local decl in let gr = ConstRef kn in @@ -221,26 +221,63 @@ let interp_assumption evdref env impls bl c = let ty = EConstr.Unsafe.to_constr ty in (ty, impls) -let declare_assumptions idl is_coe k (c,ctx) pl imps impl_is_on nl = +(* When monomorphic the universe constraints are declared with the first declaration only. *) +let next_uctx = + let empty_uctx = Monomorphic_const_entry Univ.ContextSet.empty in + function + | Polymorphic_const_entry _ as uctx -> uctx + | Monomorphic_const_entry _ -> empty_uctx + +let declare_assumptions idl is_coe k (c,uctx) pl imps nl = let refs, status, _ = - List.fold_left (fun (refs,status,ctx) id -> + List.fold_left (fun (refs,status,uctx) id -> let ref',u',status' = - declare_assumption is_coe k (c,ctx) pl imps impl_is_on nl id in - (ref',u')::refs, status' && status, Univ.ContextSet.empty) - ([],true,ctx) idl + declare_assumption is_coe k (c,uctx) pl imps false nl id in + (ref',u')::refs, status' && status, next_uctx uctx) + ([],true,uctx) idl in List.rev refs, status -let do_assumptions_unbound_univs (_, poly, _ as kind) nl l = + +let maybe_error_many_udecls = function + | ((loc,id), Some _) -> + user_err ?loc ~hdr:"many_universe_declarations" + Pp.(str "When declaring multiple axioms in one command, " ++ + str "only the first is allowed a universe binder " ++ + str "(which will be shared by the whole block).") + | (_, None) -> () + +let process_assumptions_udecls kind l = + let udecl, first_id = match l with + | (coe, ((id, udecl)::rest, c))::rest' -> + List.iter maybe_error_many_udecls rest; + List.iter (fun (coe, (idl, c)) -> List.iter maybe_error_many_udecls idl) rest'; + udecl, id + | (_, ([], _))::_ | [] -> assert false + in + let () = match kind, udecl with + | (Discharge, _, _), Some _ when Lib.sections_are_opened () -> + let loc = fst first_id in + let msg = Pp.str "Section variables cannot be polymorphic." in + user_err ?loc msg + | _ -> () + in + udecl, List.map (fun (coe, (idl, c)) -> coe, (List.map fst idl, c)) l + +let do_assumptions kind nl l = let open Context.Named.Declaration in let env = Global.env () in - let evdref = ref (Evd.from_env env) in - let l = - if poly then + let udecl, l = process_assumptions_udecls kind l in + let evdref, udecl = + let evd, udecl = Univdecls.interp_univ_decl_opt env udecl in + ref evd, udecl + in + let l = + if pi2 kind (* poly *) then (* Separate declarations so that A B : Type puts A and B in different levels. *) List.fold_right (fun (is_coe,(idl,c)) acc -> - List.fold_right (fun id acc -> - (is_coe, ([id], c)) :: acc) idl acc) + List.fold_right (fun id acc -> + (is_coe, ([id], c)) :: acc) idl acc) l [] else l in @@ -252,71 +289,31 @@ let do_assumptions_unbound_univs (_, poly, _ as kind) nl l = let ienv = List.fold_right (fun (_,id) ienv -> let impls = compute_internalization_data env Variable t imps in Id.Map.add id impls ienv) idl ienv in - ((env,ienv),((is_coe,idl),t,imps))) + ((env,ienv),((is_coe,idl),t,imps))) (env,empty_internalization_env) l in let evd = solve_remaining_evars all_and_fail_flags env !evdref Evd.empty in (* The universe constraints come from the whole telescope. *) let evd = Evd.nf_constraints evd in - let ctx = Evd.universe_context_set evd in - let nf_evar c = EConstr.Unsafe.to_constr (nf_evar evd (EConstr.of_constr c)) in - let l = List.map (on_pi2 nf_evar) l in - pi2 (List.fold_left (fun (subst,status,ctx) ((is_coe,idl),t,imps) -> - let t = replace_vars subst t in - let (refs,status') = declare_assumptions idl is_coe kind (t,ctx) Universes.empty_binders imps false nl in - let subst' = List.map2 - (fun (_,id) (c,u) -> (id,Universes.constr_of_global_univ (c,u))) - idl refs - in - (subst'@subst, status' && status, - (* The universe constraints are declared with the first declaration only. *) - Univ.ContextSet.empty)) ([],true,ctx) l) - -let do_assumptions_bound_univs coe kind nl id pl c = - let env = Global.env () in - let evd, decl = Univdecls.interp_univ_decl_opt env pl in - let evdref = ref evd in - let ty, impls = interp_type_evars_impls env evdref c in - let nf, subst = Evarutil.e_nf_evars_and_universes evdref in - let ty = EConstr.Unsafe.to_constr ty in - let ty = nf ty in - let vars = Univops.universes_of_constr ty in - let evd = Evd.restrict_universe_context !evdref vars in - let uctx = Evd.check_univ_decl ~poly:(pi2 kind) evd decl in - let binders = Evd.universe_binders evd in - let uctx = match uctx with - | Polymorphic_const_entry uctx -> - (* ?? *) - Univ.ContextSet.of_context uctx - | Monomorphic_const_entry uctx -> uctx + let nf_evar c = EConstr.to_constr evd (EConstr.of_constr c) in + let uvars, l = List.fold_left_map (fun uvars (coe,t,imps) -> + let t = nf_evar t in + let uvars = Univ.LSet.union uvars (Univops.universes_of_constr t) in + uvars, (coe,t,imps)) + Univ.LSet.empty l in - let (_, _, st) = declare_assumption coe kind (ty, uctx) binders impls false nl id in - st - -let do_assumptions kind nl l = match l with -| [coe, ([id, Some pl], c)] -> - let () = match kind with - | (Discharge, _, _) when Lib.sections_are_opened () -> - let loc = fst id in - let msg = Pp.str "Section variables cannot be polymorphic." in - user_err ?loc msg - | _ -> () - in - do_assumptions_bound_univs coe kind nl id (Some pl) c -| _ -> - let map (coe, (idl, c)) = - let map (id, univs) = match univs with - | None -> id - | Some _ -> - let loc = fst id in - let msg = - Pp.str "Assumptions with bound universes can only be defined one at a time." in - user_err ?loc msg - in - (coe, (List.map map idl, c)) - in - let l = List.map map l in - do_assumptions_unbound_univs kind nl l + let evd = Evd.restrict_universe_context evd uvars in + let uctx = Evd.check_univ_decl ~poly:(pi2 kind) evd udecl in + let ubinders = Evd.universe_binders evd in + pi2 (List.fold_left (fun (subst,status,uctx) ((is_coe,idl),t,imps) -> + let t = replace_vars subst t in + let refs, status' = declare_assumptions idl is_coe kind (t,uctx) ubinders imps nl in + let subst' = List.map2 + (fun (_,id) (c,u) -> (id, Universes.constr_of_global_univ (c,u))) + idl refs + in + subst'@subst, status' && status, next_uctx uctx) + ([], true, uctx) l) (* 3a| Elimination schemes for mutual inductive definitions *) diff --git a/vernac/command.mli b/vernac/command.mli index fb99a717b9..070f3e1120 100644 --- a/vernac/command.mli +++ b/vernac/command.mli @@ -43,7 +43,7 @@ val do_definition : Id.t -> definition_kind -> Vernacexpr.universe_decl_expr opt (** returns [false] if the assumption is neither local to a section, nor in a module type and meant to be instantiated. *) val declare_assumption : coercion_flag -> assumption_kind -> - types Univ.in_universe_context_set -> + types in_constant_universes_entry -> Universes.universe_binders -> Impargs.manual_implicits -> bool (** implicit *) -> Vernacexpr.inline -> variable Loc.located -> global_reference * Univ.Instance.t * bool -- cgit v1.2.3 From edb2b2535d62b37c324c98b28802c1b1699d4014 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Sat, 25 Nov 2017 22:08:01 +0100 Subject: Restrict universe context when declaring constants in obligations. --- vernac/obligations.ml | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) (limited to 'vernac') diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 17a596c42a..570f2e5b33 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -475,13 +475,17 @@ let declare_definition prg = (Evd.evar_universe_context_subst prg.prg_ctx) in let opaque = prg.prg_opaque in let fix_exn = Hook.get get_fix_exn () in - let univs = UState.check_univ_decl ~poly:(pi2 prg.prg_kind) prg.prg_ctx prg.prg_univdecl in - let ce = definition_entry ~fix_exn ~opaque ~types:(nf typ) ~univs (nf body) in + let typ = nf typ in + let body = nf body in + let uvars = Univ.LSet.union (Univops.universes_of_constr typ) (Univops.universes_of_constr body) in + let uctx = UState.restrict prg.prg_ctx uvars in + let univs = UState.check_univ_decl ~poly:(pi2 prg.prg_kind) uctx prg.prg_univdecl in + let ce = definition_entry ~fix_exn ~opaque ~types:typ ~univs body in let () = progmap_remove prg in - let ubinders = UState.universe_binders prg.prg_ctx in + let ubinders = UState.universe_binders uctx in DeclareDef.declare_definition prg.prg_name prg.prg_kind ce ubinders prg.prg_implicits - (Lemmas.mk_hook (fun l r -> Lemmas.call_hook fix_exn prg.prg_hook l r prg.prg_ctx; r)) + (Lemmas.mk_hook (fun l r -> Lemmas.call_hook fix_exn prg.prg_hook l r uctx; r)) let rec lam_index n t acc = match Constr.kind t with -- cgit v1.2.3