diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-04-19 12:29:42 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-04-19 12:29:42 +0000 |
| commit | 898886d5627c4f6124f5de52da7dc7b52201a5ea (patch) | |
| tree | d9c664fa588b22348e02eac5eaea2c6234a6d795 /lib/util.mli | |
| parent | 7079052932f7443ad3a0bcb6fa0cac048338ba7c (diff) | |
Reduced the complexity of evar instantiations from O(n^3) to less than O(n^2).
Reasoning modulo variable aliases induced an extra lookup in the
environment at each inversion of the components of the evar instances:
precomputing the aliases map allowed to gain a factor n.
Moreover, solve_evar_evar_l2r was recomputing the evar substitution
from the evar instance n more times than needed.
Function solve_evar_evar_l2r is still on O(n^2) but it does not seem
to be used so often actually. The trivial case has been optimized
(linear time) but the general case could probably be also cut down to
O(n*log(n)) if needed.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12954 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib/util.mli')
| -rw-r--r-- | lib/util.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/lib/util.mli b/lib/util.mli index f900e9bf7..80f2fda38 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -253,6 +253,7 @@ val array_fold_map2' : ('a -> 'b -> 'c -> 'd * 'c) -> 'a array -> 'b array -> 'c -> 'd array * 'c val array_distinct : 'a array -> bool val array_union_map : ('a -> 'b -> 'b) -> 'a array -> 'b -> 'b +val array_rev_to_list : 'a array -> 'a list (*s Matrices *) |