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