diff --git a/src/Atom.ml b/src/Atom.ml index 6154a84d1ee172fd48973a55a111a2169434a61e..cd45fa1b82c2f13269df9384e223220913656799 100644 --- a/src/Atom.ml +++ b/src/Atom.ml @@ -154,11 +154,18 @@ module Set = struct (* Sets of atoms form a monoid under union. *) - class ['z] monoid = object + class ['z] union_monoid = object method zero: 'z = empty method plus: 'z -> 'z -> 'z = union end + (* Sets of atoms form a monoid under disjoint union. *) + + class ['z] disjoint_union_monoid = object + method zero: 'z = empty + method plus: 'z -> 'z -> 'z = disjoint_union + end + (* These printing functions should be used for debugging purposes only. *) let print_to_scratch xs = diff --git a/src/Atom.mli b/src/Atom.mli index 6521dfd77268f8446f8e187d826b54bf7535172f..0dcbb64a4234623372a040f9f16462229acf2060 100644 --- a/src/Atom.mli +++ b/src/Atom.mli @@ -33,9 +33,15 @@ module Set : sig exception NonDisjointUnion of atom val disjoint_union: t -> t -> t - (* Sets of atoms form a monoid under union. *) + (* Sets of atoms form monoids under union and disjoint union. *) - class ['z] monoid : object + class ['z] union_monoid : object + constraint 'z = t + method zero: 'z + method plus: 'z -> 'z -> 'z + end + + class ['z] disjoint_union_monoid : object constraint 'z = t method zero: 'z method plus: 'z -> 'z -> 'z