From a0a5cf159a876c4b950426822cf12cf358b6da7f Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Tue, 20 Oct 2020 02:36:17 -0700
Subject: [PATCH] [sledge] Separate Funsym module

Summary: Funsym does not need to be defined as a submodule of Fol.

Reviewed By: jvillard

Differential Revision: D24306092

fbshipit-source-id: 7875f45f0
---
 sledge/src/fol.ml         | 53 +++------------------------------------
 sledge/src/fol.mli        |  2 +-
 sledge/src/ses/funsym.ml  | 49 ++++++++++++++++++++++++++++++++++++
 sledge/src/ses/funsym.mli | 30 ++++++++++++++++++++++
 sledge/src/ses/term.ml    | 12 ---------
 sledge/src/ses/term.mli   |  7 ------
 6 files changed, 84 insertions(+), 69 deletions(-)
 create mode 100644 sledge/src/ses/funsym.ml
 create mode 100644 sledge/src/ses/funsym.mli

diff --git a/sledge/src/fol.ml b/sledge/src/fol.ml
index b48e7c630..9330c02c2 100644
--- a/sledge/src/fol.ml
+++ b/sledge/src/fol.ml
@@ -9,52 +9,7 @@ let pp_boxed fs fmt =
   Format.pp_open_box fs 2 ;
   Format.kfprintf (fun fs -> Format.pp_close_box fs ()) fs fmt
 
-(*
- * (Uninterpreted) Function Symbols
- *)
-
-module Funsym = struct
-  type t =
-    | Float of string
-    | Label of {parent: string; name: string}
-    | Mul
-    | Div
-    | Rem
-    | EmptyRecord
-    | RecRecord of int
-    | BitAnd
-    | BitOr
-    | BitXor
-    | BitShl
-    | BitLshr
-    | BitAshr
-    | Signed of int
-    | Unsigned of int
-    | Convert of {src: Llair.Typ.t; dst: Llair.Typ.t}
-    | External of Ses.Term.Funsym.t
-  [@@deriving compare, equal, sexp]
-
-  let pp fs f =
-    let pf fmt = pp_boxed fs fmt in
-    match f with
-    | Float s -> pf "%s" s
-    | Label {name} -> pf "%s" name
-    | Mul -> pf "@<1>×"
-    | Div -> pf "/"
-    | Rem -> pf "%%"
-    | EmptyRecord -> pf "{}"
-    | RecRecord i -> pf "(rec_record %i)" i
-    | BitAnd -> pf "&&"
-    | BitOr -> pf "||"
-    | BitXor -> pf "xor"
-    | BitShl -> pf "shl"
-    | BitLshr -> pf "lshr"
-    | BitAshr -> pf "ashr"
-    | Signed n -> pf "(s%i)" n
-    | Unsigned n -> pf "(u%i)" n
-    | Convert {src; dst} -> pf "(%a)(%a)" Llair.Typ.pp dst Llair.Typ.pp src
-    | External sym -> pf "%a" Ses.Term.Funsym.pp sym
-end
+module Funsym = Ses.Funsym
 
 (*
  * Terms
@@ -947,9 +902,7 @@ module Term = struct
   (* uninterpreted *)
 
   let apply sym args =
-    apNt
-      (fun es -> _Apply (Funsym.External sym) (_Tuple (Array.of_list es)))
-      args
+    apNt (fun es -> _Apply sym (_Tuple (Array.of_list es))) args
 
   (** Destruct *)
 
@@ -1188,6 +1141,8 @@ let rec t_to_ses : trm -> Ses.Term.t = function
   | Apply (Unsigned n, Tuple [|x|]) -> Ses.Term.unsigned n (t_to_ses x)
   | Apply (Convert {src; dst}, Tuple [|x|]) ->
       Ses.Term.convert src ~to_:dst (t_to_ses x)
+  | Apply (sym, Tuple xs) ->
+      Ses.Term.apply sym (IArray.of_array (Array.map ~f:t_to_ses xs))
   | (Apply _ | Tuple _ | Project _) as t ->
       fail "cannot translate to Ses: %a" pp_t t ()
 
diff --git a/sledge/src/fol.mli b/sledge/src/fol.mli
index 2fe808498..43706019f 100644
--- a/sledge/src/fol.mli
+++ b/sledge/src/fol.mli
@@ -69,7 +69,7 @@ module rec Term : sig
   val project : ary:int -> idx:int -> t -> t
 
   (* uninterpreted *)
-  val apply : Ses.Term.Funsym.t -> t array -> t
+  val apply : Ses.Funsym.t -> t array -> t
 
   (* if-then-else *)
   val ite : cnd:Formula.t -> thn:t -> els:t -> t
diff --git a/sledge/src/ses/funsym.ml b/sledge/src/ses/funsym.ml
new file mode 100644
index 000000000..c46f25c5d
--- /dev/null
+++ b/sledge/src/ses/funsym.ml
@@ -0,0 +1,49 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+(** Function Symbols *)
+
+type t =
+  | Float of string
+  | Label of {parent: string; name: string}
+  | Mul
+  | Div
+  | Rem
+  | EmptyRecord
+  | RecRecord of int
+  | BitAnd
+  | BitOr
+  | BitXor
+  | BitShl
+  | BitLshr
+  | BitAshr
+  | Signed of int
+  | Unsigned of int
+  | Convert of {src: Llair.Typ.t; dst: Llair.Typ.t}
+  | Uninterp of string
+[@@deriving compare, equal, sexp]
+
+let pp ppf f =
+  let pf fmt = Format.fprintf ppf fmt in
+  match f with
+  | Float s -> pf "%s" s
+  | Label {name} -> pf "%s" name
+  | Mul -> pf "@<1>×"
+  | Div -> pf "/"
+  | Rem -> pf "%%"
+  | EmptyRecord -> pf "{}"
+  | RecRecord i -> pf "(rec_record %i)" i
+  | BitAnd -> pf "&&"
+  | BitOr -> pf "||"
+  | BitXor -> pf "xor"
+  | BitShl -> pf "shl"
+  | BitLshr -> pf "lshr"
+  | BitAshr -> pf "ashr"
+  | Signed n -> pf "(s%i)" n
+  | Unsigned n -> pf "(u%i)" n
+  | Convert {src; dst} -> pf "(%a)(%a)" Llair.Typ.pp dst Llair.Typ.pp src
+  | Uninterp sym -> pf "%s" sym
diff --git a/sledge/src/ses/funsym.mli b/sledge/src/ses/funsym.mli
new file mode 100644
index 000000000..1770f6f36
--- /dev/null
+++ b/sledge/src/ses/funsym.mli
@@ -0,0 +1,30 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+(** Function Symbols *)
+
+type t =
+  | Float of string
+  | Label of {parent: string; name: string}
+  | Mul
+  | Div
+  | Rem
+  | EmptyRecord
+  | RecRecord of int
+  | BitAnd
+  | BitOr
+  | BitXor
+  | BitShl
+  | BitLshr
+  | BitAshr
+  | Signed of int
+  | Unsigned of int
+  | Convert of {src: Llair.Typ.t; dst: Llair.Typ.t}
+  | Uninterp of string
+[@@deriving compare, equal, sexp]
+
+val pp : t pp
diff --git a/sledge/src/ses/term.ml b/sledge/src/ses/term.ml
index 3940be0a4..905a98539 100644
--- a/sledge/src/ses/term.ml
+++ b/sledge/src/ses/term.ml
@@ -9,18 +9,6 @@
 
 [@@@warning "+9"]
 
-module Funsym : sig
-  type t [@@deriving compare, equal, sexp]
-
-  val make : string -> t
-  val pp : t pp
-end = struct
-  type t = string [@@deriving compare, equal, sexp]
-
-  let make s = s
-  let pp = Format.pp_print_string
-end
-
 type op1 =
   | Signed of {bits: int}
   | Unsigned of {bits: int}
diff --git a/sledge/src/ses/term.mli b/sledge/src/ses/term.mli
index b200fb978..a7de812a7 100644
--- a/sledge/src/ses/term.mli
+++ b/sledge/src/ses/term.mli
@@ -10,13 +10,6 @@
     Pure (heap-independent) terms are arithmetic, bitwise-logical, etc.
     operations over literal values and variables. *)
 
-module Funsym : sig
-  type t [@@deriving compare, equal, sexp]
-
-  val make : string -> t
-  val pp : t pp
-end
-
 type op1 =
   | Signed of {bits: int}
       (** [Ap1 (Signed {bits= n}, arg)] is [arg] interpreted as an [n]-bit