diff options
Diffstat (limited to 'contrib/subtac/subtac_coercion.ml')
| -rw-r--r-- | contrib/subtac/subtac_coercion.ml | 168 |
1 files changed, 97 insertions, 71 deletions
diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml index da5c497c..3613ec4f 100644 --- a/contrib/subtac/subtac_coercion.ml +++ b/contrib/subtac/subtac_coercion.ml @@ -5,7 +5,7 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: subtac_coercion.ml 9284 2006-10-26 12:06:57Z msozeau $ *) +(* $Id: subtac_coercion.ml 9563 2007-01-31 09:37:18Z msozeau $ *) open Util open Names @@ -53,8 +53,6 @@ module Coercion = struct | _ -> None and disc_exist env x = - (try trace (str "Disc_exist: " ++ my_print_constr env x) - with _ -> ()); match kind_of_term x with | App (c, l) -> (match kind_of_term c with @@ -67,8 +65,6 @@ module Coercion = struct let disc_proj_exist env x = - (try trace (str "disc_proj_exist: " ++ my_print_constr env x); - with _ -> ()); match kind_of_term x with | App (c, l) -> (if Term.eq_constr c (Lazy.force sig_).proj1 @@ -108,27 +104,27 @@ module Coercion = struct : (Term.constr -> Term.constr) option = let x = nf_evar (evars_of !isevars) x and y = nf_evar (evars_of !isevars) y in - (try debug 1 (str "Coerce called for " ++ (my_print_constr env x) ++ - str " and "++ my_print_constr env y ++ - str " with evars: " ++ spc () ++ - my_print_evardefs !isevars); - with _ -> ()); +(* (try debug 1 (str "Coerce called for " ++ (my_print_constr env x) ++ *) +(* str " and "++ my_print_constr env y ++ *) +(* str " with evars: " ++ spc () ++ *) +(* my_print_evardefs !isevars); *) +(* with _ -> ()); *) let rec coerce_unify env x y = - (try debug 1 (str "coerce_unify from " ++ (my_print_constr env x) ++ - str " to "++ my_print_constr env y) - with _ -> ()); +(* (try debug 1 (str "coerce_unify from " ++ (my_print_constr env x) ++ *) +(* str " to "++ my_print_constr env y) *) +(* with _ -> ()); *) try isevars := the_conv_x_leq env x y !isevars; - (try debug 1 (str "Unified " ++ (my_print_constr env x) ++ - str " and "++ my_print_constr env y); - with _ -> ()); +(* (try debug 1 (str "Unified " ++ (my_print_constr env x) ++ *) +(* str " and "++ my_print_constr env y); *) +(* with _ -> ()); *) None with Reduction.NotConvertible -> coerce' env (hnf env isevars x) (hnf env isevars y) and coerce' env x y : (Term.constr -> Term.constr) option = let subco () = subset_coerce env isevars x y in - (try debug 1 (str "coerce' from " ++ (my_print_constr env x) ++ - str " to "++ my_print_constr env y); - with _ -> ()); +(* (try debug 1 (str "coerce' from " ++ (my_print_constr env x) ++ *) +(* str " to "++ my_print_constr env y); *) +(* with _ -> ()); *) match (kind_of_term x, kind_of_term y) with | Sort s, Sort s' -> (match s, s' with @@ -158,11 +154,11 @@ module Coercion = struct let existS = Lazy.force existS in let prod = Lazy.force prod in if len = Array.length l' && len = 2 && i = i' + && (i = Term.destInd existS.typ || i = Term.destInd prod.typ) then if i = Term.destInd existS.typ then begin - trace (str "In coerce sigma types"); let (a, pb), (a', pb') = pair_of_array l, pair_of_array l' in @@ -185,7 +181,6 @@ module Coercion = struct let c2 = coerce_unify env' b b' in match c1, c2 with None, None -> - trace (str "No coercion needed"); None | _, _ -> Some @@ -198,9 +193,8 @@ module Coercion = struct in mkApp (existS.intro, [| a'; pb'; x ; y |])) end - else if i = Term.destInd prod.typ then + else begin - debug 1 (str "In coerce prod types"); let (a, b), (a', b') = pair_of_array l, pair_of_array l' in @@ -219,14 +213,48 @@ module Coercion = struct in mkApp (prod.intro, [| a'; b'; x ; y |])) end - else subco () - else subco () - | _ -> subco ()) + else + (* if len = 1 && len = Array.length l' && i = i' then *) +(* let argx, argy = l.(0), l'.(0) in *) +(* let indtyp = Inductiveops.type_of_inductive env i in *) +(* let argname, argtype, _ = destProd indtyp in *) +(* let eq = *) +(* mkApp (Lazy.force eqind, [| argtype; argx; argy |]) *) +(* in *) +(* let pred = mkLambda (argname, argtype, *) +(* mkApp (mkInd i, [| mkRel 1 |])) *) +(* in *) +(* let evar = make_existential dummy_loc env isevars eq in *) +(* Some (fun x -> *) +(* mkApp (Lazy.force eqrec, *) +(* [| argtype; argx; pred; x; argy; evar |])) *) +(* else *)subco () + | x, y when x = y -> + let lam_type = Typing.type_of env (evars_of !isevars) c in + let rec coerce typ i co = + if i < Array.length l then + let hdx = l.(i) and hdy = l'.(i) in + let (n, eqT, restT) = destProd typ in + let pred = mkLambda (n, eqT, mkApp (lift 1 c, [| mkRel 1 |])) in + let eq = mkApp (Lazy.force eq_ind, [| eqT; hdx; hdy |]) in + let evar = make_existential dummy_loc env isevars eq in + let eq_app x = mkApp (Lazy.force eq_rect, + [| eqT; hdx; pred; x; hdy; evar|]) + in + coerce (subst1 hdy restT) (succ i) (fun x -> eq_app (co x)) + else co + in + if Array.length l = Array.length l' then ( + trace (str"Inserting coercion at application"); + Some (coerce lam_type 0 (fun x -> x)) + ) else subco () + | _ -> subco ()) | _, _ -> subco () and subset_coerce env isevars x y = match disc_subset x with Some (u, p) -> + (* trace (str "Inserting projection "); *) let c = coerce_unify env u y in let f x = app_opt c (mkApp ((Lazy.force sig_).proj1, @@ -372,13 +400,13 @@ module Coercion = struct with Reduction.NotConvertible -> raise NoCoercion let rec inh_conv_coerce_to_fail loc env isevars 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 () ++ - Evd.pr_evar_defs isevars ++ str " in env: " ++ spc () ++ - Termops.print_env env); - with _ -> ()); +(* (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 () ++ *) +(* Termops.print_env env); *) +(* with _ -> ()); *) try (the_conv_x_leq env t c1 isevars, v, t) with Reduction.NotConvertible -> (try @@ -437,14 +465,14 @@ module Coercion = struct (* 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) = - (try - debug 1 (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 () ++ - Evd.pr_evar_defs isevars ++ str " in env: " ++ spc () ++ - Termops.print_env env); - with _ -> ()); + let inh_conv_coerce_to loc env isevars 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 () ++ *) +(* Termops.print_env env); *) +(* with _ -> ()); *) match n with None -> let (evd', val', type') = @@ -462,40 +490,38 @@ module Coercion = struct | Some (init, cur) -> (isevars, cj) - let inh_conv_coerces_to loc env isevars t ((abs, t') as tycon) = - (try - debug 1 (str "Subtac_coercion.inh_conv_coerces_to called for " ++ - Termops.print_constr_env env t ++ str " and "++ spc () ++ - Evarutil.pr_tycon_type env tycon ++ str " with evars: " ++ spc () ++ - Evd.pr_evar_defs isevars ++ str " in env: " ++ spc () ++ - Termops.print_env env); - with _ -> ()); + let inh_conv_coerces_to loc env isevars t ((abs, t') as _tycon) = +(* (try *) +(* trace (str "Subtac_coercion.inh_conv_coerces_to called for " ++ *) +(* Termops.print_constr_env env t ++ str " and "++ spc () ++ *) +(* Evarutil.pr_tycon_type env tycon ++ str " with evars: " ++ spc () ++ *) +(* Evd.pr_evar_defs isevars ++ str " in env: " ++ spc () ++ *) +(* Termops.print_env env); *) +(* with _ -> ()); *) let nabsinit, nabs = match abs with None -> 0, 0 | Some (init, cur) -> init, cur in - let (rels, rng) = (* a little more effort to get products is needed *) - try decompose_prod_n nabs t - with _ -> - trace (str "decompose_prod_n failed"); - raise (Invalid_argument "Subtac_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 ( - trace (str "No occur between 0 and " ++ int (succ nabsinit)); - 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 - pi1 (try inh_conv_coerce_to_fail loc env' isevars None t t' - with NoCoercion -> - coerce_itf loc env' isevars None t t') - with NoSubtacCoercion -> - let sigma = evars_of isevars in - error_cannot_coerce env' sigma (t, t')) - else isevars + try let rels, rng = decompose_prod_n nabs t 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 ( +(* trace (str "No occur between 0 and " ++ int (succ nabsinit)); *) + 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 + pi1 (try inh_conv_coerce_to_fail loc env' isevars None t t' + with NoCoercion -> + coerce_itf loc env' isevars None t t') + with NoSubtacCoercion -> + let sigma = evars_of isevars in + error_cannot_coerce env' sigma (t, t')) + else isevars + with _ -> isevars + (* trace (str "decompose_prod_n failed"); *) + (* raise (Invalid_argument "Subtac_coercion.inh_conv_coerces_to") *) end |