From 62dc914de7ada9f271b97594bcfe51b00afb4fd8 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Mon, 13 Jan 2020 07:12:16 -0800
Subject: [PATCH] [sledge] Use a defined variant type for Term.classify

Reviewed By: ngorogiannis

Differential Revision: D19282646

fbshipit-source-id: bb8de6ec4
---
 sledge/src/llair/term.ml        | 11 +++++++----
 sledge/src/llair/term.mli       |  5 ++++-
 sledge/src/symbheap/equality.ml | 26 +++++++++++++-------------
 3 files changed, 24 insertions(+), 18 deletions(-)

diff --git a/sledge/src/llair/term.ml b/sledge/src/llair/term.ml
index 7bac1c42e..e21dda086 100644
--- a/sledge/src/llair/term.ml
+++ b/sledge/src/llair/term.ml
@@ -1032,11 +1032,14 @@ let rec is_constant e =
       Qset.for_all ~f:(fun arg _ -> is_constant arg) args
   | Label _ | Float _ | Integer _ -> true
 
+type kind = Interpreted | Simplified | Atomic | Uninterpreted
+[@@deriving compare]
+
 let classify = function
-  | Add _ | Mul _ -> `Interpreted
-  | Ap2 ((Eq | Dq), _, _) -> `Simplified
-  | Ap1 _ | Ap2 _ | Ap3 _ | ApN _ -> `Uninterpreted
-  | RecN _ | Var _ | Integer _ | Float _ | Nondet _ | Label _ -> `Atomic
+  | Add _ | Mul _ -> Interpreted
+  | Ap2 ((Eq | Dq), _, _) -> Simplified
+  | Ap1 _ | Ap2 _ | Ap3 _ | ApN _ -> Uninterpreted
+  | RecN _ | Var _ | Integer _ | Float _ | Nondet _ | Label _ -> Atomic
 
 let solve e f =
   [%Trace.call fun {pf} -> pf "%a@ %a" pp e pp f]
diff --git a/sledge/src/llair/term.mli b/sledge/src/llair/term.mli
index bdc28fcf6..d4125c52b 100644
--- a/sledge/src/llair/term.mli
+++ b/sledge/src/llair/term.mli
@@ -245,5 +245,8 @@ val fv : t -> Var.Set.t
 val is_true : t -> bool
 val is_false : t -> bool
 val is_constant : t -> bool
-val classify : t -> [> `Atomic | `Interpreted | `Simplified | `Uninterpreted]
+
+type kind = Interpreted | Simplified | Atomic | Uninterpreted
+
+val classify : t -> kind
 val solve : t -> t -> t Map.t option
diff --git a/sledge/src/symbheap/equality.ml b/sledge/src/symbheap/equality.ml
index 18acd75b9..57a39388b 100644
--- a/sledge/src/symbheap/equality.ml
+++ b/sledge/src/symbheap/equality.ml
@@ -32,8 +32,8 @@ let classes r =
   in
   Map.fold r.rep ~init:empty_map ~f:(fun ~key ~data cls ->
       match Term.classify key with
-      | `Interpreted | `Atomic -> add key data cls
-      | `Simplified | `Uninterpreted ->
+      | Interpreted | Atomic -> add key data cls
+      | Simplified | Uninterpreted ->
           add (Term.map ~f:(apply r.rep) key) data cls )
 
 (** Pretty-printing *)
@@ -86,7 +86,7 @@ let in_car r e = Map.mem r.rep e
 
 let rec iter_max_solvables e ~f =
   match Term.classify e with
-  | `Interpreted -> Term.iter ~f:(iter_max_solvables ~f) e
+  | Interpreted -> Term.iter ~f:(iter_max_solvables ~f) e
   | _ -> f e
 
 let invariant r =
@@ -94,7 +94,7 @@ let invariant r =
   @@ fun () ->
   Map.iteri r.rep ~f:(fun ~key:a ~data:_ ->
       (* no interpreted terms in carrier *)
-      assert (Poly.(Term.classify a <> `Interpreted)) ;
+      assert (Poly.(Term.classify a <> Interpreted)) ;
       (* carrier is closed under subterms *)
       iter_max_solvables a ~f:(fun b ->
           assert (
@@ -109,9 +109,9 @@ let true_ = {sat= true; rep= empty_map} |> check invariant
 (** apply a subst to maximal non-interpreted subterms *)
 let rec norm s a =
   match Term.classify a with
-  | `Interpreted -> Term.map ~f:(norm s) a
-  | `Simplified -> apply s (Term.map ~f:(norm s) a)
-  | `Atomic | `Uninterpreted -> apply s a
+  | Interpreted -> Term.map ~f:(norm s) a
+  | Simplified -> apply s (Term.map ~f:(norm s) a)
+  | Atomic | Uninterpreted -> apply s a
 
 (** terms are congruent if equal after normalizing subterms *)
 let congruent r a b =
@@ -131,20 +131,20 @@ let lookup r a =
     terms, congruence composed with rep *)
 let rec canon r a =
   match Term.classify a with
-  | `Interpreted -> Term.map ~f:(canon r) a
-  | `Simplified | `Uninterpreted -> lookup r (Term.map ~f:(canon r) a)
-  | `Atomic -> apply r.rep a
+  | Interpreted -> Term.map ~f:(canon r) a
+  | Simplified | Uninterpreted -> lookup r (Term.map ~f:(canon r) a)
+  | Atomic -> apply r.rep a
 
 (** add a term to the carrier *)
 let rec extend a r =
   match Term.classify a with
-  | `Interpreted | `Simplified -> Term.fold ~f:extend a ~init:r
-  | `Uninterpreted ->
+  | Interpreted | Simplified -> Term.fold ~f:extend a ~init:r
+  | Uninterpreted ->
       Map.find_or_add r.rep a
         ~if_found:(fun _ -> r)
         ~default:a
         ~if_added:(fun rep -> Term.fold ~f:extend a ~init:{r with rep})
-  | `Atomic -> r
+  | Atomic -> r
 
 let extend a r = extend a r |> check invariant