Correction du problème de complexité de Print Assumptions :

- Suite à une modification faite maladroitement, on ne se contentait pas 
de comparer le nom de la supposition quand on l'insérait dans l'ensemble 
des suppositions utilisées, mais aussi son type, ce qui était 
inutilement long (mais pas le facteur principal)
- L'environnement était parcouru deux fois pour chaque variable de 
section. Ce n'était pas très grave vu qu'en général on a assez peu de 
variables de sections sous la main. Mais ça restait inutile.
- Les noms qui ont déjà étés explorés sont maintenant memoizés, ce qui 
gagne dans le cas les pires (comme les théorèmes sur les réels 
typiquement) une exponentiel dans le temps de recherche (si on visualise 
l'espace de recherche comme un DAG, l'ancienne procédure le parcourais 
comme si il était un arbre, ce qui a une complexité exponentielle en la 
taille du DAG). 



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

4 files changed, 107 insertions, 58 deletions

diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index a2ece57c4..880e978af 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -1190,7 +1190,7 @@ value coq_interprete
       Instruct (DIV21INT31) {
 	print_instr("DIV21INT31");
 	/* spiwack: takes three int31 (the two first ones represent an
-                    int62) and perfoms the euclidian division of the
+                    int62) and performs the euclidian division of the
                     int62 by the int31 */
         uint64 bigint;
         bigint = UI64_of_value(accu);
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 13ef7386f..30cec7ed9 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -554,25 +554,46 @@ fun env field value ->
    axioms and sections variables on which a given term depends
    in a context (expectingly the Global context) *)
 
-type assumption =
-  | Variable of identifier*constr (* A section variable and its type *)
-  | Axiom of constant*constr      (* An axiom and its type*)
+type context_object =
+  | Variable of identifier (* A section variable or a Let definition *)
+  | Axiom of constant      (* An axiom or a constant. *)
 
 
 (* Defines a set of [assumption] *)
-module OrderedAssumption = 
+module OrderedContextObject = 
 struct 
-  type t = assumption
-  let compare = compare
+  type t = context_object
+  let compare x y = 
+      match x , y with
+      | Variable i1 , Variable i2 -> id_ord i1 i2
+      | Axiom k1 , Axiom k2 -> Pervasives.compare k1 k2
+	          (* spiwack: it would probably be cleaner
+		     to provide a [kn_ord] function *)
+      | Variable _ , Axiom _ -> -1
+      | Axiom _ , Variable _ -> 1
 end
 
-module AssumptionSet = Set.Make (OrderedAssumption)
-
-(* infix definition of set-union for redability purposes *)
-let ( ** ) s1 s2  = AssumptionSet.union s1 s2
-
-let rec assumptions t env =   
- (* Goes recursively into the terms to see if it depends on assumptions
+module ContextObjectSet = Set.Make (OrderedContextObject)
+module ContextObjectMap = Map.Make (OrderedContextObject)
+
+
+let assumptions (* t env *) =   
+  (* Infix definition for chaining function that accumulate
+     on a and a ContextObjectSet, ContextObjectMap.  *)
+  let ( ** ) f1 f2 s m = let (s',m') = f1 s m in f2 s' m' in
+  (* This function eases memoization, by checking if an object is already
+     stored before trying and applying a function. 
+     If the object is there, the function is not fired (we are in a 
+     particular case where memoized object don't need a treatment at all).
+     If the object isn't there, it is stored and the function is fired*)
+  let try_and_go o f s m =
+    if ContextObjectSet.mem o s then
+      (s,m)
+    else
+      f (ContextObjectSet.add o s) m
+  in
+  let identity2 s m = (s,m) in
+  (* Goes recursively into the term to see if it depends on assumptions
     the 3 important cases are : - Const _ where we need to first unfold
     the constant and return the needed assumptions of its body in the 
     environment,
@@ -581,44 +602,73 @@ let rec assumptions t env =
                                 - Var _ which means that the term refers
     to a section variable or a "Let" definition, in the former it is
     an assumption of [t], in the latter is must be unfolded like a Const.
-    The other cases are straightforward recursion.*)
-  match kind_of_term t with
-    | Var id -> (* a Var can be either a variable, or a "Let" definition.*)
-                (match named_body id env with
-                | None ->
-                      AssumptionSet.singleton (Variable (id,named_type id env))
-		| Some bdy -> assumptions bdy env)
-    | Meta _ | Evar _ -> Util.anomaly "Environ.assumption: does not expect a meta or an evar"
+    The other cases are straightforward recursion.
+    Calls to the environment are memoized, thus avoiding to explore
+    the DAG of the environment as if it was a tree (can cause
+    exponential behavior and prevent the algorithm from terminating
+    in reasonable time). [s] is a set of [context_object], representing
+    the object already visited.*)
+  let rec aux t env s acc =
+    match kind_of_term t with
+    | Var id -> aux_memoize_id id env s acc
+    | Meta _ | Evar _ -> 
+	Util.anomaly "Environ.assumption: does not expect a meta or an evar"
     | Cast (e1,_,e2) | Prod (_,e1,e2) | Lambda (_,e1,e2) -> 
-                   (assumptions e1 env)**(assumptions e2 env)
-    | LetIn (_,e1,e2,e3) ->(assumptions e1 env)**
-                           (assumptions e2 env)**
-                           (assumptions e3 env)
-    | App (e1, e_array) -> (assumptions e1 env)**
-                   (Array.fold_right (fun e s -> (assumptions e env)**s)
-                                      e_array AssumptionSet.empty)
-    | Case (_,e1,e2,e_array) -> (assumptions e1 env)**
-                                (assumptions e2 env)**
-                   (Array.fold_right (fun e s -> (assumptions e env)**s)
-                                      e_array AssumptionSet.empty)
+                           ((aux e1 env)**(aux e2 env)) s acc
+    | LetIn (_,e1,e2,e3) -> ((aux e1 env)**
+                             (aux e2 env)**
+                             (aux e3 env))
+	                     s acc 
+    | App (e1, e_array) -> ((aux e1 env)**
+			    (Array.fold_right 
+			       (fun e f -> (aux e env)**f)
+                               e_array identity2))
+	                   s acc
+    | Case (_,e1,e2,e_array) -> ((aux e1 env)**
+                                 (aux e2 env)**
+				 (Array.fold_right 
+				    (fun e f -> (aux e env)**f)
+                                    e_array identity2))
+	                        s acc
     | Fix (_,(_, e1_array, e2_array)) | CoFix (_,(_,e1_array, e2_array)) ->
-                   Array.fold_right (fun e s -> (assumptions e env)**s)
-                                      e1_array
-                   (Array.fold_right (fun e s -> (assumptions e env)**s)
-                                      e2_array AssumptionSet.empty)
-    | Const kn -> 
-	let cb = lookup_constant kn env in
-        (match cb.Declarations.const_body with
-        | None -> 
-	    let ctype = 
-	      match cb.Declarations.const_type with
-		| PolymorphicArity (ctx,a) -> mkArity (ctx, Type a.poly_level)
-		| NonPolymorphicType t -> t
-	    in
-	    AssumptionSet.singleton (Axiom (kn,ctype))
-        | Some body -> assumptions (Declarations.force body) env)
-    | _ -> AssumptionSet.empty (* closed atomic types + rel *)
-
+                  ((Array.fold_right 
+		      (fun e f -> (aux e env)**f)
+                      e1_array identity2) **
+                   (Array.fold_right 
+		      (fun e f -> (aux e env)**f)
+                      e2_array identity2))
+		     s acc
+    | Const kn -> aux_memoize_kn kn env s acc
+    | _ -> (s,acc) (* closed atomic types + rel *)
+
+  and add_id id env s acc =
+    (* a Var can be either a variable, or a "Let" definition.*)
+    match lookup_named id env with
+    | (_,None,t) ->
+        (s,ContextObjectMap.add (Variable id) t acc)
+    | (_,Some bdy,_) -> aux bdy env s acc
+
+  and aux_memoize_id id env =
+    try_and_go (Variable id) (add_id id env)
+
+  and add_kn kn env s acc =
+    let cb = lookup_constant kn env in
+    match cb.Declarations.const_body with
+    | None -> 
+	let ctype = 
+	  match cb.Declarations.const_type with
+	  | PolymorphicArity (ctx,a) -> mkArity (ctx, Type a.poly_level)
+	  | NonPolymorphicType t -> t
+	in
+	(s,ContextObjectMap.add (Axiom kn) ctype acc)
+    | Some body -> aux (Declarations.force body) env s acc
+
+  and aux_memoize_kn kn env =
+    try_and_go (Axiom kn) (add_kn kn env)
+ in
+ fun t env ->
+   snd (aux t env (ContextObjectSet.empty) (ContextObjectMap.empty))
+    
 (* /spiwack *)
 
 
diff --git a/kernel/environ.mli b/kernel/environ.mli
index c5b4800d5..ca41c2d7d 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -241,17 +241,16 @@ val register : env -> field -> Retroknowledge.entry -> env
 (******************************************************************)
 (* spiwack: a few declarations for the "Print Assumption" command *)
 
-type assumption =
-  | Variable of identifier*Term.constr (* A section variable and its type *)
-  | Axiom of constant*Term.constr      (* An axiom and its type*)
-
+type context_object =
+  | Variable of identifier (* A section variable or a Let definition *)
+  | Axiom of constant      (* An axiom or a constant. *)
 
 (* AssumptionSet.t is a set of [assumption] *)
-module OrderedAssumption :  Set.OrderedType with type t = assumption
-module AssumptionSet : Set.S with type elt = assumption
+module OrderedContextObject :  Set.OrderedType with type t = context_object
+module ContextObjectMap : Map.S with type key = context_object
 
 (* collects all the assumptions on which a term relies (together with
    their type *)
-val assumptions : constr -> env -> AssumptionSet.t
+val assumptions : constr -> env -> Term.types ContextObjectMap.t
 
 
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 35bb1267a..a3df35ad5 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -110,7 +110,7 @@ let env_of_senv = env_of_safe_env
 (* terms which are closed under the environnement env, i.e
    terms which only depends on constant who are themselves closed *)
 let closed env term = 
-  AssumptionSet.is_empty (assumptions env term)
+  ContextObjectMap.is_empty (assumptions env term)
 
 (* the set of safe terms in an environement any recursive set of
    terms who are known not to prove inconsistent statement. It should