summaryrefslogtreecommitdiff
path: root/pretyping/coercion.ml
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2006-11-21 21:38:49 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2006-11-21 21:38:49 +0000
commit208a0f7bfa5249f9795e6e225f309cbe715c0fad (patch)
tree591e9e512063e34099782e2518573f15ffeac003 /pretyping/coercion.ml
parentde0085539583f59dc7c4bf4e272e18711d565466 (diff)
Imported Upstream version 8.1~gammaupstream/8.1.gamma
Diffstat (limited to 'pretyping/coercion.ml')
-rw-r--r--pretyping/coercion.ml144
1 files changed, 77 insertions, 67 deletions
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index d0ee913f..cc74b0ad 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -5,7 +5,7 @@
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: coercion.ml 8875 2006-05-29 19:59:11Z msozeau $ *)
+(* $Id: coercion.ml 9257 2006-10-21 17:28:28Z herbelin $ *)
open Util
open Names
@@ -20,6 +20,7 @@ open Evarutil
open Evarconv
open Retyping
open Evd
+open Termops
module type S = sig
(*s Coercions. *)
@@ -66,7 +67,14 @@ module Default = struct
(* Typing operations dealing with coercions *)
exception NoCoercion
- let class_of1 env sigma t = class_of env sigma (nf_evar sigma t)
+ 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 =
@@ -84,7 +92,6 @@ module Default = struct
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) ->
@@ -100,7 +107,6 @@ module Default = struct
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
@@ -120,22 +126,23 @@ module Default = struct
let t = whd_betadeltaiota env (evars_of isevars) j.uj_type in
match kind_of_term t with
| Prod (_,_,_) -> (isevars,j)
- | Evar ev when not (is_defined_evar isevars ev) ->
+ | 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 (evars_of isevars) j.uj_type in
+ 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 (evars_of isevars) j.uj_type in
+ 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
- (isevars,type_judgment env (j_nf_evar (evars_of isevars) j1))
+ 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
@@ -154,8 +161,8 @@ module Default = struct
let inh_coerce_to_fail env isevars c1 v t =
let v', t' =
try
- let t1,i1 = class_of1 env (evars_of isevars) c1 in
- let t2,i2 = class_of1 env (evars_of isevars) t in
+ 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 ->
@@ -166,64 +173,68 @@ module Default = struct
in
try (the_conv_x_leq env t' c1 isevars, v', t')
with Reduction.NotConvertible -> raise NoCoercion
- open Pp
+
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) ->
- (try the_conv_x env v1 u1 isevars, Some (x, v1, v2) (* leq v1 u1? *)
- 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 v1' -> mkApp (lift 1 v, [|v1'|])) v1'
- | None -> None
- and evd', t2 =
- match v1' with
- Some v1' -> evd', subst1 v1' t2
- | None ->
- let evd', ev = new_evar evd' env ~src:(loc, InternalHole) t1' in
- evd', subst1 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))
-
+ 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
@@ -236,8 +247,7 @@ module Default = struct
error_actual_type_loc loc env sigma cj t
in
let val' = match val' with Some v -> v | None -> assert(false) in
- let nf = nf_isevar evd' in
- (evd',{ uj_val = nf val'; uj_type = nf t })
+ (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