From 6176c2879dd989029a83642caec7cd66a2a4f527 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 29 Jul 2019 10:34:47 +0200 Subject: Move cumulativity inference to the kernel. This is not quite pretty, but it is needed by the section mechanism to rebuild an inductive when closing a section. Hopefully this can be moved back at some point. --- kernel/inferCumulativity.ml | 233 +++++++++++++++++++++++++++++++++++++++ kernel/inferCumulativity.mli | 14 +++ kernel/kernel.mllib | 1 + pretyping/inferCumulativity.ml | 234 ---------------------------------------- pretyping/inferCumulativity.mli | 14 --- pretyping/pretyping.mllib | 1 - 6 files changed, 248 insertions(+), 249 deletions(-) create mode 100644 kernel/inferCumulativity.ml create mode 100644 kernel/inferCumulativity.mli delete mode 100644 pretyping/inferCumulativity.ml delete mode 100644 pretyping/inferCumulativity.mli diff --git a/kernel/inferCumulativity.ml b/kernel/inferCumulativity.ml new file mode 100644 index 0000000000..8b5b254f45 --- /dev/null +++ b/kernel/inferCumulativity.ml @@ -0,0 +1,233 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* Covariant so nontrivial *) + LMap.update u (function + | None -> None + | Some CovariantI as x -> x + | Some IrrelevantI -> Some CovariantI) + variances + +let infer_generic_instance_eq variances u = + Array.fold_left (fun variances u -> infer_level_eq u variances) + variances (Instance.to_array u) + +let infer_cumulative_ind_instance cv_pb mind_variance variances u = + Array.fold_left2 (fun variances varu u -> + match cv_pb, varu with + | _, Irrelevant -> variances + | _, Invariant | CONV, Covariant -> infer_level_eq u variances + | CUMUL, Covariant -> infer_level_leq u variances) + variances mind_variance (Instance.to_array u) + +let infer_inductive_instance cv_pb env variances ind nargs u = + let mind = Environ.lookup_mind (fst ind) env in + match mind.mind_variance with + | None -> infer_generic_instance_eq variances u + | Some mind_variance -> + if not (Int.equal (inductive_cumulativity_arguments (mind,snd ind)) nargs) + then infer_generic_instance_eq variances u + else infer_cumulative_ind_instance cv_pb mind_variance variances u + +let infer_constructor_instance_eq env variances ((mi,ind),ctor) nargs u = + let mind = Environ.lookup_mind mi env in + match mind.mind_variance with + | None -> infer_generic_instance_eq variances u + | Some _ -> + if not (Int.equal (constructor_cumulativity_arguments (mind,ind,ctor)) nargs) + then infer_generic_instance_eq variances u + else variances (* constructors are convertible at common supertype *) + +let infer_sort cv_pb variances s = + match cv_pb with + | CONV -> + LSet.fold infer_level_eq (Universe.levels (Sorts.univ_of_sort s)) variances + | CUMUL -> + LSet.fold infer_level_leq (Universe.levels (Sorts.univ_of_sort s)) variances + +let infer_table_key _infos variances c = + let open Names in + match c with + | ConstKey (_, u) -> + infer_generic_instance_eq variances u + | VarKey _ | RelKey _ -> variances + +let whd_stack (infos, tab) hd stk = CClosure.whd_stack infos tab hd stk + +let rec infer_fterm cv_pb infos variances hd stk = + Control.check_for_interrupt (); + let hd,stk = whd_stack infos hd stk in + let open CClosure in + match fterm_of hd with + | FAtom a -> + begin match kind a with + | Sort s -> infer_sort cv_pb variances s + | Meta _ -> infer_stack infos variances stk + | _ -> assert false + end + | FEvar ((_,args),e) -> + let variances = infer_stack infos variances stk in + infer_vect infos variances (Array.map (mk_clos e) args) + | FRel _ -> infer_stack infos variances stk + | FInt _ -> infer_stack infos variances stk + | FFlex fl -> + let variances = infer_table_key infos variances fl in + infer_stack infos variances stk + | FProj (_,c) -> + let variances = infer_fterm CONV infos variances c [] in + infer_stack infos variances stk + | FLambda _ -> + let (_,ty,bd) = destFLambda mk_clos hd in + let variances = infer_fterm CONV infos variances ty [] in + infer_fterm CONV infos variances bd [] + | FProd (_,dom,codom,e) -> + let variances = infer_fterm CONV infos variances dom [] in + infer_fterm cv_pb infos variances (mk_clos (Esubst.subs_lift e) codom) [] + | FInd (ind, u) -> + let variances = + if Instance.is_empty u then variances + else + let nargs = stack_args_size stk in + infer_inductive_instance cv_pb (info_env (fst infos)) variances ind nargs u + in + infer_stack infos variances stk + | FConstruct (ctor,u) -> + let variances = + if Instance.is_empty u then variances + else + let nargs = stack_args_size stk in + infer_constructor_instance_eq (info_env (fst infos)) variances ctor nargs u + in + infer_stack infos variances stk + | FFix ((_,(_,tys,cl)),e) | FCoFix ((_,(_,tys,cl)),e) -> + let n = Array.length cl in + let variances = infer_vect infos variances (Array.map (mk_clos e) tys) in + let le = Esubst.subs_liftn n e in + let variances = infer_vect infos variances (Array.map (mk_clos le) cl) in + infer_stack infos variances stk + + (* Removed by whnf *) + | FLOCKED | FCaseT _ | FLetIn _ | FApp _ | FLIFT _ | FCLOS _ -> assert false + +and infer_stack infos variances (stk:CClosure.stack) = + match stk with + | [] -> variances + | z :: stk -> + let open CClosure in + let variances = match z with + | Zapp v -> infer_vect infos variances v + | Zproj _ -> variances + | Zfix (fx,a) -> + let variances = infer_fterm CONV infos variances fx [] in + infer_stack infos variances a + | ZcaseT (_, p, br, e) -> + let variances = infer_fterm CONV infos variances (mk_clos e p) [] in + infer_vect infos variances (Array.map (mk_clos e) br) + | Zshift _ -> variances + | Zupdate _ -> variances + | Zprimitive (_,_,rargs,kargs) -> + let variances = List.fold_left (fun variances c -> infer_fterm CONV infos variances c []) variances rargs in + let variances = List.fold_left (fun variances (_,c) -> infer_fterm CONV infos variances c []) variances kargs in + variances + in + infer_stack infos variances stk + +and infer_vect infos variances v = + Array.fold_left (fun variances c -> infer_fterm CONV infos variances c []) variances v + +let infer_term cv_pb env variances c = + let open CClosure in + let infos = (create_clos_infos all env, create_tab ()) in + infer_fterm cv_pb infos variances (CClosure.inject c) [] + +let infer_arity_constructor is_arity env variances arcn = + let infer_typ typ (env,variances) = + match typ with + | Context.Rel.Declaration.LocalAssum (_, typ') -> + (Environ.push_rel typ env, infer_term CUMUL env variances typ') + | Context.Rel.Declaration.LocalDef _ -> assert false + in + let typs, codom = Reduction.dest_prod env arcn in + let env, variances = Context.Rel.fold_outside infer_typ typs ~init:(env, variances) in + (* If we have Inductive foo@{i j} : ... -> Type@{i} := C : ... -> foo Type@{j} + i is irrelevant, j is invariant. *) + if not is_arity then infer_term CUMUL env variances codom else variances + +open Entries + +let infer_inductive_core env params entries uctx = + let uarray = Instance.to_array @@ UContext.instance uctx in + if Array.is_empty uarray then raise TrivialVariance; + let env = Environ.push_context uctx env in + let variances = + Array.fold_left (fun variances u -> LMap.add u IrrelevantI variances) + LMap.empty uarray + in + let env, _ = Typeops.check_context env params in + let variances = List.fold_left (fun variances entry -> + let variances = infer_arity_constructor true + env variances entry.mind_entry_arity + in + List.fold_left (infer_arity_constructor false env) + variances entry.mind_entry_lc) + variances + entries + in + Array.map (fun u -> match LMap.find u variances with + | exception Not_found -> Invariant + | IrrelevantI -> Irrelevant + | CovariantI -> Covariant) + uarray + +let infer_inductive env mie = + let open Entries in + let params = mie.mind_entry_params in + let entries = mie.mind_entry_inds in + let variances = + match mie.mind_entry_variance with + | None -> None + | Some _ -> + let uctx = match mie.mind_entry_universes with + | Monomorphic_entry _ -> assert false + | Polymorphic_entry (_,uctx) -> uctx + in + try Some (infer_inductive_core env params entries uctx) + with TrivialVariance -> Some (Array.make (UContext.size uctx) Invariant) + in + { mie with mind_entry_variance = variances } + +let dummy_variance = let open Entries in function + | Monomorphic_entry _ -> assert false + | Polymorphic_entry (_,uctx) -> Array.make (UContext.size uctx) Irrelevant diff --git a/kernel/inferCumulativity.mli b/kernel/inferCumulativity.mli new file mode 100644 index 0000000000..a234e334d1 --- /dev/null +++ b/kernel/inferCumulativity.mli @@ -0,0 +1,14 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* Entries.mutual_inductive_entry -> + Entries.mutual_inductive_entry + +val dummy_variance : Entries.universes_entry -> Univ.Variance.t array diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib index 59c1d5890f..66bac15e9a 100644 --- a/kernel/kernel.mllib +++ b/kernel/kernel.mllib @@ -43,6 +43,7 @@ Inductive Typeops IndTyping Indtypes +InferCumulativity Cooking Term_typing Subtyping diff --git a/pretyping/inferCumulativity.ml b/pretyping/inferCumulativity.ml deleted file mode 100644 index ed069eace0..0000000000 --- a/pretyping/inferCumulativity.ml +++ /dev/null @@ -1,234 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* Covariant so nontrivial *) - LMap.update u (function - | None -> None - | Some CovariantI as x -> x - | Some IrrelevantI -> Some CovariantI) - variances - -let infer_generic_instance_eq variances u = - Array.fold_left (fun variances u -> infer_level_eq u variances) - variances (Instance.to_array u) - -let infer_cumulative_ind_instance cv_pb mind_variance variances u = - Array.fold_left2 (fun variances varu u -> - match cv_pb, varu with - | _, Irrelevant -> variances - | _, Invariant | CONV, Covariant -> infer_level_eq u variances - | CUMUL, Covariant -> infer_level_leq u variances) - variances mind_variance (Instance.to_array u) - -let infer_inductive_instance cv_pb env variances ind nargs u = - let mind = Environ.lookup_mind (fst ind) env in - match mind.mind_variance with - | None -> infer_generic_instance_eq variances u - | Some mind_variance -> - if not (Int.equal (inductive_cumulativity_arguments (mind,snd ind)) nargs) - then infer_generic_instance_eq variances u - else infer_cumulative_ind_instance cv_pb mind_variance variances u - -let infer_constructor_instance_eq env variances ((mi,ind),ctor) nargs u = - let mind = Environ.lookup_mind mi env in - match mind.mind_variance with - | None -> infer_generic_instance_eq variances u - | Some _ -> - if not (Int.equal (constructor_cumulativity_arguments (mind,ind,ctor)) nargs) - then infer_generic_instance_eq variances u - else variances (* constructors are convertible at common supertype *) - -let infer_sort cv_pb variances s = - match cv_pb with - | CONV -> - LSet.fold infer_level_eq (Universe.levels (Sorts.univ_of_sort s)) variances - | CUMUL -> - LSet.fold infer_level_leq (Universe.levels (Sorts.univ_of_sort s)) variances - -let infer_table_key infos variances c = - let open Names in - match c with - | ConstKey (_, u) -> - infer_generic_instance_eq variances u - | VarKey _ | RelKey _ -> variances - -let whd_stack (infos, tab) hd stk = CClosure.whd_stack infos tab hd stk - -let rec infer_fterm cv_pb infos variances hd stk = - Control.check_for_interrupt (); - let hd,stk = whd_stack infos hd stk in - let open CClosure in - match fterm_of hd with - | FAtom a -> - begin match kind a with - | Sort s -> infer_sort cv_pb variances s - | Meta _ -> infer_stack infos variances stk - | _ -> assert false - end - | FEvar ((_,args),e) -> - let variances = infer_stack infos variances stk in - infer_vect infos variances (Array.map (mk_clos e) args) - | FRel _ -> infer_stack infos variances stk - | FInt _ -> infer_stack infos variances stk - | FFlex fl -> - let variances = infer_table_key infos variances fl in - infer_stack infos variances stk - | FProj (_,c) -> - let variances = infer_fterm CONV infos variances c [] in - infer_stack infos variances stk - | FLambda _ -> - let (_,ty,bd) = destFLambda mk_clos hd in - let variances = infer_fterm CONV infos variances ty [] in - infer_fterm CONV infos variances bd [] - | FProd (_,dom,codom,e) -> - let variances = infer_fterm CONV infos variances dom [] in - infer_fterm cv_pb infos variances (mk_clos (Esubst.subs_lift e) codom) [] - | FInd (ind, u) -> - let variances = - if Instance.is_empty u then variances - else - let nargs = stack_args_size stk in - infer_inductive_instance cv_pb (info_env (fst infos)) variances ind nargs u - in - infer_stack infos variances stk - | FConstruct (ctor,u) -> - let variances = - if Instance.is_empty u then variances - else - let nargs = stack_args_size stk in - infer_constructor_instance_eq (info_env (fst infos)) variances ctor nargs u - in - infer_stack infos variances stk - | FFix ((_,(_,tys,cl)),e) | FCoFix ((_,(_,tys,cl)),e) -> - let n = Array.length cl in - let variances = infer_vect infos variances (Array.map (mk_clos e) tys) in - let le = Esubst.subs_liftn n e in - let variances = infer_vect infos variances (Array.map (mk_clos le) cl) in - infer_stack infos variances stk - - (* Removed by whnf *) - | FLOCKED | FCaseT _ | FLetIn _ | FApp _ | FLIFT _ | FCLOS _ -> assert false - -and infer_stack infos variances (stk:CClosure.stack) = - match stk with - | [] -> variances - | z :: stk -> - let open CClosure in - let variances = match z with - | Zapp v -> infer_vect infos variances v - | Zproj _ -> variances - | Zfix (fx,a) -> - let variances = infer_fterm CONV infos variances fx [] in - infer_stack infos variances a - | ZcaseT (ci,p,br,e) -> - let variances = infer_fterm CONV infos variances (mk_clos e p) [] in - infer_vect infos variances (Array.map (mk_clos e) br) - | Zshift _ -> variances - | Zupdate _ -> variances - | Zprimitive (_,_,rargs,kargs) -> - let variances = List.fold_left (fun variances c -> infer_fterm CONV infos variances c []) variances rargs in - let variances = List.fold_left (fun variances (_,c) -> infer_fterm CONV infos variances c []) variances kargs in - variances - in - infer_stack infos variances stk - -and infer_vect infos variances v = - Array.fold_left (fun variances c -> infer_fterm CONV infos variances c []) variances v - -let infer_term cv_pb env variances c = - let open CClosure in - let infos = (create_clos_infos all env, create_tab ()) in - infer_fterm cv_pb infos variances (CClosure.inject c) [] - -let infer_arity_constructor is_arity env variances arcn = - let infer_typ typ (env,variances) = - match typ with - | Context.Rel.Declaration.LocalAssum (_, typ') -> - (Environ.push_rel typ env, infer_term CUMUL env variances typ') - | Context.Rel.Declaration.LocalDef _ -> assert false - in - let typs, codom = Reduction.dest_prod env arcn in - let env, variances = Context.Rel.fold_outside infer_typ typs ~init:(env, variances) in - (* If we have Inductive foo@{i j} : ... -> Type@{i} := C : ... -> foo Type@{j} - i is irrelevant, j is invariant. *) - if not is_arity then infer_term CUMUL env variances codom else variances - -open Entries - -let infer_inductive_core env params entries uctx = - let uarray = Instance.to_array @@ UContext.instance uctx in - if Array.is_empty uarray then raise TrivialVariance; - let env = Environ.push_context uctx env in - let variances = - Array.fold_left (fun variances u -> LMap.add u IrrelevantI variances) - LMap.empty uarray - in - let env, params = Typeops.check_context env params in - let variances = List.fold_left (fun variances entry -> - let variances = infer_arity_constructor true - env variances entry.mind_entry_arity - in - List.fold_left (infer_arity_constructor false env) - variances entry.mind_entry_lc) - variances - entries - in - Array.map (fun u -> match LMap.find u variances with - | exception Not_found -> Invariant - | IrrelevantI -> Irrelevant - | CovariantI -> Covariant) - uarray - -let infer_inductive env mie = - let open Entries in - let { mind_entry_params = params; - mind_entry_inds = entries; } = mie - in - let variances = - match mie.mind_entry_variance with - | None -> None - | Some _ -> - let uctx = match mie.mind_entry_universes with - | Monomorphic_entry _ -> assert false - | Polymorphic_entry (_,uctx) -> uctx - in - try Some (infer_inductive_core env params entries uctx) - with TrivialVariance -> Some (Array.make (UContext.size uctx) Invariant) - in - { mie with mind_entry_variance = variances } - -let dummy_variance = let open Entries in function - | Monomorphic_entry _ -> assert false - | Polymorphic_entry (_,uctx) -> Array.make (UContext.size uctx) Irrelevant diff --git a/pretyping/inferCumulativity.mli b/pretyping/inferCumulativity.mli deleted file mode 100644 index a234e334d1..0000000000 --- a/pretyping/inferCumulativity.mli +++ /dev/null @@ -1,14 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* Entries.mutual_inductive_entry -> - Entries.mutual_inductive_entry - -val dummy_variance : Entries.universes_entry -> Univ.Variance.t array diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib index 0ca39f0404..7e140f4399 100644 --- a/pretyping/pretyping.mllib +++ b/pretyping/pretyping.mllib @@ -4,7 +4,6 @@ Locusops Pretype_errors Reductionops Inductiveops -InferCumulativity Arguments_renaming Retyping Vnorm -- cgit v1.2.3