aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--contrib/xml/xmlcommand.ml34
-rw-r--r--kernel/declarations.ml23
-rw-r--r--kernel/declarations.mli24
-rw-r--r--kernel/indtypes.ml47
-rw-r--r--kernel/indtypes.mli36
-rw-r--r--kernel/safe_typing.ml125
-rw-r--r--library/declare.ml25
-rw-r--r--parsing/pretty.ml4
-rw-r--r--toplevel/command.ml27
-rw-r--r--toplevel/discharge.ml65
10 files changed, 238 insertions, 172 deletions
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index f9736714fe..d053ed7453 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -45,6 +45,28 @@ let ext_of_tag =
| Variable -> "var"
;;
+(* Internally, for Coq V7, params of inductive types are associated
+ not to the whole block of mutual inductive (as it was in V6) but to
+ each member of the block; but externally, params remain shared by
+ all members in the concrete syntax; the following function checks
+ that the parameters of each inductive of a same block are all the
+ same, then returns this number; it fails otherwise *)
+let extract_nparams pack =
+ let module D = Declarations in
+ let module U = Util in
+ let module S = Sign in
+
+ let {D.mind_nparams=nparams0} = pack.(0) in
+ let arity0 = D.mind_user_arity pack.(0) in
+ let params0 = S.decompose_prod_n_assum nparams0 arity0 in
+ for i = 1 to Array.length pack - 1 do
+ let {D.mind_nparams=nparamsi} = pack.(i) in
+ let arityi = D.mind_user_arity pack.(i) in
+ let paramsi = S.decompose_prod_n_assum nparamsi arityi in
+ if params0 <> paramsi then U.error "Cannot convert a block of inductive definitions with parameters specific to each inductive to a block of mutual inductive definitions with parameters global to the whole block"
+ done;
+ nparams0
+
(* could_have_namesakes sp = true iff o is an object that could be cooked and *)
(* than that could exists in cooked form with the same name in a super *)
(* section of the actual section *)
@@ -598,11 +620,12 @@ let print_mutual_inductive_packet inner_types names env p =
(* and nparams is the number of "parameters" in the arity of the *)
(* mutual inductive types *)
(* returns a stream of XML tokens suitable to be pretty printed via Xml.pp *)
-let print_mutual_inductive packs fv hyps nparams env inner_types =
+let print_mutual_inductive packs fv hyps env inner_types =
let module D = Declarations in
let module E = Environ in
let module X = Xml in
let module N = Names in
+ let nparams = extract_nparams packs in
let names =
List.map
(fun p -> let {D.mind_typename=typename} = p in N.Name(typename))
@@ -698,12 +721,10 @@ let print sp fn =
| Some c -> print_definition id c typ [] hyps env inner_types
end
| T.IndRef (sp,_) ->
- let {D.mind_packets=packs ; D.mind_nparams=nparams ; D.mind_hyps=hyps} =
- G.lookup_mind sp
- in
+ let {D.mind_packets=packs ; D.mind_hyps=hyps} = G.lookup_mind sp in
let hyps = string_list_of_named_context_list hyps in
sp,Inductive,
- print_mutual_inductive packs [] hyps nparams env inner_types
+ print_mutual_inductive packs [] hyps env inner_types
| T.ConstructRef _
| T.EvarRef _ ->
Util.anomaly ("print: this should not happen")
@@ -815,12 +836,11 @@ let print_object lobj id sp dn fv env =
| "INDUCTIVE" ->
let
{D.mind_packets=packs ;
- D.mind_nparams=nparams ;
D.mind_hyps = hyps
} = G.lookup_mind sp
in
let hyps = string_list_of_named_context_list hyps in
- print_mutual_inductive packs fv hyps nparams env inner_types
+ print_mutual_inductive packs fv hyps env inner_types
| "VARIABLE" ->
let (_,(varentry,_,_)) = Declare.out_variable lobj in
begin
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 96eef57001..8be72eb94f 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -21,10 +21,16 @@ let is_defined cb =
let is_opaque cb = cb.const_opaque
+(*s Global and local constant declaration. *)
+
type constant_entry = {
const_entry_body : constr;
const_entry_type : constr option }
+type local_entry =
+ | LocalDef of constr
+ | LocalAssum of constr
+
(* Inductive entries *)
type recarg =
@@ -45,7 +51,8 @@ type one_inductive_body = {
mind_nrealargs : int;
mind_kelim : sorts list;
mind_listrec : (recarg list) array;
- mind_finite : bool }
+ mind_finite : bool;
+ mind_nparams : int }
type mutual_inductive_body = {
mind_kind : path_kind;
@@ -53,8 +60,7 @@ type mutual_inductive_body = {
mind_hyps : named_context;
mind_packets : one_inductive_body array;
mind_constraints : constraints;
- mind_singl : constr option;
- mind_nparams : int }
+ mind_singl : constr option }
let mind_type_finite mib i = mib.mind_packets.(i).mind_finite
@@ -68,10 +74,17 @@ let mind_user_arity mip = match mip.mind_user_arity with
(*s Declaration. *)
-type mutual_inductive_entry = {
+type one_inductive_entry = {
mind_entry_nparams : int;
+ mind_entry_params : (identifier * local_entry) list;
+ mind_entry_typename : identifier;
+ mind_entry_arity : constr;
+ mind_entry_consnames : identifier list;
+ mind_entry_lc : constr list }
+
+type mutual_inductive_entry = {
mind_entry_finite : bool;
- mind_entry_inds : (identifier * constr * identifier list * constr list) list}
+ mind_entry_inds : one_inductive_entry list }
let mind_nth_type_packet mib n = mib.mind_packets.(n)
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 0cc927c8ca..e24ac3bdd1 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -25,12 +25,16 @@ val is_defined : constant_body -> bool
val is_opaque : constant_body -> bool
-(*s Constant declaration. *)
+(*s Global and local constant declaration. *)
type constant_entry = {
const_entry_body : constr;
const_entry_type : constr option }
+type local_entry =
+ | LocalDef of constr
+ | LocalAssum of constr
+
(*s Inductive types (internal representation). *)
type recarg =
@@ -56,7 +60,8 @@ type one_inductive_body = {
mind_nrealargs : int;
mind_kelim : sorts list;
mind_listrec : (recarg list) array;
- mind_finite : bool }
+ mind_finite : bool;
+ mind_nparams : int }
type mutual_inductive_body = {
mind_kind : path_kind;
@@ -64,8 +69,7 @@ type mutual_inductive_body = {
mind_hyps : named_context;
mind_packets : one_inductive_body array;
mind_constraints : constraints;
- mind_singl : constr option;
- mind_nparams : int }
+ mind_singl : constr option }
val mind_type_finite : mutual_inductive_body -> int -> bool
val mind_user_lc : one_inductive_body -> types array
@@ -76,8 +80,14 @@ val mind_arities_context : mutual_inductive_body -> rel_declaration list
(*s Declaration of inductive types. *)
-type mutual_inductive_entry = {
+type one_inductive_entry = {
mind_entry_nparams : int;
- mind_entry_finite : bool;
- mind_entry_inds : (identifier * constr * identifier list * constr list) list}
+ mind_entry_params : (identifier * local_entry) list;
+ mind_entry_typename : identifier;
+ mind_entry_arity : constr;
+ mind_entry_consnames : identifier list;
+ mind_entry_lc : constr list }
+type mutual_inductive_entry = {
+ mind_entry_finite : bool;
+ mind_entry_inds : one_inductive_entry list }
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index ece400ad16..f10e59c9c7 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -59,7 +59,9 @@ let check_constructors_names id =
let mind_check_names mie =
let rec check indset cstset = function
| [] -> ()
- | (id,_,cl,_)::inds ->
+ | ind::inds ->
+ let id = ind.mind_entry_typename in
+ let cl = ind.mind_entry_consnames in
if Idset.mem id indset then
raise (InductiveError (SameNamesTypes id))
else
@@ -74,35 +76,20 @@ let mind_check_names mie =
let mind_extract_params n c =
let (l,c') = decompose_prod_n_assum n c in (l,c')
-
-let extract nparams c =
- try fst (mind_extract_params nparams c)
- with UserError _ -> raise (InductiveError BadEntry)
-
-let check_params params params' =
- if not (params = params') then raise (InductiveError BadEntry)
-
-let mind_extract_and_check_params mie =
- let nparams = mie.mind_entry_nparams in
- match mie.mind_entry_inds with
- | [] -> anomaly "empty inductive types declaration"
- | (_,ar,_,_)::l ->
- let params = extract nparams ar in
- List.iter (fun (_,c,_,_) -> check_params params (extract nparams c)) l;
- params
-
-let mind_check_lc params mie =
- let nparams = List.length params in
- let check_lc (_,_,_,lc) =
- List.iter (fun c -> check_params params (extract nparams c)) lc in
- List.iter check_lc mie.mind_entry_inds
let mind_check_arities env mie =
let check_arity id c =
if not (is_arity env Evd.empty c) then
raise (InductiveError (NotAnArity id))
in
- List.iter (fun (id,ar,_,_) -> check_arity id ar) mie.mind_entry_inds
+ List.iter
+ (fun {mind_entry_typename=id; mind_entry_arity=ar} -> check_arity id ar)
+ mie.mind_entry_inds
+
+let mind_check_wellformed env mie =
+ if mie.mind_entry_inds = [] then anomaly "empty inductive types declaration";
+ mind_check_names mie;
+ mind_check_arities env mie
(***********************************************************************)
@@ -313,9 +300,9 @@ let is_recursive listind =
in
array_exists one_is_rec
-let cci_inductive env env_ar kind nparams finite inds cst =
+let cci_inductive env env_ar kind finite inds cst =
let ntypes = List.length inds in
- let one_packet i (id,ar,cnames,issmall,isunit,lc) =
+ let one_packet i (nparams,id,ar,cnames,issmall,isunit,lc) =
let recargs = listrec_mconstr env_ar ntypes nparams i lc in
let isunit = isunit && ntypes = 1 && (not (is_recursive [0] recargs)) in
let (ar_sign,ar_sort) = splay_arity env Evd.empty (body_of_type ar) in
@@ -340,11 +327,12 @@ let cci_inductive env env_ar kind nparams finite inds cst =
mind_sort = ar_sort;
mind_kelim = kelim;
mind_listrec = recargs;
- mind_finite = finite }
+ mind_finite = finite;
+ mind_nparams = nparams }
in
let ids =
List.fold_left
- (fun acc (_,ar,_,_,_,lc) ->
+ (fun acc (_,_,ar,_,_,_,lc) ->
Idset.union (global_vars_set (body_of_type ar))
(Array.fold_left
(fun acc c -> Idset.union (global_vars_set (body_of_type c)) acc)
@@ -358,5 +346,4 @@ let cci_inductive env env_ar kind nparams finite inds cst =
mind_hyps = keep_hyps ids (named_context env);
mind_packets = packets;
mind_constraints = cst;
- mind_singl = None;
- mind_nparams = nparams }
+ mind_singl = None }
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index 71041c279e..b8ea65f16e 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -28,39 +28,27 @@ type inductive_error =
| BadInduction of bool * identifier * sorts
| NotMutualInScheme
-exception InductiveError of inductive_error
-
-(*s The following functions are utility functions to check and to
- decompose a declaration. *)
-
-(* [mind_check_names] checks the names of an inductive types declaration
- i.e. that all the types and constructors names are distinct.
- It raises an exception [InductiveError _] if it is not the case. *)
-
-val mind_check_names : mutual_inductive_entry -> unit
-
-(* [mind_extract_and_check_params] extracts the parameters of an inductive
- types declaration. It raises an exception [InductiveError _] if there is
- not enough abstractions in any of the terms of the field
- [mind_entry_inds]. *)
-
-val mind_extract_and_check_params :
- mutual_inductive_entry -> Sign.rel_context
+(* [mind_extract_params] extracts the parameters of an inductive
+ type declaration. *)
val mind_extract_params : int -> constr -> Sign.rel_context * constr
-val mind_check_lc : Sign.rel_context -> mutual_inductive_entry -> unit
+exception InductiveError of inductive_error
+
+(*s The following function does checks on inductive declarations. *)
-(* [mind_check_arities] checks that the types declared for all the
- inductive types are some arities. *)
+(* [mind_check_wellformed env mie] checks that the types declared for
+ all the inductive types are arities. It checks also that
+ constructor and inductive names altogether are distinct. It raises
+ an exception [InductiveError _] if [mie] is not well-formed *)
-val mind_check_arities : env -> mutual_inductive_entry -> unit
+val mind_check_wellformed : env -> mutual_inductive_entry -> unit
(* [cci_inductive] checks positivity and builds an inductive body *)
val cci_inductive :
- env -> env -> path_kind -> int -> bool ->
- (identifier * types * identifier list * bool * bool * types array)
+ env -> env -> path_kind -> bool ->
+ (int * identifier * types * identifier list * bool * bool * types array)
list ->
constraints ->
mutual_inductive_body
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index c0e700a130..64968c5098 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -269,6 +269,23 @@ let push_rel_assum = push_rel_or_named_assum push_rel_assum
let push_rels_with_univ vars env =
List.fold_left (fun env nvar -> push_rel_assum nvar env) env vars
+let safe_infer_local_decl env id = function
+ | LocalDef c ->
+ let (j,cst) = safe_infer env c in
+ (Name id, Some j.uj_val, j.uj_type), cst
+ | LocalAssum c ->
+ let (j,cst) = safe_infer env c in
+ (Name id, None, assumption_of_judgment env Evd.empty j), cst
+
+let safe_infer_local_decls env decls =
+ let rec inferec env = function
+ | (id, d) :: l ->
+ let env, l, cst1 = inferec env l in
+ let d, cst2 = safe_infer_local_decl env id d in
+ push_rel d env, d :: l, Constraint.union cst1 cst2
+ | [] -> env, [], Constraint.empty in
+ inferec env decls
+
(* Insertion of constants and parameters in environment. *)
let add_parameter sp t env =
@@ -370,12 +387,9 @@ let is_unit arinfos constrsinfos =
| [constrinfos] -> is_logic_constr constrinfos && is_logic_arity arinfos
| _ -> false
-let small_unit constrsinfos (env_ar,nparams,ar) =
+let small_unit constrsinfos (env_ar_par,short_arity) =
let issmall = List.for_all is_small constrsinfos in
- let arinfos =
- let (params,a) = mind_extract_params nparams ar in
- let env_par = push_rels params env_ar in
- infos_and_sort env_par a in
+ let arinfos = infos_and_sort env_ar_par short_arity in
let isunit = is_unit arinfos constrsinfos in
issmall, isunit
@@ -386,63 +400,82 @@ let enforce_type_constructor arsort smax cst =
| Type uc, Type ua -> Constraint.add (ua,Geq,uc) cst
| _,_ -> cst
-let type_one_constructor env_ar nparams arsort c =
- let infos =
- let (params,dc) = mind_extract_params nparams c in
- let env_par = push_rels params env_ar in
- infos_and_sort env_par dc
- in
- (* Constructors are typed-checked here *)
- let (j,cst) = safe_infer_type env_ar c in
+let type_one_constructor env_ar_par params arsort c =
+ let infos = infos_and_sort env_ar_par c in
+
+ (* Each constructor is typed-checked here *)
+ let (j,cst) = safe_infer_type env_ar_par c in
+ let full_cstr_type = it_mkProd_or_LetIn j.utj_val params in
(* If the arity is at some level Type arsort, then the sort of the
constructor must be below arsort; here we consider constructors with the
global parameters (which add a priori more constraints on their sort) *)
let cst2 = enforce_type_constructor arsort j.utj_type cst in
- (infos, j.utj_val, cst2)
+ (infos, full_cstr_type, cst2)
-let type_one_inductive i env_ar env_par nparams ninds (id,ar,cnames,vc) =
- let arsort = sort_of_arity env_ar ar in
+let infer_constructor_packet env_ar params short_arity arsort vc =
+ let env_ar_par = push_rels params env_ar in
let (constrsinfos,jlc,cst) =
List.fold_right
- (fun c (infosl,jl,cst) ->
- let (infos,jc,cst') = type_one_constructor env_ar nparams arsort c in
- (infos::infosl,jc::jl, Constraint.union cst cst'))
+ (fun c (infosl,l,cst) ->
+ let (infos,ct,cst') =
+ type_one_constructor env_ar_par params arsort c in
+ (infos::infosl,ct::l, Constraint.union cst cst'))
vc
- ([],[],Constraint.empty)
- in
+ ([],[],Constraint.empty) in
let vc' = Array.of_list jlc in
- let issmall,isunit = small_unit constrsinfos (env_par,nparams,ar) in
- let (_,tyar) = lookup_rel_type (ninds+1-i) env_ar in
- ((id,tyar,cnames,issmall,isunit,vc'), cst)
+ let issmall,isunit = small_unit constrsinfos (env_ar_par,short_arity) in
+ (issmall,isunit,vc', cst)
let add_mind sp mie env =
- mind_check_names mie;
- mind_check_arities env mie;
- let params = mind_extract_and_check_params mie in
- let nparams = mie.mind_entry_nparams in
- mind_check_lc params mie;
- let ninds = List.length mie.mind_entry_inds in
- let types_sign =
- List.map (fun (id,ar,_,_) -> (Name id,ar)) mie.mind_entry_inds
- in
- (* Arities with params are typed-checked here *)
- let env_arities = push_rels_with_univ types_sign env in
- let env_params = push_rels params env_arities in
- let _,inds,cst =
- List.fold_right
- (fun ind (i,inds,cst) ->
- let (ind',cst') =
- type_one_inductive i env_arities env_params nparams ninds ind
+ mind_check_wellformed env mie;
+
+ (* We first type params and arity of each inductive definition *)
+ (* This allows to build the environment of arities and to share *)
+ (* the set of constraints *)
+ let cst, env_arities, rev_params_arity_list =
+ List.fold_left
+ (fun (cst,env_arities,l) ind ->
+ (* Params are typed-checked here *)
+ let params = ind.mind_entry_params in
+ let env_params, params, cst1 = safe_infer_local_decls env params in
+ (* Arities (without params) are typed-checked here *)
+ let arity, cst2 = safe_infer_type env_params ind.mind_entry_arity in
+ (* We do not need to generate the universe of full_arity; if
+ later, after the validation of the inductive definition,
+ full_arity is used as argument or subject to cast, an
+ upper universe will be generated *)
+ let id = ind.mind_entry_typename in
+ let full_arity = it_mkProd_or_LetIn arity.utj_val params in
+ Constraint.union cst (Constraint.union cst1 cst2),
+ push_rel_assum (Name id, full_arity) env_arities,
+ (params, id, full_arity, arity.utj_val)::l)
+ (Constraint.empty,env,[])
+ mie.mind_entry_inds in
+
+ let params_arity_list = List.rev rev_params_arity_list in
+
+ (* Now, we type the constructors (without params) *)
+ let inds,cst =
+ List.fold_right2
+ (fun ind (params,id,full_arity,short_arity) (inds,cst) ->
+ let arsort = sort_of_arity env full_arity in
+ let lc = ind.mind_entry_lc in
+ let (issmall,isunit,lc',cst') =
+ infer_constructor_packet env_arities params short_arity arsort lc
in
- (i-1,ind'::inds, Constraint.union cst cst'))
+ let nparams = ind.mind_entry_nparams in
+ let consnames = ind.mind_entry_consnames in
+ let ind' = (nparams,id,full_arity,consnames,issmall,isunit,lc') in
+ (ind'::inds, Constraint.union cst cst'))
mie.mind_entry_inds
- (ninds,[],Constraint.empty)
- in
+ params_arity_list
+ ([],Constraint.empty) in
+
+ (* Finally, we build the inductive packet and push it to env *)
let kind = kind_of_path sp in
- let mib =
- cci_inductive env env_arities kind nparams mie.mind_entry_finite inds cst
+ let mib = cci_inductive env env_arities kind mie.mind_entry_finite inds cst
in
add_mind sp mib (add_constraints cst env)
diff --git a/library/declare.ml b/library/declare.ml
index 305dd815b8..4d76ef8aaa 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -172,36 +172,19 @@ let declare_constant id cd =
let inductive_names sp mie =
let names, _ =
List.fold_left
- (fun (names, n) (id,_,cnames,_) ->
+ (fun (names, n) ind ->
let indsp = (sp,n) in
let names, _ =
List.fold_left
(fun (names, p) id ->
let sp = Names.make_path (dirpath sp) id CCI in
((sp, ConstructRef (indsp,p)) :: names, p+1))
- (names, 1) cnames in
- let sp = Names.make_path (dirpath sp) id CCI in
+ (names, 1) ind.mind_entry_consnames in
+ let sp = Names.make_path (dirpath sp) ind.mind_entry_typename CCI in
((sp, IndRef indsp) :: names, n+1))
([], 0) mie.mind_entry_inds
in names
-let push_inductive_names sp mie =
- let _ =
- List.fold_left
- (fun n (id,_,cnames,_) ->
- let indsp = (sp,n) in
- let _ =
- List.fold_left
- (fun p id ->
- let sp = Names.make_path (dirpath sp) id CCI in
- Nametab.push sp (ConstructRef (indsp,p)); (p+1))
- 1 cnames in
- let sp = Names.make_path (dirpath sp) id CCI in
- Nametab.push sp (IndRef indsp);
- n+1)
- 0 mie.mind_entry_inds
- in ()
-
let check_exists_inductive (sp,_) =
if Nametab.exists_cci sp then
errorlabstrm "cache_inductive"
@@ -230,7 +213,7 @@ let (in_inductive, out_inductive) =
let declare_mind mie =
let id = match mie.mind_entry_inds with
- | (id,_,_,_)::_ -> id
+ | ind::_ -> ind.mind_entry_typename
| [] -> anomaly "cannot declare an empty list of inductives"
in
let sp = add_leaf id CCI (in_inductive mie) in
diff --git a/parsing/pretty.ml b/parsing/pretty.ml
index c22e869430..097a88e5a9 100644
--- a/parsing/pretty.ml
+++ b/parsing/pretty.ml
@@ -85,7 +85,9 @@ let print_mutual sp mib =
let pk = kind_of_path sp in
let env = Global.env () in
let evd = Evd.empty in
- let {mind_packets=mipv; mind_nparams=nparams} = mib in
+ let {mind_packets=mipv} = mib in
+ (* On suppose que tous les inductifs ont les même paramètres *)
+ let nparams = mipv.(0).mind_nparams in
let (lpars,_) = decomp_n_prod env evd nparams
(body_of_type (mind_user_arity mipv.(0))) in
let arities = Array.map (fun mip -> (Name mip.mind_typename, None, mip.mind_nf_arity)) mipv in
diff --git a/toplevel/command.ml b/toplevel/command.ml
index caa6d05d67..41085d3508 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -155,13 +155,21 @@ let build_mutual lparams lnamearconstrs finite =
(Environ.push_rel_assum (Name id,p) env, (Name id,p)::params))
(env0,[]) lparams
in
+ (* Pour permettre à terme les let-in dans les params *)
+ let params' =
+ List.map (fun (na,p) ->
+ let id = match na with
+ | Name id -> id
+ | Anonymous -> anomaly "Unnamed inductive variable"
+ in (id, LocalAssum p)) params
+ in
let (ind_env,arityl) =
List.fold_left
(fun (env,arl) (recname,arityc,_) ->
let arity = interp_type sigma env_params arityc in
let fullarity = prod_it arity params in
let env' = Environ.push_rel_assum (Name recname,fullarity) env in
- (env', (fullarity::arl)))
+ (env', (arity::arl)))
(env0,[]) lnamearconstrs
in
let ind_env_params = Environ.push_rels_assum params ind_env in
@@ -169,17 +177,16 @@ let build_mutual lparams lnamearconstrs finite =
List.map2
(fun ar (name,_,lname_constr) ->
let constrnames, bodies = List.split lname_constr in
- let constrs =
- List.map
- (fun c -> prod_it (interp_constr sigma ind_env_params c) params)
- bodies
- in (name, ar, constrnames, constrs))
+ let constrs = List.map (interp_constr sigma ind_env_params) bodies in
+ { mind_entry_nparams = nparams;
+ mind_entry_params = params';
+ mind_entry_typename = name;
+ mind_entry_arity = ar;
+ mind_entry_consnames = constrnames;
+ mind_entry_lc = constrs })
(List.rev arityl) lnamearconstrs
in
- let mie = {
- mind_entry_nparams = nparams;
- mind_entry_finite = finite;
- mind_entry_inds = mispecvec }
+ let mie = { mind_entry_finite = finite; mind_entry_inds = mispecvec }
in
let sp = declare_mind mie in
if is_verbose() then pPNL(minductive_message lrecnames);
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index 25b1383c35..b90f7e4935 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -43,21 +43,21 @@ let abstract_inductive ids_to_abs hyps inds =
list_tabulate (fun k -> applist(mkRel (k+2),[mkRel 1])) ntyp in
let inds' =
List.map
- (function (tname,arity,cnames,lc) ->
+ (function (np,tname,arity,cnames,lc) ->
let arity' = mkNamedProd id t arity in
let lc' =
List.map (fun b -> mkNamedProd id t (substl new_refs b)) lc
in
- (tname,arity',cnames,lc'))
+ (np,tname,arity',cnames,lc'))
inds
in
(inds',ABSTRACT) in
let abstract_one_def id c inds =
List.map
- (function (tname,arity,cnames,lc) ->
+ (function (np,tname,arity,cnames,lc) ->
let arity' = replace_vars [id, c] arity in
let lc' = List.map (replace_vars [id, c]) lc in
- (tname,arity',cnames,lc'))
+ (np,tname,arity',cnames,lc'))
inds in
let abstract_once ((hyps,inds,modl) as sofar) id =
match hyps with
@@ -73,7 +73,24 @@ let abstract_inductive ids_to_abs hyps inds =
List.fold_left abstract_once (hyps,inds,[]) ids_to_abs in
let inds'' =
List.map
- (fun (a,b,c,d) -> (a,body_of_type b,c,List.map body_of_type d))
+ (fun (nparams,a,arity,c,lc) ->
+ let nparams' = nparams + (List.length revmodl) in
+ let params, short_arity = decompose_prod_n_assum nparams' arity in
+ let shortlc =
+ List.map (fun c -> snd (decompose_prod_n_assum nparams' c))lc in
+ let params' =
+ List.map
+ (function
+ | (Name id,None,p) -> id, LocalAssum p
+ | (Name id,Some p,_) -> id, LocalDef p
+ | (Anonymous,_,_) -> anomaly"Unnamed inductive local variable")
+ params in
+ { mind_entry_nparams = nparams';
+ mind_entry_params = params';
+ mind_entry_typename = a;
+ mind_entry_arity = short_arity;
+ mind_entry_consnames = c;
+ mind_entry_lc = shortlc })
inds' in
(inds'', List.rev revmodl)
@@ -83,11 +100,14 @@ let process_inductive osecsp nsecsp oldenv (ids_to_discard,modlist) mib =
let inds =
array_map_to_list
(fun mip ->
- (mip.mind_typename,
- expmod_type oldenv modlist (mind_user_arity mip),
+ let nparams = mip.mind_nparams in
+ let arity = expmod_type oldenv modlist (mind_user_arity mip) in
+ let lc = Array.map (expmod_type oldenv modlist) (mind_user_lc mip) in
+ (nparams,
+ mip.mind_typename,
+ arity,
Array.to_list mip.mind_consnames,
- Array.to_list
- (Array.map (expmod_type oldenv modlist) (mind_user_lc mip))))
+ Array.to_list lc))
mib.mind_packets
in
let hyps' = map_named_context (expmod_constr oldenv modlist) mib.mind_hyps in
@@ -103,8 +123,7 @@ let process_inductive osecsp nsecsp oldenv (ids_to_discard,modlist) mib =
in
let indmodifs,cstrmodifs =
List.split (list_tabulate lmodif_one_mind mib.mind_ntypes) in
- ({ mind_entry_nparams = mib.mind_nparams + (List.length modl);
- mind_entry_finite = finite;
+ ({ mind_entry_finite = finite;
mind_entry_inds = inds' },
indmodifs,
List.flatten cstrmodifs)
@@ -116,13 +135,16 @@ let constant_message id =
let inductive_message inds =
if Options.is_verbose() then
- pPNL (hOV 0
- (match inds with
- | [] -> assert false
- | [(i,_,_,_)] -> [< pr_id i; 'sTR " is discharged." >]
- | l -> [< prlist_with_sep pr_coma
- (fun (id,_,_,_) -> pr_id id) l;
- 'sPC; 'sTR "are discharged.">]))
+ pPNL
+ (hOV 0
+ (match inds with
+ | [] -> assert false
+ | [ind] ->
+ [< pr_id ind.mind_entry_typename; 'sTR " is discharged." >]
+ | l ->
+ [< prlist_with_sep pr_coma
+ (fun ind -> pr_id ind.mind_entry_typename) l;
+ 'sPC; 'sTR "are discharged.">]))
(* Discharge operations for the various objects of the environment. *)
@@ -213,7 +235,7 @@ let process_object oldenv dir sec_sp
let mib = Environ.lookup_mind sp oldenv in
let strobj =
{ s_CONST = info.s_CONST;
- s_PARAM = mib.mind_nparams;
+ s_PARAM = (mind_nth_type_packet mib 0).mind_nparams;
s_PROJ = List.map (option_app (recalc_sp dir)) info.s_PROJ } in
((Struc ((newsp,i),strobj))::ops, ids_to_discard, work_alist)
@@ -254,7 +276,8 @@ let process_operation = function
let push_inductive_names ccitab sp mie =
let _,ccitab =
List.fold_left
- (fun (n,ccitab) (id,_,cnames,_) ->
+ (fun (n,ccitab) ind ->
+ let id = ind.mind_entry_typename in
let indsp = (sp,n) in
let _,ccitab =
List.fold_left
@@ -263,7 +286,7 @@ let push_inductive_names ccitab sp mie =
Stringmap.add (string_of_id x) (ConstructRef (indsp,p))
ccitab))
(1,Stringmap.add (string_of_id id) (IndRef indsp) ccitab)
- cnames in
+ ind.mind_entry_consnames in
(n+1,ccitab))
(0,ccitab)
mie.mind_entry_inds
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 09:53:15 +0000