From 2ea3dc4db81e6513810da086a65f9c8292d4bebf Mon Sep 17 00:00:00 2001
From: letouzey
Date: Sat, 7 Jul 2007 14:53:20 +0000
Subject: 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
---
 lib/util.ml | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'lib/util.ml')

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 = 
-- 
cgit v1.2.3