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

2 files changed, 50 insertions, 21 deletions

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 3aefeeb07..c5742268b 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -43,6 +43,34 @@ open Inductiveops
 
 (************************************************************************)
 
+(* An auxiliary function for searching for fixpoint guard indexes *)
+
+exception Found of int array
+
+let search_guard loc env possible_indexes fixdefs = 
+  (* Standard situation with only one possibility for each fix. *)
+  (* We treat it separately in order to get proper error msg. *)
+  if List.for_all (fun l->1=List.length l) possible_indexes then 
+    let indexes = Array.of_list (List.map List.hd possible_indexes) in 
+    let fix = ((indexes, 0),fixdefs) in
+    (try check_fix env fix with 
+       | e -> if loc = dummy_loc then raise e else Stdpp.raise_with_loc loc e);
+    indexes
+  else
+    (* we now search recursively amoungst all combinations *)
+    (try     
+       List.iter 
+	 (fun l -> 
+	    let indexes = Array.of_list l in 
+	    let fix = ((indexes, 0),fixdefs) in
+	    try check_fix env fix; raise (Found indexes) 
+	    with TypeError _ -> ())
+	 (list_combinations possible_indexes); 
+       let errmsg = "cannot guess decreasing argument of fix" in 
+       if loc = dummy_loc then error errmsg else 
+	 user_err_loc (loc,"search_guard", Pp.str errmsg)
+     with Found indexes -> indexes)
+
 (* To embed constr in rawconstr *)
 let ((constr_in : constr -> Dyn.t),
      (constr_out : Dyn.t -> constr)) = create "constr"
@@ -266,6 +294,8 @@ module Pretyping_F (Coercion : Coercion.S) = struct
     | RProp c -> judge_of_prop_contents c
     | RType _ -> judge_of_new_Type ()
 
+  exception Found of fixpoint
+
   (* [pretype tycon env isevars lvar lmeta cstr] attempts to type [cstr] *)
   (* in environment [env], with existential variables [(evars_of isevars)] and *)
   (* the type constraint tycon *)
@@ -342,28 +372,22 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	evar_type_fixpoint loc env isevars names ftys vdefj;
 	let fixj = match fixkind with
 	  | RFix (vn,i) ->
-	      let guard_indexes = Array.mapi 
+	      (* First, let's find the guard indexes. *)
+	      (* If recursive argument was not given by user, we try all args.
+	         An earlier approach was to look only for inductive arguments,
+		 but doing it properly involves delta-reduction, and it finally 
+                 doesn't seem to worth the effort (except for huge mutual 
+		 fixpoints ?) *)
+	      let possible_indexes = Array.to_list (Array.mapi 
 		(fun i (n,_) -> match n with 
-		   | Some n -> n 
-		   | None -> 
-		       (* Recursive argument was not given by the user : We
-			  check that there is only one inductive argument *)
-		       let ctx = ctxtv.(i) in 
-		       let isIndApp t = 
-			 isInd (fst (decompose_app (strip_head_cast t))) in
-			 (* This could be more precise (e.g. do some delta) *)
-		       let lb = List.rev_map (fun (_,_,t) -> isIndApp t) ctx in
-		       try (list_unique_index true lb) - 1
-		       with Not_found -> 
-			 Util.user_err_loc
-			   (loc,"pretype",
-			    Pp.str "cannot guess decreasing argument of fix"))
-		vn 
-	      in
-	      let fix = ((guard_indexes, i),(names,ftys,Array.map j_val vdefj)) in
-	      (try check_fix env fix with e -> Stdpp.raise_with_loc loc e);
-	      make_judge (mkFix fix) ftys.(i)
-	  | RCoFix i -> 
+		   | Some n -> [n]
+		   | None -> list_map_i (fun i _ -> i) 0 ctxtv.(i))
+		vn)
+	      in 
+	      let fixdecls = (names,ftys,Array.map j_val vdefj) in 
+	      let indexes = search_guard loc env possible_indexes fixdecls in 
+	      make_judge (mkFix ((indexes,i),fixdecls)) ftys.(i)
+	  | RCoFix i ->
 	      let cofix = (i,(names,ftys,Array.map j_val vdefj)) in
 	      (try check_cofix env cofix with e -> Stdpp.raise_with_loc loc e);
 	      make_judge (mkCoFix cofix) ftys.(i) in
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 0b9b47b7a..64144f9a4 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -18,6 +18,11 @@ open Rawterm
 open Evarutil
 (*i*)
 
+(* An auxiliary function for searching for fixpoint guard indexes *)
+
+val search_guard : 
+    Util.loc -> env -> int list list -> rec_declaration -> int array
+
 type typing_constraint = OfType of types option | IsType
 
 type var_map = (identifier * unsafe_judgment) list