diff options
Diffstat (limited to 'contrib/subtac/subtac_coercion.ml')
| -rw-r--r-- | contrib/subtac/subtac_coercion.ml | 101 |
1 files changed, 59 insertions, 42 deletions
diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml index 3613ec4f..c764443f 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 9563 2007-01-31 09:37:18Z msozeau $ *) +(* $Id: subtac_coercion.ml 9976 2007-07-12 11:58:30Z msozeau $ *) open Util open Names @@ -26,7 +26,6 @@ open Subtac_utils open Coqlib open Printer open Subtac_errors -open Context open Eterm open Pp @@ -86,6 +85,13 @@ module Coercion = struct let hnf env isevars c = whd_betadeltaiota env (evars_of !isevars) c + let lift_args n sign = + let rec liftrec k = function + | t::sign -> liftn n k t :: (liftrec (k-1) sign) + | [] -> [] + in + liftrec (List.length sign) sign + let rec mu env isevars t = let isevars = ref isevars in let rec aux v = @@ -113,15 +119,41 @@ module Coercion = struct (* (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 _ -> ()); *) - None - with Reduction.NotConvertible -> coerce' env (hnf env isevars x) (hnf env isevars y) + let x = hnf env isevars x and y = hnf env isevars y in + 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 _ -> ()); *) + None + with Reduction.NotConvertible -> coerce' env x y and coerce' env x y : (Term.constr -> Term.constr) option = let subco () = subset_coerce env isevars x y in + let rec coerce_application typ c c' l l' = + let len = Array.length l in + let rec aux tele typ i co = + if i < len then + let hdx = l.(i) and hdy = l'.(i) in + try isevars := the_conv_x_leq env hdx hdy !isevars; + let (n, eqT, restT) = destProd typ in + aux (hdx :: tele) (subst1 hdy restT) (succ i) co + with Reduction.NotConvertible -> + let (n, eqT, restT) = destProd typ in + let restargs = lift_args 1 + (List.rev (Array.to_list (Array.sub l (succ i) (len - (succ i))))) + in + let args = List.rev (restargs @ mkRel 1 :: lift_args 1 tele) in + let pred = mkLambda (n, eqT, applistc (lift 1 c) args) in + let eq = mkApp (Lazy.force eq_ind, [| eqT; hdx; hdy |]) in +(* let jmeq = mkApp (Lazy.force jmeq_ind, [| eqT; hdx; eqT; 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 + trace (str"Inserting coercion at application"); + aux (hdy :: tele) (subst1 hdy restT) (succ i) (fun x -> eq_app (co x)) + else co + in aux [] typ 0 (fun x -> x) + in (* (try debug 1 (str "coerce' from " ++ (my_print_constr env x) ++ *) (* str " to "++ my_print_constr env y); *) (* with _ -> ()); *) @@ -214,40 +246,25 @@ module Coercion = struct mkApp (prod.intro, [| a'; b'; x ; y |])) end 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 () + if i = i' && len = Array.length l' then + let evm = evars_of !isevars in + let typ = Typing.type_of env evm c in + (try subco () + with NoSubtacCoercion -> + +(* if not (is_arity env evm typ) then *) + Some (coerce_application typ c c' l l')) +(* else subco () *) + 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 () + if Array.length l = Array.length l' then + let evm = evars_of !isevars in + let lam_type = Typing.type_of env evm c in +(* if not (is_arity env evm lam_type) then ( *) + Some (coerce_application lam_type c c' l l') +(* ) else subco () *) + else subco () | _ -> subco ()) | _, _ -> subco () |