diff options
| author | Pierre-Marie Pédrot | 2020-12-11 18:21:49 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-12-11 18:28:05 +0100 |
| commit | cade097ff6e5670b5f4c3ea832b593cf88251fbd (patch) | |
| tree | ee8f0fec90e56a21f6262bcc2b8423b94e1965b6 /clib | |
| parent | 5a77078718c18b05e7ffb1366d6dd9e439ecfc91 (diff) | |
Fast path in tclPROGRESS.
We first check that the list of goals have the same length before trying to
engage into potentially costly equality checks.
Diffstat (limited to 'clib')
| -rw-r--r-- | clib/cList.ml | 6 | ||||
| -rw-r--r-- | clib/cList.mli | 3 |
2 files changed, 9 insertions, 0 deletions
diff --git a/clib/cList.ml b/clib/cList.ml index 6b13fac48c..d5520aa2b7 100644 --- a/clib/cList.ml +++ b/clib/cList.ml @@ -23,6 +23,7 @@ sig val for_all_i : (int -> 'a -> bool) -> int -> 'a list -> bool val for_all2eq : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool val prefix_of : 'a eq -> 'a list -> 'a list -> bool + val same_length : 'a list -> 'b list -> bool val interval : int -> int -> int list val make : int -> 'a -> 'a list val addn : int -> 'a -> 'a list -> 'a list @@ -154,6 +155,11 @@ external cast : 'a cell -> 'a list = "%identity" (** {6 Equality, testing} *) +let rec same_length l1 l2 = match l1, l2 with +| [], [] -> true +| _ :: l1, _ :: l2 -> same_length l1 l2 +| ([], _ :: _) | (_ :: _, []) -> false + let rec compare cmp l1 l2 = if l1 == l2 then 0 else match l1,l2 with diff --git a/clib/cList.mli b/clib/cList.mli index c8e471f989..6c8df88767 100644 --- a/clib/cList.mli +++ b/clib/cList.mli @@ -42,6 +42,9 @@ sig (** [prefix_of eq l1 l2] returns [true] if [l1] is a prefix of [l2], [false] otherwise. It uses [eq] to compare elements *) + val same_length : 'a list -> 'b list -> bool + (** A more efficient variant of [for_all2eq (fun _ _ -> true)] *) + (** {6 Creating lists} *) val interval : int -> int -> int list |