diff options
author | 2008-05-27 16:56:07 +0000 | |
---|---|---|
committer | 2008-05-27 16:56:07 +0000 | |
commit | e7116e5990033c74a81987a236c2221582957da8 (patch) | |
tree | c58b9c45a44230733f81e3fe8b3bfe235bb474a5 /parsing/printer.ml | |
parent | 69553d6a87eab1e1769332a92df26e9a02a0f6c1 (diff) |
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
Diffstat (limited to 'parsing/printer.ml')
-rw-r--r-- | parsing/printer.ml | 67 |
1 files changed, 31 insertions, 36 deletions
diff --git a/parsing/printer.ml b/parsing/printer.ml index 521dad6a0..8ef206649 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -491,44 +491,39 @@ let prterm = pr_lconstr (* spiwack: printer function for sets of Environ.assumption. It is used primarily by the Print Assumption command. *) -exception EmptyAssumptionSet - let pr_assumptionset env s = - if (Environ.AssumptionSet.is_empty s) then + if (Environ.ContextObjectMap.is_empty s) then str "Closed under the global context" else - let (vars, axioms) = Environ.AssumptionSet.partition - (function |Variable _ -> true | _ -> false) - s + let (vars,axioms) = + Environ.ContextObjectMap.fold (fun o typ r -> + let (v,a) = r in + match o with + | Variable id -> ( Some ( + Option.default (fnl ()) v + ++ str (string_of_id id) + ++ str " : " + ++ pr_ltype typ + ++ fnl () + ) + , + a ) + | Axiom kn -> ( v , + Some ( + Option.default (fnl ()) a + ++ (pr_constant env kn) + ++ str " : " + ++ pr_ltype typ + ++ fnl () + ) + ) + ) + s (None,None) in - (if Environ.AssumptionSet.is_empty vars then - mt () - else - str "Section Variables:" ++ - (Environ.AssumptionSet.fold - (function Variable (id,typ ) -> - (fun b -> b++str (string_of_id id) - ++str " : " - ++pr_ltype typ - ++fnl ()) - | _ -> anomaly - "Printer.pr_assumptionset: failure of partition (Variable)") - vars (fnl ())) - ) - ++ fnl () - ++ - if Environ.AssumptionSet.is_empty axioms then - mt () - else - str "Axioms:" ++ - (Environ.AssumptionSet.fold - (function Axiom (cst, typ) -> - (fun b -> b++(pr_constant env cst) - ++str " : " - ++pr_ltype typ - ++fnl ()) - | _ -> anomaly - "Printer.pr_assumptionset: failure of partition (Axiom)") - axioms - (fnl ())) + let (vars,axioms) = + ( Option.map (fun p -> str "Section Variables:" ++ p) vars , + Option.map (fun p -> str "Axioms:" ++ p) axioms + ) + in + (Option.default (mt ()) vars) ++ (Option.default (mt ()) axioms) |