summaryrefslogtreecommitdiff
path: root/pretyping/rawterm.ml
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2010-08-06 16:15:08 -0400
committerGravatar Stephane Glondu <steph@glondu.net>2010-08-06 16:17:55 -0400
commitf18e6146f4fd6ed5b8ded10a3e602f5f64f919f4 (patch)
treec413c5bb42d20daf5307634ae6402526bb994fd6 /pretyping/rawterm.ml
parentb9f47391f7f259c24119d1de0a87839e2cc5e80c (diff)
Imported Upstream version 8.3~rc1+dfsgupstream/8.3.rc1.dfsg
Diffstat (limited to 'pretyping/rawterm.ml')
-rw-r--r--pretyping/rawterm.ml34
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'