From 313e6bed17b400d638401a5c6e5d442eadb73d3a Mon Sep 17 00:00:00 2001 From: Jasper Hugunin Date: Mon, 4 Jun 2018 15:47:28 -0700 Subject: Implement uniform parameters in ComInductive Don't allow notations attached to uniform inductives --- plugins/funind/glob_term_to_relation.ml | 2 +- vernac/comInductive.ml | 49 ++++++++++++++++++++++++++------- vernac/comInductive.mli | 7 ++++- vernac/vernacentries.ml | 7 +++-- 4 files changed, 51 insertions(+), 14 deletions(-) diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 6b9b10312..5fc4293cb 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1499,7 +1499,7 @@ let do_build_inductive let _time2 = System.get_time () in try with_full_print - (Flags.silently (ComInductive.do_mutual_inductive rel_inds (Flags.is_universe_polymorphism ()) false false)) + (Flags.silently (ComInductive.do_mutual_inductive rel_inds (Flags.is_universe_polymorphism ()) false false ~uniform:ComInductive.NonUniformParameters)) Declarations.Finite with | UserError(s,msg) as e -> diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 0387b32ba..ad1ffa35a 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -146,7 +146,6 @@ let interp_cstrs env sigma impls mldata arity ind = let sigma, (ctyps'', cimpls) = on_snd List.split @@ List.fold_left_map (fun sigma l -> - on_snd (on_fst EConstr.Unsafe.to_constr) @@ interp_type_evars_impls env sigma ~impls l) sigma ctyps' in sigma, (cnames, ctyps'', cimpls) @@ -327,14 +326,17 @@ let check_param = function | CLocalPattern {CAst.loc} -> Loc.raise ?loc (Stream.Error "pattern with quote not allowed here") -let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite = +let interp_mutual_inductive_gen env0 (uparamsl,paramsl,indl) notations cum poly prv finite = check_all_names_different indl; List.iter check_param paramsl; - let env0 = Global.env() in + if not (List.is_empty uparamsl) && not (List.is_empty notations) + then user_err (str "Inductives with uniform parameters may not have attached notations."); let pl = (List.hd indl).ind_univs in let sigma, decl = interp_univ_decl_opt env0 pl in + let sigma, (uimpls, ((env_uparams, ctx_uparams), useruimpls)) = + interp_context_evars env0 sigma uparamsl in let sigma, (impls, ((env_params, ctx_params), userimpls)) = - interp_context_evars env0 sigma paramsl + interp_context_evars ~impl_env:uimpls env_uparams sigma paramsl in let indnames = List.map (fun ind -> ind.ind_name) indl in @@ -346,15 +348,15 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite = let sigma, arities = List.fold_left_map (fun sigma -> interp_ind_arity env_params sigma) sigma indl in let fullarities = List.map (fun (c, _, _) -> EConstr.it_mkProd_or_LetIn c ctx_params) arities in - let env_ar = push_types env0 indnames fullarities in + let env_ar = push_types env_uparams indnames fullarities in let env_ar_params = EConstr.push_rel_context ctx_params env_ar in (* Compute interpretation metadatas *) let indimpls = List.map (fun (_, _, impls) -> userimpls @ lift_implicits (Context.Rel.nhyps ctx_params) impls) arities in let arities = List.map pi1 arities and aritypoly = List.map pi2 arities in - let impls = compute_internalization_env env0 sigma ~impls (Inductive (params,true)) indnames fullarities indimpls in - let ntn_impls = compute_internalization_env env0 sigma (Inductive (params,true)) indnames fullarities indimpls in + let impls = compute_internalization_env env_uparams sigma ~impls (Inductive (params,true)) indnames fullarities indimpls in + let ntn_impls = compute_internalization_env env_uparams sigma (Inductive (params,true)) indnames fullarities indimpls in let mldatas = List.map2 (mk_mltype_data sigma env_params params) arities indnames in let sigma, constructors = @@ -365,6 +367,25 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite = List.fold_left3_map (fun sigma -> interp_cstrs env_ar_params sigma impls) sigma mldatas arities indl) () in + (* generalize over the uniform parameters *) + let nparams = Context.Rel.length ctx_params in + let nuparams = Context.Rel.length ctx_uparams in + let uargs = Context.Rel.to_extended_vect EConstr.mkRel 0 ctx_uparams in + let uparam_subst = + 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 constructors = List.map (fun (cnames,ctypes,cimpls) -> + (cnames,List.map generalize_constructor ctypes,cimpls)) + constructors + in + let ctx_params = ctx_params @ ctx_uparams in + let userimpls = useruimpls @ (lift_implicits (Context.Rel.nhyps ctx_uparams) userimpls) in + let indimpls = List.map (fun iimpl -> useruimpls @ (lift_implicits (Context.Rel.nhyps ctx_uparams) iimpl)) indimpls in + let fullarities = List.map (fun c -> EConstr.it_mkProd_or_LetIn c ctx_uparams) fullarities in + let env_ar = push_types env0 indnames fullarities in + let env_ar_params = EConstr.push_rel_context ctx_params env_ar in + (* Try further to solve evars, and instantiate them *) let sigma = solve_remaining_evars all_and_fail_flags env_params sigma (Evd.from_env env_params) in (* Compute renewed arities *) @@ -423,6 +444,9 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite = InferCumulativity.infer_inductive env_ar mind_ent else mind_ent), Evd.universe_binders sigma, impls +let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite = + interp_mutual_inductive_gen (Global.env()) ([],paramsl,indl) notations cum poly prv finite + (* Very syntactical equality *) let eq_local_binders bl1 bl2 = List.equal local_binder_eq bl1 bl2 @@ -505,10 +529,15 @@ type one_inductive_impls = Impargs.manual_explicitation list (* for inds *)* Impargs.manual_explicitation list list (* for constrs *) -let do_mutual_inductive indl cum poly prv finite = - let indl,coes,ntns = extract_mutual_inductive_declaration_components indl in +type uniform_inductive_flag = + | UniformParameters + | NonUniformParameters + +let do_mutual_inductive indl cum poly prv ~uniform finite = + let (params,indl),coes,ntns = extract_mutual_inductive_declaration_components indl in (* Interpret the types *) - let mie,pl,impls = interp_mutual_inductive indl ntns cum poly prv finite in + let indl = match uniform with UniformParameters -> (params, [], indl) | NonUniformParameters -> ([], params, indl) in + let mie,pl,impls = interp_mutual_inductive_gen (Global.env()) indl ntns cum poly prv finite in (* Declare the mutual inductive block with its associated schemes *) ignore (declare_mutual_inductive_with_eliminations mie pl impls); (* Declare the possible notations of inductive types *) diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli index 7ae8e8f71..4e30ed7de 100644 --- a/vernac/comInductive.mli +++ b/vernac/comInductive.mli @@ -19,9 +19,14 @@ open Decl_kinds (** Entry points for the vernacular commands Inductive and CoInductive *) +type uniform_inductive_flag = + | UniformParameters + | NonUniformParameters + val do_mutual_inductive : (one_inductive_expr * decl_notation list) list -> cumulative_inductive_flag -> - polymorphic -> private_flag -> Declarations.recursivity_kind -> unit + polymorphic -> private_flag -> uniform:uniform_inductive_flag -> + Declarations.recursivity_kind -> unit (************************************************************************) (** Internal API *) diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 6d1abeca1..e76921d1d 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -537,6 +537,8 @@ let should_treat_as_cumulative cum poly = else user_err Pp.(str "The NonCumulative prefix can only be used in a polymorphic context.") | None -> poly && Flags.is_polymorphic_inductive_cumulativity () +let should_treat_as_uniform () = ComInductive.NonUniformParameters (* TODO: Add a flag *) + let vernac_record cum k poly finite records = let is_cumulative = should_treat_as_cumulative cum poly in let map ((coe, (id, pl)), binders, sort, nameopt, cfs) = @@ -642,7 +644,8 @@ let vernac_inductive ~atts cum lo finite indl = in let indl = List.map unpack indl in let is_cumulative = should_treat_as_cumulative cum atts.polymorphic in - ComInductive.do_mutual_inductive indl is_cumulative atts.polymorphic lo finite + let uniform = should_treat_as_uniform () in + ComInductive.do_mutual_inductive indl is_cumulative atts.polymorphic lo ~uniform finite else user_err (str "Mixed record-inductive definitions are not allowed") (* @@ -2089,7 +2092,7 @@ let interp ?proof ~atts ~st c = | VernacExactProof c -> vernac_exact_proof c | VernacAssumption ((discharge,kind),nl,l) -> vernac_assumption ~atts discharge kind l nl - | VernacInductive (cum, priv,finite,l) -> vernac_inductive ~atts cum priv finite l + | VernacInductive (cum, priv, finite, l) -> vernac_inductive ~atts cum priv finite l | VernacFixpoint (discharge, l) -> vernac_fixpoint ~atts discharge l | VernacCoFixpoint (discharge, l) -> vernac_cofixpoint ~atts discharge l | VernacScheme l -> vernac_scheme l -- cgit v1.2.3 From 29ed1edfa71fec0b72f7286d6396a07cf895e49f Mon Sep 17 00:00:00 2001 From: Jasper Hugunin Date: Mon, 4 Jun 2018 17:26:07 -0700 Subject: Add flag Uniform Inductive Parameters --- vernac/vernacentries.ml | 15 ++++++++++++++- 1 file changed, 14 insertions(+), 1 deletion(-) diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index e76921d1d..5fda1a0da 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -537,7 +537,12 @@ let should_treat_as_cumulative cum poly = else user_err Pp.(str "The NonCumulative prefix can only be used in a polymorphic context.") | None -> poly && Flags.is_polymorphic_inductive_cumulativity () -let should_treat_as_uniform () = ComInductive.NonUniformParameters (* TODO: Add a flag *) +let uniform_inductive_parameters = ref false + +let should_treat_as_uniform () = + if !uniform_inductive_parameters + then ComInductive.UniformParameters + else ComInductive.NonUniformParameters let vernac_record cum k poly finite records = let is_cumulative = should_treat_as_cumulative cum poly in @@ -1473,6 +1478,14 @@ let _ = optread = Flags.is_polymorphic_inductive_cumulativity; optwrite = Flags.make_polymorphic_inductive_cumulativity } +let _ = + declare_bool_option + { optdepr = false; + optname = "Uniform inductive parameters"; + optkey = ["Uniform"; "Inductive"; "Parameters"]; + optread = (fun () -> !uniform_inductive_parameters); + optwrite = (fun b -> uniform_inductive_parameters := b) } + let _ = declare_int_option { optdepr = false; -- cgit v1.2.3 From 9b10e2383980c2f210049dfaf4a3031133d36ebd Mon Sep 17 00:00:00 2001 From: Jasper Hugunin Date: Mon, 4 Jun 2018 17:59:10 -0700 Subject: Add test for Uniform Inductive Parameters --- test-suite/success/uniform_inductive_parameters.v | 13 +++++++++++++ 1 file changed, 13 insertions(+) create mode 100644 test-suite/success/uniform_inductive_parameters.v diff --git a/test-suite/success/uniform_inductive_parameters.v b/test-suite/success/uniform_inductive_parameters.v new file mode 100644 index 000000000..42236a531 --- /dev/null +++ b/test-suite/success/uniform_inductive_parameters.v @@ -0,0 +1,13 @@ +Set Uniform Inductive Parameters. + +Inductive list (A : Type) := + | nil : list + | cons : A -> list -> list. +Check (list : Type -> Type). +Check (cons : forall A, A -> list A -> list A). + +Inductive list2 (A : Type) (A' := prod A A) := + | nil2 : list2 + | cons2 : A' -> list2 -> list2. +Check (list2 : Type -> Type). +Check (cons2 : forall A (A' := prod A A), A' -> list2 A -> list2 A). -- cgit v1.2.3 From ffb3ab4108fa7b6a8f03b865d6287663fc3743e5 Mon Sep 17 00:00:00 2001 From: Jasper Hugunin Date: Mon, 4 Jun 2018 18:43:25 -0700 Subject: Document option Uniform Inductive Parameters --- CHANGES | 3 +++ .../language/gallina-specification-language.rst | 26 ++++++++++++++++++++++ 2 files changed, 29 insertions(+) diff --git a/CHANGES b/CHANGES index 75f4df06a..886216724 100644 --- a/CHANGES +++ b/CHANGES @@ -52,6 +52,9 @@ Vernacular Commands - Nested proofs may be enabled through the option `Nested Proofs Allowed`. By default, they are disabled and produce an error. The deprecation warning which used to occur when using nested proofs has been removed. +- Added option Uniform Inductive Parameters which abstracts over parameters + before typechecking constructors, allowing to write for example + `Inductive list (A : Type) := nil : list | cons : A -> list -> list.` Coq binaries and process model diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index c26ae2a93..56c8aac94 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -905,6 +905,32 @@ Parametrized inductive types sort for the inductive definition and will produce a less convenient rule for case elimination. +.. opt:: Uniform Inductive Parameters + + When this option is set (it is off by default), + inductive definitions are abstracted over their parameters + before typechecking constructors, allowing to write: + + .. coqtop:: all undo + + Set Uniform Inductive Parameters. + Inductive list3 (A:Set) : Set := + | nil3 : list3 + | cons3 : A -> list3 -> list3. + + This behavior is essentially equivalent to starting a new section + and using :cmd:`Context` to give the uniform parameters, like so + (cf. :ref:`section-mechanism`): + + .. coqtop:: all undo + + Section list3. + Context (A:Set). + Inductive list3 : Set := + | nil3 : list3 + | cons3 : A -> list3 -> list3. + End list3. + .. seealso:: Section :ref:`inductive-definitions` and the :tacn:`induction` tactic. -- cgit v1.2.3