From fc10282837971f8f0648841d944dd64b11d3a3db Mon Sep 17 00:00:00 2001 From: herbelin Date: Sat, 26 Apr 2008 12:31:25 +0000 Subject: - Backtrack sur extension de syntaxe pour pose qui rentre en conflit avec "pose as" de Program. - Report des modifs de coercion.ml (révision 10840) dans subtac_coercion.ml. - Comportement de "simple apply" rendu plus proche de celui du apply 8.1 MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10854 85f007b7-540e-0410-9357-904b9bb8a0f7 --- contrib/subtac/subtac_coercion.ml | 119 +++++++++++++++----------------------- 1 file changed, 47 insertions(+), 72 deletions(-) (limited to 'contrib') diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml index 9eac4fbae..2569404b0 100644 --- a/contrib/subtac/subtac_coercion.ml +++ b/contrib/subtac/subtac_coercion.ml @@ -314,7 +314,7 @@ module Coercion = struct let coerce_itf loc env isevars v t c1 = let evars = ref isevars in let coercion = coerce loc env evars t c1 in - !evars, Option.map (app_opt coercion) v, t + !evars, Option.map (app_opt coercion) v (* Taken from pretyping/coercion.ml *) @@ -416,11 +416,15 @@ module Coercion = struct uj_type = typ' } - let inh_coerce_to_fail env isevars c1 v 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 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 (evars_of evd) c1 in + let t2,i2 = class_of1 env (evars_of evd) t in let p = lookup_path_between (i2,i1) in match v with Some v -> @@ -429,102 +433,73 @@ module Coercion = struct | None -> None, t with Not_found -> raise NoCoercion in - try (the_conv_x_leq env t' c1 isevars, v', t') + try (the_conv_x_leq env t' c1 evd, v') with Reduction.NotConvertible -> raise NoCoercion - let rec inh_conv_coerce_to_fail loc env isevars v t c1 = + + let rec inh_conv_coerce_to_fail loc env evd rigidonly v t c1 = (* (try *) (* debug 1 (str "inh_conv_coerce_to_fail called for " ++ *) (* Termops.print_constr_env env t ++ str " and "++ spc () ++ *) (* Termops.print_constr_env env c1 ++ str " with evars: " ++ spc () ++ *) -(* Subtac_utils.pr_evar_defs isevars ++ str " in env: " ++ spc () ++ *) +(* Subtac_utils.pr_evar_defs evd ++ str " in env: " ++ spc () ++ *) (* Termops.print_env env); *) (* with _ -> ()); *) - try (the_conv_x_leq env t c1 isevars, v, t) + try (the_conv_x_leq env t c1 evd, v) 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 evd rigidonly v t c1 + with NoCoercion -> + match + kind_of_term (whd_betadeltaiota env (evars_of evd) t), + kind_of_term (whd_betadeltaiota env (evars_of 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) *) + 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) = + 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 = Termops.subst_term v1 t2 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 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) as _tycon) = + let inh_conv_coerce_to_gen rigidonly loc env evd cj ((n, t) as _tycon) = (* (try *) (* trace (str "Subtac_coercion.inh_conv_coerce_to called for " ++ *) (* Termops.print_constr_env env cj.uj_type ++ str " and "++ spc () ++ *) (* Evarutil.pr_tycon_type env tycon ++ str " with evars: " ++ spc () ++ *) -(* Subtac_utils.pr_evar_defs isevars ++ str " in env: " ++ spc () ++ *) +(* Subtac_utils.pr_evar_defs evd ++ str " in env: " ++ spc () ++ *) (* Termops.print_env env); *) (* with _ -> ()); *) match n with None -> - let (evd', val', type') = + let (evd', val') = try - inh_conv_coerce_to_fail loc env isevars (Some cj.uj_val) cj.uj_type t + inh_conv_coerce_to_fail loc env evd rigidonly (Some cj.uj_val) cj.uj_type t with NoCoercion -> - let sigma = evars_of isevars in + let sigma = evars_of evd in try - coerce_itf loc env isevars (Some cj.uj_val) cj.uj_type t + coerce_itf loc env evd (Some cj.uj_val) cj.uj_type t with NoSubtacCoercion -> 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) + (evd, cj) - let inh_conv_coerce_rigid_to _ _ _ _ _ = - failwith "inh_conv_coerce_rigid_to: TODO" + let inh_conv_coerce_to = inh_conv_coerce_to_gen false + let inh_conv_coerce_rigid_to = inh_conv_coerce_to_gen true let inh_conv_coerces_to loc env isevars t ((abs, t') as _tycon) = (* (try *) @@ -550,7 +525,7 @@ module Coercion = struct env', rng, lift nabs t' in try - pi1 (try inh_conv_coerce_to_fail loc env' isevars None t t' + fst (try inh_conv_coerce_to_fail loc env' isevars false None t t' with NoCoercion -> coerce_itf loc env' isevars None t t') with NoSubtacCoercion -> -- cgit v1.2.3