Added {measure x f} as a valid recursion order.

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

11 files changed, 32 insertions, 13 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index e73e88587b..a81ca599c8 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -843,6 +843,7 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
 and extern_recursion_order scopes vars = function
     RStructRec -> CStructRec
   | RWfRec c -> CWfRec (extern true scopes vars c)
+  | RMeasureRec c -> CMeasureRec (extern true scopes vars c)
 
 
 let extern_rawconstr vars c =
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 57b5762d77..deb7abbde6 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -775,17 +775,22 @@ let internalise sigma globalenv env allow_soapp lvar c =
 	in
         let idl = Array.map
           (fun (id,(n,order),bl,ty,bd) ->
-	    let ro, ((ids',_,_),rbl) =
-	      (match order with
-		   CStructRec -> 
-		     RStructRec,
-		     List.fold_left intern_local_binder (env,[]) bl
-		 | CWfRec c -> 
-		     let before, after = list_chop (succ (out_some n)) bl in
-		     let ((ids',_,_),rafter) =
-		       List.fold_left intern_local_binder (env,[]) after in
-		     let ro = RWfRec (intern (ids', tmp_scope, scopes) c) in
-		       ro, List.fold_left intern_local_binder (env,rafter) before)
+	     let intern_ro_arg c f =
+	       let before, after = list_chop (succ (out_some n)) bl in
+	       let ((ids',_,_),rafter) =
+		 List.fold_left intern_local_binder (env,[]) after in
+	       let ro = (intern (ids', tmp_scope, scopes) c) in
+		 f ro, List.fold_left intern_local_binder (env,rafter) before
+	     in
+	     let ro, ((ids',_,_),rbl) =
+	       (match order with
+		    CStructRec -> 
+		      RStructRec,
+		      List.fold_left intern_local_binder (env,[]) bl
+		  | CWfRec c ->
+		      intern_ro_arg c (fun r -> RWfRec r)
+		  | CMeasureRec c ->
+		      intern_ro_arg c (fun r -> RMeasureRec r))
 	    in
 	    let ids'' = List.fold_right Idset.add lf ids' in
 	     ((n, ro), List.rev rbl, 
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 5b9b404425..6e7ea0f9c8 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -544,6 +544,7 @@ and cofixpoint_expr =
 and recursion_order_expr = 
   | CStructRec
   | CWfRec of constr_expr
+  | CMeasureRec of constr_expr
 
 (***********************)
 (* For binders parsing *)
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 9173d3116e..57a2c976cb 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -122,6 +122,7 @@ and cofixpoint_expr =
 and recursion_order_expr = 
   | CStructRec
   | CWfRec of constr_expr
+  | CMeasureRec of constr_expr
 
 and local_binder =
   | LocalRawDef of name located * constr_expr
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 82e1114256..2a975a9648 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -244,6 +244,7 @@ GEXTEND Gram
   fixannot:
     [ [ "{"; IDENT "struct"; id=name; "}" -> (Some id, CStructRec)
       | "{"; IDENT "wf"; id=name; rel=lconstr; "}" -> (Some id, CWfRec rel)
+      | "{"; IDENT "measure"; id=name; rel=lconstr; "}" -> (Some id, CMeasureRec rel)
       | ->  (None, CStructRec)
       ] ]
   ;
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 404e7e0dfe..68ef987498 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -237,6 +237,7 @@ GEXTEND Gram
   rec_annotation:
     [ [ "{"; IDENT "struct"; id=IDENT; "}" -> (Some (id_of_string id), CStructRec)
       | "{"; IDENT "wf"; id=IDENT; rel=lconstr; "}" -> (Some (id_of_string id), CWfRec rel) 
+      | "{"; IDENT "measure"; id=IDENT; rel=lconstr; "}" -> (Some (id_of_string id), CMeasureRec rel) 
       | ->  (None, CStructRec)
       ] ]
   ;
diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4
index bdedaf1764..0bd72db4a9 100644
--- a/parsing/g_xml.ml4
+++ b/parsing/g_xml.ml4
@@ -228,6 +228,10 @@ and interp_xml_recursionOrder x =
 	  (match l with
 	       [c] -> RWfRec (interp_xml_type c)
 	     | _ -> user_err_loc (loc, "", str "wrong number of arguments (expected one)"))
+      | "Measure" -> 
+	  (match l with
+	       [c] -> RMeasureRec (interp_xml_type c)
+	     | _ -> user_err_loc (loc, "", str "wrong number of arguments (expected one)"))
       | _ ->
           user_err_loc (locs,"",str "invalid recursion order")
 
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index e51b1fecba..613fbfe780 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -384,6 +384,8 @@ 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_name (snd (List.nth ids (out_some n))) ++ str"}"
+	| CMeasureRec c ->
+	    spc () ++ str "{measure " ++ pr lsimple c ++ pr_name (snd (List.nth ids (out_some n))) ++ 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 c50b2e52f3..b181247ab4 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -572,6 +572,9 @@ let rec pr_vernac = function
 		      | CWfRec c -> 
 			  spc() ++ str "{wf " ++ pr_name name ++ spc() ++ 
 			    pr_lconstr_expr c ++ str"}"
+		      | CMeasureRec c -> 
+			  spc() ++ str "{measure " ++ pr_name name ++ spc() ++ 
+			    pr_lconstr_expr c ++ str"}"
 	    in
             pr_id id ++ pr_binders_arg bl ++ annot ++ spc()
             ++ pr_type_option (fun c -> spc() ++ pr_lconstr_expr c) type_
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index 9a0e51e108..78e616d98a 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -73,7 +73,7 @@ type rawconstr =
 
 and rawdecl = name * rawconstr option * rawconstr
 
-and fix_recursion_order = RStructRec | RWfRec of rawconstr
+and fix_recursion_order = RStructRec | RWfRec of rawconstr | RMeasureRec of rawconstr
 
 and fix_kind =
   | RFix of ((int option * fix_recursion_order) array * int)
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index f6541ff314..c61c61b0f3 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -70,7 +70,7 @@ type rawconstr =
 
 and rawdecl = name * rawconstr option * rawconstr
 
-and fix_recursion_order = RStructRec | RWfRec of rawconstr
+and fix_recursion_order = RStructRec | RWfRec of rawconstr | RMeasureRec of rawconstr
 
 and fix_kind =
   | RFix of ((int option * fix_recursion_order) array * int)