diff options
| author | herbelin | 2010-04-19 12:29:42 +0000 |
|---|---|---|
| committer | herbelin | 2010-04-19 12:29:42 +0000 |
| commit | 898886d5627c4f6124f5de52da7dc7b52201a5ea (patch) | |
| tree | d9c664fa588b22348e02eac5eaea2c6234a6d795 /lib | |
| 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')
| -rw-r--r-- | lib/util.ml | 5 | ||||
| -rw-r--r-- | lib/util.mli | 1 |
2 files changed, 6 insertions, 0 deletions
diff --git a/lib/util.ml b/lib/util.ml index ba3d2c6d28..f3b7c99e90 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -1109,6 +1109,11 @@ let array_union_map f a acc = acc a +let array_rev_to_list a = + let rec tolist i res = + if i >= Array.length a then res else tolist (i+1) (a.(i) :: res) in + tolist 0 [] + (* Matrices *) let matrix_transpose mat = diff --git a/lib/util.mli b/lib/util.mli index f900e9bf71..80f2fda380 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 *) |