Imported Upstream version 8.3~rc1+dfsgupstream/8.3.rc1.dfsg

1 files changed, 31 insertions, 3 deletions

diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index 492d9a73..afb942fb 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: rawterm.ml 13329 2010-07-26 11:05:39Z herbelin $ *)
 
 (*i*)
 open Util
@@ -34,8 +34,6 @@ type patvar = identifier
 
 type rawsort = RProp of Term.contents | RType of Univ.universe option
 
-type binder_kind = BProd | BLambda | BLetIn
-
 type binding_kind = Lib.binding_kind = Explicit | Implicit
 
 type quantified_hypothesis = AnonHyp of int | NamedHyp of identifier
@@ -185,6 +183,36 @@ let map_rawconstr_with_binders_loc loc g f e = function
   | RDynamic (_,x) -> RDynamic (loc,x)
 *)
 
+let fold_rawconstr f acc =
+  let rec fold acc = function
+  | RVar _ -> acc
+  | RApp (_,c,args) -> List.fold_left fold (fold acc c) args
+  | RLambda (_,_,_,b,c) | RProd (_,_,_,b,c) | RLetIn (_,_,b,c) ->
+      fold (fold acc b) c
+  | RCases (_,_,rtntypopt,tml,pl) ->
+      List.fold_left fold_pattern
+	(List.fold_left fold (Option.fold_left fold acc rtntypopt) (List.map fst tml))
+	pl
+    | RLetTuple (_,_,rtntyp,b,c) ->
+	fold (fold (fold_return_type acc rtntyp) b) c
+    | RIf (_,c,rtntyp,b1,b2) ->
+	fold (fold (fold (fold_return_type acc rtntyp) c) b1) b2
+    | RRec (_,_,_,bl,tyl,bv) ->
+	let acc = Array.fold_left
+	  (List.fold_left (fun acc (na,k,bbd,bty) ->
+	    fold (Option.fold_left fold acc bbd) bty)) acc bl in
+	Array.fold_left fold (Array.fold_left fold acc tyl) bv
+    | RCast (_,c,k) -> fold (match k with CastConv (_, t) -> fold acc t | CastCoerce -> acc) c
+    | (RSort _ | RHole _ | RRef _ | REvar _ | RPatVar _ | RDynamic _) -> acc
+
+  and fold_pattern acc (_,idl,p,c) = fold acc c
+
+  and fold_return_type acc (na,tyopt) = Option.fold_left fold acc tyopt
+
+  in fold acc
+
+let iter_rawconstr f = fold_rawconstr (fun () -> f) ()
+
 let occur_rawconstr id =
   let rec occur = function
     | RVar (loc,id') -> id = id'