[sledge] Improve Monad interface

Summary:
And add Monad.Make to implement the full interface from return and
bind.

Reviewed By: ngorogiannis

Differential Revision: D24532341

fbshipit-source-id: 5740ba1c2

sledge/nonstdlib/NS.ml

@@ -20,7 +20,7 @@ module Map = Map
 module Monad = Monad
 module Multiset = Multiset
 module Option = Option
-include Option.Infix
+include Option.Import
 module Q = Q_ext
 module Set = Set
 module Sign = Sign

sledge/nonstdlib/NS.mli

@@ -128,7 +128,7 @@ include module type of Iter.Import
 (** Containers *)
 
 module Option = Option
-include module type of Option.Infix
+include module type of Option.Import
 
 module Either : sig
   type ('a, 'b) t = Left of 'a | Right of 'b

sledge/nonstdlib/monad.ml

@@ -5,53 +5,47 @@
  * LICENSE file in the root directory of this source tree.
  *)
 
-module type S = sig
+include Monad_intf
+
+module Make (M : sig
   type 'a t
 
   val return : 'a -> 'a t
-  val bind : ('a -> 'b t) -> 'a t -> 'b t
+  val bind : 'a t -> ('a -> 'b t) -> 'b t
-
+end) =
-  module Import : sig
+struct
-    val ( >>= ) : 'a t -> ('a -> 'b t) -> 'b t
+  include M
-    val ( >>| ) : 'a t -> ('a -> 'b) -> 'b t
+
-    val ( let* ) : 'a t -> ('a -> 'b t) -> 'b t
+  let map f m = bind m (fun a -> return (f a))
-    val ( and* ) : 'a t -> 'b t -> ('a * 'b) t
+  let ap m n = bind m (fun f -> bind n (fun a -> return (f a)))
-    val ( let+ ) : 'a t -> ('a -> 'b) -> 'b t
+  let prod m n = bind m (fun a -> bind n (fun b -> return (a, b)))
-    val ( and+ ) : 'a t -> 'b t -> ('a * 'b) t
+
+  module Import = struct
+    let ( |>= ) m f = map f m
+    let ( >>= ) = bind
+    let ( let* ) = bind
+    let ( and* ) = prod
+    let ( let+ ) = ( |>= )
+    let ( and+ ) = prod
   end
+
+  let bind m ~f = bind m f
+  let map m ~f = map f m
 end
 
 module State (State : sig
   type t
 end) =
 struct
-  type state = State.t
+  include Make (struct
-  type 'a t = state -> 'a * state
+    type 'a t = State.t -> 'a * State.t
 
     let return a s = (a, s)
 
-  let bind k m s =
+    let bind m k s =
       let a, s = m s in
       k a s
+  end)
 
   let run m s = m s
-
-  module Import = struct
-    let ( >>= ) m k = bind k m
-    let ( let* ) m k = bind k m
-
-    let ( and* ) : 'a t -> 'b t -> ('a * 'b) t =
-     fun m n s ->
-      let a, s = m s in
-      let b, s = n s in
-      return (a, b) s
-
-    let ( >>| ) : 'a t -> ('a -> 'b) -> 'b t =
-     fun m f ->
-      let* a = m in
-      return (f a)
-
-    let ( let+ ) = ( >>| )
-    let ( and+ ) = ( and* )
-  end
 end

sledge/nonstdlib/monad.mli

@@ -5,28 +5,19 @@
  * LICENSE file in the root directory of this source tree.
  *)
 
-module type S = sig
+include module type of Monad_intf
+
+module Make (M : sig
   type 'a t
 
   val return : 'a -> 'a t
-  val bind : ('a -> 'b t) -> 'a t -> 'b t
+  val bind : 'a t -> ('a -> 'b t) -> 'b t
-
+end) : S with type 'a t = 'a M.t
-  module Import : sig
-    val ( >>= ) : 'a t -> ('a -> 'b t) -> 'b t
-    val ( >>| ) : 'a t -> ('a -> 'b) -> 'b t
-    val ( let* ) : 'a t -> ('a -> 'b t) -> 'b t
-    val ( and* ) : 'a t -> 'b t -> ('a * 'b) t
-    val ( let+ ) : 'a t -> ('a -> 'b) -> 'b t
-    val ( and+ ) : 'a t -> 'b t -> ('a * 'b) t
-  end
-end
 
 module State (State : sig
   type t
 end) : sig
-  type state = State.t
+  include S with type 'a t = State.t -> 'a * State.t
-
-  include S with type 'a t = state -> 'a * state
 
-  val run : 'a t -> state -> 'a * state
+  val run : 'a t -> State.t -> 'a * State.t
 end

sledge/nonstdlib/monad_intf.ml

@@ -0,0 +1,25 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+module type S = sig
+  type 'a t
+
+  val return : 'a -> 'a t
+  val bind : 'a t -> f:('a -> 'b t) -> 'b t
+  val map : 'a t -> f:('a -> 'b) -> 'b t
+  val ap : ('a -> 'b) t -> 'a t -> 'b t
+  val prod : 'a t -> 'b t -> ('a * 'b) t
+
+  module Import : sig
+    val ( |>= ) : 'a t -> ('a -> 'b) -> 'b t
+    val ( >>= ) : 'a t -> ('a -> 'b t) -> 'b t
+    val ( let* ) : 'a t -> ('a -> 'b t) -> 'b t
+    val ( and* ) : 'a t -> 'b t -> ('a * 'b) t
+    val ( let+ ) : 'a t -> ('a -> 'b) -> 'b t
+    val ( and+ ) : 'a t -> 'b t -> ('a * 'b) t
+  end
+end

sledge/nonstdlib/option.ml

@@ -7,6 +7,7 @@
 
 open! NS0
 include Containers.Option
+include Monad.Make (Containers.Option)
 
 type 'a t = 'a option [@@deriving compare, equal, hash, sexp]
 
@@ -14,9 +15,7 @@ let pp fmt pp_elt fs = function
   | Some x -> Format.fprintf fs fmt pp_elt x
   | None -> ()
 
-let map xo ~f = map f xo
 let map_or xo ~default ~f = map_or ~default f xo
-let bind xo ~f = bind xo f
 let iter xo ~f = iter f xo
 let exists xo ~f = exists f xo
 let for_all xo ~f = for_all f xo

sledge/nonstdlib/option.mli

@@ -6,14 +6,17 @@
  *)
 
 open! NS0
-include module type of Containers.Option
+
+include
+  module type of Containers.Option
+    with module Infix := Containers.Option.Infix
 
 type 'a t = 'a option [@@deriving compare, equal, hash, sexp]
 
+include Monad_intf.S with type 'a t := 'a t
+
 val pp : ('a_pp -> 'a -> unit, unit) fmt -> 'a_pp -> 'a option pp
-val map : 'a t -> f:('a -> 'b) -> 'b t
 val map_or : 'a t -> default:'b -> f:('a -> 'b) -> 'b
-val bind : 'a t -> f:('a -> 'b t) -> 'b t
 val iter : 'a t -> f:('a -> unit) -> unit
 val exists : 'a t -> f:('a -> bool) -> bool
 val for_all : 'a t -> f:('a -> bool) -> bool

sledge/src/exec.ml

@@ -630,7 +630,7 @@ let strlen_spec reg ptr =
  * Symbolic Execution
  *)
 
-open Option.Infix
+open Option.Import
 
 let check_preserve_us (q0 : Sh.t) (q1 : Sh.t) =
   let gain_us = Var.Set.diff q1.us q0.us in

sledge/src/ses/equality.ml

@@ -317,7 +317,7 @@ and solve_ ?f d e s =
 let solve ?f ~us ~xs d e =
   [%Trace.call fun {pf} -> pf "%a@ %a" Term.pp d Term.pp e]
   ;
-  (solve_ ?f d e (us, xs, Subst.empty) >|= fun (_, xs, s) -> (xs, s))
+  (solve_ ?f d e (us, xs, Subst.empty) |>= fun (_, xs, s) -> (xs, s))
   |>
   [%Trace.retn fun {pf} ->
     function