From 3ef7797ef6fc605dfafb32523261fe1b023aeecb Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 28 Apr 2006 14:59:16 +0000 Subject: Imported Upstream version 8.0pl3+8.1alpha --- pretyping/coercion.ml | 425 ++++++++++++++++++++++++++++---------------------- 1 file changed, 242 insertions(+), 183 deletions(-) (limited to 'pretyping/coercion.ml') diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index be78eb2c..e01dac47 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,v 1.38.6.2 2005/11/29 21:40:52 letouzey Exp $ *) +(* $Id: coercion.ml 8695 2006-04-10 16:33:52Z msozeau $ *) open Util open Names @@ -19,189 +19,248 @@ open Recordops open Evarutil open Evarconv open Retyping +open Evd -(* Typing operations dealing with coercions *) - -let class_of1 env sigma t = class_of env sigma (nf_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 - -exception NoCoercion - -(* 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 - 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 (_,_,_) -> 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 } - | _ -> - (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) - -let inh_tosort_force env isevars j = - try - let t,i1 = class_of1 env (evars_of isevars) j.uj_type in - let p = lookup_path_to_sort_from i1 in - apply_coercion env p j t - with Not_found -> - 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 } - | 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 j1 = inh_tosort_force env isevars j in - type_judgment env (j_nf_evar (evars_of isevars) j1) - -let inh_coerce_to_fail env isevars c1 hj = - let hj' = - try - let t1,i1 = class_of1 env (evars_of isevars) c1 in - let t2,i2 = class_of1 env (evars_of isevars) hj.uj_type in - let p = lookup_path_between (i2,i1) in - 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 - -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 - inh_coerce_to_fail env isevars c1 hj - with NoCoercion -> (* try ... with _ -> ... is BAD *) - (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) - 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 - {uj_val = v2; uj_type = t2 } u2 in - { 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)) *) - (* 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 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 - { 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) - -(* 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' = +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_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 class_of1 env sigma t = class_of env sigma (nf_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 - 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' = + 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 when not (is_defined_evar isevars 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 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 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)) + 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_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 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 + 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_app (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_app (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_app (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_app (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 + let nf = nf_isevar evd' in + (evd',{ uj_val = nf val'; uj_type = nf 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 - inh_conv_coerce_to_fail env isevars hj c1 + pi1 (inh_conv_coerce_to_fail loc env' isevars None t t') 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 - + 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 -- cgit v1.2.3