From dfd897d9e4facfd2e356a1fbedef6660c5434daf Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Sun, 21 Feb 2021 13:18:27 -0800 Subject: [PATCH] [sledge] Switch Zero-One-Many type to a standard variant Reviewed By: jvillard Differential Revision: D26338018 fbshipit-source-id: 4fe5aea9f --- sledge/nonstdlib/NS.mli | 3 +++ sledge/nonstdlib/NS0.ml | 3 +++ sledge/nonstdlib/NSMap.ml | 6 +++--- sledge/nonstdlib/NSMap_intf.ml | 2 +- sledge/nonstdlib/NSSet.ml | 6 +++--- sledge/nonstdlib/NSSet_intf.ml | 2 +- sledge/nonstdlib/multiset_intf.ml | 2 +- sledge/src/fol/arithmetic.ml | 28 ++++++++++++++-------------- sledge/src/fol/context.ml | 2 -- sledge/src/fol/propositional.ml | 10 +++++----- 10 files changed, 34 insertions(+), 30 deletions(-) diff --git a/sledge/nonstdlib/NS.mli b/sledge/nonstdlib/NS.mli index 604ab765d..a49e9fe6d 100644 --- a/sledge/nonstdlib/NS.mli +++ b/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 diff --git a/sledge/nonstdlib/NS0.ml b/sledge/nonstdlib/NS0.ml index 8f388beb9..693f1cd8a 100644 --- a/sledge/nonstdlib/NS0.ml +++ 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 diff --git a/sledge/nonstdlib/NSMap.ml b/sledge/nonstdlib/NSMap.ml index 50f2366fa..812148553 100644 --- a/sledge/nonstdlib/NSMap.ml +++ 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) - | _ -> `Many ) + | l, Some v, r when is_empty l && is_empty r -> One2 (k, v) + | _ -> Many2 ) let choose_key = root_key let choose = root_binding diff --git a/sledge/nonstdlib/NSMap_intf.ml b/sledge/nonstdlib/NSMap_intf.ml index b44f7e3e1..2e2b4992a 100644 --- a/sledge/nonstdlib/NSMap_intf.ml +++ b/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 diff --git a/sledge/nonstdlib/NSSet.ml b/sledge/nonstdlib/NSSet.ml index 4aa0ea305..ca171fabf 100644 --- a/sledge/nonstdlib/NSSet.ml +++ b/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 - | _ -> `Many ) + | l, true, r when is_empty l && is_empty r -> One elt + | _ -> Many ) let pop s = match choose s with diff --git a/sledge/nonstdlib/NSSet_intf.ml b/sledge/nonstdlib/NSSet_intf.ml index 1696b725b..ca26c3507 100644 --- a/sledge/nonstdlib/NSSet_intf.ml +++ b/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)]. *) diff --git a/sledge/nonstdlib/multiset_intf.ml b/sledge/nonstdlib/multiset_intf.ml index 51492bc1a..16689a28b 100644 --- a/sledge/nonstdlib/multiset_intf.ml +++ b/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 diff --git a/sledge/src/fol/arithmetic.ml b/sledge/src/fol/arithmetic.ml index dd46d1bc5..8feaae2c0 100644 --- a/sledge/src/fol/arithmetic.ml +++ b/sledge/src/fol/arithmetic.ml @@ -168,28 +168,28 @@ struct let classify poly = match Sum.classify poly with - | `Zero -> Const Q.zero - | `One (mono, coeff) -> ( + | Zero2 -> Const Q.zero + | One2 (mono, coeff) -> ( match Prod.classify mono with - | `Zero -> Const coeff - | `One (trm, 1) -> + | Zero2 -> Const coeff + | 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 - | `One (_, 1) -> false + | Zero2 -> false + | One2 (_, 1) -> false | _ -> true ) | None -> false let get_const poly = match Sum.classify poly with - | `Zero -> Some Q.zero - | `One (mono, coeff) when Mono.equal_one mono -> Some coeff + | Zero2 -> Some Q.zero + | 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 -> () - | `Zero | `One _ -> + | Many2 -> () + | 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) diff --git a/sledge/src/fol/context.ml b/sledge/src/fol/context.ml index 4e8983153..7fa17de25 100644 --- a/sledge/src/fol/context.ml +++ b/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] diff --git a/sledge/src/fol/propositional.ml b/sledge/src/fol/propositional.ml index de3540f39..e9ee848d3 100644 --- a/sledge/src/fol/propositional.ml +++ b/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 - | `One p -> p - | `Many -> cons ~pos ~neg ) - | `One n when Fmls.is_empty pos -> _Not n + | Zero -> unit + | One p -> p + | Many -> cons ~pos ~neg ) + | One n when Fmls.is_empty pos -> _Not n | _ -> cons ~pos ~neg let _And ~pos ~neg =