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/declarations.ml | 409 ------------------------------------------------- 1 file changed, 409 deletions(-) delete mode 100644 kernel/declarations.ml (limited to 'kernel/declarations.ml') diff --git a/kernel/declarations.ml b/kernel/declarations.ml deleted file mode 100644 index 88d28323..00000000 --- a/kernel/declarations.ml +++ /dev/null @@ -1,409 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* None - | Def c -> Some c - | OpaqueDef lc -> Some (force_lazy_constr lc) - -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 - -(* Substitutions of [constant_body] *) - -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) - -(* 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 - | Imbr of inductive - -let subst_recarg sub r = match r with - | Norec -> r - | Mrec (kn,i) -> let kn' = subst_ind sub kn in - if kn==kn' then r else Mrec (kn',i) - | Imbr (kn,i) -> let kn' = subst_ind sub kn in - if kn==kn' then r else Imbr (kn',i) - -type wf_paths = recarg Rtree.t - -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 (ra<>Norec); - 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 - -(**********************************************************************) -(* Representation of mutual inductive types in the kernel *) -(* - Inductive I1 (params) : U1 := c11 : T11 | ... | c1p1 : T1p1 - ... - with In (params) : Un := cn1 : Tn1 | ... | cnpn : Tnpn -*) - -type monomorphic_inductive_arity = { - mind_user_arity : constr; - mind_sort : sorts; -} - -type inductive_arity = -| Monomorphic of monomorphic_inductive_arity -| Polymorphic of polymorphic_arity - -type one_inductive_body = { - -(* Primitive datas *) - - (* Name of the type: [Ii] *) - mind_typename : identifier; - - (* Arity context of [Ii] with parameters: [forall params, Ui] *) - mind_arity_ctxt : rel_context; - - (* Arity sort, original user arity, and allowed elim sorts, if monomorphic *) - mind_arity : inductive_arity; - - (* Names of the constructors: [cij] *) - mind_consnames : identifier array; - - (* Types of the constructors with parameters: [forall params, Tij], - where the Ik are replaced by de Bruijn index in the context - I1:forall params, U1 .. In:forall params, Un *) - mind_user_lc : types array; - -(* Derived datas *) - - (* Number of expected real arguments of the type (no let, no params) *) - mind_nrealargs : int; - - (* Length of realargs context (with let, no params) *) - mind_nrealargs_ctxt : int; - - (* List of allowed elimination sorts *) - mind_kelim : sorts_family list; - - (* Head normalized constructor types so that their conclusion is atomic *) - mind_nf_lc : types array; - - (* Length of the signature of the constructors (with let, w/o params) *) - mind_consnrealdecls : int array; - - (* Signature of recursive arguments in the constructors *) - mind_recargs : wf_paths; - -(* Datas for bytecode compilation *) - - (* number of constant constructor *) - mind_nb_constant : int; - - (* number of no constant constructor *) - mind_nb_args : int; - - mind_reloc_tbl : Cbytecodes.reloc_table; - } - -type mutual_inductive_body = { - - (* The component of the mutual inductive block *) - mind_packets : one_inductive_body array; - - (* Whether the inductive type has been declared as a record *) - mind_record : bool; - - (* Whether the type is inductive or coinductive *) - mind_finite : bool; - - (* Number of types in the block *) - mind_ntypes : int; - - (* Section hypotheses on which the block depends *) - mind_hyps : section_context; - - (* Number of expected parameters *) - mind_nparams : int; - - (* Number of recursively uniform (i.e. ordinary) parameters *) - mind_nparams_rec : int; - - (* The context of parameters (includes let-in declaration) *) - mind_params_ctxt : rel_context; - - (* Universes constraints enforced by the inductive declaration *) - mind_constraints : constraints; - - } - -let subst_indarity sub = function -| Monomorphic s -> - Monomorphic { - mind_user_arity = subst_mps sub s.mind_user_arity; - mind_sort = s.mind_sort; - } -| Polymorphic s as x -> x - -let subst_mind_packet sub mbp = - { mind_consnames = mbp.mind_consnames; - mind_consnrealdecls = mbp.mind_consnrealdecls; - 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_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; - 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 sub mib = - { mind_record = mib.mind_record ; - mind_finite = mib.mind_finite ; - mind_ntypes = mib.mind_ntypes ; - mind_hyps = (assert (mib.mind_hyps=[]); []) ; - mind_nparams = mib.mind_nparams; - mind_nparams_rec = mib.mind_nparams_rec; - mind_params_ctxt = - map_rel_context (subst_mps sub) mib.mind_params_ctxt; - 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 *) - -type structure_field_body = - | SFBconst of constant_body - | SFBmind of mutual_inductive_body - | SFBmodule of module_body - | SFBmodtype of module_type_body - -and structure_body = (label * structure_field_body) list - -and struct_expr_body = - | SEBident of module_path - | SEBfunctor of mod_bound_id * module_type_body * struct_expr_body - | SEBapply of struct_expr_body * struct_expr_body * constraints - | SEBstruct of structure_body - | SEBwith of struct_expr_body * with_declaration_body - -and with_declaration_body = - With_module_body of identifier list * module_path - | With_definition_body of identifier list * constant_body - -and module_body = - { mod_mp : module_path; - mod_expr : struct_expr_body option; - mod_type : struct_expr_body; - mod_type_alg : struct_expr_body option; - mod_constraints : constraints; - mod_delta : delta_resolver; - mod_retroknowledge : Retroknowledge.action list} - -and module_type_body = - { typ_mp : module_path; - typ_expr : struct_expr_body; - typ_expr_alg : struct_expr_body option ; - typ_constraints : constraints; - typ_delta :delta_resolver} -- cgit v1.2.3