|
|
|
|
(*
|
|
|
|
|
* 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.
|
|
|
|
|
*)
|
|
|
|
|
|
|
|
|
|
(** Arithmetic terms *)
|
|
|
|
|
|
|
|
|
|
include module type of Arithmetic_intf
|
|
|
|
|
|
[sledge] Rework term and arithmetic definitions to avoid recursive modules
Summary:
Terms include Arithmetic terms, which are polynomials over terms
themselves. Monomials are represented as maps from
terms (multiplicative factors) to integers (their powers). Polynomials
are represented as maps from monomials (indeterminates) to
rationals (coefficients). In particular, terms are represented using
maps whose keys are terms themselves. This is currently implemented
using recursive modules.
This diff uses the Comparer-based interface of Maps to express this
cycle as recursive *types* rather than recursive *modules*, see the
very beginning of trm.ml. The rest of the changes are driven by the
need to expose the Arithmetic.t type at toplevel, outside the functor
that defines the arithmetic operations, and changes to stage the
definition of term and polynomial operations to remove unnecessary
recursion.
One might hope that these changes are just moving code around, but due
to how recursive modules are implemented, this refactoring is
motivated by performance profiling. In every cycle between recursive
modules, at least one of the modules must be "safe". A "safe" module
is one where all exposed values have function type. This allows the
compiler to initialize that module with functions that immediately
raise an exception, define the other modules using it, and then tie
the recursive knot by backpatching the safe module with the actual
functions at the end. This implementation works, but has the
consequence that the compiler must treat calls to functions of safe
recursive modules as indirect calls to unknown functions. This means
that they are not inlined or even called by symbol, and instead
calling them involves spilling registers if needed, loading their
address from memory, calling them by address, and restoring any
spilled registers. For operations like Trm.compare that are a handful
of instructions on the hot path, this is a significant
difference. Since terms are the keys of maps and sets in the core of
the first-order equality solver, those map operations are very very
hot.
Reviewed By: jvillard
Differential Revision: D26250533
fbshipit-source-id: f79334c68
4 years ago
|
|
|
(** Arithmetic terms, e.g. polynomials, polymorphic in the type of
|
|
|
|
|
indeterminates. *)
|
|
|
|
|
type ('trm, 'cmp) t [@@deriving compare, equal, sexp]
|
|
|
|
|
|
|
|
|
|
(** Functor that, given a totally ordered type of indeterminate terms,
|
|
|
|
|
builds an implementation of the embedding-independent arithmetic
|
|
|
|
|
operations, and a functor that, given an embedding of arithmetic terms
|
|
|
|
|
into indeterminate terms, builds an implementation of the arithmetic
|
|
|
|
|
operations. *)
|
|
|
|
|
module Make (Ord : sig
|
|
|
|
|
type t [@@deriving equal, sexp]
|
|
|
|
|
|
|
|
|
|
include Comparer.S with type t := t
|
|
|
|
|
end) : sig
|
|
|
|
|
include S0 with type t = (Ord.t, Ord.compare) t with type trm := Ord.t
|
|
|
|
|
|
|
|
|
|
module Embed
|
|
|
|
|
(Var : Var_intf.S)
|
|
|
|
|
(Trm : TRM with type t = Ord.t with type var := Var.t)
|
|
|
|
|
(_ : EMBEDDING with type trm := Trm.t and type t := t) :
|
|
|
|
|
S with type trm := Trm.t with type t = t
|
|
|
|
|
end
|
