diff options
author | Samuel Mimram <smimram@debian.org> | 2008-07-25 15:12:53 +0200 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2008-07-25 15:12:53 +0200 |
commit | a0cfa4f118023d35b767a999d5a2ac4b082857b4 (patch) | |
tree | dabcac548e299fee1da464c93b3dba98484f45b1 /lib/rtree.mli | |
parent | 2281410e38ef99d025ea77194585a9bc019fdaa9 (diff) |
Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg
Diffstat (limited to 'lib/rtree.mli')
-rw-r--r-- | lib/rtree.mli | 61 |
1 files changed, 50 insertions, 11 deletions
diff --git a/lib/rtree.mli b/lib/rtree.mli index 7be96652..b61e6965 100644 --- a/lib/rtree.mli +++ b/lib/rtree.mli @@ -6,35 +6,74 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: rtree.mli 7493 2005-11-02 22:12:16Z mohring $ i*) +(*i $Id: rtree.mli 10690 2008-03-18 13:30:04Z barras $ 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 |