diff options
Diffstat (limited to 'pretyping/inductiveops.mli')
| -rw-r--r-- | pretyping/inductiveops.mli | 35 |
1 files changed, 24 insertions, 11 deletions
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index 7cd2ff2a..7bd61659 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -8,7 +8,6 @@ open Names open Term -open Context open Declarations open Environ open Evd @@ -92,12 +91,12 @@ val inductive_nparamdecls : inductive -> int val inductive_nparamdecls_env : env -> inductive -> int (** @return params context *) -val inductive_paramdecls : pinductive -> rel_context -val inductive_paramdecls_env : env -> pinductive -> rel_context +val inductive_paramdecls : pinductive -> Context.Rel.t +val inductive_paramdecls_env : env -> pinductive -> Context.Rel.t (** @return full arity context, hence with letin *) -val inductive_alldecls : pinductive -> rel_context -val inductive_alldecls_env : env -> pinductive -> rel_context +val inductive_alldecls : pinductive -> Context.Rel.t +val inductive_alldecls_env : env -> pinductive -> Context.Rel.t (** {7 Extract information from a constructor name} *) @@ -123,19 +122,24 @@ val inductive_has_local_defs : inductive -> bool val allowed_sorts : env -> inductive -> sorts_family list +(** (Co)Inductive records with primitive projections do not have eta-conversion, + hence no dependent elimination. *) +val has_dependent_elim : mutual_inductive_body -> bool + (** Primitive projections *) val projection_nparams : projection -> int val projection_nparams_env : env -> projection -> int val type_of_projection_knowing_arg : env -> evar_map -> Projection.t -> - constr -> types -> types + constr -> types -> types + (** Extract information from an inductive family *) type constructor_summary = { cs_cstr : pconstructor; (* internal name of the constructor plus universes *) - cs_params : constr list; (* parameters of the constructor in current ctx *) - cs_nargs : int; (* length of arguments signature (letin included) *) - cs_args : rel_context; (* signature of the arguments (letin included) *) + cs_params : constr list; (* parameters of the constructor in current ctx *) + cs_nargs : int; (* length of arguments signature (letin included) *) + cs_args : Context.Rel.t; (* signature of the arguments (letin included) *) cs_concl_realargs : constr array; (* actual realargs in the concl of cstr *) } val lift_constructor : int -> constructor_summary -> constructor_summary @@ -148,17 +152,18 @@ val get_projections : env -> inductive_family -> constant array option (** [get_arity] returns the arity of the inductive family instantiated with the parameters; if recursively non-uniform parameters are not part of the inductive family, they appears in the arity *) -val get_arity : env -> inductive_family -> rel_context * sorts_family +val get_arity : env -> inductive_family -> Context.Rel.t * sorts_family val build_dependent_constructor : constructor_summary -> constr val build_dependent_inductive : env -> inductive_family -> constr -val make_arity_signature : env -> bool -> inductive_family -> rel_context +val make_arity_signature : env -> bool -> inductive_family -> Context.Rel.t val make_arity : env -> bool -> inductive_family -> sorts -> types val build_branch_type : env -> bool -> constr -> constructor_summary -> types (** Raise [Not_found] if not given a valid inductive type *) val extract_mrectype : constr -> pinductive * constr list val find_mrectype : env -> evar_map -> types -> pinductive * constr list +val find_mrectype_vect : env -> evar_map -> types -> pinductive * constr array val find_rectype : env -> evar_map -> types -> inductive_type val find_inductive : env -> evar_map -> types -> pinductive * constr list val find_coinductive : env -> evar_map -> types -> pinductive * constr list @@ -175,6 +180,14 @@ val type_case_branches_with_names : (** Annotation for cases *) val make_case_info : env -> inductive -> case_style -> case_info +(** Make a case or substitute projections if the inductive type is a record + with primitive projections. + Fail with an error if the elimination is dependent while the + inductive type does not allow dependent elimination. *) +val make_case_or_project : + env -> inductive_family -> case_info -> + (* pred *) constr -> (* term *) constr -> (* branches *) constr array -> constr + (*i Compatibility val make_default_case_info : env -> case_style -> inductive -> case_info i*) |