From fe62eeadabc159bb197658917938bd7829e98801 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Mon, 23 Mar 2020 06:18:48 -0700
Subject: [PATCH] [sledge] Cleanup of Import

Summary:
Work on the containers revealed that 1b8746d21 was premature, and this
diff is in part a revert of that. The objectives for the global
namespace are:

- self-consistent as much as possible
- rich data type operations
- does not require maintaining lots of tedious library wrapping code
- has Marshalable containers
- has containers with functorial interfaces

For these aims, it's best to stick with Core. Base isn't enough to
define functorial interfaces for collections (without a lot of tedious
wrapping code to keep in sync manually), and since a few modules not
in Core_kernel are needed anyhow.

Reviewed By: ngorogiannis

Differential Revision: D20583756

fbshipit-source-id: d939be7d0
---
 sledge/bin/config.ml              |   4 +-
 sledge/bin/domain_itv.ml          |   6 +-
 sledge/bin/frontend.ml            |   2 +-
 sledge/bin/sledge.ml              |   9 +--
 sledge/bin/sledge_buck.ml         |   1 -
 sledge/bin/sledge_buck.mli        |   2 -
 sledge/lib/domain_intf.ml         |   2 +-
 sledge/lib/domain_sh.ml           |   2 +-
 sledge/lib/domain_used_globals.ml |   2 +-
 sledge/lib/equality.ml            |  10 +--
 sledge/lib/exp.ml                 |  44 +++++-----
 sledge/lib/exp.mli                |   7 +-
 sledge/lib/import/IArray.ml       |  17 ++--
 sledge/lib/import/IArray.mli      |   6 +-
 sledge/lib/import/import.ml       | 130 +++++++++++-------------------
 sledge/lib/import/import.mli      | 108 ++++++++-----------------
 sledge/lib/import/import0.ml      |  63 ++++-----------
 sledge/lib/import/list.ml         |  38 +++++----
 sledge/lib/import/list.mli        |   7 +-
 sledge/lib/import/map.ml          |   5 +-
 sledge/lib/import/map_intf.ml     |   2 +-
 sledge/lib/import/option.ml       |   3 +-
 sledge/lib/import/option.mli      |   4 +-
 sledge/lib/import/set_intf.ml     |   2 +-
 sledge/lib/report.ml              |   2 +-
 sledge/lib/report.mli             |   4 +-
 sledge/lib/sh.ml                  |   2 +-
 sledge/lib/term.ml                |  58 ++++++-------
 sledge/lib/term.mli               |   7 +-
 29 files changed, 214 insertions(+), 335 deletions(-)

diff --git a/sledge/bin/config.ml b/sledge/bin/config.ml
index f85bd10d9..fea786118 100644
--- a/sledge/bin/config.ml
+++ b/sledge/bin/config.ml
@@ -11,11 +11,11 @@ let config_file_env_var = "SLEDGE_CONFIG"
 let exe_relative_config_file_path = "config"
 
 let config_file =
-  match Core.Sys.getenv config_file_env_var with
+  match Sys.getenv config_file_env_var with
   | Some file -> file
   | None ->
       Filename.concat
-        (Filename.dirname Caml.Sys.executable_name)
+        (Filename.dirname Sys.executable_name)
         exe_relative_config_file_path
 
 let contents =
diff --git a/sledge/bin/domain_itv.ml b/sledge/bin/domain_itv.ml
index 882a2ff85..1205a9e34 100644
--- a/sledge/bin/domain_itv.ml
+++ b/sledge/bin/domain_itv.ml
@@ -45,7 +45,7 @@ let pp fs =
   in
   bindings >> Array.pp "@," (pp_pair Var.print Interval.print) fs
 
-let report_fmt_thunk = Fun.flip pp
+let report_fmt_thunk = Fn.flip pp
 let init _gs = Abstract1.top (Lazy.force man) (Environment.make [||] [||])
 let apron_var_of_name = (fun nm -> "%" ^ nm) >> Apron.Var.of_string
 let apron_var_of_reg = Reg.name >> apron_var_of_name
@@ -134,8 +134,8 @@ and apron_texpr_of_llair_term tm q typ =
         | Div -> Some (mk_arith_binop typ Texpr0.Div)
         | Eq -> Some (mk_bool_binop typ q Tcons0.EQ)
         | Dq -> Some (mk_bool_binop typ q Tcons0.DISEQ)
-        | Lt -> Some (Fun.flip (mk_bool_binop typ q Tcons0.SUP))
-        | Le -> Some (Fun.flip (mk_bool_binop typ q Tcons0.SUPEQ))
+        | Lt -> Some (Fn.flip (mk_bool_binop typ q Tcons0.SUP))
+        | Le -> Some (Fn.flip (mk_bool_binop typ q Tcons0.SUPEQ))
         | _ -> None
       in
       let* te1 = apron_texpr_of_llair_term t1 q typ in
diff --git a/sledge/bin/frontend.ml b/sledge/bin/frontend.ml
index c3dd27efd..59d0be287 100644
--- a/sledge/bin/frontend.ml
+++ b/sledge/bin/frontend.ml
@@ -354,7 +354,7 @@ module Llvalue = struct
   let sexp_of_t llv = Sexp.Atom (Llvm.string_of_llvalue llv)
 end
 
-let struct_rec = Exp.struct_rec (module Llvalue)
+let struct_rec = Staged.unstage (Exp.struct_rec (module Llvalue))
 
 let ptr_fld x ~ptr ~fld ~lltyp =
   let offset =
diff --git a/sledge/bin/sledge.ml b/sledge/bin/sledge.ml
index c1f88a74a..2465e68d1 100644
--- a/sledge/bin/sledge.ml
+++ b/sledge/bin/sledge.ml
@@ -7,9 +7,8 @@
 
 (** SLEdge command line interface *)
 
-let () = Printexc.record_backtrace Version.debug
+let () = Backtrace.Exn.set_recording Version.debug
 
-module Command = Core.Command
 open Command.Let_syntax
 
 type 'a param = 'a Command.Param.t
@@ -47,7 +46,7 @@ let command ~summary ?readme param =
       Format.printf "@\nRESULT: Success: Invalid Accesses: %i@."
         (Report.invalid_access_count ())
     with exn ->
-      let bt = Caml.Printexc.get_raw_backtrace () in
+      let bt = Printexc.get_raw_backtrace () in
       Trace.flush () ;
       ( match exn with
       | Frontend.Invalid_llvm msg ->
@@ -57,8 +56,8 @@ let command ~summary ?readme param =
       | Failure msg -> Format.printf "@\nRESULT: Internal error: %s@." msg
       | _ ->
           Format.printf "@\nRESULT: Unknown error: %s@."
-            (Caml.Printexc.to_string exn) ) ;
-      Caml.Printexc.raise_with_backtrace exn bt
+            (Printexc.to_string exn) ) ;
+      Printexc.raise_with_backtrace exn bt
   in
   Command.basic ~summary ?readme (trace *> param >>| wrap)
 
diff --git a/sledge/bin/sledge_buck.ml b/sledge/bin/sledge_buck.ml
index 21a115164..26ed884e6 100644
--- a/sledge/bin/sledge_buck.ml
+++ b/sledge/bin/sledge_buck.ml
@@ -167,7 +167,6 @@ let llvm_link_opt ~fuzzer ~bitcode_output modules =
 
 (** command line interface *)
 
-module Command = Core.Command
 open Command.Let_syntax
 
 let ( |*> ) a' f' = a' |> Command.Param.apply f'
diff --git a/sledge/bin/sledge_buck.mli b/sledge/bin/sledge_buck.mli
index 29eea3b43..57de68f51 100644
--- a/sledge/bin/sledge_buck.mli
+++ b/sledge/bin/sledge_buck.mli
@@ -5,8 +5,6 @@
  * LICENSE file in the root directory of this source tree.
  *)
 
-module Command = Core.Command
-
 val main :
      command:unit Command.basic_command
   -> analyze:(string list -> unit -> unit) Command.Param.t
diff --git a/sledge/lib/domain_intf.ml b/sledge/lib/domain_intf.ml
index 4fb95c3be..c141175be 100644
--- a/sledge/lib/domain_intf.ml
+++ b/sledge/lib/domain_intf.ml
@@ -10,7 +10,7 @@ module type Dom = sig
   type t [@@deriving equal, sexp_of]
 
   val pp : t pp
-  val report_fmt_thunk : t -> Format.formatter -> unit
+  val report_fmt_thunk : t -> Formatter.t -> unit
   val init : Global.t iarray -> t
   val join : t -> t -> t option
   val is_false : t -> bool
diff --git a/sledge/lib/domain_sh.ml b/sledge/lib/domain_sh.ml
index 0434101a1..11fb9eed6 100644
--- a/sledge/lib/domain_sh.ml
+++ b/sledge/lib/domain_sh.ml
@@ -10,7 +10,7 @@
 type t = Sh.t [@@deriving equal, sexp]
 
 let pp fs q = Format.fprintf fs "@[{ %a@ }@]" Sh.pp q
-let report_fmt_thunk = Fun.flip pp
+let report_fmt_thunk = Fn.flip pp
 
 (* set by cli *)
 let simplify_states = ref true
diff --git a/sledge/lib/domain_used_globals.ml b/sledge/lib/domain_used_globals.ml
index e875c8d7a..54b99ed4f 100644
--- a/sledge/lib/domain_used_globals.ml
+++ b/sledge/lib/domain_used_globals.ml
@@ -10,7 +10,7 @@
 type t = Reg.Set.t [@@deriving equal, sexp]
 
 let pp = Reg.Set.pp
-let report_fmt_thunk = Fun.flip pp
+let report_fmt_thunk = Fn.flip pp
 let empty = Reg.Set.empty
 
 let init globals =
diff --git a/sledge/lib/equality.ml b/sledge/lib/equality.ml
index 9f322c2c1..6b9e6387b 100644
--- a/sledge/lib/equality.ml
+++ b/sledge/lib/equality.ml
@@ -103,7 +103,7 @@ end = struct
     let exception Found in
     match
       Term.Map.update s e ~f:(function
-        | Some _ -> raise_notrace Found
+        | Some _ -> Exn.raise_without_backtrace Found
         | None -> e )
     with
     | exception Found -> None
@@ -188,10 +188,10 @@ let orient e f =
       let o = compare (height e) (height f) in
       if o <> 0 then o else Term.compare e f
   in
-  match Int.sign (compare e f) with
-  | Neg -> Some (e, f)
-  | Zero -> None
-  | Pos -> Some (f, e)
+  match Ordering.of_int (compare e f) with
+  | Less -> Some (e, f)
+  | Equal -> None
+  | Greater -> Some (f, e)
 
 let norm (_, _, s) e = Subst.norm s e
 
diff --git a/sledge/lib/exp.ml b/sledge/lib/exp.ml
index f6777df92..df1364bdc 100644
--- a/sledge/lib/exp.ml
+++ b/sledge/lib/exp.ml
@@ -474,28 +474,28 @@ let update typ ~rcd idx ~elt =
 
 let struct_rec key =
   let memo_id = Hashtbl.create key in
-  let rec_app = (Term.rec_app key) Term.Record in
-  fun ~id typ elt_thks ->
-    match Hashtbl.find memo_id id with
-    | None ->
-        (* Add placeholder to prevent computing [elts] in calls to
-           [struct_rec] from [elt_thks] for recursive occurrences of [id]. *)
-        let elta = Array.create ~len:(IArray.length elt_thks) null in
-        let elts = IArray.of_array elta in
-        Hashtbl.set memo_id ~key:id ~data:elts ;
-        let term =
-          rec_app ~id (IArray.map ~f:(fun elt -> lazy elt.term) elts)
-        in
-        IArray.iteri elt_thks ~f:(fun i (lazy elt) -> elta.(i) <- elt) ;
-        {desc= ApN (Struct_rec, typ, elts); term} |> check invariant
-    | Some elts ->
-        (* Do not check invariant as invariant will be checked above after
-           the thunks are forced, before which invariant-checking may
-           spuriously fail. Note that it is important that the value
-           constructed here shares the array in the memo table, so that the
-           update after forcing the recursive thunks also updates this
-           value. *)
-        {desc= ApN (Struct_rec, typ, elts); term= rec_app ~id IArray.empty}
+  let rec_app = (Staged.unstage (Term.rec_app key)) Term.Record in
+  Staged.stage
+  @@ fun ~id typ elt_thks ->
+  match Hashtbl.find memo_id id with
+  | None ->
+      (* Add placeholder to prevent computing [elts] in calls to
+         [struct_rec] from [elt_thks] for recursive occurrences of [id]. *)
+      let elta = Array.create ~len:(IArray.length elt_thks) null in
+      let elts = IArray.of_array elta in
+      Hashtbl.set memo_id ~key:id ~data:elts ;
+      let term =
+        rec_app ~id (IArray.map ~f:(fun elt -> lazy elt.term) elts)
+      in
+      IArray.iteri elt_thks ~f:(fun i (lazy elt) -> elta.(i) <- elt) ;
+      {desc= ApN (Struct_rec, typ, elts); term} |> check invariant
+  | Some elts ->
+      (* Do not check invariant as invariant will be checked above after the
+         thunks are forced, before which invariant-checking may spuriously
+         fail. Note that it is important that the value constructed here
+         shares the array in the memo table, so that the update after
+         forcing the recursive thunks also updates this value. *)
+      {desc= ApN (Struct_rec, typ, elts); term= rec_app ~id IArray.empty}
 
 let size_of exp = integer Typ.siz (Z.of_int (Typ.size_of (typ exp)))
 
diff --git a/sledge/lib/exp.mli b/sledge/lib/exp.mli
index 1f4ca615e..4244ac02f 100644
--- a/sledge/lib/exp.mli
+++ b/sledge/lib/exp.mli
@@ -188,11 +188,8 @@ val select : Typ.t -> t -> int -> t
 val update : Typ.t -> rcd:t -> int -> elt:t -> t
 
 val struct_rec :
-     (module Hashtbl.Key.S with type t = 'id)
-  -> id:'id
-  -> Typ.t
-  -> t lazy_t iarray
-  -> t
+     (module Hashtbl.Key_plain with type t = 'id)
+  -> (id:'id -> Typ.t -> t lazy_t iarray -> t) Staged.t
 (** [struct_rec Id id element_thunks] constructs a possibly-cyclic [Struct]
     value. Cycles are detected using [Id]. The caller of [struct_rec Id]
     must ensure that a single unstaging of [struct_rec Id] is used for each
diff --git a/sledge/lib/import/IArray.ml b/sledge/lib/import/IArray.ml
index 4255686c9..9097a4977 100644
--- a/sledge/lib/import/IArray.ml
+++ b/sledge/lib/import/IArray.ml
@@ -8,24 +8,21 @@
 (** IArray - Immutable view of an array *)
 
 open Import0
-module Array = Base.Array
-module Hash = Base.Hash
-open Base.Continue_or_stop
 
 (** = 'a array but covariant since imperative operations hidden *)
 type +'a t
 
-let v (a : 'a array) : 'a t = Caml.Obj.magic a
-let a (v : 'a t) : 'a array = Caml.Obj.magic v
-let _vl (al : 'a array list) : 'a t list = Caml.Obj.magic al
-let al (vl : 'a t list) : 'a array list = Caml.Obj.magic vl
+let v (a : 'a array) : 'a t = Obj.magic a
+let a (v : 'a t) : 'a array = Obj.magic v
+let _vl (al : 'a array list) : 'a t list = Obj.magic al
+let al (vl : 'a t list) : 'a array list = Obj.magic vl
 let compare cmp x y = Array.compare cmp (a x) (a y)
 let equal cmp x y = Array.equal cmp (a x) (a y)
 let hash_fold_t f s x = Hash.Builtin.hash_fold_array_frozen f s (a x)
 let t_of_sexp a_of_sexp s = v (Array.t_of_sexp a_of_sexp s)
 let sexp_of_t sexp_of_a x = Array.sexp_of_t sexp_of_a (a x)
 
-module Infix = struct
+module Import = struct
   type +'a iarray = 'a t [@@deriving compare, equal, hash, sexp]
 end
 
@@ -108,7 +105,9 @@ let fold_map_until xs ~init ~f ~finish =
   with_return (fun {return} ->
       finish
         (fold_map xs ~init ~f:(fun s x ->
-             match f s x with Continue x -> x | Stop x -> return x )) )
+             match (f s x : _ Continue_or_stop.t) with
+             | Continue x -> x
+             | Stop x -> return x )) )
 
 let concat xs = v (Array.concat (al xs))
 let copy x = v (Array.copy (a x))
diff --git a/sledge/lib/import/IArray.mli b/sledge/lib/import/IArray.mli
index 65a747484..7b9782c31 100644
--- a/sledge/lib/import/IArray.mli
+++ b/sledge/lib/import/IArray.mli
@@ -15,7 +15,7 @@ open Import0
 
 type +'a t [@@deriving compare, equal, hash, sexp]
 
-module Infix : sig
+module Import : sig
   type +'a iarray = 'a t [@@deriving compare, equal, hash, sexp]
 end
 
@@ -44,7 +44,7 @@ val fold_result :
 val fold_until :
      'a t
   -> init:'accum
-  -> f:('accum -> 'a -> ('accum, 'final) Base.Continue_or_stop.t)
+  -> f:('accum -> 'a -> ('accum, 'final) Continue_or_stop.t)
   -> finish:('accum -> 'final)
   -> 'final
 
@@ -114,7 +114,7 @@ val map_preserving_phys_equal : 'a t -> f:('a -> 'a) -> 'a t
 val fold_map_until :
      'a t
   -> init:'accum
-  -> f:('accum -> 'a -> ('accum * 'b, 'final) Base.Continue_or_stop.t)
+  -> f:('accum -> 'a -> ('accum * 'b, 'final) Continue_or_stop.t)
   -> finish:('accum * 'b t -> 'final)
   -> 'final
 
diff --git a/sledge/lib/import/import.ml b/sledge/lib/import/import.ml
index 617ff4bcf..517a1bd18 100644
--- a/sledge/lib/import/import.ml
+++ b/sledge/lib/import/import.ml
@@ -7,7 +7,6 @@
 
 (** Global namespace opened in each source file by the build system *)
 
-include Stdio
 include Import0
 
 (** Failures *)
@@ -46,57 +45,78 @@ let violates f x =
   assert (f x ; true) ;
   assert false
 
-type 'a or_error = ('a, exn * Caml.Printexc.raw_backtrace) result
-
-let or_error f x () =
-  try Ok (f x) with exn -> Error (exn, Caml.Printexc.get_raw_backtrace ())
-
 (** Extensions *)
 
 module Invariant = struct
-  include Base.Invariant
+  include Core.Invariant
 
   let invariant here t sexp_of_t f =
     assert (
       ( try f ()
         with exn ->
-          let bt = Caml.Printexc.get_raw_backtrace () in
+          let bt = Printexc.get_raw_backtrace () in
           let exn =
-            Base.Error.to_exn
-              (Base.Error.create_s
-                 (Base.Sexp.message "invariant failed"
-                    [ ("", Sexplib.Conv.sexp_of_exn exn)
-                    ; ("", Base.Source_code_position.sexp_of_t here)
-                    ; ("", sexp_of_t t) ]))
+            Error.to_exn
+              (Error.create_s
+                 (Sexp.List
+                    [ Atom "invariant failed"; sexp_of_exn exn
+                    ; Source_code_position.sexp_of_t here; sexp_of_t t ]))
           in
-          Caml.Printexc.raise_with_backtrace exn bt ) ;
+          Printexc.raise_with_backtrace exn bt ) ;
       true )
 end
 
-module Unit = Base.Unit
+(** Containers *)
 
-type unit = Unit.t [@@deriving compare, equal, hash, sexp]
+module Option = Option
+include Option.Monad_infix
+include Option.Monad_syntax
+module List = List
 
-module Bool = Base.Bool
+module Array = struct
+  include Core.Array
 
-type bool = Bool.t [@@deriving compare, equal, hash, sexp]
+  let pp sep pp_elt fs a = List.pp sep pp_elt fs (to_list a)
+end
 
-module Char = Base.Char
+module IArray = IArray
+include IArray.Import
+module Set = Set
+module Map = Map
+module Qset = Qset
 
-type char = Char.t [@@deriving compare, equal, hash, sexp]
+(** Data types *)
 
-module Int = Base.Int
+module String = struct
+  include (
+    Core.String :
+      sig
+        include
+          module type of Core.String with module Map := Core.String.Map
+      end )
+
+  module Map = Map.Make (Core.String)
+end
 
-type int = Int.t [@@deriving compare, equal, hash, sexp]
+module Q = struct
+  let pp = Q.pp_print
+  let hash = Hashtbl.hash
+  let hash_fold_t s q = Int.hash_fold_t s (hash q)
+  let sexp_of_t q = Sexp.Atom (Q.to_string q)
+
+  let t_of_sexp = function
+    | Sexp.Atom s -> Q.of_string s
+    | _ -> assert false
 
-module Int64 = Base.Int64
+  let of_z = Q.of_bigint
 
-type int64 = Int64.t [@@deriving compare, equal, hash, sexp]
+  include Q
+end
 
 module Z = struct
   let pp = Z.pp_print
   let hash = [%hash: Z.t]
-  let hash_fold_t s z = Hash.fold_int s (hash z)
+  let hash_fold_t s z = Int.hash_fold_t s (hash z)
   let sexp_of_t z = Sexp.Atom (Z.to_string z)
 
   let t_of_sexp = function
@@ -112,61 +132,3 @@ module Z = struct
 
   include Z
 end
-
-module Q = struct
-  let pp = Q.pp_print
-  let hash = Hashtbl.hash
-  let hash_fold_t s q = Hash.fold_int s (hash q)
-  let sexp_of_t q = Sexp.Atom (Q.to_string q)
-
-  let t_of_sexp = function
-    | Sexp.Atom s -> Q.of_string s
-    | _ -> assert false
-
-  let of_z = Q.of_bigint
-
-  include Q
-end
-
-module String = struct
-  module T = struct
-    include Base.String
-
-    let hash_fold_t = Hash.fold_string
-    let hash = Hash.of_fold hash_fold_t
-    let t_of_sexp = Sexplib.Conv.string_of_sexp
-    let sexp_of_t = Sexplib.Conv.sexp_of_string
-  end
-
-  include T
-  module Map = Map.Make (T)
-end
-
-type string = String.t [@@deriving compare, equal, hash, sexp]
-
-module Option = Option
-
-type 'a option = 'a Option.t [@@deriving compare, equal, hash, sexp]
-
-include Option.Monad_infix
-include Option.Monad_syntax
-module Result = Base.Result
-
-module Array = struct
-  include Base.Array
-
-  let pp sep pp_elt fs a = List.pp sep pp_elt fs (to_list a)
-end
-
-module IArray = IArray
-include IArray.Infix
-module List = List
-
-type 'a list = 'a List.t [@@deriving compare, equal, hash, sexp]
-
-module Hash_queue = Core_kernel.Hash_queue
-module Set = Set
-module Hash_set = Base.Hash_set
-module Map = Map
-module Qset = Qset
-module Hashtbl = Base.Hashtbl
diff --git a/sledge/lib/import/import.mli b/sledge/lib/import/import.mli
index b9df250bd..547c444af 100644
--- a/sledge/lib/import/import.mli
+++ b/sledge/lib/import/import.mli
@@ -7,20 +7,8 @@
 
 (** Global namespace opened in each source file by the build system *)
 
-include module type of Stdio
 include module type of Import0
 
-(** Tuple operations *)
-
-val fst3 : 'a * _ * _ -> 'a
-(** First projection from a triple. *)
-
-val snd3 : _ * 'a * _ -> 'a
-(** Second projection from a triple. *)
-
-val trd3 : _ * _ * 'a -> 'a
-(** Third projection from a triple. *)
-
 (** Function combinators *)
 
 val ( >> ) : ('a -> 'b) -> ('b -> 'c) -> 'a -> 'c
@@ -73,95 +61,63 @@ val check : ('a -> unit) -> 'a -> 'a
 val violates : ('a -> unit) -> 'a -> _
 (** Assert that function raises on argument. *)
 
-type 'a or_error = ('a, exn * Caml.Printexc.raw_backtrace) result
-
-val or_error : ('a -> 'b) -> 'a -> unit -> 'b or_error
-(** [or_error f x] runs [f x] and converts unhandled exceptions to errors. *)
-
 (** Extensions *)
 
-module Invariant : module type of Base.Invariant
-module Unit = Base.Unit
-
-type unit = Unit.t [@@deriving compare, equal, hash, sexp]
+module Invariant : module type of Core.Invariant
 
-module Bool = Base.Bool
+(** Containers *)
 
-type bool = Bool.t [@@deriving compare, equal, hash, sexp]
+module Option = Option
+include module type of Option.Monad_infix
+include module type of Option.Monad_syntax
+module List = List
 
-module Char = Base.Char
+module Array : sig
+  include module type of Array
 
-type char = Char.t [@@deriving compare, equal, hash, sexp]
+  val pp : (unit, unit) fmt -> 'a pp -> 'a array pp
+end
 
-module Int = Base.Int
+module IArray = IArray
+include module type of IArray.Import
+module Set = Set
+module Map = Map
+module Qset = Qset
 
-type int = Int.t [@@deriving compare, equal, hash, sexp]
+(** Data types *)
 
-module Int64 = Base.Int64
+module String : sig
+  include sig
+    include module type of Core.String with module Map := Core.String.Map
+  end
 
-type int64 = Int64.t [@@deriving compare, equal, hash, sexp]
+  module Map : Map.S with type key = string
+end
 
-module Z : sig
-  include module type of struct include Z end
+module Q : sig
+  include module type of struct include Q end
 
+  val of_z : Z.t -> t
   val compare : t -> t -> int
   val hash : t -> int
   val hash_fold_t : t Hash.folder
   val t_of_sexp : Sexp.t -> t
   val sexp_of_t : t -> Sexp.t
   val pp : t pp
-  val true_ : t
-  val false_ : t
-  val of_bool : bool -> t
-  val is_true : t -> bool
-  val is_false : t -> bool
 end
 
-module Q : sig
-  include module type of struct include Q end
+module Z : sig
+  include module type of struct include Z end
 
-  val of_z : Z.t -> t
   val compare : t -> t -> int
   val hash : t -> int
   val hash_fold_t : t Hash.folder
   val t_of_sexp : Sexp.t -> t
   val sexp_of_t : t -> Sexp.t
   val pp : t pp
+  val true_ : t
+  val false_ : t
+  val of_bool : bool -> t
+  val is_true : t -> bool
+  val is_false : t -> bool
 end
-
-module String : sig
-  include module type of Base.String
-
-  type t = String.t [@@deriving compare, equal, hash, sexp]
-
-  module Map : Map.S with type key = string
-end
-
-type string = String.t [@@deriving compare, equal, hash, sexp]
-
-module Option = Option
-
-type 'a option = 'a Option.t [@@deriving compare, equal, hash, sexp]
-
-include module type of Option.Monad_infix
-include module type of Option.Monad_syntax with type 'a t = 'a option
-module Result = Base.Result
-
-module Array : sig
-  include module type of Base.Array
-
-  val pp : (unit, unit) fmt -> 'a pp -> 'a array pp
-end
-
-module IArray = IArray
-include module type of IArray.Infix
-module List = List
-
-type 'a list = 'a List.t [@@deriving compare, equal, hash, sexp]
-
-module Hash_queue = Core_kernel.Hash_queue
-module Set = Set
-module Hash_set = Base.Hash_set
-module Map = Map
-module Qset = Qset
-module Hashtbl = Base.Hashtbl
diff --git a/sledge/lib/import/import0.ml b/sledge/lib/import/import0.ml
index c210e7d05..d4b6bd125 100644
--- a/sledge/lib/import/import0.ml
+++ b/sledge/lib/import/import0.ml
@@ -5,41 +5,22 @@
  * LICENSE file in the root directory of this source tree.
  *)
 
-module Poly = struct
-  external ( = ) : 'a -> 'a -> bool = "%equal"
-  external ( <> ) : 'a -> 'a -> bool = "%notequal"
-  external ( < ) : 'a -> 'a -> bool = "%lessthan"
-  external ( > ) : 'a -> 'a -> bool = "%greaterthan"
-  external ( <= ) : 'a -> 'a -> bool = "%lessequal"
-  external ( >= ) : 'a -> 'a -> bool = "%greaterequal"
-  external compare : 'a -> 'a -> int = "%compare"
-  external equal : 'a -> 'a -> bool = "%equal"
-
-  let min x y = if x <= y then x else y
-  let max x y = if x >= y then x else y
-end
-
-external ( = ) : int -> int -> bool = "%equal"
-external ( <> ) : int -> int -> bool = "%notequal"
-external ( < ) : int -> int -> bool = "%lessthan"
-external ( > ) : int -> int -> bool = "%greaterthan"
-external ( <= ) : int -> int -> bool = "%lessequal"
-external ( >= ) : int -> int -> bool = "%greaterequal"
-
-let compare (a : int) b =
-  let int_of_bool (b : bool) = (Obj.magic b : int) in
-  int_of_bool (a > b) - int_of_bool (a < b)
-
-external equal : int -> int -> bool = "%equal"
-
-let min x y = if x <= y then x else y
-let max x y = if x >= y then x else y
-
-(** Tuple operations *)
-
-let fst3 (x, _, _) = x
-let snd3 (_, y, _) = y
-let trd3 (_, _, z) = z
+include (
+  Core :
+    sig
+      include
+        module type of Core
+          with module Printexc := Core.Printexc
+           and module Option := Core.Option
+           and module List := Core.List
+           and module Map := Core.Map
+           and module Set := Core.Set
+           and module String := Core.String
+           and type -'a return := 'a Core.return
+    end )
+
+external ( == ) : 'a -> 'a -> bool = "%eq"
+external ( != ) : 'a -> 'a -> bool = "%noteq"
 
 (** Function combinators *)
 
@@ -55,9 +36,6 @@ type 'a pp = Format.formatter -> 'a -> unit
 (** Format strings. *)
 type ('a, 'b) fmt = ('a, 'b) Trace.fmt
 
-module Hash = Ppx_hash_lib.Std.Hash
-module Sexp = Sexplib.Sexp
-
 module type Applicative_syntax = sig
   type 'a t
 
@@ -71,12 +49,3 @@ module type Monad_syntax = sig
   val ( let* ) : 'a t -> ('a -> 'b t) -> 'b t
   val ( and* ) : 'a t -> 'b t -> ('a * 'b) t
 end
-
-exception Duplicate
-
-module Return = struct type 'r t = {return: 'a. 'r -> 'a} [@@unboxed] end
-
-let with_return (type a) f =
-  let module M = struct exception Return of a end in
-  let return a = raise_notrace (M.Return a) in
-  try f {Return.return} with M.Return a -> a
diff --git a/sledge/lib/import/list.ml b/sledge/lib/import/list.ml
index d84beb559..35e46f128 100644
--- a/sledge/lib/import/list.ml
+++ b/sledge/lib/import/list.ml
@@ -6,7 +6,7 @@
  *)
 
 open Import0
-include Base.List
+include Core.List
 
 let rec pp ?pre ?suf sep pp_elt fs = function
   | [] -> ()
@@ -18,7 +18,9 @@ let rec pp ?pre ?suf sep pp_elt fs = function
       | xs -> Format.fprintf fs "%( %)%a" sep (pp sep pp_elt) xs ) ;
       Option.iter suf ~f:(Format.fprintf fs)
 
-let pop_exn = function x :: xs -> (x, xs) | [] -> raise Not_found
+let pop_exn =
+  let not_found = Not_found_s (Atom "pop_exn") in
+  function x :: xs -> (x, xs) | [] -> raise not_found
 
 let find_map_remove xs ~f =
   let rec find_map_remove_ ys = function
@@ -69,16 +71,18 @@ let rev_map_unzip xs ~f =
       let y, z = f x in
       (y :: ys, z :: zs) )
 
-let remove_exn ?(equal = ( == )) xs x =
-  let rec remove_ ys = function
-    | [] -> raise Not_found
-    | z :: xs ->
-        if equal x z then rev_append ys xs else remove_ (z :: ys) xs
-  in
-  remove_ [] xs
+let remove_exn =
+  let not_found = Not_found_s (Atom "remove_exn") in
+  fun ?(equal = phys_equal) xs x ->
+    let rec remove_ ys = function
+      | [] -> raise not_found
+      | z :: xs ->
+          if equal x z then rev_append ys xs else remove_ (z :: ys) xs
+    in
+    remove_ [] xs
 
 let remove ?equal xs x =
-  try Some (remove_exn ?equal xs x) with Not_found -> None
+  try Some (remove_exn ?equal xs x) with Not_found_s _ -> None
 
 let rec rev_init n ~f =
   if n = 0 then []
@@ -88,22 +92,22 @@ let rec rev_init n ~f =
     f n :: xs
 
 let symmetric_diff ~compare xs ys =
-  let rec symmetric_diff_ xxs yys =
+  let rec symmetric_diff_ xxs yys : _ Either.t list =
     match (xxs, yys) with
     | x :: xs, y :: ys ->
         let ord = compare x y in
         if ord = 0 then symmetric_diff_ xs ys
-        else if ord < 0 then `Left x :: symmetric_diff_ xs yys
-        else `Right y :: symmetric_diff_ xxs ys
-    | xs, [] -> map ~f:(fun x -> `Left x) xs
-    | [], ys -> map ~f:(fun y -> `Right y) ys
+        else if ord < 0 then First x :: symmetric_diff_ xs yys
+        else Second y :: symmetric_diff_ xxs ys
+    | xs, [] -> map ~f:Either.first xs
+    | [], ys -> map ~f:Either.second ys
   in
   symmetric_diff_ (sort ~compare xs) (sort ~compare ys)
 
 let pp_diff ~compare sep pp_elt fs (xs, ys) =
   let pp_diff_elt fs elt =
     match elt with
-    | `Left x -> Format.fprintf fs "-- %a" pp_elt x
-    | `Right y -> Format.fprintf fs "++ %a" pp_elt y
+    | First x -> Format.fprintf fs "-- %a" pp_elt x
+    | Second y -> Format.fprintf fs "++ %a" pp_elt y
   in
   pp sep pp_diff_elt fs (symmetric_diff ~compare xs ys)
diff --git a/sledge/lib/import/list.mli b/sledge/lib/import/list.mli
index af00b0831..6aa839ba3 100644
--- a/sledge/lib/import/list.mli
+++ b/sledge/lib/import/list.mli
@@ -5,8 +5,8 @@
  * LICENSE file in the root directory of this source tree.
  *)
 
-include module type of Base.List
 open Import0
+include module type of Core.List
 
 val pp :
      ?pre:(unit, unit) fmt
@@ -53,7 +53,4 @@ val remove : ?equal:('a -> 'a -> bool) -> 'a list -> 'a -> 'a list option
 val rev_init : int -> f:(int -> 'a) -> 'a list
 
 val symmetric_diff :
-     compare:('a -> 'a -> int)
-  -> 'a t
-  -> 'a t
-  -> [`Left of 'a | `Right of 'a] t
+  compare:('a -> 'a -> int) -> 'a t -> 'a t -> ('a, 'a) Either.t t
diff --git a/sledge/lib/import/map.ml b/sledge/lib/import/map.ml
index ea84a599b..1c826dc7f 100644
--- a/sledge/lib/import/map.ml
+++ b/sledge/lib/import/map.ml
@@ -5,6 +5,7 @@
  * LICENSE file in the root directory of this source tree.
  *)
 
+open Import0
 include Map_intf
 
 module Make (Key : sig
@@ -20,7 +21,7 @@ end) : S with type key = Key.t = struct
   let compare = compare_direct
 
   let to_map t =
-    Base.Map.Using_comparator.of_tree ~comparator:Key.comparator t
+    Core.Map.Using_comparator.of_tree ~comparator:Key.comparator t
 
   let of_map m = Base.Map.Using_comparator.to_tree m
 
@@ -51,7 +52,7 @@ end) : S with type key = Key.t = struct
       | k, `Unequal vv ->
           Format.fprintf fs "[@[%a@ @<2>↦ %a@]]" pp_key k pp_diff_val vv
     in
-    let sd = Core.Sequence.to_list (symmetric_diff ~data_equal x y) in
+    let sd = Sequence.to_list (symmetric_diff ~data_equal x y) in
     if not (List.is_empty sd) then
       Format.fprintf fs "[@[<hv>%a@]];@ " (List.pp ";@ " pp_diff_elt) sd
 end
diff --git a/sledge/lib/import/map_intf.ml b/sledge/lib/import/map_intf.ml
index ccc9c7bdc..d21cf6de1 100644
--- a/sledge/lib/import/map_intf.ml
+++ b/sledge/lib/import/map_intf.ml
@@ -13,7 +13,7 @@ module type S = sig
   module Key : sig
     type t = key
 
-    include Core.Comparator.S with type t := t
+    include Comparator.S with type t := t
   end
 
   include Core_kernel.Map_intf.Make_S_plain_tree(Key).S
diff --git a/sledge/lib/import/option.ml b/sledge/lib/import/option.ml
index 8c441ce56..ae9809664 100644
--- a/sledge/lib/import/option.ml
+++ b/sledge/lib/import/option.ml
@@ -5,7 +5,8 @@
  * LICENSE file in the root directory of this source tree.
  *)
 
-include Base.Option
+open! Import0
+include Core.Option
 
 let pp fmt pp_elt fs = function
   | Some x -> Format.fprintf fs fmt pp_elt x
diff --git a/sledge/lib/import/option.mli b/sledge/lib/import/option.mli
index 94886e0c8..f26895a0c 100644
--- a/sledge/lib/import/option.mli
+++ b/sledge/lib/import/option.mli
@@ -5,8 +5,8 @@
  * LICENSE file in the root directory of this source tree.
  *)
 
-open Import0
-include module type of Base.Option
+open! Import0
+include module type of Core.Option
 
 val pp : ('a_pp -> 'a -> unit, unit) fmt -> 'a_pp -> 'a option pp
 (** Pretty-print an option. *)
diff --git a/sledge/lib/import/set_intf.ml b/sledge/lib/import/set_intf.ml
index 8db56475b..65a421583 100644
--- a/sledge/lib/import/set_intf.ml
+++ b/sledge/lib/import/set_intf.ml
@@ -13,7 +13,7 @@ module type S = sig
   module Elt : sig
     type t = elt
 
-    include Core.Comparator.S with type t := t
+    include Comparator.S with type t := t
   end
 
   include Core_kernel.Set_intf.Make_S_plain_tree(Elt).S
diff --git a/sledge/lib/report.ml b/sledge/lib/report.ml
index 2f42f8c53..df0ea6a01 100644
--- a/sledge/lib/report.ml
+++ b/sledge/lib/report.ml
@@ -26,7 +26,7 @@ let count = ref 0
 let invalid_access_count () = !count
 
 let invalid_access fmt_thunk pp access loc =
-  incr count ;
+  Int.incr count ;
   let rep fs =
     Format.fprintf fs "%a Invalid memory access@;<1 2>@[%a@]" Loc.pp
       (loc access) pp access
diff --git a/sledge/lib/report.mli b/sledge/lib/report.mli
index 9c37995bc..941b268c6 100644
--- a/sledge/lib/report.mli
+++ b/sledge/lib/report.mli
@@ -8,6 +8,6 @@
 (** Issue reporting *)
 
 val unknown_call : Llair.term -> unit
-val invalid_access_inst : (Format.formatter -> unit) -> Llair.inst -> unit
-val invalid_access_term : (Format.formatter -> unit) -> Llair.term -> unit
+val invalid_access_inst : (Formatter.t -> unit) -> Llair.inst -> unit
+val invalid_access_term : (Formatter.t -> unit) -> Llair.term -> unit
 val invalid_access_count : unit -> int
diff --git a/sledge/lib/sh.ml b/sledge/lib/sh.ml
index 0e53ac0e9..d36ca44d6 100644
--- a/sledge/lib/sh.ml
+++ b/sledge/lib/sh.ml
@@ -644,7 +644,7 @@ let rec norm_ s q =
   [%Trace.call fun {pf} -> pf "@[%a@]@ %a" Equality.Subst.pp s pp_raw q]
   ;
   let q =
-    map q ~f_sjn:(norm_ s) ~f_cong:Fun.id ~f_trm:(Equality.Subst.subst s)
+    map q ~f_sjn:(norm_ s) ~f_cong:Fn.id ~f_trm:(Equality.Subst.subst s)
   in
   let xs, cong = Equality.apply_subst (Var.Set.union q.us q.xs) s q.cong in
   exists_fresh xs {q with cong}
diff --git a/sledge/lib/term.ml b/sledge/lib/term.ml
index c0582ab1b..b2bca8fc5 100644
--- a/sledge/lib/term.ml
+++ b/sledge/lib/term.ml
@@ -226,8 +226,8 @@ let assert_monomial mono =
   | Mul args ->
       Qset.iter args ~f:(fun factor exponent ->
           assert (Q.sign exponent > 0) ;
-          assert_indeterminate factor |> Fun.id )
-  | _ -> assert_indeterminate mono |> Fun.id
+          assert_indeterminate factor |> Fn.id )
+  | _ -> assert_indeterminate mono |> Fn.id
 
 (* a polynomial term is a monomial multiplied by a non-zero coefficient
  *     c × ∏ᵢ xᵢ
@@ -241,8 +241,8 @@ let assert_poly_term mono coeff =
       | None | Some (Integer _, _) -> assert false
       | Some (_, n) -> assert (Qset.length args > 1 || not (Q.equal Q.one n))
       ) ;
-      assert_monomial mono |> Fun.id
-  | _ -> assert_monomial mono |> Fun.id
+      assert_monomial mono |> Fn.id
+  | _ -> assert_monomial mono |> Fn.id
 
 (* a polynomial is a linear combination of monomials, e.g.
  *     ∑ᵢ cᵢ × ∏ⱼ xᵢⱼ
@@ -256,7 +256,7 @@ let assert_polynomial poly =
       | None | Some (Integer _, _) -> assert false
       | Some (_, k) -> assert (Qset.length args > 1 || not (Q.equal Q.one k))
       ) ;
-      Qset.iter args ~f:(fun m c -> assert_poly_term m c |> Fun.id)
+      Qset.iter args ~f:(fun m c -> assert_poly_term m c |> Fn.id)
   | _ -> assert false
 
 (* aggregate args of Extract and Concat must be aggregate terms, in
@@ -273,8 +273,8 @@ let invariant e =
   Invariant.invariant [%here] e [%sexp_of: t]
   @@ fun () ->
   match e with
-  | Add _ -> assert_polynomial e |> Fun.id
-  | Mul _ -> assert_monomial e |> Fun.id
+  | Add _ -> assert_polynomial e |> Fn.id
+  | Mul _ -> assert_monomial e |> Fn.id
   | Ap2 (Memory, _, _) | Ap3 (Extract, _, _, _) | ApN (Concat, _) ->
       assert_aggregate e
   | ApN (Record, elts) | RecN (Record, elts) ->
@@ -783,10 +783,10 @@ let simp_uno x y = Ap2 (Uno, x, y)
 
 let rec simp_eq x y =
   match
-    match Int.sign (compare x y) with
-    | Zero -> None
-    | Neg -> Some (x, y)
-    | Pos -> Some (y, x)
+    match Ordering.of_int (compare x y) with
+    | Equal -> None
+    | Less -> Some (x, y)
+    | Greater -> Some (y, x)
   with
   (* e = e ==> true *)
   | None -> bool true
@@ -929,24 +929,24 @@ let simp_update idx rcd elt = Ap2 (Update idx, rcd, elt)
 let rec_app key =
   let memo_id = Hashtbl.create key in
   let dummy = null in
-  fun ~id op elt_thks ->
-    match Hashtbl.find memo_id id with
-    | None ->
-        (* Add placeholder to prevent computing [elts] in calls to [rec_app]
-           from [elt_thks] for recursive occurrences of [id]. *)
-        let elta = Array.create ~len:(IArray.length elt_thks) dummy in
-        let elts = IArray.of_array elta in
-        Hashtbl.set memo_id ~key:id ~data:elts ;
-        IArray.iteri elt_thks ~f:(fun i (lazy elt) -> elta.(i) <- elt) ;
-        RecN (op, elts) |> check invariant
-    | Some elts ->
-        (* Do not check invariant as invariant will be checked above after
-           the thunks are forced, before which invariant-checking may
-           spuriously fail. Note that it is important that the value
-           constructed here shares the array in the memo table, so that the
-           update after forcing the recursive thunks also updates this
-           value. *)
-        RecN (op, elts)
+  Staged.stage
+  @@ fun ~id op elt_thks ->
+  match Hashtbl.find memo_id id with
+  | None ->
+      (* Add placeholder to prevent computing [elts] in calls to [rec_app]
+         from [elt_thks] for recursive occurrences of [id]. *)
+      let elta = Array.create ~len:(IArray.length elt_thks) dummy in
+      let elts = IArray.of_array elta in
+      Hashtbl.set memo_id ~key:id ~data:elts ;
+      IArray.iteri elt_thks ~f:(fun i (lazy elt) -> elta.(i) <- elt) ;
+      RecN (op, elts) |> check invariant
+  | Some elts ->
+      (* Do not check invariant as invariant will be checked above after the
+         thunks are forced, before which invariant-checking may spuriously
+         fail. Note that it is important that the value constructed here
+         shares the array in the memo table, so that the update after
+         forcing the recursive thunks also updates this value. *)
+      RecN (op, elts)
 
 (* dispatching for normalization and invariant checking *)
 
diff --git a/sledge/lib/term.mli b/sledge/lib/term.mli
index a03955f5b..69ea56977 100644
--- a/sledge/lib/term.mli
+++ b/sledge/lib/term.mli
@@ -224,11 +224,8 @@ val update : rcd:t -> idx:int -> elt:t -> t
 
 (* recursive n-ary application *)
 val rec_app :
-     (module Hashtbl.Key.S with type t = 'id)
-  -> id:'id
-  -> recN
-  -> t lazy_t iarray
-  -> t
+     (module Hashtbl.Key_plain with type t = 'id)
+  -> (id:'id -> recN -> t lazy_t iarray -> t) Staged.t
 
 val size_of : Typ.t -> t