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 28f108a15..154793a32 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 439f83578..a24d20c68 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 38a29f76e..f1c9bfca2 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 5af36fc6b..c4418b5a6 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 b6308aba0..474c0b4dd 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 a0dabe2f4..c8c7e3b8b 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