diff options
author | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-11-10 15:05:21 +0100 |
---|---|---|
committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-02-11 22:28:39 +0100 |
commit | 6c2d10b93b819f0735a43453c78566795de8ba5a (patch) | |
tree | 14dffe59d0edfacf547b3912352f14420df047b8 /pretyping | |
parent | 1ed0836a7e0c8e05b0288f85e344ef5249d5d228 (diff) |
Use specialized function for inductive subtyping inference.
This ensures by construction that we never infer constraints outside
the variance model.
Diffstat (limited to 'pretyping')
-rw-r--r-- | pretyping/inductiveops.ml | 123 | ||||
-rw-r--r-- | pretyping/inductiveops.mli | 4 | ||||
-rw-r--r-- | pretyping/inferCumulativity.ml | 222 | ||||
-rw-r--r-- | pretyping/inferCumulativity.mli | 10 | ||||
-rw-r--r-- | pretyping/pretyping.mllib | 1 |
5 files changed, 233 insertions, 127 deletions
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 23a4ade3f..275a079d5 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -656,126 +656,3 @@ let control_only_guard env c = iter_constr_with_full_binders push_rel iter env c in iter env c - -(* inference of subtyping condition for inductive types *) - -let infer_inductive_subtyping_arity_constructor - (env, csts) (subst : constr -> constr) (arcn : types) is_arity (params : Context.Rel.t) = - let numchecked = ref 0 in - let numparams = Context.Rel.nhyps params in - let update_contexts (env, csts) csts' = - (Environ.add_constraints csts' env, Univ.Constraint.union csts csts') - in - let basic_check (env, csts) tp = - let result = - if !numchecked >= numparams then - let csts' = - Reduction.infer_conv_leq env (Environ.universes env) tp (subst tp) - in update_contexts (env, csts) csts' - else - (env, csts) - in - numchecked := !numchecked + 1; result - in - let infer_typ typ ctxs = - match typ with - | LocalAssum (_, typ') -> - begin - try - let (env, csts) = basic_check ctxs typ' in (Environ.push_rel typ env, csts) - with Reduction.NotConvertible -> - anomaly ~label:"inference of record/inductive subtyping relation failed" - (Pp.str "Can't infer subtyping for record/inductive type") - end - | _ -> anomaly (Pp.str "") - in - let arcn' = Term.it_mkProd_or_LetIn arcn params in - let typs, codom = Reduction.dest_prod env arcn' in - let last_contexts = Context.Rel.fold_outside infer_typ typs ~init:(env, csts) in - if not is_arity then basic_check last_contexts codom else last_contexts - -type ukind = - Global | Orig of int | New of int - -let make_variance uctx lmap csts = - let variance = Array.init (UContext.size uctx) (fun _ -> Variance.Irrelevant) in - let geti = Array.fold_left_i (fun i geti u -> LMap.add u i geti) - LMap.empty (Instance.to_array @@ UContext.instance uctx) - in - let lmap_rev = LMap.fold (fun u v lmap_rev -> LMap.add v u lmap_rev) lmap LMap.empty in - let analyse_univ u = - match LMap.find u lmap_rev with - | exception Not_found -> - begin match LMap.find u lmap with - | exception Not_found -> Global - | _ -> Orig (LMap.find u geti) - end - | uorig -> New (LMap.find uorig geti) - in - Constraint.iter (fun (l,d,r) -> - match analyse_univ l, analyse_univ r with - | Orig i, New j when Int.equal i j -> - begin match d with - | Lt -> anomaly ~label:"make_variance" Pp.(str "unexpected orig < new constraint") - | Eq -> variance.(i) <- Variance.sup variance.(i) Variance.Invariant - | Le -> variance.(i) <- Variance.sup variance.(i) Variance.Covariant - end - | New i, Orig j when Int.equal i j -> - begin match d with - | Lt -> anomaly ~label:"make_variance" Pp.(str "unexpected orig > new constraint") - | Eq -> variance.(i) <- Variance.sup variance.(i) Variance.Invariant - | Le -> anomaly ~label:"make_variance" Pp.(str "unexpected orig >= new constraint") - end - | (Global | Orig _ | New _), _ -> - anomaly ~label:"make_variance" Pp.(str "unexpected constraint between non copy universes") - ) csts; - variance - -let infer_inductive_subtyping env mind_ent = - let { Entries.mind_entry_params = params; - Entries.mind_entry_inds = entries; - Entries.mind_entry_universes = ground_univs; - } = mind_ent - in - let uinfind = - match ground_univs with - | Entries.Monomorphic_ind_entry _ - | Entries.Polymorphic_ind_entry _ -> ground_univs - | Entries.Cumulative_ind_entry cumi -> - begin - let uctx = CumulativityInfo.univ_context cumi in - let env = Environ.push_context uctx env in - let new_levels = Array.init (UContext.size uctx) (Level.make DirPath.empty) in - let lmap = Array.fold_left2 (fun lmap u u' -> LMap.add u u' lmap) - LMap.empty (Instance.to_array @@ UContext.instance uctx) new_levels - in - let dosubst = subst_univs_level_constr lmap in - let instance_other = Instance.of_array new_levels in - let constraints_other = - Univ.subst_univs_level_constraints - lmap (Univ.UContext.constraints uctx) - in - let uctx_other = Univ.UContext.make (instance_other, constraints_other) in - let env = Environ.push_context uctx env in - let env = Environ.push_context uctx_other env in - let (_, subtyp_constraints) = - List.fold_left - (fun ctxs indentry -> - let _, params = Typeops.infer_local_decls env params in - let ctxs' = infer_inductive_subtyping_arity_constructor - ctxs dosubst indentry.Entries.mind_entry_arity true params - in - List.fold_left - (fun ctxs cons -> - infer_inductive_subtyping_arity_constructor - ctxs dosubst cons false params - ) - ctxs' indentry.Entries.mind_entry_lc - ) (env, Univ.Constraint.empty) entries - in - let variance = make_variance uctx lmap subtyp_constraints in - Entries.Cumulative_ind_entry - (Univ.CumulativityInfo.make - (uctx, variance)) - end - in {mind_ent with Entries.mind_entry_universes = uinfind;} diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index f6b11ee66..55149552a 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -199,7 +199,3 @@ val type_of_inductive_knowing_conclusion : (********************) val control_only_guard : env -> types -> unit - -(* inference of subtyping condition for inductive types *) -val infer_inductive_subtyping : Environ.env -> Entries.mutual_inductive_entry -> - Entries.mutual_inductive_entry diff --git a/pretyping/inferCumulativity.ml b/pretyping/inferCumulativity.ml new file mode 100644 index 000000000..43d2aa75e --- /dev/null +++ b/pretyping/inferCumulativity.ml @@ -0,0 +1,222 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Reduction +open Declarations +open Constr +open Univ +open Util + +(** Throughout this module we modify a map [variances] from local + universes to [Variance.t]. It starts as a trivial mapping to + [Irrelevant] and every time we encounter a local universe we + restrict it accordingly. *) + +let infer_level_eq u variances = + if LMap.mem u variances + then LMap.set u Variance.Invariant variances + else variances + +let infer_level_leq u variances = + match LMap.find u variances with + | exception Not_found -> variances + | varu -> LMap.set u (Variance.sup varu Variance.Covariant) 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 variance_pb cv_pb var = + let open Variance in + match cv_pb, var with + | _, Irrelevant -> Irrelevant + | _, Invariant -> Invariant + | CONV, Covariant -> Invariant + | CUMUL, Covariant -> Covariant + +let infer_cumulative_ind_instance cv_pb cumi variances u = + Array.fold_left2 (fun variances varu u -> + match LMap.find u variances with + | exception Not_found -> variances + | varu' -> + LMap.set u (Variance.sup varu' (variance_pb cv_pb varu)) variances) + variances (ACumulativityInfo.variance cumi) (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_universes with + | Monomorphic_ind _ -> assert (Instance.is_empty u); variances + | Polymorphic_ind _ -> infer_generic_instance_eq variances u + | Cumulative_ind cumi -> + 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 cumi 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_universes with + | Monomorphic_ind _ -> assert (Instance.is_empty u); variances + | Polymorphic_ind _ -> infer_generic_instance_eq variances u + | Cumulative_ind cumi -> + if not (Int.equal (constructor_cumulativity_arguments (mind,ind,ctor)) nargs) + then infer_generic_instance_eq variances u + else infer_cumulative_ind_instance CONV cumi variances u + +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 rec infer_fterm cv_pb infos variances hd stk = + Control.check_for_interrupt (); + let open CClosure in + let hd,stk = whd_stack infos hd stk 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 _ -> variances + | 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) -> + let variances = infer_fterm CONV infos variances dom [] in + infer_fterm cv_pb infos variances 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 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 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 _ | FCast _ | 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 + 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 reds = RedFlags.red_add_transparent betaiotazeta Names.full_transparent_state in + let infos = create_clos_infos reds env in + infer_fterm cv_pb infos variances (CClosure.inject c) [] + +let infer_arity_constructor env variances arcn is_arity params = + let numchecked = ref 0 in + let numparams = Context.Rel.nhyps params in + let basic_check env variances tp = + let variances = + if !numchecked >= numparams then + infer_term CUMUL env variances tp + else + variances + in + numchecked := !numchecked + 1; variances + in + let infer_typ typ (env,variances) = + match typ with + | Context.Rel.Declaration.LocalAssum (_, typ') -> + (Environ.push_rel typ env, basic_check env variances typ') + | Context.Rel.Declaration.LocalDef _ -> assert false + in + let arcn' = Term.it_mkProd_or_LetIn arcn params 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 not is_arity then basic_check env variances codom else variances + +let infer_inductive env mie = + let open Entries in + let { mind_entry_params = params; + mind_entry_inds = entries; } = mie + in + let univs = + match mie.mind_entry_universes with + | Monomorphic_ind_entry _ + | Polymorphic_ind_entry _ as univs -> univs + | Cumulative_ind_entry cumi -> + let uctx = CumulativityInfo.univ_context cumi in + let uarray = Instance.to_array @@ UContext.instance uctx in + let env = Environ.push_context uctx env in + let variances = + Array.fold_left (fun variances u -> LMap.add u Variance.Irrelevant variances) + LMap.empty uarray + in + let variances = List.fold_left (fun variances entry -> + let _, params = Typeops.infer_local_decls env params in + let variances = infer_arity_constructor + env variances entry.mind_entry_arity true params + in + List.fold_left + (fun variances cons -> + infer_arity_constructor + env variances cons false params) + variances entry.mind_entry_lc) + variances + entries + in + let variances = Array.map (fun u -> LMap.find u variances) uarray in + Cumulative_ind_entry (CumulativityInfo.make (uctx, variances)) + in + { mie with mind_entry_universes = univs } diff --git a/pretyping/inferCumulativity.mli b/pretyping/inferCumulativity.mli new file mode 100644 index 000000000..a5037ea47 --- /dev/null +++ b/pretyping/inferCumulativity.mli @@ -0,0 +1,10 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +val infer_inductive : Environ.env -> Entries.mutual_inductive_entry -> + Entries.mutual_inductive_entry diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib index 1da5b4567..ae4ad0be7 100644 --- a/pretyping/pretyping.mllib +++ b/pretyping/pretyping.mllib @@ -4,6 +4,7 @@ Locusops Pretype_errors Reductionops Inductiveops +InferCumulativity Vnorm Arguments_renaming Nativenorm |