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

4 files changed, 43 insertions, 11 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index ff494c7825..0fe01799e1 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -719,7 +719,8 @@ let rec extern inctx scopes vars r =
                  let (ids,bl) = extern_local_binder scopes vars bl in
                  let vars0 = List.fold_right (name_fold Idset.add) ids vars in
                  let vars1 = List.fold_right (name_fold Idset.add) ids vars' in
-		 (fi,nv.(i), bl, extern_typ scopes vars0 ty,
+		 let n, ro = fst nv.(i), extern_recursion_order scopes vars (snd nv.(i)) in
+		 (fi, (n, ro), bl, extern_typ scopes vars0 ty,
                   extern false scopes vars1 def)) idv
 	     in 
 	     CFix (loc,(loc,idv.(n)),Array.to_list listdecl)
@@ -834,6 +835,11 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
       with
 	  No_match -> extern_symbol allscopes vars t rules
 
+and extern_recursion_order scopes vars = function
+    RStructRec -> CStructRec
+  | RWfRec c -> CWfRec (extern true scopes vars c)
+
+
 let extern_rawconstr vars c =
   extern false (None,Notation.current_scopes()) vars c
 
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 608e1bc900..bda43f8121 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -785,18 +785,29 @@ let internalise sigma globalenv env allow_soapp lvar c =
 	    raise (InternalisationError (locid,UnboundFixName (false,iddef)))
 	in
         let idl = Array.map
-          (fun (id,n,bl,ty,bd) ->
-            let ((ids',_,_),rbl) =
-              List.fold_left intern_local_binder (env,[]) bl in
+          (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 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)
+	    in
 	    let ids'' = List.fold_right Idset.add lf ids' in
-            (List.rev rbl,
+	     ((n, ro), List.rev rbl, 
              intern_type (ids',tmp_scope,scopes) ty,
              intern (ids'',None,scopes) bd)) dl in
-	RRec (loc,RFix (Array.map (fun (_,n,_,_,_) -> n) dl,n),
+	RRec (loc,RFix 
+	      (Array.map (fun (ro,_,_,_) -> ro) idl,n),
               Array.of_list lf,
-              Array.map (fun (bl,_,_) -> bl) idl,
-              Array.map (fun (_,ty,_) -> ty) idl,
-              Array.map (fun (_,_,bd) -> bd) idl)
+              Array.map (fun (_,bl,_,_) -> bl) idl,
+              Array.map (fun (_,_,ty,_) -> ty) idl,
+              Array.map (fun (_,_,_,bd) -> bd) idl)
     | CCoFix (loc, (locid,iddef), dl) ->
         let lf = List.map (fun (id,_,_,_) -> id) dl in
         let dl = Array.of_list dl in
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 6a4ad1f59b..4d4e3f88a0 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -530,8 +530,9 @@ type constr_expr =
   | CDelimiters of loc * string * constr_expr
   | CDynamic of loc * Dyn.t
 
+
 and fixpoint_expr =
-    identifier * int * local_binder list * constr_expr * constr_expr
+    identifier * (int * recursion_order_expr) * local_binder list * constr_expr * constr_expr
 
 and local_binder =
   | LocalRawDef of name located * constr_expr
@@ -540,6 +541,10 @@ and local_binder =
 and cofixpoint_expr =
     identifier * local_binder list * constr_expr * constr_expr
 
+and recursion_order_expr = 
+  | CStructRec
+  | CWfRec of constr_expr
+
 (***********************)
 (* For binders parsing *)
 
@@ -551,6 +556,9 @@ let rec local_binders_length = function
 let names_of_local_assums bl =
   List.flatten (List.map (function LocalRawAssum(l,_)->l|_->[]) bl)
 
+let names_of_local_binders bl =
+  List.flatten (List.map (function LocalRawAssum(l,_)->l|LocalRawDef(l,_)->[l]) bl)
+
 (**********************************************************************)
 (* Functions on constr_expr *)
 
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 11475cdaa2..073f9ba0b3 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -114,11 +114,15 @@ type constr_expr =
   | CDynamic of loc * Dyn.t
 
 and fixpoint_expr =
-    identifier * int * local_binder list * constr_expr * constr_expr
+    identifier * (int * recursion_order_expr) * local_binder list * constr_expr * constr_expr
 
 and cofixpoint_expr =
     identifier * local_binder list * constr_expr * constr_expr
 
+and recursion_order_expr = 
+  | CStructRec
+  | CWfRec of constr_expr
+
 and local_binder =
   | LocalRawDef of name located * constr_expr
   | LocalRawAssum of name located list * constr_expr
@@ -157,6 +161,9 @@ val local_binders_length : local_binder list -> int
 (* Does not take let binders into account *)
 val names_of_local_assums : local_binder list -> name located list
 
+(* With let binders *)
+val names_of_local_binders : local_binder list -> name located list
+
 (* Used in correctness and interface; absence of var capture not guaranteed *)
 (* in pattern-matching clauses and in binders of the form [x,y:T(x)] *)