[sledge] Refactor: Factor out destructor for Integer Terms as Term.d_int

Summary:
It is suboptimal for `Sh` to destruct terms with detailed knowledge of
their representation. So add `Term.d_int` to destruct an integer term.

Reviewed By: jvillard

Differential Revision: D21721024

fbshipit-source-id: 5f13794b6

sledge/src/sh.ml

@@ -150,12 +150,12 @@ let pp_block x fs segs =
     | {loc; bas; len; _} :: _ -> (
         Term.equal loc bas
         &&
-        match len with
+        match Term.d_int len with
-        | Integer {data} -> (
+        | Some data -> (
           match
             List.fold segs ~init:(Some Z.zero) ~f:(fun len seg ->
-                match (len, seg.siz) with
+                match (len, Term.d_int seg.siz) with
-                | Some len, Integer {data} -> Some (Z.add len data)
+                | Some len, Some data -> Some (Z.add len data)
                 | _ -> None )
           with
           | Some blk_len -> Z.equal data blk_len
@@ -286,8 +286,9 @@ let fv ?ignore_cong q =
   in
   fv_union Var.Set.empty q
 
-let invariant_pure = function
+let invariant_pure b =
-  | Term.Integer {data} -> assert (not (Z.is_false data))
+  match Term.d_int b with
+  | Some data -> assert (not (Z.is_false data))
   | _ -> assert true
 
 let invariant_seg _ = ()

sledge/src/term.ml

@@ -1140,6 +1140,10 @@ module Var = struct
   end
 end
 
+(** Destruct *)
+
+let d_int = function Integer {data} -> Some data | _ -> None
+
 (** Transform *)
 
 let map e ~f =

sledge/src/term.mli

@@ -237,6 +237,10 @@ val rec_record : int -> t
 (* convert *)
 val of_exp : Llair.Exp.t -> t
 
+(** Destruct *)
+
+val d_int : t -> Z.t option
+
 (** Transform *)
 
 val map : t -> f:(t -> t) -> t