Source file record.ml

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *         Copyright INRIA, CNRS and contributors             *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

open Pp
open CErrors
open Term
open Util
open Names
open Constr
open Context
open Environ
open Declarations
open Entries
open Type_errors
open Constrexpr
open Constrexpr_ops
open Context.Rel.Declaration
open Structures

module RelDecl = Context.Rel.Declaration

(********** definition d'un record (structure) **************)

(** Flag governing use of primitive projections. Disabled by default. *)
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, _ =
    List.fold_left2
      (fun (env, sigma, uimpls, params, impls_env) no d ->
         let sigma, (i, b, t), impl = match d with
           | Vernacexpr.AssumExpr({CAst.loc;v=id},bl,t) ->
             (* Temporary compatibility with the type-classes heuristics *)
             (* which are applied after the interpretation of bl and *)
             (* before the one of t otherwise (see #13166) *)
             let t = if bl = [] then t else mkCProdN bl t in
             let sigma, t, impl =
               ComAssumption.interp_assumption ~program_mode:false env sigma impls_env [] t in
             sigma, (id, None, t), impl
           | Vernacexpr.DefExpr({CAst.loc;v=id},bl,b,t) ->
             let sigma, (b, t), impl =
               ComDefinition.interp_definition ~program_mode:false env sigma impls_env bl None b t in
             let t = match t with Some t -> t | None -> Retyping.get_type_of env sigma b in
             sigma, (id, Some b, t), impl in
          let r = Retyping.relevance_of_type env sigma t in
         let impls_env =
           match i with
           | Anonymous -> 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)
           | Some b -> LocalDef (make_annot i r,b,t)
         in
         List.iter (Metasyntax.set_notation_for_interpretation env impls_env) no;
         (EConstr.push_rel d env, sigma, impl :: uimpls, d::params, impls_env))
      (env, sigma, [], [], impls_env) nots l
  in
  let _, _, sigma = Context.Rel.fold_outside ~init:(env,0,sigma) (fun f (env,k,sigma) ->
      let sigma = RelDecl.fold_constr (fun c sigma ->
          ComInductive.maybe_unify_params_in env sigma ~ninds ~nparams ~binders:k c)
          f sigma
      in
      EConstr.push_rel f env, k+1, sigma)
      newfs
  in
  sigma, (impls, newfs)

let compute_constructor_level evars env l =
  List.fold_right (fun d (env, univ) ->
    let univ =
      if is_local_assum d then
        let s = Retyping.get_sort_of env evars (RelDecl.get_type d) in
          Univ.sup (Sorts.univ_of_sort s) univ
      else univ
    in (EConstr.push_rel d env, univ))
    l (env, Univ.Universe.sprop)

let check_anonymous_type ind =
  match ind with
  | { CAst.v = CSort (Glob_term.UAnonymous {rigid=true}) } -> true
  | _ -> false

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")

(** [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

type projection_flags = {
  pf_subclass: bool;
  pf_canonical: bool;
}

(** [DataR.t] contains record data after interpretation /
   type-inference *)
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
    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."))

type tc_result =
  bool
  * Impargs.manual_implicits
  (* Part relative to closing the definitions *)
  * UnivNames.universe_binders
  * Entries.universes_entry
  * Entries.variance_entry
  * Constr.rel_context
  * DataR.t list

(* ps = parameter list *)
let typecheck_params_and_fields def poly udecl 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
     any Set <= i constraint for universes that might actually be instantiated with Prop. *)
  let is_template =
    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, variances = Constrintern.interp_cumul_univ_decl_opt env0 udecl 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 { 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 { DataI.name; _ } -> name) records in
    let imps = List.map (fun _ -> imps) arities in
    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 { 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
  let sigma =
    Pretyping.solve_remaining_evars Pretyping.all_and_fail_flags env_ar sigma in
  let fold sigma (typ, sort) (_, newfs) =
    let _, univ = compute_constructor_level sigma env_ar newfs in
    let univ = if Sorts.is_sprop sort then univ else Univ.Universe.sup univ Univ.type0m_univ in
      if not def && is_impredicative_sort env0 sort then
        sigma, (univ, typ)
      else
        let sigma = Evd.set_leq_sort env_ar sigma (Sorts.sort_of_univ univ) sort in
        if Univ.is_small_univ univ &&
           Option.cata (Evd.is_flexible_level sigma) false (Evd.is_sort_variable sigma sort) then
           (* We can assume that the level in aritysort is not constrained
               and clear it, if it is flexible *)
   Evd.set_eq_sort env_ar sigma Sorts.set sort, (univ, EConstr.mkSort (Sorts.sort_of_univ univ))
        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 (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)
  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 sigma (EConstr.of_constr t) in
  let () = List.iter (iter_constr ce) (List.rev newps) in
  template, imps, ubinders, univs, variances, newps, ans

type record_error =
  | MissingProj of Id.t * Id.t list
  | BadTypedProj of Id.t * env * Type_errors.type_error

let warn_cannot_define_projection =
  CWarnings.create ~name:"cannot-define-projection" ~category:"records"
         (fun msg -> hov 0 msg)

(* If a projection is not definable, we throw an error if the user
asked it to be a coercion. Otherwise, we just print an info
message. The user might still want to name the field of the record. *)
let warning_or_error ~info coe indsp err =
  let st = match err with
    | MissingProj (fi,projs) ->
        let s,have = if List.length projs > 1 then "s","were" else "","was" in
        (Id.print fi ++
           strbrk" cannot be defined because the projection" ++ str s ++ spc () ++
           prlist_with_sep pr_comma Id.print projs ++ spc () ++ str have ++
           strbrk " not defined.")
    | BadTypedProj (fi,ctx,te) ->
        match te with
          | ElimArity (_,_,_,Some (_,_,_,NonInformativeToInformative)) ->
              (Id.print fi ++
                strbrk" cannot be defined because it is informative and " ++
                Printer.pr_inductive (Global.env()) indsp ++
                strbrk " is not.")
          | ElimArity (_,_,_,Some (_,_,_,StrongEliminationOnNonSmallType)) ->
              (Id.print fi ++
                strbrk" cannot be defined because it is large and " ++
                Printer.pr_inductive (Global.env()) indsp ++
                strbrk " is not.")
          | _ ->
              (Id.print fi ++ strbrk " cannot be defined because it is not typable.")
  in
  if coe then user_err ~hdr:"structure" ~info st;
  warn_cannot_define_projection (hov 0 st)

type field_status =
  | NoProjection of Name.t
  | Projection of constr

exception NotDefinable of record_error

(* This replaces previous projection bodies in current projection *)
(* Undefined projs are collected and, at least one undefined proj occurs *)
(* in the body of current projection then the latter can not be defined *)
(* [c] is defined in ctxt [[params;fields]] and [l] is an instance of *)
(* [[fields]] defined in ctxt [[params;x:ind]] *)
let subst_projection fid l c =
  let lv = List.length l in
  let bad_projs = ref [] in
  let rec substrec depth c = match Constr.kind c with
    | Rel k ->
        (* We are in context [[params;fields;x:ind;...depth...]] *)
        if k <= depth+1 then
          c
        else if k-depth-1 <= lv then
          match List.nth l (k-depth-2) with
            | Projection t -> lift depth t
            | NoProjection (Name id) -> bad_projs := id :: !bad_projs; mkRel k
            | NoProjection Anonymous ->
                user_err  (str "Field " ++ Id.print fid ++
                  str " depends on the " ++ pr_nth (k-depth-1) ++ str
                  " field which has no name.")
        else
          mkRel (k-lv)
    | _ -> Constr.map_with_binders succ substrec depth c
  in
  let c' = lift 1 c in (* to get [c] defined in ctxt [[params;fields;x:ind]] *)
  let c'' = substrec 0 c' in
  if not (List.is_empty !bad_projs) then
    raise (NotDefinable (MissingProj (fid,List.rev !bad_projs)));
  c''

let instantiate_possibly_recursive_type ind u ntypes paramdecls fields =
  let subst = List.map_i (fun i _ -> mkRel i) 1 paramdecls in
  let subst' = List.init ntypes (fun i -> mkIndU ((ind, ntypes - i - 1), u)) in
  Termops.substl_rel_context (subst @ subst') fields

(* We build projections *)

(* 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 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 (Inductive.contract_case env (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, 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,subst) flags decl impls =
  let fi = RelDecl.get_name decl in
  let ti = RelDecl.get_type decl in
  let (sp_proj,i,subst) =
    match fi with
    | Anonymous ->
      (None,i,NoProjection fi::subst)
    | Name fid ->
      try build_named_proj
            ~primitive ~flags ~poly ~univs ~uinstance ~kind env paramdecls paramargs decl impls fid
            subst 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;
        (None,i,NoProjection fi::subst)
  in
  (nfi - 1, i,
   { Structure.proj_name = fi
   ; proj_true = is_local_assum decl
   ; proj_canonical = flags.pf_canonical
   ; proj_body = sp_proj } :: kinds
  , 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
  let poly = Declareops.inductive_is_polymorphic mib in
  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, 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) uinstance mib.mind_ntypes paramdecls fields in
  let lifted_fields = Termops.lift_rel_context 1 fields in
  let primitive =
    match mib.mind_record with
    | PrimRecord _ -> true
    | FakeRecord | NotRecord -> false
  in
  let (_,_,canonical_projections,_) =
    List.fold_left3
      (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
    List.rev canonical_projections

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) = Structure.register structure

let cache_structure o = load_structure 1 o

let subst_structure (subst, obj) = Structure.subst subst obj

let discharge_structure (_, x) = Some x

let rebuild_structure s = Structure.rebuild (Global.env()) s

let inStruc : Structure.t -> Libobject.obj =
  let open Libobject in
  declare_object {(default_object "STRUCTURE") with
    cache_function = cache_structure;
    load_function = load_structure;
    subst_function = subst_structure;
    classify_function = (fun x -> Substitute x);
    discharge_function = discharge_structure;
    rebuild_function = rebuild_structure; }

let declare_structure_entry o =
  Lib.add_anonymous_leaf (inStruc o)

(** In the type of every projection, the record is bound to a variable named
  using the first character of the record type. We rename it to avoid
  collisions with names already used in the field types.
*)

(** Get all names bound at the head of [t]. *)
let rec add_bound_names_constr (names : Id.Set.t) (t : constr) : Id.Set.t =
  match destProd t with
  | (b, _, t) ->
    let names =
      match b.binder_name with
      | Name.Anonymous -> names
      | Name.Name n -> Id.Set.add n names
    in add_bound_names_constr names t
  | exception DestKO -> names

(** Get all names bound in any record field. *)
let bound_names_rdata { DataR.fields; _ } : Id.Set.t =
  let add_names names field = add_bound_names_constr names (RelDecl.get_type field) in
  List.fold_left add_names Id.Set.empty fields

(** Pick a variable name for a record, avoiding names bound in its fields. *)
let data_name { Data.id; Data.rdata; _ } =
  let name = Id.of_string (Unicode.lowercase_first_char (Id.to_string id)) in
  Namegen.next_ident_away name (bound_names_rdata rdata)

(** 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 ~variances paramimpls params template ?(kind=Decls.StructureComponent) ?name (record_data : Data.t list) =
  let nparams = List.length params in
  let poly, ctx =
    match univs with
    | Monomorphic_entry ctx ->
      false, Monomorphic_entry Univ.ContextSet.empty
    | Polymorphic_entry (nas, ctx) ->
      true, Polymorphic_entry (nas, ctx)
  in
  let binder_name =
    match name with
    | None -> Array.map_of_list data_name record_data
    | Some n -> n
  in
  let ntypes = List.length record_data in
  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
    let type_constructor = it_mkProd_or_LetIn ind fields in
    { mind_entry_typename = id;
      mind_entry_arity = arity;
      mind_entry_consnames = [idbuild];
      mind_entry_lc = [type_constructor] }
  in
  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 () &&
    List.for_all (fun { Data.rdata = { DataR.fields; _ }; _ } -> List.exists is_local_assum fields) record_data
  in
  let mie =
    { mind_entry_params = params;
      mind_entry_record = Some (if primitive then Some binder_name else None);
      mind_entry_finite = finite;
      mind_entry_inds = blocks;
      mind_entry_private = None;
      mind_entry_universes = univs;
      mind_entry_template = template;
      mind_entry_variance = ComInductive.variance_of_entry ~cumulative ~variances univs;
    }
  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 ())
  in
  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 projections = 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 struc = Structure.make (Global.env ()) rsp projections in
    let () = declare_structure_entry struc in
    rsp
  in
  List.mapi map record_data

let implicits_of_context ctx =
  List.map (fun name -> CAst.make (Some (name,true)))
    (List.rev (Anonymous :: (List.map RelDecl.get_name ctx)))

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 (Tacred.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 ~variances ~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 ~variances 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 (Structure.find_projections ind) in
    GlobRef.IndRef ind, l
  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 ~variances 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) 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
      build_class_constant ~rdata ~univs field implfs params paramimpls coers binder id proj_name
    | _ ->
      build_record_constant ~rdata ~ubind ~univs ~variances ~cumulative ~template
        fields params paramimpls coers id idbuild binder_name
  in
  let univs, params, fields =
    match univs with
    | Polymorphic_entry (nas, univs) ->
      let usubst, auctx = Univ.abstract_universes nas univs in
      let usubst = Univ.make_instance_subst usubst in
      let map c = Vars.subst_univs_level_constr usubst c in
      let fields = Context.Rel.map map fields in
      let params = Context.Rel.map map params in
      auctx, params, fields
    | Monomorphic_entry _ ->
      Univ.AUContext.empty, params, fields
  in
  let map (impl, projs) =
    let k =
      { cl_univs = univs;
        cl_impl = impl;
        cl_strict = typeclasses_strict ();
        cl_unique = typeclasses_unique ();
        cl_context = params;
        cl_props = fields;
        cl_projs = projs }
    in
    let env = Global.env () in
    let sigma = Evd.from_env env in
    Classes.add_class env sigma k; impl
  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
  let ctx, _ = decompose_prod_assum ty in
  let args = Context.Rel.to_extended_vect Constr.mkRel 0 ctx in
  let t = mkApp (mkConstU (cst, Univ.make_abstract_instance univs), args) in
  let tc =
    { cl_univs = univs;
      cl_impl = GlobRef.ConstRef cst;
      cl_context = ctx;
      cl_props = [LocalAssum (make_annot Anonymous r, t)];
      cl_projs = [];
      cl_strict = typeclasses_strict ();
      cl_unique = typeclasses_unique ()
    }
  in
  Classes.add_class env sigma tc;
    Classes.set_typeclass_transparency (Tacred.EvalConstRef cst) false false

let add_inductive_class env sigma ind =
  let mind, oneind = Inductive.lookup_mind_specif env ind in
  let k =
    let ctx = oneind.mind_arity_ctxt in
    let univs = Declareops.inductive_polymorphic_context mind in
    let inst = Univ.make_abstract_instance univs in
    let ty = Inductive.type_of_inductive ((mind, oneind), inst) in
    let r = oneind.mind_relevance in
      { cl_univs = univs;
        cl_impl = GlobRef.IndRef ind;
        cl_context = ctx;
        cl_props = [LocalAssum (make_annot Anonymous r, ty)];
        cl_projs = [];
        cl_strict = typeclasses_strict ();
        cl_unique = typeclasses_unique () }
  in
  Classes.add_class env sigma k

let warn_already_existing_class =
  CWarnings.create ~name:"already-existing-class" ~category:"automation" Pp.(fun g ->
      Printer.pr_global g ++ str " is already declared as a typeclass.")

let declare_existing_class g =
  let env = Global.env () in
  let sigma = Evd.from_env env in
  if Typeclasses.is_class g then warn_already_existing_class g
  else
    match g with
    | GlobRef.ConstRef x -> add_constant_class env sigma x
    | GlobRef.IndRef x -> add_inductive_class env sigma x
    | _ -> user_err ~hdr:"declare_existing_class"
             (Pp.str"Unsupported class type, only constants and inductives are allowed")

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_datai { 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 { Ast.name; cfs; _ } ->
      name.CAst.v :: (List.fold_left extract_name acc cfs)) [] records
  in
  match List.duplicates Id.equal allnames with
  | [] -> ()
  | id :: _ -> user_err (str "Two objects have the same name" ++ spc () ++ quote (Id.print id))

let check_priorities kind records =
  let isnot_class = match kind with Class false -> false | _ -> true in
  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 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")
  | ps :: rem ->
    let eq_local_binders bl1 bl2 = List.equal local_binder_eq bl1 bl2 in
    let () =
      if not (List.for_all (eq_local_binders ps) rem) then
        user_err (str "Parameters should be syntactically the \
          same for each inductive type.")
    in
    ps
  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 ~variances ~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 ~variances
      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. *)
let definition_structure udecl kind ~template ~cumulative ~poly
    finite (records : Ast.t list) : GlobRef.t list =
  let () = check_unique_names records in
  let () = check_priorities kind records in
  let ps, data = extract_record_data records in
  let auto_template, impargs, ubind, univs, variances, 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
       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 ->
    class_struture ~template ~ubind ~impargs ~cumulative ~params ~univs ~variances
      def records data
  | Inductive_kw | CoInductive | Variant | Record | Structure ->
    regular_structure ~cumulative ~template ~ubind ~impargs ~univs ~variances ~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