1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(*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 node given a label and the vector of sons *)
val mk_node : 'a -> 'a t array -> 'a t
(* 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 is_node : 'a t -> bool
(* 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) *)
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
|
