# Module `Rtree`

`type 'a t`

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)

`val mk_rec_calls : int -> 'a t array`

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 : 'a t array -> 'a t array`

`val lift : int -> 'a t -> 'a t`

`lift k t`

increases of`k`

the free parameters of`t`

. Needed to avoid captures when a tree appears under`mk_rec`

`val is_node : 'a t -> bool`

`val dest_node : 'a t -> 'a * 'a t array`

Destructors (recursive calls are expanded)

`val dest_param : 'a t -> int * int`

dest_param is not needed for closed trees (i.e. with no free variable)

`val is_infinite : ('a -> 'a -> bool) -> 'a t -> bool`

Tells if a tree has an infinite branch. The first arg is a comparison used to detect already seen elements, hence loops

`val equiv : ('a -> 'a -> bool) -> ('a -> 'a -> bool) -> 'a t -> 'a t -> bool`

`Rtree.equiv eq eqlab t1 t2`

compares t1 t2 (top-down). If t1 and t2 are both nodes,`eqlab`

is called on their labels, in case of success deeper nodes are examined. In case of loop (detected via structural equality parametrized by`eq`

), then the comparison is successful.

`val equal : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool`

`Rtree.equal eq t1 t2`

compares t1 and t2, first via physical equality, then by structural equality (using`eq`

on elements), then by logical equivalence`Rtree.equiv eq eq`

`val inter : ('a -> 'a -> bool) -> ('a -> 'a -> 'a option) -> 'a -> 'a t -> 'a t -> 'a t`

`val incl : ('a -> 'a -> bool) -> ('a -> 'a -> 'a option) -> 'a -> 'a t -> 'a t -> bool`

`module Smart : sig ... end`