aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/record.ml
blob: 93429da5ace789a9cadab370d950f844c95fb26d (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

open Pp
open Errors
open Util
open Names
open Globnames
open Nameops
open Term
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 Sigma.Notations
open Context.Rel.Declaration
open Entries

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

(** Flag governing use of primitive projections. Disabled by default. *)
let primitive_flag = ref false
let _ =
  declare_bool_option
    { optsync  = true;
      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
    { optsync  = true;
      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
    { optsync  = true;
      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 evars impls_env nots l =
  List.fold_left2
    (fun (env, uimpls, params, impls) no ((loc, i), b, t) ->
      let t', impl = interp_type_evars_impls env evars ~impls t in
      let b' = Option.map (fun x -> fst (interp_casted_constr_evars_impls env evars ~impls x t')) b in
      let impls =
	match i with
	| Anonymous -> impls
	| Name id -> Id.Map.add id (compute_internalization_data env Constrintern.Method t' impl) impls
      in
      let d = match b' with
	      | None -> LocalAssum (i,t')
	      | Some b' -> LocalDef (i,b',t')
      in
      List.iter (Metasyntax.set_notation_for_interpretation impls) no;
      (push_rel d env, impl :: uimpls, d::params, impls))
    (env, [], [], 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 (get_type d) in
	  Univ.sup (univ_of_sort s) univ 
      else univ
    in (push_rel d env, univ)) 
    l (env, Univ.type0m_univ)

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 -> CHole (fst n, None, Misctypes.IntroAnonymous, None))

let binders_of_decls = List.map binder_of_decl

let typecheck_params_and_fields def id pl t ps nots fs =
  let env0 = Global.env () in
  let ctx = Evd.make_evar_universe_context env0 pl in
  let evars = ref (Evd.from_ctx ctx) in
  let _ = 
    let error bk (loc, name) = 
      match bk, name with
      | Default _, Anonymous ->
        user_err_loc (loc, "record", str "Record parameters must be named")
      | _ -> ()
    in
      List.iter 
	(function LocalRawDef (b, _) -> error default_binder_kind b
	   | LocalRawAssum (ls, bk, ce) -> List.iter (error bk) ls) ps
  in 
  let impls_env, ((env1,newps), imps) = interp_context_evars env0 evars ps in
  let t', template = match t with 
    | Some t -> 
       let env = push_rel_context newps env0 in
       let s = interp_type_evars env evars ~impls:empty_internalization_env t in
       let sred = Reductionops.whd_betadeltaiota env !evars s in
	 (match kind_of_term sred with
	 | Sort s' -> 
	   (match Evd.is_sort_variable !evars s' with
	   | Some l -> evars := Evd.make_flexible_variable !evars true l; 
	     sred, true
	   | None -> s, false)
	 | _ -> user_err_loc (constr_loc t,"", str"Sort expected."))
    | None -> 
      let uvarkind = Evd.univ_flexible_alg in
	mkSort (Evarutil.evd_comb0 (Evd.new_sort_variable uvarkind) evars), true
  in
  let fullarity = it_mkProd_or_LetIn t' newps in
  let env_ar = push_rel_context newps (push_rel (LocalAssum (Name id,fullarity)) env0) in
  let env2,impls,newfs,data =
    interp_fields_evars env_ar evars impls_env nots (binders_of_decls fs)
  in
  let sigma = 
    Pretyping.solve_remaining_evars Pretyping.all_and_fail_flags env_ar !evars (Evd.empty,!evars) in
  let evars, nf = Evarutil.nf_evars_and_universes sigma in
  let arity = nf t' in
  let arity, evars = 
    let _, univ = compute_constructor_level evars env_ar newfs in
    let ctx, aritysort = Reduction.dest_arity env0 arity in
      assert(List.is_empty ctx); (* Ensured by above analysis *)
      if not def && (Sorts.is_prop aritysort || 
	(Sorts.is_set aritysort && is_impredicative_set env0)) then
	arity, evars
      else
	let evars = Evd.set_leq_sort env_ar evars (Type univ) aritysort in
	if Univ.is_small_univ univ &&
	   Option.cata (Evd.is_flexible_level evars) false (Evd.is_sort_variable evars aritysort) then
	   (* We can assume that the level in aritysort is not constrained
	       and clear it, if it is flexible *)
	  mkArity (ctx, Sorts.sort_of_univ univ),
	  Evd.set_eq_sort env_ar evars (Prop Pos) aritysort
	else arity, evars
  in
  let evars, nf = Evarutil.nf_evars_and_universes evars in
  let newps = Context.Rel.map nf newps in
  let newfs = Context.Rel.map nf newfs in
  let ce t = Pretyping.check_evars env0 Evd.empty evars t in
    List.iter (iter_constr ce) (List.rev newps);
    List.iter (iter_constr ce) (List.rev newfs);
    Evd.universe_context ?names:pl evars, nf arity, template, imps, newps, impls, newfs

let degenerate_decl decl =
  let id = match get_name decl with
    | Name id -> id
    | Anonymous -> anomaly (Pp.str "Unnamed record variable") in
  match decl with
    | LocalAssum (_,t) -> (id, LocalAssumEntry t)
    | LocalDef (_,b,_) -> (id, LocalDefEntry b)

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

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
        (pr_id fi ++
	   strbrk" cannot be defined because the projection" ++ str s ++ spc () ++
           prlist_with_sep pr_comma pr_id projs ++ spc () ++ str have ++
	   strbrk " not defined.")
    | BadTypedProj (fi,ctx,te) ->
	match te with
	  | ElimArity (_,_,_,_,Some (_,_,NonInformativeToInformative)) ->
              (pr_id fi ++
		strbrk" cannot be defined because it is informative and " ++
		Printer.pr_inductive (Global.env()) indsp ++
		strbrk " is not.")
	  | ElimArity (_,_,_,_,Some (_,_,StrongEliminationOnNonSmallType)) ->
	      (pr_id fi ++
		strbrk" cannot be defined because it is large and " ++
		Printer.pr_inductive (Global.env()) indsp ++
		strbrk " is not.")
	  | _ ->
              (pr_id fi ++ strbrk " cannot be defined because it is not typable.")
  in
  if coe then errorlabstrm "structure" st;
  Flags.if_verbose msg_warning (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 kind_of_term 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 ->
                errorlabstrm "" (str "Field " ++ pr_id fid ++
                  str " depends on the " ++ pr_nth (k-depth-1) ++ str
                  " field which has no name.")
        else
	  mkRel (k-lv)
    | _ -> map_constr_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 indu paramdecls fields =
  let subst = List.map_i (fun i _ -> mkRel i) 1 paramdecls in
  Termops.substl_rel_context (subst@[mkIndU indu]) fields

(* We build projections *)
let declare_projections indsp ?(kind=StructureComponent) binder_name coers fieldimpls fields =
  let env = Global.env() in
  let (mib,mip) = Global.lookup_inductive indsp in
  let u = Declareops.inductive_instance mib in
  let paramdecls = Inductive.inductive_paramdecls (mib, u) in
  let poly = mib.mind_polymorphic in
  let ctx = Univ.instantiate_univ_context mib.mind_universes in
  let indu = indsp, u in
  let r = mkIndU (indsp,u) in
  let rp = applist (r, Context.Rel.to_extended_list 0 paramdecls) in
  let paramargs = Context.Rel.to_extended_list 1 paramdecls in (*def in [[params;x:rp]]*)
  let x = Name binder_name in
  let fields = instantiate_possibly_recursive_type indu paramdecls fields in
  let lifted_fields = Termops.lift_rel_context 1 fields in
  let primitive = 
    if !primitive_flag then 
      let is_primitive = 
	match mib.mind_record with
	| Some (Some _) -> true
	| Some None | None -> false
      in
	if not is_primitive then 
	  Flags.if_verbose msg_warning
	    (hov 0 (str "The record " ++ Printer.pr_inductive env indsp ++ 
		      str" could not be defined as a primitive record"));
	is_primitive
    else false
  in
  let (_,_,kinds,sp_projs,_) =
    List.fold_left3
      (fun (nfi,i,kinds,sp_projs,subst) coe decl impls ->
        let fi = get_name decl in
        let ti = 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
		(** Already defined in the kernel silently *)
		let kn = destConstRef (Nametab.locate (Libnames.qualid_of_ident fid)) in
		  Declare.definition_message fid;
		  kn, mkProj (Projection.make kn 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 _ ->
	            (* [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 LetStyle in
		      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_polymorphic = poly;
		    const_entry_universes =
		      if poly then ctx else Univ.UContext.empty;
		    const_entry_opaque = false;
		    const_entry_inline_code = false;
		    const_entry_feedback = None } in
		  let k = (DefinitionEntry entry,IsDefinition kind) in
		  let kn = declare_constant ~internal: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)

let structure_signature ctx =
  let rec deps_to_evar evm l =
    match l with [] -> Evd.empty
      | [decl] ->
        let env = Environ.empty_named_context_val in
        let evm = Sigma.Unsafe.of_evar_map evm in
        let Sigma (_, evm, _) = Evarutil.new_pure_evar env evm (get_type decl) in
        let evm = Sigma.to_evar_map evm in
        evm
      | decl::tl ->
          let env = Environ.empty_named_context_val in
          let evm = Sigma.Unsafe.of_evar_map evm in
          let Sigma (ev, evm, _) = Evarutil.new_pure_evar env evm (get_type decl) in
          let evm = Sigma.to_evar_map evm in
	  let new_tl = Util.List.map_i
	    (fun pos decl ->
	       map_type (fun t -> Termops.replace_term (mkRel pos) (mkEvar(ev,[||])) t) decl) 1 tl in
	  deps_to_evar evm new_tl in
  deps_to_evar Evd.empty (List.rev ctx)

open Typeclasses

let declare_structure finite poly ctx id idbuild paramimpls params arity template 
    fieldimpls fields ?(kind=StructureComponent) ?name is_coe coers sign =
  let nparams = List.length params and nfields = List.length fields in
  let args = Context.Rel.to_extended_list nfields params in
  let ind = applist (mkRel (1+nparams+nfields), args) in
  let type_constructor = it_mkProd_or_LetIn ind fields in
  let binder_name = 
    match name with
    | None -> Id.of_string (Unicode.lowercase_first_char (Id.to_string id)) 
    | Some n -> n
  in
  let mie_ind =
    { mind_entry_typename = id;
      mind_entry_arity = arity;
      mind_entry_template = not poly && template;
      mind_entry_consnames = [idbuild];
      mind_entry_lc = [type_constructor] }
  in
  let mie =
    { mind_entry_params = List.map degenerate_decl params;
      mind_entry_record = Some (if !primitive_flag then Some binder_name else None);
      mind_entry_finite = finite;
      mind_entry_inds = [mie_ind];
      mind_entry_polymorphic = poly;
      mind_entry_private = None;
      mind_entry_universes = ctx } in
  let kn = Command.declare_mutual_inductive_with_eliminations mie [] [(paramimpls,[])] in
  let rsp = (kn,0) in (* This is ind path of idstruc *)
  let cstr = (rsp,1) in
  let kinds,sp_projs = declare_projections rsp ~kind binder_name coers fieldimpls fields in
  let build = ConstructRef cstr in
  let () = if is_coe then Class.try_add_new_coercion build ~local:false poly in
  Recordops.declare_structure(rsp,cstr,List.rev kinds,List.rev sp_projs);
  rsp

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 get_name ctx)))

let declare_class finite def poly ctx id idbuild paramimpls params arity 
    template fieldimpls fields ?(kind=StructureComponent) is_coe coers priorities sign =
  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 (snd id) (Termops.ids_of_context (Global.env())) in
  let impl, projs =
    match fields with
    | [LocalAssum (Name proj_name, field) | LocalDef (Name proj_name, _, field)] when def ->
      let class_body = it_mkLambda_or_LetIn field params in
      let class_type = it_mkProd_or_LetIn arity params in
      let class_entry = 
	Declare.definition_entry ~types:class_type ~poly ~univs:ctx class_body in
      let cst = Declare.declare_constant (snd id)
	(DefinitionEntry class_entry, IsDefinition Definition)
      in
      let cstu = (cst, if poly then Univ.UContext.instance ctx else Univ.Instance.empty) in
      let inst_type = appvectc (mkConstU cstu)
			       (Termops.rel_vect 0 (List.length params)) in
      let proj_type =
	it_mkProd_or_LetIn (mkProd(Name binder_name, inst_type, lift 1 field)) params in
      let proj_body =
	it_mkLambda_or_LetIn (mkLambda (Name binder_name, inst_type, mkRel 1)) params in
      let proj_entry =
	Declare.definition_entry ~types:proj_type ~poly
	    ~univs:(if poly then ctx else Univ.UContext.empty) proj_body
      in
      let proj_cst = Declare.declare_constant proj_name
        (DefinitionEntry proj_entry, IsDefinition Definition)
      in
      let cref = ConstRef cst in
      Impargs.declare_manual_implicits false cref [paramimpls];
      Impargs.declare_manual_implicits false (ConstRef proj_cst) [List.hd fieldimpls];
      Classes.set_typeclass_transparency (EvalConstRef cst) false false;
      let sub = match List.hd coers with
	| Some b -> Some ((if b then Backward else Forward), List.hd priorities) 
	| None -> None 
      in
      cref, [Name proj_name, sub, Some proj_cst]
    | _ ->
       let ind = declare_structure BiFinite poly ctx (snd id) idbuild paramimpls
	  params arity template fieldimpls fields
	  ~kind:Method ~name:binder_name false (List.map (fun _ -> false) fields) sign
       in
       let coers = List.map2 (fun coe pri -> 
			      Option.map (fun b -> 
			      if b then Backward, pri else Forward, pri) coe)
	  coers priorities
       in
       let l = List.map3 (fun decl b y -> get_name decl, b, y)
         (List.rev fields) coers (Recordops.lookup_projections ind)
       in IndRef ind, l
  in
  let ctx_context =
    List.map (fun decl ->
      match Typeclasses.class_of_constr (get_type decl) with
      | Some (_, ((cl,_), _)) -> Some (cl.cl_impl, true)
      | None -> None)
      params, params
  in
  let k =
    { 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


let add_constant_class cst =
  let ty = Universes.unsafe_type_of_global (ConstRef cst) in
  let ctx, arity = decompose_prod_assum ty in
  let tc = 
    { cl_impl = ConstRef cst;
      cl_context = (List.map (const None) ctx, ctx);
      cl_props = [LocalAssum (Anonymous, arity)];
      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 ind =
  let mind, oneind = Global.lookup_inductive ind in
  let k =
    let ctx = oneind.mind_arity_ctxt in
    let inst = Univ.UContext.instance mind.mind_universes in
    let map = function
    | LocalDef _ -> None
    | LocalAssum (_, t) -> Some (lazy t)
    in
    let args = List.map_filter map ctx in
    let ty = Inductive.type_of_inductive_knowing_parameters
      (push_rel_context ctx (Global.env ()))
      ((mind,oneind),inst)
      (Array.of_list args)
    in
      { cl_impl = IndRef ind;
	cl_context = List.map (const None) ctx, ctx;
	cl_props = [LocalAssum (Anonymous, ty)];
	cl_projs = [];
	cl_strict = !typeclasses_strict;
	cl_unique = !typeclasses_unique }
  in add_class k

let declare_existing_class g =
  match g with
  | ConstRef x -> add_constant_class x
  | IndRef x -> add_inductive_class x
  | _ -> user_err_loc (Loc.dummy_loc, "declare_existing_class", 
		      Pp.str"Unsupported class type, only constants and inductives are allowed")

open Vernacexpr

(* [fs] corresponds to fields and [ps] to parameters; [coers] is a
   list telling if the corresponding fields must me declared as coercions 
   or subinstances *)
let definition_structure (kind,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cfs,idbuild,s) =
  let cfs,notations = List.split cfs in
  let cfs,priorities = List.split cfs in
  let coers,fs = List.split cfs in
  let extract_name acc = function
      Vernacexpr.AssumExpr((_,Name id),_) -> id::acc
    | Vernacexpr.DefExpr ((_,Name id),_,_) -> id::acc
    | _ -> acc in
  let allnames =  idstruc::(List.fold_left extract_name [] fs) in
  if not (List.distinct_f Id.compare allnames)
  then error "Two objects have the same name";
  let isnot_class = match kind with Class false -> false | _ -> true in
  if isnot_class && List.exists (fun opt -> not (Option.is_empty opt)) priorities then
    error "Priorities only allowed for type class substructures";
  (* Now, younger decl in params and fields is on top *)
  let (pl, ctx), arity, template, implpars, params, implfs, fields =
    States.with_state_protection (fun () ->
      typecheck_params_and_fields (kind = Class true) idstruc pl s ps notations fs) () in
  let sign = structure_signature (fields@params) in
  let gr = match kind with
    | Class def ->
	let gr = declare_class finite def poly ctx (loc,idstruc) idbuild
	  implpars params arity template implfs fields is_coe coers priorities sign in
	gr
    | _ ->
	let implfs = List.map
	  (fun impls -> implpars @ Impargs.lift_implicits
	    (succ (List.length params)) impls) implfs in
	let ind = declare_structure finite poly ctx idstruc 
	  idbuild implpars params arity template implfs 
	  fields is_coe (List.map (fun coe -> not (Option.is_empty coe)) coers) sign in
	IndRef ind
  in
  Universes.register_universe_binders gr pl;
  gr