summaryrefslogtreecommitdiff
path: root/lib/rtree.mli
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2012-01-12 16:02:20 +0100
committerGravatar Stephane Glondu <steph@glondu.net>2012-01-12 16:02:20 +0100
commit97fefe1fcca363a1317e066e7f4b99b9c1e9987b (patch)
tree97ec6b7d831cc5fb66328b0c63a11db1cbb2f158 /lib/rtree.mli
parent300293c119981054c95182a90c829058530a6b6f (diff)
Imported Upstream version 8.4~betaupstream/8.4_beta
Diffstat (limited to 'lib/rtree.mli')
-rw-r--r--lib/rtree.mli37
1 files changed, 19 insertions, 18 deletions
diff --git a/lib/rtree.mli b/lib/rtree.mli
index 01fff68a..6695fc82 100644
--- a/lib/rtree.mli
+++ b/lib/rtree.mli
@@ -1,24 +1,22 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: rtree.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
-(* Type of regular tree with nodes labelled by values of type 'a *)
-(* The implementation uses de Bruijn indices, so binding capture
+(** 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 *)
+(** Building trees *)
-(* build a node given a label and the vector of sons *)
+(** build a node given a label and the vector of sons *)
val mk_node : 'a -> 'a t array -> 'a t
-(* Build mutually recursive 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
@@ -32,27 +30,29 @@ val mk_node : 'a -> 'a t array -> 'a t
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|]|]
+ 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
+(** [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 is_node : 'a t -> bool
-(* Destructors (recursive calls are expanded) *)
+
+(** Destructors (recursive calls are expanded) *)
val dest_node : 'a t -> 'a * 'a t array
-(* dest_param is not needed for closed trees (i.e. with no free variable) *)
+
+(** 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 *)
+(** Tells if a tree has an infinite branch *)
val is_infinite : 'a t -> bool
-(* [compare_rtree f t1 t2] compares t1 t2 (top-down).
+(** [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,
@@ -66,14 +66,15 @@ 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 *)
+(** Iterators *)
val map : ('a -> 'b) -> 'a t -> 'b t
-(* [(smartmap f t) == t] if [(f a) ==a ] for all nodes *)
+
+(** [(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 *)
+(** A rather simple minded pretty-printer *)
val pp_tree : ('a -> Pp.std_ppcmds) -> 'a t -> Pp.std_ppcmds