aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--kernel/closure.ml2
-rw-r--r--kernel/environ.ml8
-rw-r--r--kernel/environ.mli2
-rw-r--r--kernel/indtypes.ml2
-rw-r--r--kernel/indtypes.mli2
-rw-r--r--kernel/inductive.ml115
-rw-r--r--kernel/inductive.mli157
-rw-r--r--kernel/instantiate.ml2
-rw-r--r--kernel/reduction.ml2
-rw-r--r--kernel/safe_typing.ml2
-rw-r--r--kernel/safe_typing.mli4
-rw-r--r--kernel/typeops.ml66
-rw-r--r--library/declare.ml5
-rw-r--r--library/declare.mli2
-rw-r--r--library/global.mli4
-rw-r--r--library/impargs.ml2
-rw-r--r--library/indrec.ml127
-rw-r--r--library/indrec.mli12
-rw-r--r--library/redinfo.ml2
-rw-r--r--parsing/pretty.ml2
-rw-r--r--parsing/pretty.mli5
-rw-r--r--pretyping/cases.ml20
-rw-r--r--pretyping/class.ml2
-rw-r--r--pretyping/detyping.ml4
-rw-r--r--proofs/pfedit.ml2
-rw-r--r--toplevel/command.ml17
-rw-r--r--toplevel/discharge.ml2
-rw-r--r--toplevel/minicoq.ml2
-rw-r--r--toplevel/record.ml5
29 files changed, 230 insertions, 349 deletions
diff --git a/kernel/closure.ml b/kernel/closure.ml
index e7b1a634f..f452a6dfc 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -309,7 +309,7 @@ let fixp_reducible redfun flgs op stk =
false
let mindsp_nparams env sp =
- let mib = lookup_mind sp env in mib.Constant.mind_nparams
+ let mib = lookup_mind sp env in mib.Declarations.mind_nparams
(* The main recursive functions
*
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 16284de7b..4f9d4e957 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -8,7 +8,7 @@ open Sign
open Univ
open Generic
open Term
-open Constant
+open Declarations
open Abstraction
(* The type of environments. *)
@@ -212,13 +212,11 @@ let abst_value env = function
| _ -> invalid_arg "abst_value"
let defined_constant env = function
- | DOPN (Const sp, _) ->
- Constant.is_defined (lookup_constant sp env)
+ | DOPN (Const sp, _) -> is_defined (lookup_constant sp env)
| _ -> invalid_arg "defined_constant"
let opaque_constant env = function
- | DOPN (Const sp, _) ->
- Constant.is_opaque (lookup_constant sp env)
+ | DOPN (Const sp, _) -> is_opaque (lookup_constant sp env)
| _ -> invalid_arg "opaque_constant"
(* A const is evaluable if it is defined and not opaque *)
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 720ff16dc..8f73b9779 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -4,7 +4,7 @@
(*i*)
open Names
open Term
-open Constant
+open Declarations
open Abstraction
open Univ
open Sign
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 9335a63b7..ea8b77570 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -5,7 +5,7 @@ open Util
open Names
open Generic
open Term
-open Constant
+open Declarations
open Inductive
open Sign
open Environ
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index 505ea1d95..e73d5779a 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -5,7 +5,7 @@
open Names
open Univ
open Term
-open Constant
+open Declarations
open Environ
(*i*)
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 823e4e612..4a7649a79 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -7,11 +7,11 @@ open Univ
open Generic
open Term
open Sign
-open Constant
+open Declarations
open Environ
open Reduction
-type mind_specif = {
+type inductive_instance = {
mis_sp : section_path;
mis_mib : mutual_inductive_body;
mis_tyi : int;
@@ -19,9 +19,11 @@ type mind_specif = {
mis_mip : mutual_inductive_packet }
let mis_ntypes mis = mis.mis_mib.mind_ntypes
+let mis_nparams mis = mis.mis_mib.mind_nparams
+
let mis_index mis = mis.mis_tyi
+
let mis_nconstr mis = Array.length (mis.mis_mip.mind_consnames)
-let mis_nparams mis = mis.mis_mib.mind_nparams
let mis_nrealargs mis = mis.mis_mip.mind_nrealargs
let mis_kelim mis = mis.mis_mip.mind_kelim
let mis_recargs mis =
@@ -46,16 +48,29 @@ let mis_lc_without_abstractions mis =
in
strip_DLAM (mis_lc mis)
+(* gives the vector of constructors and of
+ types of constructors of an inductive definition
+ correctly instanciated *)
+
let mis_type_mconstructs mispec =
let specif = mis_lc mispec
and ntypes = mis_ntypes mispec
and nconstr = mis_nconstr mispec in
let make_Ik k = mkMutInd ((mispec.mis_sp,k),mispec.mis_args)
- and make_Ck k = mkMutConstruct (((mispec.mis_sp,mispec.mis_tyi),k+1),
+ and make_Ck k = mkMutConstruct
+ (((mispec.mis_sp,mispec.mis_tyi),k+1),
mispec.mis_args) in
(Array.init nconstr make_Ck,
sAPPVList specif (list_tabulate make_Ik ntypes))
+let mis_type_mconstruct i mispec =
+ let specif = mis_lc mispec
+ and ntypes = mis_ntypes mispec
+ and nconstr = mis_nconstr mispec in
+ let make_Ik k = DOPN(MutInd(mispec.mis_sp,k),mispec.mis_args) in
+ if i > nconstr then error "Not enough constructors in the type";
+ sAPPViList (i-1) specif (list_tabulate make_Ik ntypes)
+
let mis_typed_arity mis =
let idhyps = ids_of_sign mis.mis_mib.mind_hyps
and largs = Array.to_list mis.mis_args in
@@ -81,33 +96,16 @@ let liftn_inductive_instance n depth mis = {
let lift_inductive_instance n = liftn_inductive_instance n 1
-
-type constructor_summary = {
- cs_cstr : constructor;
- cs_params : constr list;
- cs_nargs : int;
- cs_args : (name * constr) list;
- cs_concl_realargs : constr array
-}
-
-let lift_constructor n cs = {
- cs_cstr = (let (csp,ctxt) = cs.cs_cstr in (csp,Array.map (lift n) ctxt));
- cs_params = List.map (lift n) cs.cs_params;
- cs_nargs = cs.cs_nargs;
- cs_args = lift_context n cs.cs_args;
- cs_concl_realargs = Array.map (liftn n (cs.cs_nargs+1)) cs.cs_concl_realargs
+let substn_many_ind_instance cv depth mis = {
+ mis_sp = mis.mis_sp;
+ mis_mib = mis.mis_mib;
+ mis_tyi = mis.mis_tyi;
+ mis_args = Array.map (substn_many cv depth) mis.mis_args;
+ mis_mip = mis.mis_mip
}
(* [inductive_family] = [inductive_instance] applied to global parameters *)
-type inductive_family = IndFamily of mind_specif * constr list
-(* = {
- mind : inductive;
- params : constr list;
- nparams : int;
- nrealargs : int;
- nconstr : int;
- ind_kelim : sorts list;
-} *)
+type inductive_family = IndFamily of inductive_instance * constr list
type inductive_type = IndType of inductive_family * constr list
@@ -119,6 +117,14 @@ let liftn_inductive_type n d (IndType (indf, realargs)) =
IndType (liftn_inductive_family n d indf, List.map (liftn n d) realargs)
let lift_inductive_type n = liftn_inductive_type n 1
+let substn_many_ind_family cv depth (IndFamily (mis,params)) =
+ IndFamily (substn_many_ind_instance cv depth mis,
+ List.map (substn_many cv depth) params)
+
+let substn_many_ind_type cv depth (IndType (indf,realargs)) =
+ IndType (substn_many_ind_family cv depth indf,
+ List.map (substn_many cv depth) realargs)
+
let make_ind_family (mis, params) = IndFamily (mis,params)
let dest_ind_family (IndFamily (mis,params)) = (mis,params)
@@ -160,25 +166,21 @@ let inductive_path_of_constructor_path (ind_sp,i) = ind_sp
let ith_constructor_path_of_inductive_path ind_sp i = (ind_sp,i)
let inductive_of_constructor ((ind_sp,i),args) = (ind_sp,args)
+let index_of_constructor ((ind_sp,i),args) = i
let ith_constructor_of_inductive (ind_sp,args) i = ((ind_sp,i),args)
-let build_dependent_constructor cs =
- applist
- (mkMutConstruct cs.cs_cstr,
- (List.map (lift cs.cs_nargs) cs.cs_params)@(rel_list 0 cs.cs_nargs))
-
-let build_dependent_inductive (IndFamily (mis, params)) =
- let nrealargs = mis_nrealargs mis in
- applist
- (mkMutInd (mis_inductive mis),
- (List.map (lift nrealargs) params)@(rel_list 0 nrealargs))
-
exception Induc
+let extract_mrectype env sigma t =
+ let (t,l) = whd_stack env sigma t [] in
+ match t with
+ | DOPN(MutInd ind_sp,args) -> ((ind_sp,args),l)
+ | _ -> raise Induc
+
let find_mrectype env sigma c =
let (t,l) = whd_betadeltaiota_stack env sigma c [] in
match t with
- | DOPN(MutInd ind_sp,args) -> ((ind_sp,args),l)
+ | DOPN(MutInd ind_sp,args) -> ((ind_sp,args),l)
| _ -> raise Induc
let find_minductype env sigma c =
@@ -208,10 +210,24 @@ let find_inductive env sigma ty =
let (params,realargs) = list_chop nparams largs in
make_ind_type (make_ind_family (mispec,params),realargs)
+type constructor_summary = {
+ cs_cstr : constructor;
+ cs_params : constr list;
+ cs_nargs : int;
+ cs_args : (name * constr) list;
+ cs_concl_realargs : constr array
+}
+
+let lift_constructor n cs = {
+ cs_cstr = (let (csp,ctxt) = cs.cs_cstr in (csp,Array.map (lift n) ctxt));
+ cs_params = List.map (lift n) cs.cs_params;
+ cs_nargs = cs.cs_nargs;
+ cs_args = lift_context n cs.cs_args;
+ cs_concl_realargs = Array.map (liftn n (cs.cs_nargs+1)) cs.cs_concl_realargs
+}
+
let get_constructors (IndFamily (mispec,params)) =
- let specif = mis_lc mispec in
- let make_ik i = DOPN (MutInd (mispec.mis_sp,i), mispec.mis_args) in
- let types = sAPPVList specif (list_tabulate make_ik (mis_ntypes mispec)) in
+ let _,types = mis_type_mconstructs mispec in
let make_ck j =
let (args,ccl) = decompose_prod (prod_applist types.(j) params) in
let (_,vargs) = array_chop (mis_nparams mispec + 1) (destAppL (ensure_appl ccl)) in
@@ -226,6 +242,19 @@ let get_arity env sigma (IndFamily (mispec,params)) =
let arity = mis_arity mispec in
splay_arity env sigma (prod_applist arity params)
+(* Functions to build standard types related to inductive *)
+
+let build_dependent_constructor cs =
+ applist
+ (mkMutConstruct cs.cs_cstr,
+ (List.map (lift cs.cs_nargs) cs.cs_params)@(rel_list 0 cs.cs_nargs))
+
+let build_dependent_inductive (IndFamily (mis, params)) =
+ let nrealargs = mis_nrealargs mis in
+ applist
+ (mkMutInd (mis_inductive mis),
+ (List.map (lift nrealargs) params)@(rel_list 0 nrealargs))
+
(* builds the arity of an elimination predicate in sort [s] *)
let make_arity env sigma dep indf s =
let (arsign,_) = get_arity env sigma indf in
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index 51ea86f30..b7501dd64 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -6,44 +6,83 @@ open Names
open Univ
open Term
open Sign
-open Constant
+open Declarations
open Environ
open Evd
(*i*)
-(*s To give a more efficient access to the informations related to a given
- inductive type, we introduce the following type [mind_specif], which
- contains all the informations about the inductive type, including its
- instanciation arguments. *)
-
-type mind_specif = {
- mis_sp : section_path;
- mis_mib : mutual_inductive_body;
- mis_tyi : int;
- mis_args : constr array;
- mis_mip : mutual_inductive_packet }
-
-val mis_index : mind_specif -> int
-val mis_ntypes : mind_specif -> int
-val mis_nconstr : mind_specif -> int
-val mis_nparams : mind_specif -> int
-val mis_nrealargs : mind_specif -> int
-val mis_kelim : mind_specif -> sorts list
-val mis_recargs : mind_specif -> (recarg list) array array
-val mis_recarg : mind_specif -> (recarg list) array
-val mis_typename : mind_specif -> identifier
-val mis_typepath : mind_specif -> section_path
-val mis_is_recursive_subset : int list -> mind_specif -> bool
-val mis_is_recursive : mind_specif -> bool
-val mis_consnames : mind_specif -> identifier array
-val mis_typed_arity : mind_specif -> typed_type
-val mis_inductive : mind_specif -> inductive
-val mis_arity : mind_specif -> constr
-val mis_lc : mind_specif -> constr
-val mis_lc_without_abstractions : mind_specif -> constr array
-val mis_type_mconstructs : mind_specif -> constr array * constr array
-val mis_params_ctxt : mind_specif -> (name * constr) list
-val mis_sort : mind_specif -> sorts
+(*s Inductives are accessible at several stages:
+
+A [mutual_inductive_body] contains all information about a
+declaration of mutual (co-)inductive types. These informations are
+closed (they depend on no free variables) and an instance of them
+corresponds to a [mutual_inductive_instance =
+mutual_inductive_body * constr list]. One inductive type in an
+instanciated packet corresponds to an [inductive_instance =
+mutual_inductive_instance * int]. Applying global parameters to an
+inductive_instance gives an [inductive_family = inductive_instance *
+constr list]. Finally, applying real parameters gives an
+[inductive_type = inductive_family * constr list]. At each level
+corresponds various appropriated functions *)
+
+type inductive_instance (* ex-mind_specif *)
+
+val mis_index : inductive_instance -> int
+val mis_ntypes : inductive_instance -> int
+val mis_nconstr : inductive_instance -> int
+val mis_nparams : inductive_instance -> int
+val mis_nrealargs : inductive_instance -> int
+val mis_kelim : inductive_instance -> sorts list
+val mis_recargs : inductive_instance -> (recarg list) array array
+val mis_recarg : inductive_instance -> (recarg list) array
+val mis_typename : inductive_instance -> identifier
+val mis_typepath : inductive_instance -> section_path
+val mis_is_recursive_subset : int list -> inductive_instance -> bool
+val mis_is_recursive : inductive_instance -> bool
+val mis_consnames : inductive_instance -> identifier array
+val mis_typed_arity : inductive_instance -> typed_type
+val mis_inductive : inductive_instance -> inductive
+val mis_arity : inductive_instance -> constr
+val mis_lc : inductive_instance -> constr
+val mis_lc_without_abstractions : inductive_instance -> constr array
+val mis_type_mconstructs : inductive_instance -> constr array * constr array
+val mis_type_mconstruct : int -> inductive_instance -> constr
+val mis_params_ctxt : inductive_instance -> (name * constr) list
+val mis_sort : inductive_instance -> sorts
+
+(*s [inductive_family] = [inductive_instance] applied to global parameters *)
+type inductive_family = IndFamily of inductive_instance * constr list
+
+val make_ind_family : inductive_instance * constr list -> inductive_family
+val dest_ind_family : inductive_family -> inductive_instance * constr list
+
+val liftn_inductive_family : int -> int -> inductive_family -> inductive_family
+val lift_inductive_family : int -> inductive_family -> inductive_family
+val substn_many_ind_family : constr Generic.substituend array -> int
+ -> inductive_family -> inductive_family
+
+(*s [inductive_type] = [inductive_family] applied to ``real'' parameters *)
+type inductive_type = IndType of inductive_family * constr list
+
+val make_ind_type : inductive_family * constr list -> inductive_type
+val dest_ind_type : inductive_type -> inductive_family * constr list
+
+val mkAppliedInd : inductive_type -> constr
+
+val liftn_inductive_type : int -> int -> inductive_type -> inductive_type
+val lift_inductive_type : int -> inductive_type -> inductive_type
+val substn_many_ind_type : constr Generic.substituend array -> int
+ -> inductive_type -> inductive_type
+
+(*s A [constructor] is an [inductive] + an index; the following functions
+ destructs and builds [constructor] *)
+val inductive_of_constructor : constructor -> inductive
+val index_of_constructor : constructor -> int
+val ith_constructor_of_inductive : inductive -> int -> constructor
+
+val inductive_path_of_constructor_path : constructor_path -> inductive_path
+val ith_constructor_path_of_inductive_path :
+ inductive_path -> int -> constructor_path
(*s This type gathers useful informations about some instance of a constructor
relatively to some implicit context (the current one)
@@ -65,42 +104,7 @@ type constructor_summary = {
val lift_constructor : int -> constructor_summary -> constructor_summary
-(*s A variant of [mind_specif_of_mind] with pre-splitted args
-
- We recover the inductive type as \par
- [DOPN(AppL,[|MutInd mind;..params..;..realargs..|])] \par
- with [mind] = [((sp,i),localvars)] for some [sp, i, localvars].
-
- *)
-
-(* [inductive_family] = [inductive_instance] applied to global parameters *)
-type inductive_family = IndFamily of mind_specif * constr list
-
-val make_ind_family : mind_specif * constr list -> inductive_family
-val dest_ind_family : inductive_family -> mind_specif * constr list
-
-(* [inductive_type] = [inductive_family] applied to ``real'' parameters *)
-type inductive_type = IndType of inductive_family * constr list
-
-val make_ind_type : inductive_family * constr list -> inductive_type
-val dest_ind_type : inductive_type -> inductive_family * constr list
-
-val mkAppliedInd : inductive_type -> constr
-
-val liftn_inductive_family : int -> int -> inductive_family -> inductive_family
-val lift_inductive_family : int -> inductive_family -> inductive_family
-
-val liftn_inductive_type : int -> int -> inductive_type -> inductive_type
-val lift_inductive_type : int -> inductive_type -> inductive_type
-
-val inductive_of_constructor : constructor -> inductive
-
-val ith_constructor_of_inductive : inductive -> int -> constructor
-
-val inductive_path_of_constructor_path : constructor_path -> inductive_path
-
-val ith_constructor_path_of_inductive_path :
- inductive_path -> int -> constructor_path
+(*s Functions to build standard types related to inductive *)
(* This builds [(ci params (Rel 1)...(Rel ci_nargs))] which is the argument
of a dependent predicate in a Cases branch *)
@@ -123,7 +127,8 @@ val make_arity : env -> 'a evar_map -> bool -> inductive_family ->
[p]; if [dep=true], the predicate is assumed dependent *)
val build_branch_type : env -> bool -> constr -> constructor_summary -> constr
-(* [find_m*type env sigma c] coerce [c] to an recursive type (I args).
+
+(*s [find_m*type env sigma c] coerce [c] to an recursive type (I args).
[find_mrectype], [find_minductype] and [find_mcoinductype]
respectively accepts any recursive type, only an inductive type and
only a coinductive type.
@@ -133,8 +138,9 @@ exception Induc
val find_mrectype : env -> 'a evar_map -> constr -> inductive * constr list
val find_minductype : env -> 'a evar_map -> constr -> inductive * constr list
val find_mcoinductype : env -> 'a evar_map -> constr -> inductive * constr list
+val extract_mrectype : env -> 'a evar_map -> constr -> inductive * constr list
-val lookup_mind_specif : inductive -> env -> mind_specif
+val lookup_mind_specif : inductive -> env -> inductive_instance
(* [find_inductive env sigma t] builds an [inductive_type] or raises
[Induc] if [t] is not an inductive type; The result is relative to
@@ -189,7 +195,6 @@ and [get_arity env sigma is] returns [[(Anonymous,'nat')],'Set'].
(* Cases info *)
-val make_case_info : mind_specif -> case_style option -> pattern_source array
- -> case_info
-val make_default_case_info : mind_specif -> case_info
-
+val make_case_info : inductive_instance -> case_style option
+ -> pattern_source array -> case_info
+val make_default_case_info : inductive_instance -> case_info
diff --git a/kernel/instantiate.ml b/kernel/instantiate.ml
index 37e2c310c..94ab793c6 100644
--- a/kernel/instantiate.ml
+++ b/kernel/instantiate.ml
@@ -8,7 +8,7 @@ open Generic
open Term
open Sign
open Evd
-open Constant
+open Declarations
open Environ
let is_id_inst ids args =
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 51ba31504..de61b72e9 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -8,7 +8,7 @@ open Generic
open Term
open Univ
open Evd
-open Constant
+open Declarations
open Environ
open Instantiate
open Closure
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 9fc5265e9..1cf6c6eca 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -9,7 +9,7 @@ open Generic
open Term
open Reduction
open Sign
-open Constant
+open Declarations
open Inductive
open Environ
open Type_errors
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index e95aa2390..07857dea9 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -7,7 +7,7 @@ open Names
open Term
open Univ
open Sign
-open Constant
+open Declarations
open Inductive
open Environ
open Typeops
@@ -46,7 +46,7 @@ val lookup_var : identifier -> safe_environment -> name * typed_type
val lookup_rel : int -> safe_environment -> name * typed_type
val lookup_constant : section_path -> safe_environment -> constant_body
val lookup_mind : section_path -> safe_environment -> mutual_inductive_body
-val lookup_mind_specif : inductive -> safe_environment -> mind_specif
+val lookup_mind_specif : inductive -> safe_environment -> inductive_instance
val export : safe_environment -> string -> compiled_env
val import : compiled_env -> safe_environment -> safe_environment
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 6e453b60b..b62e31714 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -7,7 +7,7 @@ open Names
open Univ
open Generic
open Term
-open Constant
+open Declarations
open Sign
open Environ
open Reduction
@@ -94,62 +94,21 @@ let instantiate_arity mis =
let instantiate_arity = mis_typed_arity
let type_of_inductive env sigma i =
- let mis = lookup_mind_specif i env in
- let hyps = mis.mis_mib.mind_hyps in
(* TODO: check args *)
- instantiate_arity mis
+ instantiate_arity (lookup_mind_specif i env)
(* Constructors. *)
-(*
-let instantiate_lc mis =
- let hyps = mis.mis_mib.mind_hyps in
- let lc = mis.mis_mip.mind_lc in
- instantiate_constr (ids_of_sign hyps) lc (Array.to_list mis.mis_args)
-*)
-let instantiate_lc = mis_lc
-
-let type_of_constructor env sigma ((ind_sp,j),args as cstr) =
- let mind = inductive_of_constructor cstr in
- let mis = lookup_mind_specif mind env in
- (* TODO: check args *)
- let specif = instantiate_lc mis in
- let make_ik k = DOPN (MutInd (mis.mis_sp,k), mis.mis_args) in
- if j > mis_nconstr mis then
- anomaly "type_of_constructor"
- else
- sAPPViList (j-1) specif (list_tabulate make_ik (mis_ntypes mis))
-
-(* gives the vector of constructors and of
- types of constructors of an inductive definition
- correctly instanciated *)
-
-let mis_type_mconstructs mis =
- let specif = instantiate_lc mis
- and ntypes = mis_ntypes mis
- and nconstr = mis_nconstr mis in
- let make_ik k = DOPN (MutInd (mis.mis_sp,k), mis.mis_args)
- and make_ck k =
- DOPN (MutConstruct ((mis.mis_sp,mis.mis_tyi),k+1), mis.mis_args)
- in
- (Array.init nconstr make_ck,
- sAPPVList specif (list_tabulate make_ik ntypes))
-
let type_mconstructs env sigma mind =
- let mis = lookup_mind_specif mind env in
- mis_type_mconstructs mis
-
-let mis_type_mconstruct i mispec =
- let specif = instantiate_lc mispec
- and ntypes = mis_ntypes mispec
- and nconstr = mis_nconstr mispec in
- let make_Ik k = DOPN(MutInd(mispec.mis_sp,k),mispec.mis_args) in
- if i > nconstr then error "Not enough constructors in the type";
- sAPPViList (i-1) specif (list_tabulate make_Ik ntypes)
+ mis_type_mconstructs (lookup_mind_specif mind env)
let type_mconstruct env sigma i mind =
- let mis = lookup_mind_specif mind env in
- mis_type_mconstruct i mis
+ mis_type_mconstruct i (lookup_mind_specif mind env)
+
+let type_of_constructor env sigma cstr =
+ type_mconstruct env sigma
+ (index_of_constructor cstr)
+ (inductive_of_constructor cstr)
let type_inst_construct i (IndFamily (mis,globargs)) =
let tc = mis_type_mconstruct i mis in
@@ -695,10 +654,6 @@ let check_fix env sigma = function
(* Co-fixpoints. *)
-let mind_nparams env i =
- let mis = lookup_mind_specif i env in
- mis.mis_mib.mind_nparams
-
let check_guard_rec_meta env sigma nbfix def deftype =
let rec codomain_is_coind c =
match whd_betadeltaiota env sigma (strip_outer_cast c) with
@@ -736,7 +691,8 @@ let check_guard_rec_meta env sigma nbfix def deftype =
| (DOPN (MutConstruct(_,i as cstr_sp),l), args) ->
let lra =vlra.(i-1) in
let mI = inductive_of_constructor (cstr_sp,l) in
- let _,realargs = list_chop (mind_nparams env mI) args in
+ let mis = lookup_mind_specif mI env in
+ let _,realargs = list_chop (mis_nparams mis) args in
let rec process_args_of_constr l lra =
match l with
| [] -> true
diff --git a/library/declare.ml b/library/declare.ml
index 2a9dc279c..0bce97fe4 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -7,7 +7,7 @@ open Names
open Generic
open Term
open Sign
-open Constant
+open Declarations
open Inductive
open Reduction
open Type_errors
@@ -314,8 +314,7 @@ let declare_eliminations sp i =
in
let env = Global.env () in
let sigma = Evd.empty in
- let elim_scheme =
- strip_all_casts (mis_make_indrec env sigma [] mispec).(0) in
+ let elim_scheme = build_indrec env sigma mispec in
let npars = mis_nparams mispec in
let make_elim s = instanciate_indrec_scheme s npars elim_scheme in
let kelim = mis_kelim mispec in
diff --git a/library/declare.mli b/library/declare.mli
index 0142eb0ac..9bb9c1607 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -5,7 +5,7 @@
open Names
open Term
open Sign
-open Constant
+open Declarations
open Inductive
(*i*)
diff --git a/library/global.mli b/library/global.mli
index fbf034527..99bb478fd 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -6,7 +6,7 @@ open Names
open Univ
open Term
open Sign
-open Constant
+open Declarations
open Inductive
open Environ
open Safe_typing
@@ -36,7 +36,7 @@ val lookup_var : identifier -> name * typed_type
val lookup_rel : int -> name * typed_type
val lookup_constant : section_path -> constant_body
val lookup_mind : section_path -> mutual_inductive_body
-val lookup_mind_specif : inductive -> mind_specif
+val lookup_mind_specif : inductive -> inductive_instance
val export : string -> compiled_env
val import : compiled_env -> unit
diff --git a/library/impargs.ml b/library/impargs.ml
index 06ce6915b..fbdb17847 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -5,7 +5,7 @@ open Names
open Generic
open Term
open Reduction
-open Constant
+open Declarations
open Inductive
type implicits =
diff --git a/library/indrec.ml b/library/indrec.ml
index 8c915c451..b684226d5 100644
--- a/library/indrec.ml
+++ b/library/indrec.ml
@@ -6,7 +6,7 @@ open Util
open Names
open Generic
open Term
-open Constant
+open Declarations
open Inductive
open Instantiate
open Environ
@@ -24,69 +24,9 @@ let make_prod_dep dep env = if dep then prod_name env else simple_prod
(**********************************************************************)
(* Building case analysis schemes *)
-(*
-let mis_make_case_com depopt env sigma mispec kind =
-
- let nparams = mis_nparams mispec in
- let mind = mkMutInd ((mispec.mis_sp,mispec.mis_tyi),mispec.mis_args) in
- let t = mis_arity mispec in
- let (lc,lct) = mis_type_mconstructs mispec in
- let lnames,sort = splay_prod env sigma t in
- let nconstr = Array.length lc in
- let dep = match depopt with
- | None -> (sort<>DOP0(Sort(Prop Null)))
- | Some d -> d
- in
- if not (List.exists (base_sort_cmp CONV kind) (mis_kelim mispec)) then
- raise (InductiveError (NotAllowedCaseAnalysis (dep,kind,ind.mind)));
-
- let lnamesar,lnamespar = list_chop (List.length lnames - nparams) lnames in
- let lgar = List.length lnamesar in
- let ar = hnf_prod_appvect env sigma t (rel_vect 0 nparams) in
-
- let typP =
- if dep then
- make_arity_dep env sigma (DOP0(Sort kind)) ar
- (appvect (mind,rel_vect 0 nparams))
- else
- make_arity_nodep env sigma (DOP0(Sort kind)) ar
- in
- let rec add_branch k =
- if k = nconstr then
- it_lambda_name env
- (lambda_create env
- (appvect (mind,
- (Array.append (rel_vect (nconstr+lgar+1) nparams)
- (rel_vect 0 lgar))),
- mkMutCaseA (make_default_case_info mispec)
- (Rel (nconstr+lgar+2))
- (Rel 1)
- (rel_vect (lgar+1) nconstr)))
- (lift_context (nconstr+1) lnamesar)
- else
- mkLambda_string "f"
- (if dep then
- type_one_branch_dep env sigma
- (nparams,(rel_list (k+1) nparams),Rel (k+1)) lc.(k) lct.(k)
- else
- type_one_branch_nodep env sigma
- (nparams,(rel_list (k+1) nparams),Rel (k+1)) lct.(k))
- (add_branch (k+1))
- in
- it_lambda_name env (mkLambda_string "P" typP (add_branch 0)) lnamespar
-*)
-
-(*
-let push_rel_type sigma (na,t) env =
- push_rel (na,make_typed t (get_sort_of env sigma t)) env
-
-let push_rels vars env =
- List.fold_left (fun env nvar -> push_rel_type Evd.empty nvar env) env vars
-*)
-
(* Nouvelle version, plus concise mais plus coûteuse à cause de
- lift_constructor et lift_inductive qui ne se contente pas de lifter les
- paramètres globaux *)
+ lift_constructor et lift_inductive_family qui ne se contente pas de
+ lifter les paramètres globaux *)
let mis_make_case_com depopt env sigma mispec kind =
let lnamespar = mis_params_ctxt mispec in
@@ -96,10 +36,9 @@ let mis_make_case_com depopt env sigma mispec kind =
| Some d -> d
in
if not (List.exists (base_sort_cmp CONV kind) (mis_kelim mispec)) then
- begin
- let mind = ((mispec.mis_sp,mispec.mis_tyi),mispec.mis_args) in
- raise (InductiveError (NotAllowedCaseAnalysis (dep,kind,mind)))
- end;
+ raise
+ (InductiveError
+ (NotAllowedCaseAnalysis (dep,kind,mis_inductive mispec)));
let nbargsprod = mis_nrealargs mispec + 1 in
@@ -249,13 +188,6 @@ let mis_make_indrec env sigma listdepkind mispec =
let nparams = mis_nparams mispec in
let lnamespar = mis_params_ctxt mispec in
let env' = (* push_rels lnamespar *) env in
- let listdepkind =
- if listdepkind = [] then
- let kind = mis_sort mispec in
- let dep = kind <> Prop Null in [(mispec,dep,kind)]
- else
- listdepkind
- in
let nrec = List.length listdepkind in
let depPvec =
Array.create (mis_ntypes mispec) (None : (bool * constr) option) in
@@ -264,36 +196,12 @@ let mis_make_indrec env sigma listdepkind mispec =
assign k = function
| [] -> ()
| (mispeci,dep,_)::rest ->
- (Array.set depPvec mispeci.mis_tyi (Some(dep,Rel k));
+ (Array.set depPvec (mis_index mispeci) (Some(dep,Rel k));
assign (k-1) rest)
in
assign nrec listdepkind
in
let recargsvec = mis_recargs mispec in
-(*
- let ntypes = mis_ntypes mispec in
- let mind_arity = mis_arity mispec in
- let (lnames, kind) = splay_arity env sigma mind_arity in
- let lnamespar = list_lastn nparams lnames in
- let listdepkind =
- if listdepkind = [] then
- let dep = kind <> Prop Null in [(mispec,dep,kind)]
- else
- listdepkind
- in
- let nrec = List.length listdepkind in
- let depPvec = Array.create ntypes (None : (bool * constr) option) in
- let _ =
- let rec
- assign k = function
- | [] -> ()
- | (mispeci,dep,_)::rest ->
- (Array.set depPvec mispeci.mis_tyi (Some(dep,Rel k));
- assign (k-1) rest)
- in
- assign nrec listdepkind
- in
-*)
let make_one_rec p =
let makefix nbconstruct =
let rec mrec i ln ltyp ldef = function
@@ -358,7 +266,7 @@ let mis_make_indrec env sigma listdepkind mispec =
in
let rec make_branch i = function
| (mispeci,dep,_)::rest ->
- let tyi = mispeci.mis_tyi in
+ let tyi = mis_index mispeci in
let (lc,lct) = mis_type_mconstructs mispeci in
let rec onerec j =
if j = Array.length lc then
@@ -386,13 +294,13 @@ let mis_make_indrec env sigma listdepkind mispec =
in
let (mispeci,dep,kind) = List.nth listdepkind p in
if mis_is_recursive_subset
- (List.map (fun (mispec,_,_) -> mispec.mis_tyi) listdepkind) mispeci
+ (List.map (fun (mispec,_,_) -> mis_index mispec) listdepkind) mispeci
then
it_lambda_name env (put_arity 0 listdepkind) lnamespar
else
mis_make_case_com (Some dep) env sigma mispeci kind
in
- Array.init nrec make_one_rec
+ list_tabulate make_one_rec nrec
(**********************************************************************)
(* This builds elimination predicate for Case tactic *)
@@ -419,15 +327,15 @@ let change_sort_arity sort =
in
drec
-let instanciate_indrec_scheme sort =
+let instanciate_indrec_scheme sort =
let rec drec npar elim =
let (n,t,c) = destLambda (strip_outer_cast elim) in
if npar = 0 then
mkLambda n (change_sort_arity sort t) c
else
mkLambda n t (drec (npar-1) c)
- in
- drec
+ in
+ drec
(**********************************************************************)
(* Interface to build complex Scheme *)
@@ -441,7 +349,7 @@ let check_arities listdepkind =
raise (InductiveError (BadInduction (dep, id, kinds))))
listdepkind
-let build_indrec env sigma = function
+let build_mutual_indrec env sigma = function
| (mind,dep,s)::lrecspec ->
let ((sp,tyi),_) = mind in
let mispec = lookup_mind_specif mind env in
@@ -458,8 +366,13 @@ let build_indrec env sigma = function
in
let _ = check_arities listdepkind in
mis_make_indrec env sigma listdepkind mispec
- | _ -> assert false
+ | _ -> anomaly "build_indrec expects a non empty list of inductive types"
+let build_indrec env sigma mispec =
+ let kind = mis_sort mispec in
+ let dep = kind <> Prop Null in
+ strip_all_casts
+ (List.hd (mis_make_indrec env sigma [(mispec,dep,kind)] mispec))
(**********************************************************************)
(* To handle old Case/Match syntax in Pretyping *)
diff --git a/library/indrec.mli b/library/indrec.mli
index 6e81f5316..bfb22f4c9 100644
--- a/library/indrec.mli
+++ b/library/indrec.mli
@@ -4,7 +4,7 @@
(*i*)
open Names
open Term
-open Constant
+open Declarations
open Inductive
open Environ
open Evd
@@ -18,16 +18,16 @@ val make_case_dep : env -> 'a evar_map -> inductive -> sorts -> constr
val make_case_nodep : env -> 'a evar_map -> inductive -> sorts -> constr
val make_case_gen : env -> 'a evar_map -> inductive -> sorts -> constr
-(* This builds elimination scheme associated to inductive types *)
+(* This builds an elimination scheme associated (using the own arity
+ of the inductive) *)
-val mis_make_indrec : env -> 'a evar_map ->
- (mind_specif * bool * sorts) list -> mind_specif -> constr array
+val build_indrec : env -> 'a evar_map -> inductive_instance -> constr
val instanciate_indrec_scheme : sorts -> int -> constr -> constr
(* This builds complex [Scheme] *)
-val build_indrec :
- env -> 'a evar_map -> (inductive * bool * sorts) list -> constr array
+val build_mutual_indrec :
+ env -> 'a evar_map -> (inductive * bool * sorts) list -> constr list
(* These are for old Case/Match typing *)
diff --git a/library/redinfo.ml b/library/redinfo.ml
index 0ea9cdd92..bc51d5d75 100644
--- a/library/redinfo.ml
+++ b/library/redinfo.ml
@@ -5,7 +5,7 @@ open Util
open Names
open Generic
open Term
-open Constant
+open Declarations
open Reduction
type constant_evaluation =
diff --git a/parsing/pretty.ml b/parsing/pretty.ml
index 641fa4035..00b598646 100644
--- a/parsing/pretty.ml
+++ b/parsing/pretty.ml
@@ -6,7 +6,7 @@ open Util
open Names
open Generic
open Term
-open Constant
+open Declarations
open Inductive
open Sign
open Reduction
diff --git a/parsing/pretty.mli b/parsing/pretty.mli
index ae5ce0f25..e10c53b80 100644
--- a/parsing/pretty.mli
+++ b/parsing/pretty.mli
@@ -31,9 +31,8 @@ val print_val : env -> unsafe_judgment -> std_ppcmds
val print_type : env -> unsafe_judgment -> std_ppcmds
val print_eval :
'a reduction_function -> env -> unsafe_judgment -> std_ppcmds
-val implicit_args_msg :
- section_path -> Constant.mutual_inductive_packet array -> std_ppcmds
-val print_mutual : section_path -> Constant.mutual_inductive_body -> std_ppcmds
+val print_mutual :
+ section_path -> Declarations.mutual_inductive_body -> std_ppcmds
val print_name : identifier -> std_ppcmds
val print_opaque_name : identifier -> std_ppcmds
val print_local_context : unit -> std_ppcmds
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 36281359b..85bce776a 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -3,7 +3,7 @@ open Util
open Names
open Generic
open Term
-open Constant
+open Declarations
open Inductive
open Environ
open Sign
@@ -220,23 +220,9 @@ let lift_tomatch_type n = liftn_tomatch_type n 1
let lift_tomatch n ((current,typ),info) =
((lift n current,lift_tomatch_type n typ),info)
-let substn_many_ind_instance cv depth mis = {
- mis_sp = mis.mis_sp;
- mis_mib = mis.mis_mib;
- mis_tyi = mis.mis_tyi;
- mis_args = Array.map (substn_many cv depth) mis.mis_args;
- mis_mip = mis.mis_mip
-}
-
-let substn_many_ind_data cv depth (IndFamily (mis,params)) =
- IndFamily (substn_many_ind_instance cv depth mis,
- List.map (substn_many cv depth) params)
-
let substn_many_tomatch v depth = function
- | IsInd (t,IndType (ind_data,realargs)) ->
- IsInd (substn_many v depth t,
- IndType (substn_many_ind_data v depth ind_data,
- List.map (substn_many v depth) realargs))
+ | IsInd (t,indt) ->
+ IsInd (substn_many v depth t,substn_many_ind_type v depth indt)
| NotInd t -> NotInd (substn_many v depth t)
let subst_tomatch (depth,c) = substn_many_tomatch [|make_substituend c|] depth
diff --git a/pretyping/class.ml b/pretyping/class.ml
index 9b5a02c6f..0d011fcce 100644
--- a/pretyping/class.ml
+++ b/pretyping/class.ml
@@ -7,7 +7,7 @@ open Names
open Generic
open Term
open Inductive
-open Constant
+open Declarations
open Environ
open Lib
open Classops
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 091c14a2e..34ffa2f95 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -116,9 +116,9 @@ let encode_inductive id =
(indsp,constr_lengths)
let sp_of_spi (refsp,tyi) =
- let mip = Constant.mind_nth_type_packet (Global.lookup_mind refsp) tyi in
+ let mip = Declarations.mind_nth_type_packet (Global.lookup_mind refsp) tyi in
let (pa,_,k) = repr_path refsp in
- make_path pa mip.Constant.mind_typename k
+ make_path pa mip.Declarations.mind_typename k
(*
let (_,mip) = mind_specif_of_mind_light spi in
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 7b1794c15..d033ac5d2 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -7,7 +7,7 @@ open Names
open Sign
open Generic
open Term
-open Constant
+open Declarations
open Environ
open Evd
open Declare
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 93426fde9..9c56db03a 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -6,7 +6,7 @@ open Util
open Options
open Generic
open Term
-open Constant
+open Declarations
open Inductive
open Reduction
open Tacred
@@ -359,17 +359,12 @@ let build_scheme lnamedepindsort =
(inductive_of_ident indid,dep,s)) lnamedepindsort
in
let n = NeverDischarge in
- let listdecl = Indrec.build_indrec env0 sigma lrecspec in
- let rec declare i = function
- | fi::lf ->
- let ce =
- { const_entry_body = Cooked listdecl.(i); const_entry_type = None }
- in
- declare_constant fi (ce,n);
- declare (i+1) lf
- | _ -> ()
+ let listdecl = Indrec.build_mutual_indrec env0 sigma lrecspec in
+ let rec declare decl fi =
+ let ce = { const_entry_body = Cooked decl; const_entry_type = None }
+ in declare_constant fi (ce,n)
in
- declare 0 lrecnames;
+ List.iter2 declare listdecl lrecnames;
if is_verbose() then pPNL(recursive_message lrecnames)
let start_proof_com s stre com =
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index aa1e1e96b..1e8501f12 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -7,7 +7,7 @@ open Names
open Sign
open Generic
open Term
-open Constant
+open Declarations
open Inductive
open Instantiate
open Reduction
diff --git a/toplevel/minicoq.ml b/toplevel/minicoq.ml
index 7af018585..7df256f19 100644
--- a/toplevel/minicoq.ml
+++ b/toplevel/minicoq.ml
@@ -7,7 +7,7 @@ open Names
open Generic
open Term
open Sign
-open Constant
+open Declarations
open Inductive
open Type_errors
open Safe_typing
diff --git a/toplevel/record.ml b/toplevel/record.ml
index c4cc168d7..8f3052441 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -6,6 +6,7 @@ open Util
open Names
open Generic
open Term
+open Declarations
open Declare
open Coqast
open Ast
@@ -135,8 +136,8 @@ let definition_structure (is_coe,idstruc,ps,cfs,idbuild,s) =
let ok =
try
let cie =
- { Constant.const_entry_body = Constant.Cooked proj;
- Constant.const_entry_type = None } in
+ { const_entry_body = Cooked proj;
+ const_entry_type = None } in
(declare_constant fi (cie,NeverDischarge); true)
with UserError(s,pps) ->
((warning_or_error coe
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-04 07:57:00 +0000