From a21e1bb60f579baec910d4c3d8e8434501470b6d Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 17 May 2019 16:42:48 +0200 Subject: Move the Discharge module into the kernel. --- interp/declare.ml | 6 ++- interp/discharge.ml | 118 --------------------------------------------- interp/discharge.mli | 16 ------- interp/interp.mllib | 1 - kernel/discharge.ml | 132 +++++++++++++++++++++++++++++++++++++++++++++++++++ kernel/discharge.mli | 17 +++++++ kernel/kernel.mllib | 1 + library/lib.ml | 3 -- library/lib.mli | 1 - 9 files changed, 154 insertions(+), 141 deletions(-) delete mode 100644 interp/discharge.ml delete mode 100644 interp/discharge.mli create mode 100644 kernel/discharge.ml create mode 100644 kernel/discharge.mli diff --git a/interp/declare.ml b/interp/declare.ml index 7ee7ecb5e8..fd1f7df9aa 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -91,7 +91,8 @@ let discharge_constant ((sp, kn), obj) = let from = Global.lookup_constant con in let modlist = replacement_context () in let { abstr_ctx = hyps; abstr_subst = subst; abstr_uctx = uctx } = section_segment_of_constant con in - let abstract = (named_of_variable_context hyps, subst, uctx) in + let named_ctx = List.map fst hyps in + let abstract = (named_ctx, subst, uctx) in let new_decl = { from; info = { Opaqueproof.modlist; abstract } } in (* This is a hack: when leaving a section, we lose the constant definition, so we have to store it in the libobject to be able to retrieve it after. *) @@ -314,7 +315,8 @@ let discharge_inductive ((sp,kn),mie) = let mie = Global.lookup_mind mind in let repl = replacement_context () in let info = section_segment_of_mutual_inductive mind in - Some (Discharge.process_inductive info repl mie) + let hyps = List.map fst info.abstr_ctx in + Some (Discharge.process_inductive hyps info.abstr_subst info.abstr_uctx repl mie) let dummy_one_inductive_entry mie = { mind_entry_typename = mie.mind_entry_typename; diff --git a/interp/discharge.ml b/interp/discharge.ml deleted file mode 100644 index 1efd13adb1..0000000000 --- a/interp/discharge.ml +++ /dev/null @@ -1,118 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* lift ndecls (mkApp(mkRel (k+1),args))) in - let inds' = - List.map - (function (tname,arity,template,cnames,lc) -> - let lc' = List.map (substl subs) lc in - let lc'' = List.map (fun b -> Termops.it_mkNamedProd_wo_LetIn b decls) lc' in - let arity' = Termops.it_mkNamedProd_wo_LetIn arity decls in - (tname,arity',template,cnames,lc'')) - inds in - let nparamdecls' = nparamdecls + Array.length args in -(* To be sure to be the same as before, should probably be moved to process_inductive *) - let params' = let (_,arity,_,_,_) = List.hd inds' in - let (params,_) = decompose_prod_n_assum nparamdecls' arity in - params - in - let ind'' = - List.map - (fun (a,arity,template,c,lc) -> - let _, short_arity = decompose_prod_n_assum nparamdecls' arity in - let shortlc = - List.map (fun c -> snd (decompose_prod_n_assum nparamdecls' c)) lc in - { mind_entry_typename = a; - mind_entry_arity = short_arity; - mind_entry_template = template; - mind_entry_consnames = c; - mind_entry_lc = shortlc }) - inds' - in (params',ind'') - -let refresh_polymorphic_type_of_inductive (_,mip) = - match mip.mind_arity with - | RegularArity s -> s.mind_user_arity, false - | TemplateArity ar -> - let ctx = List.rev mip.mind_arity_ctxt in - mkArity (List.rev ctx, Sorts.sort_of_univ ar.template_level), true - -let process_inductive info modlist mib = - let section_decls = Lib.named_of_variable_context info.Lib.abstr_ctx in - let nparamdecls = Context.Rel.length mib.mind_params_ctxt in - let subst, ind_univs = - match mib.mind_universes with - | Monomorphic ctx -> Univ.empty_level_subst, Monomorphic_entry ctx - | Polymorphic auctx -> - let subst, auctx = Lib.discharge_abstract_universe_context info auctx in - let nas = Univ.AUContext.names auctx in - let auctx = Univ.AUContext.repr auctx in - subst, Polymorphic_entry (nas, auctx) - in - let variance = match mib.mind_variance with - | None -> None - | Some _ -> Some (InferCumulativity.dummy_variance ind_univs) - 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 = 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 section_decls' = Context.Named.map discharge section_decls in - let (params',inds') = abstract_inductive section_decls' nparamdecls inds in - let record = match mib.mind_record with - | PrimRecord info -> - Some (Some (Array.map (fun (x,_,_,_) -> x) info)) - | FakeRecord -> Some None - | NotRecord -> None - in - { mind_entry_record = record; - mind_entry_finite = mib.mind_finite; - mind_entry_params = params'; - mind_entry_inds = inds'; - mind_entry_private = mib.mind_private; - mind_entry_variance = variance; - mind_entry_universes = ind_univs - } - diff --git a/interp/discharge.mli b/interp/discharge.mli deleted file mode 100644 index f7408937cf..0000000000 --- a/interp/discharge.mli +++ /dev/null @@ -1,16 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* work_list -> mutual_inductive_body -> mutual_inductive_entry diff --git a/interp/interp.mllib b/interp/interp.mllib index 1262dbb181..b65a171ef9 100644 --- a/interp/interp.mllib +++ b/interp/interp.mllib @@ -16,5 +16,4 @@ Implicit_quantifiers Constrintern Modintern Constrextern -Discharge Declare diff --git a/kernel/discharge.ml b/kernel/discharge.ml new file mode 100644 index 0000000000..e7e84f14d0 --- /dev/null +++ b/kernel/discharge.ml @@ -0,0 +1,132 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* mkNamedProd_wo_LetIn d c) b d + +let abstract_inductive decls nparamdecls inds = + let ntyp = List.length inds in + let ndecls = Context.Named.length decls in + let args = Context.Named.to_instance mkVar (List.rev decls) in + let args = Array.of_list args in + let subs = List.init ntyp (fun k -> lift ndecls (mkApp(mkRel (k+1),args))) in + let inds' = + List.map + (function (tname,arity,template,cnames,lc) -> + let lc' = List.map (substl subs) lc in + let lc'' = List.map (fun b -> it_mkNamedProd_wo_LetIn b decls) lc' in + let arity' = it_mkNamedProd_wo_LetIn arity decls in + (tname,arity',template,cnames,lc'')) + inds in + let nparamdecls' = nparamdecls + Array.length args in +(* To be sure to be the same as before, should probably be moved to process_inductive *) + let params' = let (_,arity,_,_,_) = List.hd inds' in + let (params,_) = decompose_prod_n_assum nparamdecls' arity in + params + in + let ind'' = + List.map + (fun (a,arity,template,c,lc) -> + let _, short_arity = decompose_prod_n_assum nparamdecls' arity in + let shortlc = + List.map (fun c -> snd (decompose_prod_n_assum nparamdecls' c)) lc in + { mind_entry_typename = a; + mind_entry_arity = short_arity; + mind_entry_template = template; + mind_entry_consnames = c; + mind_entry_lc = shortlc }) + inds' + in (params',ind'') + +let refresh_polymorphic_type_of_inductive (_,mip) = + match mip.mind_arity with + | RegularArity s -> s.mind_user_arity, false + | TemplateArity ar -> + let ctx = List.rev mip.mind_arity_ctxt in + mkArity (List.rev ctx, Sorts.sort_of_univ ar.template_level), true + +let dummy_variance = let open Entries in function + | Monomorphic_entry _ -> assert false + | Polymorphic_entry (_,uctx) -> Array.make (Univ.UContext.size uctx) Univ.Variance.Irrelevant + +let discharge_abstract_universe_context subst abs_ctx auctx = + let open Univ in + let ainst = make_abstract_instance auctx in + let subst = Instance.append subst ainst in + let subst = make_instance_subst subst in + let auctx = Univ.subst_univs_level_abstract_universe_context subst auctx in + subst, AUContext.union abs_ctx auctx + +let process_inductive section_decls subst abs_uctx modlist mib = + let nparamdecls = Context.Rel.length mib.mind_params_ctxt in + let subst, ind_univs = + match mib.mind_universes with + | Monomorphic ctx -> Univ.empty_level_subst, Monomorphic_entry ctx + | Polymorphic auctx -> + let subst, auctx = discharge_abstract_universe_context subst abs_uctx auctx in + let nas = Univ.AUContext.names auctx in + let auctx = Univ.AUContext.repr auctx in + subst, Polymorphic_entry (nas, auctx) + in + let variance = match mib.mind_variance with + | None -> None + | Some _ -> Some (dummy_variance ind_univs) + 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 = 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 section_decls' = Context.Named.map discharge section_decls in + let (params',inds') = abstract_inductive section_decls' nparamdecls inds in + let record = match mib.mind_record with + | PrimRecord info -> + Some (Some (Array.map (fun (x,_,_,_) -> x) info)) + | FakeRecord -> Some None + | NotRecord -> None + in + { mind_entry_record = record; + mind_entry_finite = mib.mind_finite; + mind_entry_params = params'; + mind_entry_inds = inds'; + mind_entry_private = mib.mind_private; + mind_entry_variance = variance; + mind_entry_universes = ind_univs + } + diff --git a/kernel/discharge.mli b/kernel/discharge.mli new file mode 100644 index 0000000000..3e32a12c3c --- /dev/null +++ b/kernel/discharge.mli @@ -0,0 +1,17 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* + Univ.Instance.t -> Univ.AUContext.t -> work_list -> mutual_inductive_body -> mutual_inductive_entry diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib index 59c1d5890f..238cbba425 100644 --- a/kernel/kernel.mllib +++ b/kernel/kernel.mllib @@ -48,4 +48,5 @@ Term_typing Subtyping Mod_typing Nativelibrary +Discharge Safe_typing diff --git a/library/lib.ml b/library/lib.ml index 4be288ed20..daa41eca65 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -474,9 +474,6 @@ let extract_hyps (secs,ohyps) = let instance_from_variable_context = List.map fst %> List.filter is_local_assum %> List.map NamedDecl.get_id %> Array.of_list -let named_of_variable_context = - List.map fst - let name_instance inst = (* FIXME: this should probably be done at an upper level, by storing the name information in the section data structure. *) diff --git a/library/lib.mli b/library/lib.mli index 5da76961a6..c19c3bf7fa 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -168,7 +168,6 @@ type abstr_info = private { } val instance_from_variable_context : variable_context -> Id.t array -val named_of_variable_context : variable_context -> Constr.named_context val section_segment_of_constant : Constant.t -> abstr_info val section_segment_of_mutual_inductive: MutInd.t -> abstr_info -- cgit v1.2.3