diff options
Diffstat (limited to 'kernel/cooking.ml')
| -rw-r--r-- | kernel/cooking.ml | 161 |
1 files changed, 83 insertions, 78 deletions
diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 13459915..6f4541e9 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* Created by Jean-Christophe Filliâtre out of V6.3 file constants.ml @@ -17,26 +19,28 @@ open CErrors open Util open Names open Term +open Constr open Declarations -open Environ open Univ +module NamedDecl = Context.Named.Declaration + (*s Cooking the constants. *) let pop_dirpath p = match DirPath.repr p with - | [] -> anomaly ~label:"dirpath_prefix" (Pp.str "empty dirpath") + | [] -> anomaly ~label:"dirpath_prefix" (Pp.str "empty dirpath.") | _::l -> DirPath.make l let pop_mind kn = - let (mp,dir,l) = Names.repr_mind kn in - Names.make_mind mp (pop_dirpath dir) l + let (mp,dir,l) = MutInd.repr3 kn in + MutInd.make3 mp (pop_dirpath dir) l let pop_con con = - let (mp,dir,l) = Names.repr_con con in - Names.make_con mp (pop_dirpath dir) l + let (mp,dir,l) = Constant.repr3 con in + Constant.make3 mp (pop_dirpath dir) l type my_global_reference = - | ConstRef of constant + | ConstRef of Constant.t | IndRef of inductive | ConstructRef of constructor @@ -99,42 +103,42 @@ let expmod_constr cache modlist c = let share_univs = share_univs cache in let update_case_info = update_case_info cache in let rec substrec c = - match kind_of_term c with + match kind c with | Case (ci,p,t,br) -> - map_constr substrec (mkCase (update_case_info ci modlist,p,t,br)) + Constr.map substrec (mkCase (update_case_info ci modlist,p,t,br)) | Ind (ind,u) -> (try share_univs (IndRef ind) u modlist with - | Not_found -> map_constr substrec c) + | Not_found -> Constr.map substrec c) | Construct (cstr,u) -> (try share_univs (ConstructRef cstr) u modlist with - | Not_found -> map_constr substrec c) + | Not_found -> Constr.map substrec c) | Const (cst,u) -> (try share_univs (ConstRef cst) u modlist with - | Not_found -> map_constr substrec 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_of_term p' with + match kind p' with | Const (p',_) -> mkProj (make p', substrec c') | App (f, args) -> - (match kind_of_term f with + (match kind f with | Const (p', _) -> mkProj (make p', substrec c') | _ -> assert false) | _ -> assert false - with Not_found -> map_constr substrec c) + with Not_found -> Constr.map substrec c) - | _ -> map_constr substrec c + | _ -> Constr.map substrec c in if is_empty_modlist modlist then c @@ -149,10 +153,14 @@ let abstract_constant_body = type recipe = { from : constant_body; info : Opaqueproof.cooking_info } type inline = bool -type result = - constant_def * constant_type * projection_body option * - bool * constant_universes * inline - * Context.section_context option +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; +} let on_body ml hy f = function | Undef _ as x -> x @@ -161,62 +169,64 @@ let on_body ml hy f = function OpaqueDef (Opaqueproof.discharge_direct_opaque ~cook_constr:f { Opaqueproof.modlist = ml; abstract = hy } o) -let constr_of_def otab = function - | Undef _ -> assert false - | Def cs -> Mod_subst.force_constr cs - | OpaqueDef lc -> Opaqueproof.force_proof otab lc - 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 } c = +let cook_constr { Opaqueproof.modlist ; abstract = (vars, subst, _) } c = let cache = RefTable.create 13 in - let expmod = expmod_constr_subst cache modlist (pi2 abstract) in - let hyps = Context.Named.map expmod (pi1 abstract) in + let expmod = expmod_constr_subst cache modlist subst in + let hyps = Context.Named.map expmod vars in abstract_constant_body (expmod c) hyps -let lift_univs cb subst = - if cb.const_polymorphic && not (Univ.LMap.is_empty subst) then - let inst = Univ.UContext.instance cb.const_universes in - let cstrs = Univ.UContext.constraints cb.const_universes in - let len = Univ.LMap.cardinal subst in - let subst = - Array.fold_left_i (fun i acc v -> Univ.LMap.add (Level.var i) (Level.var (i + len)) acc) - subst (Univ.Instance.to_array inst) - in - let cstrs' = Univ.subst_univs_level_constraints subst cstrs in - subst, Univ.UContext.make (inst,cstrs') - else subst, cb.const_universes - -let cook_constant env { from = cb; info } = +let lift_univs cb subst auctx0 = + match cb.const_universes with + | Monomorphic_const ctx -> + assert (AUContext.is_empty auctx0); + subst, (Monomorphic_const ctx) + | Polymorphic_const 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_const (AUContext.union auctx0 auctx)) + else + let ainst = Univ.make_abstract_instance auctx in + let subst = Instance.append subst ainst in + 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 { 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 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 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) - (fun c -> abstract_constant_body (expmod c) hyps) + map cb.const_body in let const_hyps = Context.Named.fold_outside (fun decl hyps -> - let open Context.Named.Declaration in - List.filter (fun decl' -> not (Id.equal (get_id decl) (get_id decl'))) + List.filter (fun decl' -> not (Id.equal (NamedDecl.get_id decl) (NamedDecl.get_id decl'))) hyps) hyps ~init:cb.const_hyps in - let typ = match cb.const_type with - | RegularArity t -> - let typ = - abstract_constant_type (expmod t) hyps in - RegularArity typ - | TemplateArity (ctx,s) -> - let t = mkArity (ctx,Type s.template_level) in - let typ = abstract_constant_type (expmod t) hyps in - let j = make_judge (constr_of_def (opaque_tables env) body) typ in - Typeops.make_polymorphic_if_constant_for_ind env j - 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 @@ -224,32 +234,27 @@ let cook_constant env { from = cb; info } = let ((mind, _), _), n' = try let c' = share_univs cache (IndRef (pb.proj_ind,0)) Univ.Instance.empty modlist in - match kind_of_term c' with + 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 typ = (* By invariant, a regular arity *) - match typ with RegularArity t -> t | TemplateArity _ -> assert false - 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 - let univs = - let abs' = - if cb.const_polymorphic then abs_ctx - else instantiate_univ_context abs_ctx - in - UContext.union abs' univs - in - (body, typ, Option.map projection cb.const_proj, - cb.const_polymorphic, univs, cb.const_inline_code, - Some const_hyps) - -(* let cook_constant_key = Profile.declare_profile "cook_constant" *) -(* let cook_constant = Profile.profile2 cook_constant_key cook_constant *) + { + 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; + } + +(* let cook_constant_key = CProfile.declare_profile "cook_constant" *) +(* let cook_constant = CProfile.profile2 cook_constant_key cook_constant *) let expmod_constr modlist c = expmod_constr (RefTable.create 13) modlist c |