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