diff options
-rw-r--r-- | kernel/declarations.ml | 111 | ||||
-rw-r--r-- | kernel/declarations.mli | 13 | ||||
-rw-r--r-- | kernel/safe_typing.ml | 34 | ||||
-rw-r--r-- | kernel/term.mli | 1 | ||||
-rw-r--r-- | kernel/univ.ml | 27 | ||||
-rw-r--r-- | kernel/univ.mli | 1 |
6 files changed, 132 insertions, 55 deletions
diff --git a/kernel/declarations.ml b/kernel/declarations.ml index f092c8261..1a84b9876 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -83,11 +83,6 @@ type constant_def = | Def of constr_substituted | OpaqueDef of lazy_constr -let subst_constant_def sub = function - | Undef inl -> Undef inl - | Def c -> Def (subst_constr_subst sub c) - | OpaqueDef lc -> OpaqueDef (subst_lazy_constr sub lc) - type constant_body = { const_hyps : section_context; (* New: younger hyp at top *) const_body : constant_def; @@ -108,8 +103,7 @@ let is_opaque cb = match cb.const_body with | OpaqueDef _ -> true | Undef _ | Def _ -> false -(*s Inductive types (internal representation with redundant - information). *) +(* Substitutions of [constant_body] *) let subst_rel_declaration sub (id,copt,t as x) = let copt' = Option.smartmap (subst_mps sub) copt in @@ -118,6 +112,69 @@ let subst_rel_declaration sub (id,copt,t as x) = let subst_rel_context sub = list_smartmap (subst_rel_declaration sub) +(* TODO: these substitution functions could avoid duplicating things + when the substitution have preserved all the fields *) + +let subst_const_type sub arity = + if is_empty_subst sub then arity + else match arity with + | NonPolymorphicType s -> NonPolymorphicType (subst_mps sub s) + | PolymorphicArity (ctx,s) -> PolymorphicArity (subst_rel_context sub ctx,s) + +let subst_const_def sub = function + | Undef inl -> Undef inl + | Def c -> Def (subst_constr_subst sub c) + | OpaqueDef lc -> OpaqueDef (subst_lazy_constr sub lc) + +let subst_const_body sub cb = { + const_hyps = (assert (cb.const_hyps=[]); []); + const_body = subst_const_def sub cb.const_body; + const_type = subst_const_type sub cb.const_type; + const_body_code = Cemitcodes.subst_to_patch_subst sub cb.const_body_code; + const_constraints = cb.const_constraints} + +(* Hash-consing of [constant_body] *) + +let hcons_rel_decl ((n,oc,t) as d) = + let n' = hcons_name n + and oc' = Option.smartmap hcons_constr oc + and t' = hcons_types t + in if n' == n && oc' == oc && t' == t then d else (n',oc',t') + +let hcons_rel_context l = list_smartmap hcons_rel_decl l + +let hcons_polyarity ar = + { poly_param_levels = + list_smartmap (Option.smartmap hcons_univ) ar.poly_param_levels; + poly_level = hcons_univ ar.poly_level } + +let hcons_const_type = function + | NonPolymorphicType t -> + NonPolymorphicType (hcons_constr t) + | PolymorphicArity (ctx,s) -> + PolymorphicArity (hcons_rel_context ctx, hcons_polyarity s) + +let hcons_const_def = function + | Undef inl -> Undef inl + | Def l_constr -> + let constr = force l_constr in + Def (from_val (hcons_constr constr)) + | OpaqueDef lc -> + if lazy_constr_is_val lc then + let constr = force_opaque lc in + OpaqueDef (opaque_from_val (hcons_constr constr)) + else OpaqueDef lc + +let hcons_const_body cb = + { cb with + const_body = hcons_const_def cb.const_body; + const_type = hcons_const_type cb.const_type; + const_constraints = hcons_constraints cb.const_constraints } + + +(*s Inductive types (internal representation with redundant + information). *) + type recarg = | Norec | Mrec of inductive @@ -256,22 +313,7 @@ type mutual_inductive_body = { } -let subst_arity sub arity = - if is_empty_subst sub then arity - else match arity with - | NonPolymorphicType s -> NonPolymorphicType (subst_mps sub s) - | PolymorphicArity (ctx,s) -> PolymorphicArity (subst_rel_context sub ctx,s) - -(* TODO: should be changed to non-coping after Term.subst_mps *) -let subst_const_body sub cb = { - const_hyps = (assert (cb.const_hyps=[]); []); - const_body = subst_constant_def sub cb.const_body; - const_type = subst_arity sub cb.const_type; - const_body_code = Cemitcodes.subst_to_patch_subst sub cb.const_body_code; - (*const_type_code = Cemitcodes.subst_to_patch sub cb.const_type_code;*) - const_constraints = cb.const_constraints} - -let subst_arity sub = function +let subst_indarity sub = function | Monomorphic s -> Monomorphic { mind_user_arity = subst_mps sub s.mind_user_arity; @@ -285,7 +327,7 @@ let subst_mind_packet sub mbp = mind_typename = mbp.mind_typename; mind_nf_lc = array_smartmap (subst_mps sub) mbp.mind_nf_lc; mind_arity_ctxt = subst_rel_context sub mbp.mind_arity_ctxt; - mind_arity = subst_arity sub mbp.mind_arity; + mind_arity = subst_indarity sub mbp.mind_arity; mind_user_lc = array_smartmap (subst_mps sub) mbp.mind_user_lc; mind_nrealargs = mbp.mind_nrealargs; mind_nrealargs_ctxt = mbp.mind_nrealargs_ctxt; @@ -295,7 +337,6 @@ let subst_mind_packet sub mbp = mind_nb_args = mbp.mind_nb_args; mind_reloc_tbl = mbp.mind_reloc_tbl } - let subst_mind sub mib = { mind_record = mib.mind_record ; mind_finite = mib.mind_finite ; @@ -308,6 +349,26 @@ let subst_mind sub mib = mind_packets = array_smartmap (subst_mind_packet sub) mib.mind_packets ; mind_constraints = mib.mind_constraints } +let hcons_indarity = function + | Monomorphic a -> + Monomorphic { mind_user_arity = hcons_constr a.mind_user_arity; + mind_sort = hcons_sorts a.mind_sort } + | Polymorphic a -> Polymorphic (hcons_polyarity a) + +let hcons_mind_packet oib = + { oib with + mind_typename = hcons_ident oib.mind_typename; + mind_arity_ctxt = hcons_rel_context oib.mind_arity_ctxt; + mind_arity = hcons_indarity oib.mind_arity; + mind_consnames = array_smartmap hcons_ident oib.mind_consnames; + mind_user_lc = array_smartmap hcons_types oib.mind_user_lc; + mind_nf_lc = array_smartmap hcons_types oib.mind_nf_lc } + +let hcons_mind mib = + { mib with + mind_packets = array_smartmap hcons_mind_packet mib.mind_packets; + mind_params_ctxt = hcons_rel_context mib.mind_params_ctxt; + mind_constraints = hcons_constraints mib.mind_constraints } (*s Modules: signature component specifications, module types, and module declarations *) diff --git a/kernel/declarations.mli b/kernel/declarations.mli index ebedd17e6..5b800edec 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -62,8 +62,6 @@ type constant_def = | Def of constr_substituted | OpaqueDef of lazy_constr -val subst_constant_def : substitution -> constant_def -> constant_def - type constant_body = { const_hyps : section_context; (** New: younger hyp at top *) const_body : constant_def; @@ -71,6 +69,7 @@ type constant_body = { const_body_code : to_patch_substituted; const_constraints : constraints } +val subst_const_def : substitution -> constant_def -> constant_def val subst_const_body : substitution -> constant_body -> constant_body (** Is there a actual body in const_body or const_body_opaque ? *) @@ -233,3 +232,13 @@ and module_type_body = typ_constraints : constraints; (** quotiented set of equivalent constant and inductive name *) typ_delta :delta_resolver} + + +(** Hash-consing *) + +(** Here, strictly speaking, we don't perform true hash-consing + of the structure, but simply hash-cons all inner constr + and other known elements *) + +val hcons_const_body : constant_body -> constant_body +val hcons_mind : mutual_inductive_body -> mutual_inductive_body diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 0e5af7737..e5b8412ec 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -255,37 +255,14 @@ type global_declaration = | ConstantEntry of constant_entry | GlobalRecipe of Cooking.recipe -let hcons_const_type = function - | NonPolymorphicType t -> - NonPolymorphicType (hcons_constr t) - | PolymorphicArity (ctx,s) -> - PolymorphicArity (map_rel_context hcons_constr ctx,s) - -let hcons_const_body = function - | Undef inl -> Undef inl - | Def l_constr -> - let constr = Declarations.force l_constr in - Def (Declarations.from_val (hcons_constr constr)) - | OpaqueDef lc -> - if lazy_constr_is_val lc then - let constr = Declarations.force_opaque lc in - OpaqueDef (Declarations.opaque_from_val (hcons_constr constr)) - else OpaqueDef lc - -let hcons_constant_body cb = - { cb with - const_body = hcons_const_body cb.const_body; - const_type = hcons_const_type cb.const_type } - let add_constant dir l decl senv = check_label l senv; let kn = make_con senv.modinfo.modpath dir l in - let cb = - match decl with - | ConstantEntry ce -> translate_constant senv.env kn ce - | GlobalRecipe r -> - let cb = translate_recipe senv.env kn r in - if dir = empty_dirpath then hcons_constant_body cb else cb + let cb = match decl with + | ConstantEntry ce -> translate_constant senv.env kn ce + | GlobalRecipe r -> + let cb = translate_recipe senv.env kn r in + if dir = empty_dirpath then hcons_const_body cb else cb in let senv' = add_field (l,SFBconst cb) (C kn) senv in let senv'' = match cb.const_body with @@ -310,6 +287,7 @@ let add_mind dir l mie senv = all labels *) let kn = make_mind senv.modinfo.modpath dir l in let mib = translate_mind senv.env kn mie in + let mib = if mib.mind_hyps <> [] then mib else hcons_mind mib in let senv' = add_field (l,SFBmind mib) (I kn) senv in kn, senv' diff --git a/kernel/term.mli b/kernel/term.mli index c556d0a07..7992c0bab 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -626,6 +626,7 @@ val hash_constr : constr -> int (*********************************************************************) +val hcons_sorts : sorts -> sorts val hcons_constr : constr -> constr val hcons_types : types -> types diff --git a/kernel/univ.ml b/kernel/univ.ml index 96990d696..7f458f64c 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -861,3 +861,30 @@ module Huniv = let hcons_univlevel = Hashcons.simple_hcons Hunivlevel.f Names.hcons_dirpath let hcons_univ = Hashcons.simple_hcons Huniv.f hcons_univlevel +module Hconstraint = + Hashcons.Make( + struct + type t = univ_constraint + type u = universe_level -> universe_level + let hash_sub hul (l1,k,l2) = (hul l1, k, hul l2) + let equal (l1,k,l2) (l1',k',l2') = + l1 == l1' && k = k' && l2 == l2' + let hash = Hashtbl.hash + end) + +module Hconstraints = + Hashcons.Make( + struct + type t = constraints + type u = univ_constraint -> univ_constraint + let hash_sub huc s = + Constraint.fold (fun x -> Constraint.add (huc x)) s Constraint.empty + let equal s s' = + list_for_all2eq (==) + (Constraint.elements s) + (Constraint.elements s') + let hash = Hashtbl.hash + end) + +let hcons_constraint = Hashcons.simple_hcons Hconstraint.f hcons_univlevel +let hcons_constraints = Hashcons.simple_hcons Hconstraints.f hcons_constraint diff --git a/kernel/univ.mli b/kernel/univ.mli index 0dfa4a5e3..a55775372 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -105,3 +105,4 @@ val dump_universes : val hcons_univlevel : universe_level -> universe_level val hcons_univ : universe -> universe +val hcons_constraints : constraints -> constraints |