[sledge] Change Context API to use Term instead of Trm

Reviewed By: jvillard

Differential Revision: D24549079

fbshipit-source-id: 03d910a8b

sledge/src/domain_sh.ml

@@ -79,7 +79,7 @@ let term_eq_class_has_only_vars_in fvs ctx term =
       Context.pp ctx Term.pp term]
   ;
   let term_has_only_vars_in fvs term =
-    Var.Set.subset (Trm.fv term) ~of_:fvs
+    Var.Set.subset (Term.fv term) ~of_:fvs
   in
   let term_eq_class = Context.class_of ctx term in
   List.exists ~f:(term_has_only_vars_in fvs) term_eq_class
@@ -98,7 +98,7 @@ let garbage_collect (q : t) ~wrt =
         List.fold q.heap current ~f:(fun seg current ->
             if term_eq_class_has_only_vars_in current q.ctx seg.loc then
               List.fold (Context.class_of q.ctx seg.seq) current
-                ~f:(fun e c -> Var.Set.union c (Trm.fv e))
+                ~f:(fun e c -> Var.Set.union c (Term.fv e))
             else current )
       in
       all_reachable_vars current new_set q

sledge/src/fol/context.ml

@@ -601,7 +601,8 @@ let normalize r e = Term.map_trms ~f:(canon r) e
 
 let class_of r e =
   match Term.get_trm (normalize r e) with
-  | Some e' -> e' :: Trm.Map.find_multi e' (classes r)
+  | Some e' ->
+      List.map ~f:Term.of_trm (e' :: Trm.Map.find_multi e' (classes r))
   | None -> []
 
 let diff_classes r s =

sledge/src/fol/context.mli

@@ -67,7 +67,7 @@ val normalize : t -> Term.t -> Term.t
     assumptions, where [e'] and its subterms are expressed in terms of the
     canonical representatives of each equivalence class. *)
 
-val class_of : t -> Term.t -> Trm.t list
+val class_of : t -> Term.t -> Term.t list
 (** Equivalence class of [e]: all the terms [f] in the context such that
     [e = f] is implied by the assumptions. *)
 

sledge/src/fol/exp.ml

@@ -247,6 +247,10 @@ module Term = struct
 
   let ite ~cnd ~thn ~els = ite cnd thn els
 
+  (* Trm.t is embedded into Term.t *)
+  let of_trm t = `Trm t
+  let get_trm = function `Trm t -> Some t | _ -> None
+
   (** Destruct *)
 
   let d_int e = match (e : t) with `Trm (Z z) -> Some z | _ -> None
@@ -257,8 +261,6 @@ module Term = struct
     | `Trm (Q q) -> Some q
     | _ -> None
 
-  let get_trm = function `Trm t -> Some t | _ -> None
-
   (** Access *)
 
   let split_const e =

sledge/src/fol/exp.mli

@@ -51,6 +51,10 @@ module rec Term : sig
   (* if-then-else *)
   val ite : cnd:Formula.t -> thn:t -> els:t -> t
 
+  (* Trm.t is embedded into Term.t *)
+  val of_trm : Trm.t -> t
+  val get_trm : t -> Trm.t option
+
   (** Destruct *)
 
   val d_int : t -> Z.t option
@@ -58,8 +62,6 @@ module rec Term : sig
   val get_const : t -> Q.t option
   (** [get_const a] is [Some q] iff [equal a (const q)] *)
 
-  val get_trm : t -> Trm.t option
-
   (** Access *)
 
   val split_const : t -> t * Q.t

sledge/src/fol/fol.ml

@@ -13,7 +13,3 @@ module Var = Var
 module Term = Exp.Term
 module Formula = Exp.Formula
 module Context = Context
-
-(**/**)
-
-module Trm = Trm

sledge/src/fol/fol.mli

@@ -13,7 +13,3 @@ module Var = Var
 module Term = Exp.Term
 module Formula = Exp.Formula
 module Context = Context
-
-(**/**)
-
-module Trm = Trm