From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- kernel/declareops.ml | 320 +++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 320 insertions(+) create mode 100644 kernel/declareops.ml (limited to 'kernel/declareops.ml') diff --git a/kernel/declareops.ml b/kernel/declareops.ml new file mode 100644 index 00000000..48a6098e --- /dev/null +++ b/kernel/declareops.ml @@ -0,0 +1,320 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* + let x' = f sub x in + if x' == x then ar + else RegularArity x' + | TemplateArity x -> + let x' = g sub x in + if x' == x then ar + else TemplateArity x' + +let map_decl_arity f g = function + | RegularArity a -> RegularArity (f a) + | TemplateArity a -> TemplateArity (g a) + +let hcons_template_arity ar = + { template_param_levels = ar.template_param_levels; + (* List.smartmap (Option.smartmap Univ.hcons_univ_level) ar.template_param_levels; *) + template_level = Univ.hcons_univ ar.template_level } + +(** {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_has_body cb = match cb.const_body with + | Undef _ -> false + | Def _ | OpaqueDef _ -> true + +let is_opaque cb = match cb.const_body with + | OpaqueDef _ -> true + | Undef _ | Def _ -> false + +(** {7 Constant substitutions } *) + +let subst_rel_declaration sub (id,copt,t as x) = + let copt' = Option.smartmap (subst_mps sub) copt in + let t' = subst_mps sub t in + if copt == copt' && t == t' then x else (id,copt',t') + +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 + +(** No need here to check for physical equality after substitution, + at least for Def due to the delayed substitution [subst_constr_subst]. *) +let subst_const_def sub def = match def with + | Undef _ -> def + | Def c -> Def (subst_constr sub c) + | OpaqueDef o -> OpaqueDef (Opaqueproof.subst_opaque sub o) + +let subst_const_proj sub pb = + { pb with proj_ind = subst_mind sub pb.proj_ind; + proj_type = subst_mps sub pb.proj_type; + proj_body = subst_const_type sub pb.proj_body } + +let subst_const_body sub cb = + assert (List.is_empty cb.const_hyps); (* we're outside sections *) + 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 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 + else + { const_hyps = []; + const_body = body'; + const_type = type'; + const_proj = proj'; + const_body_code = + 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 } + +(** {7 Hash-consing of constants } *) + +(** This hash-consing is currently quite partial : we only + share internal fields (e.g. constr), and not the records + themselves. But would it really bring substantial gains ? *) + +let hcons_rel_decl ((n,oc,t) as d) = + let n' = Names.Name.hcons n + and oc' = Option.smartmap Term.hcons_constr oc + and t' = Term.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_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)) + | OpaqueDef _ as x -> x (* hashconsed when turned indirect *) + +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 } + +(** {6 Inductive types } *) + +let eq_recarg r1 r2 = match r1, r2 with +| Norec, Norec -> true +| Mrec i1, Mrec i2 -> Names.eq_ind i1 i2 +| Imbr i1, Imbr i2 -> Names.eq_ind i1 i2 +| _ -> false + +let subst_recarg sub r = match r with + | Norec -> r + | Mrec (kn,i) -> + let kn' = subst_mind sub kn in + if kn==kn' then r else Mrec (kn',i) + | Imbr (kn,i) -> + let kn' = subst_mind sub kn in + if kn==kn' then r else Imbr (kn',i) + +let mk_norec = Rtree.mk_node Norec [||] + +let mk_paths r recargs = + Rtree.mk_node r + (Array.map (fun l -> Rtree.mk_node Norec (Array.of_list l)) recargs) + +let dest_recarg p = fst (Rtree.dest_node p) + +(* dest_subterms returns the sizes of each argument of each constructor of + an inductive object of size [p]. This should never be done for Norec, + because the number of sons does not correspond to the number of + constructors. + *) +let dest_subterms p = + let (ra,cstrs) = Rtree.dest_node p in + assert (match ra with Norec -> false | _ -> true); + Array.map (fun t -> Array.to_list (snd (Rtree.dest_node t))) cstrs + +let recarg_length p j = + let (_,cstrs) = Rtree.dest_node p in + Array.length (snd (Rtree.dest_node cstrs.(j-1))) + +let subst_wf_paths sub p = Rtree.smartmap (subst_recarg sub) p + +(** {7 Substitution of inductive declarations } *) + +let subst_regular_ind_arity sub s = + let uar' = subst_mps sub s.mind_user_arity in + if uar' == s.mind_user_arity then s + else { mind_user_arity = uar'; mind_sort = s.mind_sort } + +let subst_template_ind_arity sub s = s + +(* FIXME records *) +let subst_ind_arity = + subst_decl_arity subst_regular_ind_arity subst_template_ind_arity + +let subst_mind_packet sub mbp = + { mind_consnames = mbp.mind_consnames; + mind_consnrealdecls = mbp.mind_consnrealdecls; + mind_consnrealargs = mbp.mind_consnrealargs; + 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_ind_arity sub mbp.mind_arity; + mind_user_lc = Array.smartmap (subst_mps sub) mbp.mind_user_lc; + mind_nrealargs = mbp.mind_nrealargs; + mind_nrealdecls = mbp.mind_nrealdecls; + mind_kelim = mbp.mind_kelim; + mind_recargs = subst_wf_paths sub mbp.mind_recargs (*wf_paths*); + mind_nb_constant = mbp.mind_nb_constant; + mind_nb_args = mbp.mind_nb_args; + mind_reloc_tbl = mbp.mind_reloc_tbl } + +let subst_mind_record sub (id, ps, pb as r) = + let ps' = Array.smartmap (subst_constant sub) ps in + let pb' = Array.smartmap (subst_const_proj sub) pb in + if ps' == ps && pb' == pb then r + else (id, ps', pb') + +let subst_mind_body sub mib = + { mind_record = Option.smartmap (Option.smartmap (subst_mind_record sub)) mib.mind_record ; + mind_finite = mib.mind_finite ; + mind_ntypes = mib.mind_ntypes ; + mind_hyps = (match mib.mind_hyps with [] -> [] | _ -> assert false); + mind_nparams = mib.mind_nparams; + mind_nparams_rec = mib.mind_nparams_rec; + mind_params_ctxt = + Context.map_rel_context (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 } + +let inductive_instance mib = + if mib.mind_polymorphic then + Univ.UContext.instance mib.mind_universes + else Univ.Instance.empty + +let inductive_context mib = + if mib.mind_polymorphic then + Univ.instantiate_univ_context mib.mind_universes + else Univ.UContext.empty + +(** {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 } + +(** Just as for constants, this hash-consing is quite partial *) + +let hcons_ind_arity = + map_decl_arity hcons_regular_ind_arity hcons_template_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 + (* 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 + mind_typename = Names.Id.hcons oib.mind_typename; + mind_arity_ctxt = hcons_rel_context oib.mind_arity_ctxt; + mind_arity = hcons_ind_arity oib.mind_arity; + mind_consnames = Array.smartmap Names.Id.hcons oib.mind_consnames; + mind_user_lc = user; + mind_nf_lc = nf } + +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 } + +(** {6 Stm machinery } *) + +let string_of_side_effect = function + | SEsubproof (c,_,_) -> Names.string_of_con c + | SEscheme (cl,_) -> + String.concat ", " (List.map (fun (_,c,_,_) -> Names.string_of_con c) cl) +type side_effects = side_effect list +let no_seff = ([] : side_effects) +let iter_side_effects f l = List.iter f (List.rev l) +let fold_side_effects f a l = List.fold_left f a l +let uniquize_side_effects l = List.rev (CList.uniquize (List.rev l)) +let union_side_effects l1 l2 = l1 @ l2 +let flatten_side_effects l = List.flatten l +let side_effects_of_list l = l +let cons_side_effects x l = x :: l +let side_effects_is_empty = List.is_empty -- cgit v1.2.3