* [Caml-list] Recursive types and functors.
@ 2003-03-26 6:28 David Brown
2003-03-26 8:25 ` Jean-Christophe Filliatre
0 siblings, 1 reply; 5+ messages in thread
From: David Brown @ 2003-03-26 6:28 UTC (permalink / raw)
To: Caml List
I have a recursive type where I'd like one of the constructors of the
type to contain a set of the type (or something like set). However, I
can't figure out how to represent this.
For example:
type foo =
| Integer of int
| String of string
| Set of FooSet
module FooSet = Set.Make (struct type t = foo let compare = compare end)
but this obviously doesn't work.
I suspect putting type foo in a functor can somehow make it work, but I
haven't quite figure out how to do it.
Thanks,
Dave Brown
-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
^ permalink raw reply [flat|nested] 5+ messages in thread
* Re: [Caml-list] Recursive types and functors.
2003-03-26 6:28 [Caml-list] Recursive types and functors David Brown
@ 2003-03-26 8:25 ` Jean-Christophe Filliatre
2003-03-26 8:57 ` David Brown
2003-03-26 9:13 ` Claude Marche
0 siblings, 2 replies; 5+ messages in thread
From: Jean-Christophe Filliatre @ 2003-03-26 8:25 UTC (permalink / raw)
To: David Brown; +Cc: Caml List
[-- Attachment #1: message body and .signature --]
[-- Type: text/plain, Size: 3096 bytes --]
David Brown writes:
> I have a recursive type where I'd like one of the constructors of the
> type to contain a set of the type (or something like set). However, I
> can't figure out how to represent this.
>
> For example:
>
> type foo =
> | Integer of int
> | String of string
> | Set of FooSet
>
> module FooSet = Set.Make (struct type t = foo let compare = compare end)
>
> but this obviously doesn't work.
I'm pretty sure this has already been discussed on this list, but I
couldn't find the related thread in the archives...
A (too) naive solution could be to make a polymorphic instance of the
Set module (either by adding an argument 'a everywhere in signatures
OrderedType and S, or by copying the functor body and replacing
Ord.compare by compare); then you have polymorphic sets, say 'a Set.t,
balanced using compare, and you can define
type foo = Integer of int | ... | Set of foo Set.t
Unfortunately this doesn't work because sets themselves shouldn't be
compared with compare, but with Set.compare (see set.mli). And then
you point out the main difficulty: comparing values in type foo
requires to be able to compare sets of foo, and comparing sets
requires to *implement* sets and thus to compare values in foo.
Fortunately, there is another solution (though a bit more complex).
First we define a more generic type 'a foo where 'a will be
substituted later by sets of foo:
type 'a foo = Integer of int | ... | Set of 'a
Then we implement a variant of module Set which implements sets given
the following signature:
module type OrderedType =
sig
type 'a t
val compare: ('a -> 'a -> int) -> 'a t -> 'a t -> int
end
that is where elements are in the polymorphic type 'a t and where the
comparison function depends on a comparison function for arguments in
'a (which will represent the sets, in fine). The functor implements a
type t for sets using balanced trees, as usual, and defines the type
of elements elt to be t Ord.t:
module Make(Ord: OrderedType) =
struct
type elt = t Ord.t
and t = Empty | Node of t * elt * t * int
Right after, it implements comparison over elements and sets in a
mutually recursive way:
let rec compare_elt x y =
Ord.compare compare x y
and compare = ... (usual comparison of sets, using compare_elt)
The remaining of the functor is exactly the same as for Set, with
compare_elt used instead of Ord.compare. I attach the implementation
of this module.
There is (at least) another solution: to use a set implementation
where comparison does not require a comparison of elements. This is
possible if, for instance, you are performing hash-consing on type foo
(which result in tagging foo values with integers, then used in the
comparison). This solution is used in Claude Marché's regexp library
(http://www.lri.fr/~marche/regexp/) and uses a hash-consing technique
available here: http://www.lri.fr/~filliatr/software.en.html
Hope this helps,
--
Jean-Christophe Filliâtre (http://www.lri.fr/~filliatr)
[-- Attachment #2: mset.mli --]
[-- Type: application/octet-stream, Size: 5082 bytes --]
(***********************************************************************)
(* *)
(* Objective Caml *)
(* *)
(* Xavier Leroy, projet Cristal, INRIA Rocquencourt *)
(* *)
(* Copyright 1996 Institut National de Recherche en Informatique et *)
(* en Automatique. All rights reserved. This file is distributed *)
(* under the terms of the GNU Library General Public License. *)
(* *)
(***********************************************************************)
(* $Id: pset.mli,v 1.2 2002/02/22 15:54:43 filliatr Exp $ *)
(* Module [Mset]: variant of module [Set] to build a type and sets of
elements in this type in a mutually recursive way. *)
module type OrderedType =
sig
type 'a t
val compare: ('a -> 'a -> int) -> 'a t -> 'a t -> int
end
(* The input signature of the functor [Mset.Make].
['a t] is the type of the set elements where ['a] will be
substituted by the type for sets of such elements.
[compare] is a total ordering function over the set elements,
given a total ordering function over sets. *)
module Make(Ord: OrderedType):
(* Functor building an implementation of the set structure *)
sig
type t
(* The type of sets. *)
type elt = t Ord.t
(* The type of the set elements. *)
val empty: t
(* The empty set. *)
val is_empty: t -> bool
(* Test whether a set is empty or not. *)
val mem: elt -> t -> bool
(* [mem x s] tests whether [x] belongs to the set [s]. *)
val add: elt -> t -> t
(* [add x s] returns a set containing all elements of [s],
plus [x]. If [x] was already in [s], [s] is returned unchanged. *)
val singleton: elt -> t
(* [singleton x] returns the one-element set containing only [x]. *)
val remove: elt -> t -> t
(* [remove x s] returns a set containing all elements of [s],
except [x]. If [x] was not in [s], [s] is returned unchanged. *)
val union: t -> t -> t
val inter: t -> t -> t
val diff: t -> t -> t
(* Union, intersection and set difference. *)
val compare_elt: elt -> elt -> int
(* Total ordering between elements. *)
val compare: t -> t -> int
(* Total ordering between sets. Can be used as the ordering function
for doing sets of sets. *)
val equal: t -> t -> bool
(* [equal s1 s2] tests whether the sets [s1] and [s2] are
equal, that is, contain equal elements. *)
val subset: t -> t -> bool
(* [subset s1 s2] tests whether the set [s1] is a subset of
the set [s2]. *)
val iter: (elt -> unit) -> t -> unit
(* [iter f s] applies [f] in turn to all elements of [s].
The order in which the elements of [s] are presented to [f]
is unspecified. *)
val fold: (elt -> 'b -> 'b) -> t -> 'b -> 'b
(* [fold f s a] computes [(f xN ... (f x2 (f x1 a))...)],
where [x1 ... xN] are the elements of [s].
The order in which elements of [s] are presented to [f] is
unspecified. *)
val for_all: (elt -> bool) -> t -> bool
(* [for_all p s] checks if all elements of the set
satisfy the predicate [p]. *)
val exists: (elt -> bool) -> t -> bool
(* [exists p s] checks if at least one element of
the set satisfies the predicate [p]. *)
val filter: (elt -> bool) -> t -> t
(* [filter p s] returns the set of all elements in [s]
that satisfy predicate [p]. *)
val partition: (elt -> bool) -> t -> t * t
(* [partition p s] returns a pair of sets [(s1, s2)], where
[s1] is the set of all the elements of [s] that satisfy the
predicate [p], and [s2] is the set of all the elements of
[s] that do not satisfy [p]. *)
val cardinal: t -> int
(* Return the number of elements of a set. *)
val elements: t -> elt list
(* Return the list of all elements of the given set.
The returned list is sorted in increasing order with respect
to the ordering [Ord.compare], where [Ord] is the argument
given to [Set.Make]. *)
val min_elt: t -> elt
(* Return the smallest element of the given set
(with respect to the [Ord.compare] ordering), or raise
[Not_found] if the set is empty. *)
val max_elt: t -> elt
(* Same as [min_elt], but returns the largest element of the
given set. *)
val choose: t -> elt
(* Return one element of the given set, or raise [Not_found] if
the set is empty. Which element is chosen is unspecified,
but equal elements will be chosen for equal sets. *)
end
[-- Attachment #3: mset.ml --]
[-- Type: application/octet-stream, Size: 9891 bytes --]
(***********************************************************************)
(* *)
(* Objective Caml *)
(* *)
(* Xavier Leroy, projet Cristal, INRIA Rocquencourt *)
(* *)
(* Copyright 1996 Institut National de Recherche en Informatique et *)
(* en Automatique. All rights reserved. This file is distributed *)
(* under the terms of the GNU Library General Public License. *)
(* *)
(***********************************************************************)
(* $Id: pset.ml,v 1.1 2000/07/07 16:13:17 filliatr Exp $ *)
(* Sets over ordered types *)
module type OrderedType =
sig
type 'a t
val compare: ('a -> 'a -> int) -> 'a t -> 'a t -> int
end
module type S =
sig
type elt
type t
val empty: t
val is_empty: t -> bool
val mem: elt -> t -> bool
val add: elt -> t -> t
val singleton: elt -> t
val remove: elt -> t -> t
val union: t -> t -> t
val inter: t -> t -> t
val diff: t -> t -> t
val compare_elt : elt -> elt -> int
val compare: t -> t -> int
val equal: t -> t -> bool
val subset: t -> t -> bool
val iter: (elt -> unit) -> t -> unit
val fold: (elt -> 'b -> 'b) -> t -> 'b -> 'b
val for_all: (elt -> bool) -> t -> bool
val exists: (elt -> bool) -> t -> bool
val filter: (elt -> bool) -> t -> t
val partition: (elt -> bool) -> t -> t * t
val cardinal: t -> int
val elements: t -> elt list
val min_elt: t -> elt
val max_elt: t -> elt
val choose: t -> elt
end
module Make(Ord: OrderedType) =
struct
type elt = t Ord.t
and t = Empty | Node of t * elt * t * int
let rec compare_elt x y =
Ord.compare compare x y
and compare_aux l1 l2 =
match (l1, l2) with
([], []) -> 0
| ([], _) -> -1
| (_, []) -> 1
| (Empty :: t1, Empty :: t2) ->
compare_aux t1 t2
| (Node(Empty, v1, r1, _) :: t1, Node(Empty, v2, r2, _) :: t2) ->
let c = compare_elt v1 v2 in
if c <> 0 then c else compare_aux (r1::t1) (r2::t2)
| (Node(l1, v1, r1, _) :: t1, t2) ->
compare_aux (l1 :: Node(Empty, v1, r1, 0) :: t1) t2
| (t1, Node(l2, v2, r2, _) :: t2) ->
compare_aux t1 (l2 :: Node(Empty, v2, r2, 0) :: t2)
and compare s1 s2 =
compare_aux [s1] [s2]
(* Sets are represented by balanced binary trees (the heights of the
children differ by at most 2 *)
let height = function
Empty -> 0
| Node(_, _, _, h) -> h
(* Creates a new node with left son l, value x and right son r.
l and r must be balanced and | height l - height r | <= 2.
Inline expansion of height for better speed. *)
let create l x r =
let hl = match l with Empty -> 0 | Node(_,_,_,h) -> h in
let hr = match r with Empty -> 0 | Node(_,_,_,h) -> h in
Node(l, x, r, (if hl >= hr then hl + 1 else hr + 1))
(* Same as create, but performs one step of rebalancing if necessary.
Assumes l and r balanced.
Inline expansion of create for better speed in the most frequent case
where no rebalancing is required. *)
let bal l x r =
let hl = match l with Empty -> 0 | Node(_,_,_,h) -> h in
let hr = match r with Empty -> 0 | Node(_,_,_,h) -> h 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 x r)
else begin
match lr with
Empty -> invalid_arg "Set.bal"
| Node(lrl, lrv, lrr, _)->
create (create ll lv lrl) lrv (create lrr x 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 x rl) rv rr
else begin
match rl with
Empty -> invalid_arg "Set.bal"
| Node(rll, rlv, rlr, _) ->
create (create l x rll) rlv (create rlr rv rr)
end
end else
Node(l, x, r, (if hl >= hr then hl + 1 else hr + 1))
(* Same as bal, but repeat rebalancing until the final result
is balanced. *)
let rec join l x r =
match bal l x r with
Empty -> invalid_arg "Set.join"
| Node(l', x', r', _) as t' ->
let d = height l' - height r' in
if d < -2 or d > 2 then join l' x' r' else t'
(* Merge two trees l and r into one.
All elements of l must precede the elements of r.
Assumes | height l - height r | <= 2. *)
let rec merge t1 t2 =
match (t1, t2) with
(Empty, t) -> t
| (t, Empty) -> t
| (Node(l1, v1, r1, h1), Node(l2, v2, r2, h2)) ->
bal l1 v1 (bal (merge r1 l2) v2 r2)
(* Same as merge, but does not assume anything about l and r. *)
let rec concat t1 t2 =
match (t1, t2) with
(Empty, t) -> t
| (t, Empty) -> t
| (Node(l1, v1, r1, h1), Node(l2, v2, r2, h2)) ->
join l1 v1 (join (concat r1 l2) v2 r2)
(* Splitting *)
let rec split x = function
Empty ->
(Empty, None, Empty)
| Node(l, v, r, _) ->
let c = compare_elt x v in
if c = 0 then (l, Some v, r)
else if c < 0 then
let (ll, vl, rl) = split x l in (ll, vl, join rl v r)
else
let (lr, vr, rr) = split x r in (join l v lr, vr, rr)
(* Implementation of the set operations *)
let empty = Empty
let is_empty = function Empty -> true | _ -> false
let rec mem x = function
Empty -> false
| Node(l, v, r, _) ->
let c = compare_elt x v in
c = 0 || mem x (if c < 0 then l else r)
let rec add x = function
Empty -> Node(Empty, x, Empty, 1)
| Node(l, v, r, _) as t ->
let c = compare_elt x v in
if c = 0 then t else
if c < 0 then bal (add x l) v r else bal l v (add x r)
let singleton x = Node(Empty, x, Empty, 1)
let rec remove x = function
Empty -> Empty
| Node(l, v, r, _) ->
let c = compare_elt x v in
if c = 0 then merge l r else
if c < 0 then bal (remove x l) v r else bal l v (remove x r)
let rec union s1 s2 =
match (s1, s2) with
(Empty, t2) -> t2
| (t1, Empty) -> t1
| (Node(l1, v1, r1, h1), Node(l2, v2, r2, h2)) ->
if h1 >= h2 then
if h2 = 1 then add v2 s1 else begin
let (l2, _, r2) = split v1 s2 in
join (union l1 l2) v1 (union r1 r2)
end
else
if h1 = 1 then add v1 s2 else begin
let (l1, _, r1) = split v2 s1 in
join (union l1 l2) v2 (union r1 r2)
end
let rec inter s1 s2 =
match (s1, s2) with
(Empty, t2) -> Empty
| (t1, Empty) -> Empty
| (Node(l1, v1, r1, _), t2) ->
match split v1 t2 with
(l2, None, r2) ->
concat (inter l1 l2) (inter r1 r2)
| (l2, Some _, r2) ->
join (inter l1 l2) v1 (inter r1 r2)
let rec diff s1 s2 =
match (s1, s2) with
(Empty, t2) -> Empty
| (t1, Empty) -> t1
| (Node(l1, v1, r1, _), t2) ->
match split v1 t2 with
(l2, None, r2) ->
join (diff l1 l2) v1 (diff r1 r2)
| (l2, Some _, r2) ->
concat (diff l1 l2) (diff r1 r2)
let equal s1 s2 =
compare s1 s2 = 0
let rec subset s1 s2 =
match (s1, s2) with
Empty, _ ->
true
| _, Empty ->
false
| Node (l1, v1, r1, _), (Node (l2, v2, r2, _) as t2) ->
let c = compare_elt v1 v2 in
if c = 0 then
subset l1 l2 && subset r1 r2
else if c < 0 then
subset (Node (l1, v1, Empty, 0)) l2 && subset r1 t2
else
subset (Node (Empty, v1, r1, 0)) r2 && subset l1 t2
let rec iter f = function
Empty -> ()
| Node(l, v, r, _) -> iter f l; f v; iter f r
let rec fold f s accu =
match s with
Empty -> accu
| Node(l, v, r, _) -> fold f l (f v (fold f r accu))
let rec for_all p = function
Empty -> true
| Node(l, v, r, _) -> p v && for_all p l && for_all p r
let rec exists p = function
Empty -> false
| Node(l, v, r, _) -> p v || exists p l || exists p r
let filter p s =
let rec filt accu = function
| Empty -> accu
| Node(l, v, r, _) ->
filt (filt (if p v then add v accu else accu) l) r in
filt Empty s
let partition p s =
let rec part (t, f as accu) = function
| Empty -> accu
| Node(l, v, r, _) ->
part (part (if p v then (add v t, f) else (t, add v f)) l) r in
part (Empty, Empty) s
let rec cardinal = function
Empty -> 0
| Node(l, v, r, _) -> cardinal l + 1 + cardinal r
let rec elements_aux accu = function
Empty -> accu
| Node(l, v, r, _) -> elements_aux (v :: elements_aux accu r) l
let elements s =
elements_aux [] s
let rec min_elt = function
Empty -> raise Not_found
| Node(Empty, v, r, _) -> v
| Node(l, v, r, _) -> min_elt l
let rec max_elt = function
Empty -> raise Not_found
| Node(l, v, Empty, _) -> v
| Node(l, v, r, _) -> max_elt r
let choose = min_elt
end
^ permalink raw reply [flat|nested] 5+ messages in thread
* Re: [Caml-list] Recursive types and functors.
2003-03-26 8:25 ` Jean-Christophe Filliatre
@ 2003-03-26 8:57 ` David Brown
2003-03-26 15:59 ` brogoff
2003-03-26 9:13 ` Claude Marche
1 sibling, 1 reply; 5+ messages in thread
From: David Brown @ 2003-03-26 8:57 UTC (permalink / raw)
To: Caml List
On Wed, Mar 26, 2003 at 09:25:13AM +0100, Jean-Christophe Filliatre wrote:
> A (too) naive solution could be to make a polymorphic instance of the
> Set module (either by adding an argument 'a everywhere in signatures
> OrderedType and S, or by copying the functor body and replacing
> Ord.compare by compare); then you have polymorphic sets, say 'a Set.t,
> balanced using compare, and you can define
Actually, my real case doesn't use sets, but a dynamic array
implementation I made myself. I originally needed a functor because I
needed an empty value to fill in past the used elements of the real
array.
What I ended up doing was filling in those elements with 'Obj.magic 0'.
I don't really like walking outside of the type system, but since I
never return them, I don't think it will be a problem.
I still may try to figure out how to do it with the multiple functor
approach, just so to learn how to do it.
Thanks,
Dave
-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
^ permalink raw reply [flat|nested] 5+ messages in thread
* Re: [Caml-list] Recursive types and functors.
2003-03-26 8:25 ` Jean-Christophe Filliatre
2003-03-26 8:57 ` David Brown
@ 2003-03-26 9:13 ` Claude Marche
1 sibling, 0 replies; 5+ messages in thread
From: Claude Marche @ 2003-03-26 9:13 UTC (permalink / raw)
To: Jean-Christophe Filliatre; +Cc: David Brown, Caml List
[-- Attachment #1: message body and .signature --]
[-- Type: text/plain, Size: 1847 bytes --]
>>>>> "JCF" == Jean-Christophe Filliatre <Jean-Christophe.Filliatre@lri.fr> writes:
JCF> David Brown writes:
>> I have a recursive type where I'd like one of the constructors of the
>> type to contain a set of the type (or something like set). However, I
>> can't figure out how to represent this.
>>
>> For example:
>>
>> type foo =
>> | Integer of int
>> | String of string
>> | Set of FooSet
>>
>> module FooSet = Set.Make (struct type t = foo let compare = compare end)
>>
>> but this obviously doesn't work.
JCF> There is (at least) another solution: to use a set implementation
JCF> where comparison does not require a comparison of elements. This is
JCF> possible if, for instance, you are performing hash-consing on type foo
JCF> (which result in tagging foo values with integers, then used in the
JCF> comparison). This solution is used in Claude Marché's regexp library
JCF> (http://www.lri.fr/~marche/regexp/) and uses a hash-consing technique
JCF> available here: http://www.lri.fr/~filliatr/software.en.html
Please find below a solution to your problem using this last
solution. In fact this is independant of hash-consing, only tagging
values with unique integers is important. hash-consing can be added if
wanted. I hope my files are self-explanatory, but otherwise please
ask me if you need help. The module Inttagset is a variant of patricia
trees borrowed from JCF. The module Foo is what you are looking for,
and test.ml is a example of use.
JCF> Hope this helps,
Me too !
--
| Claude Marché | mailto:Claude.Marche@lri.fr |
| LRI - Bât. 490 | http://www.lri.fr/~marche/ |
| Université de Paris-Sud | phoneto: +33 1 69 15 64 85 |
| F-91405 ORSAY Cedex | faxto: +33 1 69 15 65 86 |
[-- Attachment #2: inttagset.mli --]
[-- Type: application/octet-stream, Size: 2047 bytes --]
(*
* Ptset: Sets of integers implemented as Patricia trees.
* Copyright (C) 2000 Jean-Christophe FILLIATRE
*
* This software is free software; you can redistribute it and/or
* modify it under the terms of the GNU Library General Public
* License version 2, as published by the Free Software Foundation.
*
* This software is distributed in the hope that it will be useful,
* but WITHOUT ANY WARRANTY; without even the implied warranty of
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
*
* See the GNU Library General Public License version 2 for more details
* (enclosed in the file LGPL).
*)
(*i $Id: inttagset.mli,v 1.1 2003/03/07 14:04:01 marche Exp $ i*)
(*s Sets of integers implemented as Patricia trees. The following
signature is exactly [Set.S with type elt = int], with the same
specifications. This is a purely functional data-structure. The
performances are always better than the standard library's module
[Set], except for linear insertion (building a set by insertion of
consecutive integers). *)
type 'a t
val empty : 'a t
val is_empty : 'a t -> bool
val mem : int -> 'a t -> bool
val add : int -> 'a -> 'a t -> 'a t
val singleton : int -> 'a -> 'a t
val remove : int -> 'a t -> 'a t
val union : 'a t -> 'a t -> 'a t
val subset : 'a t -> 'a t -> bool
val inter : 'a t -> 'a t -> 'a t
val diff : 'a t -> 'a t -> 'a t
val equal : 'a t -> 'a t -> bool
val compare : 'a t -> 'a t -> int
val elements : 'a t -> 'a list
val choose : 'a t -> 'a
val cardinal : 'a t -> int
val iter : ('a -> unit) -> 'a t -> unit
val fold : ('a -> 'b -> 'b) -> 'a t -> 'b -> 'b
val for_all : ('a -> bool) -> 'a t -> bool
val exists : ('a -> bool) -> 'a t -> bool
val filter : ('a -> bool) -> 'a t -> 'a t
val partition : ('a -> bool) -> 'a t -> 'a t * 'a t
(*s Additional functions not appearing in the signature [Set.S] from ocaml
standard library. *)
(* [intersect u v] determines if sets [u] and [v] have a non-empty
intersection. *)
val intersect : 'a t -> 'a t -> bool
[-- Attachment #3: inttagset.ml --]
[-- Type: application/octet-stream, Size: 10945 bytes --]
(*
* Ptset: Sets of integers implemented as Patricia trees.
* Copyright (C) 2000 Jean-Christophe FILLIATRE
*
* This software is free software; you can redistribute it and/or
* modify it under the terms of the GNU Library General Public
* License version 2, as published by the Free Software Foundation.
*
* This software is distributed in the hope that it will be useful,
* but WITHOUT ANY WARRANTY; without even the implied warranty of
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
*
* See the GNU Library General Public License version 2 for more details
* (enclosed in the file LGPL).
*)
(*i $Id: inttagset.ml,v 1.1 2003/03/07 14:04:01 marche Exp $ i*)
(*s Sets of integers implemented as Patricia trees, following Chris
Okasaki and Andrew Gill's paper {\em Fast Mergeable Integer Maps}
({\tt\small http://www.cs.columbia.edu/\~{}cdo/papers.html\#ml98maps}).
Patricia trees provide faster operations than standard library's
module [Set], and especially very fast [union], [subset], [inter]
and [diff] operations. *)
(*s The idea behind Patricia trees is to build a {\em trie} on the
binary digits of the elements, and to compact the representation
by branching only one the relevant bits (i.e. the ones for which
there is at least on element in each subtree). We implement here
{\em little-endian} Patricia trees: bits are processed from
least-significant to most-significant. The trie is implemented by
the following type [t]. [Empty] stands for the empty trie, and
[Leaf k] for the singleton [k]. (Note that [k] is the actual
element.) [Branch (m,p,l,r)] represents a branching, where [p] is
the prefix (from the root of the trie) and [m] is the branching
bit (a power of 2). [l] and [r] contain the subsets for which the
branching bit is respectively 0 and 1. Invariant: the trees [l]
and [r] are not empty. *)
type 'a t =
| Empty
| Leaf of int * 'a
| Branch of int * int * 'a t * 'a t
(*s Example: the representation of the set $\{1,4,5\}$ is
$$\mathtt{Branch~(0,~1,~Leaf~4,~Branch~(1,~4,~Leaf~1,~Leaf~5))}$$
The first branching bit is the bit 0 (and the corresponding prefix
is [0b0], not of use here), with $\{4\}$ on the left and $\{1,5\}$ on the
right. Then the right subtree branches on bit 2 (and so has a branching
value of $2^2 = 4$), with prefix [0b01 = 1]. *)
(*s Empty set and singletons. *)
let empty = Empty
let is_empty = function Empty -> true | _ -> false
let singleton k e = Leaf(k,e)
(*s Testing the occurrence of a value is similar to the search in a
binary search tree, where the branching bit is used to select the
appropriate subtree. *)
let zero_bit k m = (k land m) == 0
let rec mem k = function
| Empty -> false
| Leaf(j,_) -> k == j
| Branch (_, m, l, r) -> mem k (if zero_bit k m then l else r)
(*s The following operation [join] will be used in both insertion and
union. Given two non-empty trees [t0] and [t1] with longest common
prefixes [p0] and [p1] respectively, which are supposed to
disagree, it creates the union of [t0] and [t1]. For this, it
computes the first bit [m] where [p0] and [p1] disagree and create
a branching node on that bit. Depending on the value of that bit
in [p0], [t0] will be the left subtree and [t1] the right one, or
the converse. Computing the first branching bit of [p0] and [p1]
uses a nice property of twos-complement representation of integers. *)
let lowest_bit x = x land (-x)
let branching_bit p0 p1 = lowest_bit (p0 lxor p1)
let mask p m = p land (m-1)
let join (p0,t0,p1,t1) =
let m = branching_bit p0 p1 in
if zero_bit p0 m then
Branch (mask p0 m, m, t0, t1)
else
Branch (mask p0 m, m, t1, t0)
(*s Then the insertion of value [k] in set [t] is easily implemented
using [join]. Insertion in a singleton is just the identity or a
call to [join], depending on the value of [k]. When inserting in
a branching tree, we first check if the value to insert [k]
matches the prefix [p]: if not, [join] will take care of creating
the above branching; if so, we just insert [k] in the appropriate
subtree, depending of the branching bit. *)
let match_prefix k p m = (mask k m) == p
let rec ins e k = function
| Empty -> Leaf (k,e)
| Leaf(j,_) as t ->
if j == k then t else join (k, Leaf (k,e), j, t)
| Branch (p,m,t0,t1) as t ->
if match_prefix k p m then
if zero_bit k m then
Branch (p, m, ins e k t0, t1)
else
Branch (p, m, t0, ins e k t1)
else
join (k, Leaf (k,e), p, t)
let add k e t = ins e k t
(*s The code to remove an element is basically similar to the code of
insertion. But since we have to maintain the invariant that both
subtrees of a [Branch] node are non-empty, we use here the
``smart constructor'' [branch] instead of [Branch]. *)
let branch = function
| (_,_,Empty,t) -> t
| (_,_,t,Empty) -> t
| (p,m,t0,t1) -> Branch (p,m,t0,t1)
let rec rmv k = function
| Empty -> Empty
| Leaf(j,_) as t -> if k == j then Empty else t
| Branch (p,m,t0,t1) as t ->
if match_prefix k p m then
if zero_bit k m then
branch (p, m, rmv k t0, t1)
else
branch (p, m, t0, rmv k t1)
else
t
let remove k t = rmv k t
(*s One nice property of Patricia trees is to support a fast union
operation (and also fast subset, difference and intersection
operations). When merging two branching trees we examine the
following four cases: (1) the trees have exactly the same
prefix; (2/3) one prefix contains the other one; and (4) the
prefixes disagree. In cases (1), (2) and (3) the recursion is
immediate; in case (4) the function [join] creates the appropriate
branching. *)
let rec merge = function
| Empty, t -> t
| t, Empty -> t
| Leaf(k,e), t -> add k e t
| t, Leaf(k,e) -> add k e t
| (Branch (p,m,s0,s1) as s), (Branch (q,n,t0,t1) as t) ->
if m == n && match_prefix q p m then
(* The trees have the same prefix. Merge the subtrees. *)
Branch (p, m, merge (s0,t0), merge (s1,t1))
else if m < n && match_prefix q p m then
(* [q] contains [p]. Merge [t] with a subtree of [s]. *)
if zero_bit q m then
Branch (p, m, merge (s0,t), s1)
else
Branch (p, m, s0, merge (s1,t))
else if m > n && match_prefix p q n then
(* [p] contains [q]. Merge [s] with a subtree of [t]. *)
if zero_bit p n then
Branch (q, n, merge (s,t0), t1)
else
Branch (q, n, t0, merge (s,t1))
else
(* The prefixes disagree. *)
join (p, s, q, t)
let union s t = merge (s,t)
(*s When checking if [s1] is a subset of [s2] only two of the above
four cases are relevant: when the prefixes are the same and when the
prefix of [s1] contains the one of [s2], and then the recursion is
obvious. In the other two cases, the result is [false]. *)
let rec subset s1 s2 = match (s1,s2) with
| Empty, _ -> true
| _, Empty -> false
| Leaf(k1,_), _ -> mem k1 s2
| Branch _, Leaf _ -> false
| Branch (p1,m1,l1,r1), Branch (p2,m2,l2,r2) ->
if m1 == m2 && p1 == p2 then
subset l1 l2 && subset r1 r2
else if m1 > m2 && match_prefix p1 p2 m2 then
if zero_bit p1 m2 then
subset l1 l2 && subset r1 l2
else
subset l1 r2 && subset r1 r2
else
false
(*s To compute the intersection and the difference of two sets, we
still examine the same four cases as in [merge]. The recursion is
then obvious. *)
let rec inter s1 s2 = match (s1,s2) with
| Empty, _ -> Empty
| _, Empty -> Empty
| Leaf(k1,_), _ -> if mem k1 s2 then s1 else Empty
| _, Leaf(k2,_) -> if mem k2 s1 then s2 else Empty
| Branch (p1,m1,l1,r1), Branch (p2,m2,l2,r2) ->
if m1 == m2 && p1 == p2 then
merge (inter l1 l2, inter r1 r2)
else if m1 < m2 && match_prefix p2 p1 m1 then
inter (if zero_bit p2 m1 then l1 else r1) s2
else if m1 > m2 && match_prefix p1 p2 m2 then
inter s1 (if zero_bit p1 m2 then l2 else r2)
else
Empty
let rec diff s1 s2 = match (s1,s2) with
| Empty, _ -> Empty
| _, Empty -> s1
| Leaf(k1,_), _ -> if mem k1 s2 then Empty else s1
| _, Leaf(k2,_) -> remove k2 s1
| Branch (p1,m1,l1,r1), Branch (p2,m2,l2,r2) ->
if m1 == m2 && p1 == p2 then
merge (diff l1 l2, diff r1 r2)
else if m1 < m2 && match_prefix p2 p1 m1 then
if zero_bit p2 m1 then
merge (diff l1 s2, r1)
else
merge (l1, diff r1 s2)
else if m1 > m2 && match_prefix p1 p2 m2 then
if zero_bit p1 m2 then diff s1 l2 else diff s1 r2
else
s1
(*s All the following operations ([cardinal], [iter], [fold], [for_all],
[exists], [filter], [partition], [choose], [elements]) are
implemented as for any other kind of binary trees. *)
let rec cardinal = function
| Empty -> 0
| Leaf _ -> 1
| Branch (_,_,t0,t1) -> cardinal t0 + cardinal t1
;;
let rec iter f = function
| Empty -> ()
| Leaf(_,e) -> f e
| Branch (_,_,t0,t1) -> iter f t0; iter f t1
;;
let rec fold f s accu = match s with
| Empty -> accu
| Leaf(_,e) -> f e accu
| Branch (_,_,t0,t1) -> fold f t0 (fold f t1 accu)
;;
let rec for_all p = function
| Empty -> true
| Leaf(_,e) -> p e
| Branch (_,_,t0,t1) -> for_all p t0 && for_all p t1
;;
let rec exists p = function
| Empty -> false
| Leaf(_,e) -> p e
| Branch (_,_,t0,t1) -> exists p t0 || exists p t1
;;
let filter p s =
let rec filt acc = function
| Empty -> acc
| Leaf(k,e) -> if p e then add k e acc else acc
| Branch (_,_,t0,t1) -> filt (filt acc t0) t1
in
filt Empty s
;;
let partition p s =
let rec part (t,f as acc) = function
| Empty -> acc
| Leaf(k,e) -> if p e then (add k e t, f) else (t, add k e f)
| Branch (_,_,t0,t1) -> part (part acc t0) t1
in
part (Empty, Empty) s
;;
let rec choose = function
| Empty -> raise Not_found
| Leaf(_,e) -> e
| Branch (_, _,t0,_) -> choose t0 (* we know that [t0] is non-empty *)
;;
let elements s =
let rec elements_aux acc = function
| Empty -> acc
| Leaf(_,e) -> e :: acc
| Branch (_,_,l,r) -> elements_aux (elements_aux acc l) r
in
elements_aux [] s
;;
(*s Another nice property of Patricia trees is to be independent of the
order of insertion. As a consequence, two Patricia trees have the
same elements if and only if they are structurally equal. *)
let equal = (=)
let compare = compare
(*s Additional functions w.r.t to [Set.S]. *)
let rec intersect s1 s2 = match (s1,s2) with
| Empty, _ -> false
| _, Empty -> false
| Leaf(k1,_), _ -> mem k1 s2
| _, Leaf(k2,_) -> mem k2 s1
| Branch (p1,m1,l1,r1), Branch (p2,m2,l2,r2) ->
if m1 == m2 && p1 == p2 then
intersect l1 l2 || intersect r1 r2
else if m1 < m2 && match_prefix p2 p1 m1 then
intersect (if zero_bit p2 m1 then l1 else r1) s2
else if m1 > m2 && match_prefix p1 p2 m2 then
intersect s1 (if zero_bit p1 m2 then l2 else r2)
else
false
[-- Attachment #4: foo.mli --]
[-- Type: application/octet-stream, Size: 326 bytes --]
type foo;;
type foo_node =
| Integer of int
| String of string
| Set of foo Inttagset.t
type foo_set = foo Inttagset.t
val foo_node : foo -> foo_node;;
val foo_int : int -> foo
val foo_string : string -> foo
val foo_set : foo_set -> foo
val foo_add : foo -> foo_set -> foo_set
val foo_mem : foo -> foo_set -> bool
[-- Attachment #5: foo.ml --]
[-- Type: application/octet-stream, Size: 595 bytes --]
type foo =
{
foo_tag : int;
foo_val : foo_node
}
and foo_node =
| Integer of int
| String of string
| Set of foo Inttagset.t
type foo_set = foo Inttagset.t;;
let foo_node f = f.foo_val
let tag_counter = ref 0
let foo_int i =
incr tag_counter;
{ foo_tag = !tag_counter; foo_val = Integer i }
let foo_string s =
incr tag_counter;
{ foo_tag = !tag_counter; foo_val = String s }
let foo_set s =
incr tag_counter;
{ foo_tag = !tag_counter; foo_val = Set s }
let foo_add f s = Inttagset.add f.foo_tag f s;;
let foo_mem f s = Inttagset.mem f.foo_tag s;;
[-- Attachment #6: test.ml --]
[-- Type: application/octet-stream, Size: 433 bytes --]
#load "inttagset.cmo";;
#load "foo.cmo";;
open Foo;;
let v1 =
foo_set
(foo_add (foo_int 4)
(foo_add (foo_string "hello")
Inttagset.empty));;
let v2 =
foo_set
(foo_add (foo_string "world")
(foo_add v1 Inttagset.empty));;
let rec all_strings foo acc =
match foo_node foo with
| Integer _ -> acc
| String s -> s::acc
| Set s -> Inttagset.fold all_strings s acc
;;
all_string v2;;
^ permalink raw reply [flat|nested] 5+ messages in thread
* Re: [Caml-list] Recursive types and functors.
2003-03-26 8:57 ` David Brown
@ 2003-03-26 15:59 ` brogoff
0 siblings, 0 replies; 5+ messages in thread
From: brogoff @ 2003-03-26 15:59 UTC (permalink / raw)
To: David Brown; +Cc: Caml List
Hi Dave,
There is no good solution for the problem (on the Subject: line that is) in
the language. This is on my "most annoying flaws of OCaml" list. It's been
dicussed several times on this list, and I think if you look on comp.lang.ml
you'll see a recent thread there too.
One solution you can use is the parametrization trick, that is, using an
extra type variable to untie the recursive knot. You can do this with sets in
OCaml by writing a polymorphic set functor, as others have explained. I don't
know how you'd do something similar in SML, which doesn't have a polymorphic
compare.
This really needs a solution sooner rather than later. It makes me wonder
what the point of functors is, since they're obviously not for abstract data
type libraries. OK, I'm just kidding, but it is a nasty problem.
-- Brian
On Wed, 26 Mar 2003, David Brown wrote:
> On Wed, Mar 26, 2003 at 09:25:13AM +0100, Jean-Christophe Filliatre wrote:
>
> > A (too) naive solution could be to make a polymorphic instance of the
> > Set module (either by adding an argument 'a everywhere in signatures
> > OrderedType and S, or by copying the functor body and replacing
> > Ord.compare by compare); then you have polymorphic sets, say 'a Set.t,
> > balanced using compare, and you can define
>
> Actually, my real case doesn't use sets, but a dynamic array
> implementation I made myself. I originally needed a functor because I
> needed an empty value to fill in past the used elements of the real
> array.
>
> What I ended up doing was filling in those elements with 'Obj.magic 0'.
> I don't really like walking outside of the type system, but since I
> never return them, I don't think it will be a problem.
>
> I still may try to figure out how to do it with the multiple functor
> approach, just so to learn how to do it.
>
> Thanks,
> Dave
>
> -------------------
> To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
> Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
>
-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
^ permalink raw reply [flat|nested] 5+ messages in thread
end of thread, other threads:[~2003-03-26 15:59 UTC | newest]
Thread overview: 5+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2003-03-26 6:28 [Caml-list] Recursive types and functors David Brown
2003-03-26 8:25 ` Jean-Christophe Filliatre
2003-03-26 8:57 ` David Brown
2003-03-26 15:59 ` brogoff
2003-03-26 9:13 ` Claude Marche
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox