From e6bffa602c0d744a24d7ea7418020ebd8b7dfbbf Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Sat, 7 Oct 2017 11:35:34 +0200 Subject: Fix typo in Univ.CumulativityInfo --- pretyping/inductiveops.ml | 58 +++++++++++++++++++++++------------------------ 1 file changed, 29 insertions(+), 29 deletions(-) (limited to 'pretyping/inductiveops.ml') diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 78e6bc6f14..f73f841189 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -84,7 +84,7 @@ let mis_is_recursive_subset listind rarg = List.exists (fun ra -> match dest_recarg ra with - | Mrec (_,i) -> Int.List.mem i listind + | Mrec (_,i) -> Int.List.mem i listind | _ -> false) rvec in Array.exists one_is_rec (dest_subterms rarg) @@ -361,20 +361,20 @@ let make_case_or_project env sigma indf ci pred c branches = if (* dependent *) not (Vars.noccurn sigma 1 t) && not (has_dependent_elim mib) then user_err ~hdr:"make_case_or_project" - Pp.(str"Dependent case analysis not allowed" ++ - str" on inductive type " ++ Names.MutInd.print (fst ind)) + Pp.(str"Dependent case analysis not allowed" ++ + str" on inductive type " ++ Names.MutInd.print (fst ind)) in let branch = branches.(0) in let ctx, br = decompose_lam_n_assum sigma (Array.length ps) branch in let n, subst = List.fold_right (fun decl (i, subst) -> - match decl with - | LocalAssum (na, t) -> - let t = mkProj (Projection.make ps.(i) true, c) in - (i + 1, t :: subst) - | LocalDef (na, b, t) -> (i, Vars.substl subst b :: subst)) - ctx (0, []) + match decl with + | LocalAssum (na, t) -> + let t = mkProj (Projection.make ps.(i) true, c) in + (i + 1, t :: subst) + | LocalDef (na, b, t) -> (i, Vars.substl subst b :: subst)) + ctx (0, []) in Vars.substl subst br (* substitution in a signature *) @@ -511,25 +511,25 @@ let is_predicate_explicitly_dep env sigma pred arsign = let pv' = whd_all env sigma pval in match EConstr.kind sigma pv', arsign with | Lambda (na,t,b), (LocalAssum _)::arsign -> - srec (push_rel_assum (na, t) env) b arsign + srec (push_rel_assum (na, t) env) b arsign | Lambda (na,_,t), _ -> (* The following code has an impact on the introduction names - given by the tactics "case" and "inversion": when the - elimination is not dependent, "case" uses Anonymous for - inductive types in Prop and names created by mkProd_name for - inductive types in Set/Type while "inversion" uses anonymous - for inductive types both in Prop and Set/Type !! - - Previously, whether names were created or not relied on - whether the predicate created in Indrec.make_case_com had a - dependent arity or not. To avoid different predicates - printed the same in v8, all predicates built in indrec.ml - got a dependent arity (Aug 2004). The new way to decide - whether names have to be created or not is to use an - Anonymous or Named variable to enforce the expected - dependency status (of course, Anonymous implies non - dependent, but not conversely). + given by the tactics "case" and "inversion": when the + elimination is not dependent, "case" uses Anonymous for + inductive types in Prop and names created by mkProd_name for + inductive types in Set/Type while "inversion" uses anonymous + for inductive types both in Prop and Set/Type !! + + Previously, whether names were created or not relied on + whether the predicate created in Indrec.make_case_com had a + dependent arity or not. To avoid different predicates + printed the same in v8, all predicates built in indrec.ml + got a dependent arity (Aug 2004). The new way to decide + whether names have to be created or not is to use an + Anonymous or Named variable to enforce the expected + dependency status (of course, Anonymous implies non + dependent, but not conversely). From Coq > 8.2, using or not the the effective dependency of the predicate is parametrable! *) @@ -600,15 +600,15 @@ let rec instantiate_universes env evdref scl is = function let ctx,_ = Reduction.dest_arity env ty in let u = Univ.Universe.make l in let s = - (* Does the sort of parameter [u] appear in (or equal) + (* Does the sort of parameter [u] appear in (or equal) the sort of inductive [is] ? *) if univ_level_mem l is then scl (* constrained sort: replace by scl *) else (* unconstrained sort: replace by fresh universe *) let evm, s = Evd.new_sort_variable Evd.univ_flexible !evdref in - let evm = Evd.set_leq_sort env evm s (Sorts.sort_of_univ u) in - evdref := evm; s + let evm = Evd.set_leq_sort env evm s (Sorts.sort_of_univ u) in + evdref := evm; s in (LocalAssum (na,mkArity(ctx,s))) :: instantiate_universes env evdref scl is (sign, exp) | sign, [] -> sign (* Uniform parameters are exhausted *) @@ -707,7 +707,7 @@ let infer_inductive_subtyping env evd mind_ent = | Entries.Cumulative_ind_entry cumi -> begin let uctx = Univ.CumulativityInfo.univ_context cumi in - let sbsubst = Univ.CumulativityInfo.subtyping_susbst cumi in + let sbsubst = Univ.CumulativityInfo.subtyping_subst cumi in let dosubst = subst_univs_level_constr sbsubst in let instance_other = Univ.subst_univs_level_instance sbsubst (Univ.UContext.instance uctx) -- cgit v1.2.3 From 35fba70509d9fb219b2a88f8e7bd246b2671b39b Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 9 Nov 2017 17:27:58 +0100 Subject: Simplification: cumulativity information is variance information. Since cumulativity of an inductive type is the universe constraints which make a term convertible with its universe-renamed copy, the only constraints we can get are between a universe and its copy. As such we do not need to be able to represent arbitrary constraints between universes and copied universes in a double-sized ucontext, instead we can just keep around an array describing whether a bound universe is covariant, invariant or irrelevant (CIC has no contravariant conversion rule). Printing is fairly obtuse and should be improved: when we print the CumulativityInfo we add marks to the universes of the instance: = for invariant, + for covariant and * for irrelevant. ie Record Foo@{i j k} := { foo : Type@{i} -> Type@{j} }. Print Foo. gives Cumulative Record Foo : Type@{max(i+1, j+1)} := Build_Foo { foo : Type@{i} -> Type@{j} } (* =i +j *k |= *) --- pretyping/inductiveops.ml | 62 +++++++++++++++++++++++++++++++++++++---------- 1 file changed, 49 insertions(+), 13 deletions(-) (limited to 'pretyping/inductiveops.ml') diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index f73f841189..df0b53e9c2 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -694,6 +694,43 @@ let infer_inductive_subtyping_arity_constructor let last_contexts = Context.Rel.fold_outside infer_typ typs ~init:(env, evd, 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 evd mind_ent = let { Entries.mind_entry_params = params; Entries.mind_entry_inds = entries; @@ -706,22 +743,23 @@ let infer_inductive_subtyping env evd mind_ent = | Entries.Polymorphic_ind_entry _ -> ground_univs | Entries.Cumulative_ind_entry cumi -> begin - let uctx = Univ.CumulativityInfo.univ_context cumi in - let sbsubst = Univ.CumulativityInfo.subtyping_subst cumi in - let dosubst = subst_univs_level_constr sbsubst in - let instance_other = - Univ.subst_univs_level_instance sbsubst (Univ.UContext.instance uctx) + let uctx = CumulativityInfo.univ_context cumi 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 - sbsubst (Univ.UContext.constraints uctx) + 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 evd = - Evd.merge_universe_context - evd (UState.of_context_set (Univ.ContextSet.of_context uctx_other)) + Evd.merge_context_set UState.UnivRigid + evd (Univ.ContextSet.of_context uctx_other) in let (_, _, subtyp_constraints) = List.fold_left @@ -737,12 +775,10 @@ let infer_inductive_subtyping env evd mind_ent = ) ctxs' indentry.Entries.mind_entry_lc ) (env, evd, Univ.Constraint.empty) entries - in + in + let variance = make_variance uctx lmap subtyp_constraints in Entries.Cumulative_ind_entry (Univ.CumulativityInfo.make - (Univ.CumulativityInfo.univ_context cumi, - Univ.UContext.make - (Univ.UContext.instance (Univ.CumulativityInfo.subtyp_context cumi), - subtyp_constraints))) + (uctx, variance)) end in {mind_ent with Entries.mind_entry_universes = uinfind;} -- cgit v1.2.3 From 1ed0836a7e0c8e05b0288f85e344ef5249d5d228 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Fri, 10 Nov 2017 13:23:32 +0100 Subject: Inference of inductive subtyping does not need an evar map. --- pretyping/inductiveops.ml | 29 +++++++++++++---------------- 1 file changed, 13 insertions(+), 16 deletions(-) (limited to 'pretyping/inductiveops.ml') diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index df0b53e9c2..23a4ade3f4 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -660,20 +660,20 @@ let control_only_guard env c = (* inference of subtyping condition for inductive types *) let infer_inductive_subtyping_arity_constructor - (env, evd, csts) (subst : constr -> constr) (arcn : types) is_arity (params : Context.Rel.t) = + (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, evd, csts) csts' = - (Environ.add_constraints csts' env, Evd.add_constraints evd csts', Univ.Constraint.union csts csts') + let update_contexts (env, csts) csts' = + (Environ.add_constraints csts' env, Univ.Constraint.union csts csts') in - let basic_check (env, evd, csts) tp = + let basic_check (env, csts) tp = let result = if !numchecked >= numparams then let csts' = - Reduction.infer_conv_leq ~evars:(Evd.existential_opt_value evd) env (Evd.universes evd) tp (subst tp) - in update_contexts (env, evd, csts) csts' + Reduction.infer_conv_leq env (Environ.universes env) tp (subst tp) + in update_contexts (env, csts) csts' else - (env, evd, csts) + (env, csts) in numchecked := !numchecked + 1; result in @@ -682,7 +682,7 @@ let infer_inductive_subtyping_arity_constructor | LocalAssum (_, typ') -> begin try - let (env, evd, csts) = basic_check ctxs typ' in (Environ.push_rel typ env, evd, csts) + 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") @@ -691,7 +691,7 @@ let infer_inductive_subtyping_arity_constructor 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, evd, csts) 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 = @@ -731,7 +731,7 @@ let make_variance uctx lmap csts = ) csts; variance -let infer_inductive_subtyping env evd mind_ent = +let infer_inductive_subtyping env mind_ent = let { Entries.mind_entry_params = params; Entries.mind_entry_inds = entries; Entries.mind_entry_universes = ground_univs; @@ -744,6 +744,7 @@ let infer_inductive_subtyping env evd mind_ent = | 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 @@ -757,11 +758,7 @@ let infer_inductive_subtyping env evd mind_ent = 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 evd = - Evd.merge_context_set UState.UnivRigid - evd (Univ.ContextSet.of_context uctx_other) - in - let (_, _, subtyp_constraints) = + let (_, subtyp_constraints) = List.fold_left (fun ctxs indentry -> let _, params = Typeops.infer_local_decls env params in @@ -774,7 +771,7 @@ let infer_inductive_subtyping env evd mind_ent = ctxs dosubst cons false params ) ctxs' indentry.Entries.mind_entry_lc - ) (env, evd, Univ.Constraint.empty) entries + ) (env, Univ.Constraint.empty) entries in let variance = make_variance uctx lmap subtyp_constraints in Entries.Cumulative_ind_entry -- cgit v1.2.3 From 6c2d10b93b819f0735a43453c78566795de8ba5a Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Fri, 10 Nov 2017 15:05:21 +0100 Subject: Use specialized function for inductive subtyping inference. This ensures by construction that we never infer constraints outside the variance model. --- pretyping/inductiveops.ml | 123 ---------------------------------------------- 1 file changed, 123 deletions(-) (limited to 'pretyping/inductiveops.ml') diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 23a4ade3f4..275a079d5d 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;} -- cgit v1.2.3