Rewrite of Program Fixpoint to overcome the previous limitations:

- The measure can now refer to all the formal arguments
- The recursive calls can make all the arguments vary as well
- Generalized to any relation and measure (new syntax {measure m on R})
This relies on an automatic curryfication transformation, the real
fixpoint combinator is working on a sigma type of the arguments. 
Reduces to the previous impl in case only one argument is involved.
The patch also introduces a new flag on implicit arguments that says if
the argument has to be infered (default) or can be turned into a
subgoal/obligation. Comes with a test-suite file.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12030 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 14 insertions, 8 deletions

diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 37c09704e6..9152083bf3 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -397,7 +397,8 @@ GEXTEND Gram
   fixannot:
     [ [ "{"; IDENT "struct"; id=identref; "}" -> (Some id, CStructRec)
     | "{"; IDENT "wf"; rel=constr; id=OPT identref; "}" -> (id, CWfRec rel)
-    | "{"; IDENT "measure"; rel=constr; id=OPT identref; "}" -> (id, CMeasureRec rel)
+    | "{"; IDENT "measure"; m=constr; id=OPT identref; 
+	rel = OPT [ "on"; r=constr -> r ]; "}" -> (id, CMeasureRec (m,rel))
     ] ]
   ;
   binders_let_fixannot:
diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4
index e1e334be6f..3a57fd545d 100644
--- a/parsing/g_xml.ml4
+++ b/parsing/g_xml.ml4
@@ -57,6 +57,9 @@ END
 
 (* Errors *)
 
+let error_expect_two_arguments loc =
+  user_err_loc (loc,"",str "wrong number of arguments (expect two).")
+
 let error_expect_one_argument loc =
   user_err_loc (loc,"",str "wrong number of arguments (expect one).")
 
@@ -241,8 +244,8 @@ and interp_xml_recursionOrder x =
 	     | _ -> error_expect_one_argument loc)
       | "Measure" -> 
 	  (match l with
-	       [c] -> RMeasureRec (interp_xml_type c)
-	     | _ -> error_expect_one_argument loc)
+	       [m;r] -> RMeasureRec (interp_xml_type m, Some (interp_xml_type r))
+	     | _ -> error_expect_two_arguments loc)
       | _ ->
           user_err_loc (locs,"",str "Invalid recursion order.")
 
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index e16641a834..8282895855 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -406,8 +406,9 @@ let pr_fixdecl pr prd dangling_with_for ((_,id),(n,ro),bl,t,c) =
 	  else mt() 
       | CWfRec c ->
 	  spc () ++ str "{wf " ++ pr lsimple c ++ pr_id (snd (Option.get n)) ++ str"}"
-      | CMeasureRec c ->
-	  spc () ++ str "{measure " ++ pr lsimple c ++ pr_id (snd (Option.get n)) ++ str"}"
+      | CMeasureRec (m,r) ->
+	  spc () ++ str "{measure " ++ pr lsimple m ++ pr_id (snd (Option.get n)) ++ 
+	    (match r with None -> mt() | Some r -> str" on " ++ pr lsimple r) ++ str"}"
   in
     pr_recursive_decl pr prd dangling_with_for id bl annot t c
 
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 4eb8ae9386..0054326e40 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -636,9 +636,10 @@ let rec pr_vernac = function
 		      | CWfRec c -> 
 			  spc() ++ str "{wf " ++ pr_lconstr_expr c ++ spc() ++ 
 			    pr_id id ++ str"}"
-		      | CMeasureRec c -> 
-			  spc() ++ str "{measure " ++ pr_lconstr_expr c ++ spc() ++ 
-			    pr_id id ++ str"}"
+		      | CMeasureRec (m,r) -> 
+			  spc() ++ str "{measure " ++ pr_lconstr_expr m ++ spc() ++ 
+			    pr_id id ++ (match r with None -> mt() | Some r -> str" on " ++ 
+			    pr_lconstr_expr r) ++ str"}"
 	    in
             pr_id id ++ pr_binders_arg bl ++ annot ++ spc()
             ++ pr_type_option (fun c -> spc() ++ pr_lconstr_expr c) type_