aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--kernel/declarations.ml8
-rw-r--r--kernel/declarations.mli8
-rw-r--r--kernel/indtypes.ml26
-rw-r--r--kernel/inductive.ml33
-rw-r--r--kernel/inductive.mli6
-rw-r--r--kernel/typeops.ml10
-rw-r--r--kernel/univ.ml4
-rw-r--r--library/global.ml5
-rw-r--r--library/global.mli4
-rw-r--r--library/impargs.ml4
-rw-r--r--parsing/pretty.ml21
-rw-r--r--pretyping/cases.ml4
-rw-r--r--tactics/equality.ml4
-rw-r--r--tactics/hipattern.ml6
-rw-r--r--toplevel/discharge.ml11
15 files changed, 79 insertions, 75 deletions
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 9c6ffb172..c09254c2c 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -50,8 +50,8 @@ type one_inductive_body = {
mind_nf_lc : typed_type array;
mind_nf_arity : typed_type;
(* lc and arity as given by user if not in nf; useful e.g. for Ensemble.v *)
- mind_user_lc : constr array option;
- mind_user_arity : constr option;
+ mind_user_lc : typed_type array option;
+ mind_user_arity : typed_type option;
mind_sort : sorts;
mind_nrealargs : int;
mind_kelim : sorts list;
@@ -70,11 +70,11 @@ type mutual_inductive_body = {
let mind_type_finite mib i = mib.mind_packets.(i).mind_finite
let mind_user_lc mip = match mip.mind_user_lc with
- | None -> Array.map body_of_type mip.mind_nf_lc
+ | None -> mip.mind_nf_lc
| Some lc -> lc
let mind_user_arity mip = match mip.mind_user_arity with
- | None -> body_of_type mip.mind_nf_arity
+ | None -> mip.mind_nf_arity
| Some a -> a
(*s Declaration. *)
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 4cfb3e2ab..0c8b15e3c 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -55,8 +55,8 @@ type one_inductive_body = {
mind_typename : identifier;
mind_nf_lc : typed_type array; (* constrs and arity with pre-expanded ccl *)
mind_nf_arity : typed_type;
- mind_user_lc : constr array option;
- mind_user_arity : constr option;
+ mind_user_lc : typed_type array option;
+ mind_user_arity : typed_type option;
mind_sort : sorts;
mind_nrealargs : int;
mind_kelim : sorts list;
@@ -73,8 +73,8 @@ type mutual_inductive_body = {
mind_nparams : int }
val mind_type_finite : mutual_inductive_body -> int -> bool
-val mind_user_lc : one_inductive_body -> constr array
-val mind_user_arity : one_inductive_body -> constr
+val mind_user_lc : one_inductive_body -> typed_type array
+val mind_user_arity : one_inductive_body -> typed_type
val mind_nth_type_packet : mutual_inductive_body -> int -> one_inductive_body
(*s Declaration of inductive types. *)
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index c29d4385d..74b1a7602 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -206,7 +206,7 @@ let listrec_mconstr env ntypes nparams i indlc =
let (lpar,auxlargs) = list_chop auxnpar largs in
if not (List.for_all (noccur_between n ntypes) auxlargs) then
raise (IllFormedInd (LocalNonPos n));
- let auxlc = mis_lc mispeci
+ let auxlc = mis_nf_lc mispeci
and auxntyp = mis_ntypes mispeci in
if auxntyp <> 1 then raise (IllFormedInd (LocalNonPos n));
let lrecargs = List.map (check_weak_pos n) lpar in
@@ -313,28 +313,28 @@ let cci_inductive env env_ar kind nparams finite inds cst =
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
+
let nf_ar,user_ar =
if isArity (body_of_type ar) then ar,None
- else
+ else
(make_typed_lazy (prod_it (mkSort ar_sort) ar_sign)
(fun _ -> level_of_type ar)),
- Some (body_of_type ar) in
+ Some ar in
let kelim = allowed_sorts issmall isunit ar_sort in
let lc_bodies = Array.map body_of_type lc in
+
let splayed_lc = Array.map (splay_prod_assum env Evd.empty) lc_bodies in
- let nf_lc = Array.map
- (fun (d,b) -> it_mkProd_or_LetIn b d) splayed_lc in
- let nf_typed_lc,user_lc =
- if nf_lc = lc_bodies then lc,None
- else
- (array_map2
- (fun nfc c -> make_typed_lazy nfc (fun _ -> level_of_type c))
- nf_lc lc),
- Some lc_bodies in
+ let nf_lc =
+ array_map2
+ (fun (d,b) c ->
+ make_typed_lazy
+ (it_mkProd_or_LetIn b d) (fun _ -> level_of_type c))
+ splayed_lc lc in
+ let nf_lc,user_lc = if nf_lc = lc then lc,None else nf_lc, Some lc in
{ mind_consnames = Array.of_list cnames;
mind_typename = id;
mind_user_lc = user_lc;
- mind_nf_lc = nf_typed_lc;
+ mind_nf_lc = nf_lc;
mind_user_arity = user_ar;
mind_nf_arity = nf_ar;
mind_nrealargs = List.length ar_sign - nparams;
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index bbc7918dc..3436bf962 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -40,20 +40,26 @@ let mis_typepath mis =
let mis_consnames mis = mis.mis_mip.mind_consnames
let mis_inductive mis = ((mis.mis_sp,mis.mis_tyi),mis.mis_args)
-let mis_typed_lc mis =
+let mis_typed_nf_lc mis =
let sign = mis.mis_mib.mind_hyps in
let args = Array.to_list mis.mis_args in
Array.map (fun t -> Instantiate.instantiate_type sign t args)
mis.mis_mip.mind_nf_lc
-let mis_lc mis = Array.map body_of_type (mis_typed_lc mis)
+let mis_nf_lc mis = Array.map body_of_type (mis_typed_nf_lc mis)
+
+let mis_user_lc mis =
+ let sign = mis.mis_mib.mind_hyps in
+ let args = Array.to_list mis.mis_args in
+ Array.map (fun t -> Instantiate.instantiate_type sign t args)
+ (mind_user_lc mis.mis_mip)
(* 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
+ let specif = Array.map body_of_type (mis_user_lc mispec)
and ntypes = mis_ntypes mispec
and nconstr = mis_nconstr mispec in
let make_Ik k = mkMutInd ((mispec.mis_sp,ntypes-k-1),mispec.mis_args)
@@ -64,7 +70,7 @@ let mis_type_mconstructs mispec =
Array.map (substl (list_tabulate make_Ik ntypes)) specif)
let mis_type_nf_mconstruct i mispec =
- let specif = mis_lc mispec
+ let specif = mis_nf_lc mispec
and ntypes = mis_ntypes mispec
and nconstr = mis_nconstr mispec in
let make_Ik k = mkMutInd ((mispec.mis_sp,ntypes-k-1),mispec.mis_args) in
@@ -72,28 +78,27 @@ let mis_type_nf_mconstruct i mispec =
substl (list_tabulate make_Ik ntypes) specif.(i-1)
let mis_type_mconstruct i mispec =
- let specif = mis_typed_lc mispec
+ let specif = mis_user_lc mispec
and ntypes = mis_ntypes mispec
and nconstr = mis_nconstr mispec in
let make_Ik k = mkMutInd ((mispec.mis_sp,ntypes-k-1),mispec.mis_args) in
if i > nconstr then error "Not enough constructors in the type";
typed_app (substl (list_tabulate make_Ik ntypes)) specif.(i-1)
-let mis_typed_arity mis =
+let mis_user_arity mis =
let hyps = mis.mis_mib.mind_hyps
and largs = Array.to_list mis.mis_args in
- Instantiate.instantiate_type hyps mis.mis_mip.mind_nf_arity largs
+ Instantiate.instantiate_type hyps (mind_user_arity mis.mis_mip) largs
-(*
-let mis_arity mispec = incast_type (mis_typed_arity mispec)
-*)
-
-let mis_arity mis = body_of_type (mis_typed_arity mis)
+let mis_nf_arity mis =
+ let hyps = mis.mis_mib.mind_hyps
+ and largs = Array.to_list mis.mis_args in
+ Instantiate.instantiate_type hyps mis.mis_mip.mind_nf_arity largs
let mis_params_ctxt mispec =
let paramsign,_ =
decompose_prod_n_assum mispec.mis_mib.mind_nparams
- (body_of_type (mis_typed_arity mispec))
+ (body_of_type (mis_nf_arity mispec))
in paramsign
let mis_sort mispec = mispec.mis_mip.mind_sort
@@ -250,7 +255,7 @@ let get_constructors (IndFamily (mispec,params) as indf) =
Array.init (mis_nconstr mispec) (fun j -> get_constructor indf (j+1))
let get_arity (IndFamily (mispec,params)) =
- let arity = mis_arity mispec in
+ let arity = body_of_type (mis_nf_arity mispec) in
destArity (prod_applist arity params)
(* Functions to build standard types related to inductive *)
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index 3b45dad0b..727ccf409 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -42,15 +42,15 @@ 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_nf_arity : inductive_instance -> typed_type
+val mis_user_arity : inductive_instance -> typed_type
val mis_params_ctxt : inductive_instance -> rel_context
val mis_sort : inductive_instance -> sorts
val mis_type_mconstruct : int -> inductive_instance -> typed_type
(* The ccl of constructor is pre-normalised in the following functions *)
-val mis_lc : inductive_instance -> constr array
+val mis_nf_lc : inductive_instance -> constr array
val mis_type_mconstructs : inductive_instance -> constr array * constr array
(*s [inductive_family] = [inductive_instance] applied to global parameters *)
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 74b207209..8421a0543 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -83,15 +83,7 @@ let type_of_constant = Instantiate.constant_type
(* Inductive types. *)
-(* Q: A faire disparaitre ??
-let instantiate_arity mis =
- let ids = ids_of_sign mis.mis_mib.mind_hyps in
- let args = Array.to_list mis.mis_args in
- let arity = mis.mis_mip.mind_arity in
- { body = instantiate_constr ids arity.body args;
- typ = arity.typ }
-*)
-let instantiate_arity = mis_typed_arity
+let instantiate_arity = mis_user_arity
let type_of_inductive env sigma i =
(* TODO: check args *)
diff --git a/kernel/univ.ml b/kernel/univ.ml
index f179bd370..76fc0b12a 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -403,8 +403,10 @@ let pr_reln u r =
| Terminal -> [< >]
in
prec r
-
+
let pr_universes g =
let graph = UniverseMap.fold (fun k a l -> (k,a)::l) g [] in
prlist_with_sep pr_fnl (function (_,Arc(u,r)) -> pr_reln u r) graph
+
+
diff --git a/library/global.ml b/library/global.ml
index e58f1b03b..96fb689a3 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -66,7 +66,8 @@ let mind_is_recursive =
let mind_nconstr = Util.compose Inductive.mis_nconstr lookup_mind_specif
let mind_nparams = Util.compose Inductive.mis_nparams lookup_mind_specif
-let mind_arity = Util.compose Inductive.mis_arity lookup_mind_specif
-let mind_lc = Util.compose Inductive.mis_lc lookup_mind_specif
+let mind_nf_arity x =
+ body_of_type (Inductive.mis_user_arity (lookup_mind_specif x))
+let mind_nf_lc = Util.compose Inductive.mis_nf_lc lookup_mind_specif
diff --git a/library/global.mli b/library/global.mli
index 4a993d1aa..16ed53785 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -56,6 +56,6 @@ val id_of_global : global_reference -> identifier
val mind_is_recursive : inductive -> bool
val mind_nconstr : inductive -> int
val mind_nparams : inductive -> int
-val mind_arity : inductive -> constr
-val mind_lc : inductive -> constr array
+val mind_nf_arity : inductive -> constr
+val mind_nf_lc : inductive -> constr array
diff --git a/library/impargs.ml b/library/impargs.ml
index 242b634f7..b756a1f99 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -67,8 +67,8 @@ let inductives_table = ref Spmap.empty
let declare_inductive_implicits sp =
let mib = Global.lookup_mind sp in
let imps_one_inductive mip =
- (auto_implicits (mind_user_arity mip),
- Array.map (fun c -> auto_implicits c) (mind_user_lc mip))
+ (auto_implicits (body_of_type (mind_user_arity mip)),
+ Array.map (fun c -> auto_implicits (body_of_type c)) (mind_user_lc mip))
in
let imps = Array.map imps_one_inductive mib.mind_packets in
inductives_table := Spmap.add sp imps !inductives_table
diff --git a/parsing/pretty.ml b/parsing/pretty.ml
index 1ae401dc3..3502d9ecf 100644
--- a/parsing/pretty.ml
+++ b/parsing/pretty.ml
@@ -120,7 +120,8 @@ let print_mutual sp mib =
let env = Global.env () in
let evd = Evd.empty in
let {mind_packets=mipv; mind_nparams=nparams} = mib in
- let (lpars,_) = decomp_n_prod env evd nparams (mind_user_arity mipv.(0)) 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
let env_ar = push_rels lpars env in
let env_cstr = push_rels lpars (push_rels (Array.to_list arities) env) in
@@ -131,14 +132,17 @@ let print_mutual sp mib =
let lC = mind_user_lc mip in
let lidC =
Array.to_list
- (array_map2 (fun id c -> (id,snd (decomp_n_prod env evd nparams c)))
+ (array_map2
+ (fun id c ->
+ (id,snd (decomp_n_prod env evd nparams (body_of_type c))))
mip.mind_consnames lC) in
let plidC = prlist_with_sep (fun () -> [<'bRK(1,0); 'sTR "| " >])
pr_constructor lidC in
(hV 0 [< 'sTR " "; plidC >])
in
let print_oneind mip =
- let (_,arity) = decomp_n_prod env evd nparams (mind_user_arity mip) in
+ let (_,arity) = decomp_n_prod env evd nparams
+ (body_of_type (mind_user_arity mip)) in
(hOV 0
[< (hOV 0
[< print_id mip.mind_typename ; 'bRK(1,2);
@@ -152,7 +156,8 @@ let print_mutual sp mib =
let mip = mipv.(0) in
(* Case one [co]inductive *)
if Array.length mipv = 1 then
- let (_,arity) = decomp_n_prod env evd nparams (mind_user_arity mip) in
+ let (_,arity) = decomp_n_prod env evd nparams
+ (body_of_type (mind_user_arity mip)) in
let sfinite = if mip.mind_finite then "Inductive " else "CoInductive " in
(hOV 0 [< 'sTR sfinite ; print_id mip.mind_typename ;
if nparams = 0 then
@@ -324,7 +329,7 @@ let list_filter_vec f vec =
let print_constructors fn env_ar mip =
let _ =
- array_map2 (fun id c -> fn (string_of_id id) env_ar c)
+ array_map2 (fun id c -> fn (string_of_id id) env_ar (body_of_type c))
mip.mind_consnames (mind_user_lc mip)
in ()
@@ -347,7 +352,11 @@ let crible (fn : string -> env -> constr -> unit) name =
crible_rec rest
| (sp,"INDUCTIVE") ->
let mib = Global.lookup_mind sp in
- let arities = array_map_to_list (fun mip -> (Name mip.mind_typename, None, mip.mind_nf_arity)) mib.mind_packets in
+ let arities =
+ array_map_to_list
+ (fun mip ->
+ (Name mip.mind_typename, None, mip.mind_nf_arity))
+ mib.mind_packets in
let env_ar = push_rels arities env in
(match kind_of_term const with
| IsMutInd ((sp',tyi),_) ->
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 3b3c09d38..e1ab02b73 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -895,7 +895,9 @@ let rec find_row_ind = function
exception NotCoercible
let inh_coerce_to_ind isevars env ty tyi =
- let (ntys,_) = splay_prod env !isevars (mis_arity (Global.lookup_mind_specif tyi)) in
+ let (ntys,_) =
+ splay_prod env !isevars
+ (body_of_type (mis_nf_arity (Global.lookup_mind_specif tyi))) in
let (_,evarl) =
List.fold_right
(fun (na,ty) (env,evl) ->
diff --git a/tactics/equality.ml b/tactics/equality.ml
index e0a8c8541..c27aeb195 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -566,7 +566,7 @@ let gen_absurdity id gl =
let discrimination_pf e (t,t1,t2) discriminator lbeq gls =
let env = pf_env gls in
let (indt,_) = find_mrectype env (project gls) t in
- let arity = Global.mind_arity indt in
+ let arity = Global.mind_nf_arity indt in
let sort = pf_type_of gls (pf_concl gls) in
match necessary_elimination (snd (destArity arity)) (destSort sort) with
| Type_Type ->
@@ -611,7 +611,7 @@ let discr id gls =
let discriminator =
build_discriminator sigma e_env dirn (mkVar e) sort cpath in
let (indt,_) = find_mrectype env sigma t in
- let arity = Global.mind_arity indt in
+ let arity = Global.mind_nf_arity indt in
let (pf, absurd_term) =
discrimination_pf e (t,t1,t2) discriminator lbeq gls
in
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index 1f78dcb85..944d82605 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -135,7 +135,7 @@ let match_with_disjunction t =
match kind_of_term hdapp with
| IsMutInd ind ->
let mispec = Global.lookup_mind_specif ind in
- let constr_types = mis_lc mispec in
+ let constr_types = mis_nf_lc mispec in
let only_one_arg c =
((nb_prod c) - (mis_nparams mispec)) = 1 in
if (array_for_all only_one_arg constr_types) &&
@@ -162,7 +162,7 @@ let match_with_unit_type t =
let (hdapp,args) = decomp_app t in
match (kind_of_term hdapp) with
| IsMutInd ind ->
- let constr_types = Global.mind_lc ind in
+ let constr_types = Global.mind_nf_lc ind in
let nconstr = Global.mind_nconstr ind in
let zero_args c = ((nb_prod c) - (Global.mind_nparams ind)) = 0 in
if nconstr = 1 && (array_for_all zero_args constr_types) then
@@ -185,7 +185,7 @@ let match_with_equation t =
let (hdapp,args) = decomp_app t in
match (kind_of_term hdapp) with
| IsMutInd ind ->
- let constr_types = Global.mind_lc ind in
+ let constr_types = Global.mind_nf_lc ind in
let nconstr = Global.mind_nconstr ind in
if nconstr = 1 &&
(is_matching (get_pat refl_rel_pat1) constr_types.(0) ||
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index dc6f01d34..805e4ffc0 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -230,17 +230,10 @@ let process_inductive osecsp nsecsp oldenv (ids_to_discard,modlist) mib =
array_map_to_list
(fun mip ->
(mip.mind_typename,
- make_typed_lazy
- (expmod_constr oldenv modlist (mind_user_arity mip))
- (fun _ -> level_of_type mip.mind_nf_arity),
+ expmod_type oldenv modlist (mind_user_arity mip),
Array.to_list mip.mind_consnames,
Array.to_list
- (array_map2
- (fun us nfc ->
- make_typed_lazy
- (expmod_constr oldenv modlist us)
- (fun _ -> level_of_type nfc))
- (mind_user_lc mip) mip.mind_nf_lc)))
+ (Array.map (expmod_type oldenv modlist) (mind_user_lc mip))))
mib.mind_packets
in
let (inds',modl) = abstract_inductive ids_to_discard mib.mind_hyps inds in
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 04:08:07 +0000