From 7002b3daca6da29eadf80019847630b8583c3daf Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Sun, 3 Aug 2014 20:02:49 +0200 Subject: Move to a representation of universe polymorphic constants using indices for variables. Simplifies instantiation of constants/inductives, requiring less allocation and Map.find's. Abstraction by variables is handled mostly inside the kernel but could be moved outside. --- kernel/cooking.ml | 40 +++++++++++++++++++++++++++++----------- 1 file changed, 29 insertions(+), 11 deletions(-) (limited to 'kernel/cooking.ml') diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 5fa01e5db..589a26134 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -165,18 +165,37 @@ let constr_of_def = function | Def cs -> Mod_subst.force_constr cs | OpaqueDef lc -> Opaqueproof.force_proof lc +let expmod_constr_subst cache modlist subst c = + let c = expmod_constr cache modlist c in + Vars.subst_univs_level_constr subst c let cook_constr { Opaqueproof.modlist ; abstract } c = let cache = RefTable.create 13 in - let hyps = Context.map_named_context (expmod_constr cache modlist) (fst abstract) in - abstract_constant_body (expmod_constr cache modlist c) hyps + let expmod = expmod_constr_subst cache modlist (pi2 abstract) in + let hyps = Context.map_named_context expmod (pi1 abstract) in + abstract_constant_body (expmod c) hyps + +let lift_univs cb subst = + if cb.const_polymorphic 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 = { Opaqueproof.modlist; abstract } } = let cache = RefTable.create 13 in - let abstract, abs_ctx = abstract in - let hyps = Context.map_named_context (expmod_constr cache modlist) abstract in - let body = on_body modlist (hyps, abs_ctx) - (fun c -> abstract_constant_body (expmod_constr cache modlist c) hyps) + let abstract, usubst, abs_ctx = abstract in + let usubst, univs = lift_univs cb usubst in + let expmod = expmod_constr_subst cache modlist usubst in + let hyps = Context.map_named_context expmod abstract in + let body = on_body modlist (hyps, usubst, abs_ctx) + (fun c -> abstract_constant_body (expmod c) hyps) cb.const_body in let const_hyps = @@ -186,17 +205,16 @@ let cook_constant env { from = cb; info = { Opaqueproof.modlist; abstract } } = let typ = match cb.const_type with | RegularArity t -> let typ = - abstract_constant_type (expmod_constr cache modlist t) hyps in + 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_constr cache modlist t) hyps in + let typ = abstract_constant_type (expmod t) hyps in let j = make_judge (constr_of_def body) typ in Typeops.make_polymorphic_if_constant_for_ind env j in let projection pb = - let c' = abstract_constant_body (expmod_constr cache modlist pb.proj_body) hyps in + let c' = abstract_constant_body (expmod pb.proj_body) hyps in let ((mind, _), _), n' = try let c' = share_univs cache (IndRef (pb.proj_ind,0)) Univ.Instance.empty modlist in @@ -213,7 +231,7 @@ let cook_constant env { from = cb; info = { Opaqueproof.modlist; abstract } } = { proj_ind = mind; proj_npars = pb.proj_npars + n'; proj_arg = pb.proj_arg; proj_type = ty'; proj_body = c' } in - let univs = UContext.union abs_ctx cb.const_universes in + let univs = UContext.union abs_ctx univs in (body, typ, Option.map projection cb.const_proj, cb.const_polymorphic, univs, cb.const_inline_code, Some const_hyps) -- cgit v1.2.3