diff options
Diffstat (limited to 'kernel/declareops.ml')
| -rw-r--r-- | kernel/declareops.ml | 159 |
1 files changed, 74 insertions, 85 deletions
diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 211e5e06..3652a1ce 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -1,22 +1,26 @@ (************************************************************************) -(* 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) *) (************************************************************************) open Declarations open Mod_subst open Util -open Context.Rel.Declaration + +module RelDecl = Context.Rel.Declaration (** Operations concernings types in [Declarations] : [constant_body], [mutual_inductive_body], [module_body] ... *) -let safe_flags = { +let safe_flags oracle = { check_guarded = true; check_universes = true; + conv_oracle = oracle; } (** {6 Arities } *) @@ -43,50 +47,20 @@ let hcons_template_arity ar = (** {6 Constants } *) -let instantiate cb c = - if cb.const_polymorphic then - Vars.subst_instance_constr (Univ.UContext.instance cb.const_universes) c - else c - -let body_of_constant otab cb = match cb.const_body with - | Undef _ -> None - | Def c -> Some (instantiate cb (force_constr c)) - | OpaqueDef o -> Some (instantiate cb (Opaqueproof.force_proof otab o)) - -let type_of_constant cb = - match cb.const_type with - | RegularArity t as x -> - let t' = instantiate cb t in - if t' == t then x else RegularArity t' - | TemplateArity _ as x -> x - -let constraints_of_constant otab cb = Univ.Constraint.union - (Univ.UContext.constraints cb.const_universes) - (match cb.const_body with - | Undef _ -> Univ.empty_constraint - | Def c -> Univ.empty_constraint - | OpaqueDef o -> - Univ.ContextSet.constraints (Opaqueproof.force_constraints otab o)) - -let universes_of_constant otab cb = - match cb.const_body with - | Undef _ | Def _ -> cb.const_universes - | OpaqueDef o -> - let body_uctxs = Opaqueproof.force_constraints otab o in - assert(not cb.const_polymorphic || Univ.ContextSet.is_empty body_uctxs); - let uctxs = Univ.ContextSet.of_context cb.const_universes in - Univ.ContextSet.to_context (Univ.ContextSet.union body_uctxs uctxs) - -let universes_of_polymorphic_constant otab cb = - if cb.const_polymorphic then - let univs = universes_of_constant otab cb in - Univ.instantiate_univ_context univs - else Univ.UContext.empty +let constant_is_polymorphic cb = + match cb.const_universes with + | Monomorphic_const _ -> false + | Polymorphic_const _ -> true let constant_has_body cb = match cb.const_body with | Undef _ -> false | Def _ | OpaqueDef _ -> true +let constant_polymorphic_context cb = + match cb.const_universes with + | Monomorphic_const _ -> Univ.AUContext.empty + | Polymorphic_const ctx -> ctx + let is_opaque cb = match cb.const_body with | OpaqueDef _ -> true | Undef _ | Def _ -> false @@ -94,14 +68,10 @@ let is_opaque cb = match cb.const_body with (** {7 Constant substitutions } *) let subst_rel_declaration sub = - map_constr (subst_mps sub) + RelDecl.map_constr (subst_mps sub) let subst_rel_context sub = List.smartmap (subst_rel_declaration sub) -let subst_template_cst_arity sub (ctx,s as arity) = - let ctx' = subst_rel_context sub ctx in - if ctx==ctx' then arity else (ctx',s) - let subst_const_type sub arity = if is_empty_subst sub then arity else subst_mps sub arity @@ -123,7 +93,7 @@ let subst_const_body sub cb = if is_empty_subst sub then cb else let body' = subst_const_def sub cb.const_body in - let type' = subst_decl_arity subst_const_type subst_template_cst_arity sub cb.const_type in + let type' = subst_const_type sub cb.const_type in let proj' = Option.smartmap (subst_const_proj sub) cb.const_proj in if body' == cb.const_body && type' == cb.const_type && proj' == cb.const_proj then cb @@ -134,7 +104,6 @@ let subst_const_body sub cb = const_proj = proj'; const_body_code = Option.map (Cemitcodes.subst_to_patch_subst sub) cb.const_body_code; - const_polymorphic = cb.const_polymorphic; const_universes = cb.const_universes; const_inline_code = cb.const_inline_code; const_typing_flags = cb.const_typing_flags } @@ -146,30 +115,29 @@ let subst_const_body sub cb = themselves. But would it really bring substantial gains ? *) let hcons_rel_decl = - map_type Term.hcons_types % map_value Term.hcons_constr % map_name Names.Name.hcons + 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 -let hcons_regular_const_arity t = Term.hcons_constr t - -let hcons_template_const_arity (ctx, ar) = - (hcons_rel_context ctx, hcons_template_arity ar) - -let hcons_const_type = - map_decl_arity hcons_regular_const_arity hcons_template_const_arity - 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_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 = hcons_const_type cb.const_type; - const_universes = Univ.hcons_universe_context cb.const_universes } + const_type = Constr.hcons cb.const_type; + const_universes = hcons_const_universes cb.const_universes } (** {6 Inductive types } *) @@ -258,27 +226,34 @@ let subst_mind_body sub mib = mind_params_ctxt = Context.Rel.map (subst_mps sub) mib.mind_params_ctxt; mind_packets = Array.smartmap (subst_mind_packet sub) mib.mind_packets ; - mind_polymorphic = mib.mind_polymorphic; mind_universes = mib.mind_universes; mind_private = mib.mind_private; mind_typing_flags = mib.mind_typing_flags; } -let inductive_instance mib = - if mib.mind_polymorphic then - Univ.UContext.instance mib.mind_universes - else Univ.Instance.empty +let inductive_polymorphic_context mib = + match mib.mind_universes with + | Monomorphic_ind _ -> Univ.AUContext.empty + | Polymorphic_ind ctx -> ctx + | Cumulative_ind cumi -> Univ.ACumulativityInfo.univ_context cumi + +let inductive_is_polymorphic mib = + match mib.mind_universes with + | Monomorphic_ind _ -> false + | Polymorphic_ind ctx -> true + | Cumulative_ind cumi -> true -let inductive_context mib = - if mib.mind_polymorphic then - Univ.instantiate_univ_context mib.mind_universes - else Univ.UContext.empty +let inductive_is_cumulative mib = + match mib.mind_universes with + | Monomorphic_ind _ -> false + | Polymorphic_ind ctx -> false + | Cumulative_ind cumi -> true (** {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 *) @@ -288,8 +263,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 @@ -300,18 +275,24 @@ let hcons_mind_packet oib = mind_user_lc = user; mind_nf_lc = nf } +let hcons_mind_universes miu = + match miu with + | 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) + 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_universes = Univ.hcons_universe_context mib.mind_universes } + mind_universes = hcons_mind_universes mib.mind_universes } (** {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 *) @@ -340,7 +321,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 = @@ -353,10 +334,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 @@ -368,9 +349,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 @@ -395,3 +378,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 |