diff options
Diffstat (limited to 'toplevel/record.ml')
| -rw-r--r-- | toplevel/record.ml | 122 |
1 files changed, 70 insertions, 52 deletions
diff --git a/toplevel/record.ml b/toplevel/record.ml index 737b7fb5..dc2c9264 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -90,9 +90,10 @@ let binder_of_decl = function let binders_of_decls = List.map binder_of_decl -let typecheck_params_and_fields def id t ps nots fs = +let typecheck_params_and_fields def id pl t ps nots fs = let env0 = Global.env () in - let evars = ref (Evd.from_env env0) in + let ctx = Evd.make_evar_universe_context env0 pl in + let evars = ref (Evd.from_ctx ctx) in let _ = let error bk (loc, name) = match bk, name with @@ -130,14 +131,21 @@ let typecheck_params_and_fields def id t ps nots fs = Pretyping.solve_remaining_evars Pretyping.all_and_fail_flags env_ar !evars (Evd.empty,!evars) in let evars, nf = Evarutil.nf_evars_and_universes sigma in let arity = nf t' in - let evars = + let arity, evars = let _, univ = compute_constructor_level evars env_ar newfs in let ctx, aritysort = Reduction.dest_arity env0 arity in assert(List.is_empty ctx); (* Ensured by above analysis *) if Sorts.is_prop aritysort || - (Sorts.is_set aritysort && engagement env0 = Some ImpredicativeSet) then - evars - else Evd.set_leq_sort env_ar evars (Type univ) aritysort + (Sorts.is_set aritysort && is_impredicative_set env0) then + arity, evars + else + let evars = Evd.set_leq_sort env_ar evars (Type univ) aritysort in + if Univ.is_small_univ univ then + (* We can assume that the level aritysort is not constrained + and clear it. *) + mkArity (ctx, Sorts.sort_of_univ univ), + Evd.set_eq_sort env_ar evars (Prop Pos) aritysort + else arity, evars in let evars, nf = Evarutil.nf_evars_and_universes evars in let newps = map_rel_context nf newps in @@ -145,15 +153,15 @@ let typecheck_params_and_fields def id t ps nots fs = let ce t = Evarutil.check_evars env0 Evd.empty evars t in List.iter (fun (n, b, t) -> Option.iter ce b; ce t) (List.rev newps); List.iter (fun (n, b, t) -> Option.iter ce b; ce t) (List.rev newfs); - Evd.universe_context evars, nf arity, template, imps, newps, impls, newfs + Evd.universe_context ?names:pl evars, nf arity, template, imps, newps, impls, newfs let degenerate_decl (na,b,t) = let id = match na with | Name id -> id | Anonymous -> anomaly (Pp.str "Unnamed record variable") in match b with - | None -> (id, Entries.LocalAssum t) - | Some b -> (id, Entries.LocalDef b) + | None -> (id, LocalAssum t) + | Some b -> (id, LocalDef b) type record_error = | MissingProj of Id.t * Id.t list @@ -232,7 +240,8 @@ let declare_projections indsp ?(kind=StructureComponent) binder_name coers field let (mib,mip) = Global.lookup_inductive indsp in let u = Declareops.inductive_instance mib in let paramdecls = Inductive.inductive_paramdecls (mib, u) in - let poly = mib.mind_polymorphic and ctx = Univ.instantiate_univ_context mib.mind_universes in + let poly = mib.mind_polymorphic in + let ctx = Univ.instantiate_univ_context mib.mind_universes in let indu = indsp, u in let r = mkIndU (indsp,u) in let rp = applist (r, Termops.extended_rel_list 0 paramdecls) in @@ -288,16 +297,17 @@ let declare_projections indsp ?(kind=StructureComponent) binder_name coers field try let entry = { const_entry_body = - Future.from_val (Term_typing.mk_pure_proof proj); + Future.from_val (Safe_typing.mk_pure_proof proj); const_entry_secctx = None; const_entry_type = Some projtyp; const_entry_polymorphic = poly; - const_entry_universes = ctx; + const_entry_universes = + if poly then ctx else Univ.UContext.empty; const_entry_opaque = false; const_entry_inline_code = false; const_entry_feedback = None } in let k = (DefinitionEntry entry,IsDefinition kind) in - let kn = declare_constant ~internal:KernelSilent fid k in + let kn = declare_constant ~internal:InternalTacticRequest fid k in let constr_fip = let proj_args = (*Rel 1 refers to "x"*) paramargs@[mkRel 1] in applist (mkConstU (kn,u),proj_args) @@ -366,7 +376,7 @@ let declare_structure finite poly ctx id idbuild paramimpls params arity templat mind_entry_polymorphic = poly; mind_entry_private = None; mind_entry_universes = ctx } in - let kn = Command.declare_mutual_inductive_with_eliminations mie [(paramimpls,[])] in + let kn = Command.declare_mutual_inductive_with_eliminations mie [] [(paramimpls,[])] in let rsp = (kn,0) in (* This is ind path of idstruc *) let cstr = (rsp,1) in let kinds,sp_projs = declare_projections rsp ~kind binder_name coers fieldimpls fields in @@ -396,44 +406,49 @@ let declare_class finite def poly ctx id idbuild paramimpls params arity let impl, projs = match fields with | [(Name proj_name, _, field)] when def -> - let class_body = it_mkLambda_or_LetIn field params in - let _class_type = it_mkProd_or_LetIn arity params in - let class_entry = - Declare.definition_entry (* ?types:class_type *) ~poly ~univs:ctx class_body in - let cst = Declare.declare_constant (snd id) - (DefinitionEntry class_entry, IsDefinition Definition) - in - let cstu = (cst, if poly then Univ.UContext.instance ctx else Univ.Instance.empty) in - let inst_type = appvectc (mkConstU cstu) (Termops.rel_vect 0 (List.length params)) in - let proj_type = - it_mkProd_or_LetIn (mkProd(Name binder_name, inst_type, lift 1 field)) params in - let proj_body = - it_mkLambda_or_LetIn (mkLambda (Name binder_name, inst_type, mkRel 1)) params in - let proj_entry = Declare.definition_entry ~types:proj_type ~poly ~univs:ctx proj_body in - let proj_cst = Declare.declare_constant proj_name - (DefinitionEntry proj_entry, IsDefinition Definition) - in - let cref = ConstRef cst in - Impargs.declare_manual_implicits false cref [paramimpls]; - Impargs.declare_manual_implicits false (ConstRef proj_cst) [List.hd fieldimpls]; - Classes.set_typeclass_transparency (EvalConstRef cst) false false; - let sub = match List.hd coers with - | Some b -> Some ((if b then Backward else Forward), List.hd priorities) - | None -> None - in - cref, [Name proj_name, sub, Some proj_cst] + let class_body = it_mkLambda_or_LetIn field params in + let _class_type = it_mkProd_or_LetIn arity params in + let class_entry = + Declare.definition_entry (* ?types:class_type *) ~poly ~univs:ctx class_body in + let cst = Declare.declare_constant (snd id) + (DefinitionEntry class_entry, IsDefinition Definition) + in + let cstu = (cst, if poly then Univ.UContext.instance ctx else Univ.Instance.empty) in + let inst_type = appvectc (mkConstU cstu) + (Termops.rel_vect 0 (List.length params)) in + let proj_type = + it_mkProd_or_LetIn (mkProd(Name binder_name, inst_type, lift 1 field)) params in + let proj_body = + it_mkLambda_or_LetIn (mkLambda (Name binder_name, inst_type, mkRel 1)) params in + let proj_entry = + Declare.definition_entry ~types:proj_type ~poly + ~univs:(if poly then ctx else Univ.UContext.empty) proj_body + in + let proj_cst = Declare.declare_constant proj_name + (DefinitionEntry proj_entry, IsDefinition Definition) + in + let cref = ConstRef cst in + Impargs.declare_manual_implicits false cref [paramimpls]; + Impargs.declare_manual_implicits false (ConstRef proj_cst) [List.hd fieldimpls]; + Classes.set_typeclass_transparency (EvalConstRef cst) false false; + let sub = match List.hd coers with + | Some b -> Some ((if b then Backward else Forward), List.hd priorities) + | None -> None + in + cref, [Name proj_name, sub, Some proj_cst] | _ -> - let ind = declare_structure BiFinite poly ctx (snd id) idbuild paramimpls + let ind = declare_structure BiFinite poly ctx (snd id) idbuild paramimpls params arity template fieldimpls fields ~kind:Method ~name:binder_name false (List.map (fun _ -> false) fields) sign - in - let coers = List.map2 (fun coe pri -> - Option.map (fun b -> - if b then Backward, pri else Forward, pri) coe) + in + let coers = List.map2 (fun coe pri -> + Option.map (fun b -> + if b then Backward, pri else Forward, pri) coe) coers priorities - in - IndRef ind, (List.map3 (fun (id, _, _) b y -> (id, b, y)) - (List.rev fields) coers (Recordops.lookup_projections ind)) + in + let l = List.map3 (fun (id, _, _) b y -> (id, b, y)) + (List.rev fields) coers (Recordops.lookup_projections ind) + in IndRef ind, l in let ctx_context = List.map (fun (na, b, t) -> @@ -502,7 +517,7 @@ open Vernacexpr (* [fs] corresponds to fields and [ps] to parameters; [coers] is a list telling if the corresponding fields must me declared as coercions or subinstances *) -let definition_structure (kind,poly,finite,(is_coe,(loc,idstruc)),ps,cfs,idbuild,s) = +let definition_structure (kind,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cfs,idbuild,s) = let cfs,notations = List.split cfs in let cfs,priorities = List.split cfs in let coers,fs = List.split cfs in @@ -517,11 +532,11 @@ let definition_structure (kind,poly,finite,(is_coe,(loc,idstruc)),ps,cfs,idbuild if isnot_class && List.exists (fun opt -> not (Option.is_empty opt)) priorities then error "Priorities only allowed for type class substructures"; (* Now, younger decl in params and fields is on top *) - let ctx, arity, template, implpars, params, implfs, fields = + let (pl, ctx), arity, template, implpars, params, implfs, fields = States.with_state_protection (fun () -> - typecheck_params_and_fields (kind = Class true) idstruc s ps notations fs) () in + typecheck_params_and_fields (kind = Class true) idstruc pl s ps notations fs) () in let sign = structure_signature (fields@params) in - match kind with + let gr = match kind with | Class def -> let gr = declare_class finite def poly ctx (loc,idstruc) idbuild implpars params arity template implfs fields is_coe coers priorities sign in @@ -534,3 +549,6 @@ let definition_structure (kind,poly,finite,(is_coe,(loc,idstruc)),ps,cfs,idbuild idbuild implpars params arity template implfs fields is_coe (List.map (fun coe -> not (Option.is_empty coe)) coers) sign in IndRef ind + in + Universes.register_universe_binders gr pl; + gr |