From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 2 Feb 2019 19:29:23 -0500 Subject: Imported Upstream version 8.9.0 --- kernel/cooking.ml | 79 +++++++++++++++++++++++++++---------------------------- 1 file changed, 39 insertions(+), 40 deletions(-) (limited to 'kernel/cooking.ml') diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 6f4541e9..657478a1 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -24,6 +24,7 @@ open Declarations open Univ module NamedDecl = Context.Named.Declaration +module RelDecl = Context.Rel.Declaration (*s Cooking the constants. *) @@ -126,17 +127,13 @@ let expmod_constr cache modlist c = | Not_found -> Constr.map substrec c) | Proj (p, c') -> - (try - let p' = share_univs (ConstRef (Projection.constant p)) Univ.Instance.empty modlist in - let make c = Projection.make c (Projection.unfolded p) in - match kind p' with - | Const (p',_) -> mkProj (make p', substrec c') - | App (f, args) -> - (match kind f with - | Const (p', _) -> mkProj (make p', substrec c') - | _ -> assert false) - | _ -> assert false - with Not_found -> Constr.map substrec c) + let map cst npars = + let _, newpars = Mindmap.find cst (snd modlist) in + pop_mind cst, npars + Array.length newpars + in + let p' = try Projection.map_npars map p with Not_found -> p in + let c'' = substrec c' in + if p == p' && c' == c'' then c else mkProj (p', c'') | _ -> Constr.map substrec c @@ -144,11 +141,31 @@ let expmod_constr cache modlist c = if is_empty_modlist modlist then c else substrec c -let abstract_constant_type = - List.fold_left (fun c d -> mkNamedProd_wo_LetIn d c) +(** Transforms a named context into a rel context. Also returns the list of + variables [id1 ... idn] that need to be replaced by [Rel 1 ... Rel n] to + abstract a term that lived in that context. *) +let abstract_context hyps = + let fold decl (ctx, subst) = + let id, decl = match decl with + | NamedDecl.LocalDef (id, b, t) -> + let b = Vars.subst_vars subst b in + let t = Vars.subst_vars subst t in + id, RelDecl.LocalDef (Name id, b, t) + | NamedDecl.LocalAssum (id, t) -> + let t = Vars.subst_vars subst t in + id, RelDecl.LocalAssum (Name id, t) + in + (decl :: ctx, id :: subst) + in + Context.Named.fold_outside fold hyps ~init:([], []) + +let abstract_constant_type t (hyps, subst) = + let t = Vars.subst_vars subst t in + List.fold_left (fun c d -> mkProd_wo_LetIn d c) t hyps -let abstract_constant_body = - List.fold_left (fun c d -> mkNamedLambda_or_LetIn d c) +let abstract_constant_body c (hyps, subst) = + let c = Vars.subst_vars subst c in + it_mkLambda_or_LetIn c hyps type recipe = { from : constant_body; info : Opaqueproof.cooking_info } type inline = bool @@ -156,10 +173,9 @@ type inline = bool type result = { cook_body : constant_def; cook_type : types; - cook_proj : projection_body option; cook_universes : constant_universes; cook_inline : inline; - cook_context : Context.Named.t option; + cook_context : Constr.named_context option; } let on_body ml hy f = function @@ -178,6 +194,7 @@ 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 lift_univs cb subst auctx0 = @@ -206,18 +223,19 @@ let lift_univs cb subst auctx0 = let auctx' = Univ.subst_univs_level_abstract_universe_context (Univ.make_instance_subst subst) auctx in subst, (Polymorphic_const (AUContext.union auctx0 auctx')) -let cook_constant ~hcons env { from = cb; info } = +let cook_constant ~hcons { from = cb; info } = let { Opaqueproof.modlist; abstract } = info in let cache = RefTable.create 13 in let abstract, usubst, abs_ctx = abstract in let usubst, univs = lift_univs cb usubst abs_ctx in let expmod = expmod_constr_subst cache modlist usubst in - let hyps = Context.Named.map expmod abstract 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 (hyps, usubst, abs_ctx) + let body = on_body modlist (hyps0, usubst, abs_ctx) map cb.const_body in @@ -225,30 +243,11 @@ let cook_constant ~hcons env { from = cb; info } = Context.Named.fold_outside (fun decl hyps -> List.filter (fun decl' -> not (Id.equal (NamedDecl.get_id decl) (NamedDecl.get_id decl'))) hyps) - hyps ~init:cb.const_hyps in + hyps0 ~init:cb.const_hyps in let typ = abstract_constant_type (expmod cb.const_type) hyps in - let projection pb = - let c' = abstract_constant_body (expmod pb.proj_body) hyps in - let etab = abstract_constant_body (expmod (fst pb.proj_eta)) hyps in - let etat = abstract_constant_body (expmod (snd pb.proj_eta)) hyps in - let ((mind, _), _), n' = - try - let c' = share_univs cache (IndRef (pb.proj_ind,0)) Univ.Instance.empty modlist in - match kind c' with - | App (f,l) -> (destInd f, Array.length l) - | Ind ind -> ind, 0 - | _ -> assert false - with Not_found -> (((pb.proj_ind,0),Univ.Instance.empty), 0) - in - let ctx, ty' = decompose_prod_n (n' + pb.proj_npars + 1) typ in - { proj_ind = mind; proj_npars = pb.proj_npars + n'; proj_arg = pb.proj_arg; - proj_eta = etab, etat; - proj_type = ty'; proj_body = c' } - in { cook_body = body; cook_type = typ; - cook_proj = Option.map projection cb.const_proj; cook_universes = univs; cook_inline = cb.const_inline_code; cook_context = Some const_hyps; -- cgit v1.2.3