diff options
Diffstat (limited to 'kernel/declareops.ml')
| -rw-r--r-- | kernel/declareops.ml | 40 |
1 files changed, 24 insertions, 16 deletions
diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 85dd1e66db..d8768a0fc5 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -112,7 +112,7 @@ let subst_const_body sub cb = themselves. But would it really bring substantial gains ? *) let hcons_rel_decl = - RelDecl.map_name Names.Name.hcons %> RelDecl.map_value Term.hcons_constr %> RelDecl.map_type Term.hcons_types + RelDecl.map_name Names.Name.hcons %> RelDecl.map_value Constr.hcons %> RelDecl.map_type Constr.hcons let hcons_rel_context l = List.smartmap hcons_rel_decl l @@ -120,20 +120,20 @@ let hcons_const_def = function | Undef inl -> Undef inl | Def l_constr -> let constr = force_constr l_constr in - Def (from_val (Term.hcons_constr constr)) + Def (from_val (Constr.hcons constr)) | OpaqueDef _ as x -> x (* hashconsed when turned indirect *) let hcons_const_universes cbu = match cbu with | Monomorphic_const ctx -> - Monomorphic_const (Univ.hcons_universe_context ctx) + Monomorphic_const (Univ.hcons_universe_context_set ctx) | Polymorphic_const ctx -> Polymorphic_const (Univ.hcons_abstract_universe_context ctx) let hcons_const_body cb = { cb with const_body = hcons_const_def cb.const_body; - const_type = Term.hcons_constr cb.const_type; + const_type = Constr.hcons cb.const_type; const_universes = hcons_const_universes cb.const_universes } (** {6 Inductive types } *) @@ -249,8 +249,8 @@ let inductive_is_cumulative mib = (** {6 Hash-consing of inductive declarations } *) let hcons_regular_ind_arity a = - { mind_user_arity = Term.hcons_constr a.mind_user_arity; - mind_sort = Term.hcons_sorts a.mind_sort } + { mind_user_arity = Constr.hcons a.mind_user_arity; + mind_sort = Sorts.hcons a.mind_sort } (** Just as for constants, this hash-consing is quite partial *) @@ -260,8 +260,8 @@ let hcons_ind_arity = (** Substitution of inductive declarations *) let hcons_mind_packet oib = - let user = Array.smartmap Term.hcons_types oib.mind_user_lc in - let nf = Array.smartmap Term.hcons_types oib.mind_nf_lc in + let user = Array.smartmap Constr.hcons oib.mind_user_lc in + let nf = Array.smartmap Constr.hcons oib.mind_nf_lc in (* Special optim : merge [mind_user_lc] and [mind_nf_lc] if possible *) let nf = if Array.equal (==) user nf then user else nf in { oib with @@ -274,7 +274,7 @@ let hcons_mind_packet oib = let hcons_mind_universes miu = match miu with - | Monomorphic_ind ctx -> Monomorphic_ind (Univ.hcons_universe_context ctx) + | Monomorphic_ind ctx -> Monomorphic_ind (Univ.hcons_universe_context_set ctx) | Polymorphic_ind ctx -> Polymorphic_ind (Univ.hcons_abstract_universe_context ctx) | Cumulative_ind cui -> Cumulative_ind (Univ.hcons_abstract_cumulativity_info cui) @@ -287,9 +287,9 @@ let hcons_mind mib = (** {6 Stm machinery } *) let string_of_side_effect { Entries.eff } = match eff with - | Entries.SEsubproof (c,_,_) -> "P(" ^ Names.string_of_con c ^ ")" + | Entries.SEsubproof (c,_,_) -> "P(" ^ Names.Constant.to_string c ^ ")" | Entries.SEscheme (cl,_) -> - "S(" ^ String.concat ", " (List.map (fun (_,c,_,_) -> Names.string_of_con c) cl) ^ ")" + "S(" ^ String.concat ", " (List.map (fun (_,c,_,_) -> Names.Constant.to_string c) cl) ^ ")" (** Hashconsing of modules *) @@ -318,7 +318,7 @@ let rec hcons_structure_field_body sb = match sb with let mb' = hcons_module_body mb in if mb == mb' then sb else SFBmodule mb' | SFBmodtype mb -> - let mb' = hcons_module_body mb in + let mb' = hcons_module_type mb in if mb == mb' then sb else SFBmodtype mb' and hcons_structure_body sb = @@ -331,10 +331,10 @@ and hcons_structure_body sb = List.smartmap map sb and hcons_module_signature ms = - hcons_functorize hcons_module_body hcons_structure_body hcons_module_signature ms + hcons_functorize hcons_module_type hcons_structure_body hcons_module_signature ms and hcons_module_expression me = - hcons_functorize hcons_module_body hcons_module_alg_expr hcons_module_expression me + hcons_functorize hcons_module_type hcons_module_alg_expr hcons_module_expression me and hcons_module_implementation mip = match mip with | Abstract -> Abstract @@ -346,9 +346,11 @@ and hcons_module_implementation mip = match mip with if ms == ms' then mip else Struct ms | FullStruct -> FullStruct -and hcons_module_body mb = +and hcons_generic_module_body : + 'a. ('a -> 'a) -> 'a generic_module_body -> 'a generic_module_body = + fun hcons_impl mb -> let mp' = mb.mod_mp in - let expr' = hcons_module_implementation mb.mod_expr in + let expr' = hcons_impl mb.mod_expr in let type' = hcons_module_signature mb.mod_type in let type_alg' = mb.mod_type_alg in let constraints' = Univ.hcons_universe_context_set mb.mod_constraints in @@ -373,3 +375,9 @@ and hcons_module_body mb = mod_delta = delta'; mod_retroknowledge = retroknowledge'; } + +and hcons_module_body mb = + hcons_generic_module_body hcons_module_implementation mb + +and hcons_module_type mb = + hcons_generic_module_body (fun () -> ()) mb |