aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/class.ml
blob: f8b84b7b6e94843344ebabce81dda540947f1d64 (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

(* $Id$ *)

open Util
open Pp
open Names
open Generic
open Term
open Inductive
open Constant
open Environ
open Lib
open Classops
open Declare

(* manipulations concernant les strength *)

(* gt dans le sens de "longueur du sp" (donc le moins persistant) *)

(* strength * strength -> bool *)

let stre_gt = function
  | (NeverDischarge,NeverDischarge) -> false
  | (NeverDischarge,x) -> false
  | (x,NeverDischarge) -> true
  | (DischargeAt sp1,DischargeAt sp2) -> sp_gt (sp1,sp2) 

let stre_max (stre1,stre2) =
  if stre_gt (stre1,stre2) then stre1 else stre2

let stre_max4 stre1 stre2 stre3 stre4 =
  stre_max ((stre_max (stre1,stre2)),(stre_max (stre3,stre4)))

let id_of_varid = function
  | VAR id -> id
  | _ -> anomaly "class__id_of_varid"

let stre_of_VAR c = variable_strength (destVar c)

(* lf liste des variable dont depend la coercion f
   lc liste des variable dont depend la classe source *)

let rec stre_unif_cond = function
  | ([],[]) -> NeverDischarge
  | (v::l,[]) -> stre_of_VAR v
  | ([],v::l) -> stre_of_VAR v
  | (v1::l1,v2::l2) ->
      if v1=v2 then 
	stre_unif_cond (l1,l2)
      else
	let stre1 = (stre_of_VAR v1)
	and stre2 = (stre_of_VAR v2) in 
	stre_max (stre1,stre2)

let stre_of_coe = function
  | NAM_SP sp ->
      (match global_operator sp (basename sp) with
	 | Const sp, _ -> constant_strength sp
	 | _ -> NeverDischarge)
  | NAM_Var id -> variable_strength id
  | _ -> NeverDischarge
	
(* try_add_class : Names.identifier ->
  Term.constr -> (cl_typ * int) option -> bool -> int * Libobject.strength *)

let try_add_class id v clpopt streopt check_exist = 
  let env = Global.env () in
  let t = Retyping.get_type_of env Evd.empty v in
  let p1 =
    try 
      arity_sort t 
    with Not_found -> 
      errorlabstrm "try_add_class" 
        [< 'sTR "Type of "; 'sTR (string_of_id id);
           'sTR " does not end with a sort" >] 
  in
  let cl,p =
    match clpopt with
      | None -> let (cl,_)=constructor_at_head v in (cl,p1)
      | Some (cl,p2) -> (fully_applied id p2 p1;cl,p1) 
  in
  if check_exist & class_exists cl then
    errorlabstrm "try_add_new_class" 
      [< 'sTR (string_of_id id) ; 'sTR " is already a class" >];
  let stre' = stre_of_cl cl in 
  let stre = match streopt with
    | Some stre -> stre_max (stre,stre')
    | None -> stre'
  in
  add_new_class (cl,(string_of_id id),stre,p);
  stre

(* try_add_new_class : Names.identifier -> unit *)

let try_add_new_class id stre =
  let v = global_reference CCI id in
  let _ = try_add_class id v None (Some stre) true in () 

(* check_class : Names.identifier ->
  Term.constr -> cl_typ -> int -> int * Libobject.strength *)

let check_class id v cl p =
  try 
    let _,clinfo = class_info cl in
    if p = clinfo.cL_PARAM then 
      clinfo.cL_STRE
    else 
      errorlabstrm "fully_applied" 
	[< 'sTR"Wrong number of parameters for ";'sTR(string_of_id id) >]
  with Not_found -> 
    try_add_class id v (Some (cl,p)) None false


(* decomposition de constr vers coe_typ *)

let coe_constructor_at_head t = 
  let rec aux t' =
    match kind_of_term t' with
      | IsConst (sp,l) -> (Array.to_list l),NAM_SP sp
      | IsMutInd ((sp,_),l) -> (Array.to_list l),NAM_SP sp
      | IsVar id  -> [],NAM_Var id
      | IsCast (c,_) -> aux c
      | IsMutConstruct (cstr_sp,l) -> (Array.to_list l),NAM_Construct cstr_sp
      | IsAppL(f,args) -> aux f
      |  _ -> raise Not_found
  in 
  aux (collapse_appl t)

let constructor_at_head1 t = 
  let rec aux t' =
    match kind_of_term t' with
      | IsConst (sp,l) -> t',[],(Array.to_list l),CL_SP sp,0
      | IsMutInd (ind_sp,l) -> t',[],(Array.to_list l),CL_IND ind_sp,0
      | IsVar id -> t',[],[],CL_Var id,0
      | IsCast (c,_) -> aux c
      | IsAppL(f,args) -> 
	  let t',_,l,c,_ = aux f in t',args,l,c,List.length args
      | IsProd (_,_,_) -> t',[],[],CL_FUN,0
      | IsSort _ -> t',[],[],CL_SORT,0
      |  _ -> raise Not_found
  in 
  aux (collapse_appl t)


(* condition d'heritage uniforme *)

let uniform_cond nargs lt = 
  let rec aux = function
    | (0,[]) -> true
    | (n,t::l) -> (strip_outer_cast t = Rel n) & (aux ((n-1),l))
    | _ -> false
  in 
  aux (nargs,lt)

let id_of_cl  = function
  | CL_FUN -> (id_of_string "FUNCLASS")
  | CL_SORT -> (id_of_string "SORTCLASS") 
  | CL_SP sp -> (basename sp)
  | CL_IND (sp,i) ->
      (mind_nth_type_packet (Global.lookup_mind sp) i).mind_typename
  | CL_Var id -> id 
	
let string_of_cl  = function
  | CL_FUN -> "FUNCLASS"
  | CL_SORT -> "SORTCLASS" 
  | CL_SP sp -> string_of_id (basename sp)
  | CL_IND (sp,i) ->
      string_of_id
	(mind_nth_type_packet (Global.lookup_mind sp) i).mind_typename
  | CL_Var id -> string_of_id id 

(* 
lp est la liste (inverse'e) des arguments de la coercion
ids est le nom de la classe source
sps_opt est le sp de la classe source dans le cas des structures
retourne:
la classe souce
nbre d'arguments de la classe
le constr de la class
l'indice de la classe source dans la liste lp
la liste des variables dont depend la classe source
*)

type choice = Ident of identifier | Section_path of section_path

let get_source lp source =
  let aux test =
    let rec aux1 n = function
      | [] -> raise Not_found
      | t1::lt ->
	  try 
	    let v1,lv1,l,cl1,p1 = constructor_at_head1 t1 in
            if test cl1 then 
	      cl1,p1,v1,lv1,n,l
            else 
	      aux1 (n+1) lt
          with _ -> 
	    aux1 (n + 1) lt
    in 
    aux1 1 lp
  in 
  match source with
    | None ->
	let (v1,lv1,l,cl1,p1) as x =
	  match lp with
	    | [] -> raise Not_found
            | t1::_ ->
		try constructor_at_head1 t1
                with _ -> raise Not_found
        in 
	(id_of_cl cl1),(cl1,p1,v1,lv1,1,l)
    | Some (Ident id) -> 
	id, aux (function cl -> id_of_cl cl = id)
    | Some (Section_path sp) ->
	basename sp,
	aux (function
	       | CL_SP sp1 -> sp=sp1
	       | CL_IND (sp1,i) -> sp=sp1
               | _ -> false)

let get_target t ind =
  if (ind > 1) then 
    CL_FUN,0,t
  else 
    let v2,_,_,cl2,p2 = constructor_at_head1 t in cl2,p2,v2

let prods_of t = 
  let rec aux acc = function
    | DOP2(Prod,c1,DLAM(_,c2)) -> aux (c1::acc) c2
    | (DOP2(Cast,c,_)) -> aux acc c
    | t -> t::acc
  in 
  aux [] t

(* coercion identite' *)

let lams_of t = 
  let rec aux acc = function
    | DOP2(Lambda,c1,DLAM(x,c2)) -> aux ((x,c1)::acc) c2
    | DOP2(Cast,c,_) -> aux acc c
    | t -> acc,t
  in 
  aux [] t

let build_id_coercion idf_opt ids =
  let env = Global.env () in
  let vs = construct_reference env CCI ids in 
  let c = match (strip_outer_cast vs) with
    | (DOPN(Const sp,l) as c') when Environ.evaluable_constant env c' ->
	(try Instantiate.constant_value env c'
         with _ -> errorlabstrm "build_id_coercion"
             [< 'sTR(string_of_id ids);
		'sTR" must be a transparent constant" >])
    | _ -> 
	errorlabstrm "build_id_coercion"
          [< 'sTR(string_of_id ids); 
	     'sTR" must be a transparent constant" >] 
  in
  let lams,t = lams_of c in
  let lams = List.rev lams in
  let llams = List.length lams in
  let val_f =
    List.fold_right
      (fun (x,t) u -> DOP2(Lambda,t,DLAM(x,u)))
      lams
      (DOP2(Lambda,(applistc vs (rel_list 0 llams)),
	    DLAM(Name (id_of_string "x"),Rel 1))) 
  in
  let typ_f =
    List.fold_right
      (fun (x,t) c -> DOP2(Prod,t,DLAM(x,c)))
      lams
      (DOP2(Prod,(applistc vs (rel_list 0 llams)),
	    DLAM(Anonymous,lift 1 t))) 
  in 
  let constr_f = DOP2(Cast,val_f,typ_f) in
  (* juste pour verification *)
  let _ = 
    try 
      Typing.type_of env Evd.empty constr_f
    with _ -> 
      error ("cannot be defined as coercion - "^
	     "may be a bad number of arguments") 
  in
  let idf =
    match idf_opt with
      | Some(idf) -> idf
      | None ->
	  id_of_string ("Id_"^(string_of_id ids)^"_"^
                        (string_of_cl (fst (constructor_at_head t)))) 
  in
  let constr_entry = 
    { const_entry_body = Cooked constr_f; const_entry_type = None } in
  declare_constant idf (constr_entry,NeverDischarge);
  idf

let coercion_syntax_entry id n =
  let args = (String.concat " " (list_tabulate (fun _ -> "$_") n)) ^ " $c" in
  let str = "level 10: " ^ (string_of_id id) ^
            " [ <<(" ^ (string_of_id id) ^ " " ^ args ^ ")>> ]" ^
            " -> [ (APPLIST $c):E ]"
  in
  try
    let se = Pcoq.parse_string Pcoq.Prim.syntax_entry_eoi str in
    Metasyntax.add_syntax_obj "constr" [se]
  with Stdpp.Exc_located _ -> 
    anomaly ("ill-formed syntax entry: "^str)

let fun_coercion_syntax_entry id n =
  let args =
    if n<0 then anomaly "fun_coercion_syntax_entry";
    String.concat " " (list_tabulate (fun _ -> "$_") n) ^ " $c ($LIST $l)" 
  in
  let str = "level 10: " ^ ((string_of_id id)^"1") ^
            " [ (APPLIST " ^ (string_of_id id) ^ " " ^ args ^ ") ] "  ^
      	    "-> [ (APPLIST $c ($LIST $l)):E ]"
  in
  try
    let se = Pcoq.parse_string Pcoq.Prim.syntax_entry_eoi str in
    Metasyntax.add_syntax_obj "constr" [se]
  with Stdpp.Exc_located _ -> 
    anomaly ("ill-formed syntax entry: "^str)

let coercion_syntax idf ps clt =
  match clt with
    | CL_FUN -> 
	fun_coercion_syntax_entry idf ps;
	coercion_syntax_entry idf ps
    | _ -> coercion_syntax_entry idf ps

let add_new_coercion_in_graph1 (coef,v,stre,isid,cls,clt) idf ps =
  add_anonymous_leaf
    (inCoercion
       ((coef,
	 {cOE_VALUE=v;cOE_STRE=stre;cOE_ISID=isid;cOE_PARAM=ps}),
	cls,clt));
  coercion_syntax idf ps clt

(* 
nom de la fonction coercion
strength de f
nom de la classe source (optionnel)
sp de la classe source (dans le cas des structures)
nom de la classe target (optionnel)
booleen "coercion identite'?"

lorque source est None alors target est None aussi.
*)

let try_add_new_coercion_core idf stre source target isid =
  let env = Global.env () in
  let v = construct_reference env CCI idf in
  let t = Retyping.get_type_of env Evd.empty v in
  let k = Retyping.get_type_of env Evd.empty t in
  let vj = {uj_val=v; uj_type=t; uj_kind = k} in
  let f_vardep,coef = coe_constructor_at_head v in
  if coercion_exists coef then
    errorlabstrm "try_add_coercion" 
      [< 'sTR(string_of_id idf) ; 'sTR" is already a coercion" >];
  let lp = prods_of t in
  let llp = List.length lp in
  if llp <= 1 then
    errorlabstrm "try_add_coercion"         
      [< 'sTR"Does not correspond to a coercion" >];
  let ids,(cls,ps,vs,lvs,ind,s_vardep) =
    try 
      get_source (List.tl lp) source
    with Not_found -> 
      errorlabstrm "try_add_coercion" 
        [<'sTR"We do not find the source class " >] 
  in
  if (cls = CL_FUN) then
    errorlabstrm "try_add_coercion" 
      [< 'sTR"FUNCLASS cannot be a source class" >];
  if (cls = CL_SORT) then
    errorlabstrm "try_add_coercion" 
      [< 'sTR"SORTCLASS cannot be a source class" >];
  if not (uniform_cond (llp-1-ind) lvs) then
    errorlabstrm "try_add_coercion" 
      [<'sTR(string_of_id idf);
        'sTR" does not respect the inheritance uniform condition" >];
  let clt,pt,vt =
    try 
      get_target (List.hd lp) ind 
    with Not_found -> 
      errorlabstrm "try_add_coercion" 
        [<'sTR"We cannot find the target class" >] 
  in
  let idt =
    (match target with
       | Some idt -> 
	   if idt = id_of_cl clt then 
	     idt
	   else 
	     errorlabstrm "try_add_coercion" 
               [<'sTR"The target class does not correspond to ";
		 'sTR(string_of_id idt) >]
       | None -> (id_of_cl clt)) 
  in
  let stres = check_class ids vs cls ps in
  let stret = check_class idt vt clt pt in
  let stref = stre_of_coe coef in
  let streunif = stre_unif_cond (s_vardep,f_vardep) in
  let stre' = stre_max4 stres stret stref streunif in
  (* if (stre=NeverDischarge) & (stre'<>NeverDischarge)
     then errorlabstrm "try_add_coercion" 
     [<'sTR(string_of_id idf);
     'sTR" must be declared as a local coercion (its strength is ";
     'sTR(string_of_strength stre');'sTR")" >] *)
  let stre = stre_max (stre,stre') in
  add_new_coercion_in_graph1 (coef,vj,stre,isid,cls,clt) idf ps


let try_add_new_coercion id stre =
  try_add_new_coercion_core id stre None None false

let try_add_new_coercion_subclass id stre =
  let idf = build_id_coercion None id in
  try_add_new_coercion_core idf stre (Some (Ident id)) None true

let try_add_new_coercion_with_target id stre source target isid =
  if isid then
    let idf = build_id_coercion (Some id) source in
    try_add_new_coercion_core idf stre (Some (Ident source)) (Some target) true
  else 
    try_add_new_coercion_core id stre (Some (Ident source)) (Some target) false

let try_add_new_coercion_record id stre source_sp =
  try_add_new_coercion_core id stre (Some (Section_path source_sp)) None false

(* fonctions pour le discharge: plutot sale *)

let defined_in_sec sp sec_sp =
  let ((p1,id1,k1)) = repr_path sp in
  let ((p2,id2,k2)) = repr_path sec_sp in
  p1 = (string_of_id id2)::p2

let process_class sec_sp ((cl,{cL_STR=s;cL_STRE=stre;cL_PARAM=p}) as x ) =
  let env = Global.env () in
  match cl with 
    | CL_Var id -> x
    | CL_SP sp -> 
        if defined_in_sec sp sec_sp then
	  let ((_,spid,spk)) = repr_path sp in
          let newsp = Lib.make_path spid CCI in 
          let v = global_reference CCI spid in
          let t = Retyping.get_type_of env Evd.empty v in
          let p = arity_sort t in
          (CL_SP newsp,{cL_STR=s;cL_STRE=stre;cL_PARAM=p})
        else 
	  x
    | CL_IND (sp,i) ->
        if defined_in_sec sp sec_sp then
	  let ((_,spid,spk)) = repr_path sp in
          let newsp = Lib.make_path spid CCI in 
          let v = global_reference CCI spid in
          let t = Retyping.get_type_of env Evd.empty v in
          let p = arity_sort t in
          (CL_IND (newsp,i),{cL_STR=s;cL_STRE=stre;cL_PARAM=p})
        else 
	  x
    | _ -> anomaly "process_class" 

let process_cl sec_sp cl =
  match cl with
    | CL_Var id -> CL_Var id 
    | CL_SP sp ->
	if defined_in_sec sp sec_sp then
	  let ((_,spid,spk)) = repr_path sp in
          let newsp = Lib.make_path spid CCI in 
          CL_SP newsp
        else 
	  cl
    | CL_IND (sp,i) ->
	if defined_in_sec sp sec_sp then
	  let ((_,spid,spk)) = repr_path sp in
          let newsp = Lib.make_path spid CCI in 
          CL_IND (newsp,i)
        else 
	  cl
    | _ -> cl

let process_coercion sec_sp (((coe,coeinfo),s,t) as x) =
  let s1= process_cl sec_sp s in
  let t1 = process_cl sec_sp t in
  let p = (snd (class_info s1)).cL_PARAM in
  match coe with 
    | NAM_Var id -> ((coe,coeinfo),s1,t1),id,p
    | NAM_SP sp -> 
	if defined_in_sec sp sec_sp then
	  let ((_,spid,spk)) = repr_path sp in
	  let newsp = Lib.make_path spid CCI in
	  let v = global_reference CCI spid in
	  ((NAM_SP newsp,coeinfo),s1,t1),spid,p
	else 
	  ((coe,coeinfo),s1,t1),basename sp,p
    | NAM_Construct ((sp,i),j) -> 
	if defined_in_sec sp sec_sp then 
	  let ((_,spid,spk)) = repr_path sp in
	  let newsp = Lib.make_path spid CCI in
	  let id = Global.id_of_global (MutConstruct((newsp,i),j)) in
	  let v = global_reference CCI id in
          (((NAM_Construct ((newsp,i),j)),coeinfo),s1,t1),id,p
	else 
	  ((coe,coeinfo),s1,t1),
	  Global.id_of_global (MutConstruct((sp,i),j)),
	  p