Skip to content

Commit 6c67c07

Browse files
thomas-lamiauxthomas-lamiaux
committed
change computation of uniform parameters
1 parent 80ca8f9 commit 6c67c07

File tree

3 files changed

+167
-1
lines changed

3 files changed

+167
-1
lines changed

‎kernel/indtypes.ml‎

Lines changed: 109 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -51,6 +51,110 @@ let weaker_noccur_between env x nvars t =
5151

5252
exception InductiveError = Type_errors.InductiveError
5353

54+
(************************************************************************)
55+
(************************************************************************)
56+
(* Compute Uniform Parameters *)
57+
58+
let dbg_uparams = CDebug.create ~name:"uparams" ()
59+
60+
let eta_expand_instantiation ?evars env inst ctxt =
61+
let open Context.Rel.Declaration in
62+
let eta_inst = Array.make (Array.length inst) mkProp in
63+
let rec fold subst i = function
64+
| [] -> assert (Array.length inst = i)
65+
| LocalAssum (_, ty) :: ctx ->
66+
let ty = substl subst ty in
67+
let eta_t = Reduction.eta_expand ?evars env inst.(i) ty in
68+
let () = eta_inst.(i) <- eta_t in
69+
fold (eta_t :: subst) (i + 1) ctx
70+
| LocalDef (_, bd, _) :: ctx ->
71+
fold (bd :: subst) i ctx
72+
in
73+
let () = fold [] 0 (List.rev ctxt) in
74+
eta_inst
75+
76+
let min_array_mapi ar default f = Array.fold_right min (Array.mapi f ar) default
77+
78+
(* Check which parameters are uniform *)
79+
(* let check_cst_iargs env nb_params iargs =
80+
let size_ctx = List.length @@ rel_context env in
81+
let check_rel i k = Int.equal (size_ctx - i) k in
82+
let cst = Array.mapi (fun i t -> match kind t with Rel k -> check_rel i k | _ -> false) iargs in
83+
match Array.findi (fun _ b -> not b) cst with
84+
| Some i -> i
85+
| None -> nb_params *)
86+
87+
let check_cst_iargs env params iargs =
88+
let size_ctx = List.length @@ rel_context env in
89+
let check_rel i k = Int.equal (size_ctx - i) k in
90+
let check_term i t =
91+
let t = Reduction.whd_all env t in
92+
match kind t with
93+
| Rel k -> check_rel i k
94+
| _ -> false
95+
in
96+
let rec check_tel nb_up pos_tel tel =
97+
match tel with
98+
| [] -> nb_up
99+
| LocalDef _ ::tel -> check_tel nb_up (pos_tel+1) tel
100+
| LocalAssum _ :: tel ->
101+
if check_term pos_tel iargs.(nb_up) then
102+
check_tel (nb_up+1) (pos_tel+1) tel
103+
else nb_up
104+
in
105+
check_tel 0 0 @@ List.rev params
106+
107+
(** Computes which uniform parameters are strictly positive in an argument *)
108+
let rec compute_nb_uparams_arg env params nb_nparams arg =
109+
let (local_vars, hd) = Reduction.whd_decompose_prod_decls env arg in
110+
let env = push_rel_context local_vars env in
111+
let (hd, iargs) = decompose_app hd in
112+
match kind hd with
113+
| Rel k ->
114+
(* Check if it is the inductive *)
115+
if List.length (rel_context env) < k then
116+
let iparams = fst @@ Array.chop nb_nparams iargs in
117+
check_cst_iargs env params iparams
118+
else
119+
nb_nparams
120+
| Ind ((kn_nested, _), _) ->
121+
let mib_nested = lookup_mind kn_nested env in
122+
let uparams_nested = List.rev @@ fst @@
123+
Context.Rel.chop_nhyps mib_nested.mind_nparams_rec @@
124+
List.rev mib_nested.mind_params_ctxt in
125+
let inst_uparams = fst @@ Array.chop mib_nested.mind_nparams_rec iargs in
126+
let inst_uparams = eta_expand_instantiation env inst_uparams uparams_nested in
127+
min_array_mapi inst_uparams nb_nparams @@
128+
fun _ t ->
129+
let (loc, hd) = Reduction.whd_decompose_lambda_decls env t in
130+
let env = push_rel_context loc env in
131+
compute_nb_uparams_arg env params nb_nparams hd
132+
| _ -> nb_nparams
133+
134+
let compute_nb_uparams env params inds : int =
135+
let env = set_rel_context_val empty_rel_context_val env in
136+
dbg_uparams Pp.(fun () -> str "size env =" ++ int (List.length @@ rel_context env));
137+
let nb_nparams = Context.Rel.nhyps params in
138+
let env = push_rel_context params env in
139+
min_array_mapi inds nb_nparams @@ fun _ (_, ctors) ->
140+
min_array_mapi ctors nb_nparams @@ fun _ (args, return_type) ->
141+
(* Check Arguments *)
142+
let (env, up_args) =
143+
List.fold_right (
144+
fun arg (env, acc) ->
145+
if Option.has_some @@ get_value arg then
146+
push_rel arg env, acc
147+
else
148+
let arg_up = compute_nb_uparams_arg env params nb_nparams @@ get_type arg in
149+
(push_rel arg env, min acc arg_up)
150+
) args (env, nb_nparams)
151+
in
152+
(* Check Return Type *)
153+
let (_, iargs) = decompose_app return_type in
154+
let iparams = fst @@ Array.chop nb_nparams iargs in
155+
let up_return_type = check_cst_iargs env params iparams in
156+
min up_args up_return_type
157+
54158
(************************************************************************)
55159
(************************************************************************)
56160
(* Positivity *)
@@ -579,10 +683,14 @@ let check_inductive env ~sec_univs kn mie =
579683
let names = Array.map_of_list (fun entry -> entry.mind_entry_typename, entry.mind_entry_consnames)
580684
mie.mind_entry_inds
581685
in
582-
let (nmr,recargs) = check_positivity ~chkpos kn names
686+
let (_,recargs) = check_positivity ~chkpos kn names
583687
env_ar_par paramsctxt mie.mind_entry_finite
584688
(Array.map (fun ((_,lc),(indices,_),_) -> Context.Rel.nhyps indices,lc) inds)
585689
in
690+
(* Compute uniform parameters *)
691+
let nmr = compute_nb_uparams env_ar_par paramsctxt @@
692+
Array.map (fun (_, x, _) -> x) inds in
693+
dbg_uparams Pp.(fun () -> str "UPARAMS = " ++ int nmr);
586694
(* Build the inductive packets *)
587695
let mib =
588696
build_inductive env ~sec_univs names mie.mind_entry_private univs template variance

‎test-suite/output/Inductive.out‎

Lines changed: 48 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -80,3 +80,51 @@ BoxP@{q ; a} may only be eliminated to produce values whose type is SProp or Pro
8080
Arguments BoxP A%_type_scope
8181
Expands to: Inductive Inductive.BoxP
8282
Declared in library Inductive, line 56, characters 22-26
83+
File "./output/Inductive.v", line 62, characters 0-74:
84+
Warning: Cut is nested using Box. No scheme for Box is registered as All.
85+
[register-all,automation,default]
86+
File "./output/Inductive.v", line 62, characters 0-74:
87+
Warning: Cut is nested using Box. No scheme for Box is registered as All.
88+
[register-all,automation,default]
89+
File "./output/Inductive.v", line 62, characters 0-74:
90+
Warning: Cut is nested using Box. No scheme for Box is registered as All.
91+
[register-all,automation,default]
92+
File "./output/Inductive.v", line 62, characters 0-74:
93+
Warning: Cut is nested using Box. No scheme for Box is registered as All.
94+
[register-all,automation,default]
95+
File "./output/Inductive.v", line 62, characters 0-74:
96+
Warning: Cut is nested using Box. No scheme for Box is registered as All.
97+
[register-all,automation,default]
98+
File "./output/Inductive.v", line 62, characters 0-74:
99+
Warning: Cut is nested using Box. No scheme for Box is registered as All.
100+
[register-all,automation,default]
101+
File "./output/Inductive.v", line 62, characters 0-74:
102+
Warning: Cut is nested using Box. No scheme for Box is registered as All.
103+
[register-all,automation,default]
104+
File "./output/Inductive.v", line 62, characters 0-74:
105+
Warning: Cut is nested using Box. No scheme for Box is registered as All.
106+
[register-all,automation,default]
107+
File "./output/Inductive.v", line 62, characters 0-74:
108+
Warning: Cut is nested using Box. No scheme for Box is registered as All.
109+
[register-all,automation,default]
110+
File "./output/Inductive.v", line 62, characters 0-74:
111+
Warning: Cut is nested using Box. No scheme for Box is registered as All.
112+
[register-all,automation,default]
113+
File "./output/Inductive.v", line 62, characters 0-74:
114+
Warning: Cut is nested using Box. No scheme for Box is registered as All.
115+
[register-all,automation,default]
116+
File "./output/Inductive.v", line 62, characters 0-74:
117+
Warning: Cut is nested using Box. No scheme for Box is registered as All.
118+
[register-all,automation,default]
119+
Cut_ind@{u} :
120+
forall P : forall x : unit, Cut@{u} x -> Prop,
121+
(forall (x : unit) (b : Box@{u u} (fun n : unit => Cut@{u} n)),
122+
P x (triv@{u} x b)) ->
123+
forall (x : unit) (c : Cut@{u} x), P x c
124+
(* u |= *)
125+
126+
Cut_ind is universe polymorphic
127+
Arguments Cut_ind (P triv)%_function_scope x c
128+
Cut_ind is transparent
129+
Expands to: Constant Inductive.Cut_ind
130+
Declared in library Inductive, line 62, characters 0-74

‎test-suite/output/Inductive.v‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -56,3 +56,13 @@ About ssig.
5656
Polymorphic Inductive BoxP@{q;a|} (A:Type@{q;a}) : Prop := boxP (_:A).
5757

5858
About BoxP.
59+
60+
Variant Box (F : unit -> Type) := .
61+
62+
Inductive Cut (x : unit) : Type :=
63+
| triv : Box (fun n => Cut n) -> Cut x.
64+
65+
About Cut_ind.
66+
67+
68+

0 commit comments

Comments
 (0)