diff options
Diffstat (limited to 'pretyping/coercion.ml')
| -rw-r--r-- | pretyping/coercion.ml | 144 |
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 |