From 9f36277960309addcb203351d81b067397dd07dc Mon Sep 17 00:00:00 2001 From: herbelin Date: Fri, 6 Oct 2006 18:45:03 +0000 Subject: Remplacement des nf_evar (source de complexité polynomiale) par de la réduction paresseuse. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Accessoirement, suppression d'un test evar_defined inutile car sur résultat de whd_betadeltaiota qui contient la réduction evar de tête dans coercion.ml; code mort du commit précédent dans pretyping.ml. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9223 85f007b7-540e-0410-9357-904b9bb8a0f7 --- pretyping/coercion.ml | 20 +++++++++++++------- pretyping/pretyping.ml | 7 ------- 2 files changed, 13 insertions(+), 14 deletions(-) diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 8a55a46d2..30848ded1 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -20,6 +20,7 @@ open Evarutil open Evarconv open Retyping open Evd +open Termops module type S = sig (*s Coercions. *) @@ -66,7 +67,12 @@ module Default = struct (* Typing operations dealing with coercions *) exception NoCoercion - let class_of1 env sigma t = class_of env sigma (nf_evar sigma t) + let whd_app_evar sigma t = + match kind_of_term t with + | App (f,l) -> mkApp (whd_evar sigma f,l) + | _ -> whd_evar sigma t + + let class_of1 env sigma t = class_of env sigma (whd_app_evar sigma t) (* Here, funj is a coercion therefore already typed in global context *) let apply_coercion_args env argl funj = @@ -120,7 +126,7 @@ module Default = struct 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) -> + | Evar ev -> let (isevars',t) = define_evar_as_arrow isevars ev in (isevars',{ uj_val = j.uj_val; uj_type = t }) | _ -> @@ -135,7 +141,8 @@ module Default = struct 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)) + let j2 = on_judgment_type (whd_evar (evars_of isevars)) j1 in + (isevars,type_judgment env j2) with Not_found -> error_not_a_type_loc loc env (evars_of isevars) j @@ -166,7 +173,7 @@ module Default = struct 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 -> @@ -223,7 +230,7 @@ module Default = struct (evd'', option_map (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 @@ -236,8 +243,7 @@ module Default = struct 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 }) + (evd',{ uj_val = val'; uj_type = t }) | Some (init, cur) -> (isevars, cj) let inh_conv_coerces_to loc env (isevars : evar_defs) t (abs, t') = isevars diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 1f13586dd..a94dc0451 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -194,13 +194,6 @@ module Pretyping_F (Coercion : Coercion.S) = struct | None -> j | Some t -> evd_comb2 (Coercion.inh_conv_coerce_to loc env) isevars j t - let inh_conv_coerce_to_tycon loc env isevars j = function - | None -> j - | Some t -> - let (evd',z) = Coercion.inh_conv_coerce_to loc env !isevars j t in - isevars := evd'; - z - let push_rels vars env = List.fold_right push_rel vars env (* -- cgit v1.2.3