diff options
| author | letouzey | 2007-07-07 14:53:20 +0000 |
|---|---|---|
| committer | letouzey | 2007-07-07 14:53:20 +0000 |
| commit | 2ea3dc4db81e6513810da086a65f9c8292d4bebf (patch) | |
| tree | 99dbbb64a79f44d9258e702421550f575eef0ad7 /lib | |
| parent | f565fd1643b4df66bf22cc95ed86b549b8a46505 (diff) | |
If a fixpoint is not written with an explicit { struct ... }, then
all arguments are tried successively (from left to right) until one is
found that satisfies the structural decreasing condition.
When the system accepts a fixpoint, it now prints which decreasing argument
was used, e.g:
plus is recursively defined (decreasing on 1st argument)
The search is quite brute-force, and may need to be optimized for huge mutual
fixpoints (?). Anyway, writing explicit {struct} is always a possible fallback.
N.B. in the standard library, only 4 functions have an decreasing argument
different from the one that would be automatically infered:
List.nth, List.nth_ok, List.nth_error, FMapPositive.xfind
And compiling with as few explicit struct as possible would add about 15s
in compilation time for the whole standard library.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9961 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/util.ml | 8 | ||||
| -rw-r--r-- | lib/util.mli | 3 |
2 files changed, 11 insertions, 0 deletions
diff --git a/lib/util.ml b/lib/util.ml index a1c011ce1b..590d649931 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -445,6 +445,14 @@ let list_fold_map' f l e = let list_map_assoc f = List.map (fun (x,a) -> (x,f a)) +(* list_combinations [[a;b];[c;d]] gives [[a;c];[a;d];[b;c];[b;d]] *) + +let rec list_combinations = function + | [] -> [[]] + | l::ll -> + let res = list_combinations ll in + list_map_append (fun x -> List.map (fun l -> x::l) res) l + (* Arrays *) let array_exists f v = diff --git a/lib/util.mli b/lib/util.mli index 5c59708211..c315ecd0ac 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -138,6 +138,9 @@ val list_join_map : ('a -> 'b list) -> 'a list -> 'b list val list_fold_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b list -> 'a * 'c list val list_fold_map' : ('b -> 'a -> 'c * 'a) -> 'b list -> 'a -> 'c list * 'a val list_map_assoc : ('a -> 'b) -> ('c * 'a) list -> ('c * 'b) list +(* list_combinations [[a;b];[c;d]] gives [[a;c];[a;d];[b;c];[b;d]] *) +val list_combinations : 'a list list -> 'a list list + (*s Arrays. *) |