aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--kernel/indtypes.ml22
-rw-r--r--library/impargs.ml4
-rw-r--r--library/indrec.ml8
-rw-r--r--parsing/pretty.ml49
-rw-r--r--toplevel/discharge.ml12
5 files changed, 46 insertions, 49 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 979d24536..197f5c299 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -315,12 +315,30 @@ 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
+ (make_typed_lazy (prod_it (mkSort ar_sort) ar_sign)
+ (fun _ -> level_of_type ar)),
+ Some (body_of_type 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 env Evd.empty) lc_bodies in
+ let nf_lc = Array.map (fun (d,b) -> prod_it 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
{ mind_consnames = Array.of_list cnames;
mind_typename = id;
- mind_lc = lc;
+ mind_user_lc = user_lc;
+ mind_nf_lc = nf_typed_lc;
+ mind_user_arity = user_ar;
+ mind_nf_arity = nf_ar;
mind_nrealargs = List.length ar_sign - nparams;
- mind_arity = ar;
mind_sort = ar_sort;
mind_kelim = kelim;
mind_listrec = recargs;
diff --git a/library/impargs.ml b/library/impargs.ml
index 5b52f1976..bae96bc14 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 (body_of_type mip.mind_arity),
- Array.map (fun c -> auto_implicits (body_of_type c)) mip.mind_lc)
+ (auto_implicits (mind_user_arity mip),
+ Array.map (fun c -> auto_implicits 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/library/indrec.ml b/library/indrec.ml
index da5aeec34..d24ce2aa6 100644
--- a/library/indrec.ml
+++ b/library/indrec.ml
@@ -52,7 +52,7 @@ let mis_make_case_com depopt env sigma mispec kind =
if k = mis_nconstr mispec then
let nbprod = k+1 in
let ind = make_ind_family (mispec,rel_list nbprod nparams) in
- let lnamesar,_ = get_arity env' sigma ind in
+ let lnamesar,_ = get_arity ind in
let ci = make_default_case_info mispec in
it_lambda_name env'
(lambda_create env'
@@ -69,7 +69,7 @@ let mis_make_case_com depopt env sigma mispec kind =
(add_branch (k+1))
in
let indf = make_ind_family (mispec,rel_list 0 nparams) in
- let typP = make_arity env' sigma dep indf kind in
+ let typP = make_arity env' dep indf kind in
it_lambda_name env (mkLambda_string "P" typP (add_branch 0)) lnamespar
(* check if the type depends recursively on one of the inductive scheme *)
@@ -210,7 +210,7 @@ let mis_make_indrec env sigma listdepkind mispec =
(* arity in the context P1..P_nrec f1..f_nbconstruct *)
let params = rel_list (nrec+nbconstruct) nparams in
let indf = make_ind_family (mispeci,params) in
- let lnames,_ = get_arity env sigma indf in
+ let lnames,_ = get_arity indf in
let nar = mis_nrealargs mispeci in
let decf = nar+nrec+nbconstruct+nrec in
@@ -281,7 +281,7 @@ let mis_make_indrec env sigma listdepkind mispec =
let rec put_arity i = function
| (mispeci,dep,kinds)::rest ->
let indf = make_ind_family (mispeci,rel_list i nparams) in
- let typP = make_arity env sigma dep indf kinds in
+ let typP = make_arity env dep indf kinds in
mkLambda_string "P" typP (put_arity (i+1) rest)
| [] ->
make_branch 0 listdepkind
diff --git a/parsing/pretty.ml b/parsing/pretty.ml
index c7fcbd729..9d189edfc 100644
--- a/parsing/pretty.ml
+++ b/parsing/pretty.ml
@@ -130,7 +130,7 @@ 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 (body_of_type mipv.(0).mind_arity) in
+ let (lpars,_) = decomp_n_prod env evd nparams (mind_user_arity mipv.(0)) in
let lparsname = List.map fst lpars in
let lna = Array.map (fun mip -> Name mip.mind_typename) mipv in
let lparsprint = assumptions_for_print lparsname in
@@ -138,20 +138,18 @@ let print_mutual sp mib =
let pc = pterminenv ass_name c in [< print_id id; 'sTR " : "; pc >]
in
let print_constructors mip =
- let lC = mip.mind_lc in
+ let lC = mind_user_lc mip in
let ass_name = assumptions_for_print (lparsname@(Array.to_list lna)) in
let lidC =
Array.to_list
- (array_map2
- (fun id c ->
- (id,snd (decomp_n_prod env evd nparams (body_of_type c))))
+ (array_map2 (fun id c -> (id,snd (decomp_n_prod env evd nparams c)))
mip.mind_consnames lC) in
let plidC = prlist_with_sep (fun () -> [<'bRK(1,0); 'sTR "| " >])
(prass ass_name) lidC in
(hV 0 [< 'sTR " "; plidC >])
in
let print_oneind mip =
- let (_,arity) = decomp_n_prod env evd nparams (body_of_type mip.mind_arity) in
+ let (_,arity) = decomp_n_prod env evd nparams (mind_user_arity mip) in
(hOV 0
[< (hOV 0
[< print_id mip.mind_typename ; 'bRK(1,2);
@@ -166,7 +164,7 @@ 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 (body_of_type mip.mind_arity) in
+ let (_,arity) = decomp_n_prod env evd nparams (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
@@ -327,45 +325,18 @@ let list_filter_vec f vec =
in
frec (Array.length vec -1) []
- (* The four functions print_constructors_head, print_all_constructors_head,
- print_constructors_rel and crible implement the behavior needed for the
- Coq Search command. These functions take as first argument the procedure
+ (* The functions print_constructors and crible implement the behavior needed
+ for the Coq Search command.
+ These functions take as first argument the procedure
that will be called to treat each entry. This procedure receives the name
of the object, the assumptions that will make it possible to print its type,
and the constr term that represent its type. *)
-(*
-let print_constructors_head
- (fn : string -> unit assumptions -> constr -> unit) c lna mip =
- let lC = mip.mind_lc in
- let ass_name = assumptions_for_print lna in
- let lidC = array_map2 (fun id c_0 -> (id,c_0)) mip.mind_consnames lC in
- let flid = list_filter_vec (fun (_,c_0) -> head_const (body_of_type c_0) = c) lidC in
- List.iter
- (function (id,c_0) -> fn (string_of_id id) ass_name (body_of_type c_0)) flid
-
-let print_all_constructors_head fn c mib =
- let mipvec = mib.mind_packets
- and n = mib.mind_ntypes in
- let lna = array_map_to_list (fun mip -> Name mip.mind_typename) mipvec in
- for i = 0 to n-1 do
- print_constructors_head fn c lna mipvec.(i)
- done
-
-let print_constructors_rel fn lna mip =
- let lC = mip.mind_lc in
- let ass_name = assumptions_for_print lna in
- let lidC = array_map2 (fun id c -> (id,c)) mip.mind_consnames lC in
- let flid = list_filter_vec (fun (_,c) -> isRel (head_const (body_of_type c))) lidC in
- List.iter (function (id,c) -> fn (string_of_id id) ass_name (body_of_type c))
- flid
-*)
-
let print_constructors fn lna mip =
let ass_name = assumptions_for_print lna in
let _ =
- array_map2 (fun id c -> fn (string_of_id id) ass_name (body_of_type c))
- mip.mind_consnames mip.mind_lc
+ array_map2 (fun id c -> fn (string_of_id id) ass_name c)
+ mip.mind_consnames (mind_user_lc mip)
in ()
let crible (fn : string -> unit assumptions -> constr -> unit) name =
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index da223b541..ebf70569d 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -207,9 +207,17 @@ let process_inductive osecsp nsecsp oldenv (ids_to_discard,modlist) mib =
array_map_to_list
(fun mip ->
(mip.mind_typename,
- expmod_type oldenv modlist mip.mind_arity,
+ make_typed_lazy
+ (expmod_constr oldenv modlist (mind_user_arity mip))
+ (fun _ -> level_of_type mip.mind_nf_arity),
Array.to_list mip.mind_consnames,
- array_map_to_list (expmod_type oldenv modlist) mip.mind_lc))
+ 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)))
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-29 07:39:28 +0000