diff options
Diffstat (limited to 'kernel/cooking.ml')
| -rw-r--r-- | kernel/cooking.ml | 220 |
1 files changed, 170 insertions, 50 deletions
diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 9b6e37251f..0951b07d49 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -159,31 +159,38 @@ type 'opaque result = { cook_body : (constr Mod_subst.substituted, 'opaque) constant_def; cook_type : types; cook_universes : universes; - cook_private_univs : Univ.ContextSet.t option; cook_relevance : Sorts.relevance; cook_inline : inline; cook_context : Constr.named_context option; } -let on_body ml hy f = function - | Undef _ as x -> x - | Def cs -> Def (Mod_subst.from_val (f (Mod_subst.force_constr cs))) - | OpaqueDef o -> - OpaqueDef (Opaqueproof.discharge_direct_opaque ~cook_constr:f - { Opaqueproof.modlist = ml; abstract = hy } o) - | Primitive _ -> CErrors.anomaly (Pp.str "Primitives cannot be cooked") - let expmod_constr_subst cache modlist subst c = let subst = Univ.make_instance_subst subst in let c = expmod_constr cache modlist c in Vars.subst_univs_level_constr subst c -let cook_constr { Opaqueproof.modlist ; abstract = (vars, subst, _) } c = - let cache = RefTable.create 13 in - let expmod = expmod_constr_subst cache modlist subst in - let hyps = Context.Named.map expmod vars in - let hyps = abstract_context hyps in - abstract_constant_body (expmod c) hyps +let discharge_abstract_universe_context subst abs_ctx auctx = + (** Given a named instance [subst := u₀ ... uₙ₋₁] together with an abstract + context [auctx0 := 0 ... n - 1 |= C{0, ..., n - 1}] of the same length, + and another abstract context relative to the former context + [auctx := 0 ... m - 1 |= C'{u₀, ..., uₙ₋₁, 0, ..., m - 1}], + construct the lifted abstract universe context + [0 ... n - 1 n ... n + m - 1 |= + C{0, ... n - 1} ∪ + C'{0, ..., n - 1, n, ..., n + m - 1} ] + together with the instance + [u₀ ... uₙ₋₁ Var(0) ... Var (m - 1)]. + *) + if (Univ.Instance.is_empty subst) then + (** Still need to take the union for the constraints between globals *) + subst, (AUContext.union abs_ctx auctx) + else + let open Univ in + let ainst = make_abstract_instance auctx in + let subst = Instance.append subst ainst in + let substf = make_instance_subst subst in + let auctx = Univ.subst_univs_level_abstract_universe_context substf auctx in + subst, (AUContext.union abs_ctx auctx) let lift_univs cb subst auctx0 = match cb.const_universes with @@ -191,28 +198,35 @@ let lift_univs cb subst auctx0 = assert (AUContext.is_empty auctx0); subst, (Monomorphic ctx) | Polymorphic auctx -> - (** Given a named instance [subst := u₀ ... uₙ₋₁] together with an abstract - context [auctx0 := 0 ... n - 1 |= C{0, ..., n - 1}] of the same length, - and another abstract context relative to the former context - [auctx := 0 ... m - 1 |= C'{u₀, ..., uₙ₋₁, 0, ..., m - 1}], - construct the lifted abstract universe context - [0 ... n - 1 n ... n + m - 1 |= - C{0, ... n - 1} ∪ - C'{0, ..., n - 1, n, ..., n + m - 1} ] - together with the instance - [u₀ ... uₙ₋₁ Var(0) ... Var (m - 1)]. - *) - if (Univ.Instance.is_empty subst) then - (** Still need to take the union for the constraints between globals *) - subst, (Polymorphic (AUContext.union auctx0 auctx)) - else - let ainst = Univ.make_abstract_instance auctx in - let subst = Instance.append subst ainst in - let substf = Univ.make_instance_subst subst in - let auctx' = Univ.subst_univs_level_abstract_universe_context substf auctx in - subst, (Polymorphic (AUContext.union auctx0 auctx')) - -let cook_constant ~hcons { from = cb; info } = + let subst, auctx = discharge_abstract_universe_context subst auctx0 auctx in + subst, (Polymorphic auctx) + +let cook_constr { Opaqueproof.modlist ; abstract } (c, priv) = + let cache = RefTable.create 13 in + let abstract, usubst, abs_ctx = abstract in + let usubst, priv = match priv with + | Opaqueproof.PrivateMonomorphic () -> + let () = assert (AUContext.is_empty abs_ctx) in + let () = assert (Instance.is_empty usubst) in + usubst, priv + | Opaqueproof.PrivatePolymorphic (univs, ctx) -> + let ainst = Instance.of_array (Array.init univs Level.var) in + let usubst = Instance.append usubst ainst in + let ctx = on_snd (Univ.subst_univs_level_constraints (Univ.make_instance_subst usubst)) ctx in + let univs = univs + AUContext.size abs_ctx in + usubst, Opaqueproof.PrivatePolymorphic (univs, ctx) + in + let expmod = expmod_constr_subst cache modlist usubst in + let hyps = Context.Named.map expmod abstract in + let hyps = abstract_context hyps in + let c = abstract_constant_body (expmod c) hyps in + (c, priv) + +let cook_constr infos c = + let fold info c = cook_constr info c in + List.fold_right fold infos c + +let cook_constant { from = cb; info } = let { Opaqueproof.modlist; abstract } = info in let cache = RefTable.create 13 in let abstract, usubst, abs_ctx = abstract in @@ -220,13 +234,13 @@ let cook_constant ~hcons { from = cb; info } = let expmod = expmod_constr_subst cache modlist usubst in let hyps0 = Context.Named.map expmod abstract in let hyps = abstract_context hyps0 in - let map c = - let c = abstract_constant_body (expmod c) hyps in - if hcons then Constr.hcons c else c - in - let body = on_body modlist (hyps0, usubst, abs_ctx) - map - cb.const_body + let map c = abstract_constant_body (expmod c) hyps in + let body = match cb.const_body with + | Undef _ as x -> x + | Def cs -> Def (Mod_subst.from_val (map (Mod_subst.force_constr cs))) + | OpaqueDef o -> + OpaqueDef (Opaqueproof.discharge_direct_opaque info o) + | Primitive _ -> CErrors.anomaly (Pp.str "Primitives cannot be cooked") in let const_hyps = Context.Named.fold_outside (fun decl hyps -> @@ -234,15 +248,10 @@ let cook_constant ~hcons { from = cb; info } = hyps) hyps0 ~init:cb.const_hyps in let typ = abstract_constant_type (expmod cb.const_type) hyps in - let private_univs = Option.map (on_snd (Univ.subst_univs_level_constraints - (Univ.make_instance_subst usubst))) - cb.const_private_poly_univs - in { cook_body = body; cook_type = typ; cook_universes = univs; - cook_private_univs = private_univs; cook_relevance = cb.const_relevance; cook_inline = cb.const_inline_code; cook_context = Some const_hyps; @@ -251,4 +260,115 @@ let cook_constant ~hcons { from = cb; info } = (* let cook_constant_key = CProfile.declare_profile "cook_constant" *) (* let cook_constant = CProfile.profile2 cook_constant_key cook_constant *) +(********************************) +(* Discharging mutual inductive *) + +(* Replace + + Var(y1)..Var(yq):C1..Cq |- Ij:Bj + Var(y1)..Var(yq):C1..Cq; I1..Ip:B1..Bp |- ci : Ti + + by + + |- Ij: (y1..yq:C1..Cq)Bj + I1..Ip:(B1 y1..yq)..(Bp y1..yq) |- ci : (y1..yq:C1..Cq)Ti[Ij:=(Ij y1..yq)] +*) + +let it_mkNamedProd_wo_LetIn b d = + List.fold_left (fun c d -> mkNamedProd_wo_LetIn d c) b d + +let abstract_inductive decls nparamdecls inds = + let open Entries in + 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 (Vars.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 cook_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 cook_inductive { Opaqueproof.modlist; abstract } mib = + let open Entries in + let (section_decls, subst, abs_uctx) = abstract 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 = discharge_abstract_universe_context subst abs_uctx auctx in + let subst = Univ.make_instance_subst subst 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 cache = RefTable.create 13 in + let discharge c = Vars.subst_univs_level_constr subst (expmod_constr cache 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 + } + let expmod_constr modlist c = expmod_constr (RefTable.create 13) modlist c |