Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}.

May cause make world to fail because of dependency problems, make depend clean
world should fix that (hopefully).


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

5 files changed, 59 insertions, 25 deletions

diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 6208952d32..9c39878c7d 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -57,29 +57,29 @@ let rec mkCLambdaN loc bll c =
   | [] -> c
   | LocalRawAssum ([],_) :: bll -> mkCLambdaN loc bll c
 
-let rec index_of_annot loc bl ann =
+let rec index_and_rec_order_of_annot loc bl ann =
   match names_of_local_assums bl,ann with
-    | [_], None -> 0
-    | lids, Some x ->
+    | [_], (None, r) -> 0, r
+    | lids, (Some x, ro) ->
         let ids = List.map snd lids in
-        (try list_index (snd x) ids - 1
+        (try list_index (snd x) ids - 1, ro
         with Not_found ->
           user_err_loc(fst x,"index_of_annot", Pp.str"no such fix variable"))
     | _ -> user_err_loc(loc,"index_of_annot",
       Pp.str "cannot guess decreasing argument of fix")
 
 let mk_fixb (id,bl,ann,body,(loc,tyc)) =
-  let n = index_of_annot (fst id) bl ann in
+  let n,ro = index_and_rec_order_of_annot (fst id) bl ann in
   let ty = match tyc with
       Some ty -> ty
     | None -> CHole loc in
-  (snd id,n,bl,ty,body)
+  (snd id,(n,ro),bl,ty,body)
 
 let mk_cofixb (id,bl,ann,body,(loc,tyc)) =
   let _ = option_app (fun (aloc,_) ->
     Util.user_err_loc
       (aloc,"Constr:mk_cofixb",
-       Pp.str"Annotation forbidden in cofix expression")) ann in
+       Pp.str"Annotation forbidden in cofix expression")) (fst ann) in
   let ty = match tyc with
       Some ty -> ty
     | None -> CHole loc in
@@ -243,8 +243,10 @@ GEXTEND Gram
         c=operconstr LEVEL "200" -> (id,bl,ann,c,ty) ] ]
   ;
   fixannot:
-    [ [ "{"; IDENT "struct"; id=name; "}" -> Some id
-      | -> None ] ]
+    [ [ "{"; IDENT "struct"; id=name; "}" -> (Some id, CStructRec)
+      | "{"; IDENT "wf"; id=name; rel=lconstr; "}" -> (Some id, CWfRec rel)
+      | ->  (None, CStructRec)
+      ] ]
   ;
   match_constr:
     [ [ "match"; ci=LIST1 case_item SEP ","; ty=OPT case_type; "with";
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index ad3cc5b363..87f388a748 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 (* $Id$ *)
+(*i camlp4deps: "parsing/grammar.cma" i*)
 
 open Pp
 open Util
@@ -211,11 +212,11 @@ GEXTEND Gram
   (* (co)-fixpoints *)
   rec_definition:
     [ [ id = ident; bl = LIST1 binder_let;
-        annot = OPT rec_annotation; type_ = type_cstr; 
+        annot = rec_annotation; type_ = type_cstr; 
 	":="; def = lconstr; ntn = decl_notation ->
           let names = List.map snd (names_of_local_assums bl) in
           let ni =
-            match annot with
+            match fst annot with
                 Some id ->
                   (try list_index (Name id) names - 1
                   with Not_found ->  Util.user_err_loc
@@ -227,7 +228,7 @@ GEXTEND Gram
                       (loc,"Fixpoint",
                        Pp.str "the recursive argument needs to be specified");
                   0 in
-	  ((id, ni, bl, type_, def),ntn) ] ]
+	  ((id, (ni, snd annot), bl, type_, def),ntn) ] ]
   ;
   corec_definition:
     [ [ id = ident; bl = LIST0 binder_let; c = type_cstr; ":=";
@@ -235,7 +236,10 @@ GEXTEND Gram
           (id,bl,c ,def) ] ]
   ;
   rec_annotation:
-    [ [ "{"; IDENT "struct"; id=IDENT; "}" -> id_of_string id ] ]
+    [ [ "{"; IDENT "struct"; id=IDENT; "}" -> (Some (id_of_string id), CStructRec)
+      | "{"; IDENT "wf"; id=IDENT; rel=lconstr; "}" -> (Some (id_of_string id), CWfRec rel) 
+      | ->  (None, CStructRec)
+      ] ]
   ;
   type_cstr:
     [ [ ":"; c=lconstr -> c 
diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4
index 7b7e471c64..1df3d1f256 100644
--- a/parsing/g_xml.ml4
+++ b/parsing/g_xml.ml4
@@ -187,12 +187,31 @@ and interp_xml_decl_alias s x =
 and interp_xml_def x = interp_xml_decl_alias "def" x
 and interp_xml_decl x = interp_xml_decl_alias "decl" x
 
+and interp_xml_recursionOrder x =
+  let (loc, al, l) = interp_xml_tag "RecursionOrder" x in
+  let (locs, s) = get_xml_attr "type" al in
+    match s with
+	"Structural" -> 
+	  (match l with [] -> RStructRec
+	     | _ -> user_err_loc (loc, "", str "wrong number of arguments (expected none)"))
+      | "WellFounded" -> 
+	  (match l with
+	       [c] -> RWfRec (interp_xml_type c)
+	     | _ -> user_err_loc (loc, "", str "wrong number of arguments (expected one)"))
+      | _ ->
+          user_err_loc (locs,"",str "invalid recursion order")
+
+
 and interp_xml_FixFunction x =
   match interp_xml_tag "FixFunction" x with
-  | (loc,al,[x1;x2]) ->
-      (nmtoken (get_xml_attr "recIndex" al),
+  | (loc,al,[x1;x2;x3]) ->
+      ((nmtoken (get_xml_attr "recIndex" al),
+	interp_xml_recursionOrder x1),
+       (get_xml_ident al, interp_xml_type x2, interp_xml_body x3))
+  | (loc,al,[x1;x2]) -> (* For backwards compatibility *)
+      ((nmtoken (get_xml_attr "recIndex" al), RStructRec),
        (get_xml_ident al, interp_xml_type x1, interp_xml_body x2))
-    | (loc,_,_) -> 
+  | (loc,_,_) -> 
         user_err_loc (loc,"",str "wrong number of arguments (expect one)")
 
 and interp_xml_CoFixFunction x =
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 8bf2f42075..a95fa4bad8 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -374,13 +374,18 @@ let pr_recursive_decl pr pr_dangling dangling_with_for id bl annot t c =
   pr_opt_type_spc pr t ++ str " :=" ++
   pr_sep_com (fun () -> brk(1,2)) (pr_body ltop) c
 
-let pr_fixdecl pr prd dangling_with_for (id,n,bl,t,c) =
+let pr_fixdecl pr prd dangling_with_for (id,(n,ro),bl,t,c) =
   let annot =
     let ids = names_of_local_assums bl in
-    if List.length ids > 1 then 
-      spc() ++ str "{struct " ++ pr_name (snd (List.nth ids n)) ++ str"}"
-    else mt() in
-  pr_recursive_decl pr prd dangling_with_for id bl annot t c
+      match ro with
+	  CStructRec ->
+	    if List.length ids > 1 then 
+	      spc() ++ str "{struct " ++ pr_name (snd (List.nth ids n)) ++ str"}"
+	    else mt() 
+	| CWfRec c ->
+	    spc () ++ str "{wf " ++ pr lsimple c ++ pr_name (snd (List.nth ids n)) ++ str"}"
+  in
+    pr_recursive_decl pr prd dangling_with_for id bl annot t c
 
 let pr_cofixdecl pr prd dangling_with_for (id,bl,t,c) =
   pr_recursive_decl pr prd dangling_with_for id bl (mt()) t c
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index e7fc0e01ff..c08b076173 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -549,7 +549,7 @@ let rec pr_vernac = function
         | LocalRawAssum (nal,_) -> nal
         | LocalRawDef (_,_) -> [] in
       let pr_onerec = function
-        | (id,n,bl,type_,def),ntn ->
+        | (id,(n,ro),bl,type_,def),ntn ->
             let (bl',def,type_) =
               if Options.do_translate() then extract_def_binders def type_
               else ([],def,type_) in
@@ -561,9 +561,13 @@ let rec pr_vernac = function
                 warn (str "non-printable fixpoint \""++pr_id id++str"\"");
                 Anonymous in
             let annot =
-              if List.length ids > 1 then 
-                spc() ++ str "{struct " ++ pr_name name ++ str"}"
-              else mt() in
+	      match (ro : Topconstr.recursion_order_expr) with
+		  CStructRec -> 
+		    if List.length ids > 1 then 
+                      spc() ++ str "{struct " ++ pr_name name ++ str"}"
+		    else mt()
+		| CWfRec c -> spc() ++ str "{wf " ++ 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_
             ++ str" :=" ++ brk(1,1) ++ pr_lconstr def ++