From 7ed8a6a26055c3a4f4e2b0876a8aa199536de5f3 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Thu, 28 Nov 2019 12:41:29 -0800
Subject: [PATCH] [sledge] Simplify and improve using local subst in sigs

Summary:
OCaml 4.08 supports a form of signature-local bindings, to that a type
can be defined in order to be used in other definitions, without
being part of the signature itself.

Reviewed By: ngorogiannis, jvillard

Differential Revision: D18736380

fbshipit-source-id: 0bb043de6
---
 sledge/src/llair/exp.ml      | 5 -----
 sledge/src/llair/exp.mli     | 8 +++++---
 sledge/src/llair/term.ml     | 4 ----
 sledge/src/llair/term.mli    | 7 ++++---
 sledge/src/symbheap/exec.mli | 6 +++---
 5 files changed, 12 insertions(+), 18 deletions(-)

diff --git a/sledge/src/llair/exp.ml b/sledge/src/llair/exp.ml
index ea9e53a47..40df044f0 100644
--- a/sledge/src/llair/exp.ml
+++ b/sledge/src/llair/exp.ml
@@ -308,9 +308,6 @@ and typ_of exp =
   [@@warning "-9"]
 
 let typ = typ_of
-
-type exp = t
-
 let pp_exp = pp
 
 (** Registers are the expressions constructed by [Reg] *)
@@ -319,8 +316,6 @@ module Reg = struct
 
   let pp = pp
 
-  type reg = t
-
   let var r =
     match Var.of_term r.term with Some v -> v | _ -> violates invariant r
 
diff --git a/sledge/src/llair/exp.mli b/sledge/src/llair/exp.mli
index 04fc6ae67..8048fbddd 100644
--- a/sledge/src/llair/exp.mli
+++ b/sledge/src/llair/exp.mli
@@ -96,16 +96,16 @@ val pp : t pp
 
 include Invariant.S with type t := t
 
-type exp = t
-
 (** Exp.Reg is re-exported as Reg *)
 module Reg : sig
+  type exp := t
   type t = private exp [@@deriving compare, equal, hash, sexp]
-  type reg = t
 
   include Comparator.S with type t := t
 
   module Set : sig
+    type reg := t
+
     type t = (reg, comparator_witness) Set.t
     [@@deriving compare, equal, sexp]
 
@@ -117,6 +117,8 @@ module Reg : sig
   end
 
   module Map : sig
+    type reg := t
+
     type 'a t = (reg, 'a, comparator_witness) Map.t
     [@@deriving compare, equal, sexp]
 
diff --git a/sledge/src/llair/term.ml b/sledge/src/llair/term.ml
index fe85359e0..f88f5f9ef 100644
--- a/sledge/src/llair/term.ml
+++ b/sledge/src/llair/term.ml
@@ -216,8 +216,6 @@ and pp_record fs elts =
             Format.fprintf fs "@[<h>%a@]" (Vector.pp ",@ " pp) elts )
       elts]
 
-type term = t
-
 let pp_t = pp ?is_x:None
 let pp_full = pp
 let pp = pp_t
@@ -296,8 +294,6 @@ module Var = struct
 
   let pp = pp
 
-  type var = t
-
   module Set = struct
     include (
       Set :
diff --git a/sledge/src/llair/term.mli b/sledge/src/llair/term.mli
index f5a6b6baa..cbb678e65 100644
--- a/sledge/src/llair/term.mli
+++ b/sledge/src/llair/term.mli
@@ -87,16 +87,16 @@ val pp_full : ?is_x:(t -> bool) -> t pp
 val pp : t pp
 val invariant : t -> unit
 
-type term = t
-
 (** Term.Var is re-exported as Var *)
 module Var : sig
+  type term := t
   type t = private term [@@deriving compare, equal, hash, sexp]
-  type var = t
 
   include Comparator.S with type t := t
 
   module Set : sig
+    type var := t
+
     type t = (var, comparator_witness) Set.t
     [@@deriving compare, equal, sexp]
 
@@ -120,6 +120,7 @@ module Var : sig
   val global : t -> bool
 
   module Subst : sig
+    type var := t
     type t [@@deriving compare, equal, sexp]
 
     val pp : t pp
diff --git a/sledge/src/symbheap/exec.mli b/sledge/src/symbheap/exec.mli
index 7a5d9a557..28a05b0e3 100644
--- a/sledge/src/symbheap/exec.mli
+++ b/sledge/src/symbheap/exec.mli
@@ -10,14 +10,14 @@
 val assume : Sh.t -> Term.t -> Sh.t option
 val kill : Sh.t -> Var.t -> Sh.t
 val move : Sh.t -> (Var.t * Term.t) vector -> Sh.t
-val load : Sh.t -> reg:Var.var -> ptr:Term.t -> len:Term.t -> Sh.t option
+val load : Sh.t -> reg:Var.t -> ptr:Term.t -> len:Term.t -> Sh.t option
 val store : Sh.t -> ptr:Term.t -> exp:Term.t -> len:Term.t -> Sh.t option
 val memset : Sh.t -> dst:Term.t -> byt:Term.t -> len:Term.t -> Sh.t option
 val memcpy : Sh.t -> dst:Term.t -> src:Term.t -> len:Term.t -> Sh.t option
 val memmov : Sh.t -> dst:Term.t -> src:Term.t -> len:Term.t -> Sh.t option
-val alloc : Sh.t -> reg:Var.var -> num:Term.t -> len:Term.t -> Sh.t option
+val alloc : Sh.t -> reg:Var.t -> num:Term.t -> len:Term.t -> Sh.t option
 val free : Sh.t -> ptr:Term.t -> Sh.t option
-val nondet : Sh.t -> Var.var option -> Sh.t
+val nondet : Sh.t -> Var.t option -> Sh.t
 val abort : Sh.t -> Sh.t option
 
 val intrinsic :