From d331f7f1ac0ec2ed12d458597d558a1988db1ba6 Mon Sep 17 00:00:00 2001 From: barras Date: Tue, 7 Sep 2004 19:28:25 +0000 Subject: deuxieme vague de modifs: evar_defs fonctionnel git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6071 85f007b7-540e-0410-9357-904b9bb8a0f7 --- pretyping/coercion.ml | 95 ++++++++++++++++++--------------------------------- 1 file changed, 33 insertions(+), 62 deletions(-) (limited to 'pretyping/coercion.ml') diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index ddbdf94b4..347bc7b8e 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -77,16 +77,16 @@ let apply_coercion env p hj typ_cl = 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 (_,_,_) -> j + | Prod (_,_,_) -> (isevars,j) | Evar ev when not (is_defined_evar isevars ev) -> - let t = define_evar_as_arrow isevars ev in - { uj_val = j.uj_val; uj_type = t } + 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 p = lookup_path_to_fun_from i1 in - apply_coercion env p j t - with Not_found -> j) + (isevars,apply_coercion env p j t) + with Not_found -> (isevars,j)) let inh_tosort_force env isevars j = try @@ -99,13 +99,13 @@ let inh_tosort_force env isevars j = let inh_coerce_to_sort env isevars j = let typ = whd_betadeltaiota env (evars_of isevars) j.uj_type in match kind_of_term typ with - | Sort s -> { utj_val = j.uj_val; utj_type = s } + | Sort s -> (isevars,{ utj_val = j.uj_val; utj_type = s }) | Evar ev when not (is_defined_evar isevars ev) -> - let s = define_evar_as_sort isevars ev in - { utj_val = j.uj_val; utj_type = s } + let (isevars',s) = define_evar_as_sort isevars ev in + (isevars',{ utj_val = j.uj_val; utj_type = s }) | _ -> let j1 = inh_tosort_force env isevars j in - type_judgment env (j_nf_evar (evars_of isevars) j1) + (isevars,type_judgment env (j_nf_evar (evars_of isevars) j1)) let inh_coerce_to_fail env isevars c1 hj = let hj' = @@ -116,33 +116,34 @@ let inh_coerce_to_fail env isevars c1 hj = apply_coercion env p hj t2 with Not_found -> raise NoCoercion in - if the_conv_x_leq env isevars hj'.uj_type c1 then - hj' - else - raise NoCoercion + try (the_conv_x_leq env hj'.uj_type c1 isevars, hj') + with Reduction.NotConvertible -> raise NoCoercion let rec inh_conv_coerce_to_fail env isevars hj c1 = let {uj_val = v; uj_type = t} = hj in - if the_conv_x_leq env isevars t c1 then hj - else - try + try (the_conv_x_leq env t c1 isevars, hj) + with Reduction.NotConvertible -> + (try inh_coerce_to_fail env isevars c1 hj - with NoCoercion -> (* try ... with _ -> ... is BAD *) + 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' = whd_betadeltaiota env (evars_of isevars) v in - if (match kind_of_term v' with - | Lambda (_,v1,v2) -> - the_conv_x env isevars v1 u1 (* leq v1 u1? *) - | _ -> false) + let (evd',b) = + match kind_of_term v' with + | Lambda (_,v1,v2) -> + (try the_conv_x env v1 u1 isevars, true (* leq v1 u1? *) + with Reduction.NotConvertible -> (isevars, false)) + | _ -> (isevars,false) in + if b then let (x,v1,v2) = destLambda v' in let env1 = push_rel (x,None,v1) env in - let h2 = inh_conv_coerce_to_fail env1 isevars + let (evd'',h2) = inh_conv_coerce_to_fail env1 evd' {uj_val = v2; uj_type = t2 } u2 in - { uj_val = mkLambda (x, v1, h2.uj_val); - uj_type = mkProd (x, v1, h2.uj_type) } + (evd'',{ uj_val = mkLambda (x, v1, h2.uj_val); + uj_type = mkProd (x, v1, h2.uj_type) }) else (* 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)) *) @@ -151,57 +152,27 @@ let rec inh_conv_coerce_to_fail env isevars hj c1 = | Anonymous -> Name (id_of_string "x") | _ -> name) in let env1 = push_rel (name,None,u1) env in - let h1 = + let (evd',h1) = inh_conv_coerce_to_fail env1 isevars {uj_val = mkRel 1; uj_type = (lift 1 u1) } (lift 1 t1) in - let h2 = inh_conv_coerce_to_fail env1 isevars + let (evd'',h2) = inh_conv_coerce_to_fail env1 evd' { uj_val = mkApp (lift 1 v, [|h1.uj_val|]); uj_type = subst1 h1.uj_val t2 } u2 in - { uj_val = mkLambda (name, u1, h2.uj_val); - uj_type = mkProd (name, u1, h2.uj_type) } - | _ -> raise NoCoercion) + (evd'', + { uj_val = mkLambda (name, u1, h2.uj_val); + uj_type = mkProd (name, u1, h2.uj_type) }) + | _ -> 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 t = - let cj' = + let (evd',cj') = try inh_conv_coerce_to_fail env isevars cj t with NoCoercion -> let sigma = evars_of isevars in error_actual_type_loc loc env sigma cj t in - { uj_val = cj'.uj_val; uj_type = t } - -(* [inh_apply_rel_list loc env isevars args f tycon] tries to type [(f - args)] of type [tycon] (if any) by inserting coercions in front of - each arg$_i$, if necessary *) - -let inh_apply_rel_list apploc env isevars argjl (funloc,funj) tycon = - let rec apply_rec env n resj = function - | [] -> resj - | (loc,hj)::restjl -> - let sigma = evars_of isevars in - let resj = inh_app_fun env isevars resj in - let ntyp = whd_betadeltaiota env sigma resj.uj_type in - match kind_of_term ntyp with - | Prod (na,c1,c2) -> - let hj' = - try - inh_conv_coerce_to_fail env isevars hj c1 - with NoCoercion -> - error_cant_apply_bad_type_loc apploc env sigma - (1,c1,hj.uj_type) resj (List.map snd restjl) in - let newresj = - { uj_val = applist (j_val resj, [j_val hj']); - uj_type = subst1 hj'.uj_val c2 } in - apply_rec (push_rel (na,None,c1) env) (n+1) newresj restjl - | _ -> - error_cant_apply_not_functional_loc - (join_loc funloc loc) env sigma resj - (List.map snd restjl) - in - apply_rec env 1 funj argjl - + (evd',{ uj_val = cj'.uj_val; uj_type = t }) -- cgit v1.2.3