|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \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 Sorts
open Util
open Names
open Globnames
open Nameops
open Constr
open Context
open Vars
open Environ
open Declarations
open Entries
open Declare
open Constrintern
open Decl_kinds
open Type_errors
open Constrexpr
open Constrexpr_ops
open Goptions
open Context.Rel.Declaration
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 () =
declare_bool_option
{ optdepr = false;
optname = "use of primitive projections";
optkey = ["Primitive";"Projections"];
optread = (fun () -> !primitive_flag) ;
optwrite = (fun b -> primitive_flag := b) }
let typeclasses_strict = ref false
let () =
declare_bool_option
{ optdepr = false;
optname = "strict typeclass resolution";
optkey = ["Typeclasses";"Strict";"Resolution"];
optread = (fun () -> !typeclasses_strict);
optwrite = (fun b -> typeclasses_strict := b); }
let typeclasses_unique = ref false
let () =
declare_bool_option
{ optdepr = false;
optname = "unique typeclass instances";
optkey = ["Typeclasses";"Unique";"Instances"];
optread = (fun () -> !typeclasses_unique);
optwrite = (fun b -> typeclasses_unique := b); }
let interp_fields_evars env sigma impls_env nots l =
List.fold_left2
(fun (env, sigma, uimpls, params, impls) no ({CAst.loc;v=i}, b, t) ->
let sigma, (t', impl) = interp_type_evars_impls ~program_mode:false env sigma ~impls t in
let r = Retyping.relevance_of_type env sigma t' in
let sigma, b' =
Option.cata (fun x -> on_snd (fun x -> Some (fst x)) @@
interp_casted_constr_evars_impls ~program_mode:false env sigma ~impls x t') (sigma,None) b in
let impls =
match i with
| Anonymous -> impls
| Name id -> Id.Map.add id (compute_internalization_data env sigma Constrintern.Method t' impl) impls
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) no;
(EConstr.push_rel d env, sigma, impl :: uimpls, d::params, impls))
(env, sigma, [], [], impls_env) nots l
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 (univ_of_sort s) univ
else univ
in (EConstr.push_rel d env, univ))
l (env, Univ.Universe.sprop)
let binder_of_decl = function
| Vernacexpr.AssumExpr(n,t) -> (n,None,t)
| Vernacexpr.DefExpr(n,c,t) ->
(n,Some c, match t with Some c -> c
| None -> CAst.make ?loc:n.CAst.loc @@ CHole (None, Namegen.IntroAnonymous, None))
let binders_of_decls = List.map binder_of_decl
let check_anonymous_type ind =
match ind with
| { CAst.v = CSort (Glob_term.GType []) } -> true
| _ -> false
let typecheck_params_and_fields finite def poly pl ps records =
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
let env0 = if not poly && is_template then Environ.set_universes_lbound env0 Univ.Level.prop else env0 in
let sigma, decl = Constrexpr_ops.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.GType []) } -> 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 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 env_ar = EConstr.push_rel_context newps (List.fold_left3 fold env0 records arities relevances) in
let assums = List.filter is_local_assum newps in
let impls_env =
let params = List.map (RelDecl.get_name %> Name.get_id) assums in
let ty = Inductive (params, (finite != Declarations.BiFinite)) in
let ids = List.map (fun (id, _, _, _) -> id) records in
let imps = List.map (fun _ -> imps) arities in
compute_internalization_env env0 sigma ~impls:impls_env ty ids arities imps
in
let fold sigma (_, _, nots, fs) arity =
let _, sigma, impls, newfs, _ = interp_fields_evars env_ar sigma impls_env nots (binders_of_decls fs) in
(sigma, (impls, newfs))
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
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)
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 (Evd.from_env env0) sigma (EConstr.of_constr t) in
let () = List.iter (iter_constr ce) (List.rev newps) in
ubinders, univs, template, newps, imps, 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 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" 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 *)
let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers 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
| 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 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 lifted_fields = Termops.lift_rel_context 1 fields in
let primitive =
match mib.mind_record with
| PrimRecord _ -> true
| FakeRecord | NotRecord -> false
in
let (_,_,kinds,sp_projs,_) =
List.fold_left3
(fun (nfi,i,kinds,sp_projs,subst) coe 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 kn, term =
if is_local_assum decl && primitive then
let p = Projection.Repr.make indsp
~proj_npars:mib.mind_nparams
~proj_arg:i
(Label.of_id fid)
in
(* Already defined by declare_mind silently *)
let kn = Projection.Repr.constant p in
Declare.definition_message fid;
kn, mkProj (Projection.make p false,mkRel 1)
else
let ccl = subst_projection fid subst ti in
let body = match decl with
| LocalDef (_,ci,_) -> subst_projection fid subst ci
| LocalAssum ({binder_relevance=rci},_) ->
(* [ccl] is defined in context [params;x:rp] *)
(* [ccl'] is defined in context [params;x:rp;x:rp] *)
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 have no is *)
mkCase (ci, p, mkRel 1, [|branch|])
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
try
let entry = {
const_entry_body =
Future.from_val (Safe_typing.mk_pure_proof proj);
const_entry_secctx = None;
const_entry_type = Some projtyp;
const_entry_universes = ctx;
const_entry_opaque = false;
const_entry_inline_code = false;
const_entry_feedback = None } in
let k = (DefinitionEntry entry,IsDefinition kind) in
let kn = declare_constant ~internal:InternalTacticRequest fid k in
let constr_fip =
let proj_args = (*Rel 1 refers to "x"*) paramargs@[mkRel 1] in
applist (mkConstU (kn,u),proj_args)
in
Declare.definition_message fid;
kn, constr_fip
with Type_errors.TypeError (ctx,te) ->
raise (NotDefinable (BadTypedProj (fid,ctx,te)))
in
let refi = ConstRef kn in
Impargs.maybe_declare_manual_implicits false refi impls;
if coe then begin
let cl = Class.class_of_global (IndRef indsp) in
Class.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 ->
warning_or_error coe indsp why;
(None::sp_projs,i,NoProjection fi::subst) in
(nfi-1,i,(fi, is_local_assum decl)::kinds,sp_projs,subst))
(List.length fields,0,[],[],[]) coers (List.rev fields) (List.rev fieldimpls)
in (kinds,sp_projs)
open Typeclasses
let declare_structure ~cum finite ubinders univs paramimpls params template ?(kind=StructureComponent) ?name record_data =
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 variance = if poly && cum then Some (InferCumulativity.dummy_variance ctx) else None in
let binder_name =
match name with
| None ->
let map (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 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
let template =
let template_candidate () =
ComInductive.template_polymorphism_candidate (Global.env ()) 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");
if template && not (template_candidate ()) then
user_err Pp.(strbrk "record cannot be made template polymorphic on any universe");
template
| None, template ->
(* auto detect template *)
ComInductive.should_auto_template id (template && template_candidate ())
in
{ mind_entry_typename = id;
mind_entry_arity = arity;
mind_entry_template = template;
mind_entry_consnames = [idbuild];
mind_entry_lc = [type_constructor] }
in
let blocks = List.mapi mk_block record_data in
let primitive =
!primitive_flag &&
List.for_all (fun (_,_,_,_,_,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_variance = variance;
}
in
let mie = InferCumulativity.infer_inductive (Global.env ()) mie in
let impls = List.map (fun _ -> paramimpls, []) record_data in
let kn = ComInductive.declare_mutual_inductive_with_eliminations mie ubinders impls
~primitive_expected:!primitive_flag
in
let map i (_, _, _, _, fieldimpls, fields, is_coe, 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 = ConstructRef cstr in
let () = if is_coe then Class.try_add_new_coercion build ~local:false poly in
let () = Recordops.declare_structure(cstr, List.rev kinds, List.rev sp_projs) in
rsp
in
List.mapi map record_data
let implicits_of_context ctx =
List.map_i (fun i name ->
let explname =
match name with
| Name n -> Some n
| Anonymous -> None
in ExplByPos (i, explname), (true, true, true))
1 (List.rev (Anonymous :: (List.map RelDecl.get_name ctx)))
let declare_class def cum ubinders univs id idbuild paramimpls params univ arity
template fieldimpls fields ?(kind=StructureComponent) coers priorities =
let fieldimpls =
(* Make the class implicit in the projections, and the params if applicable. *)
let len = List.length params in
let impls = implicits_of_context params in
List.map (fun x -> impls @ Impargs.lift_implicits (succ len) x) fieldimpls
in
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 ->
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 id
(DefinitionEntry class_entry, 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 proj_name
(DefinitionEntry proj_entry, IsDefinition Definition)
in
let cref = ConstRef cst in
Impargs.declare_manual_implicits false cref paramimpls;
Impargs.declare_manual_implicits false (ConstRef proj_cst) (List.hd fieldimpls);
Classes.set_typeclass_transparency (EvalConstRef cst) false false;
let sub = match List.hd coers with
| Some b -> Some ((if b then Backward else Forward), List.hd priorities)
| None -> None
in
[cref, [Name proj_name, sub, Some proj_cst]]
| _ ->
let record_data = [id, idbuild, univ, arity, fieldimpls, fields, false, List.map (fun _ -> false) fields] in
let inds = declare_structure ~cum Declarations.BiFinite ubinders univs paramimpls
params template ~kind:Method ~name:[|binder_name|] record_data
in
let coers = List.map2 (fun coe pri ->
Option.map (fun b ->
if b then Backward, pri else Forward, pri) coe)
coers priorities
in
let map ind =
let l = List.map3 (fun decl b y -> RelDecl.get_name decl, b, y)
(List.rev fields) coers (Recordops.lookup_projections ind)
in IndRef ind, l
in
List.map map inds
in
let ctx_context =
List.map (fun decl ->
match Typeclasses.class_of_constr Evd.empty (EConstr.of_constr (RelDecl.get_type decl)) with
| Some (_, ((cl,_), _)) -> Some cl.cl_impl
| None -> None)
params, params
in
let univs, ctx_context, 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 ctx_context = on_snd (fun d -> Context.Rel.map map d) ctx_context in
auctx, ctx_context, fields
| Monomorphic_entry _ ->
Univ.AUContext.empty, ctx_context, fields
in
let map (impl, projs) =
let k =
{ cl_univs = univs;
cl_impl = impl;
cl_strict = !typeclasses_strict;
cl_unique = !typeclasses_unique;
cl_context = ctx_context;
cl_props = fields;
cl_projs = projs }
in
add_class k; impl
in
List.map map data
let add_constant_class env cst =
let ty, univs = Typeops.type_of_global_in_context env (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 = ConstRef cst;
cl_context = (List.map (const None) ctx, ctx);
cl_props = [LocalAssum (make_annot Anonymous r, t)];
cl_projs = [];
cl_strict = !typeclasses_strict;
cl_unique = !typeclasses_unique
}
in add_class tc;
set_typeclass_transparency (EvalConstRef cst) false false
let add_inductive_class env 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 env = push_context ~strict:false (Univ.AUContext.repr univs) env in
let env = push_rel_context ctx env in
let inst = Univ.make_abstract_instance univs in
let ty = Inductive.type_of_inductive env ((mind, oneind), inst) in
let r = Inductive.relevance_of_inductive env ind in
{ cl_univs = univs;
cl_impl = IndRef ind;
cl_context = List.map (const None) ctx, ctx;
cl_props = [LocalAssum (make_annot Anonymous r, ty)];
cl_projs = [];
cl_strict = !typeclasses_strict;
cl_unique = !typeclasses_unique }
in add_class 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
if Typeclasses.is_class g then warn_already_existing_class g
else
match g with
| ConstRef x -> add_constant_class env x
| IndRef x -> add_inductive_class env x
| _ -> user_err ~hdr:"declare_existing_class"
(Pp.str"Unsupported class type, only constants and inductives are allowed")
open Vernacexpr
let check_unique_names records =
let extract_name acc (((_, bnd), _), _) = match bnd 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
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 (_, _, _, cfs, _, _) =
List.exists (fun ((_, pri), _) -> not (Option.is_empty pri)) 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 (fun (((_, f), _), _) -> f) cfs in
id.CAst.v, s, List.map snd cfs, fs
in
let data = List.map map records in
let pss = List.map (fun (_, _, ps, _, _, _) -> ps) 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
(* [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 cum 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 =
States.with_state_protection (fun () ->
typecheck_params_and_fields finite (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
| [r], [d] -> r, d
| _, _ -> CErrors.user_err (str "Mutual definitional classes are not handled")
in
let priorities = List.map (fun ((_, id), _) -> {hint_priority = id; hint_pattern = None}) cfs in
let coers = List.map (fun (((coe, _), _), _) -> coe) cfs in
declare_class def cum ubinders univs id.CAst.v idbuild
implpars params univ arity template implfs fields coers priorities
| _ ->
let map impls = implpars @ Impargs.lift_implicits (succ (List.length params)) 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 coers = List.map (fun (((coe, _), _), _) -> coe) cfs in
let coe = List.map (fun coe -> not (Option.is_empty coe)) coers in
id.CAst.v, idbuild, univ, arity, implfs, fields, is_coe, coe
in
let data = List.map2 map data records in
let inds = declare_structure ~cum finite ubinders univs implpars params template data in
List.map (fun ind -> IndRef ind) inds
[ Dauer der Verarbeitung: 0.14 Sekunden
(vorverarbeitet)
]
|
