From 62adf2b9e03afa212fcd8819226da068bf4a32b8 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Tue, 29 Oct 2019 13:20:04 +0100 Subject: Pretyping.check_evars: make initial evar map optional There are no users in Coq but maybe some plugin wants it so don't completely remove it --- vernac/comInductive.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'vernac/comInductive.ml') diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 2aee9bd47f..2afb5e9d65 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -369,10 +369,10 @@ let interp_mutual_inductive_constr ~env0 ~sigma ~template ~udecl ~env_ar ~env_pa let arityconcl = List.map (Option.map (fun (_anon, s) -> EConstr.ESorts.kind sigma s)) arityconcl in let sigma = restrict_inductive_universes sigma ctx_params (List.map snd arities) constructors in let uctx = Evd.check_univ_decl ~poly sigma udecl in - List.iter (fun c -> check_evars env_params (Evd.from_env env_params) sigma (EConstr.of_constr (snd c))) arities; - Context.Rel.iter (fun c -> check_evars env0 (Evd.from_env env0) sigma (EConstr.of_constr c)) ctx_params; + List.iter (fun c -> check_evars env_params sigma (EConstr.of_constr (snd c))) arities; + Context.Rel.iter (fun c -> check_evars env0 sigma (EConstr.of_constr c)) ctx_params; List.iter (fun (_,ctyps,_) -> - List.iter (fun c -> check_evars env_ar_params (Evd.from_env env_ar_params) sigma (EConstr.of_constr c)) ctyps) + List.iter (fun c -> check_evars env_ar_params sigma (EConstr.of_constr c)) ctyps) constructors; (* Build the inductive entries *) -- cgit v1.2.3 From 097796f1ebfa4009502e23494af08f332613ace3 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Tue, 29 Oct 2019 13:27:25 +0100 Subject: comInductive: remove redundant check_evars calls We do [solve_remaining_evars all_and_fail_flags] immediately before calling [interp_mutual_inductive_constr] so these checks are extra. --- vernac/comInductive.ml | 9 ++------- 1 file changed, 2 insertions(+), 7 deletions(-) (limited to 'vernac/comInductive.ml') diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 2afb5e9d65..812bf7b021 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -353,7 +353,7 @@ let restrict_inductive_universes sigma ctx_params arities constructors = let uvars = List.fold_right (fun (_,ctypes,_) -> List.fold_right merge_universes_of_constr ctypes) constructors uvars in Evd.restrict_universe_context sigma uvars -let interp_mutual_inductive_constr ~env0 ~sigma ~template ~udecl ~env_ar ~env_params ~ctx_params ~indnames ~arities ~arityconcl ~constructors ~env_ar_params ~cumulative ~poly ~private_ind ~finite = +let interp_mutual_inductive_constr ~env0 ~sigma ~template ~udecl ~env_ar ~ctx_params ~indnames ~arities ~arityconcl ~constructors ~env_ar_params ~cumulative ~poly ~private_ind ~finite = (* Compute renewed arities *) let sigma = Evd.minimize_universes sigma in let nf = Evarutil.nf_evars_universes sigma in @@ -369,11 +369,6 @@ let interp_mutual_inductive_constr ~env0 ~sigma ~template ~udecl ~env_ar ~env_pa let arityconcl = List.map (Option.map (fun (_anon, s) -> EConstr.ESorts.kind sigma s)) arityconcl in let sigma = restrict_inductive_universes sigma ctx_params (List.map snd arities) constructors in let uctx = Evd.check_univ_decl ~poly sigma udecl in - List.iter (fun c -> check_evars env_params sigma (EConstr.of_constr (snd c))) arities; - Context.Rel.iter (fun c -> check_evars env0 sigma (EConstr.of_constr c)) ctx_params; - List.iter (fun (_,ctyps,_) -> - List.iter (fun c -> check_evars env_ar_params sigma (EConstr.of_constr c)) ctyps) - constructors; (* Build the inductive entries *) let entries = List.map4 (fun indname (templatearity, arity) concl (cnames,ctypes,cimpls) -> @@ -509,7 +504,7 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not indimpls, List.map (fun impls -> userimpls @ impls) cimpls) indimpls constructors in - let mie, pl = interp_mutual_inductive_constr ~env0 ~template ~sigma ~env_params ~env_ar ~ctx_params ~udecl ~arities ~arityconcl ~constructors ~env_ar_params ~poly ~finite ~cumulative ~private_ind ~indnames in + let mie, pl = interp_mutual_inductive_constr ~env0 ~template ~sigma ~env_ar ~ctx_params ~udecl ~arities ~arityconcl ~constructors ~env_ar_params ~poly ~finite ~cumulative ~private_ind ~indnames in (mie, pl, impls) -- cgit v1.2.3 From b621bc02657bd1effcca371b56260b0a7a327ed9 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Tue, 29 Oct 2019 13:36:06 +0100 Subject: reduce arguments of template_polymorphism_candidate take only the template_check flag instead of the whole env --- vernac/comInductive.ml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'vernac/comInductive.ml') diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 812bf7b021..56ff757e1a 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -323,18 +323,18 @@ let check_named {CAst.loc;v=na} = match na with let msg = str "Parameters must be named." in user_err ?loc msg -let template_polymorphism_candidate env ~ctor_levels uctx params concl = +let template_polymorphism_candidate ~template_check ~ctor_levels uctx params concl = match uctx with | Entries.Monomorphic_entry uctx -> let concltemplate = Option.cata (fun s -> not (Sorts.is_small s)) false concl in if not concltemplate then false + else if not template_check then true else - let template_check = Environ.check_template env in let conclu = Option.cata Sorts.univ_of_sort Univ.type0m_univ concl in let params, conclunivs = IndTyping.template_polymorphic_univs ~template_check ~ctor_levels uctx params conclu in - not (template_check && Univ.LSet.is_empty conclunivs) + not (Univ.LSet.is_empty conclunivs) | Entries.Polymorphic_entry _ -> false let check_param = function @@ -353,7 +353,7 @@ let restrict_inductive_universes sigma ctx_params arities constructors = let uvars = List.fold_right (fun (_,ctypes,_) -> List.fold_right merge_universes_of_constr ctypes) constructors uvars in Evd.restrict_universe_context sigma uvars -let interp_mutual_inductive_constr ~env0 ~sigma ~template ~udecl ~env_ar ~ctx_params ~indnames ~arities ~arityconcl ~constructors ~env_ar_params ~cumulative ~poly ~private_ind ~finite = +let interp_mutual_inductive_constr ~sigma ~template ~udecl ~env_ar ~ctx_params ~indnames ~arities ~arityconcl ~constructors ~env_ar_params ~cumulative ~poly ~private_ind ~finite = (* Compute renewed arities *) let sigma = Evd.minimize_universes sigma in let nf = Evarutil.nf_evars_universes sigma in @@ -385,7 +385,7 @@ let interp_mutual_inductive_constr ~env0 ~sigma ~template ~udecl ~env_ar ~ctx_pa List.fold_left (fun levels c -> add_levels c levels) param_levels ctypes in - template_polymorphism_candidate env0 ~ctor_levels uctx ctx_params concl + template_polymorphism_candidate ~template_check:(Environ.check_template env_ar_params) ~ctor_levels uctx ctx_params concl in let template = match template with | Some template -> @@ -504,7 +504,7 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not indimpls, List.map (fun impls -> userimpls @ impls) cimpls) indimpls constructors in - let mie, pl = interp_mutual_inductive_constr ~env0 ~template ~sigma ~env_ar ~ctx_params ~udecl ~arities ~arityconcl ~constructors ~env_ar_params ~poly ~finite ~cumulative ~private_ind ~indnames in + let mie, pl = interp_mutual_inductive_constr ~template ~sigma ~env_ar ~ctx_params ~udecl ~arities ~arityconcl ~constructors ~env_ar_params ~poly ~finite ~cumulative ~private_ind ~indnames in (mie, pl, impls) -- cgit v1.2.3 From 4f1d657f42957d0c2d115424564eedf599584cbc Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Tue, 29 Oct 2019 13:50:47 +0100 Subject: Remove variance info from inductive entries, infer in indtyping It gets thrown away if the inductive is declared in a section anyway, and there is no user syntax to specify it. --- vernac/comInductive.ml | 11 ++++------- 1 file changed, 4 insertions(+), 7 deletions(-) (limited to 'vernac/comInductive.ml') diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 56ff757e1a..5cf2b680ca 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -353,7 +353,7 @@ let restrict_inductive_universes sigma ctx_params arities constructors = let uvars = List.fold_right (fun (_,ctypes,_) -> List.fold_right merge_universes_of_constr ctypes) constructors uvars in Evd.restrict_universe_context sigma uvars -let interp_mutual_inductive_constr ~sigma ~template ~udecl ~env_ar ~ctx_params ~indnames ~arities ~arityconcl ~constructors ~env_ar_params ~cumulative ~poly ~private_ind ~finite = +let interp_mutual_inductive_constr ~sigma ~template ~udecl ~ctx_params ~indnames ~arities ~arityconcl ~constructors ~env_ar_params ~cumulative ~poly ~private_ind ~finite = (* Compute renewed arities *) let sigma = Evd.minimize_universes sigma in let nf = Evarutil.nf_evars_universes sigma in @@ -403,7 +403,6 @@ let interp_mutual_inductive_constr ~sigma ~template ~udecl ~env_ar ~ctx_params ~ }) indnames arities arityconcl constructors in - let variance = if poly && cumulative then Some (InferCumulativity.dummy_variance uctx) else None in (* Build the mutual inductive entry *) let mind_ent = { mind_entry_params = ctx_params; @@ -412,12 +411,10 @@ let interp_mutual_inductive_constr ~sigma ~template ~udecl ~env_ar ~ctx_params ~ mind_entry_inds = entries; mind_entry_private = if private_ind then Some false else None; mind_entry_universes = uctx; - mind_entry_variance = variance; + mind_entry_cumulative = poly && cumulative; } in - (if poly && cumulative then - InferCumulativity.infer_inductive env_ar mind_ent - else mind_ent), Evd.universe_binders sigma + mind_ent, Evd.universe_binders sigma let interp_params env udecl uparamsl paramsl = let sigma, udecl = interp_univ_decl_opt env udecl in @@ -504,7 +501,7 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not indimpls, List.map (fun impls -> userimpls @ impls) cimpls) indimpls constructors in - let mie, pl = interp_mutual_inductive_constr ~template ~sigma ~env_ar ~ctx_params ~udecl ~arities ~arityconcl ~constructors ~env_ar_params ~poly ~finite ~cumulative ~private_ind ~indnames in + let mie, pl = interp_mutual_inductive_constr ~template ~sigma ~ctx_params ~udecl ~arities ~arityconcl ~constructors ~env_ar_params ~poly ~finite ~cumulative ~private_ind ~indnames in (mie, pl, impls) -- cgit v1.2.3 From 82a1f73aa6c70672e212f9122c325425f9129570 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Tue, 29 Oct 2019 14:05:24 +0100 Subject: Don't pass (ignored) implicits to interp_mutual_inductive_constr --- vernac/comInductive.ml | 20 +++++++++++--------- 1 file changed, 11 insertions(+), 9 deletions(-) (limited to 'vernac/comInductive.ml') diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 5cf2b680ca..b603c54026 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -255,7 +255,7 @@ let inductive_levels env evd arities inds = in let cstrs_levels, min_levels, sizes = CList.split3 - (List.map2 (fun (_,tys,_) (arity,(ctx,du)) -> + (List.map2 (fun (_,tys) (arity,(ctx,du)) -> let len = List.length tys in let minlev = Sorts.univ_of_sort du in let minlev = @@ -350,28 +350,28 @@ let restrict_inductive_universes sigma ctx_params arities constructors = let uvars = Univ.LSet.empty in let uvars = Context.Rel.(fold_outside (Declaration.fold_constr merge_universes_of_constr) ctx_params ~init:uvars) in let uvars = List.fold_right merge_universes_of_constr arities uvars in - let uvars = List.fold_right (fun (_,ctypes,_) -> List.fold_right merge_universes_of_constr ctypes) constructors uvars in + let uvars = List.fold_right (fun (_,ctypes) -> List.fold_right merge_universes_of_constr ctypes) constructors uvars in Evd.restrict_universe_context sigma uvars let interp_mutual_inductive_constr ~sigma ~template ~udecl ~ctx_params ~indnames ~arities ~arityconcl ~constructors ~env_ar_params ~cumulative ~poly ~private_ind ~finite = (* Compute renewed arities *) let sigma = Evd.minimize_universes sigma in let nf = Evarutil.nf_evars_universes sigma in - let constructors = List.map (on_pi2 (List.map nf)) constructors in + let constructors = List.map (on_snd (List.map nf)) constructors in let arities = List.map EConstr.(to_constr sigma) arities in let sigma = List.fold_left make_anonymous_conclusion_flexible sigma arityconcl in let sigma, arities = inductive_levels env_ar_params sigma arities constructors in let sigma = Evd.minimize_universes sigma in let nf = Evarutil.nf_evars_universes sigma in let arities = List.map (on_snd nf) arities in - let constructors = List.map (on_pi2 (List.map nf)) constructors in + let constructors = List.map (on_snd (List.map nf)) constructors in let ctx_params = List.map Termops.(map_rel_decl (EConstr.to_constr sigma)) ctx_params in let arityconcl = List.map (Option.map (fun (_anon, s) -> EConstr.ESorts.kind sigma s)) arityconcl in let sigma = restrict_inductive_universes sigma ctx_params (List.map snd arities) constructors in let uctx = Evd.check_univ_decl ~poly sigma udecl in (* Build the inductive entries *) - let entries = List.map4 (fun indname (templatearity, arity) concl (cnames,ctypes,cimpls) -> + let entries = List.map4 (fun indname (templatearity, arity) concl (cnames,ctypes) -> let template_candidate () = templatearity || let ctor_levels = @@ -484,9 +484,10 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not List.init (List.length indl) EConstr.(fun i -> mkApp (mkRel (i + 1 + nuparams), uargs)) @ List.init nuparams EConstr.(fun i -> mkRel (i + 1)) in let generalize_constructor c = EConstr.Unsafe.to_constr (EConstr.Vars.substnl uparam_subst nparams c) in + let cimpls = List.map pi3 constructors in let constructors = List.map (fun (cnames,ctypes,cimpls) -> - (cnames,List.map generalize_constructor ctypes,cimpls)) - constructors + (cnames,List.map generalize_constructor ctypes)) + constructors in let ctx_params = ctx_params @ ctx_uparams in let userimpls = useruimpls @ userimpls in @@ -497,9 +498,10 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not (* Try further to solve evars, and instantiate them *) let sigma = solve_remaining_evars all_and_fail_flags env_params sigma in let impls = - List.map2 (fun indimpls (_,_,cimpls) -> + List.map2 (fun indimpls cimpls -> indimpls, List.map (fun impls -> - userimpls @ impls) cimpls) indimpls constructors + userimpls @ impls) cimpls) + indimpls cimpls in let mie, pl = interp_mutual_inductive_constr ~template ~sigma ~ctx_params ~udecl ~arities ~arityconcl ~constructors ~env_ar_params ~poly ~finite ~cumulative ~private_ind ~indnames in (mie, pl, impls) -- cgit v1.2.3