diff options
Diffstat (limited to 'vernac/comInductive.ml')
| -rw-r--r-- | vernac/comInductive.ml | 53 |
1 files changed, 30 insertions, 23 deletions
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 8de1c69424..edb03a5c89 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -42,7 +42,6 @@ let should_auto_template = let auto = ref true in let () = declare_bool_option { optdepr = false; - optname = "Automatically make some inductive types template polymorphic"; optkey = ["Auto";"Template";"Polymorphism"]; optread = (fun () -> !auto); optwrite = (fun b -> auto := b); } @@ -323,16 +322,15 @@ 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 ~template_check ~ctor_levels uctx params concl = +let template_polymorphism_candidate ~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 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 + IndTyping.template_polymorphic_univs ~ctor_levels uctx params conclu in not (Univ.LSet.is_empty conclunivs) | Entries.Polymorphic_entry _ -> false @@ -385,7 +383,7 @@ let interp_mutual_inductive_constr ~sigma ~template ~udecl ~ctx_params ~indnames List.fold_left (fun levels c -> add_levels c levels) param_levels ctypes in - template_polymorphism_candidate ~template_check:(Environ.check_template env_ar_params) ~ctor_levels uctx ctx_params concl + template_polymorphism_candidate ~ctor_levels uctx ctx_params concl in let template = match template with | Some template -> @@ -435,32 +433,33 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not then user_err (str "Inductives with uniform parameters may not have attached notations."); let indnames = List.map (fun ind -> ind.ind_name) indl in - let sigma, env_params, infos = + + (* In case of template polymorphism, we need to compute more constraints *) + let env0 = if poly then env0 else Environ.set_universes_lbound env0 Univ.Level.prop in + + let sigma, env_params, (ctx_params, env_uparams, ctx_uparams, params, userimpls, useruimpls, impls, udecl) = interp_params env0 udecl uparamsl paramsl in (* Interpret the arities *) let arities = List.map (intern_ind_arity env_params sigma) indl in - let sigma, env_params, (ctx_params, env_uparams, ctx_uparams, params, userimpls, useruimpls, impls, udecl), arities, is_template = - let is_template = List.exists (fun (_,_,_,pseudo_poly) -> not (Option.is_empty pseudo_poly)) arities in - if not poly && is_template then - (* In case of template polymorphism, we need to compute more constraints *) - let env0 = Environ.set_universes_lbound env0 Univ.Level.prop in - let sigma, env_params, infos = - interp_params env0 udecl uparamsl paramsl - in - let arities = List.map (intern_ind_arity env_params sigma) indl in - sigma, env_params, infos, arities, is_template - else sigma, env_params, infos, arities, is_template - in - let sigma, arities = List.fold_left_map (pretype_ind_arity env_params) sigma arities in let arities, relevances, arityconcl, indimpls = List.split4 arities in - let fullarities = List.map (fun c -> EConstr.it_mkProd_or_LetIn c ctx_params) arities in + let lift1_ctx ctx = + let t = EConstr.it_mkProd_or_LetIn EConstr.mkProp ctx in + let t = EConstr.Vars.lift 1 t in + let ctx, _ = EConstr.decompose_prod_assum sigma t in + ctx + in + let ctx_params_lifted, fullarities = CList.fold_left_map + (fun ctx_params c -> lift1_ctx ctx_params, EConstr.it_mkProd_or_LetIn c ctx_params) + ctx_params + arities + in let env_ar = push_types env_uparams indnames relevances fullarities in - let env_ar_params = EConstr.push_rel_context ctx_params env_ar in + let env_ar_params = EConstr.push_rel_context ctx_params_lifted env_ar in (* Compute interpretation metadatas *) let indimpls = List.map (fun impls -> userimpls @ impls) indimpls in @@ -511,6 +510,9 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not let eq_local_binders bl1 bl2 = List.equal local_binder_eq bl1 bl2 +let eq_params (up1,p1) (up2,p2) = + eq_local_binders up1 up2 && Option.equal eq_local_binders p1 p2 + let extract_coercions indl = let mkqid (_,({CAst.v=id},_)) = qualid_of_ident id in let extract lc = List.filter (fun (iscoe,_) -> iscoe) lc in @@ -521,7 +523,7 @@ let extract_params indl = match paramsl with | [] -> anomaly (Pp.str "empty list of inductive types.") | params::paramsl -> - if not (List.for_all (eq_local_binders params) paramsl) then user_err Pp.(str + if not (List.for_all (eq_params params) paramsl) then user_err Pp.(str "Parameters should be syntactically the same for each inductive type."); params @@ -546,7 +548,12 @@ type uniform_inductive_flag = let do_mutual_inductive ~template udecl indl ~cumulative ~poly ~private_ind ~uniform finite = let (params,indl),coes,ntns = extract_mutual_inductive_declaration_components indl in (* Interpret the types *) - let indl = match uniform with UniformParameters -> (params, [], indl) | NonUniformParameters -> ([], params, indl) in + let indl = match params with + | uparams, Some params -> (uparams, params, indl) + | params, None -> 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 (DeclareInd.declare_mutual_inductive_with_eliminations mie pl impls); |