diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/classes.ml | 2 | ||||
| -rw-r--r-- | vernac/comAssumption.ml | 2 | ||||
| -rw-r--r-- | vernac/comInductive.ml | 44 | ||||
| -rw-r--r-- | vernac/comInductive.mli | 40 | ||||
| -rw-r--r-- | vernac/declaremods.ml | 22 | ||||
| -rw-r--r-- | vernac/egramcoq.ml | 12 | ||||
| -rw-r--r-- | vernac/metasyntax.ml | 2 | ||||
| -rw-r--r-- | vernac/record.ml | 9 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 2 |
9 files changed, 63 insertions, 72 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml index 0333b73ffe..c9b5144299 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -410,7 +410,7 @@ let do_instance_resolve_TC termtype sigma env = (* Beware of this step, it is required as to minimize universes. *) let sigma = Evd.minimize_universes sigma in (* Check that the type is free of evars now. *) - Pretyping.check_evars env (Evd.from_env env) sigma termtype; + Pretyping.check_evars env sigma termtype; termtype, sigma let do_instance_type_ctx_instance props k env' ctx' sigma ~program_mode subst = diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index a001420f74..8a403e5a03 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -255,7 +255,7 @@ let context ~poly l = let sigma, (_, ((_env, ctx), impls)) = interp_context_evars ~program_mode:false env sigma l in (* Note, we must use the normalized evar from now on! *) let sigma = Evd.minimize_universes sigma in - let ce t = Pretyping.check_evars env (Evd.from_env env) sigma t in + let ce t = Pretyping.check_evars env sigma t in let () = List.iter (fun decl -> Context.Rel.Declaration.iter_constr ce decl) ctx in (* reorder, evar-normalize and add implicit status *) let ctx = List.rev_map (fun d -> diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 2aee9bd47f..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 = @@ -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 @@ -350,33 +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 ~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 ~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 - 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 entries = List.map4 (fun indname (templatearity, arity) concl (cnames,ctypes) -> let template_candidate () = templatearity || let ctor_levels = @@ -390,7 +385,7 @@ let interp_mutual_inductive_constr ~env0 ~sigma ~template ~udecl ~env_ar ~env_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 -> @@ -408,7 +403,6 @@ let interp_mutual_inductive_constr ~env0 ~sigma ~template ~udecl ~env_ar ~env_pa }) 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; @@ -417,12 +411,10 @@ let interp_mutual_inductive_constr ~env0 ~sigma ~template ~udecl ~env_ar ~env_pa 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 @@ -492,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 @@ -505,11 +498,12 @@ 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 ~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 ~template ~sigma ~ctx_params ~udecl ~arities ~arityconcl ~constructors ~env_ar_params ~poly ~finite ~cumulative ~private_ind ~indnames in (mie, pl, impls) diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli index ef05b213d8..cc104b3762 100644 --- a/vernac/comInductive.mli +++ b/vernac/comInductive.mli @@ -49,24 +49,22 @@ val declare_mutual_inductive_with_eliminations -> Names.MutInd.t [@@ocaml.deprecated "Please use DeclareInd.declare_mutual_inductive_with_eliminations"] -val interp_mutual_inductive_constr : - env0:Environ.env -> - sigma:Evd.evar_map -> - template:bool option -> - udecl:UState.universe_decl -> - env_ar:Environ.env -> - env_params:Environ.env -> - ctx_params:(EConstr.t, EConstr.t) Context.Rel.Declaration.pt list -> - indnames:Names.Id.t list -> - arities:EConstr.t list -> - arityconcl:(bool * EConstr.ESorts.t) option list -> - constructors:(Names.Id.t list * Constr.constr list * 'a list list) list -> - env_ar_params:Environ.env -> - cumulative:bool -> - poly:bool -> - private_ind:bool -> - finite:Declarations.recursivity_kind -> - Entries.mutual_inductive_entry * UnivNames.universe_binders +val interp_mutual_inductive_constr + : sigma:Evd.evar_map + -> template:bool option + -> udecl:UState.universe_decl + -> ctx_params:(EConstr.t, EConstr.t) Context.Rel.Declaration.pt list + -> indnames:Names.Id.t list + -> arities:EConstr.t list + -> arityconcl:(bool * EConstr.ESorts.t) option list + -> constructors:(Names.Id.t list * Constr.constr list) list + -> env_ar_params:Environ.env + (** Environment with the inductives and parameters in the rel_context *) + -> cumulative:bool + -> poly:bool + -> private_ind:bool + -> finite:Declarations.recursivity_kind + -> Entries.mutual_inductive_entry * UnivNames.universe_binders (************************************************************************) (** Internal API, exported for Record *) @@ -78,17 +76,17 @@ val should_auto_template : Id.t -> bool -> bool inductive under consideration. *) val template_polymorphism_candidate - : Environ.env + : template_check:bool -> ctor_levels:Univ.LSet.t -> Entries.universes_entry -> Constr.rel_context -> Sorts.t option -> bool -(** [template_polymorphism_candidate env ~ctor_levels uctx params +(** [template_polymorphism_candidate ~template_check ~ctor_levels uctx params conclsort] is [true] iff an inductive with params [params], conclusion [conclsort] and universe levels appearing in the constructor arguments [ctor_levels] would be definable as template polymorphic. It should have at least one universe in its monomorphic universe context that can be made parametric in its - conclusion sort, if one is given. If the [Template Check] flag is + conclusion sort, if one is given. If the [template_check] flag is false we just check that the conclusion sort is not small. *) diff --git a/vernac/declaremods.ml b/vernac/declaremods.ml index 54dda09e83..c816a4eb4f 100644 --- a/vernac/declaremods.ml +++ b/vernac/declaremods.ml @@ -550,7 +550,7 @@ let intern_arg (acc, cst) (idl,(typ,ann)) = let lib_dir = Lib.library_dp() in let env = Global.env() in let (mty, _, cst') = Modintern.interp_module_ast env Modintern.ModType typ in - let () = Global.push_context_set true cst' in + let () = Global.push_context_set ~strict:true cst' in let env = Global.env () in let sobjs = get_module_sobjs false env inl mty in let mp0 = get_module_path mty in @@ -674,7 +674,7 @@ module RawModOps = struct let start_module export id args res fs = let mp = Global.start_module id in let arg_entries_r, cst = intern_args args in - let () = Global.push_context_set true cst in + let () = Global.push_context_set ~strict:true cst in let env = Global.env () in let res_entry_o, subtyps, cst = match res with | Enforce (res,ann) -> @@ -689,7 +689,7 @@ let start_module export id args res fs = let typs, cst = build_subtypes env mp arg_entries_r resl in None, typs, cst in - let () = Global.push_context_set true cst in + let () = Global.push_context_set ~strict:true cst in openmod_info := { cur_typ = res_entry_o; cur_typs = subtyps }; let prefix = Lib.start_module export id mp fs in Nametab.(push_dir (Until 1) (prefix.obj_dir) (GlobDirRef.DirOpenModule prefix)); @@ -782,7 +782,7 @@ let declare_module id args res mexpr_o fs = | None -> None | _ -> inl_res in - let () = Global.push_context_set true cst in + let () = Global.push_context_set ~strict:true cst in let mp_env,resolver = Global.add_module id entry inl in (* Name consistency check : kernel vs. library *) @@ -804,10 +804,10 @@ module RawModTypeOps = struct let start_modtype id args mtys fs = let mp = Global.start_modtype id in let arg_entries_r, cst = intern_args args in - let () = Global.push_context_set true cst in + let () = Global.push_context_set ~strict:true cst in let env = Global.env () in let sub_mty_l, cst = build_subtypes env mp arg_entries_r mtys in - let () = Global.push_context_set true cst in + let () = Global.push_context_set ~strict:true cst in openmodtype_info := sub_mty_l; let prefix = Lib.start_modtype id mp fs in Nametab.(push_dir (Until 1) (prefix.obj_dir) (GlobDirRef.DirOpenModtype prefix)); @@ -835,19 +835,19 @@ let declare_modtype id args mtys (mty,ann) fs = then we adds the module parameters to the global env. *) let mp = Global.start_modtype id in let arg_entries_r, cst = intern_args args in - let () = Global.push_context_set true cst in + let () = Global.push_context_set ~strict:true cst in let params = mk_params_entry arg_entries_r in let env = Global.env () in let mte, _, cst = Modintern.interp_module_ast env Modintern.ModType mty in - let () = Global.push_context_set true cst in + let () = Global.push_context_set ~strict:true cst in let env = Global.env () in (* We check immediately that mte is well-formed *) let _, _, _, cst = Mod_typing.translate_mse env None inl mte in - let () = Global.push_context_set true cst in + let () = Global.push_context_set ~strict:true cst in let env = Global.env () in let entry = params, mte in let sub_mty_l, cst = build_subtypes env mp arg_entries_r mtys in - let () = Global.push_context_set true cst in + let () = Global.push_context_set ~strict:true cst in let env = Global.env () in let sobjs = get_functor_sobjs false env inl entry in let subst = map_mp (get_module_path (snd entry)) mp empty_delta_resolver in @@ -903,7 +903,7 @@ let type_of_incl env is_mod = function let declare_one_include (me_ast,annot) = let env = Global.env() in let me, kind, cst = Modintern.interp_module_ast env Modintern.ModAny me_ast in - let () = Global.push_context_set true cst in + let () = Global.push_context_set ~strict:true cst in let env = Global.env () in let is_mod = (kind == Modintern.Module) in let cur_mp = Lib.current_mp () in diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml index e02f94629c..b65a126f55 100644 --- a/vernac/egramcoq.ml +++ b/vernac/egramcoq.ml @@ -247,7 +247,7 @@ type (_, _) entry = | TTReference : ('self, qualid) entry | TTBigint : ('self, string) entry | TTConstr : notation_entry * prod_info * 'r target -> ('r, 'r) entry -| TTConstrList : prod_info * string Tok.p list * 'r target -> ('r, 'r list) entry +| TTConstrList : notation_entry * prod_info * string Tok.p list * 'r target -> ('r, 'r list) entry | TTPattern : int -> ('self, cases_pattern_expr) entry | TTOpenBinderList : ('self, local_binder_expr list) entry | TTClosedBinderList : string Tok.p list -> ('self, local_binder_expr list list) entry @@ -347,12 +347,12 @@ let symbol_of_target : type s. _ -> _ -> _ -> _ -> s target -> (s, s) mayrec_sym let symbol_of_entry : type s r. _ -> _ -> (s, r) entry -> (s, r) mayrec_symbol = fun assoc from typ -> match typ with | TTConstr (s, p, forpat) -> symbol_of_target s p assoc from forpat -| TTConstrList (typ', [], forpat) -> - begin match symbol_of_target InConstrEntry typ' assoc from forpat with +| TTConstrList (s, typ', [], forpat) -> + begin match symbol_of_target s typ' assoc from forpat with | MayRecNo s -> MayRecNo (Alist1 s) | MayRecMay s -> MayRecMay (Alist1 s) end -| TTConstrList (typ', tkl, forpat) -> - begin match symbol_of_target InConstrEntry typ' assoc from forpat with +| TTConstrList (s, typ', tkl, forpat) -> + begin match symbol_of_target s typ' assoc from forpat with | MayRecNo s -> MayRecNo (Alist1sep (s, make_sep_rules tkl)) | MayRecMay s -> MayRecMay (Alist1sep (s, make_sep_rules tkl)) end | TTPattern p -> MayRecNo (Aentryl (Constr.pattern, string_of_int p)) @@ -369,7 +369,7 @@ let interp_entry forpat e = match e with | ETProdBigint -> TTAny TTBigint | ETProdConstr (s,p) -> TTAny (TTConstr (s, p, forpat)) | ETProdPattern p -> TTAny (TTPattern p) -| ETProdConstrList (p, tkl) -> TTAny (TTConstrList (p, tkl, forpat)) +| ETProdConstrList (s, p, tkl) -> TTAny (TTConstrList (s, p, tkl, forpat)) | ETProdBinderList ETBinderOpen -> TTAny TTOpenBinderList | ETProdBinderList (ETBinderClosed tkl) -> TTAny (TTClosedBinderList tkl) diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index e23522da9e..35681aed13 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -611,7 +611,7 @@ let expand_list_rule s typ tkl x n p ll = else if Int.equal i (p+n) then let hds = GramConstrListMark (p+n,true,p) :: hds - @ [GramConstrNonTerminal (ETProdConstrList (typ,tkl), Some x)] in + @ [GramConstrNonTerminal (ETProdConstrList (s, typ,tkl), Some x)] in distribute hds ll else distribute (GramConstrListMark (i+1,false,p) :: hds @ [main]) ll @ diff --git a/vernac/record.ml b/vernac/record.ml index d85b71df44..ea10e06d02 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -202,7 +202,7 @@ let typecheck_params_and_fields finite def poly pl ps records = in let univs = Evd.check_univ_decl ~poly sigma decl in let ubinders = Evd.universe_binders sigma in - let ce t = Pretyping.check_evars env0 (Evd.from_env env0) sigma (EConstr.of_constr t) in + let ce t = Pretyping.check_evars env0 sigma (EConstr.of_constr t) in let () = List.iter (iter_constr ce) (List.rev newps) in ubinders, univs, template, newps, imps, ans @@ -411,7 +411,6 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa | Polymorphic_entry (nas, ctx) -> true, Polymorphic_entry (nas, ctx) in - let variance = if poly && cumulative then Some (InferCumulativity.dummy_variance ctx) else None in let binder_name = match name with | None -> @@ -447,7 +446,8 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa univs) param_levels fields in - ComInductive.template_polymorphism_candidate (Global.env ()) ~ctor_levels univs params + let template_check = Environ.check_template (Global.env ()) in + ComInductive.template_polymorphism_candidate ~template_check ~ctor_levels univs params (Some (Sorts.sort_of_univ min_univ)) in match template with @@ -477,10 +477,9 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa mind_entry_inds = blocks; mind_entry_private = None; mind_entry_universes = univs; - mind_entry_variance = variance; + mind_entry_cumulative = poly && cumulative; } in - let mie = InferCumulativity.infer_inductive (Global.env ()) mie in let impls = List.map (fun _ -> paramimpls, []) record_data in let kn = DeclareInd.declare_mutual_inductive_with_eliminations mie ubinders impls ~primitive_expected:!primitive_flag diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index e4965614d8..439ec61d38 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1621,7 +1621,7 @@ let vernac_global_check c = let c,uctx = interp_constr env sigma c in let senv = Global.safe_env() in let uctx = UState.context_set uctx in - let senv = Safe_typing.push_context_set false uctx senv in + let senv = Safe_typing.push_context_set ~strict:false uctx senv in let c = EConstr.to_constr sigma c in let j = Safe_typing.typing senv c in let env = Safe_typing.env_of_safe_env senv in |