← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to lib/rtree.mli

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
lib/rtree.mli
 
1
(************************************************************************)
 
2
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
 
4
(*   \VV/  **************************************************************)
 
5
(*    //   *      This file is distributed under the terms of the       *)
 
6
(*         *       GNU Lesser General Public License Version 2.1        *)
 
7
(************************************************************************)
 
8
 
 
9
(*i $Id: rtree.mli 10690 2008-03-18 13:30:04Z barras $ i*)
 
10
 
 
11
(* Type of regular tree with nodes labelled by values of type 'a *)
 
12
(* The implementation uses de Bruijn indices, so binding capture
 
13
   is avoided by the lift operator (see example below) *)
 
14
type 'a t 
 
15
 
 
16
(* Building trees *)
 
17
 
 
18
(* build a node given a label and the vector of sons *)
 
19
val mk_node  : 'a -> 'a t array -> 'a t
 
20
 
 
21
(* Build mutually recursive trees:
 
22
    X_1 = f_1(X_1,..,X_n) ... X_n = f_n(X_1,..,X_n)
 
23
   is obtained by the following pseudo-code
 
24
   let vx = mk_rec_calls n in
 
25
   let [|x_1;..;x_n|] =
 
26
      mk_rec[|f_1(vx.(0),..,vx.(n-1);..;f_n(vx.(0),..,vx.(n-1))|]
 
27
 
 
28
  First example: build  rec X = a(X,Y) and Y = b(X,Y,Y)
 
29
  let [|vx;vy|] = mk_rec_calls 2 in
 
30
  let [|x;y|] = mk_rec [|mk_node a [|vx;vy|]; mk_node b [|vx;vy;vy|]|]
 
31
 
 
32
  Another example: nested recursive trees rec Y = b(rec X = a(X,Y),Y,Y)
 
33
  let [|vy|] = mk_rec_calls 1 in
 
34
  let [|vx|] = mk_rec_calls 1 in
 
35
  let [|x|] = mk_rec[|mk_node a [|vx;lift 1 vy|]
 
36
  let [|y|] = mk_rec[|mk_node b [|x;vy;vy|]|]
 
37
  (note the lift to avoid
 
38
 *)
 
39
val mk_rec_calls : int -> 'a t array
 
40
val mk_rec   : 'a t array -> 'a t array
 
41
 
 
42
(* [lift k t] increases of [k] the free parameters of [t]. Needed
 
43
   to avoid captures when a tree appears under [mk_rec] *) 
 
44
val lift : int -> 'a t -> 'a t
 
45
 
 
46
val is_node : 'a t -> bool
 
47
(* Destructors (recursive calls are expanded) *)
 
48
val dest_node  : 'a t -> 'a * 'a t array
 
49
(* dest_param is not needed for closed trees (i.e. with no free variable) *)
 
50
val dest_param : 'a t -> int * int
 
51
 
 
52
(* Tells if a tree has an infinite branch *)
 
53
val is_infinite : 'a t -> bool
 
54
 
 
55
(* [compare_rtree f t1 t2] compares t1 t2 (top-down).
 
56
   f is called on each node: if the result is negative then the
 
57
   traversal ends on false, it is is positive then deeper nodes are
 
58
   not examined, and the traversal continues on respective siblings,
 
59
   and if it is 0, then the traversal continues on sons, pairwise.
 
60
   In this latter case, if the nodes do not have the same number of
 
61
   sons, then the traversal ends on false.
 
62
   In case of loop, the traversal is successful and it resumes on
 
63
   siblings.
 
64
 *)
 
65
val compare_rtree : ('a t -> 'b t -> int) -> 'a t -> 'b t -> bool
 
66
 
 
67
val eq_rtree : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
 
68
 
 
69
(* Iterators *)
 
70
 
 
71
val map : ('a -> 'b) -> 'a t -> 'b t
 
72
(* [(smartmap f t) == t] if [(f a) ==a ] for all nodes *)
 
73
val smartmap : ('a -> 'a) -> 'a t -> 'a t
 
74
val fold : (bool -> 'a t -> ('a t -> 'b) -> 'b) -> 'a t -> 'b
 
75
val fold2 :
 
76
  (bool -> 'a t -> 'b -> ('a t -> 'b -> 'c) -> 'c) -> 'a t -> 'b -> 'c
 
77
 
 
78
(* A rather simple minded pretty-printer *)
 
79
val pp_tree : ('a -> Pp.std_ppcmds) -> 'a t -> Pp.std_ppcmds