|
|
|
(*
|
|
|
|
* 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.
|
|
|
|
*)
|
|
|
|
|
|
|
|
open! NS0
|
|
|
|
include module type of Base.List
|
|
|
|
|
|
|
|
val pp :
|
|
|
|
?pre:(unit, unit) fmt
|
|
|
|
-> ?suf:(unit, unit) fmt
|
|
|
|
-> (unit, unit) fmt
|
|
|
|
-> 'a pp
|
|
|
|
-> 'a list pp
|
|
|
|
(** Pretty-print a list. *)
|
|
|
|
|
|
|
|
val pp_diff :
|
|
|
|
compare:('a -> 'a -> int)
|
|
|
|
-> (unit, unit) fmt
|
|
|
|
-> 'a pp
|
|
|
|
-> ('a list * 'a list) pp
|
|
|
|
|
[sledge] Represent recursive records non-recursively
Summary:
In LLVM it is possible for struct constant values to be directly
recursive, with no pointer dereference to close the cycle. These
appear for example as the values of vtables from C++ code.
Currently such recursive records in the Exp and Term languages are
represented as genuinely cyclic values. Compared to a standard term
representation, the presence of cyclic values is a significant
complication everywhere. Since the backend solver does not do anything
such as induction over these, they have to be treated as essentially
atomic.
This patch changes the representation to a standard non-recursive tree
term structure. Instead of cyclic references, an explicit constructor
is added for the "non-tree edges", which simply indicates which
ancestor record value to which the recursive reference points.
There is a potential issue with this representation, since for
mutually recursive records, the representation is not canonical: it
chooses one of the records in the cycle to start from and expresses
the cycles relative to that. Currently the choice of representation is
dictated by the frontend. For the case of vtables, the frontend
translates globals in the same order they appear in the LLVM IR, so
the representation choice is fixed.
It may turn out that other potential uses require more reasoning
support in the backend solver, which would involve a theory of
equality of record values induced by equating the representations
resulting from different rotations of the cycle of records.
Reviewed By: jvillard
Differential Revision: D21441533
fbshipit-source-id: 0c5a11378
5 years ago
|
|
|
val findi : 'a -> 'a t -> int option
|
|
|
|
(** [findi x xs] is [Some i] when [nth xs i == x], otherwise [None]. *)
|
|
|
|
|
|
|
|
val pop_exn : 'a list -> 'a * 'a list
|
|
|
|
|
|
|
|
val find_map_remove :
|
|
|
|
'a list -> f:('a -> 'b option) -> ('b * 'a list) option
|
|
|
|
|
|
|
|
val fold_option :
|
|
|
|
'a t -> init:'accum -> f:('accum -> 'a -> 'accum option) -> 'accum option
|
|
|
|
(** [fold_option t ~init ~f] is a short-circuiting version of [fold] that
|
|
|
|
runs in the [Option] monad. If [f] returns [None], that value is
|
|
|
|
returned without any additional invocations of [f]. *)
|
|
|
|
|
|
|
|
val map_endo : 'a t -> f:('a -> 'a) -> 'a t
|
|
|
|
(** Like map, but specialized to require [f] to be an endofunction, which
|
|
|
|
enables preserving [==] if [f] preserves [==] of every element. *)
|
|
|
|
|
|
|
|
val rev_map_unzip : 'a t -> f:('a -> 'b * 'c) -> 'b list * 'c list
|
|
|
|
(** [rev_map_unzip ~f xs] is [unzip (rev_map ~f xs)] but more efficient. *)
|
|
|
|
|
|
|
|
val remove_exn : ?equal:('a -> 'a -> bool) -> 'a list -> 'a -> 'a list
|
|
|
|
(** Returns the input list without the first element [equal] to the
|
|
|
|
argument, or raise [Not_found_s] if no such element exists. [equal]
|
|
|
|
defaults to physical equality. *)
|
|
|
|
|
|
|
|
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 -> ('a, 'a) Either.t t
|