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

1 files changed, 49 insertions, 10 deletions

diff --git a/lib/rtree.mli b/lib/rtree.mli
index 554af8163..db5475b79 100644
--- a/lib/rtree.mli
+++ b/lib/rtree.mli
@@ -9,32 +9,71 @@
 (*i $Id$ i*)
 
 (* Type of regular tree with nodes labelled by values of type 'a *)
-
+(* The implementation uses de Bruijn indices, so binding capture
+   is avoided by the lift operator (see example below) *)
 type 'a t 
 
 (* Building trees *)
-(* build a recursive call *) 
-val mk_param : int -> 'a t
+
 (* build a node given a label and the vector of sons *)
 val mk_node  : 'a -> 'a t array -> 'a t
-(* build mutually dependent trees *)
+
+(* Build mutually recursive trees:
+    X_1 = f_1(X_1,..,X_n) ... X_n = f_n(X_1,..,X_n)
+   is obtained by the following pseudo-code
+   let vx = mk_rec_calls n in
+   let [|x_1;..;x_n|] =
+      mk_rec[|f_1(vx.(0),..,vx.(n-1);..;f_n(vx.(0),..,vx.(n-1))|]
+
+  First example: build  rec X = a(X,Y) and Y = b(X,Y,Y)
+  let [|vx;vy|] = mk_rec_calls 2 in
+  let [|x;y|] = mk_rec [|mk_node a [|vx;vy|]; mk_node b [|vx;vy;vy|]|]
+
+  Another example: nested recursive trees rec Y = b(rec X = a(X,Y),Y,Y)
+  let [|vy|] = mk_rec_calls 1 in
+  let [|vx|] = mk_rec_calls 1 in
+  let [|x|] = mk_rec[|mk_node a [|vx;lift 1 vy|]
+  let [|y|] = mk_rec[|mk_node b [|x;vy;vy|]|]
+  (note the lift to avoid
+ *)
+val mk_rec_calls : int -> 'a t array
 val mk_rec   : 'a t array -> 'a t array
 
 (* [lift k t] increases of [k] the free parameters of [t]. Needed
    to avoid captures when a tree appears under [mk_rec] *) 
 val lift : int -> 'a t -> 'a t
 
-val map : ('a -> 'b) -> 'a t -> 'b t
-
-(* [(smartmap f t) == t] if [(f a) ==a ] for all nodes *)
-val smartmap : ('a -> 'a) -> 'a t -> 'a t
-
+val is_node : 'a t -> bool
 (* Destructors (recursive calls are expanded) *)
-val dest_param : 'a t -> int
 val dest_node  : 'a t -> 'a * 'a t array
+(* dest_param is not needed for closed trees (i.e. with no free variable) *)
+val dest_param : 'a t -> int * int
 
 (* Tells if a tree has an infinite branch *)
 val is_infinite : 'a t -> bool
 
+(* [compare_rtree f t1 t2] compares t1 t2 (top-down).
+   f is called on each node: if the result is negative then the
+   traversal ends on false, it is is positive then deeper nodes are
+   not examined, and the traversal continues on respective siblings,
+   and if it is 0, then the traversal continues on sons, pairwise.
+   In this latter case, if the nodes do not have the same number of
+   sons, then the traversal ends on false.
+   In case of loop, the traversal is successful and it resumes on
+   siblings.
+ *)
+val compare_rtree : ('a t -> 'b t -> int) -> 'a t -> 'b t -> bool
+
+val eq_rtree : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
+
+(* Iterators *)
+
+val map : ('a -> 'b) -> 'a t -> 'b t
+(* [(smartmap f t) == t] if [(f a) ==a ] for all nodes *)
+val smartmap : ('a -> 'a) -> 'a t -> 'a t
+val fold : (bool -> 'a t -> ('a t -> 'b) -> 'b) -> 'a t -> 'b
+val fold2 :
+  (bool -> 'a t -> 'b -> ('a t -> 'b -> 'c) -> 'c) -> 'a t -> 'b -> 'c
+
 (* A rather simple minded pretty-printer *)
 val pp_tree : ('a -> Pp.std_ppcmds) -> 'a t -> Pp.std_ppcmds