Add set/map to qvar and quality

engine/uState.ml

@@ -47,8 +47,8 @@ module QState : sig
 end =
 struct
 
-module QSet = Set.Make(Sorts.QVar)
-module QMap = Map.Make(Sorts.QVar)
+module QSet = Sorts.QVar.Set
+module QMap = Sorts.QVar.Map
 
 type t = {
   qmap : Sorts.Quality.t option QMap.t;

kernel/sorts.ml

@@ -54,11 +54,32 @@ struct
       Printf.sprintf "%sα%d" s q
 
   let raw_pr q = Pp.str (to_string q)
+
+  module Self = struct type nonrec t = t let compare = compare end
+  module Set = CSet.Make(Self)
+  module Map = CMap.Make(Self)
 end
 
 module Quality = struct
   type t = QVar of QVar.t | QProp | QSProp | QType
 
+  let equal a b = match a, b with
+    | QVar a, QVar b -> QVar.equal a b
+    | QProp, QProp | QSProp, QSProp | QType, QType -> true
+    | (QVar _ | QProp | QSProp | QType), _ -> false
+
+  let compare a b = match a, b with
+    | QVar a, QVar b -> QVar.compare a b
+    | QVar _, _ -> -1
+    | _, QVar _ -> 1
+    | QProp, QProp -> 0
+    | QProp, _ -> -1
+    | _, QProp -> 1
+    | QSProp, QSProp -> 0
+    | QSProp, _ -> -1
+    | _, QSProp -> 1
+    | QType, QType -> 0
+
   let pr prv = function
     | QVar v -> prv v
     | QProp -> Pp.str "Prop"
@@ -67,6 +88,10 @@ module Quality = struct
 
   let raw_pr q = pr QVar.raw_pr q
 
+  module Self = struct type nonrec t = t let compare = compare end
+  module Set = CSet.Make(Self)
+  module Map = CMap.Make(Self)
+
 end
 
 type t =

kernel/sorts.mli

@@ -29,16 +29,28 @@ sig
   val raw_pr : t -> Pp.t
   val to_string : t -> string
   (** Debug printing *)
+
+  module Set : CSig.SetS with type elt = t
+
+  module Map : CMap.ExtS with type key = t and module Set := Set
 end
 
 module Quality : sig
   type t =
     | QVar of QVar.t
     | QProp | QSProp | QType
 
+  val equal : t -> t -> bool
+
+  val compare : t -> t -> int
+
   val pr : (QVar.t -> Pp.t) -> t -> Pp.t
 
   val raw_pr : t -> Pp.t
+
+  module Set : CSig.SetS with type elt = t
+
+  module Map : CMap.ExtS with type key = t and module Set := Set
 end
 
 type t = private