diff options
Diffstat (limited to 'vernac/comInductive.ml')
| -rw-r--r-- | vernac/comInductive.ml | 197 |
1 files changed, 69 insertions, 128 deletions
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 98b869d72e..36aa7a37a2 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -15,18 +15,15 @@ open Util open Constr open Context open Environ -open Declare open Names open Libnames open Nameops open Constrexpr open Constrexpr_ops open Constrintern -open Impargs open Reductionops open Type_errors open Pretyping -open Indschemes open Context.Rel.Declaration open Entries @@ -80,12 +77,6 @@ type structured_one_inductive_expr = { ind_lc : (Id.t * constr_expr) list } -let minductive_message = function - | [] -> user_err Pp.(str "No inductive definition.") - | [x] -> (Id.print x ++ str " is defined") - | l -> hov 0 (prlist_with_sep pr_comma Id.print l ++ - spc () ++ str "are defined") - let check_all_names_different indl = let ind_names = List.map (fun ind -> ind.ind_name) indl in let cstr_names = List.map_append (fun ind -> List.map fst ind.ind_lc) indl in @@ -363,6 +354,67 @@ 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 = + (* 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 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 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 + 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 (_,ctyps,_) -> + List.iter (fun c -> check_evars env_ar_params (Evd.from_env 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) -> + let template_candidate () = + templatearity || template_polymorphism_candidate env0 uctx ctx_params concl in + let template = match template with + | Some template -> + if poly && template then user_err + Pp.(strbrk "Template-polymorphism and universe polymorphism are not compatible."); + if template && not (template_candidate ()) then + user_err Pp.(strbrk "Inductive " ++ Id.print indname ++ + str" cannot be made template polymorphic."); + template + | None -> + should_auto_template indname (template_candidate ()) + in + { mind_entry_typename = indname; + mind_entry_arity = arity; + mind_entry_template = template; + mind_entry_consnames = cnames; + mind_entry_lc = ctypes + }) + 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; + mind_entry_record = None; + mind_entry_finite = finite; + mind_entry_inds = entries; + mind_entry_private = if private_ind then Some false else None; + mind_entry_universes = uctx; + mind_entry_variance = variance; + } + in + (if poly && cumulative then + InferCumulativity.infer_inductive env_ar mind_ent + else mind_ent), Evd.universe_binders sigma + let interp_params env udecl uparamsl paramsl = let sigma, udecl = interp_univ_decl_opt env udecl in let sigma, (uimpls, ((env_uparams, ctx_uparams), useruimpls)) = @@ -441,73 +493,16 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not let fullarities = List.map (fun c -> EConstr.it_mkProd_or_LetIn c ctx_uparams) fullarities in let env_ar = push_types env0 indnames relevances 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 in - (* Compute renewed arities *) - let sigma = Evd.minimize_universes sigma in - let nf = Evarutil.nf_evars_universes sigma in - let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf cl,impsl)) 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 (fun (template, arity) -> template, nf arity) arities in - let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf cl,impsl)) 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 - 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 (_,ctyps,_) -> - List.iter (fun c -> check_evars env_ar_params (Evd.from_env env_ar_params) sigma (EConstr.of_constr c)) ctyps) - constructors; - - (* Build the inductive entries *) - let entries = List.map4 (fun ind (templatearity, arity) concl (cnames,ctypes,cimpls) -> - let template_candidate () = - templatearity || template_polymorphism_candidate env0 uctx ctx_params concl in - let template = match template with - | Some template -> - if poly && template then user_err - Pp.(strbrk "Template-polymorphism and universe polymorphism are not compatible."); - if template && not (template_candidate ()) then - user_err Pp.(strbrk "Inductive " ++ Id.print ind.ind_name ++ - str" cannot be made template polymorphic."); - template - | None -> - should_auto_template ind.ind_name (template_candidate ()) - in - { mind_entry_typename = ind.ind_name; - mind_entry_arity = arity; - mind_entry_template = template; - mind_entry_consnames = cnames; - mind_entry_lc = ctypes - }) - indl arities arityconcl constructors - in let impls = - List.map2 (fun indimpls (_,_,cimpls) -> + List.map2 (fun indimpls (_,_,cimpls) -> indimpls, List.map (fun impls -> - userimpls @ impls) cimpls) indimpls 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; - mind_entry_record = None; - mind_entry_finite = finite; - mind_entry_inds = entries; - mind_entry_private = if private_ind then Some false else None; - mind_entry_universes = uctx; - mind_entry_variance = variance; - } + userimpls @ impls) cimpls) indimpls constructors in - (if poly && cumulative then - InferCumulativity.infer_inductive env_ar mind_ent - else mind_ent), Evd.universe_binders sigma, impls + 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 + (mie, pl, impls) + (* Very syntactical equality *) let eq_local_binders bl1 bl2 = @@ -541,62 +536,6 @@ let extract_mutual_inductive_declaration_components indl = let indl = extract_inductive indl in (params,indl), coes, List.flatten ntnl -let is_recursive mie = - let rec is_recursive_constructor lift typ = - match Constr.kind typ with - | Prod (_,arg,rest) -> - not (EConstr.Vars.noccurn Evd.empty (* FIXME *) lift (EConstr.of_constr arg)) || - is_recursive_constructor (lift+1) rest - | LetIn (na,b,t,rest) -> is_recursive_constructor (lift+1) rest - | _ -> false - in - match mie.mind_entry_inds with - | [ind] -> - let nparams = List.length mie.mind_entry_params in - List.exists (fun t -> is_recursive_constructor (nparams+1) t) ind.mind_entry_lc - | _ -> false - -let warn_non_primitive_record = - CWarnings.create ~name:"non-primitive-record" ~category:"record" - (fun indsp -> - (hov 0 (str "The record " ++ Nametab.pr_global_env Id.Set.empty (GlobRef.IndRef indsp) ++ - strbrk" could not be defined as a primitive record"))) - -let declare_mutual_inductive_with_eliminations ?(primitive_expected=false) mie pl impls = - (* spiwack: raises an error if the structure is supposed to be non-recursive, - but isn't *) - begin match mie.mind_entry_finite with - | Declarations.BiFinite when is_recursive mie -> - if Option.has_some mie.mind_entry_record then - user_err Pp.(str "Records declared with the keywords Record or Structure cannot be recursive. You can, however, define recursive records using the Inductive or CoInductive command.") - else - user_err Pp.(str ("Types declared with the keyword Variant cannot be recursive. Recursive types are defined with the Inductive and CoInductive command.")) - | _ -> () - end; - let names = List.map (fun e -> e.mind_entry_typename) mie.mind_entry_inds in - let (_, kn), prim = declare_mind mie in - let mind = Global.mind_of_delta_kn kn in - if primitive_expected && not prim then warn_non_primitive_record (mind,0); - Declare.declare_univ_binders (GlobRef.IndRef (mind,0)) pl; - List.iteri (fun i (indimpls, constrimpls) -> - let ind = (mind,i) in - let gr = GlobRef.IndRef ind in - maybe_declare_manual_implicits false gr indimpls; - List.iteri - (fun j impls -> - maybe_declare_manual_implicits false - (GlobRef.ConstructRef (ind, succ j)) impls) - constrimpls) - impls; - Flags.if_verbose Feedback.msg_info (minductive_message names); - if mie.mind_entry_private == None - then declare_default_schemes mind; - mind - -type one_inductive_impls = - Impargs.manual_implicits (* for inds *) * - Impargs.manual_implicits list (* for constrs *) - type uniform_inductive_flag = | UniformParameters | NonUniformParameters @@ -607,7 +546,7 @@ let do_mutual_inductive ~template udecl indl ~cumulative ~poly ~private_ind ~uni let indl = match uniform with UniformParameters -> (params, [], indl) | NonUniformParameters -> ([], params, indl) in let mie,pl,impls = interp_mutual_inductive_gen (Global.env()) ~template udecl indl ntns ~cumulative ~poly ~private_ind finite in (* Declare the mutual inductive block with its associated schemes *) - ignore (declare_mutual_inductive_with_eliminations mie pl impls); + ignore (DeclareInd.declare_mutual_inductive_with_eliminations mie pl impls); (* Declare the possible notations of inductive types *) List.iter (Metasyntax.add_notation_interpretation (Global.env ())) ntns; (* Declare the coercions *) @@ -652,3 +591,5 @@ let make_cases ind = let consref = GlobRef.ConstructRef (ith_constructor_of_inductive ind (i + 1)) in (Libnames.string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty consref) :: al') :: l) mip.mind_nf_lc [] + +let declare_mutual_inductive_with_eliminations = DeclareInd.declare_mutual_inductive_with_eliminations |