Backtrack sur la mémoïsation de nf_evar.

L'expérience prouve que ce n'est pas franchement concluant.
On peut se risquer à une explication :
 - nf_evar, version mémoïsée n'est pas tail recursive
 - On retarde la substitution des hypothèses de l'evar en échange de
faire moins de substitutions d'evars. Intuitivement c'est intéressant
seulement si il y a plus de substitutions d'evar dupliquées que
d'hypothèses dupliquées. Ce qui ne doit pas être le cas (ne serait-ce
que parce que dupliquer une evar duplique aussi ses variables libres).

This reverts commit 066a564021788e995eb166ad6ed6e55611d6f593.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11958 85f007b7-540e-0410-9357-904b9bb8a0f7

8 files changed, 49 insertions, 174 deletions

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index d0ed4f1363..29b5b87a7d 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -58,10 +58,10 @@ let jv_nf_evar = Pretype_errors.jv_nf_evar
 let tj_nf_evar = Pretype_errors.tj_nf_evar
 
 let nf_named_context_evar sigma ctx = 
-  Sign.map_named_context (Evd.nf_evar sigma) ctx
+  Sign.map_named_context (Reductionops.nf_evar sigma) ctx
 
 let nf_rel_context_evar sigma ctx = 
-  Sign.map_rel_context (Evd.nf_evar sigma) ctx
+  Sign.map_rel_context (Reductionops.nf_evar sigma) ctx
     
 let nf_env_evar sigma env = 
   let nc' = nf_named_context_evar sigma (Environ.named_context env) in
@@ -70,11 +70,11 @@ let nf_env_evar sigma env =
 
 let nf_evar_info evc info =
   { info with 
-    evar_concl = Evd.nf_evar evc info.evar_concl;
-    evar_hyps = map_named_val (Evd.nf_evar evc) info.evar_hyps;
+    evar_concl = Reductionops.nf_evar evc info.evar_concl;
+    evar_hyps = map_named_val (Reductionops.nf_evar evc) info.evar_hyps;
     evar_body = match info.evar_body with
       | Evar_empty -> Evar_empty
-      | Evar_defined c -> Evar_defined (Evd.nf_evar evc c) }
+      | Evar_defined c -> Evar_defined (Reductionops.nf_evar evc c) }
 
 let nf_evars evm = Evd.fold (fun ev evi evm' -> Evd.add evm' ev (nf_evar_info evm evi))
 		     evm Evd.empty
@@ -112,7 +112,7 @@ let push_dependent_evars sigma emap =
   Evd.fold (fun ev {evar_concl = ccl} (sigma',emap') ->
     List.fold_left 
       (fun (sigma',emap') ev -> 
-	(Evd.add sigma' ev (Evd.find emap' ev),Evd.unsafe_remove emap' ev))
+	(Evd.add sigma' ev (Evd.find emap' ev),Evd.remove emap' ev))
       (sigma',emap') (collect_evars emap' ccl))
     emap (sigma,emap)
 
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index a5d36f9141..6bc77abcb6 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -65,9 +65,9 @@ let eq_evar_info ei1 ei2 =
 
 (* spiwack: Revised hierarchy :
       - ExistentialMap ( Maps of existential_keys )
-      - EvarInfoMap ( .t ~ evar_info ExistentialMap.t )
+      - EvarInfoMap ( .t = evar_info ExistentialMap.t )
       - EvarMap ( .t = EvarInfoMap.t * sort_constraints )
-      - evar_defs (= unification states, exported)
+      - evar_defs (exported)
 *)
 
 module ExistentialMap = Intmap
@@ -77,65 +77,24 @@ module ExistentialSet = Intset
 exception NotInstantiatedEvar
 
 module EvarInfoMap = struct
-   (**************************************************************
-    * EvarInfoMap represents maps from [evar] to [evar_info] (that is
-    * a structure which associates to existential variables their type
-    * and possibly their definition (aka body)) plus certain cached
-    * information (values of [whd_evar] and [nf_evar] on those 
-    * existential variables before substituting anything for their 
-    * hypotheses).
-    * Caches are represented as mutable cells (in the type 
-    * [cached_info] which encapsulates [evar_info]) to keep caching 
-    * transparent to the interface. The down side of using mutable 
-    * cells in a persistant data-structure is that mutations influence
-    * past versions of the structure. To ensure that the structure stays
-    * pure we have to  track a "version number" together with the 
-    * cache. If the cache is more recent than the structure then it is
-    * considered inconsistent and discarded.
-    * The price is that we cannot say much about the effect of 
-    * caching in the worst case. Also caching makes [nf_evar]
-    * and [whd_evar] non-tail recursive (because substitution of
-    * the hypotheses is delayed). Which may make them inefficient
-    * in some cases.
-    *************************************************************)
-
-
-  (* Invariant: whd and nf are [None] while evar_info.evar_body is [Evar_Empty] *)
-  type cached_info = { 
-      evar_info : evar_info ;
-      (* stores the last computed whd of the existential variale. *)
-      mutable whd : (int*constr) option;
-      (* stores the last computed nf (=fully instantiated value) of the existential var.*)
-      mutable nf : (int*constr) option
-  } 
-  let empty_cache ei = { evar_info=ei;whd=None;nf=None }
-
-  (* mapping * version number *)
-  type t = cached_info ExistentialMap.t*int
-
-  let empty = (ExistentialMap.empty,0)
-
-  let to_list (evc,_) = (* Workaround for change in Map.fold behavior *)
-    let l = ref [] in 
-    ExistentialMap.iter (fun evk x -> l := (evk,x.evar_info)::!l) evc;
-    !l
+  type t = evar_info ExistentialMap.t
 
-  let dom (evc,_) = ExistentialMap.fold (fun evk _ acc -> evk::acc) evc []
-  let find (evc,_) k = (ExistentialMap.find k evc).evar_info
-  let mem (evc,_) k = ExistentialMap.mem k evc
+  let empty = ExistentialMap.empty
 
-  let add (evd,v) evk newinfo =  
-    (ExistentialMap.add evk (empty_cache newinfo) evd,v+1)
+  let to_list evc = (* Workaround for change in Map.fold behavior *)
+    let l = ref [] in 
+    ExistentialMap.iter (fun evk x -> l := (evk,x)::!l) evc;
+    !l
 
-  (* spiwack: this should be considered deprecated *)
-  let unsafe_remove (evc,v) k = (ExistentialMap.remove k evc,v+1)
+  let dom evc = ExistentialMap.fold (fun evk _ acc -> evk::acc) evc []
+  let find evc k = ExistentialMap.find k evc
+  let remove evc k = ExistentialMap.remove k evc
+  let mem evc k = ExistentialMap.mem k evc
+  let fold = ExistentialMap.fold
 
-  let map f (evc,v)= 
-    (ExistentialMap.map (fun ci -> empty_cache (f ci.evar_info)) evc,0)
-  let fold f (evc,_)= ExistentialMap.fold (fun evk ci acc -> f evk ci.evar_info acc) evc
+  let add evd evk newinfo =  ExistentialMap.add evk newinfo evd
 
-  let equal f (evc1,_) (evc2,_) = 
-    ExistentialMap.equal (fun ci1 ci2 -> f ci1.evar_info ci2.evar_info) evc1 evc2
+  let equal = ExistentialMap.equal
 
   let define evd evk body = 
     let oldinfo =
@@ -145,7 +104,7 @@ module EvarInfoMap = struct
       { oldinfo with
 	  evar_body = Evar_defined body } in
       match oldinfo.evar_body with
-	| Evar_empty -> add evd evk newinfo
+	| Evar_empty -> ExistentialMap.add evk newinfo evd
 	| _ -> anomaly "Evd.define: cannot define an evar twice"
 
   let is_evar sigma evk = mem sigma evk
@@ -192,82 +151,19 @@ module EvarInfoMap = struct
     let hyps = evar_filtered_context info in
       instantiate_evar hyps info.evar_concl (Array.to_list args)
 
-  let get_evar_body evi =
-    match evar_body evi with
-      | Evar_defined c -> c 
-      | Evar_empty -> raise NotInstantiatedEvar
-    
   let existential_value sigma (n,args) =
     let info = find sigma n in
     let hyps = evar_filtered_context info in
-    let c = get_evar_body info in
-    instantiate_evar hyps c (Array.to_list args)
+      match evar_body info with
+	| Evar_defined c ->
+	    instantiate_evar hyps c (Array.to_list args)
+	| Evar_empty ->
+	    raise NotInstantiatedEvar
 
   let existential_opt_value sigma ev =
     try Some (existential_value sigma ev)
     with NotInstantiatedEvar -> None
 
-  (*** Computing instantiated forms of existential variables. ***)
-
-  let get_whd_cache ci = ci.whd
-  let set_whd_cache ci v c = ci.whd <- Some (v,c)
-  let get_nf_cache ci = ci.nf
-  let set_nf_cache ci v c = ci.nf <- Some (v,c)
-
-  (* [inst_gen] is the prototype for [whd_evar] and [nf_evar]. It takes
-      as additional parameters a pair of arguments [set]/[get] which 
-      are meant to respectively cache a ([constr]) value (together with
-      a version number) and return the value previously cached by [set].
-      It also takes an argument [r] which specifies what to do on non-[Evar]
-      terms. That is "just return it" for [whd_evar], and "operate recursively
-      on subterms" for [nf_evar]. *)
-  let rec inst_gen set get r sigma c =
-    match kind_of_term c with
-      | Evar (e,args) -> 
-	  begin try 
-	    let (c',hyps) = inst_gen_of_evar set get r sigma e in
-	    instantiate_evar hyps c' (Array.to_list args)
-	  with Not_found | NotInstantiatedEvar -> c end
-      | _ -> r c
-  and inst_gen_of_evar set get r ((sigma,v) as evc) e =
-    let oci =  ExistentialMap.find e sigma in
-    let info = oci.evar_info in
-    let hyps = evar_filtered_context info in
-    match get oci with
-      | None ->
-	  (* The cache is empty. 
-	      We call [inst_gen] recursively to construct the cache. *)
-	  let c = get_evar_body info in
-	  let c' = inst_gen set get r evc c in
-	  set oci v c';
-	  (c', hyps)
-      | Some (v',_) when v' > v ->
-	  (* This is a copy of previous case. It'd be better to factorise it somehow,
-	      but "when" clauses cannot operate on operands of or-patterns. *)
-	  (* The cache is inconsistent (comes from a future version
-	      of the map). 
-	      We call [inst_gen] recursively to construct the cache. *)
-	  let c = get_evar_body info in
-	  let c' = inst_gen set get r evc c in
-	  set oci v c';
-	  (c', hyps)
-      | Some (v',c) when v' < v -> 
-	  (* The cache is consistent but not necessarily complete. 
-	      It comes from a past version of the map.
-	      We call [inst_gen] recursively on the cached value, 
-	      and update the cache. *)
-	  let c' = inst_gen set get r evc c in
-	  set oci v c';
-	  (c', hyps)
-      | Some (_,c') (*when v'=v *) ->
-	  (* The cache is fully consistent, as it has been made on
-	      this version of the map. We can simply return it. *)
-	  (c', hyps)
-
-  let  whd_evar = inst_gen set_whd_cache get_whd_cache Util.identity
-  let rec nf_evar sigma c = 
-    inst_gen set_nf_cache get_nf_cache (map_constr  (nf_evar sigma)) sigma c
-
 end
 
 (*******************************************************************)
@@ -341,11 +237,6 @@ let is_sort_var s scstr =
         with Not_found -> false)
     | _ -> false
 
-let rec nf_sort_var scstr t =
-  match kind_of_term t with
-    | Sort s when is_sort_var s scstr -> whd_sort_var scstr t
-    | _ -> map_constr (nf_sort_var scstr) t
-
 let new_sort_var cstr =
   let u = Termops.new_univ() in
   (u, UniverseMap.add u (SortVar([],[])) cstr)
@@ -414,8 +305,7 @@ module EvarMap = struct
   let add (sigma,sm) k v = (EvarInfoMap.add sigma k v, sm)
   let dom (sigma,_) = EvarInfoMap.dom sigma
   let find (sigma,_) = EvarInfoMap.find sigma
-  (* spiwack: unsafe_remove should be considered deprecated *)
-  let unsafe_remove (sigma,sm) k = (EvarInfoMap.unsafe_remove sigma k, sm)
+  let remove (sigma,sm) k = (EvarInfoMap.remove sigma k, sm)
   let mem (sigma,_) = EvarInfoMap.mem sigma
   let to_list (sigma,_) = EvarInfoMap.to_list sigma
   let fold f (sigma,_) = EvarInfoMap.fold f sigma
@@ -431,17 +321,6 @@ module EvarMap = struct
 
   let merge e e' = fold (fun n v sigma -> add sigma n v) e' e
   
-  let whd_evar (sigma,sm) c =
-    let c = EvarInfoMap.whd_evar sigma c in
-    match kind_of_term c with
-      | Sort s when is_sort_var s sm -> whd_sort_var sm c
-      | _ -> c
-
-
-  let nf_evar (sigma,sm) c =
-    let c = EvarInfoMap.nf_evar sigma c in
-    nf_sort_var sm c
-
 end
  
 (*******************************************************************)
@@ -567,8 +446,7 @@ let merge d1 d2 = {
   metas = Metamap.fold (fun k m r -> Metamap.add k m r) d2.metas d1.metas
 }
 let add d e i = { d with evars=EvarMap.add d.evars e i }
-(* spiwack: unsafe_remove should be considered deprecated *)
-let unsafe_remove d e = { d with evars=EvarMap.unsafe_remove d.evars e }
+let remove d e = { d with evars=EvarMap.remove d.evars e }
 let dom d = EvarMap.dom d.evars
 let find d e = EvarMap.find d.evars e
 let mem d e = EvarMap.mem d.evars e
@@ -608,7 +486,7 @@ let subst_evar_defs_light sub evd =
   assert (evd.conv_pbs = []);
   { evd with
       metas = Metamap.map (map_clb (subst_mps sub)) evd.metas;
-      evars = EvarInfoMap.map (subst_evar_info sub)  (fst evd.evars), snd evd.evars
+      evars = ExistentialMap.map (subst_evar_info sub)  (fst evd.evars), snd evd.evars
   }
 
 let subst_evar_map = subst_evar_defs_light
@@ -701,8 +579,6 @@ let extract_all_conv_pbs evd =
 let evar_merge evd evars =
   { evd with evars = EvarMap.merge evd.evars evars.evars }
 
-
-
 (**********************************************************)
 (* Sort variables *)
 
@@ -719,12 +595,6 @@ let define_sort_variable ({evars=(sigma,sm)}as d) u s =
 let pr_sort_constraints {evars=(_,sm)} = pr_sort_cstrs sm
 
 (**********************************************************)
-(* Substitution of existential variables  *)
-
-let whd_evar { evars=em } t = EvarMap.whd_evar em t
-let nf_evar { evars=em } t = EvarMap.nf_evar em t
-
-(**********************************************************)
 (* Accessing metas *)
 
 let meta_list evd = metamap_to_list evd.metas
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index da1cfd130e..ac708d1ec7 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -132,6 +132,7 @@ val add : evar_defs -> evar -> evar_info -> evar_defs
 
 val dom : evar_defs -> evar list
 val find : evar_defs -> evar -> evar_info
+val remove : evar_defs -> evar -> evar_defs
 val mem : evar_defs -> evar -> bool
 val to_list : evar_defs -> (evar * evar_info) list
 val fold : (evar -> evar_info -> 'a -> 'a) -> evar_defs -> 'a -> 'a
@@ -239,13 +240,6 @@ val whd_sort_variable : evar_defs -> constr -> constr
 val set_leq_sort_variable : evar_defs -> sorts -> sorts -> evar_defs
 val define_sort_variable : evar_defs -> sorts -> sorts -> evar_defs
 
-
-(**********************************************************)
-(* Substitution of existential variables  *)
-
-val whd_evar : evar_defs -> constr -> constr
-val nf_evar : evar_defs -> constr -> constr
-
 (*********************************************************************)
 (* constr with holes *)
 type open_constr = evar_defs * constr
@@ -281,5 +275,4 @@ val create_evar_defs      : evar_defs -> evar_defs
 val create_goal_evar_defs : evar_defs -> evar_defs
 val is_defined_evar :  evar_defs -> existential -> bool
 val subst_evar_map : substitution -> evar_defs -> evar_defs
-val unsafe_remove : evar_defs -> evar -> evar_defs
 (*** /Deprecaded ***)
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index ef154620f7..06d1aa533b 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -46,7 +46,7 @@ let precatchable_exception = function
     Nametab.GlobalizationError _ | PretypeError _)) -> true
   | _ -> false
 
-let nf_evar = Evd.nf_evar
+let nf_evar = Reductionops.nf_evar
 let j_nf_evar sigma j = 
   { uj_val = nf_evar sigma j.uj_val;
     uj_type = nf_evar sigma j.uj_type }
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 37b65cf907..b6749db198 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -311,7 +311,7 @@ let is_open_canonical_projection sigma (c,args) =
   try 
     let l = Refmap.find (global_of_constr c) !object_table in
     let n = (snd (List.hd l)).o_NPARAMS in
-    try isEvar (Evd.whd_evar sigma (List.nth args n)) with Failure _ -> false
+    try isEvar (whd_evar sigma (List.nth args n)) with Failure _ -> false
   with Not_found -> false
 
 let freeze () =
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 53b23af123..38ac3485b2 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -490,6 +490,18 @@ let whd_eta c = app_stack (local_whd_state_gen eta Evd.empty (c,empty_stack))
 (*                   Reduction Functions                                    *)
 (****************************************************************************)
 
+(* Replacing defined evars for error messages *)
+let rec whd_evar sigma c =
+  match kind_of_term c with
+    | Evar ev ->
+        (match safe_evar_value sigma ev with
+            Some c -> whd_evar sigma c
+          | None -> c)
+    | Sort s when is_sort_variable sigma s -> whd_sort_variable sigma c
+    | _ -> c
+
+let nf_evar =
+  local_strong whd_evar
 
 (* lazy reduction functions. The infos must be created for each term *)
 (* Note by HH [oct 08] : why would it be the job of clos_norm_flags to add
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 902c314b53..535101d743 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -91,11 +91,11 @@ val clos_norm_flags : Closure.RedFlags.reds -> reduction_function
 val nf_beta : local_reduction_function
 val nf_betaiota : local_reduction_function
 val nf_betadeltaiota : reduction_function
-(* arnaud: val nf_evar : evar_map -> constr -> constr *)
+val nf_evar : evar_map -> constr -> constr
 
 val nf_betaiota_preserving_vm_cast : reduction_function
 (* Lazy strategy, weak head reduction *)
-(* arnaud: val whd_evar :  evar_map -> constr -> constr*)
+val whd_evar :  evar_map -> constr -> constr
 val whd_beta : local_reduction_function
 val whd_betaiota : local_reduction_function
 val whd_betaiotazeta : local_reduction_function
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 3f2d0b4251..3323c75b48 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -125,7 +125,7 @@ let retype sigma metamap =
     | _ -> family_of_sort (decomp_sort env sigma (type_of env t))
 
   and type_of_global_reference_knowing_parameters env c args =
-    let argtyps = Array.map (fun c -> Evd.nf_evar sigma (type_of env c)) args in
+    let argtyps = Array.map (fun c -> nf_evar sigma (type_of env c)) args in
     match kind_of_term c with
     | Ind ind ->
       let (_,mip) = lookup_mind_specif env ind in
@@ -146,7 +146,7 @@ let type_of_global_reference_knowing_parameters env sigma c args =
   let _,_,_,f = retype sigma [] in f env c args
 
 let type_of_global_reference_knowing_conclusion env sigma c conclty =
-  let conclty = Evd.nf_evar sigma conclty in
+  let conclty = nf_evar sigma conclty in
   match kind_of_term c with
     | Ind ind ->
         let (_,mip) = Inductive.lookup_mind_specif env ind in