[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

@@ -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
 

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]
 

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 :

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

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 :