aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/coercion.ml
blob: 913e80f3995ebc2be3c95f52e66ce6c2ccf7e0e5 (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
(************************************************************************)
(*  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        *)
(************************************************************************)

(* Created by Hugo Herbelin for Coq V7 by isolating the coercion
   mechanism out of the type inference algorithm in file trad.ml from
   Coq V6.3, Nov 1999; The coercion mechanism was implemented in
   trad.ml by Amokrane Saïbi, May 1996 *)
(* Addition of products and sorts in canonical structures by Pierre
   Corbineau, Feb 2008 *)
(* Turned into an abstract compilation unit by Matthieu Sozeau, March 2006 *)

open CErrors
open Util
open Names
open Term
open Vars
open Reductionops
open Environ
open Typeops
open Pretype_errors
open Classops
open Evarutil
open Evarconv
open Evd
open Termops
open Globnames

let use_typeclasses_for_conversion = ref true

let _ =
  Goptions.declare_bool_option
    { Goptions.optsync  = true;
      optdepr  = false;
      optname  = "use typeclass resolution during conversion";
      optkey   = ["Typeclass"; "Resolution"; "For"; "Conversion"];
      optread  = (fun () -> !use_typeclasses_for_conversion);
      optwrite = (fun b -> use_typeclasses_for_conversion := b) }


(* Typing operations dealing with coercions *)
exception NoCoercion
exception NoCoercionNoUnifier of evar_map * unification_error

(* Here, funj is a coercion therefore already typed in global context *)
let apply_coercion_args env evd check isproj argl funj =
  let evdref = ref evd in
  let rec apply_rec acc typ = function
    | [] ->
      if isproj then
	let cst = fst (destConst (j_val funj)) in
	let p = Projection.make cst false in
	let pb = lookup_projection p env in
	let args = List.skipn pb.Declarations.proj_npars argl in
	let hd, tl = match args with hd :: tl -> hd, tl | [] -> assert false in
	  { uj_val = applist (mkProj (p, hd), tl);
	    uj_type = typ }
      else
	{ uj_val = applist (j_val funj,argl);
	  uj_type = typ }
    | h::restl -> (* On devrait pouvoir s'arranger pour qu'on n'ait pas a faire hnf_constr *)
      match kind_of_term (whd_all env evd typ) with
      | Prod (_,c1,c2) ->
        if check && not (e_cumul env evdref (Retyping.get_type_of env evd h) c1) then
	  raise NoCoercion;
        apply_rec (h::acc) (subst1 h c2) restl
      | _ -> anomaly (Pp.str "apply_coercion_args")
  in
  let res = apply_rec [] funj.uj_type argl in
    !evdref, res

(* appliquer le chemin de coercions de patterns p *)
let apply_pattern_coercion loc pat p =
  List.fold_left
    (fun pat (co,n) ->
       let f i = if i<n then Glob_term.PatVar (loc, Anonymous) else pat in
	 Glob_term.PatCstr (loc, co, List.init (n+1) f, Anonymous))
    pat p

(* raise Not_found if no coercion found *)
let inh_pattern_coerce_to loc env pat ind1 ind2 =
  let p = lookup_pattern_path_between env (ind1,ind2) in
    apply_pattern_coercion loc pat p

(* Program coercions *)

open Program

let make_existential loc ?(opaque = not (get_proofs_transparency ()))  env evdref c =
  let src = (loc, Evar_kinds.QuestionMark (Evar_kinds.Define opaque)) in
  Evarutil.e_new_evar env evdref ~src c

let app_opt env evdref f t =
  whd_betaiota !evdref (app_opt f t)

let pair_of_array a = (a.(0), a.(1))

let disc_subset x =
  match kind_of_term x with
  | App (c, l) ->
      (match kind_of_term c with
       Ind (i,_) ->
	 let len = Array.length l in
	 let sigty = delayed_force sig_typ in
	   if Int.equal len 2 && eq_ind i (Globnames.destIndRef sigty)
	   then
	     let (a, b) = pair_of_array l in
	       Some (a, b)
	   else None
       | _ -> None)
  | _ -> None

exception NoSubtacCoercion
  
let hnf env evd c = whd_all env evd c
let hnf_nodelta env evd c = whd_betaiota evd c

let lift_args n sign =
  let rec liftrec k = function
    | t::sign -> liftn n k t :: (liftrec (k-1) sign)
    | [] -> []
  in
    liftrec (List.length sign) sign

let mu env evdref t =
  let rec aux v =
    let v' = hnf env !evdref v in
      match disc_subset v' with
      | Some (u, p) ->
	let f, ct = aux u in
	let p = hnf_nodelta env !evdref p in
	  (Some (fun x ->
		   app_opt env evdref 
		     f (papp evdref sig_proj1 [| u; p; x |])),
	   ct)
      | None -> (None, v)
  in aux t

and coerce loc env evdref (x : Term.constr) (y : Term.constr)
    : (Term.constr -> Term.constr) option
    =
  let open Context.Rel.Declaration in
  let rec coerce_unify env x y =
    let x = hnf env !evdref x and y = hnf env !evdref y in
      try
	evdref := the_conv_x_leq env x y !evdref;
	None
      with UnableToUnify _ -> coerce' env x y
  and coerce' env x y : (Term.constr -> Term.constr) option =
    let subco () = subset_coerce env evdref x y in
    let dest_prod c =
      let open Context.Rel.Declaration in
      match Reductionops.splay_prod_n env ( !evdref) 1 c with
      | [LocalAssum (na,t) | LocalDef (na,_,t)], c -> (na,t), c
      | _ -> raise NoSubtacCoercion
    in
    let coerce_application typ typ' c c' l l' =
      let len = Array.length l in
      let rec aux tele typ typ' i co =
	if i < len then
	  let hdx = l.(i) and hdy = l'.(i) in
	    try evdref := the_conv_x_leq env hdx hdy !evdref;
	      let (n, eqT), restT = dest_prod typ in
	      let (n', eqT'), restT' = dest_prod typ' in
		aux (hdx :: tele) (subst1 hdx restT) (subst1 hdy restT') (succ i) co
	    with UnableToUnify _ ->
	      let (n, eqT), restT = dest_prod typ in
	      let (n', eqT'), restT' = dest_prod typ' in
	      let _ =
		try evdref := the_conv_x_leq env eqT eqT' !evdref
		with UnableToUnify _ -> raise NoSubtacCoercion
	      in
		(* Disallow equalities on arities *)
		if Reduction.is_arity env eqT then raise NoSubtacCoercion;
		let restargs = lift_args 1
		  (List.rev (Array.to_list (Array.sub l (succ i) (len - (succ i)))))
		in
		let args = List.rev (restargs @ mkRel 1 :: List.map (lift 1) tele) in
		let pred = mkLambda (n, eqT, applistc (lift 1 c) args) in
		let eq = papp evdref coq_eq_ind [| eqT; hdx; hdy |] in
		let evar = make_existential loc env evdref eq in
		let eq_app x = papp evdref coq_eq_rect
		  [| eqT; hdx; pred; x; hdy; evar|] 
		in
		  aux (hdy :: tele) (subst1 hdx restT) 
		    (subst1 hdy restT') (succ i)  (fun x -> eq_app (co x))
	else Some (fun x -> 
	  let term = co x in
	    Typing.e_solve_evars env evdref term)
      in
	if isEvar c || isEvar c' || not (Program.is_program_generalized_coercion ()) then
	  (* Second-order unification needed. *)
	  raise NoSubtacCoercion;
	aux [] typ typ' 0 (fun x -> x)
    in
      match (kind_of_term x, kind_of_term y) with
      | Sort s, Sort s' ->
        (match s, s' with
	| Prop x, Prop y when x == y -> None
	| Prop _, Type _ -> None
	| Type x, Type y when Univ.Universe.equal x y -> None (* false *)
	| _ -> subco ())
      | Prod (name, a, b), Prod (name', a', b') ->
	  let name' = 
	    Name (Namegen.next_ident_away Namegen.default_dependent_ident (Termops.ids_of_context env))
	  in
	  let env' = push_rel (LocalAssum (name', a')) env in
	  let c1 = coerce_unify env' (lift 1 a') (lift 1 a) in
	    (* env, x : a' |- c1 : lift 1 a' > lift 1 a *)
	  let coec1 = app_opt env' evdref c1 (mkRel 1) in
	    (* env, x : a' |- c1[x] : lift 1 a *)
	  let c2 = coerce_unify env' (subst1 coec1 (liftn 1 2 b)) b' in
	    (* env, x : a' |- c2 : b[c1[x]/x]] > b' *)
	    (match c1, c2 with
	     | None, None -> None
	     | _, _ ->
		 Some
		   (fun f ->
		      mkLambda (name', a',
				app_opt env' evdref c2
				  (mkApp (lift 1 f, [| coec1 |])))))

      | App (c, l), App (c', l') ->
	  (match kind_of_term c, kind_of_term c' with
	   Ind (i, u), Ind (i', u') -> (* Inductive types *)
	     let len = Array.length l in
	     let sigT = delayed_force sigT_typ in
	     let prod = delayed_force prod_typ in
	       (* Sigma types *)
	       if Int.equal len (Array.length l') && Int.equal len 2 && eq_ind i i'
		 && (eq_ind i (destIndRef sigT) || eq_ind i (destIndRef prod))
	       then
		 if eq_ind i (destIndRef sigT)
		 then
		   begin
		     let (a, pb), (a', pb') =
		       pair_of_array l, pair_of_array l'
		     in
		     let c1 = coerce_unify env a a' in
		     let remove_head a c =
		       match kind_of_term c with
		       | Lambda (n, t, t') -> c, t'
		       | Evar (k, args) ->
			   let (evs, t) = Evardefine.define_evar_as_lambda env !evdref (k,args) in
			     evdref := evs;
			     let (n, dom, rng) = destLambda t in
			     let dom = whd_evar !evdref dom in
			       if isEvar dom then
				 let (domk, args) = destEvar dom in
				   evdref := define domk a !evdref;
			       else ();
			       t, rng
		       | _ -> raise NoSubtacCoercion
		     in
		     let (pb, b), (pb', b') = remove_head a pb, remove_head a' pb' in
		     let env' = push_rel (LocalAssum (Name Namegen.default_dependent_ident, a)) env in
		     let c2 = coerce_unify env' b b' in
		       match c1, c2 with
		       | None, None -> None
		       | _, _ ->
			   Some
			     (fun x ->
				let x, y =
				  app_opt env' evdref c1 (papp evdref sigT_proj1
							    [| a; pb; x |]),
				  app_opt env' evdref c2 (papp evdref sigT_proj2
							  [| a; pb; x |])
				in
				  papp evdref sigT_intro [| a'; pb'; x ; y |])
		   end
		 else
		   begin
		     let (a, b), (a', b') =
		       pair_of_array l, pair_of_array l'
		     in
		     let c1 = coerce_unify env a a' in
		     let c2 = coerce_unify env b b' in
		       match c1, c2 with
		       | None, None -> None
		       | _, _ ->
			   Some
			     (fun x ->
				let x, y =
				  app_opt env evdref c1 (papp evdref prod_proj1
							   [| a; b; x |]),
				  app_opt env evdref c2 (papp evdref prod_proj2
							   [| a; b; x |])
				in
				  papp evdref prod_intro [| a'; b'; x ; y |])
		   end
	       else
		 if eq_ind i i' && Int.equal len (Array.length l') then
		   let evm = !evdref in
		     (try subco ()
		      with NoSubtacCoercion ->
			let typ = Typing.unsafe_type_of env evm c in
			let typ' = Typing.unsafe_type_of env evm c' in
			  coerce_application typ typ' c c' l l')
		 else
		   subco ()
	   | x, y when Constr.equal c c' ->
	       if Int.equal (Array.length l) (Array.length l') then
		 let evm =  !evdref in
		 let lam_type = Typing.unsafe_type_of env evm c in
		 let lam_type' = Typing.unsafe_type_of env evm c' in
		   coerce_application lam_type lam_type' c c' l l'
	       else subco ()
	   | _ -> subco ())
      | _, _ ->  subco ()

  and subset_coerce env evdref x y =
    match disc_subset x with
    Some (u, p) ->
      let c = coerce_unify env u y in
      let f x =
	app_opt env evdref c (papp evdref sig_proj1 [| u; p; x |])
      in Some f
    | None ->
	match disc_subset y with
	Some (u, p) ->
	  let c = coerce_unify env x u in
	    Some
	      (fun x ->
		 let cx = app_opt env evdref c x in
		 let evar = make_existential loc env evdref (mkApp (p, [| cx |]))
		 in
		   (papp evdref sig_intro [| u; p; cx; evar |]))
	| None ->
	    raise NoSubtacCoercion
  in coerce_unify env x y

let app_coercion env evdref coercion v =
  match coercion with
  | None -> v
  | Some f ->
     let v' = Typing.e_solve_evars env evdref (f v) in
     whd_betaiota !evdref v'

let coerce_itf loc env evd v t c1 =
  let evdref = ref evd in
  let coercion = coerce loc env evdref t c1 in
  let t = Option.map (app_coercion env evdref coercion) v in
    !evdref, t

let saturate_evd env evd =
  Typeclasses.resolve_typeclasses
    ~filter:Typeclasses.no_goals ~split:true ~fail:false env evd

(* Apply coercion path from p to hj; raise NoCoercion if not applicable *)
let apply_coercion env sigma p hj typ_cl =
  try
    let j,t,evd = 
      List.fold_left
        (fun (ja,typ_cl,sigma) i ->
	  let ((fv,isid,isproj),ctx) = coercion_value i in
	  let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx in
	  let argl = (class_args_of env sigma typ_cl)@[ja.uj_val] in
	  let sigma, jres = 
	    apply_coercion_args env sigma true isproj argl fv 
	  in
	    (if isid then
	      { uj_val = ja.uj_val; uj_type = jres.uj_type }
	     else
	      jres),
	    jres.uj_type,sigma)
      (hj,typ_cl,sigma) p
    in evd, j
  with NoCoercion as e -> raise e
  | e when CErrors.noncritical e -> anomaly (Pp.str "apply_coercion")

(* Try to coerce to a funclass; raise NoCoercion if not possible *)
let inh_app_fun_core env evd j =
  let t = whd_all env evd j.uj_type in
    match kind_of_term t with
    | Prod (_,_,_) -> (evd,j)
    | Evar ev ->
	let (evd',t) = Evardefine.define_evar_as_product evd ev in
	  (evd',{ uj_val = j.uj_val; uj_type = t })
    | _ ->
      	try let t,p =
	  lookup_path_to_fun_from env evd j.uj_type in
	    apply_coercion env evd p j t
	with Not_found | NoCoercion ->
          if Flags.is_program_mode () then
	  try
	    let evdref = ref evd in
	    let coercef, t = mu env evdref t in
	    let res = { uj_val = app_opt env evdref coercef j.uj_val; uj_type = t } in
	      (!evdref, res)
	  with NoSubtacCoercion | NoCoercion ->
	    (evd,j)
          else raise NoCoercion

(* Try to coerce to a funclass; returns [j] if no coercion is applicable *)
let inh_app_fun resolve_tc env evd j =
  try inh_app_fun_core env evd j
  with
  | NoCoercion when not resolve_tc
    || not !use_typeclasses_for_conversion -> (evd, j)
  | NoCoercion ->
    try inh_app_fun_core env (saturate_evd env evd) j
    with NoCoercion -> (evd, j)

let inh_tosort_force loc env evd j =
  try
    let t,p = lookup_path_to_sort_from env evd j.uj_type in
    let evd,j1 = apply_coercion env evd p j t in
    let j2 = on_judgment_type (whd_evar evd) j1 in
      (evd,type_judgment env j2)
  with Not_found | NoCoercion ->
    error_not_a_type_loc loc env evd j

let inh_coerce_to_sort loc env evd j =
  let typ = whd_all env evd j.uj_type in
    match kind_of_term typ with
    | Sort s -> (evd,{ utj_val = j.uj_val; utj_type = s })
    | Evar ev when not (is_defined evd (fst ev)) ->
	let (evd',s) = Evardefine.define_evar_as_sort env evd ev in
	  (evd',{ utj_val = j.uj_val; utj_type = s })
    | _ ->
	inh_tosort_force loc env evd j

let inh_coerce_to_base loc env evd j =
  if Flags.is_program_mode () then
    let evdref = ref evd in
    let ct, typ' = mu env evdref j.uj_type in
    let res =
      { uj_val = app_coercion env evdref ct j.uj_val;
	uj_type = typ' }
    in !evdref, res
  else (evd, j)

let inh_coerce_to_prod loc env evd t =
  if Flags.is_program_mode () then
    let evdref = ref evd in
    let _, typ' = mu env evdref t in
      !evdref, typ'
  else (evd, t)

let inh_coerce_to_fail env evd rigidonly v t c1 =
  if rigidonly && not (Heads.is_rigid env c1 && Heads.is_rigid env t)
  then
    raise NoCoercion
  else
    let evd, v', t' =
      try
	let t2,t1,p = lookup_path_between env evd (t,c1) in
	  match v with
	  | Some v ->
	    let evd,j =
	      apply_coercion env evd p
		{uj_val = v; uj_type = t} t2 in
	      evd, Some j.uj_val, j.uj_type
	  | None -> evd, None, t
      with Not_found -> raise NoCoercion
    in
      try (the_conv_x_leq env t' c1 evd, v')
      with UnableToUnify _ -> raise NoCoercion

let rec inh_conv_coerce_to_fail loc env evd rigidonly v t c1 =
  try (the_conv_x_leq env t c1 evd, v)
  with UnableToUnify (best_failed_evd,e) ->
    try inh_coerce_to_fail env evd rigidonly v t c1
    with NoCoercion ->
      match
      kind_of_term (whd_all env evd t),
      kind_of_term (whd_all env evd c1)
      with
      | Prod (name,t1,t2), Prod (_,u1,u2) ->
          (* Conversion did not work, we may succeed with a coercion. *)
          (* We eta-expand (hence possibly modifying the original term!) *)
	  (* and look for a coercion c:u1->t1 s.t. fun x:u1 => v' (c x)) *)
	  (* has type forall (x:u1), u2 (with v' recursively obtained) *)
          (* Note: we retype the term because sort-polymorphism may have *)
          (* weaken its type *)
	  let name = match name with
	    | Anonymous -> Name Namegen.default_dependent_ident
	    | _ -> name in
	  let open Context.Rel.Declaration in
	  let env1 = push_rel (LocalAssum (name,u1)) env in
	  let (evd', v1) =
	    inh_conv_coerce_to_fail loc env1 evd rigidonly
              (Some (mkRel 1)) (lift 1 u1) (lift 1 t1) in
          let v1 = Option.get v1 in
	  let v2 = Option.map (fun v -> beta_applist (lift 1 v,[v1])) v in
	  let t2 = match v2 with
	    | None -> subst_term v1 t2
	    | Some v2 -> Retyping.get_type_of env1 evd' v2 in
	  let (evd'',v2') = inh_conv_coerce_to_fail loc env1 evd' rigidonly v2 t2 u2 in
	    (evd'', Option.map (fun v2' -> mkLambda (name, u1, v2')) v2')
      | _ -> raise (NoCoercionNoUnifier (best_failed_evd,e))

(* Look for cj' obtained from cj by inserting coercions, s.t. cj'.typ = t *)
let inh_conv_coerce_to_gen resolve_tc rigidonly loc env evd cj t =
  let (evd', val') =
    try
      inh_conv_coerce_to_fail loc env evd rigidonly (Some cj.uj_val) cj.uj_type t
    with NoCoercionNoUnifier (best_failed_evd,e) ->
      try
	if Flags.is_program_mode () then
	  coerce_itf loc env evd (Some cj.uj_val) cj.uj_type t
	else raise NoSubtacCoercion
      with
      | NoSubtacCoercion when not resolve_tc || not !use_typeclasses_for_conversion ->
	  error_actual_type_loc loc env best_failed_evd cj t e
      | NoSubtacCoercion ->
	let evd' = saturate_evd env evd in
      	  try
	    if evd' == evd then 
	      error_actual_type_loc loc env best_failed_evd cj t e
	    else 
      	      inh_conv_coerce_to_fail loc env evd' rigidonly (Some cj.uj_val) cj.uj_type t
	  with NoCoercionNoUnifier (_evd,_error) ->
	    error_actual_type_loc loc env best_failed_evd cj t e
  in
  let val' = match val' with Some v -> v | None -> assert(false) in
    (evd',{ uj_val = val'; uj_type = t })

let inh_conv_coerce_to resolve_tc = inh_conv_coerce_to_gen resolve_tc false
let inh_conv_coerce_rigid_to resolve_tc = inh_conv_coerce_to_gen resolve_tc true

let inh_conv_coerces_to loc env evd t t' =
  try
    fst (inh_conv_coerce_to_fail loc env evd true None t t')
  with NoCoercion ->
    evd (* Maybe not enough information to unify *)