[sledge] Switch Zero-One-Many type to a standard variant

Reviewed By: jvillard

Differential Revision: D26338018

fbshipit-source-id: 4fe5aea9f

sledge/nonstdlib/NS.mli

@@ -150,6 +150,9 @@ module Comparer = Comparer
 module Option = Option
 include module type of Option.Import
 
+type 'a zero_one_many = Zero | One of 'a | Many
+type ('a, 'b) zero_one_many2 = Zero2 | One2 of 'a * 'b | Many2
+
 module Either : sig
   type ('a, 'b) t = Left of 'a | Right of 'b
 

sledge/nonstdlib/NS0.ml

@@ -131,6 +131,9 @@ let fold_map_from_map map x s ~f =
 
 (** Containers *)
 
+type 'a zero_one_many = Zero | One of 'a | Many
+type ('a, 'b) zero_one_many2 = Zero2 | One2 of 'a * 'b | Many2
+
 (* from upcoming Stdlib *)
 module Either = struct
   type ('a, 'b) t = Left of 'a | Right of 'b

sledge/nonstdlib/NSMap.ml

@@ -154,11 +154,11 @@ struct
 
   let classify m =
     match root_key m with
-    | None -> `Zero
+    | None -> Zero2
     | Some k -> (
       match M.split k m with
-      | l, Some v, r when is_empty l && is_empty r -> `One (k, v)
+      | l, Some v, r when is_empty l && is_empty r -> One2 (k, v)
-      | _ -> `Many )
+      | _ -> Many2 )
 
   let choose_key = root_key
   let choose = root_binding

sledge/nonstdlib/NSMap_intf.ml

@@ -69,7 +69,7 @@ module type S = sig
   val is_singleton : 'a t -> bool
   val length : 'a t -> int
   val only_binding : 'a t -> (key * 'a) option
-  val classify : 'a t -> [`Zero | `One of key * 'a | `Many]
+  val classify : 'a t -> (key, 'a) zero_one_many2
 
   val choose_key : 'a t -> key option
   (** Find an unspecified key. Different keys may be chosen for equivalent

sledge/nonstdlib/NSSet.ml

@@ -98,11 +98,11 @@ struct
 
   let classify s =
     match root_elt s with
-    | None -> `Zero
+    | None -> Zero
     | Some elt -> (
       match S.split elt s with
-      | l, true, r when is_empty l && is_empty r -> `One elt
+      | l, true, r when is_empty l && is_empty r -> One elt
-      | _ -> `Many )
+      | _ -> Many )
 
   let pop s =
     match choose s with

sledge/nonstdlib/NSSet_intf.ml

@@ -72,7 +72,7 @@ module type S = sig
   val disjoint : t -> t -> bool
   val max_elt : t -> elt option
   val only_elt : t -> elt option
-  val classify : t -> [`Zero | `One of elt | `Many]
+  val classify : t -> elt zero_one_many
 
   val pop : t -> (elt * t) option
   (** Find and remove an unspecified element. [O(1)]. *)

sledge/nonstdlib/multiset_intf.ml

@@ -109,7 +109,7 @@ module type S = sig
   val pop_min_elt : t -> (elt * mul * t) option
   (** Find and remove minimum element. [O(log n)]. *)
 
-  val classify : t -> [`Zero | `One of elt * mul | `Many]
+  val classify : t -> (elt, mul) zero_one_many2
   (** Classify a set as either empty, singleton, or otherwise. *)
 
   val find_and_remove : elt -> t -> (mul * t) option

sledge/src/fol/arithmetic.ml

@@ -168,28 +168,28 @@ struct
 
     let classify poly =
       match Sum.classify poly with
-      | `Zero -> Const Q.zero
+      | Zero2 -> Const Q.zero
-      | `One (mono, coeff) -> (
+      | One2 (mono, coeff) -> (
         match Prod.classify mono with
-        | `Zero -> Const coeff
+        | Zero2 -> Const coeff
-        | `One (trm, 1) ->
+        | One2 (trm, 1) ->
             if Q.equal Q.one coeff then Trm trm else Interpreted
         | _ -> Uninterpreted )
-      | `Many -> Interpreted
+      | Many2 -> Interpreted
 
     let is_uninterpreted poly =
       match Sum.only_elt poly with
       | Some (mono, _) -> (
         match Prod.classify mono with
-        | `Zero -> false
+        | Zero2 -> false
-        | `One (_, 1) -> false
+        | One2 (_, 1) -> false
         | _ -> true )
       | None -> false
 
     let get_const poly =
       match Sum.classify poly with
-      | `Zero -> Some Q.zero
+      | Zero2 -> Some Q.zero
-      | `One (mono, coeff) when Mono.equal_one mono -> Some coeff
+      | One2 (mono, coeff) when Mono.equal_one mono -> Some coeff
       | _ -> None
 
     let get_mono poly =
@@ -258,8 +258,8 @@ struct
           | None -> ()
           | Some poly -> (
             match Sum.classify poly with
-            | `Many -> ()
+            | Many2 -> ()
-            | `Zero | `One _ ->
+            | Zero2 | One2 _ ->
                 (* polynomial factors are not constant or singleton, which
                    should have been flattened into the parent monomial *)
                 assert false ) ) ;
@@ -297,11 +297,11 @@ struct
         | Some poly -> (
           match Sum.classify poly with
           (* 0 ^ p₁ ==> 0 × 1 *)
-          | `Zero -> (Q.zero, Mono.one)
+          | Zero2 -> (Q.zero, Mono.one)
           (* (Σᵢ₌₁¹ cᵢ × Xᵢ) ^ p₁ ==> cᵢ^p₁ × Πⱼ₌₁¹ Xⱼ^pⱼ *)
-          | `One (mono, coeff) -> (Q.pow coeff power, Mono.pow mono power)
+          | One2 (mono, coeff) -> (Q.pow coeff power, Mono.pow mono power)
           (* (Σᵢ₌₁ⁿ cᵢ × Xᵢ) ^ p₁ ==> 1 × Πⱼ₌₁¹ (Σᵢ₌₁ⁿ cᵢ × Xᵢ)^pⱼ *)
-          | `Many -> (Q.one, Mono.of_ base power) )
+          | Many2 -> (Q.one, Mono.of_ base power) )
         (* X₁ ^ p₁ ==> 1 × Πⱼ₌₁¹ Xⱼ^pⱼ *)
         | None -> (Q.one, Mono.of_ base power)
 

sledge/src/fol/context.ml

@@ -997,8 +997,6 @@ let subst_invariant us s0 s =
           || not (Var.Set.subset (Trm.fv key) ~of_:us) ) ) ;
     true )
 
-type 'a zom = Zero | One of 'a | Many
-
 (** try to solve [p = q] such that [fv (p - q) ⊆ us ∪ xs] and [p - q]
     has at most one maximal solvable subterm, [kill], where
     [fv kill ⊈ us]; solve [p = q] for [kill]; extend subst mapping [kill]

sledge/src/fol/propositional.ml

@@ -95,12 +95,12 @@ struct
       then zero
       else
         match Fmls.classify neg with
-        | `Zero -> (
+        | Zero -> (
           match Fmls.classify pos with
-          | `Zero -> unit
+          | Zero -> unit
-          | `One p -> p
+          | One p -> p
-          | `Many -> cons ~pos ~neg )
+          | Many -> cons ~pos ~neg )
-        | `One n when Fmls.is_empty pos -> _Not n
+        | One n when Fmls.is_empty pos -> _Not n
         | _ -> cons ~pos ~neg
 
     let _And ~pos ~neg =