From 603bfb392805fb8d1559d304bcf1b9c7b938bb6e Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 11 Jul 2017 17:16:18 +0200 Subject: Getting rid of AUContext abstraction breakers in Recordops. --- API/API.mli | 7 ++++++- pretyping/evarconv.ml | 3 ++- pretyping/recordops.ml | 8 +++----- pretyping/recordops.mli | 2 +- 4 files changed, 12 insertions(+), 8 deletions(-) diff --git a/API/API.mli b/API/API.mli index 9f7a6ded81..a661b34c5b 100644 --- a/API/API.mli +++ b/API/API.mli @@ -84,6 +84,11 @@ sig val empty : t end + module AUContext : + sig + type t = Univ.AUContext.t + end + type universe_context = UContext.t [@@ocaml.deprecated "alias of API.Univ.UContext.t"] @@ -2884,7 +2889,7 @@ sig | Default_cs type obj_typ = Recordops.obj_typ = { o_DEF : Term.constr; - o_CTX : Univ.ContextSet.t; + o_CTX : Univ.AUContext.t; o_INJ : int option; (** position of trivial argument *) o_TABS : Term.constr list; (** ordered *) o_TPARAMS : Term.constr list; (** ordered *) diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 87f29ba492..cb76df4e8a 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -205,7 +205,8 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) = else match (Stack.strip_n_app (l_us-1) sk2_effective) with | None -> raise Not_found | Some (l',el,s') -> (l'@Stack.append_app [|el|] Stack.empty,s') in - let subst, ctx' = Universes.fresh_universe_context_set_instance ctx in + let u, ctx' = Universes.fresh_instance_from ctx None in + let subst = Univ.make_inverse_instance_subst u in let c = EConstr.of_constr c in let c' = subst_univs_level_constr subst c in let t' = EConstr.of_constr t' in diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index c498089ca8..a23579609a 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -134,7 +134,7 @@ let find_projection = function type obj_typ = { o_DEF : constr; - o_CTX : Univ.ContextSet.t; + o_CTX : Univ.AUContext.t; o_INJ : int option; (* position of trivial argument if any *) o_TABS : constr list; (* ordered *) o_TPARAMS : constr list; (* ordered *) @@ -203,10 +203,8 @@ let warn_projection_no_head_constant = let compute_canonical_projections warn (con,ind) = let env = Global.env () in let ctx = Environ.constant_context env con in - let u = Univ.AUContext.instance ctx in - let ctx = Univ.UContext.make (u, Univ.AUContext.instantiate u ctx) in + let u = Univ.make_abstract_instance ctx in let v = (mkConstU (con,u)) in - let ctx = Univ.ContextSet.of_context ctx in let c = Environ.constant_value_in env (con,u) in let sign,t = Reductionops.splay_lam env Evd.empty (EConstr.of_constr c) in let t = EConstr.Unsafe.to_constr t in @@ -302,7 +300,7 @@ let error_not_structure ref = let check_and_decompose_canonical_structure ref = let sp = match ref with ConstRef sp -> sp | _ -> error_not_structure ref in let env = Global.env () in - let u = Univ.AUContext.instance (Environ.constant_context env sp) in + let u = Univ.make_abstract_instance (Environ.constant_context env sp) in let vc = match Environ.constant_opt_value_in env (sp, u) with | Some vc -> vc | None -> error_not_structure ref in diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli index 27d1650af0..de09edcdcb 100644 --- a/pretyping/recordops.mli +++ b/pretyping/recordops.mli @@ -57,7 +57,7 @@ type cs_pattern = type obj_typ = { o_DEF : constr; - o_CTX : Univ.ContextSet.t; + o_CTX : Univ.AUContext.t; o_INJ : int option; (** position of trivial argument *) o_TABS : constr list; (** ordered *) o_TPARAMS : constr list; (** ordered *) -- cgit v1.2.3 From 8f13a227f8d73b78128d9a3bb060cf03d382b708 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 11 Jul 2017 17:49:41 +0200 Subject: Getting rid of AUContext abstraction breakers in Search. --- vernac/search.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/vernac/search.ml b/vernac/search.ml index 788a2aa4a9..5cf6a94912 100644 --- a/vernac/search.ml +++ b/vernac/search.ml @@ -85,7 +85,7 @@ let iter_declarations (fn : global_reference -> env -> constr -> unit) = let mib = Global.lookup_mind mind in let iter_packet i mip = let ind = (mind, i) in - let u = Univ.AUContext.instance (Declareops.inductive_polymorphic_context mib) in + let u = Univ.make_abstract_instance (Declareops.inductive_polymorphic_context mib) in let i = (ind, u) in let typ = Inductiveops.type_of_inductive env i in let () = fn (IndRef ind) env typ in -- cgit v1.2.3 From 8b3978baa5ceb41aaec4d9864c878847b82682d7 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 11 Jul 2017 17:54:52 +0200 Subject: Getting rid of AUContext abstraction breakers in Record. --- vernac/record.ml | 21 ++++++++++----------- 1 file changed, 10 insertions(+), 11 deletions(-) diff --git a/vernac/record.ml b/vernac/record.ml index 366f504545..b179616487 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -265,16 +265,10 @@ let warn_non_primitive_record = let declare_projections indsp ?(kind=StructureComponent) binder_name coers fieldimpls fields = let env = Global.env() in let (mib,mip) = Global.lookup_inductive indsp in - let u = Univ.AUContext.instance (Declareops.inductive_polymorphic_context mib) in - let paramdecls = Inductive.inductive_paramdecls (mib, u) in let poly = Declareops.inductive_is_polymorphic mib in - let ctx = - match mib.mind_universes with - | Monomorphic_ind ctx -> ctx - | Polymorphic_ind auctx -> Univ.instantiate_univ_context auctx - | Cumulative_ind cumi -> - Univ.instantiate_univ_context (Univ.ACumulativityInfo.univ_context cumi) - 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 let r = mkIndU (indsp,u) in let rp = applist (r, Context.Rel.to_extended_list mkRel 0 paramdecls) in @@ -334,8 +328,7 @@ let declare_projections indsp ?(kind=StructureComponent) binder_name coers field const_entry_secctx = None; const_entry_type = Some projtyp; const_entry_polymorphic = poly; - const_entry_universes = - if poly then ctx else Univ.UContext.empty; + const_entry_universes = ctx; const_entry_opaque = false; const_entry_inline_code = false; const_entry_feedback = None } in @@ -431,6 +424,12 @@ let declare_structure finite univs id idbuild paramimpls params arity template let kn = Command.declare_mutual_inductive_with_eliminations mie [] [(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 fieldimpls fields in let build = ConstructRef cstr in let () = if is_coe then Class.try_add_new_coercion build ~local:false poly in -- cgit v1.2.3 From 001c95411b6674423886a085d8f624ea031a9ebc Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 11 Jul 2017 19:29:26 +0200 Subject: Safer API for Global.type_of_global_in_context. We return the abstract context instead of an arbitrary instantiation. --- library/global.ml | 12 +++++------- library/global.mli | 4 ++-- pretyping/typeclasses.ml | 6 ++++-- vernac/indschemes.ml | 5 ++--- 4 files changed, 13 insertions(+), 14 deletions(-) diff --git a/library/global.ml b/library/global.ml index e90151bffe..cb6334c746 100644 --- a/library/global.ml +++ b/library/global.ml @@ -194,26 +194,24 @@ let type_of_global_unsafe r = let type_of_global_in_context env r = match r with - | VarRef id -> Environ.named_type id env, Univ.UContext.empty + | VarRef id -> Environ.named_type id env, Univ.AUContext.empty | ConstRef c -> let cb = Environ.lookup_constant c env in let univs = Declareops.constant_polymorphic_context cb in - let inst = Univ.AUContext.instance univs in - let univs = Univ.UContext.make (inst, Univ.AUContext.instantiate inst univs) in + let env = Environ.push_context ~strict:false (Univ.AUContext.repr univs) env in Typeops.type_of_constant_type env cb.Declarations.const_type, univs | IndRef ind -> let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in let univs = Declareops.inductive_polymorphic_context mib in - let inst = Univ.AUContext.instance univs in - let univs = Univ.UContext.make (inst, Univ.AUContext.instantiate inst univs) in + let inst = Univ.make_abstract_instance univs in + let env = Environ.push_context ~strict:false (Univ.AUContext.repr univs) env in Inductive.type_of_inductive env (specif, inst), univs | ConstructRef cstr -> let (mib,oib as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in let univs = Declareops.inductive_polymorphic_context mib in - let inst = Univ.AUContext.instance univs in - let univs = Univ.UContext.make (inst, Univ.AUContext.instantiate inst univs) in + let inst = Univ.make_abstract_instance univs in Inductive.type_of_constructor (cstr,inst) specif, univs let universes_of_global env r = diff --git a/library/global.mli b/library/global.mli index 5ddf54b4af..d9190736f4 100644 --- a/library/global.mli +++ b/library/global.mli @@ -123,8 +123,8 @@ val is_template_polymorphic : Globnames.global_reference -> bool val is_type_in_type : Globnames.global_reference -> bool val type_of_global_in_context : Environ.env -> - Globnames.global_reference -> Constr.types Univ.in_universe_context -(** Returns the type of the constant in its global or local universe + Globnames.global_reference -> Constr.types * Univ.AUContext.t +(** Returns the type of the constant in its local universe context. The type should not be used without pushing it's universe context in the environmnent of usage. For non-universe-polymorphic constants, it does not matter. *) diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index bae831b637..6de5bc28ba 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -279,8 +279,10 @@ let build_subclasses ~check env sigma glob { hint_priority = pri } = Nameops.add_suffix _id ("_subinstance_" ^ string_of_int !i)) in let ty, ctx = Global.type_of_global_in_context env glob in + let inst, ctx = Universes.fresh_instance_from ctx None in + let ty = Vars.subst_instance_constr inst ty in let ty = EConstr.of_constr ty in - let sigma = Evd.merge_context_set Evd.univ_rigid sigma (Univ.ContextSet.of_context ctx) in + let sigma = Evd.merge_context_set Evd.univ_rigid sigma ctx in let rec aux pri c ty path = match class_of_constr sigma ty with | None -> [] @@ -317,7 +319,7 @@ let build_subclasses ~check env sigma glob { hint_priority = pri } = hints @ (path', info, body) :: rest in List.fold_left declare_proj [] projs in - let term = Universes.constr_of_global_univ (glob,Univ.UContext.instance ctx) in + let term = Universes.constr_of_global_univ (glob, inst) in (*FIXME subclasses should now get substituted for each particular instance of the polymorphic superclass *) aux pri term ty [glob] diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index 6d93f0e410..3d97a767c8 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -383,9 +383,8 @@ let do_mutual_induction_scheme lnamedepindsort = match inst with | None -> let _, ctx = Global.type_of_global_in_context env0 (IndRef ind) in - let ctxs = Univ.ContextSet.of_context ctx in - let evd = Evd.from_ctx (Evd.evar_universe_context_of ctxs) in - let u = Univ.UContext.instance ctx in + let u, ctx = Universes.fresh_instance_from ctx None in + let evd = Evd.from_ctx (Evd.evar_universe_context_of ctx) in evd, (ind,u), Some u | Some ui -> evd, (ind, ui), inst in -- cgit v1.2.3 From 9938aed874d3e15e5d21689ea841bdc3e6ebb40e Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 11 Jul 2017 21:51:23 +0200 Subject: Safer API for Global.body_of_constant and variants. We aditionally return the abstract universe context inside the option. This is relatively painless as most uses were using the option as a boolean. --- API/API.mli | 4 ++-- library/global.ml | 5 ++--- library/global.mli | 4 ++-- library/heads.ml | 2 +- plugins/funind/functional_principles_proofs.ml | 4 ++-- plugins/funind/functional_principles_types.ml | 2 +- plugins/funind/indfun.ml | 2 +- printing/prettyp.ml | 5 +++-- stm/stm.ml | 3 ++- vernac/assumptions.ml | 4 ++-- vernac/lemmas.ml | 3 ++- 11 files changed, 20 insertions(+), 18 deletions(-) diff --git a/API/API.mli b/API/API.mli index a661b34c5b..48fd3a682f 100644 --- a/API/API.mli +++ b/API/API.mli @@ -2716,8 +2716,8 @@ sig val type_of_global_unsafe : Globnames.global_reference -> Term.types val current_dirpath : unit -> Names.DirPath.t - val body_of_constant_body : Declarations.constant_body -> Term.constr option - val body_of_constant : Names.Constant.t -> Term.constr option + val body_of_constant_body : Declarations.constant_body -> (Term.constr * Univ.AUContext.t) option + val body_of_constant : Names.Constant.t -> (Term.constr * Univ.AUContext.t) option val add_constraints : Univ.Constraint.t -> unit end diff --git a/library/global.ml b/library/global.ml index cb6334c746..3a74f535d9 100644 --- a/library/global.ml +++ b/library/global.ml @@ -126,9 +126,8 @@ let opaque_tables () = Environ.opaque_tables (env ()) let instantiate cb c = let open Declarations in match cb.const_universes with - | Monomorphic_const _ -> c - | Polymorphic_const ctx -> - Vars.subst_instance_constr (Univ.AUContext.instance ctx) c + | Monomorphic_const _ -> c, Univ.AUContext.empty + | Polymorphic_const ctx -> c, ctx let body_of_constant_body cb = let open Declarations in diff --git a/library/global.mli b/library/global.mli index d9190736f4..d6d2f1f851 100644 --- a/library/global.mli +++ b/library/global.mli @@ -89,8 +89,8 @@ val constant_of_delta_kn : kernel_name -> constant val mind_of_delta_kn : kernel_name -> mutual_inductive val opaque_tables : unit -> Opaqueproof.opaquetab -val body_of_constant : constant -> Term.constr option -val body_of_constant_body : Declarations.constant_body -> Term.constr option +val body_of_constant : constant -> (Term.constr * Univ.AUContext.t) option +val body_of_constant_body : Declarations.constant_body -> (Term.constr * Univ.AUContext.t) option (** Global universe name <-> level mapping *) type universe_names = diff --git a/library/heads.ml b/library/heads.ml index a1cb812429..c12fa94791 100644 --- a/library/heads.ml +++ b/library/heads.ml @@ -132,7 +132,7 @@ let compute_head = function in (match body with | None -> RigidHead (RigidParameter cst) - | Some c -> kind_of_head env c) + | Some (c, _) -> kind_of_head env c) | EvalVarRef id -> (match Global.lookup_named id with | LocalDef (_,c,_) when not (Decls.variable_opacity id) -> diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index ba46f78aa8..dc43ea7c46 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -957,7 +957,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num (* observe (str "rec_args_num := " ++ str (string_of_int (rec_args_num + 1) )); *) let f_def = Global.lookup_constant (fst (destConst evd f)) in let eq_lhs = mkApp(f,Array.init (nb_params + nb_args) (fun i -> mkRel(nb_params + nb_args - i))) in - let f_body = Option.get (Global.body_of_constant_body f_def) in + let (f_body, _) = Option.get (Global.body_of_constant_body f_def) in let f_body = EConstr.of_constr f_body in let params,f_body_with_params = decompose_lam_n evd nb_params f_body in let (_,num),(_,_,bodies) = destFix evd f_body_with_params in @@ -1091,7 +1091,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam in let get_body const = match Global.body_of_constant const with - | Some body -> + | Some (body, _) -> Tacred.cbv_norm_flags (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA]) (Global.env ()) diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 8ffd15f9fb..8c9b514e67 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -407,7 +407,7 @@ let get_funs_constant mp dp = function const -> let find_constant_body const = match Global.body_of_constant const with - | Some body -> + | Some (body, _) -> let body = Tacred.cbv_norm_flags (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA]) (Global.env ()) diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 2c5dae1cde..ff7667e991 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -851,7 +851,7 @@ let make_graph (f_ref:global_reference) = in (match Global.body_of_constant_body c_body with | None -> error "Cannot build a graph over an axiom!" - | Some body -> + | Some (body, _) -> let env = Global.env () in let sigma = Evd.from_env env in let extern_body,extern_type = diff --git a/printing/prettyp.ml b/printing/prettyp.ml index ff12737f66..d1e51c9f3c 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -557,9 +557,10 @@ let print_constant with_values sep sp = print_basename sp ++ print_instance sigma cb ++ str " : " ++ cut () ++ pr_ltype typ ++ str" ]" ++ Printer.pr_universe_ctx sigma univs - | _ -> + | Some (c, ctx) -> + let c = Vars.subst_instance_constr (Univ.AUContext.instance ctx) c in print_basename sp ++ print_instance sigma cb ++ str sep ++ cut () ++ - (if with_values then print_typed_body env sigma (val_0,typ) else pr_ltype typ)++ + (if with_values then print_typed_body env sigma (Some c,typ) else pr_ltype typ)++ Printer.pr_universe_ctx sigma univs) let gallina_print_constant_with_infos sp = diff --git a/stm/stm.ml b/stm/stm.ml index fd3d418c10..d38491fec2 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1576,8 +1576,9 @@ end = struct (* {{{ *) let uc = Option.get (Opaqueproof.get_constraints (Global.opaque_tables ()) o) in + let map (c, ctx) = Vars.subst_instance_constr (Univ.AUContext.instance ctx) c in let pr = - Future.from_val (Option.get (Global.body_of_constant_body c)) in + Future.from_val (map (Option.get (Global.body_of_constant_body c))) in let uc = Future.chain ~pure:true uc Univ.hcons_universe_context_set in diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml index db07bbd068..86bbf46a35 100644 --- a/vernac/assumptions.ml +++ b/vernac/assumptions.ml @@ -187,7 +187,7 @@ let rec traverse current ctx accu t = match kind_of_term t with let body () = id |> Global.lookup_named |> NamedDecl.get_value in traverse_object accu body (VarRef id) | Const (kn, _) -> - let body () = Global.body_of_constant_body (lookup_constant kn) in + let body () = Option.map fst (Global.body_of_constant_body (lookup_constant kn)) in traverse_object accu body (ConstRef kn) | Ind ((mind, _) as ind, _) -> traverse_inductive accu mind (IndRef ind) @@ -200,7 +200,7 @@ let rec traverse current ctx accu t = match kind_of_term t with | Lambda(_,_,oty), Const (kn, _) when Vars.noccurn 1 oty && not (Declareops.constant_has_body (lookup_constant kn)) -> - let body () = Global.body_of_constant_body (lookup_constant kn) in + let body () = Option.map fst (Global.body_of_constant_body (lookup_constant kn)) in traverse_object ~inhabits:(current,ctx,Vars.subst1 mkProp oty) accu body (ConstRef kn) | _ -> diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 2eeaf4d5dc..cfd489ddef 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -49,7 +49,8 @@ let retrieve_first_recthm = function (NamedDecl.get_value (Global.lookup_named id),variable_opacity id) | ConstRef cst -> let cb = Global.lookup_constant cst in - (Global.body_of_constant_body cb, is_opaque cb) + let map (c, ctx) = Vars.subst_instance_constr (Univ.AUContext.instance ctx) c in + (Option.map map (Global.body_of_constant_body cb), is_opaque cb) | _ -> assert false let adjust_guardness_conditions const = function -- cgit v1.2.3 From 8930c48b4c81837ad9ded8ff8747c9a7ff8bed59 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 11 Jul 2017 22:49:32 +0200 Subject: Make the typeclass implementation fully compatible with universe polymorphism. This essentially means storing the abstract universe context in the typeclass data, and abstracting it when necessary. --- API/API.mli | 1 + pretyping/typeclasses.ml | 65 ++++++++++++++++++++++++++--------------------- pretyping/typeclasses.mli | 6 ++++- vernac/classes.ml | 2 +- vernac/record.ml | 30 +++++++++++++++------- 5 files changed, 64 insertions(+), 40 deletions(-) diff --git a/API/API.mli b/API/API.mli index 48fd3a682f..0f3394fe9f 100644 --- a/API/API.mli +++ b/API/API.mli @@ -3048,6 +3048,7 @@ end module Typeclasses : sig type typeclass = Typeclasses.typeclass = { + cl_univs : Univ.AUContext.t; cl_impl : Globnames.global_reference; cl_context : (Globnames.global_reference * bool) option list * Context.Rel.t; cl_props : Context.Rel.t; diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 6de5bc28ba..5af36fc6b0 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -57,6 +57,9 @@ type direction = Forward | Backward (* This module defines type-classes *) type typeclass = { + (* Universe quantification *) + cl_univs : Univ.AUContext.t; + (* The class implementation *) cl_impl : global_reference; @@ -111,23 +114,11 @@ let new_instance cl info glob poly impl = let classes : typeclasses ref = Summary.ref Refmap.empty ~name:"classes" let instances : instances ref = Summary.ref Refmap.empty ~name:"instances" -let typeclass_univ_instance (cl,u') = - let subst = - let u = - match cl.cl_impl with - | ConstRef c -> - let cb = Global.lookup_constant c in - Univ.AUContext.instance (Declareops.constant_polymorphic_context cb) - | IndRef c -> - let mib,oib = Global.lookup_inductive c in - Univ.AUContext.instance (Declareops.inductive_polymorphic_context mib) - | _ -> Univ.Instance.empty - in Array.fold_left2 (fun subst u u' -> Univ.LMap.add u u' subst) - Univ.LMap.empty (Univ.Instance.to_array u) (Univ.Instance.to_array u') - in - let subst_ctx = Context.Rel.map (subst_univs_level_constr subst) in - { cl with cl_context = fst cl.cl_context, subst_ctx (snd cl.cl_context); - cl_props = subst_ctx cl.cl_props}, u' +let typeclass_univ_instance (cl, u) = + assert (Univ.AUContext.size cl.cl_univs == Univ.Instance.length u); + let subst_ctx c = Context.Rel.map (subst_instance_constr u) c in + { cl with cl_context = on_snd subst_ctx cl.cl_context; + cl_props = subst_ctx cl.cl_props} let class_info c = try Refmap.find c !classes @@ -185,13 +176,28 @@ let subst_class (subst,cl) = do_subst_ctx ctx in let do_subst_projs projs = List.smartmap (fun (x, y, z) -> (x, y, Option.smartmap do_subst_con z)) projs in - { cl_impl = do_subst_gr cl.cl_impl; + { cl_univs = cl.cl_univs; + cl_impl = do_subst_gr cl.cl_impl; cl_context = do_subst_context cl.cl_context; cl_props = do_subst_ctx cl.cl_props; cl_projs = do_subst_projs cl.cl_projs; cl_strict = cl.cl_strict; cl_unique = cl.cl_unique } +(** FIXME: share this with Cooking somewhere in a nicely packed API *) +let lift_abstract_context subst abs_ctx auctx = + let open Univ in + let len = LMap.cardinal subst in + let rec gen_subst i acc = + if i < 0 then acc + else + let acc = LMap.add (Level.var i) (Level.var (i + len)) acc in + gen_subst (pred i) acc + in + let subst = gen_subst (AUContext.size auctx - 1) subst in + let auctx = Univ.subst_univs_level_abstract_universe_context subst auctx in + subst, AUContext.union abs_ctx auctx + let discharge_class (_,cl) = let repl = Lib.replacement_context () in let rel_of_variable_context ctx = List.fold_right @@ -199,15 +205,14 @@ let discharge_class (_,cl) = let decl' = decl |> NamedDecl.map_constr (substn_vars 1 subst) |> NamedDecl.to_rel_decl in (decl' :: ctx', NamedDecl.get_id decl :: subst) ) ctx ([], []) in - let discharge_rel_context subst n rel = + let discharge_rel_context (subst, usubst) n rel = let rel = Context.Rel.map (Cooking.expmod_constr repl) rel in - let ctx, _ = - List.fold_right - (fun decl (ctx, k) -> - RelDecl.map_constr (substn_vars k subst) decl :: ctx, succ k - ) - rel ([], n) - in ctx + let fold decl (ctx, k) = + let map c = subst_univs_level_constr usubst (substn_vars k subst c) in + RelDecl.map_constr map decl :: ctx, succ k + in + let ctx, _ = List.fold_right fold rel ([], n) in + ctx in let abs_context cl = match cl.cl_impl with @@ -229,10 +234,12 @@ let discharge_class (_,cl) = if cl_impl' == cl.cl_impl then cl else let ctx, usubst, uctx = abs_context cl in let ctx, subst = rel_of_variable_context ctx in - let context = discharge_context ctx subst cl.cl_context in - let props = discharge_rel_context subst (succ (List.length (fst cl.cl_context))) cl.cl_props in + let usubst, cl_univs' = lift_abstract_context usubst uctx cl.cl_univs in + let context = discharge_context ctx (subst, usubst) cl.cl_context in + let props = discharge_rel_context (subst, usubst) (succ (List.length (fst cl.cl_context))) cl.cl_props in let discharge_proj (x, y, z) = x, y, Option.smartmap Lib.discharge_con z in - { cl_impl = cl_impl'; + { cl_univs = cl_univs'; + cl_impl = cl_impl'; cl_context = context; cl_props = props; cl_projs = List.smartmap discharge_proj cl.cl_projs; diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index a8e90ca17d..99cdbd3a36 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -16,6 +16,10 @@ type direction = Forward | Backward (** This module defines type-classes *) type typeclass = { + (** The toplevel universe quantification in which the typeclass lives. In + particular, [cl_props] and [cl_context] are quantified over it. *) + cl_univs : Univ.AUContext.t; + (** The class implementation: a record parameterized by the context with defs in it or a definition if the class is a singleton. This acts as the class' global identifier. *) cl_impl : global_reference; @@ -64,7 +68,7 @@ val class_info : global_reference -> typeclass (** raises a UserError if not a c val dest_class_app : env -> evar_map -> EConstr.constr -> (typeclass * EConstr.EInstance.t) * constr list (** Get the instantiated typeclass structure for a given universe instance. *) -val typeclass_univ_instance : typeclass puniverses -> typeclass puniverses +val typeclass_univ_instance : typeclass puniverses -> typeclass (** Just return None if not a class *) val class_of_constr : evar_map -> EConstr.constr -> (EConstr.rel_context * ((typeclass * EConstr.EInstance.t) * constr list)) option diff --git a/vernac/classes.ml b/vernac/classes.ml index a528b96407..d6d4b164b3 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -164,7 +164,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p let ctx'' = ctx' @ ctx in let (k, u), args = Typeclasses.dest_class_app (push_rel_context ctx'' env) !evars (EConstr.of_constr c) in let u = EConstr.EInstance.kind !evars u in - let cl, u = Typeclasses.typeclass_univ_instance (k, u) in + let cl = Typeclasses.typeclass_univ_instance (k, u) in let _, args = List.fold_right (fun decl (args, args') -> match decl with diff --git a/vernac/record.ml b/vernac/record.ml index b179616487..63ca227862 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -517,8 +517,18 @@ let declare_class finite def cum poly ctx id idbuild paramimpls params arity | None -> None) params, params in + let univs, ctx_context, fields = + if poly then + let usubst, auctx = Univ.abstract_universes ctx 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 + in let k = - { cl_impl = impl; + { cl_univs = univs; + cl_impl = impl; cl_strict = !typeclasses_strict; cl_unique = !typeclasses_unique; cl_context = ctx_context; @@ -529,10 +539,11 @@ let declare_class finite def cum poly ctx id idbuild paramimpls params arity let add_constant_class cst = - let ty = Universes.unsafe_type_of_global (ConstRef cst) in + let ty, univs = Global.type_of_global_in_context (Global.env ()) (ConstRef cst) in let ctx, arity = decompose_prod_assum ty in let tc = - { cl_impl = ConstRef cst; + { cl_univs = univs; + cl_impl = ConstRef cst; cl_context = (List.map (const None) ctx, ctx); cl_props = [LocalAssum (Anonymous, arity)]; cl_projs = []; @@ -546,12 +557,13 @@ let add_inductive_class ind = let mind, oneind = Global.lookup_inductive ind in let k = let ctx = oneind.mind_arity_ctxt in - let inst = Univ.AUContext.instance (Declareops.inductive_polymorphic_context mind) in - let ty = Inductive.type_of_inductive - (push_rel_context ctx (Global.env ())) - ((mind,oneind),inst) - in - { cl_impl = IndRef ind; + let univs = Declareops.inductive_polymorphic_context mind in + let env = push_context ~strict:false (Univ.AUContext.repr univs) (Global.env ()) in + let env = push_rel_context ctx env in + let inst = Univ.make_abstract_instance univs in + let ty = Inductive.type_of_inductive env ((mind, oneind), inst) in + { cl_univs = univs; + cl_impl = IndRef ind; cl_context = List.map (const None) ctx, ctx; cl_props = [LocalAssum (Anonymous, ty)]; cl_projs = []; -- cgit v1.2.3 From fb49af8874d01871ea7ca0bd2a46d135dba27bc2 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 11 Jul 2017 18:30:44 +0200 Subject: Getting rid of AUContext abstraction breakers in Discharge. --- library/declare.ml | 4 ++-- library/lib.ml | 13 +++++++++++++ library/lib.mli | 2 ++ pretyping/typeclasses.ml | 18 ++---------------- vernac/discharge.ml | 34 ++++++++++++++-------------------- vernac/discharge.mli | 3 +-- 6 files changed, 34 insertions(+), 40 deletions(-) diff --git a/library/declare.ml b/library/declare.ml index 28f108a151..154793a32d 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -333,9 +333,9 @@ let discharge_inductive ((sp,kn),(dhyps,mie)) = let mind = Global.mind_of_delta_kn kn in let mie = Global.lookup_mind mind in let repl = replacement_context () in - let sechyps,usubst,uctx = section_segment_of_mutual_inductive mind in + let sechyps, _, _ as info = section_segment_of_mutual_inductive mind in Some (discharged_hyps kn sechyps, - Discharge.process_inductive (named_of_variable_context sechyps,uctx) repl mie) + Discharge.process_inductive info repl mie) let dummy_one_inductive_entry mie = { mind_entry_typename = mie.mind_entry_typename; diff --git a/library/lib.ml b/library/lib.ml index 439f83578d..a24d20c681 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -645,3 +645,16 @@ let discharge_con cst = let discharge_inductive (kn,i) = (discharge_kn kn,i) + +let discharge_abstract_universe_context (_, subst, abs_ctx) auctx = + let open Univ in + let len = LMap.cardinal subst in + let rec gen_subst i acc = + if i < 0 then acc + else + let acc = LMap.add (Level.var i) (Level.var (i + len)) acc in + gen_subst (pred i) acc + in + let subst = gen_subst (AUContext.size auctx - 1) subst in + let auctx = Univ.subst_univs_level_abstract_universe_context subst auctx in + subst, AUContext.union abs_ctx auctx diff --git a/library/lib.mli b/library/lib.mli index 38a29f76e3..f1c9bfca24 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -183,3 +183,5 @@ val discharge_kn : Names.mutual_inductive -> Names.mutual_inductive val discharge_con : Names.constant -> Names.constant val discharge_global : Globnames.global_reference -> Globnames.global_reference val discharge_inductive : Names.inductive -> Names.inductive +val discharge_abstract_universe_context : + abstr_info -> Univ.AUContext.t -> Univ.universe_level_subst * Univ.AUContext.t diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 5af36fc6b0..c4418b5a67 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -184,20 +184,6 @@ let subst_class (subst,cl) = cl_strict = cl.cl_strict; cl_unique = cl.cl_unique } -(** FIXME: share this with Cooking somewhere in a nicely packed API *) -let lift_abstract_context subst abs_ctx auctx = - let open Univ in - let len = LMap.cardinal subst in - let rec gen_subst i acc = - if i < 0 then acc - else - let acc = LMap.add (Level.var i) (Level.var (i + len)) acc in - gen_subst (pred i) acc - in - let subst = gen_subst (AUContext.size auctx - 1) subst in - let auctx = Univ.subst_univs_level_abstract_universe_context subst auctx in - subst, AUContext.union abs_ctx auctx - let discharge_class (_,cl) = let repl = Lib.replacement_context () in let rel_of_variable_context ctx = List.fold_right @@ -232,9 +218,9 @@ let discharge_class (_,cl) = in grs', discharge_rel_context subst 1 ctx @ ctx' in let cl_impl' = Lib.discharge_global cl.cl_impl in if cl_impl' == cl.cl_impl then cl else - let ctx, usubst, uctx = abs_context cl in + let ctx, _, _ as info = abs_context cl in let ctx, subst = rel_of_variable_context ctx in - let usubst, cl_univs' = lift_abstract_context usubst uctx cl.cl_univs in + let usubst, cl_univs' = Lib.discharge_abstract_universe_context info cl.cl_univs in let context = discharge_context ctx (subst, usubst) cl.cl_context in let props = discharge_rel_context (subst, usubst) (succ (List.length (fst cl.cl_context))) cl.cl_props in let discharge_proj (x, y, z) = x, y, Option.smartmap Lib.discharge_con z in diff --git a/vernac/discharge.ml b/vernac/discharge.ml index b6308aba00..474c0b4dd2 100644 --- a/vernac/discharge.ml +++ b/vernac/discharge.ml @@ -77,42 +77,36 @@ let refresh_polymorphic_type_of_inductive (_,mip) = let ctx = List.rev mip.mind_arity_ctxt in mkArity (List.rev ctx, Type ar.template_level), true -let process_inductive (sechyps,abs_ctx) modlist mib = +let process_inductive (sechyps,_,_ as info) modlist mib = + let sechyps = Lib.named_of_variable_context sechyps in let nparams = mib.mind_nparams in - let subst, univs = + let subst, ind_univs = match mib.mind_universes with - | Monomorphic_ind ctx -> Univ.Instance.empty, ctx + | Monomorphic_ind ctx -> Univ.empty_level_subst, Monomorphic_ind_entry ctx | Polymorphic_ind auctx -> - Univ.AUContext.instance auctx, Univ.instantiate_univ_context auctx + let subst, auctx = Lib.discharge_abstract_universe_context info auctx in + let auctx = Univ.AUContext.repr auctx in + subst, Polymorphic_ind_entry auctx | Cumulative_ind cumi -> let auctx = Univ.ACumulativityInfo.univ_context cumi in - Univ.AUContext.instance auctx, Univ.instantiate_univ_context auctx + let subst, auctx = Lib.discharge_abstract_universe_context info auctx in + let auctx = Univ.AUContext.repr auctx in + subst, Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context auctx) in + let discharge c = Vars.subst_univs_level_constr subst (expmod_constr modlist c) in let inds = Array.map_to_list (fun mip -> let ty, template = refresh_polymorphic_type_of_inductive (mib,mip) in - let arity = expmod_constr modlist ty in - let arity = Vars.subst_instance_constr subst arity in - let lc = Array.map - (fun c -> Vars.subst_instance_constr subst (expmod_constr modlist c)) - mip.mind_user_lc - in + let arity = discharge ty in + let lc = Array.map discharge mip.mind_user_lc in (mip.mind_typename, arity, template, Array.to_list mip.mind_consnames, Array.to_list lc)) mib.mind_packets in - let sechyps' = Context.Named.map (expmod_constr modlist) sechyps in + let sechyps' = Context.Named.map discharge sechyps in let (params',inds') = abstract_inductive sechyps' nparams inds in - let abs_ctx = Univ.instantiate_univ_context abs_ctx in - let univs = Univ.UContext.union abs_ctx univs in - let ind_univs = - match mib.mind_universes with - | Monomorphic_ind _ -> Monomorphic_ind_entry univs - | Polymorphic_ind _ -> Polymorphic_ind_entry univs - | Cumulative_ind _ -> - Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context univs) in let record = match mib.mind_record with | Some (Some (id, _, _)) -> Some (Some id) | Some None -> Some None diff --git a/vernac/discharge.mli b/vernac/discharge.mli index a0dabe2f46..c8c7e3b8b8 100644 --- a/vernac/discharge.mli +++ b/vernac/discharge.mli @@ -11,5 +11,4 @@ open Entries open Opaqueproof val process_inductive : - ((Term.constr, Term.constr) Context.Named.pt * Univ.abstract_universe_context) - -> work_list -> mutual_inductive_body -> mutual_inductive_entry + Lib.abstr_info -> work_list -> mutual_inductive_body -> mutual_inductive_entry -- cgit v1.2.3 From 1014de55656c2698500089d940a12f7e4b26a0de Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 12 Jul 2017 14:32:55 +0200 Subject: Getting rid of AUContext abstraction breakers in Elimschemes. --- tactics/elimschemes.ml | 21 ++++----------------- 1 file changed, 4 insertions(+), 17 deletions(-) diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml index e058806a35..2d2a0c1b2a 100644 --- a/tactics/elimschemes.ml +++ b/tactics/elimschemes.ml @@ -46,28 +46,15 @@ let optimize_non_type_induction_scheme kind dep sort _ ind = let sigma, nf = Evarutil.nf_evars_and_universes sigma in (nf c', Evd.evar_universe_context sigma), eff else - let mib,mip = Inductive.lookup_mind_specif env ind in - let ctx = Declareops.inductive_polymorphic_context mib in - let u = Univ.AUContext.instance ctx in - let ctx = Univ.UContext.make (u, Univ.AUContext.instantiate u ctx) in - let ctxset = Univ.ContextSet.of_context ctx in - let ectx = Evd.evar_universe_context_of ctxset in - let sigma = Evd.merge_universe_context sigma ectx in - let sigma, c = build_induction_scheme env sigma (ind,u) dep sort in + let sigma, pind = Evd.fresh_inductive_instance env sigma ind in + let sigma, c = build_induction_scheme env sigma pind dep sort in (c, Evd.evar_universe_context sigma), Safe_typing.empty_private_constants let build_induction_scheme_in_type dep sort ind = let env = Global.env () in let sigma = Evd.from_env env in - let ctx = - let mib,mip = Inductive.lookup_mind_specif env ind in - Declareops.inductive_polymorphic_context mib - in - let u = Univ.AUContext.instance ctx in - let ctx = Univ.UContext.make (u, Univ.AUContext.instantiate u ctx) in - let ctxset = Univ.ContextSet.of_context ctx in - let sigma = Evd.merge_universe_context sigma (Evd.evar_universe_context_of ctxset) in - let sigma, c = build_induction_scheme env sigma (ind,u) dep sort in + let sigma, pind = Evd.fresh_inductive_instance env sigma ind in + let sigma, c = build_induction_scheme env sigma pind dep sort in c, Evd.evar_universe_context sigma let rect_scheme_kind_from_type = -- cgit v1.2.3 From 71563ebb86a83bc7cdfc17f58493f59428d764b0 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 12 Jul 2017 14:49:26 +0200 Subject: Safer API for constr_of_global, and getting rid of unsafe_constr_of_global. --- API/API.mli | 4 +- engine/termops.ml | 2 +- engine/universes.ml | 66 --------------------------- engine/universes.mli | 11 ----- library/global.ml | 19 ++++++++ library/global.mli | 7 +++ plugins/funind/functional_principles_types.ml | 2 +- plugins/funind/recdef.ml | 2 +- plugins/ssr/ssrvernac.ml4 | 3 +- pretyping/classops.ml | 2 +- pretyping/pretyping.ml | 4 +- printing/prettyp.ml | 6 ++- tactics/tactics.ml | 4 +- 13 files changed, 43 insertions(+), 89 deletions(-) diff --git a/API/API.mli b/API/API.mli index 0f3394fe9f..f8fb96aa96 100644 --- a/API/API.mli +++ b/API/API.mli @@ -2684,10 +2684,8 @@ sig val fresh_inductive_instance : Environ.env -> Names.inductive -> Term.pinductive Univ.in_universe_context_set val new_Type : Names.DirPath.t -> Term.types val type_of_global : Globnames.global_reference -> Term.types Univ.in_universe_context_set - val unsafe_type_of_global : Globnames.global_reference -> Term.types val constr_of_global : Prelude.global_reference -> Term.constr val new_univ_level : Names.DirPath.t -> Univ.Level.t - val unsafe_constr_of_global : Globnames.global_reference -> Term.constr Univ.in_universe_context val new_sort_in_family : Sorts.family -> Sorts.t val pr_with_global_universes : Univ.Level.t -> Pp.std_ppcmds val pr_universe_opt_subst : universe_opt_subst -> Pp.std_ppcmds @@ -2713,6 +2711,8 @@ sig val env_of_context : Environ.named_context_val -> Environ.env val is_polymorphic : Globnames.global_reference -> bool + val constr_of_global_in_context : Environ.env -> Globnames.global_reference -> Constr.t * Univ.AUContext.t + val type_of_global_in_context : Environ.env -> Globnames.global_reference -> Constr.t * Univ.AUContext.t val type_of_global_unsafe : Globnames.global_reference -> Term.types val current_dirpath : unit -> Names.DirPath.t diff --git a/engine/termops.ml b/engine/termops.ml index fc3291df15..1aba2bbdd1 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -906,7 +906,7 @@ let collect_vars sigma c = aux Id.Set.empty c let vars_of_global_reference env gr = - let c, _ = Universes.unsafe_constr_of_global gr in + let c, _ = Global.constr_of_global_in_context env gr in vars_of_global (Global.env ()) c (* Tests whether [m] is a subterm of [t]: diff --git a/engine/universes.ml b/engine/universes.ml index fc441fd0b4..21854b3faa 100644 --- a/engine/universes.ml +++ b/engine/universes.ml @@ -319,9 +319,6 @@ let fresh_instance_from ctx inst = let constraints = AUContext.instantiate inst ctx in inst, (ctx', constraints) -let unsafe_instance_from ctx = - (Univ.AUContext.instance ctx, Univ.instantiate_univ_context ctx) - (** Fresh universe polymorphic construction *) let fresh_constant_instance env c inst = @@ -358,34 +355,6 @@ let fresh_constructor_instance env (ind,i) inst = let inst, ctx = fresh_instance_from (ACumulativityInfo.univ_context acumi) inst in (((ind,i),inst), ctx) -let unsafe_constant_instance env c = - let cb = lookup_constant c env in - match cb.Declarations.const_universes with - | Declarations.Monomorphic_const _ -> - ((c,Instance.empty), UContext.empty) - | Declarations.Polymorphic_const auctx -> - let inst, ctx = unsafe_instance_from auctx in ((c, inst), ctx) - -let unsafe_inductive_instance env ind = - let mib, mip = Inductive.lookup_mind_specif env ind in - match mib.Declarations.mind_universes with - | Declarations.Monomorphic_ind _ -> ((ind,Instance.empty), UContext.empty) - | Declarations.Polymorphic_ind auctx -> - let inst, ctx = unsafe_instance_from auctx in ((ind,inst), ctx) - | Declarations.Cumulative_ind acumi -> - let inst, ctx = unsafe_instance_from (ACumulativityInfo.univ_context acumi) in - ((ind,inst), ctx) - -let unsafe_constructor_instance env (ind,i) = - let mib, mip = Inductive.lookup_mind_specif env ind in - match mib.Declarations.mind_universes with - | Declarations.Monomorphic_ind _ -> (((ind, i),Instance.empty), UContext.empty) - | Declarations.Polymorphic_ind auctx -> - let inst, ctx = unsafe_instance_from auctx in (((ind, i),inst), ctx) - | Declarations.Cumulative_ind acumi -> - let inst, ctx = unsafe_instance_from (ACumulativityInfo.univ_context acumi) in - (((ind, i),inst), ctx) - open Globnames let fresh_global_instance ?names env gr = @@ -410,19 +379,6 @@ let fresh_inductive_instance env sp = let fresh_constructor_instance env sp = fresh_constructor_instance env sp None -let unsafe_global_instance env gr = - match gr with - | VarRef id -> mkVar id, UContext.empty - | ConstRef sp -> - let c, ctx = unsafe_constant_instance env sp in - mkConstU c, ctx - | ConstructRef sp -> - let c, ctx = unsafe_constructor_instance env sp in - mkConstructU c, ctx - | IndRef sp -> - let c, ctx = unsafe_inductive_instance env sp in - mkIndU c, ctx - let constr_of_global gr = let c, ctx = fresh_global_instance (Global.env ()) gr in if not (Univ.ContextSet.is_empty ctx) then @@ -437,9 +393,6 @@ let constr_of_global gr = let constr_of_reference = constr_of_global -let unsafe_constr_of_global gr = - unsafe_global_instance (Global.env ()) gr - let constr_of_global_univ (gr,u) = match gr with | VarRef id -> mkVar id @@ -513,25 +466,6 @@ let type_of_reference env r = let type_of_global t = type_of_reference (Global.env ()) t -let unsafe_type_of_reference env r = - match r with - | VarRef id -> Environ.named_type id env - | ConstRef c -> - let cb = Environ.lookup_constant c env in - Typeops.type_of_constant_type env cb.const_type - - | IndRef ind -> - let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in - let (_, inst), _ = unsafe_inductive_instance env ind in - Inductive.type_of_inductive env (specif, inst) - - | ConstructRef (ind, _ as cstr) -> - let (mib,oib as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in - let (_, inst), _ = unsafe_inductive_instance env ind in - Inductive.type_of_constructor (cstr,inst) specif - -let unsafe_type_of_global t = unsafe_type_of_reference (Global.env ()) t - let fresh_sort_in_family env = function | InProp -> prop_sort, ContextSet.empty | InSet -> set_sort, ContextSet.empty diff --git a/engine/universes.mli b/engine/universes.mli index 5f4d212b69..8d0f106def 100644 --- a/engine/universes.mli +++ b/engine/universes.mli @@ -189,22 +189,11 @@ val constr_of_global : Globnames.global_reference -> constr (** ** DEPRECATED ** synonym of [constr_of_global] *) val constr_of_reference : Globnames.global_reference -> constr -(** [unsafe_constr_of_global gr] turns [gr] into a constr, works on polymorphic - references by taking the original universe instance that is not recorded - anywhere. The constraints are forgotten as well. DO NOT USE in new code. *) -val unsafe_constr_of_global : Globnames.global_reference -> constr in_universe_context - (** Returns the type of the global reference, by creating a fresh instance of polymorphic references and computing their instantiated universe context. (side-effect on the universe counter, use with care). *) val type_of_global : Globnames.global_reference -> types in_universe_context_set -(** [unsafe_type_of_global gr] returns [gr]'s type, works on polymorphic - references by taking the original universe instance that is not recorded - anywhere. The constraints are forgotten as well. - USE with care. *) -val unsafe_type_of_global : Globnames.global_reference -> types - (** Full universes substitutions into terms *) val nf_evars_and_universes_opt_subst : (existential -> constr option) -> diff --git a/library/global.ml b/library/global.ml index 3a74f535d9..5fff265663 100644 --- a/library/global.ml +++ b/library/global.ml @@ -191,6 +191,25 @@ let type_of_global_unsafe r = let inst = Univ.AUContext.instance (Declareops.inductive_polymorphic_context mib) in Inductive.type_of_constructor (cstr,inst) specif +let constr_of_global_in_context env r = + let open Constr in + match r with + | VarRef id -> mkVar id, Univ.AUContext.empty + | ConstRef c -> + let cb = Environ.lookup_constant c env in + let univs = Declareops.constant_polymorphic_context cb in + mkConstU (c, Univ.make_abstract_instance univs), univs + | IndRef ind -> + let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in + let univs = Declareops.inductive_polymorphic_context mib in + mkIndU (ind, Univ.make_abstract_instance univs), univs + | ConstructRef cstr -> + let (mib,oib as specif) = + Inductive.lookup_mind_specif env (inductive_of_constructor cstr) + in + let univs = Declareops.inductive_polymorphic_context mib in + mkConstructU (cstr, Univ.make_abstract_instance univs), univs + let type_of_global_in_context env r = match r with | VarRef id -> Environ.named_type id env, Univ.AUContext.empty diff --git a/library/global.mli b/library/global.mli index d6d2f1f851..0f1cec44a5 100644 --- a/library/global.mli +++ b/library/global.mli @@ -122,6 +122,13 @@ val is_polymorphic : Globnames.global_reference -> bool val is_template_polymorphic : Globnames.global_reference -> bool val is_type_in_type : Globnames.global_reference -> bool +val constr_of_global_in_context : Environ.env -> + Globnames.global_reference -> Constr.types * Univ.AUContext.t +(** Returns the type of the constant in its local universe + context. The type should not be used without pushing it's universe + context in the environmnent of usage. For non-universe-polymorphic + constants, it does not matter. *) + val type_of_global_in_context : Environ.env -> Globnames.global_reference -> Constr.types * Univ.AUContext.t (** Returns the type of the constant in its local universe diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 8c9b514e67..d726c1a2bb 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -651,7 +651,7 @@ let build_case_scheme fa = (* in *) let funs = let (_,f,_) = fa in - try fst (Universes.unsafe_constr_of_global (Smartlocate.global_with_alias f)) + try fst (Global.constr_of_global_in_context (Global.env ()) (Smartlocate.global_with_alias f)) with Not_found -> user_err ~hdr:"FunInd.build_case_scheme" (str "Cannot find " ++ Libnames.pr_reference f) in diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 1705cac789..bc550c8b9c 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -90,7 +90,7 @@ let type_of_const sigma t = |_ -> assert false let constr_of_global x = - fst (Universes.unsafe_constr_of_global x) + fst (Global.constr_of_global_in_context (Global.env ()) x) let constant sl s = constr_of_global (find_reference sl s) diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4 index 4c8827bf84..cb6a2cd695 100644 --- a/plugins/ssr/ssrvernac.ml4 +++ b/plugins/ssr/ssrvernac.ml4 @@ -337,7 +337,8 @@ let coerce_search_pattern_to_sort hpat = Pattern.PApp (fp, args') in let hr, na = splay_search_pattern 0 hpat in let dc, ht = - Reductionops.splay_prod env sigma (EConstr.of_constr (Universes.unsafe_type_of_global hr)) in + let hr, _ = Global.type_of_global_in_context (Global.env ()) hr (** FIXME *) in + Reductionops.splay_prod env sigma (EConstr.of_constr hr) in let np = List.length dc in if np < na then CErrors.user_err (Pp.str "too many arguments in head search pattern") else let hpat' = if np = na then hpat else mkPApp hpat (np - na) [||] in diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 948aa26cac..078990a8c1 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -403,7 +403,7 @@ type coercion = { (* Computation of the class arity *) let reference_arity_length ref = - let t = Universes.unsafe_type_of_global ref in + let t, _ = Global.type_of_global_in_context (Global.env ()) ref in List.length (fst (Reductionops.splay_arity (Global.env()) Evd.empty (EConstr.of_constr t))) (** FIXME *) let projection_arity_length p = diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index e166e0e9df..bfc6bf5cff 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -511,8 +511,8 @@ let pretype_global ?loc rigid env evd gr us = match us with | None -> evd, None | Some l -> - let _, ctx = Universes.unsafe_constr_of_global gr in - let len = Univ.UContext.size ctx in + let _, ctx = Global.constr_of_global_in_context env.ExtraEnv.env gr in + let len = Univ.AUContext.size ctx in interp_instance ?loc evd ~len l in let (sigma, c) = Evd.fresh_global ?loc ~rigid ?names:instance env.ExtraEnv.env evd gr in diff --git a/printing/prettyp.ml b/printing/prettyp.ml index d1e51c9f3c..a0c88a7af1 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -798,9 +798,11 @@ let print_opaque_name qid = | IndRef (sp,_) -> print_inductive sp | ConstructRef cstr as gr -> - let open EConstr in - let ty = Universes.unsafe_type_of_global gr in + let ty, ctx = Global.type_of_global_in_context env gr in + let inst = Univ.AUContext.instance ctx in + let ty = Vars.subst_instance_constr inst ty in let ty = EConstr.of_constr ty in + let open EConstr in print_typed_value (mkConstruct cstr, ty) | VarRef id -> env |> lookup_named id |> NamedDecl.set_id id |> print_named_decl diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 2e3a4e33b3..177c44bcbb 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -5004,7 +5004,9 @@ let cache_term_by_tactic_then ~opaque ?(goal_type=None) id gk tac tacK = in let cst = Impargs.with_implicit_protection cst () in (* let evd, lem = Evd.fresh_global (Global.env ()) evd (ConstRef cst) in *) - let lem, ctx = Universes.unsafe_constr_of_global (ConstRef cst) in + let lem, ctx = Global.constr_of_global_in_context (Global.env ()) (ConstRef cst) in + let inst = Univ.AUContext.instance ctx in + let lem = CVars.subst_instance_constr inst lem in let lem = EConstr.of_constr lem in let evd = Evd.set_universe_context evd ectx in let open Safe_typing in -- cgit v1.2.3 From 34bcd562cc9c8e5e6b0f3b79a15b9c55dd98813e Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 12 Jul 2017 15:29:10 +0200 Subject: The only abstraction-breaking function in Univ is now AUContext.instance. --- kernel/univ.ml | 8 -------- kernel/univ.mli | 6 ------ printing/prettyp.ml | 7 +++++-- printing/printmod.ml | 15 +++++++++++++-- vernac/himsg.ml | 2 +- 5 files changed, 19 insertions(+), 19 deletions(-) diff --git a/kernel/univ.ml b/kernel/univ.ml index 6614d60276..02b02db893 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -1292,14 +1292,6 @@ let subst_univs_constraints subst csts = (fun c cstrs -> subst_univs_constraint subst c cstrs) csts Constraint.empty -(** Substitute instance inst for ctx in csts *) -let instantiate_univ_context (ctx, csts) = - (ctx, subst_instance_constraints ctx csts) - -(** Substitute instance inst for ctx in universe constraints and subtyping constraints *) -let instantiate_cumulativity_info (univcst, subtpcst) = - (instantiate_univ_context univcst, instantiate_univ_context subtpcst) - let make_instance_subst i = let arr = Instance.to_array i in Array.fold_left_i (fun i acc l -> diff --git a/kernel/univ.mli b/kernel/univ.mli index 53297ac462..99092a543e 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -461,12 +461,6 @@ val abstract_cumulativity_info : cumulativity_info -> universe_level_subst * abs val make_abstract_instance : abstract_universe_context -> universe_instance -(** Don't use. *) -val instantiate_univ_context : abstract_universe_context -> universe_context - -(** Don't use. *) -val instantiate_cumulativity_info : abstract_cumulativity_info -> cumulativity_info - (** {6 Pretty-printing of universes. } *) val pr_constraint_type : constraint_type -> Pp.std_ppcmds diff --git a/printing/prettyp.ml b/printing/prettyp.ml index a0c88a7af1..5cd79ed6df 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -532,7 +532,9 @@ let print_constant with_values sep sp = begin match cb.const_universes with | Monomorphic_const ctx -> ctx - | Polymorphic_const ctx -> Univ.instantiate_univ_context ctx + | Polymorphic_const ctx -> + let inst = Univ.AUContext.instance ctx in + Univ.UContext.make (inst, Univ.AUContext.instantiate inst ctx) end | OpaqueDef o -> let body_uctxs = Opaqueproof.force_constraints otab o in @@ -542,7 +544,8 @@ let print_constant with_values sep sp = Univ.ContextSet.to_context (Univ.ContextSet.union body_uctxs uctxs) | Polymorphic_const ctx -> assert(Univ.ContextSet.is_empty body_uctxs); - Univ.instantiate_univ_context ctx + let inst = Univ.AUContext.instance ctx in + Univ.UContext.make (inst, Univ.AUContext.instantiate inst ctx) in let ctx = Evd.evar_universe_context_of_binders diff --git a/printing/printmod.ml b/printing/printmod.ml index 2e0e6d2845..5c7dcdc10f 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -110,6 +110,17 @@ let print_one_inductive env sigma mib ((_,i) as ind) = str ": " ++ Printer.pr_lconstr_env envpar sigma arity ++ str " :=") ++ brk(0,2) ++ print_constructors envpar sigma mip.mind_consnames cstrtypes +let instantiate_cumulativity_info cumi = + let open Univ in + let univs = ACumulativityInfo.univ_context cumi in + let subtyp = ACumulativityInfo.subtyp_context cumi in + let expose ctx = + let inst = AUContext.instance ctx in + let cst = AUContext.instantiate inst ctx in + UContext.make (inst, cst) + in + CumulativityInfo.make (expose univs, expose subtyp) + let print_mutual_inductive env mind mib = let inds = List.init (Array.length mib.mind_packets) (fun x -> (mind, x)) in @@ -133,7 +144,7 @@ let print_mutual_inductive env mind mib = | Monomorphic_ind _ | Polymorphic_ind _ -> str "" | Cumulative_ind cumi -> Printer.pr_cumulativity_info - sigma (Univ.instantiate_cumulativity_info cumi)) + sigma (instantiate_cumulativity_info cumi)) let get_fields = let rec prodec_rec l subst c = @@ -191,7 +202,7 @@ let print_record env mind mib = | Monomorphic_ind _ | Polymorphic_ind _ -> str "" | Cumulative_ind cumi -> Printer.pr_cumulativity_info - sigma (Univ.instantiate_cumulativity_info cumi) + sigma (instantiate_cumulativity_info cumi) ) let pr_mutual_inductive_body env mind mib = diff --git a/vernac/himsg.ml b/vernac/himsg.ml index 86dcb6d4dc..784c6d3387 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -909,7 +909,7 @@ let explain_not_match_error = function quote (Printer.safe_pr_lconstr_env env Evd.empty t2) | IncompatibleConstraints cst -> str " the expected (polymorphic) constraints do not imply " ++ - let cst = Univ.UContext.constraints (Univ.instantiate_univ_context cst) in + let cst = Univ.AUContext.instantiate (Univ.AUContext.instance cst) cst in quote (Univ.pr_constraints (Termops.pr_evd_level Evd.empty) cst) let explain_signature_mismatch l spec why = -- cgit v1.2.3 From 469a9b3242891b089b4a211e96b5b568277f7fc0 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 12 Jul 2017 15:55:51 +0200 Subject: Remove the function Global.type_of_global_unsafe. --- API/API.mli | 1 - interp/notation.ml | 6 +++--- library/global.ml | 18 ------------------ library/global.mli | 11 ----------- library/impargs.ml | 7 ++++--- plugins/extraction/table.ml | 7 ++++--- plugins/funind/indfun_common.ml | 2 +- pretyping/typeclasses.ml | 2 +- printing/prettyp.ml | 5 +++-- tactics/hints.ml | 2 +- vernac/auto_ind_decl.ml | 2 +- vernac/class.ml | 6 ++++-- vernac/classes.ml | 2 +- vernac/search.ml | 2 +- vernac/vernacentries.ml | 2 +- 15 files changed, 25 insertions(+), 50 deletions(-) diff --git a/API/API.mli b/API/API.mli index f8fb96aa96..e8418552c4 100644 --- a/API/API.mli +++ b/API/API.mli @@ -2713,7 +2713,6 @@ sig val constr_of_global_in_context : Environ.env -> Globnames.global_reference -> Constr.t * Univ.AUContext.t val type_of_global_in_context : Environ.env -> Globnames.global_reference -> Constr.t * Univ.AUContext.t - val type_of_global_unsafe : Globnames.global_reference -> Term.types val current_dirpath : unit -> Names.DirPath.t val body_of_constant_body : Declarations.constant_body -> (Term.constr * Univ.AUContext.t) option diff --git a/interp/notation.ml b/interp/notation.ml index 4067a6b945..c07a009438 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -718,13 +718,13 @@ let rebuild_arguments_scope (req,r,n,l,_) = match req with | ArgsScopeNoDischarge -> assert false | ArgsScopeAuto -> - let scs,cls = compute_arguments_scope_full (fst(Universes.type_of_global r)(*FIXME?*)) in + let scs,cls = compute_arguments_scope_full (fst(Global.type_of_global_in_context (Global.env ()) r)(*FIXME?*)) in (req,r,List.length scs,scs,cls) | ArgsScopeManual -> (* Add to the manually given scopes the one found automatically for the extra parameters of the section. Discard the classes of the manually given scopes to avoid further re-computations. *) - let l',cls = compute_arguments_scope_full (Global.type_of_global_unsafe r) in + let l',cls = compute_arguments_scope_full (fst (Global.type_of_global_in_context (Global.env ()) r)) in let l1 = List.firstn n l' in let cls1 = List.firstn n cls in (req,r,0,l1@l,cls1) @@ -768,7 +768,7 @@ let find_arguments_scope r = with Not_found -> [] let declare_ref_arguments_scope ref = - let t = Global.type_of_global_unsafe ref in + let t, _ = Global.type_of_global_in_context (Global.env ()) ref in let (scs,cls as o) = compute_arguments_scope_full t in declare_arguments_scope_gen ArgsScopeAuto ref (List.length scs) o diff --git a/library/global.ml b/library/global.ml index 5fff265663..5b17855dce 100644 --- a/library/global.ml +++ b/library/global.ml @@ -173,24 +173,6 @@ open Globnames (** Build a fresh instance for a given context, its associated substitution and the instantiated constraints. *) -let type_of_global_unsafe r = - let env = env() in - match r with - | VarRef id -> Environ.named_type id env - | ConstRef c -> - let cb = Environ.lookup_constant c env in - let inst = Univ.AUContext.instance (Declareops.constant_polymorphic_context cb) in - let ty = Typeops.type_of_constant_type env cb.Declarations.const_type in - Vars.subst_instance_constr inst ty - | IndRef ind -> - let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in - let inst = Univ.AUContext.instance (Declareops.inductive_polymorphic_context mib) in - Inductive.type_of_inductive env (specif, inst) - | ConstructRef cstr -> - let (mib,oib as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in - let inst = Univ.AUContext.instance (Declareops.inductive_polymorphic_context mib) in - Inductive.type_of_constructor (cstr,inst) specif - let constr_of_global_in_context env r = let open Constr in match r with diff --git a/library/global.mli b/library/global.mli index 0f1cec44a5..431747c524 100644 --- a/library/global.mli +++ b/library/global.mli @@ -136,17 +136,6 @@ val type_of_global_in_context : Environ.env -> context in the environmnent of usage. For non-universe-polymorphic constants, it does not matter. *) -val type_of_global_unsafe : Globnames.global_reference -> Constr.types -(** Returns the type of the constant, forgetting its universe context if - it is polymorphic, use with care: for polymorphic constants, the - type cannot be used to produce a term used by the kernel. For safe - handling of polymorphic global references, one should look at a - particular instantiation of the reference, in some particular - universe context (part of an [env] or [evar_map]), see - e.g. [type_of_constant_in]. If you want to create a fresh instance - of the reference and get its type look at [Evd.fresh_global] or - [Evarutil.new_global] and [Retyping.get_type_of]. *) - (** Returns the universe context of the global reference (whatever its polymorphic status is). *) val universes_of_global : Globnames.global_reference -> Univ.abstract_universe_context diff --git a/library/impargs.ml b/library/impargs.ml index 351addf2fa..b7125fc85d 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -431,12 +431,13 @@ let compute_mib_implicits flags manual kn = (Array.mapi (* No need to lift, arities contain no de Bruijn *) (fun i mip -> (** No need to care about constraints here *) - Context.Rel.Declaration.LocalAssum (Name mip.mind_typename, Global.type_of_global_unsafe (IndRef (kn,i)))) + let ty, _ = Global.type_of_global_in_context env (IndRef (kn,i)) in + Context.Rel.Declaration.LocalAssum (Name mip.mind_typename, ty)) mib.mind_packets) in let env_ar = push_rel_context ar env in let imps_one_inductive i mip = let ind = (kn,i) in - let ar = Global.type_of_global_unsafe (IndRef ind) in + let ar, _ = Global.type_of_global_in_context env (IndRef ind) in ((IndRef ind,compute_semi_auto_implicits env flags manual ar), Array.mapi (fun j c -> (ConstructRef (ind,j+1),compute_semi_auto_implicits env_ar flags manual c)) @@ -674,7 +675,7 @@ let projection_implicits env p impls = let declare_manual_implicits local ref ?enriching l = let flags = !implicit_args in let env = Global.env () in - let t = Global.type_of_global_unsafe ref in + let t, _ = Global.type_of_global_in_context (Global.env ()) ref in let enriching = Option.default flags.auto enriching in let isrigid,autoimpls = compute_auto_implicits env flags enriching t in let l' = match l with diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 2642aeefa4..dff3548fd8 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -445,9 +445,10 @@ let error_MPfile_as_mod mp b = "Please "^s2^"use (Recursive) Extraction Library instead.\n")) let argnames_of_global r = - let typ = Global.type_of_global_unsafe r in + let env = Global.env () in + let typ, _ = Global.type_of_global_in_context env r in let rels,_ = - decompose_prod (Reduction.whd_all (Global.env ()) typ) in + decompose_prod (Reduction.whd_all env typ) in List.rev_map fst rels let msg_of_implicit = function @@ -878,7 +879,7 @@ let extract_constant_inline inline r ids s = match g with | ConstRef kn -> let env = Global.env () in - let typ = Global.type_of_global_unsafe (ConstRef kn) in + let typ, _ = Global.type_of_global_in_context env (ConstRef kn) in let typ = Reduction.whd_all env typ in if Reduction.is_arity env typ then begin diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 6fe6888f3d..61fbca23f2 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -342,7 +342,7 @@ let pr_info f_info = str "function_constant_type := " ++ (try Printer.pr_lconstr - (Global.type_of_global_unsafe (ConstRef f_info.function_constant)) + (fst (Global.type_of_global_in_context (Global.env ()) (ConstRef f_info.function_constant))) with e when CErrors.noncritical e -> mt ()) ++ fnl () ++ str "equation_lemma := " ++ pr_ocst f_info.equation_lemma ++ fnl () ++ str "completeness_lemma :=" ++ pr_ocst f_info.completeness_lemma ++ fnl () ++ diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index c4418b5a67..d4fa266c02 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -400,7 +400,7 @@ let remove_instance i = remove_instance_hint i.is_impl let declare_instance info local glob = - let ty = Global.type_of_global_unsafe glob in + let ty, _ = Global.type_of_global_in_context (Global.env ()) glob in let info = Option.default {hint_priority = None; hint_pattern = None} info in match class_of_constr Evd.empty (EConstr.of_constr ty) with | Some (rels, ((tc,_), args) as _cl) -> diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 5cd79ed6df..827c0e4583 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -70,7 +70,8 @@ let int_or_no n = if Int.equal n 0 then str "no" else int n let print_basename sp = pr_global (ConstRef sp) let print_ref reduce ref = - let typ = Global.type_of_global_unsafe ref in + let typ, ctx = Global.type_of_global_in_context (Global.env ()) ref in + let typ = Vars.subst_instance_constr (Univ.AUContext.instance ctx) typ in let typ = EConstr.of_constr typ in let typ = if reduce then @@ -137,7 +138,7 @@ let print_renames_list prefix l = hv 2 (prlist_with_sep pr_comma (fun x -> x) (List.map Name.print l))] let need_expansion impl ref = - let typ = Global.type_of_global_unsafe ref in + let typ, _ = Global.type_of_global_in_context (Global.env ()) ref in let ctx = prod_assum typ in let nprods = List.count is_local_assum ctx in not (List.is_empty impl) && List.length impl >= nprods && diff --git a/tactics/hints.ml b/tactics/hints.ml index c2c80e6305..a572508d47 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -937,7 +937,7 @@ let make_extern pri pat tacast = let make_mode ref m = let open Term in - let ty = Global.type_of_global_unsafe ref in + let ty, _ = Global.type_of_global_in_context (Global.env ()) ref in let ctx, t = decompose_prod ty in let n = List.length ctx in let m' = Array.of_list m in diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index 248224e6b7..59920742d8 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -105,7 +105,7 @@ let mkFullInd (ind,u) n = else mkIndU (ind,u) let check_bool_is_defined () = - try let _ = Global.type_of_global_unsafe Coqlib.glob_bool in () + try let _ = Global.type_of_global_in_context (Global.env ()) Coqlib.glob_bool in () with e when CErrors.noncritical e -> raise (UndefinedCst "bool") let beq_scheme_kind_aux = ref (fun _ -> failwith "Undefined") diff --git a/vernac/class.ml b/vernac/class.ml index 0b510bbcf0..be682977e5 100644 --- a/vernac/class.ml +++ b/vernac/class.ml @@ -62,7 +62,9 @@ let explain_coercion_error g = function (* Verifications pour l'ajout d'une classe *) let check_reference_arity ref = - if not (Reductionops.is_arity (Global.env()) Evd.empty (EConstr.of_constr (Global.type_of_global_unsafe ref))) (** FIXME *) then + let env = Global.env () in + let c, _ = Global.type_of_global_in_context env ref in + if not (Reductionops.is_arity env Evd.empty (EConstr.of_constr c)) (** FIXME *) then raise (CoercionError (NotAClass ref)) let check_arity = function @@ -252,7 +254,7 @@ let warn_uniform_inheritance = let add_new_coercion_core coef stre poly source target isid = check_source source; - let t = Global.type_of_global_unsafe coef in + let t, _ = Global.type_of_global_in_context (Global.env ()) coef in if coercion_exists coef then raise (CoercionError AlreadyExists); let tg,lp = prods_of t in let llp = List.length lp in diff --git a/vernac/classes.ml b/vernac/classes.ml index d6d4b164b3..ab1892a18e 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -68,7 +68,7 @@ let _ = let existing_instance glob g info = let c = global g in let info = Option.default Hints.empty_hint_info info in - let instance = Global.type_of_global_unsafe c in + let instance, _ = Global.type_of_global_in_context (Global.env ()) c in let _, r = decompose_prod_assum instance in match class_of_constr Evd.empty (EConstr.of_constr r) with | Some (_, ((tc,u), _)) -> add_instance (new_instance tc info glob diff --git a/vernac/search.ml b/vernac/search.ml index 5cf6a94912..0f56f81e74 100644 --- a/vernac/search.ml +++ b/vernac/search.ml @@ -78,7 +78,7 @@ let iter_declarations (fn : global_reference -> env -> constr -> unit) = | "CONSTANT" -> let cst = Global.constant_of_delta_kn kn in let gr = ConstRef cst in - let typ = Global.type_of_global_unsafe gr in + let (typ, _) = Global.type_of_global_in_context (Global.env ()) gr in fn gr env typ | "INDUCTIVE" -> let mind = Global.mind_of_delta_kn kn in diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index bbec28afff..8a647c6c18 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -986,7 +986,7 @@ let vernac_arguments locality reference args more_implicits nargs_for_red flags let sr = smart_global reference in let inf_names = - let ty = Global.type_of_global_unsafe sr in + let ty, _ = Global.type_of_global_in_context (Global.env ()) sr in Impargs.compute_implicits_names (Global.env ()) ty in let prev_names = -- cgit v1.2.3 From f2a01d400c92c48caf79771f17820a492f99057b Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 12 Jul 2017 16:54:12 +0200 Subject: Removing the uses of abstraction-breaking code in Obligations. --- vernac/obligations.ml | 34 +++++++++++++--------------------- 1 file changed, 13 insertions(+), 21 deletions(-) diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 5a1c260b1f..4b1565d3ce 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -285,7 +285,7 @@ type obligation = { obl_name : Id.t; obl_type : types; obl_location : Evar_kinds.t Loc.located; - obl_body : constant obligation_body option; + obl_body : pconstant obligation_body option; obl_status : bool * Evar_kinds.obligation_definition_status; obl_deps : Int.Set.t; obl_tac : unit Proofview.tactic option; @@ -358,18 +358,8 @@ let _ = let evar_of_obligation o = make_evar (Global.named_context_val ()) o.obl_type -let get_body obl = - match obl.obl_body with - | None -> None - | Some (DefinedObl c) -> - let u = Univ.AUContext.instance (Environ.constant_context (Global.env ()) c) in - let pc = (c, u) in - Some (DefinedObl pc) - | Some (TermObl c) -> - Some (TermObl c) - let get_obligation_body expand obl = - match get_body obl with + match obl.obl_body with | None -> None | Some c -> if expand && snd obl.obl_status == Evar_kinds.Expand then @@ -664,7 +654,7 @@ let declare_obligation prg obl body ty uctx = definition_message obl.obl_name; true, { obl with obl_body = if poly then - Some (DefinedObl constant) + Some (DefinedObl (constant, Univ.UContext.instance uctx)) else Some (TermObl (it_mkLambda_or_LetIn_or_clean (mkApp (mkConst constant, args)) ctx)) } @@ -892,20 +882,22 @@ let obligation_hook prg obl num auto ctx' _ gr = if not transparent then err_not_transp () | _ -> () in - let obl = { obl with obl_body = Some (DefinedObl cst) } in - let () = if transparent then add_hint true prg cst in - let obls = Array.copy obls in - let _ = obls.(num) <- obl in let ctx' = match ctx' with None -> prg.prg_ctx | Some ctx' -> ctx' in - let ctx' = + let inst, ctx' = if not (pi2 prg.prg_kind) (* Not polymorphic *) then (* The universe context was declared globally, we continue from the new global environment. *) let evd = Evd.from_env (Global.env ()) in let ctx' = Evd.merge_universe_subst evd (Evd.universe_subst (Evd.from_ctx ctx')) in - Evd.evar_universe_context ctx' - else ctx' + Univ.Instance.empty, Evd.evar_universe_context ctx' + else + let (_, uctx) = UState.universe_context ctx' in + Univ.UContext.instance uctx, ctx' in + let obl = { obl with obl_body = Some (DefinedObl (cst, inst)) } in + let () = if transparent then add_hint true prg cst in + let obls = Array.copy obls in + let _ = obls.(num) <- obl in let prg = { prg with prg_ctx = ctx' } in let () = try ignore (update_obls prg obls (pred rem)) @@ -1132,7 +1124,7 @@ let admit_prog prg = (ParameterEntry (None,false,(x.obl_type,ctx),None), IsAssumption Conjectural) in assumption_message x.obl_name; - obls.(i) <- { x with obl_body = Some (DefinedObl kn) } + obls.(i) <- { x with obl_body = Some (DefinedObl (kn, Univ.Instance.empty)) } | Some _ -> ()) obls; ignore(update_obls prg obls 0) -- cgit v1.2.3 From a59bdc4144476c0794ff24fc6180e21671842395 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 12 Jul 2017 17:57:22 +0200 Subject: Removing the uses of abstraction-breaking code in Lemmas. I had to slightly tweak a test in order to work around a bug of simpl that loses universes constraints when refolding polymorphic fixpoints. --- test-suite/bugs/closed/HoTT_coq_123.v | 6 +++++- vernac/lemmas.ml | 8 +++++--- 2 files changed, 10 insertions(+), 4 deletions(-) diff --git a/test-suite/bugs/closed/HoTT_coq_123.v b/test-suite/bugs/closed/HoTT_coq_123.v index cd9cad4064..7bed956f3e 100644 --- a/test-suite/bugs/closed/HoTT_coq_123.v +++ b/test-suite/bugs/closed/HoTT_coq_123.v @@ -104,11 +104,15 @@ Record Functor (C D : PreCategory) := morphism_of : forall s d, morphism C s d -> morphism D (object_of s) (object_of d) }. +(** Workaround to simpl losing universe constraints, see bug #5645. *) +Ltac simpl' := + simpl; match goal with [ |- ?P ] => let T := type of P in idtac end. + Global Instance trunc_forall `{Funext} `{P : A -> Type} `{forall a, IsTrunc n (P a)} : IsTrunc n (forall a, P a) | 100. Proof. generalize dependent P. - induction n as [ | n' IH]; (simpl; intros P ?). + induction n as [ | n' IH]; (simpl'; intros P ?). - admit. - pose (fun f g => trunc_equiv (@apD10 A P f g) ^-1); admit. Defined. diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index cfd489ddef..645320c603 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -44,12 +44,14 @@ let call_hook fix_exn hook l c = (* Support for mutually proved theorems *) -let retrieve_first_recthm = function +let retrieve_first_recthm uctx = function | VarRef id -> (NamedDecl.get_value (Global.lookup_named id),variable_opacity id) | ConstRef cst -> let cb = Global.lookup_constant cst in - let map (c, ctx) = Vars.subst_instance_constr (Univ.AUContext.instance ctx) c in + let (_, uctx) = UState.universe_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) | _ -> assert false @@ -413,7 +415,7 @@ let start_proof_with_initialization kind ctx recguard thms snl hook = let other_thms_data = if List.is_empty other_thms then [] else (* there are several theorems defined mutually *) - let body,opaq = retrieve_first_recthm ref in + 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.context_set (*FIXME*) ctx in -- cgit v1.2.3 From 0411c7e08b58edc4785c2be396fad0a037056a11 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 13 Jul 2017 18:26:44 +0200 Subject: Removing a use of AUContext.instance in the STM. We only delay monomorphic proofs in quick mode, so that their universe context will always be empty. --- stm/stm.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/stm/stm.ml b/stm/stm.ml index d38491fec2..7c96208546 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1576,7 +1576,8 @@ end = struct (* {{{ *) let uc = Option.get (Opaqueproof.get_constraints (Global.opaque_tables ()) o) in - let map (c, ctx) = Vars.subst_instance_constr (Univ.AUContext.instance ctx) c in + (** We only manipulate monomorphic terms here. *) + let map (c, ctx) = assert (Univ.AUContext.is_empty ctx); c in let pr = Future.from_val (map (Option.get (Global.body_of_constant_body c))) in let uc = -- cgit v1.2.3 From 6806059f7c043b45e6c42f382f069f8c49ed1c1f Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 13 Jul 2017 00:50:02 +0200 Subject: Getting rid of abstraction breaking code in tclABSTRACT. This is probably the hardest case of them all, because tclABSTRACT fundamentally relies on the names of universes from the constant instance being the same as the one in the current goal. Adding to that the fact that the kernel is doing strange things when provided with a polymorphic definition with body universe constraints, it turns out to be a hellish nightmare to handle properly. At some point we need to clarifiy this in the kernel as well, although we leave it for some other patch. --- tactics/tactics.ml | 18 +++++++++++++----- test-suite/success/abstract_poly.v | 20 ++++++++++++++++++++ 2 files changed, 33 insertions(+), 5 deletions(-) create mode 100644 test-suite/success/abstract_poly.v diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 177c44bcbb..c979b8b040 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -5003,11 +5003,19 @@ let cache_term_by_tactic_then ~opaque ?(goal_type=None) id gk tac tacK = Declare.declare_constant ~internal:Declare.InternalTacticRequest ~local:true id decl in let cst = Impargs.with_implicit_protection cst () in - (* let evd, lem = Evd.fresh_global (Global.env ()) evd (ConstRef cst) in *) - let lem, ctx = Global.constr_of_global_in_context (Global.env ()) (ConstRef cst) in - let inst = Univ.AUContext.instance ctx in - let lem = CVars.subst_instance_constr inst lem in - let lem = EConstr.of_constr lem in + let lem = + if const.Entries.const_entry_polymorphic then + let uctx = Univ.ContextSet.of_context const.Entries.const_entry_universes in + (** Hack: the kernel may generate definitions whose universe variables are + not the same as requested in the entry because of constraints delayed + in the body, even in polymorphic mode. We mimick what it does for now + in hope it is fixed at some point. *) + let (_, body_uctx), _ = Future.force const.Entries.const_entry_body in + let uctx = Univ.ContextSet.to_context (Univ.ContextSet.union uctx body_uctx) in + let u = Univ.UContext.instance uctx in + mkConstU (cst, EInstance.make u) + else mkConst cst + in let evd = Evd.set_universe_context evd ectx in let open Safe_typing in let eff = private_con_of_con (Global.safe_env ()) cst in diff --git a/test-suite/success/abstract_poly.v b/test-suite/success/abstract_poly.v new file mode 100644 index 0000000000..b736b734fd --- /dev/null +++ b/test-suite/success/abstract_poly.v @@ -0,0 +1,20 @@ +Set Universe Polymorphism. + +Inductive path@{i} {A : Type@{i}} (x : A) : A -> Type@{i} := refl : path x x. +Inductive unit@{i} : Type@{i} := tt. + +Lemma foo@{i j} : forall (m n : unit@{i}) (P : unit -> Type@{j}), path m n -> P m -> P n. +Proof. +intros m n P e p. +abstract (rewrite e in p; exact p). +Defined. + +Check foo_subproof@{Set Set}. + +Lemma bar : forall (m n : unit) (P : unit -> Type), path m n -> P m -> P n. +Proof. +intros m n P e p. +abstract (rewrite e in p; exact p). +Defined. + +Check bar_subproof@{Set Set Set}. -- cgit v1.2.3 From e23f495c25749478c0a64c479d888e3671157c7d Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 14 Jul 2017 13:27:56 +0200 Subject: Document the changes in API brought by this series of patches. --- dev/doc/changes.txt | 20 ++++++++++++++++++++ library/global.mli | 7 +++++++ 2 files changed, 27 insertions(+) diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index 159be9a582..62c3bc40c1 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -1,3 +1,23 @@ +========================================= += CHANGES BETWEEN COQ V8.6 AND COQ V8.8 = +========================================= + +* ML API * + +We removed the following functions: + +- Universes.unsafe_constr_of_global: use Global.constr_of_global_in_context + instead. The returned term contains De Bruijn universe variables. If you don't + depend on universes being instantiated, simply drop the context. +- Universes.unsafe_type_of_global: same as above with + Global.type_of_global_in_context + +We changed the type of the following functions: + +- Global.body_of_constant_body: now also returns the abstract universe context. + The returned term contains De Bruijn universe variables. +- Global.body_of_constant: same as above. + ========================================= = CHANGES BETWEEN COQ V8.6 AND COQ V8.7 = ========================================= diff --git a/library/global.mli b/library/global.mli index 431747c524..48bcfa989f 100644 --- a/library/global.mli +++ b/library/global.mli @@ -89,8 +89,15 @@ val constant_of_delta_kn : kernel_name -> constant val mind_of_delta_kn : kernel_name -> mutual_inductive val opaque_tables : unit -> Opaqueproof.opaquetab + val body_of_constant : constant -> (Term.constr * Univ.AUContext.t) option +(** Returns the body of the constant if it has any, and the polymorphic context + it lives in. For monomorphic constant, the latter is empty, and for + polymorphic constants, the term contains De Bruijn universe variables that + need to be instantiated. *) + val body_of_constant_body : Declarations.constant_body -> (Term.constr * Univ.AUContext.t) option +(** Same as {!body_of_constant} but on {!Declarations.constant_body}. *) (** Global universe name <-> level mapping *) type universe_names = -- cgit v1.2.3 From b21cd4620e0983a23dd11c0f582bf367662aeee3 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 14 Jul 2017 13:55:45 +0200 Subject: Fix a typo in dev/changes. --- dev/doc/changes.txt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index 62c3bc40c1..c3c86ac5c5 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -1,5 +1,5 @@ ========================================= -= CHANGES BETWEEN COQ V8.6 AND COQ V8.8 = += CHANGES BETWEEN COQ V8.7 AND COQ V8.8 = ========================================= * ML API * -- cgit v1.2.3