diff git a/demos/basic/OST.ml b/demos/basic/OST.ml
new file mode 100644
index 0000000000000000000000000000000000000000..e4e0e6ffa0a59ac26fd85b9bafdd9e54e72f82ee
 /dev/null
+++ b/demos/basic/OST.ml
@@ 0,0 +1,108 @@
+(* This is a variant of OCaml's [Set] module, where each node in the binary
+ search tree carries its size (i.e., the number of its elements). The tree
+ is thus an ordered statistics tree, and supports [select] and [rank] in
+ logarithmic time and [cardinal] in constant time. *)
+
+(* This implementation is minimalistic  many set operations are missing. *)
+
+module Make (Ord : Set.OrderedType) = struct
+
+ type elt = Ord.t
+ type t = Empty  Node of t * elt * t * (* height: *) int * (* size: *) int
+
+ let height = function
+ Empty > 0
+  Node(_, _, _, h, _) > h
+
+ let size = function
+ Empty > 0
+  Node(_, _, _, _, s) > s
+
+ let create l v r =
+ let hl = height l in
+ let hr = height r in
+ Node(l, v, r, (if hl >= hr then hl + 1 else hr + 1), size l + 1 + size r)
+
+ let bal l v r =
+ let hl = height l in
+ let hr = height r in
+ if hl > hr + 2 then begin
+ match l with
+ Empty > invalid_arg "Set.bal"
+  Node(ll, lv, lr, _, _) >
+ if height ll >= height lr then
+ create ll lv (create lr v r)
+ else begin
+ match lr with
+ Empty > invalid_arg "Set.bal"
+  Node(lrl, lrv, lrr, _, _)>
+ create (create ll lv lrl) lrv (create lrr v r)
+ end
+ end else if hr > hl + 2 then begin
+ match r with
+ Empty > invalid_arg "Set.bal"
+  Node(rl, rv, rr, _, _) >
+ if height rr >= height rl then
+ create (create l v rl) rv rr
+ else begin
+ match rl with
+ Empty > invalid_arg "Set.bal"
+  Node(rll, rlv, rlr, _, _) >
+ create (create l v rll) rlv (create rlr rv rr)
+ end
+ end else
+ Node(l, v, r, (if hl >= hr then hl + 1 else hr + 1), size l + 1 + size r)
+
+ let rec add x = function
+ Empty > Node(Empty, x, Empty, 1, 1)
+  Node(l, v, r, _, _) as t >
+ let c = Ord.compare x v in
+ if c = 0 then t else
+ if c < 0 then
+ let ll = add x l in
+ if l == ll then t else bal ll v r
+ else
+ let rr = add x r in
+ if r == rr then t else bal l v rr
+
+ let empty = Empty
+
+ let cardinal = size
+
+ let rec select i = function
+  Empty >
+ (* [i] is out of bounds *)
+ assert false
+  Node (l, v, r, _, s) >
+ assert (0 <= i && i < s);
+ let sl = size l in
+ if i < sl then
+ select i l
+ else if i = sl then
+ v
+ else
+ select (i  sl  1) r
+
+ let pick xs =
+ let s = size xs in
+ if s = 0 then
+ raise Not_found
+ else
+ select (Random.int s) xs
+
+ let rec rank accu x = function
+  Empty >
+ raise Not_found
+  Node (l, v, r, _, _) >
+ let c = Ord.compare x v in
+ if c = 0 then
+ accu + size l
+ else if c < 0 then
+ rank accu x l
+ else
+ rank (accu + size l + 1) x r
+
+ let rank =
+ rank 0
+
+end
diff git a/demos/basic/OST.mli b/demos/basic/OST.mli
new file mode 100644
index 0000000000000000000000000000000000000000..c2d367e11a2fc38964b40b1b7ebf09b17b0bf20b
 /dev/null
+++ b/demos/basic/OST.mli
@@ 0,0 +1,48 @@
+(* This is a variant of OCaml's [Set] module, where each node in the binary
+ search tree carries its size (i.e., the number of its elements). The tree
+ is thus an ordered statistics tree, and supports [select] and [rank] in
+ logarithmic time and [cardinal] in constant time. *)
+
+(* This implementation is minimalistic  many set operations are missing. *)
+
+module Make (Ord : Set.OrderedType) : sig
+
+ (* The type of set elements. *)
+
+ type elt = Ord.t
+
+ (* The type of sets. *)
+
+ type t
+
+ (* [empty] is the empty set. *)
+
+ val empty: t
+
+ (* [add x xs] is the union of the singleton set [x] and of the set [xs]. *)
+
+ val add: elt > t > t
+
+ (* [cardinal xs] is the number of elements in the set [xs]. *)
+
+ val cardinal: t > int
+
+ (* [select i xs] returns the [i]th element of the set [xs], viewed as an
+ increasing sequence. The index [i] must lie between 0 (included) and
+ [cardinal xs] (excluded). *)
+
+ val select: int > t > elt
+
+ (* [pick xs] returns a randomlydistributed random element of the set [xs].
+ If [xs] is empty, the exception [Not_found] is raised. *)
+
+ val pick: t > elt
+
+ (* [rank x xs] returns the rank of the element [x] in the set [xs], viewed
+ as an increasing sequence. This rank is comprised between 0 (included) and
+ [cardinal xs] (excluded). If [x] is not a member of [xs], the exception
+ [Not_found] is raised. *)
+
+ val rank: elt > t > int
+
+end
diff git a/demos/basic/TermGenerator.ml b/demos/basic/TermGenerator.ml
index ed9a45d50c6fe8442846086e71696c0231a79f63..9348b2c6c9323c4f660743e307e0db8865144271 100644
 a/demos/basic/TermGenerator.ml
+++ b/demos/basic/TermGenerator.ml
@@ 1,5 +1,10 @@
open Term
+module StringSet =
+ OST.Make(String)
+
+(* Randomly split an integer [n] into [n1 + n2]. *)
+
let split n =
assert (n >= 0);
let n1 = Random.int (n + 1) in
@@ 8,25 +13,18 @@ let split n =
assert (0 <= n2 && n2 <= n);
n1, n2
let random_variable () =
+(* Randomly generate a name between "a" and "z". *)
+
+let random_name () =
let i = Random.int 26 in
let c = Char.chr (Char.code 'a' + i) in
String.make 1 c
module StringSet =
 Set.Make(String)

let random_set_element xs = (* inefficient *)
 let n = StringSet.cardinal xs in
 assert (n > 0);
 let i = Random.int n in
 List.nth (StringSet.elements xs) i

let rec generate env n =
assert (n >= 0);
 assert (not (StringSet.is_empty env));
+ assert (StringSet.cardinal env > 0);
if n = 0 then
 TVar (random_set_element env)
+ TVar (StringSet.pick env)
else
match Random.int 2 with
 0 >
@@ 39,7 +37,7 @@ let rec generate env n =
and generate_lambda env n =
let n = n  1 in
 let x = random_variable () in
+ let x = random_name () in
let env = StringSet.add x env in
TLambda (x, generate env n)