From 21ced6af62939e3f441efcd74ba95a87ed57270d Mon Sep 17 00:00:00 2001 From: Mehdi Bouaziz Date: Mon, 11 Jun 2018 08:47:09 -0700 Subject: [PATCH] PartialOrder Reviewed By: ngorogiannis Differential Revision: D8350238 fbshipit-source-id: 3ec4f34 --- infer/src/bufferoverrun/itv.ml | 14 +------------- infer/src/istd/PartialOrder.ml | 25 +++++++++++++++++++++++++ infer/src/istd/PartialOrder.mli | 14 ++++++++++++++ 3 files changed, 40 insertions(+), 13 deletions(-) create mode 100644 infer/src/istd/PartialOrder.ml create mode 100644 infer/src/istd/PartialOrder.mli diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml index 447c090b4..b17bba3a5 100644 --- a/infer/src/bufferoverrun/itv.ml +++ b/infer/src/bufferoverrun/itv.ml @@ -690,19 +690,7 @@ module Bound = struct let eq : t -> t -> bool = fun x y -> le x y && le y x - let xcompare ~lhs ~rhs = - let ller = le lhs rhs in - let rlel = le rhs lhs in - match (ller, rlel) with - | true, true -> - `Equal - | true, false -> - `LeftSmallerThanRight - | false, true -> - `RightSmallerThanLeft - | false, false -> - `NotComparable - + let xcompare = PartialOrder.of_le ~le let remove_max_int : t -> t = fun x -> diff --git a/infer/src/istd/PartialOrder.ml b/infer/src/istd/PartialOrder.ml new file mode 100644 index 000000000..a9f98c59a --- /dev/null +++ b/infer/src/istd/PartialOrder.ml @@ -0,0 +1,25 @@ +(* + * Copyright (c) 2018-present, Facebook, Inc. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) + +open! IStd + +type total = [`LeftSmallerThanRight | `Equal | `RightSmallerThanLeft] + +type t = [total | `NotComparable] + +let of_le ~le ~lhs ~rhs = + let ller = le lhs rhs in + let rlel = le rhs lhs in + match (ller, rlel) with + | true, true -> + `Equal + | true, false -> + `LeftSmallerThanRight + | false, true -> + `RightSmallerThanLeft + | false, false -> + `NotComparable diff --git a/infer/src/istd/PartialOrder.mli b/infer/src/istd/PartialOrder.mli new file mode 100644 index 000000000..bb27e24be --- /dev/null +++ b/infer/src/istd/PartialOrder.mli @@ -0,0 +1,14 @@ +(* + * Copyright (c) 2018-present, Facebook, Inc. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) + +open! IStd + +type total = [`LeftSmallerThanRight | `Equal | `RightSmallerThanLeft] + +type t = [total | `NotComparable] + +val of_le : le:('a -> 'a -> bool) -> lhs:'a -> rhs:'a -> t