Module `Rtree`Source

Sourcetype '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)

Building trees

Sourceval mk_node : 'a -> 'a t array -> 'a t

build a node given a label and the vector of sons

Sourceval 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))|

Sourceval mk_rec : 'a t array -> 'a t array

Sourceval 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

Sourceval is_node : 'a t -> bool

Sourceval dest_node : 'a t -> 'a * 'a t array

Destructors (recursive calls are expanded)

Sourceval dest_param : 'a t -> int * int

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

Sourceval 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

Sourceval 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.

Sourceval 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

Source

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

Source

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

Iterators

Sourceval map : ('a -> 'b) -> 'a t -> 'b t

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.lib/Rtree/index.html

Module `Rtree`Source

package coq

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.lib/Rtree/index.html

Module RtreeSource

Module `Rtree`Source