1(*
2 * Copyright 2014, NICTA
3 *
4 * This software may be distributed and modified according to the terms of
5 * the BSD 2-Clause license. Note that NO WARRANTY is provided.
6 * See "LICENSE_BSD2.txt" for details.
7 *
8 * @TAG(NICTA_BSD)
9 *)
10
11(*
12 * Sets of items.
13 *
14 * Currently implemented using sorted lists.
15 *)
16
17signature SET =
18sig
19  type key
20  type 'a set
21
22  val empty : key set
23  val is_empty : key set -> bool
24  val make : key list -> key set
25  val dest : key set -> key list
26  val inter : key set -> key set -> key set
27  val subtract : key set -> key set -> key set (* NOTE: subtracts first from second *)
28  val union : key set -> key set -> key set
29  val union_sets : key set list -> key set
30  val insert : key -> key set -> key set
31  val contains : key set -> key -> bool
32  val subset : (key set * key set) -> bool
33  val card: key set -> int
34  val map: (key -> key) -> key set -> key set
35  val filter: (key -> bool) -> key set -> key set
36end;
37
38functor Set(Key: KEY): SET =
39struct
40
41type key = Key.key;
42
43(*
44 * We wrap everything in a private datatype to enforce the user to only use the
45 * abstract interface.
46 *)
47datatype 'a set = S of 'a list;
48
49(* Make a set from a list. *)
50fun make x = Ord_List.make Key.ord x |> S
51
52(* Convert the set back into a list. *)
53fun dest (S x) = x
54
55(* Emptiness *)
56val empty = S []
57fun is_empty (S x) = (length x = 0)
58
59(* Set manipulation. *)
60fun inter (S a) (S b) = Ord_List.inter Key.ord a b |> S
61fun subtract (S a) (S b) = Ord_List.subtract Key.ord a b |> S
62fun union (S a) (S b) = Ord_List.union Key.ord a b |> S
63fun insert a (S b) = Ord_List.insert Key.ord a b |> S
64fun union_sets l = fold union l empty
65fun contains (S l) a = Ord_List.member Key.ord l a
66fun subset (S a, S b) = Ord_List.subset Key.ord (a, b)
67fun card (S a) = length a
68fun map f (S a) = make (List.map f a)
69fun filter f (S a) = S (List.filter f a)
70
71end;
72
73structure Intset = Set(type key = int val ord = int_ord);
74structure Symset = Set(type key = string val ord = fast_string_ord);
75structure Varset = Set(type key = (string * typ) val ord =
76    fn (a,b) => Term_Ord.var_ord (((fst a, 0), snd a), ((fst b, 0), snd b)));
77structure Typset = Set(type key = typ val ord = Term_Ord.typ_ord);
78
79type varset = Varset.key Varset.set
80type symset = Symset.key Symset.set
81type typset = Typset.key Typset.set
82
83