From b341b58104ff14f10a5e170d4bfbc7a02f12755f Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 15 Mar 2020 02:43:42 -0400 Subject: [record] Cleanup of data structure and functions [1/2] In preparation for reworking the record declaration path to use the common infrastructure, we perform some refactoring. The current choices are far from definitive, as we will consolidate the data types more as we move along with the work here. --- vernac/record.ml | 390 ++++++++++++++++++++++++++++-------------------- vernac/record.mli | 30 ++-- vernac/vernacentries.ml | 10 +- 3 files changed, 243 insertions(+), 187 deletions(-) diff --git a/vernac/record.ml b/vernac/record.ml index 2c56604d8f..ebd83bb6d2 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -11,24 +11,17 @@ open Pp open CErrors open Term -open Sorts open Util open Names -open Nameops open Constr open Context -open Vars open Environ open Declarations open Entries -open Declare -open Constrintern open Type_errors open Constrexpr open Constrexpr_ops -open Goptions open Context.Rel.Declaration -open Libobject module RelDecl = Context.Rel.Declaration @@ -37,6 +30,7 @@ module RelDecl = Context.Rel.Declaration (** Flag governing use of primitive projections. Disabled by default. *) let primitive_flag = ref false let () = + let open Goptions in declare_bool_option { optdepr = false; optkey = ["Primitive";"Projections"]; @@ -45,6 +39,7 @@ let () = let typeclasses_strict = ref false let () = + let open Goptions in declare_bool_option { optdepr = false; optkey = ["Typeclasses";"Strict";"Resolution"]; @@ -53,6 +48,7 @@ let () = let typeclasses_unique = ref false let () = + let open Goptions in declare_bool_option { optdepr = false; optkey = ["Typeclasses";"Unique";"Instances"]; @@ -81,7 +77,8 @@ let interp_fields_evars env sigma ~ninds ~nparams impls_env nots l = let impls_env = match i with | Anonymous -> impls_env - | Name id -> Id.Map.add id (compute_internalization_data env sigma id Constrintern.Method t impl) impls_env + | Name id -> + Id.Map.add id (Constrintern.compute_internalization_data env sigma id Constrintern.Method t impl) impls_env in let d = match b with | None -> LocalAssum (make_annot i r,t) @@ -106,7 +103,7 @@ let compute_constructor_level evars env l = let univ = if is_local_assum d then let s = Retyping.get_sort_of env evars (RelDecl.get_type d) in - Univ.sup (univ_of_sort s) univ + Univ.sup (Sorts.univ_of_sort s) univ else univ in (EConstr.push_rel d env, univ)) l (env, Univ.Universe.sprop) @@ -116,68 +113,83 @@ let check_anonymous_type ind = | { CAst.v = CSort (Glob_term.UAnonymous {rigid=true}) } -> true | _ -> false -let typecheck_params_and_fields def poly pl ps records = +let error_parameters_must_be_named bk {CAst.loc; v=name} = + match bk, name with + | Default _, Anonymous -> + CErrors.user_err ?loc ~hdr:"record" (str "Record parameters must be named") + | _ -> () + +let check_parameters_must_be_named = function + | CLocalDef (b, _, _) -> + error_parameters_must_be_named default_binder_kind b + | CLocalAssum (ls, bk, ce) -> + List.iter (error_parameters_must_be_named bk) ls + | CLocalPattern {CAst.loc} -> + Loc.raise ?loc (Stream.Error "pattern with quote not allowed in record parameters") + +module DataI = struct + type t = + { name : Id.t + ; arity : Constrexpr.constr_expr option + ; nots : Vernacexpr.decl_notation list list + ; fs : Vernacexpr.local_decl_expr list + } +end + +let build_type_telescope newps env0 (sigma, template) { DataI.arity; _ } = match arity with + | None -> + let uvarkind = Evd.univ_flexible_alg in + let sigma, s = Evd.new_sort_variable uvarkind sigma in + (sigma, template), (EConstr.mkSort s, s) + | Some t -> + let env = EConstr.push_rel_context newps env0 in + let poly = + match t with + | { CAst.v = CSort (Glob_term.UAnonymous {rigid=true}) } -> true | _ -> false in + let impls = Constrintern.empty_internalization_env in + let sigma, s = Constrintern.interp_type_evars ~program_mode:false env sigma ~impls t in + let sred = Reductionops.whd_allnolet env sigma s in + (match EConstr.kind sigma sred with + | Sort s' -> + let s' = EConstr.ESorts.kind sigma s' in + (if poly then + match Evd.is_sort_variable sigma s' with + | Some l -> + let sigma = Evd.make_flexible_variable sigma ~algebraic:true l in + (sigma, template), (s, s') + | None -> + (sigma, false), (s, s') + else (sigma, false), (s, s')) + | _ -> user_err ?loc:(constr_loc t) (str"Sort expected.")) + +(* ps = parameter list *) +let typecheck_params_and_fields def poly pl ps (records : DataI.t list) = let env0 = Global.env () in (* Special case elaboration for template-polymorphic inductives, lower bound on introduced universes is Prop so that we do not miss any Set <= i constraint for universes that might actually be instantiated with Prop. *) let is_template = - List.exists (fun (_, arity, _, _) -> Option.cata check_anonymous_type true arity) records in + List.exists (fun { DataI.arity; _} -> Option.cata check_anonymous_type true arity) records in let env0 = if not poly && is_template then Environ.set_universes_lbound env0 UGraph.Bound.Prop else env0 in - let sigma, decl = interp_univ_decl_opt env0 pl in - let () = - let error bk {CAst.loc; v=name} = - match bk, name with - | Default _, Anonymous -> - user_err ?loc ~hdr:"record" (str "Record parameters must be named") - | _ -> () - in - List.iter - (function CLocalDef (b, _, _) -> error default_binder_kind b - | CLocalAssum (ls, bk, ce) -> List.iter (error bk) ls - | CLocalPattern {CAst.loc} -> - Loc.raise ?loc (Stream.Error "pattern with quote not allowed in record parameters")) ps - in - let sigma, (impls_env, ((env1,newps), imps)) = interp_context_evars ~program_mode:false env0 sigma ps in - let fold (sigma, template) (_, t, _, _) = match t with - | Some t -> - let env = EConstr.push_rel_context newps env0 in - let poly = - match t with - | { CAst.v = CSort (Glob_term.UAnonymous {rigid=true}) } -> true | _ -> false in - let sigma, s = interp_type_evars ~program_mode:false env sigma ~impls:empty_internalization_env t in - let sred = Reductionops.whd_allnolet env sigma s in - (match EConstr.kind sigma sred with - | Sort s' -> - let s' = EConstr.ESorts.kind sigma s' in - (if poly then - match Evd.is_sort_variable sigma s' with - | Some l -> - let sigma = Evd.make_flexible_variable sigma ~algebraic:true l in - (sigma, template), (s, s') - | None -> - (sigma, false), (s, s') - else (sigma, false), (s, s')) - | _ -> user_err ?loc:(constr_loc t) (str"Sort expected.")) - | None -> - let uvarkind = Evd.univ_flexible_alg in - let sigma, s = Evd.new_sort_variable uvarkind sigma in - (sigma, template), (EConstr.mkSort s, s) - in - let (sigma, template), typs = List.fold_left_map fold (sigma, true) records in + let sigma, decl = Constrintern.interp_univ_decl_opt env0 pl in + let () = List.iter check_parameters_must_be_named ps in + let sigma, (impls_env, ((env1,newps), imps)) = + Constrintern.interp_context_evars ~program_mode:false env0 sigma ps in + let (sigma, template), typs = + List.fold_left_map (build_type_telescope newps env0) (sigma, true) records in let arities = List.map (fun (typ, _) -> EConstr.it_mkProd_or_LetIn typ newps) typs in let relevances = List.map (fun (_,s) -> Sorts.relevance_of_sort s) typs in - let fold accu (id, _, _, _) arity r = - EConstr.push_rel (LocalAssum (make_annot (Name id) r,arity)) accu in + let fold accu { DataI.name; _ } arity r = + EConstr.push_rel (LocalAssum (make_annot (Name name) r,arity)) accu in let env_ar = EConstr.push_rel_context newps (List.fold_left3 fold env0 records arities relevances) in let impls_env = - let ids = List.map (fun (id, _, _, _) -> id) records in + let ids = List.map (fun { DataI.name; _ } -> name) records in let imps = List.map (fun _ -> imps) arities in - compute_internalization_env env0 sigma ~impls:impls_env Inductive ids arities imps + Constrintern.compute_internalization_env env0 sigma ~impls:impls_env Constrintern.Inductive ids arities imps in let ninds = List.length arities in let nparams = List.length newps in - let fold sigma (_, _, nots, fs) arity = + let fold sigma { DataI.nots; fs; _ } arity = interp_fields_evars env_ar sigma ~ninds ~nparams impls_env nots fs in let (sigma, data) = List.fold_left2_map fold sigma records arities in @@ -299,20 +311,92 @@ type projection_flags = { } (* We build projections *) -let declare_projections indsp ctx ?(kind=Decls.StructureComponent) binder_name flags fieldimpls fields = + +(* TODO: refactor the declaration part here; this requires some + surgery as Evarutil.finalize is called too early in the path *) +let build_proj env mib indsp primitive x rp lifted_fields ~poly paramdecls paramargs ~uinstance ~kind ~univs + (nfi,i,kinds,sp_projs,subst) flags decl impls = + let fi = RelDecl.get_name decl in + let ti = RelDecl.get_type decl in + let (sp_projs,i,subst) = + match fi with + | Anonymous -> + (None::sp_projs,i,NoProjection fi::subst) + | Name fid -> + try + let ccl = subst_projection fid subst ti in + let body, p_opt = match decl with + | LocalDef (_,ci,_) -> subst_projection fid subst ci, None + | LocalAssum ({binder_relevance=rci},_) -> + (* [ccl] is defined in context [params;x:rp] *) + (* [ccl'] is defined in context [params;x:rp;x:rp] *) + if primitive then + let p = Projection.Repr.make indsp + ~proj_npars:mib.mind_nparams ~proj_arg:i (Label.of_id fid) in + mkProj (Projection.make p true, mkRel 1), Some p + else + let ccl' = liftn 1 2 ccl in + let p = mkLambda (x, lift 1 rp, ccl') in + let branch = it_mkLambda_or_LetIn (mkRel nfi) lifted_fields in + let ci = Inductiveops.make_case_info env indsp rci LetStyle in + (* Record projections are always NoInvert because + they're at constant relevance *) + mkCase (ci, p, NoInvert, mkRel 1, [|branch|]), None + in + let proj = it_mkLambda_or_LetIn (mkLambda (x,rp,body)) paramdecls in + let projtyp = it_mkProd_or_LetIn (mkProd (x,rp,ccl)) paramdecls in + let entry = Declare.definition_entry ~univs ~types:projtyp proj in + let kind = Decls.IsDefinition kind in + let kn = + try Declare.declare_constant ~name:fid ~kind (Declare.DefinitionEntry entry) + with Type_errors.TypeError (ctx,te) as exn when not primitive -> + let _, info = Exninfo.capture exn in + Exninfo.iraise (NotDefinable (BadTypedProj (fid,ctx,te)),info) + in + Declare.definition_message fid; + let term = match p_opt with + | Some p -> + let _ = DeclareInd.declare_primitive_projection p kn in + mkProj (Projection.make p false,mkRel 1) + | None -> + let proj_args = (*Rel 1 refers to "x"*) paramargs@[mkRel 1] in + match decl with + | LocalDef (_,ci,_) when primitive -> body + | _ -> applist (mkConstU (kn,uinstance),proj_args) + in + let refi = GlobRef.ConstRef kn in + Impargs.maybe_declare_manual_implicits false refi impls; + if flags.pf_subclass then begin + let cl = ComCoercion.class_of_global (GlobRef.IndRef indsp) in + ComCoercion.try_add_new_coercion_with_source refi ~local:false ~poly ~source:cl + end; + let i = if is_local_assum decl then i+1 else i in + (Some kn::sp_projs, i, Projection term::subst) + with NotDefinable why as exn -> + let _, info = Exninfo.capture exn in + warning_or_error ~info flags.pf_subclass indsp why; + (None::sp_projs,i,NoProjection fi::subst) + in + (nfi - 1, i, + { Recordops.pk_name = fi + ; pk_true_proj = is_local_assum decl + ; pk_canonical = flags.pf_canonical } :: kinds + , sp_projs, subst) + +let declare_projections indsp univs ?(kind=Decls.StructureComponent) binder_name flags fieldimpls fields = let env = Global.env() in let (mib,mip) = Global.lookup_inductive indsp in let poly = Declareops.inductive_is_polymorphic mib in - let u = match ctx with + let uinstance = match univs with | Polymorphic_entry (_, ctx) -> Univ.UContext.instance ctx | Monomorphic_entry ctx -> Univ.Instance.empty in - let paramdecls = Inductive.inductive_paramdecls (mib, u) in - let r = mkIndU (indsp,u) in + let paramdecls = Inductive.inductive_paramdecls (mib, uinstance) in + let r = mkIndU (indsp,uinstance) in let rp = applist (r, Context.Rel.to_extended_list mkRel 0 paramdecls) in let paramargs = Context.Rel.to_extended_list mkRel 1 paramdecls in (*def in [[params;x:rp]]*) let x = make_annot (Name binder_name) mip.mind_relevance in - let fields = instantiate_possibly_recursive_type (fst indsp) u mib.mind_ntypes paramdecls fields in + let fields = instantiate_possibly_recursive_type (fst indsp) uinstance mib.mind_ntypes paramdecls fields in let lifted_fields = Termops.lift_rel_context 1 fields in let primitive = match mib.mind_record with @@ -321,69 +405,7 @@ let declare_projections indsp ctx ?(kind=Decls.StructureComponent) binder_name f in let (_,_,kinds,sp_projs,_) = List.fold_left3 - (fun (nfi,i,kinds,sp_projs,subst) flags decl impls -> - let fi = RelDecl.get_name decl in - let ti = RelDecl.get_type decl in - let (sp_projs,i,subst) = - match fi with - | Anonymous -> - (None::sp_projs,i,NoProjection fi::subst) - | Name fid -> - try - let ccl = subst_projection fid subst ti in - let body, p_opt = match decl with - | LocalDef (_,ci,_) -> subst_projection fid subst ci, None - | LocalAssum ({binder_relevance=rci},_) -> - (* [ccl] is defined in context [params;x:rp] *) - (* [ccl'] is defined in context [params;x:rp;x:rp] *) - if primitive then - let p = Projection.Repr.make indsp - ~proj_npars:mib.mind_nparams ~proj_arg:i (Label.of_id fid) in - mkProj (Projection.make p true, mkRel 1), Some p - else - let ccl' = liftn 1 2 ccl in - let p = mkLambda (x, lift 1 rp, ccl') in - let branch = it_mkLambda_or_LetIn (mkRel nfi) lifted_fields in - let ci = Inductiveops.make_case_info env indsp rci LetStyle in - (* Record projections are always NoInvert because - they're at constant relevance *) - mkCase (ci, p, NoInvert, mkRel 1, [|branch|]), None - in - let proj = it_mkLambda_or_LetIn (mkLambda (x,rp,body)) paramdecls in - let projtyp = it_mkProd_or_LetIn (mkProd (x,rp,ccl)) paramdecls in - let entry = Declare.definition_entry ~univs:ctx ~types:projtyp proj in - let kind = Decls.IsDefinition kind in - let kn = - try declare_constant ~name:fid ~kind (Declare.DefinitionEntry entry) - with Type_errors.TypeError (ctx,te) as exn when not primitive -> - let _, info = Exninfo.capture exn in - Exninfo.iraise (NotDefinable (BadTypedProj (fid,ctx,te)),info) - in - Declare.definition_message fid; - let term = match p_opt with - | Some p -> - let _ = DeclareInd.declare_primitive_projection p kn in - mkProj (Projection.make p false,mkRel 1) - | None -> - let proj_args = (*Rel 1 refers to "x"*) paramargs@[mkRel 1] in - match decl with - | LocalDef (_,ci,_) when primitive -> body - | _ -> applist (mkConstU (kn,u),proj_args) - in - let refi = GlobRef.ConstRef kn in - Impargs.maybe_declare_manual_implicits false refi impls; - if flags.pf_subclass then begin - let cl = ComCoercion.class_of_global (GlobRef.IndRef indsp) in - ComCoercion.try_add_new_coercion_with_source refi ~local:false ~poly ~source:cl - end; - let i = if is_local_assum decl then i+1 else i in - (Some kn::sp_projs, i, Projection term::subst) - with NotDefinable why as exn -> - let _, info = Exninfo.capture exn in - warning_or_error ~info flags.pf_subclass indsp why; - (None::sp_projs,i,NoProjection fi::subst) - in - (nfi - 1, i, { Recordops.pk_name = fi ; pk_true_proj = is_local_assum decl ; pk_canonical = flags.pf_canonical } :: kinds, sp_projs, subst)) + (build_proj env mib indsp primitive x rp lifted_fields ~poly paramdecls paramargs ~uinstance ~kind ~univs) (List.length fields,0,[],[],[]) flags (List.rev fields) (List.rev fieldimpls) in (kinds,sp_projs) @@ -402,7 +424,8 @@ let discharge_structure (_, x) = Some x let rebuild_structure s = Recordops.rebuild_structure (Global.env()) s -let inStruc : Recordops.struc_typ -> obj = +let inStruc : Recordops.struc_typ -> Libobject.obj = + let open Libobject in declare_object {(default_object "STRUCTURE") with cache_function = cache_structure; load_function = load_structure; @@ -414,7 +437,20 @@ let inStruc : Recordops.struc_typ -> obj = let declare_structure_entry o = Lib.add_anonymous_leaf (inStruc o) -let declare_structure ~cumulative finite ubinders univs paramimpls params template ?(kind=Decls.StructureComponent) ?name record_data = +module Data = struct + type t = + { id : Id.t + ; idbuild : Id.t + ; min_univ : Univ.Universe.t + ; arity : Constr.t + ; fieldimpls : Impargs.manual_implicits list + ; fields : Constr.rel_context + ; is_coercion : bool + ; coers : projection_flags list + } +end + +let declare_structure ~cumulative finite ubinders ~univs paramimpls params template ?(kind=Decls.StructureComponent) ?name (record_data : Data.t list) = let nparams = List.length params in let poly, ctx = match univs with @@ -426,14 +462,14 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa let binder_name = match name with | None -> - let map (id, _, _, _, _, _, _, _) = + let map { Data.id; _ } = Id.of_string (Unicode.lowercase_first_char (Id.to_string id)) in Array.map_of_list map record_data | Some n -> n in let ntypes = List.length record_data in - let mk_block i (id, idbuild, min_univ, arity, _, fields, _, _) = + let mk_block i { Data.id; idbuild; min_univ; arity; fields; _ } = let nfields = List.length fields in let args = Context.Rel.to_extended_list mkRel nfields params in let ind = applist (mkRel (ntypes - i + nparams + nfields), args) in @@ -444,7 +480,7 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa mind_entry_lc = [type_constructor] } in let blocks = List.mapi mk_block record_data in - let check_template (id, _, min_univ, _, _, fields, _, _) = + let check_template { Data.id; min_univ; fields; _ } = let template_candidate () = (* we use some dummy values for the arities in the rel_context as univs_of_constr doesn't care about localassums and @@ -479,7 +515,7 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa let template = List.for_all check_template record_data in let primitive = !primitive_flag && - List.for_all (fun (_,_,_,_,_,fields,_,_) -> List.exists is_local_assum fields) record_data + List.for_all (fun { Data.fields; _ } -> List.exists is_local_assum fields) record_data in let mie = { mind_entry_params = params; @@ -496,12 +532,12 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa let kn = DeclareInd.declare_mutual_inductive_with_eliminations mie ubinders impls ~primitive_expected:!primitive_flag in - let map i (_, _, _, _, fieldimpls, fields, is_coe, coers) = + let map i { Data.fieldimpls; fields; is_coercion; coers } = let rsp = (kn, i) in (* This is ind path of idstruc *) let cstr = (rsp, 1) in let kinds,sp_projs = declare_projections rsp ctx ~kind binder_name.(i) coers fieldimpls fields in let build = GlobRef.ConstructRef cstr in - let () = if is_coe then ComCoercion.try_add_new_coercion build ~local:false ~poly in + let () = if is_coercion then ComCoercion.try_add_new_coercion build ~local:false ~poly in let npars = Inductiveops.inductive_nparams (Global.env()) rsp in let struc = { Recordops.s_CONST = cstr; @@ -519,7 +555,7 @@ let implicits_of_context ctx = List.map (fun name -> CAst.make (Some (name,true))) (List.rev (Anonymous :: (List.map RelDecl.get_name ctx))) -let declare_class def cumulative ubinders univs id idbuild paramimpls params univ arity +let declare_class def cumulative ubinders univs id idbuild paramimpls params min_univ arity template fieldimpls fields ?(kind=Decls.StructureComponent) coers = let fieldimpls = (* Make the class implicit in the projections, and the params if applicable. *) @@ -529,15 +565,15 @@ let declare_class def cumulative ubinders univs id idbuild paramimpls params uni let binder_name = Namegen.next_ident_away id (Termops.vars_of_env (Global.env())) in let data = match fields with - | [LocalAssum ({binder_name=Name proj_name} as binder, field) - | LocalDef ({binder_name=Name proj_name} as binder, _, field)] when def -> + | [ LocalAssum ({binder_name=Name proj_name} as binder, field) + | LocalDef ({binder_name=Name proj_name} as binder, _, field) ] when def -> let binder = {binder with binder_name=Name binder_name} in 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 ~univs class_body in let cst = Declare.declare_constant ~name:id - (DefinitionEntry class_entry) ~kind:Decls.(IsDefinition Definition) + (Declare.DefinitionEntry class_entry) ~kind:Decls.(IsDefinition Definition) in let inst, univs = match univs with | Polymorphic_entry (_, uctx) -> Univ.UContext.instance uctx, univs @@ -552,7 +588,7 @@ let declare_class def cumulative ubinders univs id idbuild paramimpls params uni it_mkLambda_or_LetIn (mkLambda (binder, inst_type, mkRel 1)) params in let proj_entry = Declare.definition_entry ~types:proj_type ~univs proj_body in let proj_cst = Declare.declare_constant ~name:proj_name - (DefinitionEntry proj_entry) ~kind:Decls.(IsDefinition Definition) + (Declare.DefinitionEntry proj_entry) ~kind:Decls.(IsDefinition Definition) in let cref = GlobRef.ConstRef cst in Impargs.declare_manual_implicits false cref paramimpls; @@ -566,10 +602,18 @@ let declare_class def cumulative ubinders univs id idbuild paramimpls params uni } in [cref, [m]] | _ -> - let record_data = [id, idbuild, univ, arity, fieldimpls, fields, false, - List.map (fun _ -> { pf_subclass = false ; pf_canonical = true }) fields] in - let inds = declare_structure ~cumulative Declarations.BiFinite ubinders univs paramimpls - params template ~kind:Decls.Method ~name:[|binder_name|] record_data + let record_data = + { Data.id + ; idbuild + ; min_univ + ; arity + ; fieldimpls + ; fields + ; is_coercion = false + ; coers = List.map (fun _ -> { pf_subclass = false ; pf_canonical = true }) fields + } in + let inds = declare_structure ~cumulative Declarations.BiFinite ubinders ~univs paramimpls + params template ~kind:Decls.Method ~name:[|binder_name|] [record_data] in let map ind = let map decl b y = { @@ -667,14 +711,34 @@ let declare_existing_class g = open Vernacexpr +module Ast = struct + type t = + { name : Names.lident + ; is_coercion : coercion_flag + ; binders: local_binder_expr list + ; cfs : (local_decl_expr * record_field_attr) list + ; idbuild : Id.t + ; sort : constr_expr option + } + + let to_idata { name; is_coercion; cfs; idbuild; sort } = + let fs = List.map fst cfs in + { DataI.name = name.CAst.v + ; arity = sort + ; nots = List.map (fun (_, { rf_notation }) -> rf_notation) cfs + ; fs + } + +end + let check_unique_names records = let extract_name acc (rf_decl, _) = match rf_decl with Vernacexpr.AssumExpr({CAst.v=Name id},_,_) -> id::acc | Vernacexpr.DefExpr ({CAst.v=Name id},_,_,_) -> id::acc | _ -> acc in let allnames = - List.fold_left (fun acc (_, id, _, cfs, _, _) -> - id.CAst.v :: (List.fold_left extract_name acc cfs)) [] records + List.fold_left (fun acc { Ast.name; cfs; _ } -> + name.CAst.v :: (List.fold_left extract_name acc cfs)) [] records in match List.duplicates Id.equal allnames with | [] -> () @@ -682,19 +746,15 @@ let check_unique_names records = let check_priorities kind records = let isnot_class = match kind with Class false -> false | _ -> true in - let has_priority (_, _, _, cfs, _, _) = + let has_priority { Ast.cfs; _ } = List.exists (fun (_, { rf_priority }) -> not (Option.is_empty rf_priority)) cfs in if isnot_class && List.exists has_priority records then user_err Pp.(str "Priorities only allowed for type class substructures") let extract_record_data records = - let map (is_coe, id, _, cfs, idbuild, s) = - let fs = List.map fst cfs in - id.CAst.v, s, List.map (fun (_, { rf_notation }) -> rf_notation) cfs, fs - in - let data = List.map map records in - let pss = List.map (fun (_, _, ps, _, _, _) -> ps) records in + let data = List.map Ast.to_idata records in + let pss = List.map (fun { Ast.binders; _ } -> binders) records in let ps = match pss with | [] -> CErrors.anomaly (str "Empty record block") | ps :: rem -> @@ -711,40 +771,44 @@ let extract_record_data records = (* [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 udecl kind ~template ~cumulative ~poly finite records = +let definition_structure udecl kind ~template ~cumulative ~poly finite (records : Ast.t list) = let () = check_unique_names records in let () = check_priorities kind records in let ps, data = extract_record_data records in let ubinders, univs, auto_template, params, implpars, data = + (* In theory we should be able to use + [Notation.with_notation_protection], due to the call to + Metasyntax.set_notation_for_interpretation, however something + is messing state beyond that. + *) Vernacstate.System.protect (fun () -> typecheck_params_and_fields (kind = Class true) poly udecl ps data) () in let template = template, auto_template in match kind with | Class def -> - let (_, id, _, cfs, idbuild, _), (univ, arity, implfs, fields) = match records, data with + let { Ast.name; cfs; idbuild; _ }, (univ, arity, implfs, fields) = match records, data with | [r], [d] -> r, d | _, _ -> CErrors.user_err (str "Mutual definitional classes are not handled") in - let coers = List.map (fun (_, { rf_subclass=coe; rf_priority=pri }) -> - match coe with - | Vernacexpr.BackInstance -> Some {hint_priority = pri ; hint_pattern = None} + let coers = List.map (fun (_, { rf_subclass; rf_priority }) -> + match rf_subclass with + | Vernacexpr.BackInstance -> Some {hint_priority = rf_priority; hint_pattern = None} | Vernacexpr.NoInstance -> None) - cfs - in - declare_class def cumulative ubinders univs id.CAst.v idbuild + cfs in + declare_class def cumulative ubinders univs name.CAst.v idbuild implpars params univ arity template implfs fields coers | _ -> let map impls = implpars @ [CAst.make None] @ impls in let data = List.map (fun (univ, arity, implfs, fields) -> (univ, arity, List.map map implfs, fields)) data in - let map (univ, arity, implfs, fields) (is_coe, id, _, cfs, idbuild, _) = - let coe = List.map (fun (_, { rf_subclass ; rf_canonical }) -> + let map (min_univ, arity, fieldimpls, fields) { Ast.name; is_coercion; cfs; idbuild; _ } = + let coers = List.map (fun (_, { rf_subclass ; rf_canonical }) -> { pf_subclass = (match rf_subclass with Vernacexpr.BackInstance -> true | Vernacexpr.NoInstance -> false); pf_canonical = rf_canonical }) cfs in - id.CAst.v, idbuild, univ, arity, implfs, fields, is_coe, coe + { Data.id = name.CAst.v; idbuild; min_univ; arity; fieldimpls; fields; is_coercion; coers } in let data = List.map2 map data records in - let inds = declare_structure ~cumulative finite ubinders univs implpars params template data in + let inds = declare_structure ~cumulative finite ubinders ~univs implpars params template data in List.map (fun ind -> GlobRef.IndRef ind) inds diff --git a/vernac/record.mli b/vernac/record.mli index 38a622977a..c3b84540f0 100644 --- a/vernac/record.mli +++ b/vernac/record.mli @@ -14,20 +14,16 @@ open Constrexpr val primitive_flag : bool ref -type projection_flags = { - pf_subclass: bool; - pf_canonical: bool; -} - -val declare_projections : - inductive -> - Entries.universes_entry -> - ?kind:Decls.definition_object_kind -> - Id.t -> - projection_flags list -> - Impargs.manual_implicits list -> - Constr.rel_context -> - Recordops.proj_kind list * Constant.t option list +module Ast : sig + type t = + { name : Names.lident + ; is_coercion : coercion_flag + ; binders: local_binder_expr list + ; cfs : (local_decl_expr * record_field_attr) list + ; idbuild : Id.t + ; sort : constr_expr option + } +end val definition_structure : universe_decl_expr option @@ -36,11 +32,7 @@ val definition_structure -> cumulative:bool -> poly:bool -> Declarations.recursivity_kind - -> (coercion_flag * - Names.lident * - local_binder_expr list * - (local_decl_expr * record_field_attr) list * - Id.t * constr_expr option) list + -> Ast.t list -> GlobRef.t list val declare_existing_class : GlobRef.t -> unit diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 824bf35b1d..6a09250627 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -715,16 +715,16 @@ let should_treat_as_uniform () = else ComInductive.NonUniformParameters let vernac_record ~template udecl ~cumulative k ~poly finite records = - let map ((coe, id), binders, sort, nameopt, cfs) = - let const = match nameopt with - | None -> Nameops.add_prefix "Build_" id.v + let map ((is_coercion, name), binders, sort, nameopt, cfs) = + let idbuild = match nameopt with + | None -> Nameops.add_prefix "Build_" name.v | Some lid -> let () = Dumpglob.dump_definition lid false "constr" in lid.v in let () = if Dumpglob.dump () then - let () = Dumpglob.dump_definition id false "rec" in + let () = Dumpglob.dump_definition name false "rec" in let iter (x, _) = match x with | Vernacexpr.(AssumExpr ({loc;v=Name id}, _, _) | DefExpr ({loc;v=Name id}, _, _, _)) -> Dumpglob.dump_definition (make ?loc id) false "proj" @@ -732,7 +732,7 @@ let vernac_record ~template udecl ~cumulative k ~poly finite records = in List.iter iter cfs in - coe, id, binders, cfs, const, sort + Record.Ast.{ name; is_coercion; binders; cfs; idbuild; sort } in let records = List.map map records in ignore(Record.definition_structure ~template udecl k ~cumulative ~poly finite records) -- cgit v1.2.3 From e47d39403f9830d7a84c32bdc3e9cf360427b7e8 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 15 Mar 2020 00:13:55 -0400 Subject: [record] Cleanup of data structure and functions [2/2] In preparation for reworking the record declaration path to use the common infrastructure, we perform some refactoring. The current choices are far from definitive, as we will consolidate the data types more as we move along with the work here. --- vernac/record.ml | 116 +++++++++++++++++++++++++++++++------------------------ 1 file changed, 66 insertions(+), 50 deletions(-) diff --git a/vernac/record.ml b/vernac/record.ml index ebd83bb6d2..b0b6194d7f 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -136,6 +136,30 @@ module DataI = struct } end +type projection_flags = { + pf_subclass: bool; + pf_canonical: bool; +} + +module DataR = struct + type t = + { min_univ : Univ.Universe.t + ; arity : Constr.t + ; implfs : Impargs.manual_implicits list + ; fields : Constr.rel_declaration list + } +end + +module Data = struct + type t = + { id : Id.t + ; idbuild : Id.t + ; is_coercion : bool + ; coers : projection_flags list + ; rdata : DataR.t + } +end + let build_type_telescope newps env0 (sigma, template) { DataI.arity; _ } = match arity with | None -> let uvarkind = Evd.univ_flexible_alg in @@ -162,8 +186,17 @@ let build_type_telescope newps env0 (sigma, template) { DataI.arity; _ } = match else (sigma, false), (s, s')) | _ -> user_err ?loc:(constr_loc t) (str"Sort expected.")) +type tc_result = + bool + * Impargs.manual_implicits + (* Part relative to closing the definitions *) + * UnivNames.universe_binders + * Entries.universes_entry + * Constr.rel_context + * DataR.t list + (* ps = parameter list *) -let typecheck_params_and_fields def poly pl ps (records : DataI.t list) = +let typecheck_params_and_fields def poly pl ps (records : DataI.t list) : tc_result = let env0 = Global.env () in (* Special case elaboration for template-polymorphic inductives, lower bound on introduced universes is Prop so that we do not miss @@ -210,12 +243,13 @@ let typecheck_params_and_fields def poly pl ps (records : DataI.t list) = else sigma, (univ, typ) in let (sigma, typs) = List.fold_left2_map fold sigma typs data in + (* TODO: Have this use Declaredef.prepare_definition *) let sigma, (newps, ans) = Evarutil.finalize sigma (fun nf -> let newps = List.map (RelDecl.map_constr_het nf) newps in - let map (impls, newfs) (univ, typ) = - let newfs = List.map (RelDecl.map_constr_het nf) newfs in - let typ = nf typ in - (univ, typ, impls, newfs) + let map (implfs, fields) (min_univ, typ) = + let fields = List.map (RelDecl.map_constr_het nf) fields in + let arity = nf typ in + { DataR.min_univ; arity; implfs; fields } in let ans = List.map2 map data typs in newps, ans) @@ -224,7 +258,7 @@ let typecheck_params_and_fields def poly pl ps (records : DataI.t list) = let ubinders = Evd.universe_binders sigma 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 + template, imps, ubinders, univs, newps, ans type record_error = | MissingProj of Id.t * Id.t list @@ -305,11 +339,6 @@ let instantiate_possibly_recursive_type ind u ntypes paramdecls fields = let subst' = List.init ntypes (fun i -> mkIndU ((ind, ntypes - i - 1), u)) in Termops.substl_rel_context (subst @ subst') fields -type projection_flags = { - pf_subclass: bool; - pf_canonical: bool; -} - (* We build projections *) (* TODO: refactor the declaration part here; this requires some @@ -437,19 +466,6 @@ let inStruc : Recordops.struc_typ -> Libobject.obj = let declare_structure_entry o = Lib.add_anonymous_leaf (inStruc o) -module Data = struct - type t = - { id : Id.t - ; idbuild : Id.t - ; min_univ : Univ.Universe.t - ; arity : Constr.t - ; fieldimpls : Impargs.manual_implicits list - ; fields : Constr.rel_context - ; is_coercion : bool - ; coers : projection_flags list - } -end - let declare_structure ~cumulative finite ubinders ~univs paramimpls params template ?(kind=Decls.StructureComponent) ?name (record_data : Data.t list) = let nparams = List.length params in let poly, ctx = @@ -469,7 +485,7 @@ let declare_structure ~cumulative finite ubinders ~univs paramimpls params templ | Some n -> n in let ntypes = List.length record_data in - let mk_block i { Data.id; idbuild; min_univ; arity; fields; _ } = + let mk_block i { Data.id; idbuild; rdata = { DataR.min_univ; arity; fields; _ }; _ } = let nfields = List.length fields in let args = Context.Rel.to_extended_list mkRel nfields params in let ind = applist (mkRel (ntypes - i + nparams + nfields), args) in @@ -480,7 +496,7 @@ let declare_structure ~cumulative finite ubinders ~univs paramimpls params templ mind_entry_lc = [type_constructor] } in let blocks = List.mapi mk_block record_data in - let check_template { Data.id; min_univ; fields; _ } = + let check_template { Data.id; rdata = { DataR.min_univ; fields; _ }; _ } = let template_candidate () = (* we use some dummy values for the arities in the rel_context as univs_of_constr doesn't care about localassums and @@ -515,7 +531,7 @@ let declare_structure ~cumulative finite ubinders ~univs paramimpls params templ let template = List.for_all check_template record_data in let primitive = !primitive_flag && - List.for_all (fun { Data.fields; _ } -> List.exists is_local_assum fields) record_data + List.for_all (fun { Data.rdata = { DataR.fields; _ }; _ } -> List.exists is_local_assum fields) record_data in let mie = { mind_entry_params = params; @@ -532,10 +548,10 @@ let declare_structure ~cumulative finite ubinders ~univs paramimpls params templ let kn = DeclareInd.declare_mutual_inductive_with_eliminations mie ubinders impls ~primitive_expected:!primitive_flag in - let map i { Data.fieldimpls; fields; is_coercion; coers } = + let map i { Data.is_coercion; coers; rdata = { DataR.implfs; fields; _}; _ } = let rsp = (kn, i) in (* This is ind path of idstruc *) let cstr = (rsp, 1) in - let kinds,sp_projs = declare_projections rsp ctx ~kind binder_name.(i) coers fieldimpls fields in + let kinds,sp_projs = declare_projections rsp ctx ~kind binder_name.(i) coers implfs fields in let build = GlobRef.ConstructRef cstr in let () = if is_coercion then ComCoercion.try_add_new_coercion build ~local:false ~poly in let npars = Inductiveops.inductive_nparams (Global.env()) rsp in @@ -555,21 +571,23 @@ let implicits_of_context ctx = List.map (fun name -> CAst.make (Some (name,true))) (List.rev (Anonymous :: (List.map RelDecl.get_name ctx))) -let declare_class def cumulative ubinders univs id idbuild paramimpls params min_univ arity - template fieldimpls fields ?(kind=Decls.StructureComponent) coers = - let fieldimpls = +let declare_class def cumulative ubinders univs id idbuild paramimpls params + rdata template ?(kind=Decls.StructureComponent) coers = + let implfs = (* Make the class implicit in the projections, and the params if applicable. *) let impls = implicits_of_context params in - List.map (fun x -> impls @ x) fieldimpls + List.map (fun x -> impls @ x) rdata.DataR.implfs in + let rdata = { rdata with DataR.implfs } in let binder_name = Namegen.next_ident_away id (Termops.vars_of_env (Global.env())) in + let fields = rdata.DataR.fields in let data = match fields with | [ LocalAssum ({binder_name=Name proj_name} as binder, field) | LocalDef ({binder_name=Name proj_name} as binder, _, field) ] when def -> let binder = {binder with binder_name=Name binder_name} in let class_body = it_mkLambda_or_LetIn field params in - let class_type = it_mkProd_or_LetIn arity params in + let class_type = it_mkProd_or_LetIn rdata.DataR.arity params in let class_entry = Declare.definition_entry ~types:class_type ~univs class_body in let cst = Declare.declare_constant ~name:id @@ -592,7 +610,7 @@ let declare_class def cumulative ubinders univs id idbuild paramimpls params min in let cref = GlobRef.ConstRef cst in Impargs.declare_manual_implicits false cref paramimpls; - Impargs.declare_manual_implicits false (GlobRef.ConstRef proj_cst) (List.hd fieldimpls); + Impargs.declare_manual_implicits false (GlobRef.ConstRef proj_cst) (List.hd implfs); Classes.set_typeclass_transparency (EvalConstRef cst) false false; let sub = List.hd coers in let m = { @@ -605,12 +623,9 @@ let declare_class def cumulative ubinders univs id idbuild paramimpls params min let record_data = { Data.id ; idbuild - ; min_univ - ; arity - ; fieldimpls - ; fields ; is_coercion = false ; coers = List.map (fun _ -> { pf_subclass = false ; pf_canonical = true }) fields + ; rdata } in let inds = declare_structure ~cumulative Declarations.BiFinite ubinders ~univs paramimpls params template ~kind:Decls.Method ~name:[|binder_name|] [record_data] @@ -721,14 +736,13 @@ module Ast = struct ; sort : constr_expr option } - let to_idata { name; is_coercion; cfs; idbuild; sort } = + let to_rdata { name; is_coercion; cfs; idbuild; sort } = let fs = List.map fst cfs in { DataI.name = name.CAst.v ; arity = sort ; nots = List.map (fun (_, { rf_notation }) -> rf_notation) cfs ; fs } - end let check_unique_names records = @@ -753,7 +767,7 @@ let check_priorities kind records = user_err Pp.(str "Priorities only allowed for type class substructures") let extract_record_data records = - let data = List.map Ast.to_idata records in + let data = List.map Ast.to_rdata records in let pss = List.map (fun { Ast.binders; _ } -> binders) records in let ps = match pss with | [] -> CErrors.anomaly (str "Empty record block") @@ -775,7 +789,7 @@ let definition_structure udecl kind ~template ~cumulative ~poly finite (records let () = check_unique_names records in let () = check_priorities kind records in let ps, data = extract_record_data records in - let ubinders, univs, auto_template, params, implpars, data = + let auto_template, implpars, ubinders, univs, params, data = (* In theory we should be able to use [Notation.with_notation_protection], due to the call to Metasyntax.set_notation_for_interpretation, however something @@ -786,9 +800,10 @@ let definition_structure udecl kind ~template ~cumulative ~poly finite (records let template = template, auto_template in match kind with | Class def -> - let { Ast.name; cfs; idbuild; _ }, (univ, arity, implfs, fields) = match records, data with + let { Ast.name; cfs; idbuild; _ }, rdata = match records, data with | [r], [d] -> r, d - | _, _ -> CErrors.user_err (str "Mutual definitional classes are not handled") + | _, _ -> + CErrors.user_err (str "Mutual definitional classes are not handled") in let coers = List.map (fun (_, { rf_subclass; rf_priority }) -> match rf_subclass with @@ -796,18 +811,19 @@ let definition_structure udecl kind ~template ~cumulative ~poly finite (records | Vernacexpr.NoInstance -> None) cfs in declare_class def cumulative ubinders univs name.CAst.v idbuild - implpars params univ arity template implfs fields coers + implpars params rdata template coers | _ -> - let map impls = implpars @ [CAst.make None] @ impls in - let data = List.map (fun (univ, arity, implfs, fields) -> (univ, arity, List.map map implfs, fields)) data in - let map (min_univ, arity, fieldimpls, fields) { Ast.name; is_coercion; cfs; idbuild; _ } = + let adjust_impls impls = implpars @ [CAst.make None] @ impls in + let data = List.map (fun ({ DataR.implfs; _ } as d) -> { d with DataR.implfs = List.map adjust_impls implfs }) data in + (* let map (min_univ, arity, fieldimpls, fields) { Ast.name; is_coercion; cfs; idbuild; _ } = *) + let map rdata { Ast.name; is_coercion; cfs; idbuild; _ } = let coers = List.map (fun (_, { rf_subclass ; rf_canonical }) -> { pf_subclass = (match rf_subclass with Vernacexpr.BackInstance -> true | Vernacexpr.NoInstance -> false); pf_canonical = rf_canonical }) cfs in - { Data.id = name.CAst.v; idbuild; min_univ; arity; fieldimpls; fields; is_coercion; coers } + { Data.id = name.CAst.v; idbuild; rdata; is_coercion; coers } in let data = List.map2 map data records in let inds = declare_structure ~cumulative finite ubinders ~univs implpars params template data in -- cgit v1.2.3 From d4ce120346aaecef518c0781cf194308bad55f12 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 30 Jun 2020 16:27:29 +0200 Subject: [record] Refactor nested functions. In preparation for better handling of the regular record / class codepath. This will also allow to pack record data better. --- vernac/record.ml | 353 +++++++++++++++++++++++++++++-------------------------- 1 file changed, 186 insertions(+), 167 deletions(-) diff --git a/vernac/record.ml b/vernac/record.ml index b0b6194d7f..24d03e70d6 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -343,6 +343,57 @@ let instantiate_possibly_recursive_type ind u ntypes paramdecls fields = (* TODO: refactor the declaration part here; this requires some surgery as Evarutil.finalize is called too early in the path *) +let build_named_proj ~primitive ~flags ~poly ~univs ~uinstance ~kind env paramdecls + paramargs decl impls fid subst sp_projs nfi ti i indsp mib lifted_fields x rp = + let ccl = subst_projection fid subst ti in + let body, p_opt = match decl with + | LocalDef (_,ci,_) -> subst_projection fid subst ci, None + | LocalAssum ({binder_relevance=rci},_) -> + (* [ccl] is defined in context [params;x:rp] *) + (* [ccl'] is defined in context [params;x:rp;x:rp] *) + if primitive then + let p = Projection.Repr.make indsp + ~proj_npars:mib.mind_nparams ~proj_arg:i (Label.of_id fid) in + mkProj (Projection.make p true, mkRel 1), Some p + else + let ccl' = liftn 1 2 ccl in + let p = mkLambda (x, lift 1 rp, ccl') in + let branch = it_mkLambda_or_LetIn (mkRel nfi) lifted_fields in + let ci = Inductiveops.make_case_info env indsp rci LetStyle in + (* Record projections are always NoInvert because they're at + constant relevance *) + mkCase (ci, p, NoInvert, mkRel 1, [|branch|]), None + in + let proj = it_mkLambda_or_LetIn (mkLambda (x,rp,body)) paramdecls in + let projtyp = it_mkProd_or_LetIn (mkProd (x,rp,ccl)) paramdecls in + let entry = Declare.definition_entry ~univs ~types:projtyp proj in + let kind = Decls.IsDefinition kind in + let kn = + try Declare.declare_constant ~name:fid ~kind (Declare.DefinitionEntry entry) + with Type_errors.TypeError (ctx,te) as exn when not primitive -> + let _, info = Exninfo.capture exn in + Exninfo.iraise (NotDefinable (BadTypedProj (fid,ctx,te)),info) + in + Declare.definition_message fid; + let term = match p_opt with + | Some p -> + let _ = DeclareInd.declare_primitive_projection p kn in + mkProj (Projection.make p false,mkRel 1) + | None -> + let proj_args = (*Rel 1 refers to "x"*) paramargs@[mkRel 1] in + match decl with + | LocalDef (_,ci,_) when primitive -> body + | _ -> applist (mkConstU (kn,uinstance),proj_args) + in + let refi = GlobRef.ConstRef kn in + Impargs.maybe_declare_manual_implicits false refi impls; + if flags.pf_subclass then begin + let cl = ComCoercion.class_of_global (GlobRef.IndRef indsp) in + ComCoercion.try_add_new_coercion_with_source refi ~local:false ~poly ~source:cl + end; + let i = if is_local_assum decl then i+1 else i in + (Some kn::sp_projs, i, Projection term::subst) + let build_proj env mib indsp primitive x rp lifted_fields ~poly paramdecls paramargs ~uinstance ~kind ~univs (nfi,i,kinds,sp_projs,subst) flags decl impls = let fi = RelDecl.get_name decl in @@ -352,55 +403,9 @@ let build_proj env mib indsp primitive x rp lifted_fields ~poly paramdecls param | Anonymous -> (None::sp_projs,i,NoProjection fi::subst) | Name fid -> - try - let ccl = subst_projection fid subst ti in - let body, p_opt = match decl with - | LocalDef (_,ci,_) -> subst_projection fid subst ci, None - | LocalAssum ({binder_relevance=rci},_) -> - (* [ccl] is defined in context [params;x:rp] *) - (* [ccl'] is defined in context [params;x:rp;x:rp] *) - if primitive then - let p = Projection.Repr.make indsp - ~proj_npars:mib.mind_nparams ~proj_arg:i (Label.of_id fid) in - mkProj (Projection.make p true, mkRel 1), Some p - else - let ccl' = liftn 1 2 ccl in - let p = mkLambda (x, lift 1 rp, ccl') in - let branch = it_mkLambda_or_LetIn (mkRel nfi) lifted_fields in - let ci = Inductiveops.make_case_info env indsp rci LetStyle in - (* Record projections are always NoInvert because - they're at constant relevance *) - mkCase (ci, p, NoInvert, mkRel 1, [|branch|]), None - in - let proj = it_mkLambda_or_LetIn (mkLambda (x,rp,body)) paramdecls in - let projtyp = it_mkProd_or_LetIn (mkProd (x,rp,ccl)) paramdecls in - let entry = Declare.definition_entry ~univs ~types:projtyp proj in - let kind = Decls.IsDefinition kind in - let kn = - try Declare.declare_constant ~name:fid ~kind (Declare.DefinitionEntry entry) - with Type_errors.TypeError (ctx,te) as exn when not primitive -> - let _, info = Exninfo.capture exn in - Exninfo.iraise (NotDefinable (BadTypedProj (fid,ctx,te)),info) - in - Declare.definition_message fid; - let term = match p_opt with - | Some p -> - let _ = DeclareInd.declare_primitive_projection p kn in - mkProj (Projection.make p false,mkRel 1) - | None -> - let proj_args = (*Rel 1 refers to "x"*) paramargs@[mkRel 1] in - match decl with - | LocalDef (_,ci,_) when primitive -> body - | _ -> applist (mkConstU (kn,uinstance),proj_args) - in - let refi = GlobRef.ConstRef kn in - Impargs.maybe_declare_manual_implicits false refi impls; - if flags.pf_subclass then begin - let cl = ComCoercion.class_of_global (GlobRef.IndRef indsp) in - ComCoercion.try_add_new_coercion_with_source refi ~local:false ~poly ~source:cl - end; - let i = if is_local_assum decl then i+1 else i in - (Some kn::sp_projs, i, Projection term::subst) + try build_named_proj + ~primitive ~flags ~poly ~univs ~uinstance ~kind env paramdecls paramargs decl impls fid + subst sp_projs nfi ti i indsp mib lifted_fields x rp with NotDefinable why as exn -> let _, info = Exninfo.capture exn in warning_or_error ~info flags.pf_subclass indsp why; @@ -440,6 +445,38 @@ let declare_projections indsp univs ?(kind=Decls.StructureComponent) binder_name open Typeclasses +let check_template ~template ~poly ~univs ~params { Data.id; rdata = { DataR.min_univ; fields; _ }; _ } = + let template_candidate () = + (* we use some dummy values for the arities in the rel_context + as univs_of_constr doesn't care about localassums and + getting the real values is too annoying *) + let add_levels c levels = Univ.LSet.union levels (Vars.universes_of_constr c) in + let param_levels = + List.fold_left (fun levels d -> match d with + | LocalAssum _ -> levels + | LocalDef (_,b,t) -> add_levels b (add_levels t levels)) + Univ.LSet.empty params + in + let ctor_levels = List.fold_left + (fun univs d -> + let univs = + RelDecl.fold_constr (fun c univs -> add_levels c univs) d univs + in + univs) + param_levels fields + in + ComInductive.template_polymorphism_candidate ~ctor_levels univs params + (Some (Sorts.sort_of_univ min_univ)) + in + match template with + | Some template, _ -> + (* templateness explicitly requested *) + if poly && template then user_err Pp.(strbrk "template and polymorphism not compatible"); + template + | None, template -> + (* auto detect template *) + ComInductive.should_auto_template id (template && template_candidate ()) + let load_structure i (_, structure) = Recordops.register_structure structure @@ -466,7 +503,7 @@ let inStruc : Recordops.struc_typ -> Libobject.obj = let declare_structure_entry o = Lib.add_anonymous_leaf (inStruc o) -let declare_structure ~cumulative finite ubinders ~univs paramimpls params template ?(kind=Decls.StructureComponent) ?name (record_data : Data.t list) = +let declare_structure ~cumulative finite ~ubind ~univs paramimpls params template ?(kind=Decls.StructureComponent) ?name (record_data : Data.t list) = let nparams = List.length params in let poly, ctx = match univs with @@ -496,39 +533,7 @@ let declare_structure ~cumulative finite ubinders ~univs paramimpls params templ mind_entry_lc = [type_constructor] } in let blocks = List.mapi mk_block record_data in - let check_template { Data.id; rdata = { DataR.min_univ; fields; _ }; _ } = - let template_candidate () = - (* we use some dummy values for the arities in the rel_context - as univs_of_constr doesn't care about localassums and - getting the real values is too annoying *) - let add_levels c levels = Univ.LSet.union levels (Vars.universes_of_constr c) in - let param_levels = - List.fold_left (fun levels d -> match d with - | LocalAssum _ -> levels - | LocalDef (_,b,t) -> add_levels b (add_levels t levels)) - Univ.LSet.empty params - in - let ctor_levels = List.fold_left - (fun univs d -> - let univs = - RelDecl.fold_constr (fun c univs -> add_levels c univs) d univs - in - univs) - param_levels fields - in - ComInductive.template_polymorphism_candidate ~ctor_levels univs params - (Some (Sorts.sort_of_univ min_univ)) - in - match template with - | Some template, _ -> - (* templateness explicitly requested *) - if poly && template then user_err Pp.(strbrk "template and polymorphism not compatible"); - template - | None, template -> - (* auto detect template *) - ComInductive.should_auto_template id (template && template_candidate ()) - in - let template = List.for_all check_template record_data in + let template = List.for_all (check_template ~template ~univs ~poly ~params) record_data in let primitive = !primitive_flag && List.for_all (fun { Data.rdata = { DataR.fields; _ }; _ } -> List.exists is_local_assum fields) record_data @@ -545,7 +550,7 @@ let declare_structure ~cumulative finite ubinders ~univs paramimpls params templ } in let impls = List.map (fun _ -> paramimpls, []) record_data in - let kn = DeclareInd.declare_mutual_inductive_with_eliminations mie ubinders impls + let kn = DeclareInd.declare_mutual_inductive_with_eliminations mie ubind impls ~primitive_expected:!primitive_flag in let map i { Data.is_coercion; coers; rdata = { DataR.implfs; fields; _}; _ } = @@ -571,7 +576,64 @@ let implicits_of_context ctx = List.map (fun name -> CAst.make (Some (name,true))) (List.rev (Anonymous :: (List.map RelDecl.get_name ctx))) -let declare_class def cumulative ubinders univs id idbuild paramimpls params +let build_class_constant ~univs ~rdata field implfs params paramimpls coers binder id proj_name = + let class_body = it_mkLambda_or_LetIn field params in + let class_type = it_mkProd_or_LetIn rdata.DataR.arity params in + let class_entry = + Declare.definition_entry ~types:class_type ~univs class_body in + let cst = Declare.declare_constant ~name:id + (Declare.DefinitionEntry class_entry) ~kind:Decls.(IsDefinition Definition) + in + let inst, univs = match univs with + | Polymorphic_entry (_, uctx) -> Univ.UContext.instance uctx, univs + | Monomorphic_entry _ -> Univ.Instance.empty, Monomorphic_entry Univ.ContextSet.empty + in + let cstu = (cst, inst) in + let inst_type = appvectc (mkConstU cstu) + (Termops.rel_vect 0 (List.length params)) in + let proj_type = + it_mkProd_or_LetIn (mkProd(binder, inst_type, lift 1 field)) params in + let proj_body = + it_mkLambda_or_LetIn (mkLambda (binder, inst_type, mkRel 1)) params in + let proj_entry = Declare.definition_entry ~types:proj_type ~univs proj_body in + let proj_cst = Declare.declare_constant ~name:proj_name + (Declare.DefinitionEntry proj_entry) ~kind:Decls.(IsDefinition Definition) + in + let cref = GlobRef.ConstRef cst in + Impargs.declare_manual_implicits false cref paramimpls; + Impargs.declare_manual_implicits false (GlobRef.ConstRef proj_cst) (List.hd implfs); + Classes.set_typeclass_transparency (EvalConstRef cst) false false; + let sub = List.hd coers in + let m = { + meth_name = Name proj_name; + meth_info = sub; + meth_const = Some proj_cst; + } in + [cref, [m]] + +let build_record_constant ~rdata ~ubind ~univs ~cumulative ~template fields params paramimpls coers id idbuild binder_name = + let record_data = + { Data.id + ; idbuild + ; is_coercion = false + ; coers = List.map (fun _ -> { pf_subclass = false ; pf_canonical = true }) fields + ; rdata + } in + let inds = declare_structure ~cumulative Declarations.BiFinite ~ubind ~univs paramimpls + params template ~kind:Decls.Method ~name:[|binder_name|] [record_data] + in + let map ind = + let map decl b y = { + meth_name = RelDecl.get_name decl; + meth_info = b; + meth_const = y; + } in + let l = List.map3 map (List.rev fields) coers (Recordops.lookup_projections ind) in + GlobRef.IndRef ind, l + in + List.map map inds + +let declare_class def ~cumulative ~ubind ~univs id idbuild paramimpls params rdata template ?(kind=Decls.StructureComponent) coers = let implfs = (* Make the class implicit in the projections, and the params if applicable. *) @@ -586,60 +648,9 @@ let declare_class def cumulative ubinders univs id idbuild paramimpls params | [ LocalAssum ({binder_name=Name proj_name} as binder, field) | LocalDef ({binder_name=Name proj_name} as binder, _, field) ] when def -> let binder = {binder with binder_name=Name binder_name} in - let class_body = it_mkLambda_or_LetIn field params in - let class_type = it_mkProd_or_LetIn rdata.DataR.arity params in - let class_entry = - Declare.definition_entry ~types:class_type ~univs class_body in - let cst = Declare.declare_constant ~name:id - (Declare.DefinitionEntry class_entry) ~kind:Decls.(IsDefinition Definition) - in - let inst, univs = match univs with - | Polymorphic_entry (_, uctx) -> Univ.UContext.instance uctx, univs - | Monomorphic_entry _ -> Univ.Instance.empty, Monomorphic_entry Univ.ContextSet.empty - in - let cstu = (cst, inst) in - let inst_type = appvectc (mkConstU cstu) - (Termops.rel_vect 0 (List.length params)) in - let proj_type = - it_mkProd_or_LetIn (mkProd(binder, inst_type, lift 1 field)) params in - let proj_body = - it_mkLambda_or_LetIn (mkLambda (binder, inst_type, mkRel 1)) params in - let proj_entry = Declare.definition_entry ~types:proj_type ~univs proj_body in - let proj_cst = Declare.declare_constant ~name:proj_name - (Declare.DefinitionEntry proj_entry) ~kind:Decls.(IsDefinition Definition) - in - let cref = GlobRef.ConstRef cst in - Impargs.declare_manual_implicits false cref paramimpls; - Impargs.declare_manual_implicits false (GlobRef.ConstRef proj_cst) (List.hd implfs); - Classes.set_typeclass_transparency (EvalConstRef cst) false false; - let sub = List.hd coers in - let m = { - meth_name = Name proj_name; - meth_info = sub; - meth_const = Some proj_cst; - } in - [cref, [m]] + build_class_constant ~rdata ~univs field implfs params paramimpls coers binder id proj_name | _ -> - let record_data = - { Data.id - ; idbuild - ; is_coercion = false - ; coers = List.map (fun _ -> { pf_subclass = false ; pf_canonical = true }) fields - ; rdata - } in - let inds = declare_structure ~cumulative Declarations.BiFinite ubinders ~univs paramimpls - params template ~kind:Decls.Method ~name:[|binder_name|] [record_data] - in - let map ind = - let map decl b y = { - meth_name = RelDecl.get_name decl; - meth_info = b; - meth_const = y; - } in - let l = List.map3 map (List.rev fields) coers (Recordops.lookup_projections ind) in - GlobRef.IndRef ind, l - in - List.map map inds + build_record_constant ~rdata ~ubind ~univs ~cumulative ~template fields params paramimpls coers id idbuild binder_name in let univs, params, fields = match univs with @@ -782,6 +793,39 @@ let extract_record_data records = in ps, data +(* declaring structures, common data to refactor *) +let class_struture ~cumulative ~template ~ubind ~impargs ~univs ~params def records data = + let { Ast.name; cfs; idbuild; _ }, rdata = match records, data with + | [r], [d] -> r, d + | _, _ -> + CErrors.user_err (str "Mutual definitional classes are not handled") + in + let coers = List.map (fun (_, { rf_subclass; rf_priority }) -> + match rf_subclass with + | Vernacexpr.BackInstance -> Some {hint_priority = rf_priority; hint_pattern = None} + | Vernacexpr.NoInstance -> None) + cfs + in + declare_class def ~cumulative ~ubind ~univs name.CAst.v idbuild + impargs params rdata template coers + +let regular_structure ~cumulative ~template ~ubind ~impargs ~univs ~params ~finite records data = + let adjust_impls impls = impargs @ [CAst.make None] @ impls in + let data = List.map (fun ({ DataR.implfs; _ } as d) -> { d with DataR.implfs = List.map adjust_impls implfs }) data in + (* let map (min_univ, arity, fieldimpls, fields) { Ast.name; is_coercion; cfs; idbuild; _ } = *) + let map rdata { Ast.name; is_coercion; cfs; idbuild; _ } = + let coers = List.map (fun (_, { rf_subclass ; rf_canonical }) -> + { pf_subclass = + (match rf_subclass with Vernacexpr.BackInstance -> true | Vernacexpr.NoInstance -> false); + pf_canonical = rf_canonical }) + cfs + in + { Data.id = name.CAst.v; idbuild; rdata; is_coercion; coers } + in + let data = List.map2 map data records in + let inds = declare_structure ~cumulative finite ~ubind ~univs impargs params template data in + List.map (fun ind -> GlobRef.IndRef ind) inds + (* [fs] corresponds to fields and [ps] to parameters; [coers] is a list telling if the corresponding fields must me declared as coercions or subinstances. *) @@ -789,7 +833,7 @@ let definition_structure udecl kind ~template ~cumulative ~poly finite (records let () = check_unique_names records in let () = check_priorities kind records in let ps, data = extract_record_data records in - let auto_template, implpars, ubinders, univs, params, data = + let auto_template, impargs, ubind, univs, params, data = (* In theory we should be able to use [Notation.with_notation_protection], due to the call to Metasyntax.set_notation_for_interpretation, however something @@ -800,31 +844,6 @@ let definition_structure udecl kind ~template ~cumulative ~poly finite (records let template = template, auto_template in match kind with | Class def -> - let { Ast.name; cfs; idbuild; _ }, rdata = match records, data with - | [r], [d] -> r, d - | _, _ -> - CErrors.user_err (str "Mutual definitional classes are not handled") - in - let coers = List.map (fun (_, { rf_subclass; rf_priority }) -> - match rf_subclass with - | Vernacexpr.BackInstance -> Some {hint_priority = rf_priority; hint_pattern = None} - | Vernacexpr.NoInstance -> None) - cfs in - declare_class def cumulative ubinders univs name.CAst.v idbuild - implpars params rdata template coers - | _ -> - let adjust_impls impls = implpars @ [CAst.make None] @ impls in - let data = List.map (fun ({ DataR.implfs; _ } as d) -> { d with DataR.implfs = List.map adjust_impls implfs }) data in - (* let map (min_univ, arity, fieldimpls, fields) { Ast.name; is_coercion; cfs; idbuild; _ } = *) - let map rdata { Ast.name; is_coercion; cfs; idbuild; _ } = - let coers = List.map (fun (_, { rf_subclass ; rf_canonical }) -> - { pf_subclass = - (match rf_subclass with Vernacexpr.BackInstance -> true | Vernacexpr.NoInstance -> false); - pf_canonical = rf_canonical }) - cfs - in - { Data.id = name.CAst.v; idbuild; rdata; is_coercion; coers } - in - let data = List.map2 map data records in - let inds = declare_structure ~cumulative finite ubinders ~univs implpars params template data in - List.map (fun ind -> GlobRef.IndRef ind) inds + class_struture ~template ~ubind ~impargs ~cumulative ~params ~univs def records data + | Inductive_kw | CoInductive | Variant | Record | Structure -> + regular_structure ~cumulative ~template ~ubind ~impargs ~univs ~params ~finite records data -- cgit v1.2.3 From df19ab7cc9931580171ed910f6b2d15ff8247492 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 2 Jul 2020 17:41:53 +0200 Subject: [record] Options API cleanup. --- vernac/record.ml | 59 +++++++++++++++++++++++-------------------------------- vernac/record.mli | 2 -- 2 files changed, 25 insertions(+), 36 deletions(-) diff --git a/vernac/record.ml b/vernac/record.ml index 24d03e70d6..6e024d08ca 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -28,32 +28,23 @@ module RelDecl = Context.Rel.Declaration (********** definition d'un record (structure) **************) (** Flag governing use of primitive projections. Disabled by default. *) -let primitive_flag = ref false -let () = - let open Goptions in - declare_bool_option - { optdepr = false; - optkey = ["Primitive";"Projections"]; - optread = (fun () -> !primitive_flag) ; - optwrite = (fun b -> primitive_flag := b) } - -let typeclasses_strict = ref false -let () = - let open Goptions in - declare_bool_option - { optdepr = false; - optkey = ["Typeclasses";"Strict";"Resolution"]; - optread = (fun () -> !typeclasses_strict); - optwrite = (fun b -> typeclasses_strict := b); } - -let typeclasses_unique = ref false -let () = - let open Goptions in - declare_bool_option - { optdepr = false; - optkey = ["Typeclasses";"Unique";"Instances"]; - optread = (fun () -> !typeclasses_unique); - optwrite = (fun b -> typeclasses_unique := b); } +let primitive_flag = + Goptions.declare_bool_option_and_ref + ~depr:false + ~key:["Primitive";"Projections"] + ~value:false + +let typeclasses_strict = + Goptions.declare_bool_option_and_ref + ~depr:false + ~key:["Typeclasses";"Strict";"Resolution"] + ~value:false + +let typeclasses_unique = + Goptions.declare_bool_option_and_ref + ~depr:false + ~key:["Typeclasses";"Unique";"Instances"] + ~value:false let interp_fields_evars env sigma ~ninds ~nparams impls_env nots l = let _, sigma, impls, newfs, _ = @@ -535,7 +526,7 @@ let declare_structure ~cumulative finite ~ubind ~univs paramimpls params templat let blocks = List.mapi mk_block record_data in let template = List.for_all (check_template ~template ~univs ~poly ~params) record_data in let primitive = - !primitive_flag && + primitive_flag () && List.for_all (fun { Data.rdata = { DataR.fields; _ }; _ } -> List.exists is_local_assum fields) record_data in let mie = @@ -551,7 +542,7 @@ let declare_structure ~cumulative finite ~ubind ~univs paramimpls params templat in let impls = List.map (fun _ -> paramimpls, []) record_data in let kn = DeclareInd.declare_mutual_inductive_with_eliminations mie ubind impls - ~primitive_expected:!primitive_flag + ~primitive_expected:(primitive_flag ()) in let map i { Data.is_coercion; coers; rdata = { DataR.implfs; fields; _}; _ } = let rsp = (kn, i) in (* This is ind path of idstruc *) @@ -668,8 +659,8 @@ let declare_class def ~cumulative ~ubind ~univs id idbuild paramimpls params let k = { cl_univs = univs; cl_impl = impl; - cl_strict = !typeclasses_strict; - cl_unique = !typeclasses_unique; + cl_strict = typeclasses_strict (); + cl_unique = typeclasses_unique (); cl_context = params; cl_props = fields; cl_projs = projs } @@ -693,8 +684,8 @@ let add_constant_class env sigma cst = cl_context = ctx; cl_props = [LocalAssum (make_annot Anonymous r, t)]; cl_projs = []; - cl_strict = !typeclasses_strict; - cl_unique = !typeclasses_unique + cl_strict = typeclasses_strict (); + cl_unique = typeclasses_unique () } in Classes.add_class env sigma tc; @@ -715,8 +706,8 @@ let add_inductive_class env sigma ind = cl_context = ctx; cl_props = [LocalAssum (make_annot Anonymous r, ty)]; cl_projs = []; - cl_strict = !typeclasses_strict; - cl_unique = !typeclasses_unique } + cl_strict = typeclasses_strict (); + cl_unique = typeclasses_unique () } in Classes.add_class env sigma k diff --git a/vernac/record.mli b/vernac/record.mli index c3b84540f0..86819a25ec 100644 --- a/vernac/record.mli +++ b/vernac/record.mli @@ -12,8 +12,6 @@ open Names open Vernacexpr open Constrexpr -val primitive_flag : bool ref - module Ast : sig type t = { name : Names.lident -- cgit v1.2.3 From 593e99514abc1b43a011f4ae64f40443714b0a68 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 30 Jun 2020 18:03:14 +0200 Subject: [record] [ci] Overlay for elpi We re-expose `declare_projections` and `declare_structure_entry` as it is needed by coq-elpi. Ideally we would provide a better way in recordops to interact with this, in fact `declare_structure_entry` is just a wrapper around recordops + libobject structure so there is hope it goes away entirely in the future. The need for Elpi to manually call `declare_projections` should actually disappear in future refactorings. --- .../12611-ejgallego-record+refactor.sh | 9 +++++++++ vernac/record.ml | 9 +++++++++ vernac/record.mli | 23 ++++++++++++++++++++-- 3 files changed, 39 insertions(+), 2 deletions(-) create mode 100644 dev/ci/user-overlays/12611-ejgallego-record+refactor.sh diff --git a/dev/ci/user-overlays/12611-ejgallego-record+refactor.sh b/dev/ci/user-overlays/12611-ejgallego-record+refactor.sh new file mode 100644 index 0000000000..b7d21ed59c --- /dev/null +++ b/dev/ci/user-overlays/12611-ejgallego-record+refactor.sh @@ -0,0 +1,9 @@ +if [ "$CI_PULL_REQUEST" = "12611" ] || [ "$CI_BRANCH" = "record+refactor" ]; then + + elpi_CI_REF=record+refactor + elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi + +# mtac2_CI_REF=record+refactor +# mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2 + +fi diff --git a/vernac/record.ml b/vernac/record.ml index 6e024d08ca..4c9479f386 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -838,3 +838,12 @@ let definition_structure udecl kind ~template ~cumulative ~poly finite (records class_struture ~template ~ubind ~impargs ~cumulative ~params ~univs def records data | Inductive_kw | CoInductive | Variant | Record | Structure -> regular_structure ~cumulative ~template ~ubind ~impargs ~univs ~params ~finite records data + +module Internal = struct + type nonrec projection_flags = projection_flags = { + pf_subclass: bool; + pf_canonical: bool; + } + let declare_projections = declare_projections + let declare_structure_entry = declare_structure_entry +end diff --git a/vernac/record.mli b/vernac/record.mli index 86819a25ec..ffcae2975e 100644 --- a/vernac/record.mli +++ b/vernac/record.mli @@ -35,5 +35,24 @@ val definition_structure val declare_existing_class : GlobRef.t -> unit -(** Used by elpi *) -val declare_structure_entry : Recordops.struc_typ -> unit +(* Implementation internals, consult Coq developers before using; + current user Elpi, see https://github.com/LPCIC/coq-elpi/pull/151 *) +module Internal : sig + type projection_flags = { + pf_subclass: bool; + pf_canonical: bool; + } + + val declare_projections + : Names.inductive + -> Entries.universes_entry + -> ?kind:Decls.definition_object_kind + -> Names.Id.t + -> projection_flags list + -> Impargs.manual_implicits list + -> Constr.rel_context + -> Recordops.proj_kind list * Names.Constant.t option list + + val declare_structure_entry : Recordops.struc_typ -> unit + +end -- cgit v1.2.3 From 94048f8960910cee604946d1b950b21bcc662ff8 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 16 Oct 2020 15:50:14 +0200 Subject: [record] Some documentation + minor refactoring Co-authored-by: --- vernac/record.ml | 64 ++++++++++++++++++++++++++++++++++++++++++++++++++------ 1 file changed, 58 insertions(+), 6 deletions(-) diff --git a/vernac/record.ml b/vernac/record.ml index 4c9479f386..891d7fcebe 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -118,11 +118,16 @@ let check_parameters_must_be_named = function | CLocalPattern {CAst.loc} -> Loc.raise ?loc (Stream.Error "pattern with quote not allowed in record parameters") +(** [DataI.t] contains the information used in record interpretation, + it is a strict subset of [Ast.t] thus this should be + eventually removed or merged with [Ast.t] *) module DataI = struct type t = { name : Id.t ; arity : Constrexpr.constr_expr option + (** declared sort for the record *) ; nots : Vernacexpr.decl_notation list list + (** notations for fields *) ; fs : Vernacexpr.local_decl_expr list } end @@ -132,6 +137,8 @@ type projection_flags = { pf_canonical: bool; } +(** [DataR.t] contains record data after interpretation / + type-inference *) module DataR = struct type t = { min_univ : Univ.Universe.t @@ -334,6 +341,11 @@ let instantiate_possibly_recursive_type ind u ntypes paramdecls fields = (* TODO: refactor the declaration part here; this requires some surgery as Evarutil.finalize is called too early in the path *) +(** This builds and _declares_ a named projection, the code looks + tricky due to the term manipulation. It also handles declaring the + implicits parameters, coercion status, etc... of the projection; + this could be refactored as noted above by moving to the + higher-level declare constant API *) let build_named_proj ~primitive ~flags ~poly ~univs ~uinstance ~kind env paramdecls paramargs decl impls fid subst sp_projs nfi ti i indsp mib lifted_fields x rp = let ccl = subst_projection fid subst ti in @@ -385,6 +397,8 @@ let build_named_proj ~primitive ~flags ~poly ~univs ~uinstance ~kind env paramde let i = if is_local_assum decl then i+1 else i in (Some kn::sp_projs, i, Projection term::subst) +(** [build_proj] will build a projection for each field, or skip if + the field is anonymous, i.e. [_ : t] *) let build_proj env mib indsp primitive x rp lifted_fields ~poly paramdecls paramargs ~uinstance ~kind ~univs (nfi,i,kinds,sp_projs,subst) flags decl impls = let fi = RelDecl.get_name decl in @@ -408,6 +422,8 @@ let build_proj env mib indsp primitive x rp lifted_fields ~poly paramdecls param ; pk_canonical = flags.pf_canonical } :: kinds , sp_projs, subst) +(** [declare_projections] prepares the common context for all record + projections and then calls [build_proj] for each one. *) let declare_projections indsp univs ?(kind=Decls.StructureComponent) binder_name flags fieldimpls fields = let env = Global.env() in let (mib,mip) = Global.lookup_inductive indsp in @@ -494,6 +510,21 @@ let inStruc : Recordops.struc_typ -> Libobject.obj = let declare_structure_entry o = Lib.add_anonymous_leaf (inStruc o) +(** Main record declaration part: + + The entry point is [definition_structure], which will match on the + declared [kind] and then either follow the regular record + declaration path to [declare_structure] or handle the record as a + class declaration with [declare_class]. + +*) + +(** [declare_structure] does two principal things: + + - prepares and declares the low-level (mutual) inductive corresponding to [record_data] + - prepares and declares the corresponding record projections, mainly taken care of by + [declare_projections] +*) let declare_structure ~cumulative finite ~ubind ~univs paramimpls params template ?(kind=Decls.StructureComponent) ?name (record_data : Data.t list) = let nparams = List.length params in let poly, ctx = @@ -624,6 +655,28 @@ let build_record_constant ~rdata ~ubind ~univs ~cumulative ~template fields para in List.map map inds +(** [declare_class] will prepare and declare a [Class]. This is done in + 2 steps: + + 1. two markely different paths are followed depending on whether the + class declaration refers to a constant "definitional classes" or to + a record, that is to say: + + Class foo := bar : T. + + which is equivalent to + + Definition foo := T. + Definition bar (x:foo) : T := x. + Existing Class foo. + + vs + + Class foo := { ... }. + + 2. declare the class, using the information from 1. in the form of [Classes.typeclass] + + *) let declare_class def ~cumulative ~ubind ~univs id idbuild paramimpls params rdata template ?(kind=Decls.StructureComponent) coers = let implfs = @@ -671,7 +724,6 @@ let declare_class def ~cumulative ~ubind ~univs id idbuild paramimpls params in List.map map data - let add_constant_class env sigma cst = let ty, univs = Typeops.type_of_global_in_context env (GlobRef.ConstRef cst) in let r = (Environ.lookup_constant cst env).const_relevance in @@ -738,7 +790,7 @@ module Ast = struct ; sort : constr_expr option } - let to_rdata { name; is_coercion; cfs; idbuild; sort } = + let to_datai { name; is_coercion; cfs; idbuild; sort } = let fs = List.map fst cfs in { DataI.name = name.CAst.v ; arity = sort @@ -769,7 +821,7 @@ let check_priorities kind records = user_err Pp.(str "Priorities only allowed for type class substructures") let extract_record_data records = - let data = List.map Ast.to_rdata records in + let data = List.map Ast.to_datai records in let pss = List.map (fun { Ast.binders; _ } -> binders) records in let ps = match pss with | [] -> CErrors.anomaly (str "Empty record block") @@ -817,9 +869,9 @@ let regular_structure ~cumulative ~template ~ubind ~impargs ~univs ~params ~fini let inds = declare_structure ~cumulative finite ~ubind ~univs impargs params template data in List.map (fun ind -> GlobRef.IndRef ind) inds -(* [fs] corresponds to fields and [ps] to parameters; [coers] is a - list telling if the corresponding fields must me declared as coercions - or subinstances. *) +(** [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 udecl kind ~template ~cumulative ~poly finite (records : Ast.t list) = let () = check_unique_names records in let () = check_priorities kind records in -- cgit v1.2.3