From e7116e5990033c74a81987a236c2221582957da8 Mon Sep 17 00:00:00 2001 From: aspiwack Date: Tue, 27 May 2008 16:56:07 +0000 Subject: 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). MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11001 85f007b7-540e-0410-9357-904b9bb8a0f7 --- kernel/safe_typing.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/safe_typing.ml') 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 -- cgit v1.2.3