summaryrefslogtreecommitdiff
path: root/pretyping/coercion.ml
blob: cc74b0ad05cfe0bc7974e7beef37e6edc0ef5176 (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
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)
(* $Id: coercion.ml 9257 2006-10-21 17:28:28Z herbelin $ *)

open Util
open Names
open Term
open Reductionops
open Environ
open Typeops
open Pretype_errors
open Classops
open Recordops
open Evarutil
open Evarconv
open Retyping
open Evd
open Termops

module type S = sig
  (*s Coercions. *)
  
  (* [inh_app_fun env isevars j] coerces [j] to a function; i.e. it
     inserts a coercion into [j], if needed, in such a way it gets as
     type a product; it returns [j] if no coercion is applicable *)
  val inh_app_fun :
    env -> evar_defs -> unsafe_judgment -> evar_defs * unsafe_judgment
    
  (* [inh_coerce_to_sort env isevars j] coerces [j] to a type; i.e. it
     inserts a coercion into [j], if needed, in such a way it gets as
     type a sort; it fails if no coercion is applicable *)
  val inh_coerce_to_sort : loc ->
    env -> evar_defs -> unsafe_judgment -> evar_defs * unsafe_type_judgment

  (* [inh_coerce_to_base env isevars j] coerces [j] to its base type; i.e. it
     inserts a coercion into [j], if needed, in such a way it gets as
     type its base type (the notion depends on the coercion system) *)
  val inh_coerce_to_base : loc ->
    env -> evar_defs -> unsafe_judgment -> evar_defs * unsafe_judgment
    
  (* [inh_conv_coerce_to loc env isevars j t] coerces [j] to an object of type 
     [t]; i.e. it inserts a coercion into [j], if needed, in such a way [t] and
     [j.uj_type] are convertible; it fails if no coercion is applicable *)
  val inh_conv_coerce_to : loc -> 
    env -> evar_defs -> unsafe_judgment -> type_constraint_type -> evar_defs * unsafe_judgment
    

  (* [inh_conv_coerces_to loc env isevars t t'] checks if an object of type [t]
     is coercible to an object of type [t'] adding evar constraints if needed;
     it fails if no coercion exists *)
  val inh_conv_coerces_to : loc -> 
    env -> evar_defs -> types -> type_constraint_type -> evar_defs

  (* [inh_pattern_coerce_to loc env isevars pat ind1 ind2] coerces the Cases
     pattern [pat] typed in [ind1] into a pattern typed in [ind2];
     raises [Not_found] if no coercion found *)
  val inh_pattern_coerce_to :
    loc  -> Rawterm.cases_pattern -> inductive -> inductive -> Rawterm.cases_pattern
end

module Default = struct
  (* Typing operations dealing with coercions *)
  exception NoCoercion

  let whd_app_evar sigma t =
    match kind_of_term t with
      | App (f,l) -> mkApp (whd_evar sigma f,l)
      | _ -> whd_evar sigma t

  let class_of1 env isevars t =
    let sigma = evars_of isevars in
    class_of env sigma (whd_app_evar sigma t)

  (* Here, funj is a coercion therefore already typed in global context *)
  let apply_coercion_args env argl funj =
    let rec apply_rec acc typ = function
      | [] -> { uj_val = applist (j_val funj,argl);
		uj_type = typ }
      | h::restl ->
	  (* On devrait pouvoir s'arranger pour qu'on n'ait pas à faire hnf_constr *)
  	  match kind_of_term (whd_betadeltaiota env Evd.empty typ) with
	    | Prod (_,c1,c2) -> 
		(* Typage garanti par l'appel à app_coercion*)
		apply_rec (h::acc) (subst1 h c2) restl
	    | _ -> anomaly "apply_coercion_args"
    in 
      apply_rec [] funj.uj_type argl

  (* 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 Rawterm.PatVar (loc, Anonymous) else pat in
	   Rawterm.PatCstr (loc, co, list_tabulate f (n+1), Anonymous))
      pat p

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

  (* appliquer le chemin de coercions p à hj *)
  let apply_coercion env p hj typ_cl =
    try 
      fst (List.fold_left
             (fun (ja,typ_cl) i -> 
		let fv,isid = coercion_value i in
		let argl = (class_args_of typ_cl)@[ja.uj_val] in
		let jres = apply_coercion_args env argl fv in
		  (if isid then 
		     { uj_val = ja.uj_val; uj_type = jres.uj_type }
		   else 
		     jres),
		jres.uj_type)
             (hj,typ_cl) p)
    with _ -> anomaly "apply_coercion"

  let inh_app_fun env isevars j = 
    let t = whd_betadeltaiota env (evars_of isevars) j.uj_type in
      match kind_of_term t with
	| Prod (_,_,_) -> (isevars,j)
	| Evar ev ->
	    let (isevars',t) = define_evar_as_arrow isevars ev in
	      (isevars',{ uj_val = j.uj_val; uj_type = t })
	| _ ->
       	    (try
 	       let t,i1 = class_of1 env isevars j.uj_type in
      	       let p = lookup_path_to_fun_from i1 in
		 (isevars,apply_coercion env p j t)
	     with Not_found -> (isevars,j))

  let inh_tosort_force loc env isevars j =
    try
      let t,i1 = class_of1 env isevars j.uj_type in
      let p = lookup_path_to_sort_from i1 in
      let j1 = apply_coercion env p j t in 
      let j2 = on_judgment_type (whd_evar (evars_of isevars)) j1 in
        (isevars,type_judgment env j2)
    with Not_found ->
      error_not_a_type_loc loc env (evars_of isevars) j

  let inh_coerce_to_sort loc env isevars j =
    let typ = whd_betadeltaiota env (evars_of isevars) j.uj_type in
      match kind_of_term typ with
	| Sort s -> (isevars,{ utj_val = j.uj_val; utj_type = s })
	| Evar ev when not (is_defined_evar isevars ev) ->
	    let (isevars',s) = define_evar_as_sort isevars ev in
	      (isevars',{ utj_val = j.uj_val; utj_type = s })
	| _ ->
	    inh_tosort_force loc env isevars j

  let inh_coerce_to_base loc env isevars j = (isevars, j)

  let inh_coerce_to_fail env isevars c1 v t =
    let v', t' =
      try 
	let t1,i1 = class_of1 env isevars c1 in
	let t2,i2 = class_of1 env isevars t in
	let p = lookup_path_between (i2,i1) in
	  match v with
	      Some v -> 
		let j = apply_coercion env p {uj_val = v; uj_type = t} t2 in
		  Some j.uj_val, j.uj_type
	    | None -> None, t
      with Not_found -> raise NoCoercion 
    in
      try (the_conv_x_leq env t' c1 isevars, v', t')
      with Reduction.NotConvertible -> raise NoCoercion

  let rec inh_conv_coerce_to_fail loc env isevars v t c1 =
    try (the_conv_x_leq env t c1 isevars, v, t)
    with Reduction.NotConvertible ->
    try inh_coerce_to_fail env isevars c1 v t
    with NoCoercion ->
    match
      kind_of_term (whd_betadeltaiota env (evars_of isevars) t),
      kind_of_term (whd_betadeltaiota env (evars_of isevars) c1)
    with
    | Prod (_,t1,t2), Prod (name,u1,u2) -> 
	let v' = option_map (whd_betadeltaiota env (evars_of isevars)) v in
	let (evd',b) =
	  match v' with 
	  | Some v' ->
	      (match kind_of_term v' with
	       | Lambda (x,v1,v2) ->
		   (* sous-typage non contravariant: pas de "leq v1 u1" *)
		   (try the_conv_x env v1 u1 isevars, Some (x, v1, v2)
		   with Reduction.NotConvertible -> (isevars, None))
	       | _  -> (isevars, None))
	  | None -> (isevars, None)
	in
	(match b with
	 | Some (x, v1, v2) ->
	     let env1 = push_rel (x,None,v1) env in
	     let (evd'', v2', t2') = inh_conv_coerce_to_fail loc env1 evd'
	       (Some v2) t2 u2 in
	     (evd'', option_map (fun v2' -> mkLambda (x, v1, v2')) v2', 
	     mkProd (x, v1, t2'))
	 | None ->
	     (* Mismatch on t1 and u1 or not a lambda: we eta-expand *)
	     (* we look for a coercion c:u1->t1 s.t. [name:u1](v' (c x)) *)
	     (* has type (name:u1)u2 (with v' recursively obtained) *)
	     let name = match name with 
	       | Anonymous -> Name (id_of_string "x")
	       | _ -> name
	     in
	     let env1 = push_rel (name,None,u1) env in
	     let (evd', v1', t1') =
	       inh_conv_coerce_to_fail loc env1 isevars
		 (Some (mkRel 1)) (lift 1 u1) (lift 1 t1)
	     in
	     let (evd'', v2', t2') = 
	       let v2 =
		 match v with 
		 | Some v -> option_map (fun x -> mkApp(lift 1 v,[|x|])) v1'
		 | None -> None
	       and evd', t2 =
		 match v1' with 
		 | Some v1' -> evd', subst_term v1' t2
		 | None -> 
		     let evd', ev =
		       new_evar evd' env ~src:(loc, InternalHole) t1' in
		     evd', subst_term ev t2
	       in
	       inh_conv_coerce_to_fail loc env1 evd' v2 t2 u2
	     in
	     (evd'', option_map (fun v2' -> mkLambda (name, u1, v2')) v2',
	     mkProd (name, u1, t2')))
    | _ -> raise NoCoercion

  (* Look for cj' obtained from cj by inserting coercions, s.t. cj'.typ = t *)
  let inh_conv_coerce_to loc env isevars cj (n, t) =
    match n with
	None ->
	  let (evd', val', type') = 
	    try 
	      inh_conv_coerce_to_fail loc env isevars (Some cj.uj_val) cj.uj_type t
	    with NoCoercion ->
	      let sigma = evars_of isevars in
		error_actual_type_loc loc env sigma cj t
	  in
	  let val' = match val' with Some v -> v | None -> assert(false) in
	    (evd',{ uj_val = val'; uj_type = t })
      | Some (init, cur) -> (isevars, cj)
      
    let inh_conv_coerces_to loc env (isevars : evar_defs) t (abs, t') = isevars
      (* Still problematic, as it changes unification 
      let nabsinit, nabs = 
	match abs with
	    None -> 0, 0
	  | Some (init, cur) -> init, cur
      in
	try 
	  let (rels, rng) = 
	    (* a little more effort to get products is needed *) 
	    try decompose_prod_n nabs t
	    with _ -> 
	      if !Options.debug then
		msg_warning (str "decompose_prod_n failed");
	      raise (Invalid_argument "Coercion.inh_conv_coerces_to")
	  in
	    (* The final range free variables must have been replaced by evars, we accept only that evars
	       in rng are applied to free vars. *)
	    if noccur_with_meta 0 (succ nabsinit) rng then (
	      let env', t, t' = 
		let env' = List.fold_right (fun (n, t) env -> push_rel (n, None, t) env) rels env in
		  env', rng, lift nabs t'
	      in
		try 
		  pi1 (inh_conv_coerce_to_fail loc env' isevars None t t')
		with NoCoercion ->
		  isevars) (* Maybe not enough information to unify *)
	      (*let sigma = evars_of isevars in
		error_cannot_coerce env' sigma (t, t'))*)
	    else isevars
	with Invalid_argument _ -> isevars	  *)
end